|
1 theory Forward imports Primes begin |
|
2 |
|
3 text{*\noindent |
|
4 Forward proof material: of, OF, THEN, simplify, rule_format. |
|
5 *} |
|
6 |
|
7 text{*\noindent |
|
8 SKIP most developments... |
|
9 *} |
|
10 |
|
11 (** Commutativity **) |
|
12 |
|
13 lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" |
|
14 apply (auto simp add: is_gcd_def); |
|
15 done |
|
16 |
|
17 lemma gcd_commute: "gcd m n = gcd n m" |
|
18 apply (rule is_gcd_unique) |
|
19 apply (rule is_gcd) |
|
20 apply (subst is_gcd_commute) |
|
21 apply (simp add: is_gcd) |
|
22 done |
|
23 |
|
24 lemma gcd_1 [simp]: "gcd m (Suc 0) = Suc 0" |
|
25 apply simp |
|
26 done |
|
27 |
|
28 lemma gcd_1_left [simp]: "gcd (Suc 0) m = Suc 0" |
|
29 apply (simp add: gcd_commute [of "Suc 0"]) |
|
30 done |
|
31 |
|
32 text{*\noindent |
|
33 as far as HERE. |
|
34 *} |
|
35 |
|
36 text{*\noindent |
|
37 SKIP THIS PROOF |
|
38 *} |
|
39 |
|
40 lemma gcd_mult_distrib2: "k * gcd m n = gcd (k*m) (k*n)" |
|
41 apply (induct_tac m n rule: gcd.induct) |
|
42 apply (case_tac "n=0") |
|
43 apply simp |
|
44 apply (case_tac "k=0") |
|
45 apply simp_all |
|
46 done |
|
47 |
|
48 text {* |
|
49 @{thm[display] gcd_mult_distrib2} |
|
50 \rulename{gcd_mult_distrib2} |
|
51 *}; |
|
52 |
|
53 text{*\noindent |
|
54 of, simplified |
|
55 *} |
|
56 |
|
57 |
|
58 lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]; |
|
59 lemmas gcd_mult_1 = gcd_mult_0 [simplified]; |
|
60 |
|
61 lemmas where1 = gcd_mult_distrib2 [where m=1] |
|
62 |
|
63 lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1] |
|
64 |
|
65 lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] |
|
66 |
|
67 text {* |
|
68 example using ``of'': |
|
69 @{thm[display] gcd_mult_distrib2 [of _ 1]} |
|
70 |
|
71 example using ``where'': |
|
72 @{thm[display] gcd_mult_distrib2 [where m=1]} |
|
73 |
|
74 example using ``where'', ``and'': |
|
75 @{thm[display] gcd_mult_distrib2 [where m=1 and k="j+k"]} |
|
76 |
|
77 @{thm[display] gcd_mult_0} |
|
78 \rulename{gcd_mult_0} |
|
79 |
|
80 @{thm[display] gcd_mult_1} |
|
81 \rulename{gcd_mult_1} |
|
82 |
|
83 @{thm[display] sym} |
|
84 \rulename{sym} |
|
85 *}; |
|
86 |
|
87 lemmas gcd_mult0 = gcd_mult_1 [THEN sym]; |
|
88 (*not quite right: we need ?k but this gives k*) |
|
89 |
|
90 lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]; |
|
91 (*better in one step!*) |
|
92 |
|
93 text {* |
|
94 more legible, and variables properly generalized |
|
95 *}; |
|
96 |
|
97 lemma gcd_mult [simp]: "gcd k (k*n) = k" |
|
98 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym]) |
|
99 |
|
100 |
|
101 lemmas gcd_self0 = gcd_mult [of k 1, simplified]; |
|
102 |
|
103 |
|
104 text {* |
|
105 @{thm[display] gcd_mult} |
|
106 \rulename{gcd_mult} |
|
107 |
|
108 @{thm[display] gcd_self0} |
|
109 \rulename{gcd_self0} |
|
110 *}; |
|
111 |
|
112 text {* |
|
113 Rules handy with THEN |
|
114 |
|
115 @{thm[display] iffD1} |
|
116 \rulename{iffD1} |
|
117 |
|
118 @{thm[display] iffD2} |
|
119 \rulename{iffD2} |
|
120 *}; |
|
121 |
|
122 |
|
123 text {* |
|
124 again: more legible, and variables properly generalized |
|
125 *}; |
|
126 |
|
127 lemma gcd_self [simp]: "gcd k k = k" |
|
128 by (rule gcd_mult [of k 1, simplified]) |
|
129 |
|
130 |
|
131 text{* |
|
132 NEXT SECTION: Methods for Forward Proof |
|
133 |
|
134 NEW |
|
135 |
|
136 theorem arg_cong, useful in forward steps |
|
137 @{thm[display] arg_cong[no_vars]} |
|
138 \rulename{arg_cong} |
|
139 *} |
|
140 |
|
141 lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)" |
|
142 apply (intro notI) |
|
143 txt{* |
|
144 before using arg_cong |
|
145 @{subgoals[display,indent=0,margin=65]} |
|
146 *}; |
|
147 apply (drule_tac f="\<lambda>x. x mod u" in arg_cong) |
|
148 txt{* |
|
149 after using arg_cong |
|
150 @{subgoals[display,indent=0,margin=65]} |
|
151 *}; |
|
152 apply (simp add: mod_Suc) |
|
153 done |
|
154 |
|
155 text{* |
|
156 have just used this rule: |
|
157 @{thm[display] mod_Suc[no_vars]} |
|
158 \rulename{mod_Suc} |
|
159 |
|
160 @{thm[display] mult_le_mono1[no_vars]} |
|
161 \rulename{mult_le_mono1} |
|
162 *} |
|
163 |
|
164 |
|
165 text{* |
|
166 example of "insert" |
|
167 *} |
|
168 |
|
169 lemma relprime_dvd_mult: |
|
170 "\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m" |
|
171 apply (insert gcd_mult_distrib2 [of m k n]) |
|
172 txt{*@{subgoals[display,indent=0,margin=65]}*} |
|
173 apply simp |
|
174 txt{*@{subgoals[display,indent=0,margin=65]}*} |
|
175 apply (erule_tac t="m" in ssubst); |
|
176 apply simp |
|
177 done |
|
178 |
|
179 |
|
180 text {* |
|
181 @{thm[display] relprime_dvd_mult} |
|
182 \rulename{relprime_dvd_mult} |
|
183 |
|
184 Another example of "insert" |
|
185 |
|
186 @{thm[display] mod_div_equality} |
|
187 \rulename{mod_div_equality} |
|
188 *}; |
|
189 |
|
190 (*MOVED to Force.thy, which now depends only on Divides.thy |
|
191 lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)" |
|
192 *) |
|
193 |
|
194 lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"; |
|
195 by (auto intro: relprime_dvd_mult elim: dvdE) |
|
196 |
|
197 lemma relprime_20_81: "gcd 20 81 = 1"; |
|
198 by (simp add: gcd.simps) |
|
199 |
|
200 text {* |
|
201 Examples of 'OF' |
|
202 |
|
203 @{thm[display] relprime_dvd_mult} |
|
204 \rulename{relprime_dvd_mult} |
|
205 |
|
206 @{thm[display] relprime_dvd_mult [OF relprime_20_81]} |
|
207 |
|
208 @{thm[display] dvd_refl} |
|
209 \rulename{dvd_refl} |
|
210 |
|
211 @{thm[display] dvd_add} |
|
212 \rulename{dvd_add} |
|
213 |
|
214 @{thm[display] dvd_add [OF dvd_refl dvd_refl]} |
|
215 |
|
216 @{thm[display] dvd_add [OF _ dvd_refl]} |
|
217 *}; |
|
218 |
|
219 lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)"; |
|
220 apply (subgoal_tac "z = 34 \<or> z = 36") |
|
221 txt{* |
|
222 the tactic leaves two subgoals: |
|
223 @{subgoals[display,indent=0,margin=65]} |
|
224 *}; |
|
225 apply blast |
|
226 apply (subgoal_tac "z \<noteq> 35") |
|
227 txt{* |
|
228 the tactic leaves two subgoals: |
|
229 @{subgoals[display,indent=0,margin=65]} |
|
230 *}; |
|
231 apply arith |
|
232 apply force |
|
233 done |
|
234 |
|
235 |
|
236 end |