128 |
128 |
129 (*Note: rec(a, 0, %z w.z) is pred(a). *) |
129 (*Note: rec(a, 0, %z w.z) is pred(a). *) |
130 |
130 |
131 lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N" |
131 lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N" |
132 apply (unfold arith_defs) |
132 apply (unfold arith_defs) |
133 apply (tactic {* NE_tac "b" 1 *}) |
133 apply (tactic {* NE_tac @{context} "b" 1 *}) |
134 apply (tactic "hyp_rew_tac []") |
134 apply (tactic "hyp_rew_tac []") |
135 done |
135 done |
136 |
136 |
137 |
137 |
138 (*Essential to simplify FIRST!! (Else we get a critical pair) |
138 (*Essential to simplify FIRST!! (Else we get a critical pair) |
139 succ(a) - succ(b) rewrites to pred(succ(a) - b) *) |
139 succ(a) - succ(b) rewrites to pred(succ(a) - b) *) |
140 lemma diff_succ_succ: "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N" |
140 lemma diff_succ_succ: "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N" |
141 apply (unfold arith_defs) |
141 apply (unfold arith_defs) |
142 apply (tactic "hyp_rew_tac []") |
142 apply (tactic "hyp_rew_tac []") |
143 apply (tactic {* NE_tac "b" 1 *}) |
143 apply (tactic {* NE_tac @{context} "b" 1 *}) |
144 apply (tactic "hyp_rew_tac []") |
144 apply (tactic "hyp_rew_tac []") |
145 done |
145 done |
146 |
146 |
147 |
147 |
148 subsection {* Simplification *} |
148 subsection {* Simplification *} |
186 |
186 |
187 subsection {* Addition *} |
187 subsection {* Addition *} |
188 |
188 |
189 (*Associative law for addition*) |
189 (*Associative law for addition*) |
190 lemma add_assoc: "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N" |
190 lemma add_assoc: "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N" |
191 apply (tactic {* NE_tac "a" 1 *}) |
191 apply (tactic {* NE_tac @{context} "a" 1 *}) |
192 apply (tactic "hyp_arith_rew_tac []") |
192 apply (tactic "hyp_arith_rew_tac []") |
193 done |
193 done |
194 |
194 |
195 |
195 |
196 (*Commutative law for addition. Can be proved using three inductions. |
196 (*Commutative law for addition. Can be proved using three inductions. |
197 Must simplify after first induction! Orientation of rewrites is delicate*) |
197 Must simplify after first induction! Orientation of rewrites is delicate*) |
198 lemma add_commute: "[| a:N; b:N |] ==> a #+ b = b #+ a : N" |
198 lemma add_commute: "[| a:N; b:N |] ==> a #+ b = b #+ a : N" |
199 apply (tactic {* NE_tac "a" 1 *}) |
199 apply (tactic {* NE_tac @{context} "a" 1 *}) |
200 apply (tactic "hyp_arith_rew_tac []") |
200 apply (tactic "hyp_arith_rew_tac []") |
201 apply (tactic {* NE_tac "b" 2 *}) |
201 apply (tactic {* NE_tac @{context} "b" 2 *}) |
202 apply (rule sym_elem) |
202 apply (rule sym_elem) |
203 apply (tactic {* NE_tac "b" 1 *}) |
203 apply (tactic {* NE_tac @{context} "b" 1 *}) |
204 apply (tactic "hyp_arith_rew_tac []") |
204 apply (tactic "hyp_arith_rew_tac []") |
205 done |
205 done |
206 |
206 |
207 |
207 |
208 subsection {* Multiplication *} |
208 subsection {* Multiplication *} |
209 |
209 |
210 (*right annihilation in product*) |
210 (*right annihilation in product*) |
211 lemma mult_0_right: "a:N ==> a #* 0 = 0 : N" |
211 lemma mult_0_right: "a:N ==> a #* 0 = 0 : N" |
212 apply (tactic {* NE_tac "a" 1 *}) |
212 apply (tactic {* NE_tac @{context} "a" 1 *}) |
213 apply (tactic "hyp_arith_rew_tac []") |
213 apply (tactic "hyp_arith_rew_tac []") |
214 done |
214 done |
215 |
215 |
216 (*right successor law for multiplication*) |
216 (*right successor law for multiplication*) |
217 lemma mult_succ_right: "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N" |
217 lemma mult_succ_right: "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N" |
218 apply (tactic {* NE_tac "a" 1 *}) |
218 apply (tactic {* NE_tac @{context} "a" 1 *}) |
219 apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *}) |
219 apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *}) |
220 apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ |
220 apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ |
221 done |
221 done |
222 |
222 |
223 (*Commutative law for multiplication*) |
223 (*Commutative law for multiplication*) |
224 lemma mult_commute: "[| a:N; b:N |] ==> a #* b = b #* a : N" |
224 lemma mult_commute: "[| a:N; b:N |] ==> a #* b = b #* a : N" |
225 apply (tactic {* NE_tac "a" 1 *}) |
225 apply (tactic {* NE_tac @{context} "a" 1 *}) |
226 apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *}) |
226 apply (tactic {* hyp_arith_rew_tac [@{thm mult_0_right}, @{thm mult_succ_right}] *}) |
227 done |
227 done |
228 |
228 |
229 (*addition distributes over multiplication*) |
229 (*addition distributes over multiplication*) |
230 lemma add_mult_distrib: "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" |
230 lemma add_mult_distrib: "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" |
231 apply (tactic {* NE_tac "a" 1 *}) |
231 apply (tactic {* NE_tac @{context} "a" 1 *}) |
232 apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *}) |
232 apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *}) |
233 done |
233 done |
234 |
234 |
235 (*Associative law for multiplication*) |
235 (*Associative law for multiplication*) |
236 lemma mult_assoc: "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N" |
236 lemma mult_assoc: "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N" |
237 apply (tactic {* NE_tac "a" 1 *}) |
237 apply (tactic {* NE_tac @{context} "a" 1 *}) |
238 apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *}) |
238 apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *}) |
239 done |
239 done |
240 |
240 |
241 |
241 |
242 subsection {* Difference *} |
242 subsection {* Difference *} |
243 |
243 |
244 text {* |
244 text {* |
245 Difference on natural numbers, without negative numbers |
245 Difference on natural numbers, without negative numbers |
246 a - b = 0 iff a<=b a - b = succ(c) iff a>b *} |
246 a - b = 0 iff a<=b a - b = succ(c) iff a>b *} |
247 |
247 |
248 lemma diff_self_eq_0: "a:N ==> a - a = 0 : N" |
248 lemma diff_self_eq_0: "a:N ==> a - a = 0 : N" |
249 apply (tactic {* NE_tac "a" 1 *}) |
249 apply (tactic {* NE_tac @{context} "a" 1 *}) |
250 apply (tactic "hyp_arith_rew_tac []") |
250 apply (tactic "hyp_arith_rew_tac []") |
251 done |
251 done |
252 |
252 |
253 |
253 |
254 lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N" |
254 lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N" |
256 |
256 |
257 (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x. |
257 (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x. |
258 An example of induction over a quantified formula (a product). |
258 An example of induction over a quantified formula (a product). |
259 Uses rewriting with a quantified, implicative inductive hypothesis.*) |
259 Uses rewriting with a quantified, implicative inductive hypothesis.*) |
260 lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)" |
260 lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)" |
261 apply (tactic {* NE_tac "b" 1 *}) |
261 apply (tactic {* NE_tac @{context} "b" 1 *}) |
262 (*strip one "universal quantifier" but not the "implication"*) |
262 (*strip one "universal quantifier" but not the "implication"*) |
263 apply (rule_tac [3] intr_rls) |
263 apply (rule_tac [3] intr_rls) |
264 (*case analysis on x in |
264 (*case analysis on x in |
265 (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *) |
265 (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *) |
266 apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4") |
266 apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac 4") |
267 (*Prepare for simplification of types -- the antecedent succ(u)<=x *) |
267 (*Prepare for simplification of types -- the antecedent succ(u)<=x *) |
268 apply (rule_tac [5] replace_type) |
268 apply (rule_tac [5] replace_type) |
269 apply (rule_tac [4] replace_type) |
269 apply (rule_tac [4] replace_type) |
270 apply (tactic "arith_rew_tac []") |
270 apply (tactic "arith_rew_tac []") |
271 (*Solves first 0 goal, simplifies others. Two sugbgoals remain. |
271 (*Solves first 0 goal, simplifies others. Two sugbgoals remain. |
324 apply (tactic {* typechk_tac [thm "diff_typing"] *}) |
324 apply (tactic {* typechk_tac [thm "diff_typing"] *}) |
325 done |
325 done |
326 |
326 |
327 (*If a+b=0 then a=0. Surprisingly tedious*) |
327 (*If a+b=0 then a=0. Surprisingly tedious*) |
328 lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" |
328 lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" |
329 apply (tactic {* NE_tac "a" 1 *}) |
329 apply (tactic {* NE_tac @{context} "a" 1 *}) |
330 apply (rule_tac [3] replace_type) |
330 apply (rule_tac [3] replace_type) |
331 apply (tactic "arith_rew_tac []") |
331 apply (tactic "arith_rew_tac []") |
332 apply (tactic "intr_tac []") (*strips remaining PRODs*) |
332 apply (tactic "intr_tac []") (*strips remaining PRODs*) |
333 apply (rule_tac [2] zero_ne_succ [THEN FE]) |
333 apply (rule_tac [2] zero_ne_succ [THEN FE]) |
334 apply (erule_tac [3] EqE [THEN sym_elem]) |
334 apply (erule_tac [3] EqE [THEN sym_elem]) |
432 (*Version of above with same condition as the mod one*) |
432 (*Version of above with same condition as the mod one*) |
433 lemma divC_succ2: "[| a:N; b:N |] ==> |
433 lemma divC_succ2: "[| a:N; b:N |] ==> |
434 succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N" |
434 succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N" |
435 apply (rule divC_succ [THEN trans_elem]) |
435 apply (rule divC_succ [THEN trans_elem]) |
436 apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *}) |
436 apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *}) |
437 apply (tactic {* NE_tac "succ (a mod b) |-|b" 1 *}) |
437 apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *}) |
438 apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *}) |
438 apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *}) |
439 done |
439 done |
440 |
440 |
441 (*for case analysis on whether a number is 0 or a successor*) |
441 (*for case analysis on whether a number is 0 or a successor*) |
442 lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : |
442 lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : |
443 Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))" |
443 Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))" |
444 apply (tactic {* NE_tac "a" 1 *}) |
444 apply (tactic {* NE_tac @{context} "a" 1 *}) |
445 apply (rule_tac [3] PlusI_inr) |
445 apply (rule_tac [3] PlusI_inr) |
446 apply (rule_tac [2] PlusI_inl) |
446 apply (rule_tac [2] PlusI_inl) |
447 apply (tactic eqintr_tac) |
447 apply (tactic eqintr_tac) |
448 apply (tactic "equal_tac []") |
448 apply (tactic "equal_tac []") |
449 done |
449 done |
450 |
450 |
451 (*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) |
451 (*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) |
452 lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N" |
452 lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N" |
453 apply (tactic {* NE_tac "a" 1 *}) |
453 apply (tactic {* NE_tac @{context} "a" 1 *}) |
454 apply (tactic {* arith_rew_tac (thms "div_typing_rls" @ |
454 apply (tactic {* arith_rew_tac (thms "div_typing_rls" @ |
455 [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *}) |
455 [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *}) |
456 apply (rule EqE) |
456 apply (rule EqE) |
457 (*case analysis on succ(u mod b)|-|b *) |
457 (*case analysis on succ(u mod b)|-|b *) |
458 apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE]) |
458 apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE]) |