(****************************************************************************)
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