(* Author: *)
theory Day1_Extras
imports Day1
begin
subsection{* Extra tricks *}
text{* Here we describe some low-level proof-manipulation that you might find in the libraries of
Isabelle. We do not encourage their use as they obfuscate the content of the proofs for other
readers. These subsection is not meant to be explained in the lecture. *}
text{* Sometimes Isabelle has in its libraries the theorems @{term "P \ Q"} and @{term "Q \ R"},
but you need the related result @{term "P \ R"}. Instead of adding it as a lemma, you can
concatenate them with the THEN or OF modifiers: *}
lemma
assumes fact1: "P \ Q"
and fact2: "Q \ R"
shows "P \ R"
apply(drule fact2[OF fact1])
\ \Check the content of "fact2[OF fact1]" with @{command thm} inside the proof.\
thm fact2[OF fact1]
apply assumption
done
lemma
assumes fact1: "P \ Q"
and fact2: "Q \ R"
shows "P \ R"
using fact1[THEN fact2]
apply assumption
done
text{* Prove the following results concatenating the rules ``allE, allI, conjE, and conjI''. Use
both methods of concatenation, one for each proof (you may need to use Skolem variables):*}
lemma "(\x. P x) \ (P x \ R) \ R"
oops
lemma "(\x. P x) \ (P x \ R) \ R"
oops
lemma "P \ Q \ (P \ Q \ R) \ R"
oops
lemma "P \ Q \ (P \ Q \ R) \ R"
oops
text{* Isabelle fails to understand the proof that we want her to do next. You already know at least
two ways to fix this WITHOUT adding an extra line. Correct the proof: *}
lemma "P \ Q \ A \ B \ A"
apply(erule conjE)
apply assumption
done
oops
text{* In the prvious proof, you can tell Isabelle she is picking the wrong assumption by using
@{command back} as below. This approach is NOT favored over your proof above: *}
lemma "\ P \ Q; A \ B \ \ A"
apply(erule conjE)
back \ \Isabelle! You picked the wrong one!\
apply(assumption)
done
text{* When using @{command by}, you can separate them with parenthesis: *}
lemma "P \ Q \ P \ R"
by (rule disjI1) (erule conjE)
text{* Prove the following lemma twice using only the theorems @{thm subst} and @{thm sym}. Try to
shorten its proof to only one line. Use two different previously learned shortening methods, one in
each proof. *}
lemma "t = s \ P s \ P t"
oops
lemma "t = s \ P s \ P t"
oops
text{* Isabelle can sometimes deduce the rule to apply next. You just need to type ``apply rule'':*}
lemma "A \ B \ C \ A \ B \ C"
apply rule \ \Not recommended when the rule is not obvious from context\
apply assumption
apply rule
apply assumption+
done
text{* You can indicate Isabelle the rule to apply by using the command @{command declare}, the
theorem and its argument ``intro''. For example: *}
declare xorI2 [intro] \ \You might need to prove the lemma first.\
text{* Test this, prove the following theorem starting with ``apply rule'': *}
lemma "\ P \ Q \ xor P Q"
oops
text{* Finally, there are abbreviations for finishing your proof, specifically: ``. = by assumption''
and ``.. = by rule''. Test this yourself. Prove the following lemmas. Avoid any line separating
them. Which one should be proved ``by assumption'' and which one ``by rule''?: *}
lemma "P \ P"
oops
lemma "\ P \ Q \ xor P Q"
oops
text{* Study the output generated by the following proof by moving the red cursor to the end of each
line, one by one. Then answer the questions: *}
lemma
assumes First and Second and Third and fourth:Fourth
shows "((Fourth \ Third) \ Second) \ First"
apply(rule conjI)+
prefer 4
using assms(1)
\ \Check @{thm assms} and its arguments (1, 2, 3 or 4) by playing with the next line:\
thm assms
apply assumption
prefer 3
using `Second`
apply assumption
defer
using \Third\
apply assumption
using fourth
by assumption
\ \What does @{command prefer} do?\
(* you may type your answer here *)
\ \What does @{command defer} do?\
(* you may type your answer here *)
\ \What are the three methods to reference unnamed assumptions in a proof?\
(* you may type your answer here *)
\ \Can we use "assms" and two arguments to refer to two assumptions?\
(* you may type your answer here *)
text{* Study the output generated by the following proof by moving the red cursor to the end of each
line, one by one. What do we use the command @{command subgoal} for? *}
(* you may type your answer here *)
lemma
assumes P and "\x. Q x"
shows "P \ (\x. Q x)"
apply(rule conjI)+
subgoal
using assms(1)
.
apply(rule allI)
subgoal for x \ \What happens if you delete the ``for x'' part?\
(* you may type your answer here *)
using assms(2)[of x] \ \Another way to call Skolem variables when they've been made explicit.\
by assumption
done
\ \Study the proof below, then change the arguments so that they talk about x, y and z (instead of
a, b and c).\
lemma (in ord)
"\ m n. \ n. n > m \ \n1 n2 n3. n1 < n2 \ n2 < n3 \ n1 < n3 \ m > n \ \z > m. z > n"
apply(erule exE)
apply(rename_tac y x z)
apply(erule_tac x="x" in allE)
apply(erule_tac x="y" in allE)
apply(erule_tac x=z in allE)
apply(drule mp, assumption)+
apply(rule_tac x=z in exI)
by(rule conjI)
text{* Study the proof below, then complete it by deleting all the remaining unnecessary
premises in the subgoal: *}
lemma "Betty Botter bought butter \ butter bitter \ put it batter \ batter bitter \
but a bit better butter \ batter better \ batter bitter"
apply(thin_tac "Betty _ _ _") (* REMOVE *)
apply(thin_tac "butter _")
oops
text{* You can add theorems to the simplifier with @{command declare}: *}
lemma xor_TrueI: "(P \ \ P) = True"
unfolding xor_iff by simp
lemma xor_FalseI: "(P \ P) = False"
unfolding xor_def2 by simp
lemma xor_conmute:"(P \ Q) = (Q \ P)"
sorry \ \Prove this theorem appropiately. \
declare xor_TrueI [simp]
and xor_FalseI [simp]
and xor_conmute [simp]
\ \Alternatively, you can add theorems to the simplifier directly when declaring them:\
lemma xor_TrueE[simp]: "(P \ True) = (\ P)"
sorry \ \Prove this theorem appropiately. \
lemma xor_FalseE[simp]: "(P \ False) = P"
sorry \ \Prove this theorem appropiately. \
text{* By adding the wrong theorems, you may create infinite loops with simp. A good rule of thumb
is to only add local equalities (within a class or a locale --see respective session--) and guarantee
that the right hand side is "simpler" than the left hand side.*}
text{* You can also delete theorems from the simplifier with @{command declare}. Notice how the next
proof is not finished. Then uncomment the line below and observe any changes in Output. *}
(* declare xor_conmute [simp del] *)
lemma "(P \ (\ True)) = (P)"
apply simp
oops
\ \You can control the power of the simplifier with the modifiers "add, only, del, no_asm, and
split". \
lemma xor_assoc:"(P \ Q \ R) = ((P \ Q) \ R)"
oops \ \Prove but instead of using "unfolding", use "simp add:" like below\
lemma
assumes "(f \ g) P = R"
shows "R \ ((f \ g) P) = False"
apply(simp add: assms) \ \Correct this proof. Instead of "add" write "only"\
by simp
declare xor_conmute [simp]
lemma "(P \ (\ True)) = (P)"
oops \ \Prove again but by removing xor_conmute with simp del\
declare xor_conmute [simp del]
lemma "(f \ g) P = R \ R \ ((f \ g) P) = False"
apply(simp (no_asm)) \ \simplifier won't attack the premises\
by simp
lemma "(case n of 0 \ 1 | (Suc n) \ (Suc (Suc n))) = Suc n"
apply(simp split: nat.split) \ \used for datatype ``cases'' (upcoming session)\
done
lemma
assumes "f P = Q"
shows "P \ (\ P)" "Q \ f P"
apply(auto simp: ) \ \Add the appropriate fact to the simplifier so that auto proves this lemma.\
oops
lemma
fixes x::real
assumes "(x < y) \ (X x) \ (Y y)"
and "\ x \ y" and "x \ y"
shows "(X x) \ (Y y)"
using assms(2,3) by (force intro: assms(1))
\ \Many different proofs with the same ingredients won't work. It is important that we indicated
that assumption 1 should be used as an intro-rule while the others don't. \
end