99 |
90 |
100 val diff_0_eq_0 = prove_goalw Arith.thy [diff_def] |
91 val diff_0_eq_0 = prove_goalw Arith.thy [diff_def] |
101 "n:nat ==> 0 #- n = 0" |
92 "n:nat ==> 0 #- n = 0" |
102 (fn [prem]=> |
93 (fn [prem]=> |
103 [ (rtac (prem RS nat_induct) 1), |
94 [ (rtac (prem RS nat_induct) 1), |
104 (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]); |
95 (ALLGOALS (asm_simp_tac nat_ss)) ]); |
105 |
96 |
106 (*Must simplify BEFORE the induction!! (Else we get a critical pair) |
97 (*Must simplify BEFORE the induction!! (Else we get a critical pair) |
107 succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *) |
98 succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *) |
108 val diff_succ_succ = prove_goalw Arith.thy [diff_def] |
99 val diff_succ_succ = prove_goalw Arith.thy [diff_def] |
109 "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n" |
100 "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n" |
110 (fn prems=> |
101 (fn prems=> |
111 [ (ASM_SIMP_TAC (nat_ss addrews prems) 1), |
102 [ (asm_simp_tac (nat_ss addsimps prems) 1), |
112 (nat_ind_tac "n" prems 1), |
103 (nat_ind_tac "n" prems 1), |
113 (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]); |
104 (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]); |
114 |
105 |
115 val prems = goal Arith.thy |
106 val prems = goal Arith.thy |
116 "[| m:nat; n:nat |] ==> m #- n : succ(m)"; |
107 "[| m:nat; n:nat |] ==> m #- n : succ(m)"; |
117 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
108 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
118 by (resolve_tac prems 1); |
109 by (resolve_tac prems 1); |
119 by (resolve_tac prems 1); |
110 by (resolve_tac prems 1); |
120 by (etac succE 3); |
111 by (etac succE 3); |
121 by (ALLGOALS |
112 by (ALLGOALS |
122 (ASM_SIMP_TAC |
113 (asm_simp_tac |
123 (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ])))); |
114 (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ])))); |
124 val diff_leq = result(); |
115 val diff_leq = result(); |
125 |
116 |
126 (*** Simplification over add, mult, diff ***) |
117 (*** Simplification over add, mult, diff ***) |
127 |
118 |
128 val arith_typechecks = [add_type, mult_type, diff_type]; |
119 val arith_typechecks = [add_type, mult_type, diff_type]; |
129 val arith_rews = [add_0, add_succ, |
120 val arith_rews = [add_0, add_succ, |
130 mult_0, mult_succ, |
121 mult_0, mult_succ, |
131 diff_0, diff_0_eq_0, diff_succ_succ]; |
122 diff_0, diff_0_eq_0, diff_succ_succ]; |
132 |
123 |
133 val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"]; |
124 val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks); |
134 |
|
135 val arith_ss = nat_ss addcongs arith_congs |
|
136 addrews (arith_rews@arith_typechecks); |
|
137 |
125 |
138 (*** Addition ***) |
126 (*** Addition ***) |
139 |
127 |
140 (*Associative law for addition*) |
128 (*Associative law for addition*) |
141 val add_assoc = prove_goal Arith.thy |
129 val add_assoc = prove_goal Arith.thy |
142 "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)" |
130 "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)" |
143 (fn prems=> |
131 (fn prems=> |
144 [ (nat_ind_tac "m" prems 1), |
132 [ (nat_ind_tac "m" prems 1), |
145 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
133 (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
146 |
134 |
147 (*The following two lemmas are used for add_commute and sometimes |
135 (*The following two lemmas are used for add_commute and sometimes |
148 elsewhere, since they are safe for rewriting.*) |
136 elsewhere, since they are safe for rewriting.*) |
149 val add_0_right = prove_goal Arith.thy |
137 val add_0_right = prove_goal Arith.thy |
150 "m:nat ==> m #+ 0 = m" |
138 "m:nat ==> m #+ 0 = m" |
151 (fn prems=> |
139 (fn prems=> |
152 [ (nat_ind_tac "m" prems 1), |
140 [ (nat_ind_tac "m" prems 1), |
153 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
141 (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
154 |
142 |
155 val add_succ_right = prove_goal Arith.thy |
143 val add_succ_right = prove_goal Arith.thy |
156 "m:nat ==> m #+ succ(n) = succ(m #+ n)" |
144 "m:nat ==> m #+ succ(n) = succ(m #+ n)" |
157 (fn prems=> |
145 (fn prems=> |
158 [ (nat_ind_tac "m" prems 1), |
146 [ (nat_ind_tac "m" prems 1), |
159 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
147 (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
160 |
148 |
161 (*Commutative law for addition*) |
149 (*Commutative law for addition*) |
162 val add_commute = prove_goal Arith.thy |
150 val add_commute = prove_goal Arith.thy |
163 "[| m:nat; n:nat |] ==> m #+ n = n #+ m" |
151 "[| m:nat; n:nat |] ==> m #+ n = n #+ m" |
164 (fn prems=> |
152 (fn prems=> |
165 [ (nat_ind_tac "n" prems 1), |
153 [ (nat_ind_tac "n" prems 1), |
166 (ALLGOALS |
154 (ALLGOALS |
167 (ASM_SIMP_TAC |
155 (asm_simp_tac |
168 (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]); |
156 (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]); |
169 |
157 |
170 (*Cancellation law on the left*) |
158 (*Cancellation law on the left*) |
171 val [knat,eqn] = goal Arith.thy |
159 val [knat,eqn] = goal Arith.thy |
172 "[| k:nat; k #+ m = k #+ n |] ==> m=n"; |
160 "[| k:nat; k #+ m = k #+ n |] ==> m=n"; |
173 by (rtac (eqn RS rev_mp) 1); |
161 by (rtac (eqn RS rev_mp) 1); |
174 by (nat_ind_tac "k" [knat] 1); |
162 by (nat_ind_tac "k" [knat] 1); |
175 by (ALLGOALS (SIMP_TAC arith_ss)); |
163 by (ALLGOALS (simp_tac arith_ss)); |
176 by (fast_tac ZF_cs 1); |
164 by (fast_tac ZF_cs 1); |
177 val add_left_cancel = result(); |
165 val add_left_cancel = result(); |
178 |
166 |
179 (*** Multiplication ***) |
167 (*** Multiplication ***) |
180 |
168 |
181 (*right annihilation in product*) |
169 (*right annihilation in product*) |
182 val mult_0_right = prove_goal Arith.thy |
170 val mult_0_right = prove_goal Arith.thy |
183 "m:nat ==> m #* 0 = 0" |
171 "m:nat ==> m #* 0 = 0" |
184 (fn prems=> |
172 (fn prems=> |
185 [ (nat_ind_tac "m" prems 1), |
173 [ (nat_ind_tac "m" prems 1), |
186 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
174 (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
187 |
175 |
188 (*right successor law for multiplication*) |
176 (*right successor law for multiplication*) |
189 val mult_succ_right = prove_goal Arith.thy |
177 val mult_succ_right = prove_goal Arith.thy |
190 "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)" |
178 "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)" |
191 (fn prems=> |
179 (fn _=> |
192 [ (nat_ind_tac "m" prems 1), |
180 [ (nat_ind_tac "m" [] 1), |
193 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))), |
181 (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))), |
194 (*The final goal requires the commutative law for addition*) |
182 (*The final goal requires the commutative law for addition*) |
195 (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]); |
183 (rtac (add_commute RS subst_context) 1), |
|
184 (REPEAT (assume_tac 1)) ]); |
196 |
185 |
197 (*Commutative law for multiplication*) |
186 (*Commutative law for multiplication*) |
198 val mult_commute = prove_goal Arith.thy |
187 val mult_commute = prove_goal Arith.thy |
199 "[| m:nat; n:nat |] ==> m #* n = n #* m" |
188 "[| m:nat; n:nat |] ==> m #* n = n #* m" |
200 (fn prems=> |
189 (fn prems=> |
201 [ (nat_ind_tac "m" prems 1), |
190 [ (nat_ind_tac "m" prems 1), |
202 (ALLGOALS (ASM_SIMP_TAC |
191 (ALLGOALS (asm_simp_tac |
203 (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]); |
192 (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]); |
204 |
193 |
205 (*addition distributes over multiplication*) |
194 (*addition distributes over multiplication*) |
206 val add_mult_distrib = prove_goal Arith.thy |
195 val add_mult_distrib = prove_goal Arith.thy |
207 "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)" |
196 "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)" |
208 (fn prems=> |
197 (fn prems=> |
209 [ (nat_ind_tac "m" prems 1), |
198 [ (nat_ind_tac "m" prems 1), |
210 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]); |
199 (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]); |
211 |
200 |
212 (*Distributive law on the left; requires an extra typing premise*) |
201 (*Distributive law on the left; requires an extra typing premise*) |
213 val add_mult_distrib_left = prove_goal Arith.thy |
202 val add_mult_distrib_left = prove_goal Arith.thy |
214 "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" |
203 "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" |
215 (fn prems=> |
204 (fn prems=> |
216 let val mult_commute' = read_instantiate [("m","k")] mult_commute |
205 let val mult_commute' = read_instantiate [("m","k")] mult_commute |
217 val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems) |
206 val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems) |
218 in [ (SIMP_TAC ss 1) ] |
207 in [ (simp_tac ss 1) ] |
219 end); |
208 end); |
220 |
209 |
221 (*Associative law for multiplication*) |
210 (*Associative law for multiplication*) |
222 val mult_assoc = prove_goal Arith.thy |
211 val mult_assoc = prove_goal Arith.thy |
223 "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)" |
212 "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)" |
224 (fn prems=> |
213 (fn prems=> |
225 [ (nat_ind_tac "m" prems 1), |
214 [ (nat_ind_tac "m" prems 1), |
226 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]); |
215 (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]); |
227 |
216 |
228 |
217 |
229 (*** Difference ***) |
218 (*** Difference ***) |
230 |
219 |
231 val diff_self_eq_0 = prove_goal Arith.thy |
220 val diff_self_eq_0 = prove_goal Arith.thy |
232 "m:nat ==> m #- m = 0" |
221 "m:nat ==> m #- m = 0" |
233 (fn prems=> |
222 (fn prems=> |
234 [ (nat_ind_tac "m" prems 1), |
223 [ (nat_ind_tac "m" prems 1), |
235 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
224 (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
236 |
225 |
237 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) |
226 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) |
238 val notless::prems = goal Arith.thy |
227 val notless::prems = goal Arith.thy |
239 "[| ~m:n; m:nat; n:nat |] ==> n #+ (m#-n) = m"; |
228 "[| ~m:n; m:nat; n:nat |] ==> n #+ (m#-n) = m"; |
240 by (rtac (notless RS rev_mp) 1); |
229 by (rtac (notless RS rev_mp) 1); |
241 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
230 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
242 by (resolve_tac prems 1); |
231 by (resolve_tac prems 1); |
243 by (resolve_tac prems 1); |
232 by (resolve_tac prems 1); |
244 by (ALLGOALS (ASM_SIMP_TAC |
233 by (ALLGOALS (asm_simp_tac |
245 (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ, |
234 (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, |
246 naturals_are_ordinals])))); |
235 naturals_are_ordinals])))); |
247 val add_diff_inverse = result(); |
236 val add_diff_inverse = result(); |
248 |
237 |
249 |
238 |
250 (*Subtraction is the inverse of addition. *) |
239 (*Subtraction is the inverse of addition. *) |
251 val [mnat,nnat] = goal Arith.thy |
240 val [mnat,nnat] = goal Arith.thy |
252 "[| m:nat; n:nat |] ==> (n#+m) #-n = m"; |
241 "[| m:nat; n:nat |] ==> (n#+m) #-n = m"; |
253 by (rtac (nnat RS nat_induct) 1); |
242 by (rtac (nnat RS nat_induct) 1); |
254 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat]))); |
243 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); |
255 val diff_add_inverse = result(); |
244 val diff_add_inverse = result(); |
256 |
245 |
257 val [mnat,nnat] = goal Arith.thy |
246 val [mnat,nnat] = goal Arith.thy |
258 "[| m:nat; n:nat |] ==> n #- (n#+m) = 0"; |
247 "[| m:nat; n:nat |] ==> n #- (n#+m) = 0"; |
259 by (rtac (nnat RS nat_induct) 1); |
248 by (rtac (nnat RS nat_induct) 1); |
260 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat]))); |
249 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); |
261 val diff_add_0 = result(); |
250 val diff_add_0 = result(); |
262 |
251 |
263 |
252 |
264 (*** Remainder ***) |
253 (*** Remainder ***) |
265 |
254 |
266 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
255 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
267 val prems = goal Arith.thy |
256 goal Arith.thy "!!m n. [| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m"; |
268 "[| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m"; |
|
269 by (cut_facts_tac prems 1); |
|
270 by (etac rev_mp 1); |
257 by (etac rev_mp 1); |
271 by (etac rev_mp 1); |
258 by (etac rev_mp 1); |
272 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
259 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
273 by (resolve_tac prems 1); |
260 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ]))); |
274 by (resolve_tac prems 1); |
|
275 by (ALLGOALS (ASM_SIMP_TAC |
|
276 (nat_ss addrews (prems@[diff_leq,diff_succ_succ])))); |
|
277 val div_termination = result(); |
261 val div_termination = result(); |
278 |
262 |
279 val div_rls = |
263 val div_rls = |
280 [Ord_transrec_type, apply_type, div_termination, if_type] @ |
264 [Ord_transrec_type, apply_type, div_termination, if_type] @ |
281 nat_typechecks; |
265 nat_typechecks; |
308 val div_type = result(); |
292 val div_type = result(); |
309 |
293 |
310 val prems = goal Arith.thy |
294 val prems = goal Arith.thy |
311 "[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0"; |
295 "[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0"; |
312 by (rtac (div_def RS def_transrec RS trans) 1); |
296 by (rtac (div_def RS def_transrec RS trans) 1); |
313 by (SIMP_TAC (div_ss addrews prems) 1); |
297 by (simp_tac (div_ss addsimps prems) 1); |
314 val div_less = result(); |
298 val div_less = result(); |
315 |
299 |
316 val prems = goal Arith.thy |
300 val prems = goal Arith.thy |
317 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)"; |
301 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)"; |
318 by (rtac (div_def RS def_transrec RS trans) 1); |
302 by (rtac (div_def RS def_transrec RS trans) 1); |
319 by (SIMP_TAC (div_ss addrews prems) 1); |
303 by (simp_tac (div_ss addsimps prems) 1); |
320 val div_geq = result(); |
304 val div_geq = result(); |
321 |
305 |
322 (*Main Result.*) |
306 (*Main Result.*) |
323 val prems = goal Arith.thy |
307 val prems = goal Arith.thy |
324 "[| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; |
308 "[| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; |
325 by (res_inst_tac [("i","m")] complete_induct 1); |
309 by (res_inst_tac [("i","m")] complete_induct 1); |
326 by (resolve_tac prems 1); |
310 by (resolve_tac prems 1); |
327 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1); |
311 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1); |
328 by (ALLGOALS |
312 by (ALLGOALS |
329 (ASM_SIMP_TAC |
313 (asm_simp_tac |
330 (arith_ss addrews ([mod_type,div_type] @ prems @ |
314 (arith_ss addsimps ([mod_type,div_type] @ prems @ |
331 [mod_less,mod_geq, div_less, div_geq, |
315 [mod_less,mod_geq, div_less, div_geq, |
332 add_assoc, add_diff_inverse, div_termination])))); |
316 add_assoc, add_diff_inverse, div_termination])))); |
333 val mod_div_equality = result(); |
317 val mod_div_equality = result(); |
334 |
318 |
335 |
319 |
336 (**** Additional theorems about "less than" ****) |
320 (**** Additional theorems about "less than" ****) |
337 |
321 |
338 val [mnat,nnat] = goal Arith.thy |
322 val [mnat,nnat] = goal Arith.thy |
339 "[| m:nat; n:nat |] ==> ~ (m #+ n) : n"; |
323 "[| m:nat; n:nat |] ==> ~ (m #+ n) : n"; |
340 by (rtac (mnat RS nat_induct) 1); |
324 by (rtac (mnat RS nat_induct) 1); |
341 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl]))); |
325 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl]))); |
342 by (rtac notI 1); |
326 by (rtac notI 1); |
343 by (etac notE 1); |
327 by (etac notE 1); |
344 by (etac (succI1 RS Ord_trans) 1); |
328 by (etac (succI1 RS Ord_trans) 1); |
345 by (rtac (nnat RS naturals_are_ordinals) 1); |
329 by (rtac (nnat RS naturals_are_ordinals) 1); |
346 val add_not_less_self = result(); |
330 val add_not_less_self = result(); |