1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/Rules/Forward.thy Wed Jan 10 11:09:11 2001 +0100
1.3 @@ -0,0 +1,202 @@
1.4 +theory Forward = Primes:
1.5 +
1.6 +text{*\noindent
1.7 +Forward proof material: of, OF, THEN, simplify, rule_format.
1.8 +*}
1.9 +
1.10 +text{*\noindent
1.11 +SKIP most developments...
1.12 +*}
1.13 +
1.14 +(** Commutativity **)
1.15 +
1.16 +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
1.17 + apply (auto simp add: is_gcd_def);
1.18 + done
1.19 +
1.20 +lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
1.21 + apply (rule is_gcd_unique)
1.22 + apply (rule is_gcd)
1.23 + apply (subst is_gcd_commute)
1.24 + apply (simp add: is_gcd)
1.25 + done
1.26 +
1.27 +lemma gcd_1 [simp]: "gcd(m,1) = 1"
1.28 + apply (simp)
1.29 + done
1.30 +
1.31 +lemma gcd_1_left [simp]: "gcd(1,m) = 1"
1.32 + apply (simp add: gcd_commute [of 1])
1.33 + done
1.34 +
1.35 +text{*\noindent
1.36 +as far as HERE.
1.37 +*}
1.38 +
1.39 +
1.40 +text {*
1.41 +@{thm[display] gcd_1}
1.42 +\rulename{gcd_1}
1.43 +
1.44 +@{thm[display] gcd_1_left}
1.45 +\rulename{gcd_1_left}
1.46 +*};
1.47 +
1.48 +text{*\noindent
1.49 +SKIP THIS PROOF
1.50 +*}
1.51 +
1.52 +lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
1.53 +apply (induct_tac m n rule: gcd.induct)
1.54 +apply (case_tac "n=0")
1.55 +apply (simp)
1.56 +apply (case_tac "k=0")
1.57 +apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
1.58 +done
1.59 +
1.60 +text {*
1.61 +@{thm[display] gcd_mult_distrib2}
1.62 +\rulename{gcd_mult_distrib2}
1.63 +*};
1.64 +
1.65 +text{*\noindent
1.66 +of, simplified
1.67 +*}
1.68 +
1.69 +
1.70 +lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1];
1.71 +lemmas gcd_mult_1 = gcd_mult_0 [simplified];
1.72 +
1.73 +text {*
1.74 +@{thm[display] gcd_mult_distrib2 [of _ 1]}
1.75 +
1.76 +@{thm[display] gcd_mult_0}
1.77 +\rulename{gcd_mult_0}
1.78 +
1.79 +@{thm[display] gcd_mult_1}
1.80 +\rulename{gcd_mult_1}
1.81 +
1.82 +@{thm[display] sym}
1.83 +\rulename{sym}
1.84 +*};
1.85 +
1.86 +lemmas gcd_mult = gcd_mult_1 [THEN sym];
1.87 +
1.88 +lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
1.89 + (*better in one step!*)
1.90 +
1.91 +text {*
1.92 +more legible
1.93 +*};
1.94 +
1.95 +lemma gcd_mult [simp]: "gcd(k, k*n) = k"
1.96 +by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
1.97 +
1.98 +
1.99 +lemmas gcd_self = gcd_mult [of k 1, simplified];
1.100 +
1.101 +
1.102 +text {*
1.103 +Rules handy with THEN
1.104 +
1.105 +@{thm[display] iffD1}
1.106 +\rulename{iffD1}
1.107 +
1.108 +@{thm[display] iffD2}
1.109 +\rulename{iffD2}
1.110 +*};
1.111 +
1.112 +
1.113 +text {*
1.114 +again: more legible
1.115 +*};
1.116 +
1.117 +lemma gcd_self [simp]: "gcd(k,k) = k"
1.118 +by (rule gcd_mult [of k 1, simplified])
1.119 +
1.120 +
1.121 +lemma relprime_dvd_mult:
1.122 + "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m";
1.123 +apply (insert gcd_mult_distrib2 [of m k n])
1.124 +apply (simp)
1.125 +apply (erule_tac t="m" in ssubst);
1.126 +apply (simp)
1.127 +done
1.128 +
1.129 +
1.130 +text {*
1.131 +Another example of "insert"
1.132 +
1.133 +@{thm[display] mod_div_equality}
1.134 +\rulename{mod_div_equality}
1.135 +*};
1.136 +
1.137 +lemma div_mult_self_is_m:
1.138 + "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
1.139 +apply (insert mod_div_equality [of "m*n" n])
1.140 +apply (simp)
1.141 +done
1.142 +
1.143 +lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
1.144 +by (blast intro: relprime_dvd_mult dvd_trans)
1.145 +
1.146 +
1.147 +lemma relprime_20_81: "gcd(#20,#81) = 1";
1.148 +by (simp add: gcd.simps)
1.149 +
1.150 +
1.151 +
1.152 +text {*
1.153 +Examples of 'OF'
1.154 +
1.155 +@{thm[display] relprime_dvd_mult}
1.156 +\rulename{relprime_dvd_mult}
1.157 +
1.158 +@{thm[display] relprime_dvd_mult [OF relprime_20_81]}
1.159 +
1.160 +@{thm[display] dvd_refl}
1.161 +\rulename{dvd_refl}
1.162 +
1.163 +@{thm[display] dvd_add}
1.164 +\rulename{dvd_add}
1.165 +
1.166 +@{thm[display] dvd_add [OF dvd_refl dvd_refl]}
1.167 +
1.168 +@{thm[display] dvd_add [OF _ dvd_refl]}
1.169 +*};
1.170 +
1.171 +lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)";
1.172 +apply (subgoal_tac "z = #34 \<or> z = #36")
1.173 +apply blast
1.174 +apply (subgoal_tac "z \<noteq> #35")
1.175 +apply arith
1.176 +apply force
1.177 +done
1.178 +
1.179 +text
1.180 +{*
1.181 +proof\ (prove):\ step\ 1\isanewline
1.182 +\isanewline
1.183 +goal\ (lemma):\isanewline
1.184 +\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline
1.185 +\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
1.186 +\ \ \ \ \ \ \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isasymrbrakk \isanewline
1.187 +\ \ \ \ \isasymLongrightarrow \ Q\ z\isanewline
1.188 +\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline
1.189 +\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36
1.190 +
1.191 +
1.192 +
1.193 +proof\ (prove):\ step\ 3\isanewline
1.194 +\isanewline
1.195 +goal\ (lemma):\isanewline
1.196 +\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline
1.197 +\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
1.198 +\ \ \ \ \ \ \ z\ \isasymnoteq \ \#35\isasymrbrakk \isanewline
1.199 +\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isanewline
1.200 +\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline
1.201 +\ \ \ \ \isasymLongrightarrow \ z\ \isasymnoteq \ \#35
1.202 +*}
1.203 +
1.204 +
1.205 +end