(****************************************************************************) chapter {* Automated Reasoning Course Jacques Fleuriot Propositional Logic in Isabelle *} (****************************************************************************) theory Prop imports Main begin (****************************************************************************) section {* Introduction *} text {* This Isabelle theory file accompanies Lectures 2-4 of the Automated Reasoning course. By stepping through it you should become familiar with how to undertake propositional logic proofs in Isabelle. *} (****************************************************************************) section {* First theorems *} theorem K: "A \ B \ A" apply (rule impI) apply (rule impI) apply assumption done text {* The rules "impI" and "assumption" above are examples of Isabelle proof methods. After processing "done" above, the front-end will display a version of the theorem with the A and B replaced by ?A and ?B. These are schematic or meta variables that can be freely instantiated if theorem K is used in some further proof. Theorems can involve assumptions from the start. For example, here is the Isabelle version of the natural deduction derivation of A, B \ A \ (B \ A) *} theorem a_conj_theorem: "\ A ; B \ \ A \ (B \ A)" apply (rule conjI) apply assumption apply (rule conjI) apply assumption apply assumption done text {* We can add "+" to the end of a method in order to apply it more than once. We can also use the keyword "by" instead of "apply" for the final line of the proof. This allows us to discard the "done". So, the same theorem can be proved as follows: *} theorem a_conj_theorem2: "\ A ; B \ \ A \ (B \ A)" apply (rule conjI) apply assumption apply (rule conjI) by assumption+ (****************************************************************************) section {* More On Applying Rules *} text {* A simple propositional fact is B \ A from the assumption A \ B. In Isabelle, this lemma can be proved as follows: *} lemma "A \ B \ B \ A" apply (erule disjE) apply (rule disjI2) apply assumption apply (rule disjI1) by assumption text {* It is instructive to see what happens when we apply a rule backward such that not all of its variables can be immediately instantiated. Look at what happens below after "rule disjE". We get schematic variables in both subgoals that then are instantiated once we apply the assumption method on the 1st subgoal. *} lemma "A \ B \ B \ A" apply (rule disjE) apply assumption apply (rule disjI2) apply assumption apply (rule disjI1) by assumption (****************************************************************************) section {* More Methods *} text {* Isabelle also provides the methods "drule" and "frule" for forwards reasoning. These are best used with destruction rules. For example: *} lemma "A \ B \ A" apply (drule conjunct1) by assumption lemma "A \ B \ A" apply (frule conjunct1) by assumption (****************************************************************************) section {* Problems Revisited *} text{* We can now return to the three problems first posed in Lecture 2. The written proof of Example 1 is shown in Lecture 3. Its equivalent Isabelle proof is: *} lemma example1: "(SunnyTomorrow \ RainyTomorrow) \ \SunnyTomorrow \ RainyTomorrow" apply (rule impI) apply (erule conjE) apply (erule disjE) apply (erule notE) by assumption+ text{* The proofs of Examples 2 and 3 are: *} lemma example2: "(Class \ Pop) \ (Class \ Soph) \ \Pop \ Soph" apply (rule impI) apply (erule conjE)+ apply (erule disjE) apply (erule impE) apply assumption+ apply (erule notE) by assumption lemma example3: "(M \ L) \ (M \ W) \ \(L \ W) \ M \ (M \ L) \ (M \ W)" apply (rule impI) apply (erule conjE)+ apply (erule disjE) apply (erule disjE) apply (rule disjI1) apply assumption apply (rule disjI1) apply assumption apply (erule disjE) apply (rule disjI1) apply assumption apply (erule notE) apply (rule conjI) by assumption+ (*****************************************************************************) section {* Applying Rules to Correct Assumptions *} text {* Consider the following lemma and proof: *} lemma conj_elim1: "\ A \ B; C \ D \ \ D" apply (erule conjE) apply (erule conjE) by assumption text {* Notice that in this proof we had to apply the rule "conjE" twice in order to eliminate the conjunction in the second assumption. We could have avoided writing the extra proof step by using "+": *} lemma conj_elim2: "\ A \ B; C \ D \ \ D" apply (erule conjE)+ by assumption text {* Although this new proof is shorter, we have still carried out an unnecessary step: we do not need to eliminate the conjunction in the first assumption. If we want to apply "conjE" to a an assumption different from the first one it matches, then we can rotate the ordering of our assumptions. To do this Isabelle provides a tactic called "rotate_tac". An alternative proof is thus: *} lemma conj_elim3: "\ A \ B; C \ D \ \ D" apply (rotate_tac 1) apply (erule conjE) by assumption text {* If our list of assumptions is very large, we may not want to use "rotate_tac". A better approach is to explicitly tell Isabelle what instantiations the variables in a rule should take when we apply it. To do this we use the methods "rule_tac", "erule_tac", "drule_tac" and "frule_tac". Our alternative proof of "conj_elim" is: *} lemma conj_elim4: "\ A \ B; C \ D \ \ D" apply (erule_tac P=C and Q=D in conjE) by assumption text {* In the above proof it is not neccessary to tell Isabelle the variable Q in the rule "conjE" should be instantiated to D. Isabelle can automatically infer this! So our proof becomes: *} lemma conj_elim5: "\ A \ B; C \ D \ \ D" apply (erule_tac P=C in conjE) by assumption (*****************************************************************************) section{* More Rules of the Game *} text {* If you start proving a lemma but get stuck, you can always type the command "oops" to abandon the proof. For example: *} lemma A_and_B_imp_B_or_A: "A \ B \ B \ A" oops text {* Now imagine we want to use A \ B \ B \ A to prove later lemmas and theorems. As it is not a rule (since it does not have the \) we use it by inserting it as an assumption in our proof. This is done using a tactic called "cut_tac". Consider the following lemma and try uncommenting the "apply" command. *} lemma "A \ B \ B \ A" (* apply (cut_tac A_and_B_imp_B_or_A)*) (* Isabelle complains! *) oops text {* When we try to insert A \ B \ B \ A into our proof Isabelle complains. This is because Isabelle does not know the theorem. The command "oops" allowed us to abandon our proof, but it also told Isabelle to forget the lemma completely. To allow Isabelle to continue checking this theory, comment out again the "apply" command above. Instead of using "oops", we could have used the command "sorry": *} lemma A_and_B_imp_B_or_A_take2: "A \ B \ B \ A" sorry text {* The command "sorry" tells Isabelle to abandon the proof but pretend that the lemma has been proved. This allows us to use it in later proofs: *} lemma cut_in_action: "A \ B \ B \ A" apply (cut_tac A_and_B_imp_B_or_A_take2) apply (erule impE) apply assumption+ done text {* A word of warning: "sorry" is a cheat allowing you to make progress. You should return to the incomplete proof and finish it to be completely sure the rest of your theory is valid. *} (*****************************************************************************) section {* Automation *} text{* It may seem tedious having to type in all these commands. Isabelle does provide a fair amount of automation. The tactics "simp" and "auto" both use the classical reasoner of Isabelle and can make life a lot easier. Example: *} lemma proved_by_simp: "A \ B \ B \ A" by simp lemma proved_by_auto: "A \ B \ B \ A" by auto end