|
1 theory Forward = Primes: |
|
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,1) = 1" |
|
25 apply (simp) |
|
26 done |
|
27 |
|
28 lemma gcd_1_left [simp]: "gcd(1,m) = 1" |
|
29 apply (simp add: gcd_commute [of 1]) |
|
30 done |
|
31 |
|
32 text{*\noindent |
|
33 as far as HERE. |
|
34 *} |
|
35 |
|
36 |
|
37 text {* |
|
38 @{thm[display] gcd_1} |
|
39 \rulename{gcd_1} |
|
40 |
|
41 @{thm[display] gcd_1_left} |
|
42 \rulename{gcd_1_left} |
|
43 *}; |
|
44 |
|
45 text{*\noindent |
|
46 SKIP THIS PROOF |
|
47 *} |
|
48 |
|
49 lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)" |
|
50 apply (induct_tac m n rule: gcd.induct) |
|
51 apply (case_tac "n=0") |
|
52 apply (simp) |
|
53 apply (case_tac "k=0") |
|
54 apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) |
|
55 done |
|
56 |
|
57 text {* |
|
58 @{thm[display] gcd_mult_distrib2} |
|
59 \rulename{gcd_mult_distrib2} |
|
60 *}; |
|
61 |
|
62 text{*\noindent |
|
63 of, simplified |
|
64 *} |
|
65 |
|
66 |
|
67 lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]; |
|
68 lemmas gcd_mult_1 = gcd_mult_0 [simplified]; |
|
69 |
|
70 text {* |
|
71 @{thm[display] gcd_mult_distrib2 [of _ 1]} |
|
72 |
|
73 @{thm[display] gcd_mult_0} |
|
74 \rulename{gcd_mult_0} |
|
75 |
|
76 @{thm[display] gcd_mult_1} |
|
77 \rulename{gcd_mult_1} |
|
78 |
|
79 @{thm[display] sym} |
|
80 \rulename{sym} |
|
81 *}; |
|
82 |
|
83 lemmas gcd_mult = gcd_mult_1 [THEN sym]; |
|
84 |
|
85 lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym]; |
|
86 (*better in one step!*) |
|
87 |
|
88 text {* |
|
89 more legible |
|
90 *}; |
|
91 |
|
92 lemma gcd_mult [simp]: "gcd(k, k*n) = k" |
|
93 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym]) |
|
94 |
|
95 |
|
96 lemmas gcd_self = gcd_mult [of k 1, simplified]; |
|
97 |
|
98 |
|
99 text {* |
|
100 Rules handy with THEN |
|
101 |
|
102 @{thm[display] iffD1} |
|
103 \rulename{iffD1} |
|
104 |
|
105 @{thm[display] iffD2} |
|
106 \rulename{iffD2} |
|
107 *}; |
|
108 |
|
109 |
|
110 text {* |
|
111 again: more legible |
|
112 *}; |
|
113 |
|
114 lemma gcd_self [simp]: "gcd(k,k) = k" |
|
115 by (rule gcd_mult [of k 1, simplified]) |
|
116 |
|
117 |
|
118 lemma relprime_dvd_mult: |
|
119 "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"; |
|
120 apply (insert gcd_mult_distrib2 [of m k n]) |
|
121 apply (simp) |
|
122 apply (erule_tac t="m" in ssubst); |
|
123 apply (simp) |
|
124 done |
|
125 |
|
126 |
|
127 text {* |
|
128 Another example of "insert" |
|
129 |
|
130 @{thm[display] mod_div_equality} |
|
131 \rulename{mod_div_equality} |
|
132 *}; |
|
133 |
|
134 lemma div_mult_self_is_m: |
|
135 "0<n \<Longrightarrow> (m*n) div n = (m::nat)" |
|
136 apply (insert mod_div_equality [of "m*n" n]) |
|
137 apply (simp) |
|
138 done |
|
139 |
|
140 lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"; |
|
141 by (blast intro: relprime_dvd_mult dvd_trans) |
|
142 |
|
143 |
|
144 lemma relprime_20_81: "gcd(#20,#81) = 1"; |
|
145 by (simp add: gcd.simps) |
|
146 |
|
147 |
|
148 |
|
149 text {* |
|
150 Examples of 'OF' |
|
151 |
|
152 @{thm[display] relprime_dvd_mult} |
|
153 \rulename{relprime_dvd_mult} |
|
154 |
|
155 @{thm[display] relprime_dvd_mult [OF relprime_20_81]} |
|
156 |
|
157 @{thm[display] dvd_refl} |
|
158 \rulename{dvd_refl} |
|
159 |
|
160 @{thm[display] dvd_add} |
|
161 \rulename{dvd_add} |
|
162 |
|
163 @{thm[display] dvd_add [OF dvd_refl dvd_refl]} |
|
164 |
|
165 @{thm[display] dvd_add [OF _ dvd_refl]} |
|
166 *}; |
|
167 |
|
168 lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)"; |
|
169 apply (subgoal_tac "z = #34 \<or> z = #36") |
|
170 apply blast |
|
171 apply (subgoal_tac "z \<noteq> #35") |
|
172 apply arith |
|
173 apply force |
|
174 done |
|
175 |
|
176 text |
|
177 {* |
|
178 proof\ (prove):\ step\ 1\isanewline |
|
179 \isanewline |
|
180 goal\ (lemma):\isanewline |
|
181 \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline |
|
182 \ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline |
|
183 \ \ \ \ \ \ \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isasymrbrakk \isanewline |
|
184 \ \ \ \ \isasymLongrightarrow \ Q\ z\isanewline |
|
185 \ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline |
|
186 \ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36 |
|
187 |
|
188 |
|
189 |
|
190 proof\ (prove):\ step\ 3\isanewline |
|
191 \isanewline |
|
192 goal\ (lemma):\isanewline |
|
193 \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline |
|
194 \ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline |
|
195 \ \ \ \ \ \ \ z\ \isasymnoteq \ \#35\isasymrbrakk \isanewline |
|
196 \ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isanewline |
|
197 \ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline |
|
198 \ \ \ \ \isasymLongrightarrow \ z\ \isasymnoteq \ \#35 |
|
199 *} |
|
200 |
|
201 |
|
202 end |