summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 23 Oct 2000 16:25:04 +0200 | |

changeset 10295 | 8eb12693cead |

parent 10294 | 2ec9c808a8a7 |

child 10296 | 0c5907082459 |

the Rules chapter and theories

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Rules/Basic.thy Mon Oct 23 16:25:04 2000 +0200 @@ -0,0 +1,290 @@ +theory Basic = Main: + +lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)" +apply (rule conjI) + apply assumption +apply (rule conjI) + apply assumption +apply assumption +done + + +lemma disj_swap: "P | Q \<Longrightarrow> Q | P" +apply (erule disjE) + apply (rule disjI2) + apply assumption +apply (rule disjI1) +apply assumption +done + +lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P" +apply (rule conjI) + apply (drule conjunct2) + apply assumption +apply (drule conjunct1) +apply assumption +done + +lemma imp_uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R" +apply (rule impI) +apply (erule conjE) +apply (drule mp) + apply assumption +apply (drule mp) + apply assumption + apply assumption +done + +text {* +substitution + +@{thm[display] ssubst} +\rulename{ssubst} +*}; + +lemma "\<lbrakk> x = f x; P(f x) \<rbrakk> \<Longrightarrow> P x" +apply (erule ssubst) +apply assumption +done + +text {* +also provable by simp (re-orients) +*}; + +lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x" +apply (erule ssubst) +back +back +back +back +apply assumption +done + +text {* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}x\ {\isacharequal}\ f\ x{\isacharsemicolon}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ x\ x\isanewline +\ \isadigit{1}{\isachardot}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright} + +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}x\ {\isacharequal}\ f\ x{\isacharsemicolon}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ x\ x\isanewline +\ \isadigit{1}{\isachardot}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x\ {\isasymLongrightarrow}\ P\ x\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright} + +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}x\ {\isacharequal}\ f\ x{\isacharsemicolon}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ x\ x\isanewline +\ \isadigit{1}{\isachardot}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ x\ {\isacharparenleft}f\ x{\isacharparenright} + +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}x\ {\isacharequal}\ f\ x{\isacharsemicolon}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ x\ x\isanewline +\ \isadigit{1}{\isachardot}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x\ {\isasymLongrightarrow}\ P\ x\ x\ {\isacharparenleft}f\ x{\isacharparenright} + +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}x\ {\isacharequal}\ f\ x{\isacharsemicolon}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ x\ x\isanewline +\ \isadigit{1}{\isachardot}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}f\ x{\isacharparenright}\ x +*}; + +lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x" +apply (erule ssubst, assumption) +done + +lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x" +apply (erule_tac P="\<lambda>u. P u u x" in ssubst); +apply assumption +done + + +text {* +negation + +@{thm[display] notI} +\rulename{notI} + +@{thm[display] notE} +\rulename{notE} + +@{thm[display] classical} +\rulename{classical} + +@{thm[display] contrapos_pp} +\rulename{contrapos_pp} + +@{thm[display] contrapos_np} +\rulename{contrapos_np} + +@{thm[display] contrapos_nn} +\rulename{contrapos_nn} +*}; + + +lemma "\<lbrakk>\<not>(P\<longrightarrow>Q); \<not>(R\<longrightarrow>Q)\<rbrakk> \<Longrightarrow> R" +apply (erule_tac Q="R\<longrightarrow>Q" in contrapos_np) +txt{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}{\isasymnot}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isacharsemicolon}\ {\isasymnot}\ {\isacharparenleft}R\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ R\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}{\isasymnot}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isacharsemicolon}\ {\isasymnot}\ R{\isasymrbrakk}\ {\isasymLongrightarrow}\ R\ {\isasymlongrightarrow}\ Q +*} + +apply intro +txt{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{3}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}{\isasymnot}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isacharsemicolon}\ {\isasymnot}\ {\isacharparenleft}R\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ R\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}{\isasymnot}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isacharsemicolon}\ {\isasymnot}\ R{\isacharsemicolon}\ R{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q +*} +apply (erule notE, assumption) +done + + +lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R" +apply intro +txt{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isasymand}\ R\ {\isasymLongrightarrow}\ P\ {\isasymor}\ Q\ {\isasymand}\ R\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isasymand}\ R{\isacharsemicolon}\ {\isasymnot}\ {\isacharparenleft}Q\ {\isasymand}\ R{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P +*} + +apply (elim conjE disjE) + apply assumption + +txt{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{4}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isasymand}\ R\ {\isasymLongrightarrow}\ P\ {\isasymor}\ Q\ {\isasymand}\ R\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}{\isasymnot}\ {\isacharparenleft}Q\ {\isasymand}\ R{\isacharparenright}{\isacharsemicolon}\ R{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P +*} + +apply (erule contrapos_np, rule conjI) +txt{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{6}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isasymand}\ R\ {\isasymLongrightarrow}\ P\ {\isasymor}\ Q\ {\isasymand}\ R\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ R +*} + + apply assumption + apply assumption +done + + + +text{*Quantifiers*} + +lemma "\<forall>x. P x \<longrightarrow> P x" +apply (rule allI) +apply (rule impI) +apply assumption +done + +lemma "(\<forall>x. P \<longrightarrow> Q x) \<Longrightarrow> P \<longrightarrow> (\<forall>x. Q x)" +apply (rule impI) +apply (rule allI) +apply (drule spec) +apply (drule mp) + apply assumption + apply assumption +done + +lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (f x); P a\<rbrakk> \<Longrightarrow> P(f (f a))" +apply (frule spec) +apply (drule mp, assumption) +apply (drule spec) +apply (drule mp, assumption, assumption) +done + +text +{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymlongrightarrow}\ P\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharsemicolon}\ P\ a{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ a{\isacharparenright}{\isacharparenright}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymlongrightarrow}\ P\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharsemicolon}\ P\ a{\isacharsemicolon}\ P\ {\isacharquery}x\ {\isasymlongrightarrow}\ P\ {\isacharparenleft}f\ {\isacharquery}x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ a{\isacharparenright}{\isacharparenright} +*} + +text{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{3}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymlongrightarrow}\ P\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharsemicolon}\ P\ a{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ a{\isacharparenright}{\isacharparenright}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymlongrightarrow}\ P\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharsemicolon}\ P\ a{\isacharsemicolon}\ P\ {\isacharparenleft}f\ a{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ a{\isacharparenright}{\isacharparenright} +*} + +lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (f x); P a\<rbrakk> \<Longrightarrow> P(f (f a))" +by blast + +lemma "(\<exists>x. P x) \<or> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<or> Q x" +apply elim + apply intro + apply assumption +apply (intro exI disjI2) (*or else we get disjCI*) +apply assumption +done + +lemma "(P\<longrightarrow>Q) \<or> (Q\<longrightarrow>P)" +apply intro +apply elim +apply assumption +done + +lemma "(P\<or>Q)\<and>(P\<or>R) \<Longrightarrow> P \<or> (Q\<and>R)" +apply intro +apply (elim conjE disjE) +apply blast +apply blast +apply blast +apply blast +(*apply elim*) +done + +lemma "(\<exists>x. P \<and> Q x) \<Longrightarrow> P \<and> (\<exists>x. Q x)" +apply (erule exE) +apply (erule conjE) +apply (rule conjI) + apply assumption +apply (rule exI) + apply assumption +done + +lemma "(\<exists>x. P x) \<and> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<and> Q x" +apply (erule conjE) +apply (erule exE) +apply (erule exE) +apply (rule exI) +apply (rule conjI) + apply assumption +oops + +lemma "\<forall> z. R z z \<Longrightarrow> \<exists>x. \<forall> y. R x y" +apply (rule exI) +apply (rule allI) +apply (drule spec) +oops + +lemma "\<forall>x. \<exists> y. x=y" +apply (rule allI) +apply (rule exI) +apply (rule refl) +done + +lemma "\<exists>x. \<forall> y. x=y" +apply (rule exI) +apply (rule allI) +oops + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Rules/Blast.thy Mon Oct 23 16:25:04 2000 +0200 @@ -0,0 +1,40 @@ +theory Blast = Main: + +lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y)))) = + ((\<exists>x. \<forall>y. q(x)=q(y)) = ((\<exists>x. p(x))=(\<forall>y. q(y))))" +apply blast +done + +text{*\noindent Until now, we have proved everything using only induction and +simplification. Substantial proofs require more elaborate types of +inference.*} + +lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and> + \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and> + (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and> + (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and> + (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x)) + \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"; +apply blast +done + +lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) = + (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))" +apply blast +done + +text {* +@{thm[display] mult_is_0} + \rulename{mult_is_0}} + +@{thm[display] finite_Un} + \rulename{finite_Un}} +*}; + + +lemma [iff]: "(xs@ys = []) = (xs=[] & ys=[])" + apply (induct_tac xs) + by (simp_all); + +(*ideas for uses of intro, etc.: ex/Primes/is_gcd_unique?*) +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Rules/Force.thy Mon Oct 23 16:25:04 2000 +0200 @@ -0,0 +1,41 @@ +theory Force = Main: + + + +lemma "(\<forall>x. P x) \<and> (\<exists>x. Q x) \<longrightarrow> (\<forall>x. P x \<and> Q x)" +apply clarify +oops + +text {* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ Q\ x{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ xa{\isachardot}\ {\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x{\isacharsemicolon}\ Q\ xa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ {\isasymand}\ Q\ x +*}; + +text {* +couldn't find a good example of clarsimp + +@{thm[display]"someI"} +\rulename{someI} +*}; + +lemma "\<lbrakk>Q a; P a\<rbrakk> \<Longrightarrow> P (SOME x. P x \<and> Q x) \<and> Q (SOME x. P x \<and> Q x)" +apply (rule someI) +oops + +lemma "\<lbrakk>Q a; P a\<rbrakk> \<Longrightarrow> P (SOME x. P x \<and> Q x) \<and> Q (SOME x. P x \<and> Q x)" +apply (fast intro!: someI) +done + +text{* +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline +\isanewline +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline +{\isasymlbrakk}Q\ a{\isacharsemicolon}\ P\ a{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}SOME\ x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\ {\isasymand}\ Q\ {\isacharparenleft}SOME\ x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\isanewline +\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}Q\ a{\isacharsemicolon}\ P\ a{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharquery}x\ {\isasymand}\ Q\ {\isacharquery}x +*} + +end +

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Rules/Primes.thy Mon Oct 23 16:25:04 2000 +0200 @@ -0,0 +1,351 @@ +(* EXTRACT from HOL/ex/Primes.thy*) + +theory Primes = Main: +consts + gcd :: "nat*nat=>nat" (*Euclid's algorithm *) + +recdef gcd "measure ((\<lambda>(m,n).n) ::nat*nat=>nat)" + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" + + +ML "Pretty.setmargin 64" +ML "IsarOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*) + + +text {* +\begin{quote} +@{thm[display]"dvd_def"} +\rulename{dvd_def} +\end{quote} +*}; + + +(*** Euclid's Algorithm ***) + +lemma gcd_0 [simp]: "gcd(m,0) = m" + apply (simp); + done + +lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd(m,n) = gcd (n, m mod n)" + apply (simp) + done; + +declare gcd.simps [simp del]; + +(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) +lemma gcd_dvd_both: "(gcd(m,n) dvd m) \<and> (gcd(m,n) dvd n)" + apply (induct_tac m n rule: gcd.induct) + apply (case_tac "n=0") + apply (simp_all) + apply (blast dest: dvd_mod_imp_dvd) + done + + +text {* +@{thm[display] dvd_mod_imp_dvd} +\rulename{dvd_mod_imp_dvd} + +@{thm[display] dvd_trans} +\rulename{dvd_trans} + +\begin{isabelle} +proof\ (prove):\ step\ 3\isanewline +\isanewline +goal\ (lemma\ gcd_dvd_both):\isanewline +gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n\isanewline +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk 0\ <\ n;\ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ gcd\ (n,\ m\ mod\ n)\ dvd\ m +\end{isabelle} +*}; + + +lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1] +lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]; + + +text {* +\begin{quote} +@{thm[display] gcd_dvd1} +\rulename{gcd_dvd1} + +@{thm[display] gcd_dvd2} +\rulename{gcd_dvd2} +\end{quote} +*}; + +(*Maximality: for all m,n,k naturals, + if k divides m and k divides n then k divides gcd(m,n)*) +lemma gcd_greatest [rule_format]: + "(k dvd m) \<longrightarrow> (k dvd n) \<longrightarrow> k dvd gcd(m,n)" + apply (induct_tac m n rule: gcd.induct) + apply (case_tac "n=0") + apply (simp_all add: dvd_mod); + done; + +theorem gcd_greatest_iff [iff]: + "k dvd gcd(m,n) = (k dvd m \<and> k dvd n)" + apply (blast intro!: gcd_greatest intro: dvd_trans); + done; + + +constdefs + is_gcd :: "[nat,nat,nat]=>bool" (*gcd as a relation*) + "is_gcd p m n == p dvd m \<and> p dvd n \<and> + (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)" + +(*Function gcd yields the Greatest Common Divisor*) +lemma is_gcd: "is_gcd (gcd(m,n)) m n" + apply (simp add: is_gcd_def gcd_greatest); + done + +(*uniqueness of GCDs*) +lemma is_gcd_unique: "\<lbrakk> is_gcd m a b; is_gcd n a b \<rbrakk> \<Longrightarrow> m=n" + apply (simp add: is_gcd_def); + apply (blast intro: dvd_anti_sym) + done + + +text {* +@{thm[display] dvd_anti_sym} +\rulename{dvd_anti_sym} + +\begin{isabelle} +proof\ (prove):\ step\ 1\isanewline +\isanewline +goal\ (lemma\ is_gcd_unique):\isanewline +\isasymlbrakk is_gcd\ m\ a\ b;\ is_gcd\ n\ a\ b\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n\isanewline +\ 1.\ \isasymlbrakk m\ dvd\ a\ \isasymand \ m\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ m);\isanewline +\ \ \ \ \ \ \ n\ dvd\ a\ \isasymand \ n\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ n)\isasymrbrakk \isanewline +\ \ \ \ \isasymLongrightarrow \ m\ =\ n +\end{isabelle} +*}; + +lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))" + apply (rule is_gcd_unique) + apply (rule is_gcd) + apply (simp add: is_gcd_def); + apply (blast intro: dvd_trans); + done + +text{* +\begin{isabelle} +proof\ (prove):\ step\ 3\isanewline +\isanewline +goal\ (lemma\ gcd_assoc):\isanewline +gcd\ (gcd\ (k,\ m),\ n)\ =\ gcd\ (k,\ gcd\ (m,\ n))\isanewline +\ 1.\ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ k\ \isasymand \isanewline +\ \ \ \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ m\ \isasymand \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ n +\end{isabelle} +*} + + +lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)" + apply (blast intro: dvd_trans); + done + +(*This is half of the proof (by dvd_anti_sym) of*) +lemma gcd_mult_cancel: "gcd(k,n) = 1 \<Longrightarrow> gcd(k*m, n) = gcd(m,n)" + oops + + + +text{*\noindent +Forward proof material: of, OF, THEN, simplify. +*} + +text{*\noindent +SKIP most developments... +*} + +(** Commutativity **) + +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" + apply (auto simp add: is_gcd_def); + done + +lemma gcd_commute: "gcd(m,n) = gcd(n,m)" + apply (rule is_gcd_unique) + apply (rule is_gcd) + apply (subst is_gcd_commute) + apply (simp add: is_gcd) + done + +lemma gcd_1 [simp]: "gcd(m,1) = 1" + apply (simp) + done + +lemma gcd_1_left [simp]: "gcd(1,m) = 1" + apply (simp add: gcd_commute [of 1]) + done + +text{*\noindent +as far as HERE. +*} + + +text {* +@{thm[display] gcd_1} +\rulename{gcd_1} + +@{thm[display] gcd_1_left} +\rulename{gcd_1_left} +*}; + +text{*\noindent +SKIP THIS PROOF +*} + +lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)" + apply (induct_tac m n rule: gcd.induct) + apply (case_tac "n=0") + apply (simp) + apply (case_tac "k=0") + apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) + done + +text {* +@{thm[display] gcd_mult_distrib2} +\rulename{gcd_mult_distrib2} +*}; + +text{*\noindent +of, simplified +*} + + +lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]; +lemmas gcd_mult_1 = gcd_mult_0 [simplified]; + +text {* +@{thm[display] gcd_mult_distrib2 [of _ 1]} + +@{thm[display] gcd_mult_0} +\rulename{gcd_mult_0} + +@{thm[display] gcd_mult_1} +\rulename{gcd_mult_1} + +@{thm[display] sym} +\rulename{sym} +*}; + +lemmas gcd_mult = gcd_mult_1 [THEN sym]; + +lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym]; + (*better in one step!*) + +text {* +more legible +*}; + +lemma gcd_mult [simp]: "gcd(k, k*n) = k" + apply (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym]) + done + +lemmas gcd_self = gcd_mult [of k 1, simplified]; + + +text {* +Rules handy with THEN + +@{thm[display] iffD1} +\rulename{iffD1} + +@{thm[display] iffD2} +\rulename{iffD2} +*}; + + +text {* +again: more legible +*}; + +lemma gcd_self [simp]: "gcd(k,k) = k" + apply (rule gcd_mult [of k 1, simplified]) + done + +lemma relprime_dvd_mult: + "\<lbrakk> gcd(k,n)=1; k dvd (m*n) \<rbrakk> \<Longrightarrow> k dvd m"; + apply (insert gcd_mult_distrib2 [of m k n]) + apply (simp) + apply (erule_tac t="m" in ssubst); + apply (simp) + done + + +text {* +Another example of "insert" + +@{thm[display] mod_div_equality} +\rulename{mod_div_equality} +*}; + +lemma div_mult_self_is_m: + "0<n \<Longrightarrow> (m*n) div n = (m::nat)" + apply (insert mod_div_equality [of "m*n" n]) + apply (simp) + done + +lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m"; + apply (blast intro: relprime_dvd_mult dvd_trans) + done + +lemma relprime_20_81: "gcd(#20,#81) = 1"; + apply (simp add: gcd.simps) + done + + +text {* +Examples of 'OF' + +@{thm[display] relprime_dvd_mult} +\rulename{relprime_dvd_mult} + +@{thm[display] relprime_dvd_mult [OF relprime_20_81]} + +@{thm[display] dvd_refl} +\rulename{dvd_refl} + +@{thm[display] dvd_add} +\rulename{dvd_add} + +@{thm[display] dvd_add [OF dvd_refl dvd_refl]} + +@{thm[display] dvd_add [OF _ dvd_refl]} +*}; + +lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)"; +apply (subgoal_tac "z = #34 \<or> z = #36") +apply blast +apply (subgoal_tac "z \<noteq> #35") +apply arith +apply force +done + +text +{* +proof\ (prove):\ step\ 1\isanewline +\isanewline +goal\ (lemma):\isanewline +\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline +\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline +\ \ \ \ \ \ \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isasymrbrakk \isanewline +\ \ \ \ \isasymLongrightarrow \ Q\ z\isanewline +\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline +\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36 + + + +proof\ (prove):\ step\ 3\isanewline +\isanewline +goal\ (lemma):\isanewline +\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline +\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline +\ \ \ \ \ \ \ z\ \isasymnoteq \ \#35\isasymrbrakk \isanewline +\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isanewline +\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline +\ \ \ \ \isasymLongrightarrow \ z\ \isasymnoteq \ \#35 +*} + + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Rules/rules.tex Mon Oct 23 16:25:04 2000 +0200 @@ -0,0 +1,1871 @@ +\chapter{The Rules of the Game} +\label{chap:rules} + +Until now, we have proved everything using only induction and simplification. +Substantial proofs require more elaborate forms of inference. This chapter +outlines the concepts and techniques that underlie reasoning in Isabelle. The examples +are mainly drawn from predicate logic. The first examples in this +chapter will consist of detailed, low-level proof steps. Later, we shall +see how to automate such reasoning using the methods \isa{blast}, +\isa{auto} and others. + +\section{Natural deduction} + +In Isabelle, proofs are constructed using inference rules. The +most familiar inference rule is probably \emph{modus ponens}: +\[ \infer{Q}{P\imp Q & P} \] +This rule says that from $P\imp Q$ and $P$ +we may infer~$Q$. + +%Early logical formalisms had this +%rule and at most one or two others, along with many complicated +%axioms. Any desired theorem could be obtained by applying \emph{modus +%ponens} or other rules to the axioms, but proofs were +%hard to find. For example, a standard inference system has +%these two axioms (amongst others): +%\begin{gather*} +% P\imp(Q\imp P) \tag{K}\\ +% (P\imp(Q\imp R))\imp ((P\imp Q)\imp(P\imp R)) \tag{S} +%\end{gather*} +%Try proving the trivial fact $P\imp P$ using these axioms and \emph{modus +%ponens}! + +\textbf{Natural deduction} is an attempt to formalize logic in a way +that mirrors human reasoning patterns. +% +%Instead of having a few +%inference rules and many axioms, it has many inference rules +%and few axioms. +% +For each logical symbol (say, $\conj$), there +are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules. +The introduction rules allow us to infer this symbol (say, to +infer conjunctions). The elimination rules allow us to deduce +consequences from this symbol. Ideally each rule should mention +one symbol only. For predicate logic this can be +done, but when users define their own concepts they typically +have to refer to other symbols as well. It is best not be dogmatic. + +Natural deduction generally deserves its name. It is easy to use. Each +proof step consists of identifying the outermost symbol of a formula and +applying the corresponding rule. It creates new subgoals in +an obvious way from parts of the chosen formula. Expanding the +definitions of constants can blow up the goal enormously. Deriving natural +deduction rules for such constants lets us reason in terms of their key +properties, which might otherwise be obscured by the technicalities of its +definition. Natural deduction rules also lend themselves to automation. +Isabelle's +\textbf{classical reasoner} accepts any suitable collection of natural deduction +rules and uses them to search for proofs automatically. Isabelle is designed around +natural deduction and many of its tools use the terminology of introduction and +elimination rules. + + +\section{Introduction rules} + +An \textbf{introduction} rule tells us when we can infer a formula +containing a specific logical symbol. For example, the conjunction +introduction rule says that if we have $P$ and if we have $Q$ then +we have $P\conj Q$. In a mathematics text, it is typically shown +like this: +\[ \infer{P\conj Q}{P & Q} \] +The rule introduces the conjunction +symbol~($\conj$) in its conclusion. Of course, in Isabelle proofs we +mainly reason backwards. When we apply this rule, the subgoal already has +the form of a conjunction; the proof step makes this conjunction symbol +disappear. + +In Isabelle notation, the rule looks like this: +\begin{isabelle} +\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI} +\end{isabelle} +Carefully examine the syntax. The premises appear to the +left of the arrow and the conclusion to the right. The premises (if +more than one) are grouped using the fat brackets. The question marks +indicate \textbf{schematic variables} (also called \textbf{unknowns}): they may +be replaced by arbitrary formulas. If we use the rule backwards, Isabelle +tries to unify the current subgoal with the conclusion of the rule, which +has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below, +\S\ref{sec:unification}.) If successful, +it yields new subgoals given by the formulas assigned to +\isa{?P} and \isa{?Q}. + +The following trivial proof illustrates this point. +\begin{isabelle} +\isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\ +Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ +(Q\ \isasymand\ P){"}\isanewline +\isacommand{apply}\ (rule\ conjI)\isanewline +\ \isacommand{apply}\ assumption\isanewline +\isacommand{apply}\ (rule\ conjI)\isanewline +\ \isacommand{apply}\ assumption\isanewline +\isacommand{apply}\ assumption +\end{isabelle} +At the start, Isabelle presents +us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved, +\isa{P\ \isasymand\ +(Q\ \isasymand\ P)}. We are working backwards, so when we +apply conjunction introduction, the rule removes the outermost occurrence +of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply +the proof method {\isa{rule}} --- here with {\isa{conjI}}, the conjunction +introduction rule. +\begin{isabelle} +%{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\ +%\isasymand\ P\isanewline +\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline +\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P +\end{isabelle} +Isabelle leaves two new subgoals: the two halves of the original conjunction. +The first is simply \isa{P}, which is trivial, since \isa{P} is among +the assumptions. We can apply the {\isa{assumption}} +method, which proves a subgoal by finding a matching assumption. +\begin{isabelle} +\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ +Q\ \isasymand\ P +\end{isabelle} +We are left with the subgoal of proving +\isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply +\isa{rule conjI} again. +\begin{isabelle} +\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline +\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P +\end{isabelle} +We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved +using the {\isa{assumption}} method. + + +\section{Elimination rules} + +\textbf{Elimination} rules work in the opposite direction from introduction +rules. In the case of conjunction, there are two such rules. +From $P\conj Q$ we infer $P$. also, from $P\conj Q$ +we infer $Q$: +\[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \] + +Now consider disjunction. There are two introduction rules, which resemble inverted forms of the +conjunction elimination rules: +\[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \] + +What is the disjunction elimination rule? The situation is rather different from +conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we +cannot conclude that $Q$ is true; there are no direct +elimination rules of the sort that we have seen for conjunction. Instead, +there is an elimination rule that works indirectly. If we are trying to prove +something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider +two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is +true and prove $R$ a second time. Here we see a fundamental concept used in natural +deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under +different assumptions. The assumptions are local to these subproofs and are visible +nowhere else. + +In a logic text, the disjunction elimination rule might be shown +like this: +\[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \] +The assumptions $[P]$ and $[Q]$ are bracketed +to emphasize that they are local to their subproofs. In Isabelle +notation, the already-familiar \isa\isasymLongrightarrow syntax serves the +same purpose: +\begin{isabelle} +\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE} +\end{isabelle} +When we use this sort of elimination rule backwards, it produces +a case split. (We have this before, in proofs by induction.) The following proof +illustrates the use of disjunction elimination. +\begin{isabelle} +\isacommand{lemma}\ disj_swap:\ {"}P\ \isasymor\ Q\ +\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline +\isacommand{apply}\ (erule\ disjE)\isanewline +\ \isacommand{apply}\ (rule\ disjI2)\isanewline +\ \isacommand{apply}\ assumption\isanewline +\isacommand{apply}\ (rule\ disjI1)\isanewline +\isacommand{apply}\ assumption +\end{isabelle} +We assume \isa{P\ \isasymor\ Q} and +must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction +elimination rule, \isa{disjE}. The method {\isa{erule}} applies an +elimination rule to the assumptions, searching for one that matches the +rule's first premise. Deleting that assumption, it +return the subgoals for the remaining premises. Most of the +time, this is the best way to use elimination rules; only rarely is there +any point in keeping the assumption. + +\begin{isabelle} +%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline +\ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline +\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P +\end{isabelle} +Here it leaves us with two subgoals. The first assumes \isa{P} and the +second assumes \isa{Q}. Tackling the first subgoal, we need to +show \isa{Q\ \isasymor\ P}\@. The second introduction rule (\isa{disjI2}) +can reduce this to \isa{P}, which matches the assumption. So, we apply the +{\isa{rule}} method with \isa{disjI2} \ldots +\begin{isabelle} +\ 1.\ P\ \isasymLongrightarrow\ P\isanewline +\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P +\end{isabelle} +\ldots and finish off with the {\isa{assumption}} +method. We are left with the other subgoal, which +assumes \isa{Q}. +\begin{isabelle} +\ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P +\end{isabelle} +Its proof is similar, using the introduction +rule \isa{disjI1}. + +The result of this proof is a new inference rule \isa{disj_swap}, which is neither +an introduction nor an elimination rule, but which might +be useful. We can use it to replace any goal of the form $Q\disj P$ +by a one of the form $P\disj Q$. + + + +\section{Destruction rules: some examples} + +Now let us examine the analogous proof for conjunction. +\begin{isabelle} +\isacommand{lemma}\ conj_swap:\ {"}P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline +\isacommand{apply}\ (rule\ conjI)\isanewline +\ \isacommand{apply}\ (drule\ conjunct2)\isanewline +\ \isacommand{apply}\ assumption\isanewline +\isacommand{apply}\ (drule\ conjunct1)\isanewline +\isacommand{apply}\ assumption +\end{isabelle} +Recall that the conjunction elimination rules --- whose Isabelle names are +\isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half +of a conjunction. Rules of this sort (where the conclusion is a subformula of a +premise) are called \textbf{destruction} rules, by analogy with the destructor +functions of functional pr§gramming.% +\footnote{This Isabelle terminology has no counterpart in standard logic texts, +although the distinction between the two forms of elimination rule is well known. +Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules are very +bad. What is catastrophic about them is the parasitic presence of a formula [$R$] +which has no structural link with the formula which is eliminated.''} + +The first proof step applies conjunction introduction, leaving +two subgoals: +\begin{isabelle} +%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline +\ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline +\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P +\end{isabelle} + +To invoke the elimination rule, we apply a new method, \isa{drule}. +Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if +you prefer). Applying the +second conjunction rule using \isa{drule} replaces the assumption +\isa{P\ \isasymand\ Q} by \isa{Q}. +\begin{isabelle} +\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline +\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P +\end{isabelle} +The resulting subgoal can be proved by applying \isa{assumption}. +The other subgoal is similarly proved, using the \isa{conjunct1} rule and the +\isa{assumption} method. + +Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to +you. Isabelle does not attempt to work out whether a rule +is an introduction rule or an elimination rule. The +method determines how the rule will be interpreted. Many rules +can be used in more than one way. For example, \isa{disj_swap} can +be applied to assumptions as well as to goals; it replaces any +assumption of the form +$P\disj Q$ by a one of the form $Q\disj P$. + +Destruction rules are simpler in form than indirect rules such as \isa{disjE}, +but they can be inconvenient. Each of the conjunction rules discards half +of the formula, when usually we want to take both parts of the conjunction as new +assumptions. The easiest way to do so is by using an +alternative conjunction elimination rule that resembles \isa{disjE}. It is seldom, +if ever, seen in logic books. In Isabelle syntax it looks like this: +\begin{isabelle} +\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE} +\end{isabelle} + +\begin{exercise} +Use the rule {\isa{conjE}} to shorten the proof above. +\end{exercise} + + +\section{Implication} + +At the start of this chapter, we saw the rule \textit{modus ponens}. It is, in fact, +a destruction rule. The matching introduction rule looks like this +in Isabelle: +\begin{isabelle} +(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\ +\isasymlongrightarrow\ ?Q\rulename{impI} +\end{isabelle} +And this is \textit{modus ponens}: +\begin{isabelle} +\isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\ +\isasymLongrightarrow\ ?Q +\rulename{mp} +\end{isabelle} + +Here is a proof using the rules for implication. This +lemma performs a sort of uncurrying, replacing the two antecedents +of a nested implication by a conjunction. +\begin{isabelle} +\isacommand{lemma}\ imp_uncurry:\ +{"}P\ \isasymlongrightarrow\ (Q\ +\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ +\isasymand\ Q\ \isasymlongrightarrow\ +R"\isanewline +\isacommand{apply}\ (rule\ impI)\isanewline +\isacommand{apply}\ (erule\ conjE)\isanewline +\isacommand{apply}\ (drule\ mp)\isanewline +\ \isacommand{apply}\ assumption\isanewline +\isacommand{apply}\ (drule\ mp)\isanewline +\ \ \isacommand{apply}\ assumption\isanewline +\ \isacommand{apply}\ assumption +\end{isabelle} +First, we state the lemma and apply implication introduction (\isa{rule impI}), +which moves the conjunction to the assumptions. +\begin{isabelle} +%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\ +%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline +\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R +\end{isabelle} +Next, we apply conjunction elimination (\isa{erule conjE}), which splits this +conjunction into two parts. +\begin{isabelle} +\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\ +Q\isasymrbrakk\ \isasymLongrightarrow\ R +\end{isabelle} +Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\ +\isasymlongrightarrow\ R)}, where the parentheses have been inserted for +clarity. The nested implication requires two applications of +\textit{modus ponens}: \isa{drule mp}. The first use yields the +implication \isa{Q\ +\isasymlongrightarrow\ R}, but first we must prove the extra subgoal +\isa{P}, which we do by assumption. +\begin{isabelle} +\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline +\ 2.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R +\end{isabelle} +Repeating these steps for \isa{Q\ +\isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}. +\begin{isabelle} +\ 1.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ +\isasymLongrightarrow\ R +\end{isabelle} + +The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow} +both stand for implication, but they differ in many respects. Isabelle +uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is +built-in and Isabelle's inference mechanisms treat it specially. On the +other hand, \isa{\isasymlongrightarrow} is just one of the many connectives +available in higher-order logic. We reason about it using inference rules +such as \isa{impI} and \isa{mp}, just as we reason about the other +connectives. You will have to use \isa{\isasymlongrightarrow} in any +context that requires a formula of higher-order logic. Use +\isa{\isasymLongrightarrow} to separate a theorem's preconditions from its +conclusion. + +When using induction, often the desired theorem results in an induction +hypothesis that is too weak. In such cases you may have to invent a more +complicated induction formula, typically involving +\isa{\isasymlongrightarrow} and \isa{\isasymforall}. From this lemma you +derive the desired theorem , typically involving +\isa{\isasymLongrightarrow}. We shall see an example below, +\S\ref{sec:proving-euclid}. + + + +\remark{negation: notI, notE, ccontr, swap, contrapos?} + + +\section{Unification and substitution}\label{sec:unification} + +As we have seen, Isabelle rules involve variables that begin with a +question mark. These are called \textbf{schematic} variables and act as +placeholders for terms. \textbf{Unification} refers to the process of +making two terms identical, possibly by replacing their variables by +terms. The simplest case is when the two terms are already the same. Next +simplest is when the variables in only one of the term + are replaced; this is called \textbf{pattern-matching}. The +{\isa{rule}} method typically matches the rule's conclusion +against the current subgoal. In the most complex case, variables in both +terms are replaced; the {\isa{rule}} method can do this the goal +itself contains schematic variables. Other occurrences of the variables in +the rule or proof state are updated at the same time. + +Schematic variables in goals are sometimes called \textbf{unknowns}. They +are useful because they let us proceed with a proof even when we do not +know what certain terms should be --- as when the goal is $\exists x.\,P$. +They can be filled in later, often automatically. + + Unification is well known to Prolog programmers. Isabelle uses \textbf{higher-order} +unification, which is unification in the +typed $\lambda$-calculus. The general case is +undecidable, but for our purposes, the differences from ordinary +unification are straightforward. It handles bound variables +correctly, avoiding capture. The two terms \isa{{\isasymlambda}x.\ ?P} and +\isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by +\isa{t x} is forbidden because the free occurrence of~\isa{x} would become +bound. The two terms +\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are +trivially unifiable because they differ only by a bound variable renaming. + +Higher-order unification sometimes must invent +$\lambda$-terms to replace function variables, +which can lead to a combinatorial explosion. However, Isabelle proofs tend +to involve easy cases where there are few possibilities for the +$\lambda$-term being constructed. In the easiest case, the +function variable is applied only to bound variables, +as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and +\isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace +\isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most +one unifier, like ordinary unification. A harder case is +unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h}, +namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}. +Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is +exponential in the number of occurrences of~\isa{a} in the second term. + +Isabelle also uses function variables to express \textbf{substitution}. +A typical substitution rule allows us to replace one term by +another if we know that two terms are equal. +\[ \infer{P[t/x]}{s=t & P[s/x]} \] +The conclusion uses a notation for substitution: $P[t/x]$ is the result of +replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions +designated by~$x$, which gives it additional power. For example, it can +derive symmetry of equality from reflexivity. Using $x=s$ for~$P$ +replaces just the first $s$ in $s=s$ by~$t$. +\[ \infer{t=s}{s=t & \infer{s=s}{}} \] + +The Isabelle version of the substitution rule looks like this: +\begin{isabelle} +\isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\ +?t +\rulename{ssubst} +\end{isabelle} +Crucially, \isa{?P} is a function +variable: it can be replaced by a $\lambda$-expression +involving one bound variable whose occurrences identify the places +in which $s$ will be replaced by~$t$. The proof above requires +\isa{{\isasymlambda}x.~x=s}. + +The \isa{simp} method replaces equals by equals, but using the substitution +rule gives us more control. Consider this proof: +\begin{isabelle} +\isacommand{lemma}\ +"{\isasymlbrakk}\ x\ +=\ f\ x;\ odd(f\ +x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\ +x"\isanewline +\isacommand{apply}\ (erule\ ssubst)\isanewline +\isacommand{apply}\ assumption\isanewline +\isacommand{done}\end{isabelle} +% +The simplifier might loop, replacing \isa{x} by \isa{f x} and then by +\isa{f(f x)} and so forth. (Actually, \isa{simp} +sees the danger and re-orients this equality, but in more complicated cases +it can be fooled.) When we apply substitution, Isabelle replaces every +\isa{x} in the subgoal by \isa{f x} just once: it cannot loop. The +resulting subgoal is trivial by assumption. + +We are using the \isa{erule} method it in a novel way. Hitherto, +the conclusion of the rule was just a variable such as~\isa{?R}, but it may +be any term. The conclusion is unified with the subgoal just as +it would be with the \isa{rule} method. At the same time \isa{erule} looks +for an assumption that matches the rule's first premise, as usual. With +\isa{ssubst} the effect is to find, use and delete an equality +assumption. + + +Higher-order unification can be tricky, as this example indicates: +\begin{isabelle} +\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ +f\ x;\ triple\ (f\ x)\ +(f\ x)\ x\ \isasymrbrakk\ +\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline +\isacommand{apply}\ (erule\ ssubst)\isanewline +\isacommand{back}\isanewline +\isacommand{back}\isanewline +\isacommand{back}\isanewline +\isacommand{back}\isanewline +\isacommand{apply}\ assumption\isanewline +\isacommand{done} +\end{isabelle} +% +By default, Isabelle tries to substitute for all the +occurrences. Applying \isa{erule\ ssubst} yields this subgoal: +\begin{isabelle} +\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x) +\end{isabelle} +The substitution should have been done in the first two occurrences +of~\isa{x} only. Isabelle has gone too far. The \isa{back} +method allows us to reject this possibility and get a new one: +\begin{isabelle} +\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x) +\end{isabelle} +% +Now Isabelle has left the first occurrence of~\isa{x} alone. That is +promising but it is not the desired combination. So we use \isa{back} +again: +\begin{isabelle} +\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x) +\end{isabelle} +% +This also is wrong, so we use \isa{back} again: +\begin{isabelle} +\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x) +\end{isabelle} +% +And this one is wrong too. Looking carefully at the series +of alternatives, we see a binary countdown with reversed bits: 111, +011, 101, 001. Invoke \isa{back} again: +\begin{isabelle} +\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x% +\end{isabelle} +At last, we have the right combination! This goal follows by assumption. + +Never use {\isa{back}} in the final version of a proof. +It should only be used for exploration. One way to get rid of {\isa{back}} +to combine two methods in a single \textbf{apply} command. Isabelle +applies the first method and then the second. If the second method +fails then Isabelle automatically backtracks. This process continues until +the first method produces an output that the second method can +use. We get a one-line proof of our example: +\begin{isabelle} +\isacommand{lemma}\ +"{\isasymlbrakk}\ x\ +=\ f\ x;\ triple\ (f\ +x)\ (f\ x)\ x\ +\isasymrbrakk\ +\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline +\isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline +\isacommand{done} +\end{isabelle} + +The most general way to get rid of the {\isa{back}} command is +to instantiate variables in the rule. The method {\isa{rule\_tac}} is +similar to \isa{rule}, but it +makes some of the rule's variables denote specified terms. +Also available are {\isa{drule\_tac}} and \isa{erule\_tac}. Here we need +\isa{erule\_tac} since above we used +\isa{erule}. +\begin{isabelle} +\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline +\isacommand{apply}\ (erule_tac\ +P={"}{\isasymlambda}u.\ triple\ u\ +u\ x"\ \isakeyword{in}\ +ssubst)\isanewline +\isacommand{apply}\ assumption\isanewline +\isacommand{done} +\end{isabelle} +% +To specify a desired substitution +requires instantiating the variable \isa{?P} with a $\lambda$-expression. +The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\ +u\ x} indicate that the first two arguments have to be substituted, leaving +the third unchanged. + +An alternative to {\isa{rule\_tac}} is to use \isa{rule} with the +{\isa{of}} directive, described in \S\ref{sec:forward} below. An +advantage of {\isa{rule\_tac}} is that the instantiations may refer to +variables bound in the current subgoal. + + +\section{Negation} + +Negation causes surprising complexity in proofs. Its natural +deduction rules are straightforward, but additional rules seem +necessary in order to handle negated assumptions gracefully. + +Negation introduction deduces $\neg P$ if assuming $P$ leads to a +contradiction. Negation elimination deduces any formula in the +presence of $\neg P$ together with~$P$: +\begin{isabelle} +(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P% +\rulename{notI}\isanewline +\isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R% +\rulename{notE} +\end{isabelle} +% +Classical logic allows us to assume $\neg P$ +when attempting to prove~$P$: +\begin{isabelle} +(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P% +\rulename{classical} +\end{isabelle} +% +Three further rules are variations on the theme of contrapositive. +They differ in the placement of the negation symbols: +\begin{isabelle} +\isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% +\rulename{contrapos_pp}\isanewline +\isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% +\rulename{contrapos_np}\isanewline +\isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P% +\rulename{contrapos_nn} +\end{isabelle} +% +These rules are typically applied using the {\isa{erule}} method, where +their effect is to form a contrapositive from an +assumption and the goal's conclusion. + +The most important of these is \isa{contrapos_np}. It is useful +for applying introduction rules to negated assumptions. For instance, +the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we +might want to use conjunction introduction on it. +Before we can do so, we must move that assumption so that it +becomes the conclusion. The following proof demonstrates this +technique: +\begin{isabelle} +\isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\ +\isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\ +R"\isanewline +\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\ +contrapos_np)\isanewline +\isacommand{apply}\ intro\isanewline +\isacommand{apply}\ (erule\ notE,\ assumption)\isanewline +\isacommand{done} +\end{isabelle} +% +There are two negated assumptions and we need to exchange the conclusion with the +second one. The method \isa{erule contrapos_np} would select the first assumption, +which we do not want. So we specify the desired assumption explicitly, using +\isa{erule_tac}. This is the resulting subgoal: +\begin{isabelle} +\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ +R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q% +\end{isabelle} +The former conclusion, namely \isa{R}, now appears negated among the assumptions, +while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new +conclusion. + +We can now apply introduction rules. We use the {\isa{intro}} method, which +repeatedly applies built-in introduction rules. Here its effect is equivalent +to \isa{rule impI}.\begin{isabelle} +\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\ +R\isasymrbrakk\ \isasymLongrightarrow\ Q% +\end{isabelle} +We can see a contradiction in the form of assumptions \isa{\isasymnot\ R} +and~\isa{R}, which suggests using negation elimination. If applied on its own, +however, it will select the first negated assumption, which is useless. Instead, +we combine the rule with the +\isa{assumption} method: +\begin{isabelle} +\ \ \ \ \ (erule\ notE,\ assumption) +\end{isabelle} +Now when Isabelle selects the first assumption, it tries to prove \isa{P\ +\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the +assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption. That +concludes the proof. + +\medskip + +Here is another example. +\begin{isabelle} +\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\ +\isasymLongrightarrow\ P\ \isasymor\ Q\ \isasymand\ R"\isanewline +\isacommand{apply}\ intro% + + +\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline +\ \isacommand{apply}\ assumption +\isanewline +\isacommand{apply}\ (erule\ contrapos_np,\ rule\ conjI)\isanewline +\ \ \isacommand{apply}\ assumption\isanewline +\ \isacommand{apply}\ assumption\isanewline +\isacommand{done} +\end{isabelle} +% +The first proof step applies the {\isa{intro}} method, which repeatedly +uses built-in introduction rules. Here it creates the negative assumption \isa{\isasymnot\ (Q\ \isasymand\ +R)}. +\begin{isabelle} +\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\ +R)\isasymrbrakk\ \isasymLongrightarrow\ P% +\end{isabelle} +It comes from \isa{disjCI}, a disjunction introduction rule that is more +powerful than the separate rules \isa{disjI1} and \isa{disjI2}. + +Next we apply the {\isa{elim}} method, which repeatedly applies +elimination rules; here, the elimination rules given +in the command. One of the subgoals is trivial, leaving us with one other: +\begin{isabelle} +\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P% +\end{isabelle} +% +Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The +combination +\begin{isabelle} +\ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI) +\end{isabelle} +is robust: the \isa{conjI} forces the \isa{erule} to select a +conjunction. The two subgoals are the ones we would expect from appling +conjunction introduction to +\isa{Q\ +\isasymand\ R}: +\begin{isabelle} +\ 1.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ +Q\isanewline +\ 2.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R% +\end{isabelle} +The rest of the proof is trivial. + + +\section{The universal quantifier} + +Quantifiers require formalizing syntactic substitution and the notion of \textbf{arbitrary +value}. Consider the universal quantifier. In a logic book, its +introduction rule looks like this: +\[ \infer{\forall x.\,P}{P} \] +Typically, a proviso written in English says that $x$ must not +occur in the assumptions. This proviso guarantees that $x$ can be regarded as +arbitrary, since it has not been assumed to satisfy any special conditions. +Isabelle's underlying formalism, called the +\textbf{meta-logic}, eliminates the need for English. It provides its own universal +quantifier (\isasymAnd) to express the notion of an arbitrary value. We have +already seen another symbol of the meta-logic, namely +\isa\isasymLongrightarrow, which expresses inference rules and the treatment of +assumptions. The only other symbol in the meta-logic is \isa\isasymequiv, which +can be used to define constants. + +Returning to the universal quantifier, we find that having a similar quantifier +as part of the meta-logic makes the introduction rule trivial to express: +\begin{isabelle} +({\isasymAnd}x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI} +\end{isabelle} + + +The following trivial proof demonstrates how the universal introduction +rule works. +\begin{isabelle} +\isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline +\isacommand{apply}\ (rule\ allI)\isanewline +\isacommand{apply}\ (rule\ impI)\isanewline +\isacommand{apply}\ assumption +\end{isabelle} +The first step invokes the rule by applying the method \isa{rule allI}. +\begin{isabelle} +%{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline +\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymlongrightarrow\ P\ x +\end{isabelle} +Note that the resulting proof state has a bound variable, +namely~\bigisa{x}. The rule has replaced the universal quantifier of +higher-order logic by Isabelle's meta-level quantifier. Our goal is to +prove +\isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is +an implication, so we apply the corresponding introduction rule (\isa{impI}). +\begin{isabelle} +\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymLongrightarrow\ P\ x +\end{isabelle} +The {\isa{assumption}} method proves this last subgoal. + +\medskip +Now consider universal elimination. In a logic text, +the rule looks like this: +\[ \infer{P[t/x]}{\forall x.\,P} \] +The conclusion is $P$ with $t$ substituted for the variable~$x$. +Isabelle expresses substitution using a function variable: +\begin{isabelle} +{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec} +\end{isabelle} +This destruction rule takes a +universally quantified formula and removes the quantifier, replacing +the bound variable \bigisa{x} by the schematic variable \bigisa{?x}. Recall that a +schematic variable starts with a question mark and acts as a +placeholder: it can be replaced by any term. + +To see how this works, let us derive a rule about reducing +the scope of a universal quantifier. In mathematical notation we write +\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \] +with the proviso `$x$ not free in~$P$.' Isabelle's treatment of +substitution makes the proviso unnecessary. The conclusion is expressed as +\isa{P\ +\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the +variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a +bound variable capture. Here is the isabelle proof in full: +\begin{isabelle} +\isacommand{lemma}\ "({\isasymforall}x.\ P\ +\isasymlongrightarrow\ Q\ x)\ \isasymLongrightarrow\ P\ +\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x){"}\isanewline +\isacommand{apply}\ (rule\ impI)\isanewline +\isacommand{apply}\ (rule\ allI)\isanewline +\isacommand{apply}\ (drule\ spec)\isanewline +\isacommand{apply}\ (drule\ mp)\isanewline +\ \ \isacommand{apply}\ assumption\isanewline +\ \isacommand{apply}\ assumption +\end{isabelle} +First we apply implies introduction (\isa{rule impI}), +which moves the \isa{P} from the conclusion to the assumptions. Then +we apply universal introduction (\isa{rule allI}). +\begin{isabelle} +%{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x\ \isasymLongrightarrow\ P\ +%\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)\isanewline +\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x +\end{isabelle} +As before, it replaces the HOL +quantifier by a meta-level quantifier, producing a subgoal that +binds the variable~\bigisa{x}. The leading bound variables +(here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\ +\isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the +conclusion, here \isa{Q\ x}. At each proof step, the subgoals inherit the +previous context, though some context elements may be added or deleted. +Applying \isa{erule} deletes an assumption, while many natural deduction +rules add bound variables or assumptions. + +Now, to reason from the universally quantified +assumption, we apply the elimination rule using the {\isa{drule}} +method. This rule is called \isa{spec} because it specializes a universal formula +to a particular term. +\begin{isabelle} +\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ P\ \isasymlongrightarrow\ Q\ (?x2\ +x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x +\end{isabelle} +Observe how the context has changed. The quantified formula is gone, +replaced by a new assumption derived from its body. Informally, we have +removed the quantifier. The quantified variable +has been replaced by the curious term +\bigisa{?x2~x}; it acts as a placeholder that may be replaced +by any term that can be built up from~\bigisa{x}. (Formally, \bigisa{?x2} is an +unknown of function type, applied to the argument~\bigisa{x}.) This new assumption is +an implication, so we can use \emph{modus ponens} on it. As before, it requires +proving the antecedent (in this case \isa{P}) and leaves us with the consequent. +\begin{isabelle} +\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ Q\ (?x2\ x){\isasymrbrakk}\ +\isasymLongrightarrow\ Q\ x +\end{isabelle} +The consequent is \isa{Q} applied to that placeholder. It may be replaced by any +term built from~\bigisa{x}, and here +it should simply be~\bigisa{x}. The \isa{assumption} method will do this. +The assumption need not be identical to the conclusion, provided the two formulas are +unifiable. + +\medskip +Note that \isa{drule spec} removes the universal quantifier and --- as +usual with elimination rules --- discards the original formula. Sometimes, a +universal formula has to be kept so that it can be used again. Then we use a new +method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces +the selected assumption. The \isa{f} is for `forward.' + +In this example, we intuitively see that to go from \isa{P\ a} to \isa{P(f\ (f\ +a))} requires two uses of the quantified assumption, one for each +additional~\isa{f}. +\begin{isabelle} +\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x); +\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(f\ (f\ a))"\isanewline +\isacommand{apply}\ (frule\ spec)\isanewline +\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline +\isacommand{apply}\ (drule\ spec)\isanewline +\isacommand{apply}\ (drule\ mp,\ assumption,\ assumption)\isanewline +\isacommand{done} +\end{isabelle} +% +Applying \isa{frule\ spec} leaves this subgoal: +\begin{isabelle} +\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (f\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a)) +\end{isabelle} +It is just what \isa{drule} would have left except that the quantified +assumption is still present. The next step is to apply \isa{mp} to the +implication and the assumption \isa{P\ a}, which leaves this subgoal: +\begin{isabelle} +\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ (f\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a)) +\end{isabelle} +% +We have created the assumption \isa{P(f\ a)}, which is progress. To finish the +proof, we apply \isa{spec} one last time, using \isa{drule}. One final trick: if +we then apply +\begin{isabelle} +\ \ \ \ \ (drule\ mp,\ assumption) +\end{isabelle} +it will add a second copy of \isa{P(f\ a)} instead of the desired \isa{P(f\ +(f\ a))}. Bundling both \isa{assumption} calls with \isa{drule mp} causes +Isabelle to backtrack and find the correct one. + + +\section{The existential quantifier} + +The concepts just presented also apply to the existential quantifier, +whose introduction rule looks like this in Isabelle: +\begin{isabelle} +?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI} +\end{isabelle} +If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x. +P(x)$ is also true. It is essentially a dual of the universal elimination rule, and +logic texts present it using the same notation for substitution. The existential +elimination rule looks like this +in a logic text: +\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \] +% +It looks like this in Isabelle: +\begin{isabelle} +\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ {\isasymAnd}x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE} +\end{isabelle} +% +Given an existentially quantified theorem and some +formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with +the universal introduction rule, the textbook version imposes a proviso on the +quantified variable, which Isabelle expresses using its meta-logic. Note that it is +enough to have a universal quantifier in the meta-logic; we do not need an existential +quantifier to be built in as well.\remark{EX example needed?} + +Isabelle/HOL also provides Hilbert's +$\epsilon$-operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is +true, provided such a value exists. Using this operator, we can express an +existential destruction rule: +\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \] +This rule is seldom used, for it can cause exponential blow-up. The +main use of $\epsilon x. P(x)$ is in definitions when $P(x)$ characterizes $x$ +uniquely. For instance, we can define the cardinality of a finite set~$A$ to be that +$n$ such that $A$ is in one-to-one correspondance with $\{1,\ldots,n\}$. We can then +prove that the cardinality of the empty set is zero (since $n=0$ satisfies the +description) and proceed to prove other facts.\remark{SOME theorems +and example} + +\begin{exercise} +Prove the lemma +\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \] +\emph{Hint}: the proof is similar +to the one just above for the universal quantifier. +\end{exercise} + + +\section{Some proofs that fail} + +Most of the examples in this tutorial involve proving theorems. But not every +conjecture is true, and it can be instructive to see how +proofs fail. Here we attempt to prove a distributive law involving +the existential quantifier and conjunction. +\begin{isabelle} +\isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x"\isanewline +\isacommand{apply}\ (erule\ conjE)\isanewline +\isacommand{apply}\ (erule\ exE)\isanewline +\isacommand{apply}\ (erule\ exE)\isanewline +\isacommand{apply}\ (rule\ exI)\isanewline +\isacommand{apply}\ (rule\ conjI)\isanewline +\ \isacommand{apply}\ assumption\isanewline +\isacommand{oops} +\end{isabelle} +The first steps are routine. We apply conjunction elimination (\isa{erule +conjE}) to split the assumption in two, leaving two existentially quantified +assumptions. Applying existential elimination (\isa{erule exE}) removes one of +the quantifiers. +\begin{isabelle} +%({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ +%\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline +\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x +\end{isabelle} +% +When we remove the other quantifier, we get a different bound +variable in the subgoal. (The name \isa{xa} is generated automatically.) +\begin{isabelle} +\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ +\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x +\end{isabelle} +The proviso of the existential elimination rule has forced the variables to +differ: we can hardly expect two arbitrary values to be equal! There is +no way to prove this subgoal. Removing the +conclusion's existential quantifier yields two +identical placeholders, which can become any term involving the variables \bigisa{x} +and~\bigisa{xa}. We need one to become \bigisa{x} +and the other to become~\bigisa{xa}, but Isabelle requires all instances of a +placeholder to be identical. +\begin{isabelle} +\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ +\isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline +\ 2.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa) +\end{isabelle} +We can prove either subgoal +using the \isa{assumption} method. If we prove the first one, the placeholder +changes into~\bigisa{x}. +\begin{isabelle} +\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ +\isasymLongrightarrow\ Q\ x +\end{isabelle} +We are left with a subgoal that cannot be proved, +because there is no way to prove that \bigisa{x} +equals~\bigisa{xa}. Applying the \isa{assumption} method results in an +error message: +\begin{isabelle} +*** empty result sequence -- proof command failed +\end{isabelle} +We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command. + +\medskip + +Here is another abortive proof, illustrating the interaction between +bound variables and unknowns. +If $R$ is a reflexive relation, +is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when +we attempt to prove it. +\begin{isabelle} +\isacommand{lemma}\ "{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ +{\isasymexists}x.\ {\isasymforall}y.\ R\ x\ y"\isanewline +\isacommand{apply}\ (rule\ exI)\isanewline +\isacommand{apply}\ (rule\ allI)\isanewline +\isacommand{apply}\ (drule\ spec)\isanewline +\isacommand{oops} +\end{isabelle} +First, +we remove the existential quantifier. The new proof state has +an unknown, namely~\bigisa{?x}. +\begin{isabelle} +%{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\ +%{\isasymforall}y.\ R\ x\ y\isanewline +\ 1.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymforall}y.\ R\ ?x\ y +\end{isabelle} +Next, we remove the universal quantifier +from the conclusion, putting the bound variable~\isa{y} into the subgoal. +\begin{isabelle} +\ 1.\ {\isasymAnd}y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y +\end{isabelle} +Finally, we try to apply our reflexivity assumption. We obtain a +new assumption whose identical placeholders may be replaced by +any term involving~\bigisa{y}. +\begin{isabelle} +\ 1.\ {\isasymAnd}y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y +\end{isabelle} +This subgoal can only be proved by putting \bigisa{y} for all the placeholders, +making the assumption and conclusion become \isa{R\ y\ y}. +But Isabelle refuses to substitute \bigisa{y}, a bound variable, for +\bigisa{?x}; that would be a bound variable capture. The proof fails. +Note that Isabelle can replace \bigisa{?z2~y} by \bigisa{y}; this involves +instantiating +\bigisa{?z2} to the identity function. + +This example is typical of how Isabelle enforces sound quantifier reasoning. + + +\section{Proving theorems using the \emph{\texttt{blast}} method} + +It is hard to prove substantial theorems using the methods +described above. A proof may be dozens or hundreds of steps long. You +may need to search among different ways of proving certain +subgoals. Often a choice that proves one subgoal renders another +impossible to prove. There are further complications that we have not +discussed, concerning negation and disjunction. Isabelle's +\textbf{classical reasoner} is a family of tools that perform such +proofs automatically. The most important of these is the +{\isa{blast}} method. + +In this section, we shall first see how to use the classical +reasoner in its default mode and then how to insert additional +rules, enabling it to work in new problem domains. + + We begin with examples from pure predicate logic. The following +example is known as Andrew's challenge. Peter Andrews designed +it to be hard to prove by automatic means.% +\footnote{Pelletier~\cite{pelletier86} describes it and many other +problems for automatic theorem provers.} +The nested biconditionals cause an exponential explosion: the formal +proof is enormous. However, the {\isa{blast}} method proves it in +a fraction of a second. +\begin{isabelle} +\isacommand{lemma}\ +"(({\isasymexists}x.\ +{\isasymforall}y.\ +p(x){=}p(y){)}\ +=\ +(({\isasymexists}x.\ +q(x){)}=({\isasymforall}y.\ +p(y){)}){)}\ +\ \ =\ \ \ \ \isanewline +\ \ \ \ \ \ \ \ +(({\isasymexists}x.\ +{\isasymforall}y.\ +q(x){=}q(y){)}\ +=\ +(({\isasymexists}x.\ +p(x){)}=({\isasymforall}y.\ +q(y){)}){)}"\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{done} +\end{isabelle} +The next example is a logic problem composed by Lewis Carroll. +The {\isa{blast}} method finds it trivial. Moreover, it turns out +that not all of the assumptions are necessary. We can easily +experiment with variations of this formula and see which ones +can be proved. +\begin{isabelle} +\isacommand{lemma}\ +"({\isasymforall}x.\ +honest(x)\ \isasymand\ +industrious(x)\ \isasymlongrightarrow\ +healthy(x){)}\ +\isasymand\ \ \isanewline +\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\ +grocer(x)\ \isasymand\ +healthy(x){)}\ +\isasymand\ \isanewline +\ \ \ \ \ \ \ \ ({\isasymforall}x.\ +industrious(x)\ \isasymand\ +grocer(x)\ \isasymlongrightarrow\ +honest(x){)}\ +\isasymand\ \isanewline +\ \ \ \ \ \ \ \ ({\isasymforall}x.\ +cyclist(x)\ \isasymlongrightarrow\ +industrious(x){)}\ +\isasymand\ \isanewline +\ \ \ \ \ \ \ \ ({\isasymforall}x.\ +{\isasymnot}healthy(x)\ \isasymand\ +cyclist(x)\ \isasymlongrightarrow\ +{\isasymnot}honest(x){)}\ +\ \isanewline +\ \ \ \ \ \ \ \ \isasymlongrightarrow\ +({\isasymforall}x.\ +grocer(x)\ \isasymlongrightarrow\ +{\isasymnot}cyclist(x){)}"\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{done} +\end{isabelle} +The {\isa{blast}} method is also effective for set theory, which is +described in the next chapter. This formula below may look horrible, but +the \isa{blast} method proves it easily. +\begin{isabelle} +\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i){)}\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j){)}\ =\isanewline +\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j){)}"\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{done} +\end{isabelle} + +Few subgoals are couched purely in predicate logic and set theory. +We can extend the scope of the classical reasoner by giving it new rules. +Extending it effectively requires understanding the notions of +introduction, elimination and destruction rules. Moreover, there is a +distinction between safe and unsafe rules. A \textbf{safe} rule is one +that can be applied backwards without losing information; an +\textbf{unsafe} rule loses information, perhaps transforming the subgoal +into one that cannot be proved. The safe/unsafe +distinction affects the proof search: if a proof attempt fails, the +classical reasoner backtracks to the most recent unsafe rule application +and makes another choice. + +An important special case avoids all these complications. A logical +equivalence, which in higher-order logic is an equality between +formulas, can be given to the classical +reasoner and simplifier by using the attribute {\isa{iff}}. You +should do so if the right hand side of the equivalence is +simpler than the left-hand side. + +For example, here is a simple fact about list concatenation. +The result of appending two lists is empty if and only if both +of the lists are themselves empty. Obviously, applying this equivalence +will result in a simpler goal. When stating this lemma, we include +the {\isa{iff}} attribute. Once we have proved the lemma, Isabelle +will make it known to the classical reasoner (and to the simplifier). +\begin{isabelle} +\isacommand{lemma}\ +[iff]{:}\ +"(xs{\isacharat}ys\ =\ +\isacharbrackleft{]})\ =\ +(xs=[]\ +\isacharampersand\ +ys=[]{)}"\isanewline +\isacommand{apply}\ (induct_tac\ +xs)\isanewline +\isacommand{apply}\ (simp_all) +\isanewline +\isacommand{done} +\end{isabelle} +% +This fact about multiplication is also appropriate for +the {\isa{iff}} attribute:\remark{the ?s are ugly here but we need +them again when talking about \isa{of}; we need a consistent style} +\begin{isabelle} +(\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0) +\end{isabelle} +A product is zero if and only if one of the factors is zero. The +reasoning involves a logical \textsc{or}. Proving new rules for +disjunctive reasoning is hard, but translating to an actual disjunction +works: the classical reasoner handles disjunction properly. + +In more detail, this is how the {\isa{iff}} attribute works. It converts +the equivalence $P=Q$ to a pair of rules: the introduction +rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the +classical reasoner as safe rules, ensuring that all occurrences of $P$ in +a subgoal are replaced by~$Q$. The simplifier performs the same +replacement, since \isa{iff} gives $P=Q$ to the +simplifier. But classical reasoning is different from +simplification. Simplification is deterministic: it applies rewrite rules +repeatedly, as long as possible, in order to \emph{transform} a goal. Classical +reasoning uses search and backtracking in order to \emph{prove} a goal. + + +\section{Proving the correctness of Euclid's algorithm} +\label{sec:proving-euclid} + +A brief development will illustrate advanced use of +\isa{blast}. In \S\ref{sec:recdef-simplification}, we declared the +recursive function {\isa{gcd}}: +\begin{isabelle} +\isacommand{consts}\ gcd\ :{:}\ {"}nat{\isacharasterisk}nat={\isachargreater}nat"\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline +\isacommand{recdef}\ gcd\ {"}measure\ ((\isasymlambda(m{,}n){.}n)\ :{:}nat{\isacharasterisk}nat={\isachargreater}nat){"}\isanewline +\ \ \ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n){)}"% +\end{isabelle} +Let us prove that it computes the greatest common +divisor of its two arguments. +% +%The declaration yields a recursion +%equation for {\isa{gcd}}. Simplifying with this equation can +%cause looping, expanding to ever-larger expressions of if-then-else +%and {\isa{gcd}} calls. To prevent this, we prove separate simplification rules +%for $n=0$\ldots +%\begin{isabelle} +%\isacommand{lemma}\ gcd_0\ [simp]{:}\ {"}gcd(m,0)\ =\ m"\isanewline +%\isacommand{apply}\ (simp)\isanewline +%\isacommand{done} +%\end{isabelle} +%\ldots{} and for $n>0$: +%\begin{isabelle} +%\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m{,}n)\ =\ gcd\ (n,\ m\ mod\ n){"}\isanewline +%\isacommand{apply}\ (simp)\isanewline +%\isacommand{done} +%\end{isabelle} +%This second rule is similar to the original equation but +%does not loop because it is conditional. It can be applied only +%when the second argument is known to be non-zero. +%Armed with our two new simplification rules, we now delete the +%original {\isa{gcd}} recursion equation. +%\begin{isabelle} +%\isacommand{declare}\ gcd{.}simps\ [simp\ del] +%\end{isabelle} +% +%Now we can prove some interesting facts about the {\isa{gcd}} function, +%for exampe, that it computes a common divisor of its arguments. +% +The theorem is expressed in terms of the familiar +\textbf{divides} relation from number theory: +\begin{isabelle} +?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ \isacharasterisk\ k +\rulename{dvd_def} +\end{isabelle} +% +A simple induction proves the theorem. Here \isa{gcd.induct} refers to the +induction rule returned by \isa{recdef}. The proof relies on the simplification +rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the +definition of \isa{gcd} can cause looping. +\begin{isabelle} +\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m{,}n)\ dvd\ m)\ \isasymand\ (gcd(m{,}n)\ dvd\ n){"}\isanewline +\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd{.}induct)\isanewline +\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline +\isacommand{apply}\ (simp_all)\isanewline +\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline +\isacommand{done}% +\end{isabelle} +Notice that the induction formula +is a conjunction. This is necessary: in the inductive step, each +half of the conjunction establishes the other. The first three proof steps +are applying induction, performing a case analysis on \isa{n}, +and simplifying. Let us pass over these quickly and consider +the use of {\isa{blast}}. We have reached the following +subgoal: +\begin{isabelle} +%gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline +\ 1.\ {\isasymAnd}m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline + \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n){\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m +\end{isabelle} +% +One of the assumptions, the induction hypothesis, is a conjunction. +The two divides relationships it asserts are enough to prove +the conclusion, for we have the following theorem at our disposal: +\begin{isabelle} +\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m% +\rulename{dvd_mod_imp_dvd} +\end{isabelle} +% +This theorem can be applied in various ways. As an introduction rule, it +would cause backward chaining from the conclusion (namely +\isa{?k\ dvd\ ?m}) to the two premises, which +also involve the divides relation. This process does not look promising +and could easily loop. More sensible is to apply the rule in the forward +direction; each step would eliminate the \isa{mod} symboi from an +assumption, so the process must terminate. + +So the final proof step applies the \isa{blast} method. +Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells \isa{blast} +to use it as destruction rule: in the forward direction. + +\medskip +We have proved a conjunction. Now, let us give names to each of the +two halves: +\begin{isabelle} +\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline +\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]% +\end{isabelle} + +Several things are happening here. The keyword \isacommand{lemmas} +tells Isabelle to transform a theorem in some way and to +give a name to the resulting theorem. Attributes can be given, +here \isa{iff}, which supplies the new theorems to the classical reasoner +and the simplifier. The directive {\isa{THEN}}, which will be explained +below, supplies the lemma +\isa{gcd_dvd_both} to the +destruction rule \isa{conjunct1} in order to extract the first part. +\begin{isabelle} +\ \ \ \ \ gcd\ +(?m1,\ +?n1)\ dvd\ +?m1% +\end{isabelle} +The variable names \isa{?m1} and \isa{?n1} arise because +Isabelle renames schematic variables to prevent +clashes. The second \isacommand{lemmas} declaration yields +\begin{isabelle} +\ \ \ \ \ gcd\ +(?m1,\ +?n1)\ dvd\ +?n1% +\end{isabelle} +Later, we shall explore this type of forward reasoning in detail. + +To complete the verification of the {\isa{gcd}} function, we must +prove that it returns the greatest of all the common divisors +of its arguments. The proof is by induction and simplification. +\begin{isabelle} +\isacommand{lemma}\ gcd_greatest\ +[rule_format]{:}\isanewline +\ \ \ \ \ \ \ "(k\ dvd\ +m)\ \isasymlongrightarrow\ (k\ dvd\ +n)\ \isasymlongrightarrow\ k\ dvd\ +gcd(m{,}n)"\isanewline +\isacommand{apply}\ (induct_tac\ m\ n\ +rule:\ gcd{.}induct)\isanewline +\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline +\isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline +\isacommand{done} +\end{isabelle} +% +Note that the theorem has been expressed using HOL implication, +\isa{\isasymlongrightarrow}, because the induction affects the two +preconditions. The directive \isa{rule_format} tells Isabelle to replace +each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before +storing the theorem we have proved. This directive also removes outer +universal quantifiers, converting a theorem into the usual format for +inference rules. + +The facts proved above can be summarized as a single logical +equivalence. This step gives us a chance to see another application +of \isa{blast}, and it is worth doing for sound logical reasons. +\begin{isabelle} +\isacommand{theorem}\ gcd_greatest_iff\ [iff]{:}\isanewline +\ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m{,}n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline +\isacommand{apply}\ (blast\ intro!{:}\ gcd_greatest\ intro:\ dvd_trans)\isanewline +\isacommand{done} +\end{isabelle} +This theorem concisely expresses the correctness of the {\isa{gcd}} +function. +We state it with the {\isa{iff}} attribute so that +Isabelle can use it to remove some occurrences of {\isa{gcd}}. +The theorem has a one-line +proof using {\isa{blast}} supplied with four introduction +rules: note the {\isa{intro}} attribute. The exclamation mark +({\isa{intro}}{\isa{!}})\ signifies safe rules, which are +applied aggressively. Rules given without the exclamation mark +are applied reluctantly and their uses can be undone if +the search backtracks. Here the unsafe rule expresses transitivity +of the divides relation: +\begin{isabelle} +\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p% +\rulename{dvd_trans} +\end{isabelle} +Applying \isa{dvd_trans} as +an introduction rule entails a risk of looping, for it multiplies +occurrences of the divides symbol. However, this proof relies +on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply +aggressively because it yields simpler subgoals. The proof implicitly +uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were +declared using \isa{iff}. + + +\section{Other classical reasoning methods} + +The {\isa{blast}} method is our main workhorse for proving theorems +automatically. Other components of the classical reasoner interact +with the simplifier. Still others perform classical reasoning +to a limited extent, giving the user fine control over the proof. + +Of the latter methods, the most useful is {\isa{clarify}}. It performs +all obvious reasoning steps without splitting the goal into multiple +parts. It does not apply rules that could render the +goal unprovable (so-called unsafe rules). By performing the obvious +steps, {\isa{clarify}} lays bare the difficult parts of the problem, +where human intervention is necessary. + +For example, the following conjecture is false: +\begin{isabelle} +\isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\ +({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\ +\isasymand\ Q\ x)"\isanewline +\isacommand{apply}\ clarify +\end{isabelle} +The {\isa{blast}} method would simply fail, but {\isa{clarify}} presents +a subgoal that helps us see why we cannot continue the proof. +\begin{isabelle} +\ 1.\ {\isasymAnd}x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\ +xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x +\end{isabelle} +The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x} +refer to distinct bound variables. To reach this state, \isa{clarify} applied +the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall} +and the elimination rule for ~\isa{\isasymand}. It did not apply the introduction +rule for \isa{\isasymand} because of its policy never to split goals. + +Also available is {\isa{clarsimp}}, a method that interleaves {\isa{clarify}} +and {\isa{simp}}. Also there is \isa{safe}, which like \isa{clarify} performs +obvious steps and even applies those that split goals. + +The {\isa{force}} method applies the classical reasoner and simplifier +to one goal. +\remark{example needed? most +things done by blast, simp or auto can also be done by force, so why add a new +one?} +Unless it can prove the goal, it fails. Contrast +that with the auto method, which also combines classical reasoning +with simplification. The latter's purpose is to prove all the +easy subgoals and parts of subgoals. Unfortunately, it can produce +large numbers of new subgoals; also, since it proves some subgoals +and splits others, it obscures the structure of the proof tree. +The {\isa{force}} method does not have these drawbacks. Another +difference: {\isa{force}} tries harder than {\isa{auto}} to prove +its goal, so it can take much longer to terminate. + +Older components of the classical reasoner have largely been +superseded by {\isa{blast}}, but they still have niche applications. +Most important among these are {\isa{fast}} and {\isa{best}}. While {\isa{blast}} +searches for proofs using a built-in first-order reasoner, these +earlier methods search for proofs using standard Isabelle inference. +That makes them slower but enables them to work correctly in the +presence of the more unusual features of Isabelle rules, such +as type classes and function unknowns. For example, the introduction rule +for Hilbert's epsilon-operator has the following form: +\begin{isabelle} +?P\ ?x\ \isasymLongrightarrow\ ?P\ (Eps\ ?P) +\rulename{someI} +\end{isabelle} + +The repeated occurrence of the variable \isa{?P} makes this rule tricky +to apply. Consider this contrived example: +\begin{isabelle} +\isacommand{lemma}\ "{\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\isanewline +\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\ +\isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline +\isacommand{apply}\ (rule\ someI) +\end{isabelle} +% +We can apply rule \isa{someI} explicitly. It yields the +following subgoal: +\begin{isabelle} +\ 1.\ {\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\ +\isasymand\ Q\ ?x% +\end{isabelle} +The proof from this point is trivial. The question now arises, could we have +proved the theorem with a single command? Not using {\isa{blast}} method: it +cannot perform the higher-order unification that is necessary here. The +{\isa{fast}} method succeeds: +\begin{isabelle} +\isacommand{apply}\ (fast\ intro!:\ someI) +\end{isabelle} + +The {\isa{best}} method is similar to {\isa{fast}} but it uses a +best-first search instead of depth-first search. Accordingly, +it is slower but is less susceptible to divergence. Transitivity +rules usually cause {\isa{fast}} to loop where often {\isa{best}} +can manage. + +Here is a summary of the classical reasoning methods: +\begin{itemize} +\item \isa{blast} works automatically and is the fastest +\item \isa{clarify} and \isa{clarsimp} perform obvious steps without splitting the +goal; \isa{safe} even splits goals +\item \isa{force} uses classical reasoning and simplification to prove a goal; + \isa{auto} is similar but leaves what it cannot prove +\item \isa{fast} and \isa{best} are legacy methods that work well with rules involving +unusual features +\end{itemize} +A table illustrates the relationships among four of these methods. +\begin{center} +\begin{tabular}{r|l|l|} + & no split & split \\ \hline + no simp & \isa{clarify} & \isa{safe} \\ \hline + simp & \isa{clarsimp} & \isa{auto} \\ \hline +\end{tabular} +\end{center} + + + + +\section{Forward proof}\label{sec:forward} + +Forward proof means deriving new facts from old ones. It is the +most fundamental type of proof. Backward proof, by working from goals to +subgoals, can help us find a difficult proof. But it is +not always the best way of presenting the proof so found. Forward +proof is particuarly good for reasoning from the general +to the specific. For example, consider the following distributive law for +the +\isa{gcd} function: +\[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\] + +Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$) +\[ k = \gcd(k,k\times n)\] +We have derived a new fact about \isa{gcd}; if re-oriented, it might be +useful for simplification. After re-orienting it and putting $n=1$, we +derive another useful law: +\[ \gcd(k,k)=k \] +Substituting values for variables --- instantiation --- is a forward step. +Re-orientation works by applying the symmetry of equality to +an equation, so it too is a forward step. + +Now let us reproduce our examples in Isabelle. Here is the distributive +law: +\begin{isabelle}% +?k\ \isacharasterisk\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ \isacharasterisk\ ?m,\ ?k\ \isacharasterisk\ ?n) +\rulename{gcd_mult_distrib2} +\end{isabelle}% +The first step is to replace \isa{?m} by~1 in this law. We refer to the +variables not by name but by their position in the theorem, from left to +right. In this case, the variables are \isa{?k}, \isa{?m} and~\isa{?n}. +So, the expression +\hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m} +by~\isa{1}. +\begin{isabelle} +\isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1] +\end{isabelle} +% +The command +\isa{thm gcd_mult_0} +displays the resulting theorem: +\begin{isabelle} +\ \ \ \ \ k\ \isacharasterisk\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ \isacharasterisk\ 1,\ k\ \isacharasterisk\ ?n) +\end{isabelle} +Something is odd: {\isa{k}} is an ordinary variable, while {\isa{?n}} +is schematic. We did not specify an instantiation +for {\isa{?n}}. In its present form, the theorem does not allow +substitution for {\isa{k}}. One solution is to avoid giving an instantiation for +\isa{?k}: instead of a term we can put an underscore~(\isa{_}). For example, +\begin{isabelle} +\ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1] +\end{isabelle} +replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged. Anyway, let us put +the theorem \isa{gcd_mult_0} into a simplified form: +\begin{isabelle} +\isacommand{lemmas}\ +gcd_mult_1\ =\ gcd_mult_0\ +[simplified]% +\end{isabelle} +% +Again, we display the resulting theorem: +\begin{isabelle} +\ \ \ \ \ k\ =\ gcd\ (k,\ k\ \isacharasterisk\ ?n) +\end{isabelle} +% +To re-orient the equation requires the symmetry rule: +\begin{isabelle} +?s\ =\ ?t\ +\isasymLongrightarrow\ ?t\ =\ +?s% +\rulename{sym} +\end{isabelle} +The following declaration gives our equation to \isa{sym}: +\begin{isabelle} +\ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\ +[THEN\ sym] +\end{isabelle} +% +Here is the result: +\begin{isabelle} +\ \ \ \ \ gcd\ (k,\ k\ \isacharasterisk\ +?n)\ =\ k% +\end{isabelle} +\isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the +resulting conclusion.\remark{figure necessary?} The effect is to exchange the +two operands of the equality. Typically {\isa{THEN}} is used with destruction +rules. Above we have used +\isa{THEN~conjunct1} to extract the first part of the theorem +\isa{gcd_dvd_both}. Also useful is \isa{THEN~spec}, which removes the quantifier +from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp}, which converts the +implication $P\imp Q$ into the rule $\vcenter{\infer{Q}{P}}$. +Similar to \isa{mp} are the following two rules, which extract +the two directions of reasoning about a boolean equivalence: +\begin{isabelle} +\isasymlbrakk?Q\ =\ +?P;\ ?Q\isasymrbrakk\ +\isasymLongrightarrow\ ?P% +\rulename{iffD1}% +\isanewline +\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ +\isasymLongrightarrow\ ?P% +\rulename{iffD2} +\end{isabelle} +% +Normally we would never name the intermediate theorems +such as \isa{gcd_mult_0} and +\isa{gcd_mult_1} but would combine +the three forward steps: +\begin{isabelle} +\isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]% +\end{isabelle} +The directives, or attributes, are processed from left to right. This +declaration of \isa{gcd_mult} is equivalent to the +previous one. + +Such declarations can make the proof script hard to read: +what is being proved? More legible +is to state the new lemma explicitly and to prove it using a single +\isa{rule} method whose operand is expressed using forward reasoning: +\begin{isabelle} +\isacommand{lemma}\ gcd_mult\ +[simp]{:}\ +"gcd(k,\ +k{\isacharasterisk}n)\ =\ +k"\isanewline +\isacommand{apply}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]{)}\isanewline +\isacommand{done} +\end{isabelle} +Compared with the previous proof of \isa{gcd_mult}, this +version shows the reader what has been proved. Also, it receives +the usual Isabelle treatment. In particular, Isabelle generalizes over all +variables: the resulting theorem will have {\isa{?k}} instead of {\isa{k}}. + +At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here +is the Isabelle version: +\begin{isabelle} +\isacommand{lemma}\ gcd_self\ +[simp]{:}\ +"gcd(k{,}k)\ +=\ k"\isanewline +\isacommand{apply}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified]{)}\isanewline +\isacommand{done} +\end{isabelle} + +Recall that \isa{of} generates an instance of a rule by specifying +values for its variables. Analogous is \isa{OF}, which generates an +instance of a rule by specifying facts for its premises. Let us try +it with this rule: +\begin{isabelle} +{\isasymlbrakk}gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n){\isasymrbrakk}\ +\isasymLongrightarrow\ ?k\ dvd\ ?m +\rulename{relprime_dvd_mult} +\end{isabelle} +First, we +prove an instance of its first premise: +\begin{isabelle} +\isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline +\isacommand{apply}\ (simp\ add:\ gcd{.}simps)\isanewline +\isacommand{done}% +\end{isabelle} +We have evaluated an application of the \isa{gcd} function by +simplification. Expression evaluation is not guaranteed to terminate, and +certainly is not efficient; Isabelle performs arithmetic operations by +rewriting symbolic bit strings. Here, however, the simplification takes +less than one second. We can specify this new lemma to {\isa{OF}}, +generating an instance of \isa{relprime_dvd_mult}. The expression +\begin{isabelle} +\ \ \ \ \ relprime_dvd_mult [OF relprime_20_81] +\end{isabelle} +yields the theorem +\begin{isabelle} +\ \ \ \ \ \isacharhash20\ dvd\ (?m\ \isacharasterisk\ \isacharhash81)\ \isasymLongrightarrow\ \isacharhash20\ dvd\ ?m% +\end{isabelle} +% +{\isa{OF}} takes any number of operands. Consider +the following facts about the divides relation: +\begin{isabelle} +\isasymlbrakk?k\ dvd\ ?m;\ +?k\ dvd\ ?n\isasymrbrakk\ +\isasymLongrightarrow\ ?k\ dvd\ +(?m\ \isacharplus\ +?n) +\rulename{dvd_add}\isanewline +?m\ dvd\ ?m% +\rulename{dvd_refl} +\end{isabelle} +Let us supply \isa{dvd_refl} for each of the premises of \isa{dvd_add}: +\begin{isabelle} +\ \ \ \ \ dvd_add [OF dvd_refl dvd_refl] +\end{isabelle} +Here is the theorem that we have expressed: +\begin{isabelle} +\ \ \ \ \ ?k\ dvd\ (?k\ \isacharplus\ ?k) +\end{isabelle} +As with \isa{of}, we can use the \isa{_} symbol to leave some positions +unspecified: +\begin{isabelle} +\ \ \ \ \ dvd_add [OF _ dvd_refl] +\end{isabelle} +The result is +\begin{isabelle} +\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ \isacharplus\ ?k) +\end{isabelle} + +You may have noticed that {\isa{THEN}} and {\isa{OF}} are based on +the same idea, namely to combine two rules. They differ in the +order of the combination and thus in their effect. We use \isa{THEN} +typically with a destruction rule to extract a subformula of the current +theorem. We use \isa{OF} with a list of facts to generate an instance of +the current theorem. + + +Here is a summary of the primitives for forward reasoning: +\begin{itemize} +\item {\isa{of}} instantiates the variables of a rule to a list of terms +\item {\isa{OF}} applies a rule to a list of theorems +\item {\isa{THEN}} gives a theorem to a named rule and returns the +conclusion +\end{itemize} + + +\section{Methods for forward proof} + +We have seen that forward proof works well within a backward +proof. Also in that spirit is the \isa{insert} method, which inserts a +given theorem as a new assumption of the current subgoal. This already +is a forward step; moreover, we may (as always when using a theorem) apply +{\isa{of}}, {\isa{THEN}} and other directives. The new assumption can then +be used to help prove the subgoal. + +For example, consider this theorem about the divides relation. +Only the first proof step is given; it inserts the distributive law for +\isa{gcd}. We specify its variables as shown. +\begin{isabelle} +\isacommand{lemma}\ +relprime_dvd_mult:\isanewline +\ \ \ \ \ \ \ "{\isasymlbrakk}\ gcd(k,n){=}1;\ +k\ dvd\ (m*n)\ +{\isasymrbrakk}\ +\isasymLongrightarrow\ k\ dvd\ +m"\isanewline +\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\ +n]) +\end{isabelle} +In the resulting subgoal, note how the equation has been +inserted: +\begin{isabelle} +{\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ +dvd\ (m\ \isacharasterisk\ +n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\ +m\isanewline +\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline +\ \ \ \ \ m\ \isacharasterisk\ gcd\ +(k,\ n)\ +=\ gcd\ (m\ \isacharasterisk\ +k,\ m\ \isacharasterisk\ +n){\isasymrbrakk}\isanewline +\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m +\end{isabelle} +The next proof step, \isa{\isacommand{apply}(simp)}, +utilizes the assumption \isa{gcd(k,n)\ =\ +1}. Here is the result: +\begin{isabelle} +{\isasymlbrakk}gcd\ (k,\ +n)\ =\ 1;\ k\ +dvd\ (m\ \isacharasterisk\ +n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\ +m\isanewline +\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline +\ \ \ \ \ m\ =\ gcd\ (m\ +\isacharasterisk\ k,\ m\ \isacharasterisk\ +n){\isasymrbrakk}\isanewline +\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m +\end{isabelle} +Simplification has yielded an equation for \isa{m} that will be used to +complete the proof. + +\medskip +Here is another proof using \isa{insert}. \remark{Effect with unknowns?} +Division and remainder obey a well-known law: +\begin{isabelle} +(?m\ div\ ?n)\ \isacharasterisk\ +?n\ \isacharplus\ ?m\ mod\ ?n\ +=\ ?m +\rulename{mod_div_equality} +\end{isabelle} + +We refer to this law explicitly in the following proof: +\begin{isabelle} +\isacommand{lemma}\ div_mult_self_is_m:\ \isanewline +\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m{\isacharasterisk}n)\ div\ n\ =\ (m:{:}nat)"\isanewline +\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m{\isacharasterisk}n"\ n]{)}\isanewline +\isacommand{apply}\ (simp)\isanewline +\isacommand{done} +\end{isabelle} +The first step inserts the law, specifying \isa{m*n} and +\isa{n} for its variables. Notice that nontrivial expressions must be +enclosed in quotation marks. Here is the resulting +subgoal, with its new assumption: +\begin{isabelle} +%0\ \isacharless\ n\ \isasymLongrightarrow\ (m\ +%\isacharasterisk\ n)\ div\ n\ =\ m\isanewline +\ 1.\ \isasymlbrakk0\ \isacharless\ +n;\ \ (m\ \isacharasterisk\ n)\ div\ n\ +\isacharasterisk\ n\ \isacharplus\ (m\ \isacharasterisk\ n)\ mod\ n\ +=\ m\ \isacharasterisk\ n\isasymrbrakk\isanewline +\ \ \ \ \isasymLongrightarrow\ (m\ \isacharasterisk\ n)\ div\ n\ +=\ m +\end{isabelle} +Simplification reduces \isa{(m\ \isacharasterisk\ n)\ mod\ n} to zero. +Then it cancels the factor~\isa{n} on both +sides of the equation, proving the theorem. + +\medskip +A similar method is {\isa{subgoal\_tac}}. Instead of inserting +a theorem as an assumption, it inserts an arbitrary formula. +This formula must be proved later as a separate subgoal. The +idea is to claim that the formula holds on the basis of the current +assumptions, to use this claim to complete the proof, and finally +to justify the claim. It is a valuable means of giving the proof +some structure. The explicit formula will be more readable than +proof commands that yield that formula indirectly. + +Look at the following example. +\begin{isabelle} +\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ \#37;\ \#66\ <\ \#2*z;\ z*z\ +\isasymnoteq\ \#1225;\ Q(\#34);\ Q(\#36)\isasymrbrakk\isanewline +\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline +\isacommand{apply}\ (subgoal_tac\ "z\ =\ \#34\ \isasymor\ z\ =\ +\#36")\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ \#35")\isanewline +\isacommand{apply}\ arith\isanewline +\isacommand{apply}\ force\isanewline +\isacommand{done} +\end{isabelle} +Let us prove it informally. The first assumption tells us +that \isa{z} is no greater than 36. The second tells us that \isa{z} +is at least 34. The third assumption tells us that \isa{z} cannot be 35, since +$35\times35=1225$. So \isa{z} is either 34 or 36, and since \isa{Q} holds for +both of those values, we have the conclusion. + +The Isabelle proof closely follows this reasoning. The first +step is to claim that \isa{z} is either 34 or 36. The resulting proof +state gives us two subgoals: +\begin{isabelle} +%{\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ +%Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline +\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline +\ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline +\ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline +\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline +\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36 +\end{isabelle} + +The first subgoal is trivial, but for the second Isabelle needs help to eliminate +the case +\isa{z}=35. The second invocation of {\isa{subgoal\_tac}} leaves two +subgoals: +\begin{isabelle} +\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ +\#1225;\ Q\ \#34;\ Q\ \#36;\isanewline +\ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline +\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline +\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline +\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35 +\end{isabelle} + +Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic: +the method {\isa{arith}}. For the second subgoal we apply the method {\isa{force}}, +which proceeds by assuming that \isa{z}=35 and arriving at a contradiction. + + +\medskip +Summary of these methods: +\begin{itemize} +\item {\isa{insert}} adds a theorem as a new assumption +\item {\isa{subgoal_tac}} adds a formula as a new assumption and leaves the +subgoal of proving that formula +\end{itemize}