author | paulson |
Tue, 26 Mar 1996 11:42:36 +0100 | |
changeset 1609 | 5324067d993f |
parent 1461 | 6bcb44e4d6e5 |
child 1623 | 2b8573c1b1c1 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/arith.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
1609 | 6 |
Arithmetic operators and their definitions |
0 | 7 |
|
8 |
Proofs about elementary arithmetic: addition, multiplication, etc. |
|
9 |
||
10 |
Could prove def_rec_0, def_rec_succ... |
|
11 |
*) |
|
12 |
||
13 |
open Arith; |
|
14 |
||
15 |
(*"Difference" is subtraction of natural numbers. |
|
16 |
There are no negative numbers; we have |
|
17 |
m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. |
|
18 |
Also, rec(m, 0, %z w.z) is pred(m). |
|
19 |
*) |
|
20 |
||
21 |
(** rec -- better than nat_rec; the succ case has no type requirement! **) |
|
22 |
||
23 |
val rec_trans = rec_def RS def_transrec RS trans; |
|
24 |
||
25 |
goal Arith.thy "rec(0,a,b) = a"; |
|
26 |
by (rtac rec_trans 1); |
|
27 |
by (rtac nat_case_0 1); |
|
760 | 28 |
qed "rec_0"; |
0 | 29 |
|
30 |
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))"; |
|
31 |
by (rtac rec_trans 1); |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
32 |
by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1); |
760 | 33 |
qed "rec_succ"; |
0 | 34 |
|
35 |
val major::prems = goal Arith.thy |
|
36 |
"[| n: nat; \ |
|
37 |
\ a: C(0); \ |
|
38 |
\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \ |
|
39 |
\ |] ==> rec(n,a,b) : C(n)"; |
|
40 |
by (rtac (major RS nat_induct) 1); |
|
41 |
by (ALLGOALS |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
42 |
(asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ])))); |
760 | 43 |
qed "rec_type"; |
0 | 44 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
45 |
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]; |
0 | 46 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
47 |
val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff, |
1461 | 48 |
nat_le_refl]; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
49 |
|
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
50 |
val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks); |
0 | 51 |
|
52 |
||
53 |
(** Addition **) |
|
54 |
||
760 | 55 |
qed_goalw "add_type" Arith.thy [add_def] |
0 | 56 |
"[| m:nat; n:nat |] ==> m #+ n : nat" |
57 |
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); |
|
58 |
||
760 | 59 |
qed_goalw "add_0" Arith.thy [add_def] |
0 | 60 |
"0 #+ n = n" |
61 |
(fn _ => [ (rtac rec_0 1) ]); |
|
62 |
||
760 | 63 |
qed_goalw "add_succ" Arith.thy [add_def] |
0 | 64 |
"succ(m) #+ n = succ(m #+ n)" |
65 |
(fn _=> [ (rtac rec_succ 1) ]); |
|
66 |
||
67 |
(** Multiplication **) |
|
68 |
||
760 | 69 |
qed_goalw "mult_type" Arith.thy [mult_def] |
0 | 70 |
"[| m:nat; n:nat |] ==> m #* n : nat" |
71 |
(fn prems=> |
|
72 |
[ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]); |
|
73 |
||
760 | 74 |
qed_goalw "mult_0" Arith.thy [mult_def] |
0 | 75 |
"0 #* n = 0" |
76 |
(fn _ => [ (rtac rec_0 1) ]); |
|
77 |
||
760 | 78 |
qed_goalw "mult_succ" Arith.thy [mult_def] |
0 | 79 |
"succ(m) #* n = n #+ (m #* n)" |
80 |
(fn _ => [ (rtac rec_succ 1) ]); |
|
81 |
||
82 |
(** Difference **) |
|
83 |
||
760 | 84 |
qed_goalw "diff_type" Arith.thy [diff_def] |
0 | 85 |
"[| m:nat; n:nat |] ==> m #- n : nat" |
86 |
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); |
|
87 |
||
760 | 88 |
qed_goalw "diff_0" Arith.thy [diff_def] |
0 | 89 |
"m #- 0 = m" |
90 |
(fn _ => [ (rtac rec_0 1) ]); |
|
91 |
||
760 | 92 |
qed_goalw "diff_0_eq_0" Arith.thy [diff_def] |
0 | 93 |
"n:nat ==> 0 #- n = 0" |
94 |
(fn [prem]=> |
|
95 |
[ (rtac (prem RS nat_induct) 1), |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
96 |
(ALLGOALS (asm_simp_tac nat_ss)) ]); |
0 | 97 |
|
98 |
(*Must simplify BEFORE the induction!! (Else we get a critical pair) |
|
99 |
succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *) |
|
760 | 100 |
qed_goalw "diff_succ_succ" Arith.thy [diff_def] |
0 | 101 |
"[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n" |
102 |
(fn prems=> |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
103 |
[ (asm_simp_tac (nat_ss addsimps prems) 1), |
0 | 104 |
(nat_ind_tac "n" prems 1), |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
105 |
(ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]); |
0 | 106 |
|
107 |
val prems = goal Arith.thy |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
108 |
"[| m:nat; n:nat |] ==> m #- n le m"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
109 |
by (rtac (prems MRS diff_induct) 1); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
110 |
by (etac leE 3); |
0 | 111 |
by (ALLGOALS |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
112 |
(asm_simp_tac |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
113 |
(nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, |
1461 | 114 |
diff_succ_succ, nat_into_Ord])))); |
760 | 115 |
qed "diff_le_self"; |
0 | 116 |
|
117 |
(*** Simplification over add, mult, diff ***) |
|
118 |
||
119 |
val arith_typechecks = [add_type, mult_type, diff_type]; |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
120 |
val arith_simps = [add_0, add_succ, |
1461 | 121 |
mult_0, mult_succ, |
122 |
diff_0, diff_0_eq_0, diff_succ_succ]; |
|
0 | 123 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
124 |
val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks); |
0 | 125 |
|
126 |
(*** Addition ***) |
|
127 |
||
128 |
(*Associative law for addition*) |
|
760 | 129 |
qed_goal "add_assoc" Arith.thy |
0 | 130 |
"m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)" |
131 |
(fn prems=> |
|
132 |
[ (nat_ind_tac "m" prems 1), |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
133 |
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
0 | 134 |
|
135 |
(*The following two lemmas are used for add_commute and sometimes |
|
136 |
elsewhere, since they are safe for rewriting.*) |
|
760 | 137 |
qed_goal "add_0_right" Arith.thy |
0 | 138 |
"m:nat ==> m #+ 0 = m" |
139 |
(fn prems=> |
|
140 |
[ (nat_ind_tac "m" prems 1), |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
141 |
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
0 | 142 |
|
760 | 143 |
qed_goal "add_succ_right" Arith.thy |
0 | 144 |
"m:nat ==> m #+ succ(n) = succ(m #+ n)" |
145 |
(fn prems=> |
|
146 |
[ (nat_ind_tac "m" prems 1), |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
147 |
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
0 | 148 |
|
149 |
(*Commutative law for addition*) |
|
760 | 150 |
qed_goal "add_commute" Arith.thy |
435 | 151 |
"!!m n. [| m:nat; n:nat |] ==> m #+ n = n #+ m" |
152 |
(fn _ => |
|
153 |
[ (nat_ind_tac "n" [] 1), |
|
0 | 154 |
(ALLGOALS |
435 | 155 |
(asm_simp_tac (arith_ss addsimps [add_0_right, add_succ_right]))) ]); |
156 |
||
437 | 157 |
(*for a/c rewriting*) |
760 | 158 |
qed_goal "add_left_commute" Arith.thy |
437 | 159 |
"!!m n k. [| m:nat; n:nat |] ==> m#+(n#+k)=n#+(m#+k)" |
160 |
(fn _ => [asm_simp_tac (ZF_ss addsimps [add_assoc RS sym, add_commute]) 1]); |
|
435 | 161 |
|
162 |
(*Addition is an AC-operator*) |
|
163 |
val add_ac = [add_assoc, add_commute, add_left_commute]; |
|
0 | 164 |
|
165 |
(*Cancellation law on the left*) |
|
437 | 166 |
val [eqn,knat] = goal Arith.thy |
167 |
"[| k #+ m = k #+ n; k:nat |] ==> m=n"; |
|
0 | 168 |
by (rtac (eqn RS rev_mp) 1); |
169 |
by (nat_ind_tac "k" [knat] 1); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
170 |
by (ALLGOALS (simp_tac arith_ss)); |
760 | 171 |
qed "add_left_cancel"; |
0 | 172 |
|
173 |
(*** Multiplication ***) |
|
174 |
||
175 |
(*right annihilation in product*) |
|
760 | 176 |
qed_goal "mult_0_right" Arith.thy |
435 | 177 |
"!!m. m:nat ==> m #* 0 = 0" |
178 |
(fn _=> |
|
179 |
[ (nat_ind_tac "m" [] 1), |
|
180 |
(ALLGOALS (asm_simp_tac arith_ss)) ]); |
|
0 | 181 |
|
182 |
(*right successor law for multiplication*) |
|
760 | 183 |
qed_goal "mult_succ_right" Arith.thy |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
184 |
"!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)" |
435 | 185 |
(fn _ => |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
186 |
[ (nat_ind_tac "m" [] 1), |
435 | 187 |
(ALLGOALS (asm_simp_tac (arith_ss addsimps add_ac))) ]); |
0 | 188 |
|
189 |
(*Commutative law for multiplication*) |
|
760 | 190 |
qed_goal "mult_commute" Arith.thy |
0 | 191 |
"[| m:nat; n:nat |] ==> m #* n = n #* m" |
192 |
(fn prems=> |
|
193 |
[ (nat_ind_tac "m" prems 1), |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
194 |
(ALLGOALS (asm_simp_tac |
1461 | 195 |
(arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]); |
0 | 196 |
|
197 |
(*addition distributes over multiplication*) |
|
760 | 198 |
qed_goal "add_mult_distrib" Arith.thy |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
199 |
"!!m n. [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)" |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
200 |
(fn _=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
201 |
[ (etac nat_induct 1), |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
202 |
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]); |
0 | 203 |
|
204 |
(*Distributive law on the left; requires an extra typing premise*) |
|
760 | 205 |
qed_goal "add_mult_distrib_left" Arith.thy |
435 | 206 |
"!!m. [| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" |
0 | 207 |
(fn prems=> |
435 | 208 |
[ (nat_ind_tac "m" [] 1), |
209 |
(asm_simp_tac (arith_ss addsimps [mult_0_right]) 1), |
|
210 |
(asm_simp_tac (arith_ss addsimps ([mult_succ_right] @ add_ac)) 1) ]); |
|
0 | 211 |
|
212 |
(*Associative law for multiplication*) |
|
760 | 213 |
qed_goal "mult_assoc" Arith.thy |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
214 |
"!!m n k. [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)" |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
215 |
(fn _=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
216 |
[ (etac nat_induct 1), |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
217 |
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]); |
0 | 218 |
|
437 | 219 |
(*for a/c rewriting*) |
760 | 220 |
qed_goal "mult_left_commute" Arith.thy |
437 | 221 |
"!!m n k. [| m:nat; n:nat; k:nat |] ==> m #* (n #* k) = n #* (m #* k)" |
222 |
(fn _ => [rtac (mult_commute RS trans) 1, |
|
223 |
rtac (mult_assoc RS trans) 3, |
|
1461 | 224 |
rtac (mult_commute RS subst_context) 6, |
225 |
REPEAT (ares_tac [mult_type] 1)]); |
|
437 | 226 |
|
227 |
val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; |
|
228 |
||
0 | 229 |
|
230 |
(*** Difference ***) |
|
231 |
||
760 | 232 |
qed_goal "diff_self_eq_0" Arith.thy |
0 | 233 |
"m:nat ==> m #- m = 0" |
234 |
(fn prems=> |
|
235 |
[ (nat_ind_tac "m" prems 1), |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
236 |
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); |
0 | 237 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
238 |
(*Addition is the inverse of subtraction*) |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
239 |
goal Arith.thy "!!m n. [| n le m; m:nat |] ==> n #+ (m#-n) = m"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
240 |
by (forward_tac [lt_nat_in_nat] 1); |
127 | 241 |
by (etac nat_succI 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
242 |
by (etac rev_mp 1); |
0 | 243 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
244 |
by (ALLGOALS (asm_simp_tac arith_ss)); |
760 | 245 |
qed "add_diff_inverse"; |
0 | 246 |
|
1609 | 247 |
(*Proof is IDENTICAL to that above*) |
248 |
goal Arith.thy "!!m n. [| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)"; |
|
249 |
by (forward_tac [lt_nat_in_nat] 1); |
|
250 |
by (etac nat_succI 1); |
|
251 |
by (etac rev_mp 1); |
|
252 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
253 |
by (ALLGOALS (asm_simp_tac arith_ss)); |
|
254 |
qed "diff_succ"; |
|
255 |
||
0 | 256 |
(*Subtraction is the inverse of addition. *) |
257 |
val [mnat,nnat] = goal Arith.thy |
|
437 | 258 |
"[| m:nat; n:nat |] ==> (n#+m) #- n = m"; |
0 | 259 |
by (rtac (nnat RS nat_induct) 1); |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
260 |
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); |
760 | 261 |
qed "diff_add_inverse"; |
0 | 262 |
|
437 | 263 |
goal Arith.thy |
264 |
"!!m n. [| m:nat; n:nat |] ==> (m#+n) #- n = m"; |
|
265 |
by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1); |
|
266 |
by (REPEAT (ares_tac [diff_add_inverse] 1)); |
|
760 | 267 |
qed "diff_add_inverse2"; |
437 | 268 |
|
0 | 269 |
val [mnat,nnat] = goal Arith.thy |
270 |
"[| m:nat; n:nat |] ==> n #- (n#+m) = 0"; |
|
271 |
by (rtac (nnat RS nat_induct) 1); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
272 |
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); |
760 | 273 |
qed "diff_add_0"; |
0 | 274 |
|
275 |
(*** Remainder ***) |
|
276 |
||
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
277 |
goal Arith.thy "!!m n. [| 0<n; n le m; m:nat |] ==> m #- n < m"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
278 |
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
0 | 279 |
by (etac rev_mp 1); |
280 |
by (etac rev_mp 1); |
|
281 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
282 |
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ]))); |
760 | 283 |
qed "div_termination"; |
0 | 284 |
|
1461 | 285 |
val div_rls = (*for mod and div*) |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
286 |
nat_typechecks @ |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
287 |
[Ord_transrec_type, apply_type, div_termination RS ltD, if_type, |
435 | 288 |
nat_into_Ord, not_lt_iff_le RS iffD1]; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
289 |
|
435 | 290 |
val div_ss = ZF_ss addsimps [nat_into_Ord, div_termination RS ltD, |
1461 | 291 |
not_lt_iff_le RS iffD2]; |
0 | 292 |
|
293 |
(*Type checking depends upon termination!*) |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
294 |
goalw Arith.thy [mod_def] "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n : nat"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
295 |
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
760 | 296 |
qed "mod_type"; |
0 | 297 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
298 |
goal Arith.thy "!!m n. [| 0<n; m<n |] ==> m mod n = m"; |
0 | 299 |
by (rtac (mod_def RS def_transrec RS trans) 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
300 |
by (asm_simp_tac div_ss 1); |
760 | 301 |
qed "mod_less"; |
0 | 302 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
303 |
goal Arith.thy "!!m n. [| 0<n; n le m; m:nat |] ==> m mod n = (m#-n) mod n"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
304 |
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
0 | 305 |
by (rtac (mod_def RS def_transrec RS trans) 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
306 |
by (asm_simp_tac div_ss 1); |
760 | 307 |
qed "mod_geq"; |
0 | 308 |
|
309 |
(*** Quotient ***) |
|
310 |
||
311 |
(*Type checking depends upon termination!*) |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
312 |
goalw Arith.thy [div_def] |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
313 |
"!!m n. [| 0<n; m:nat; n:nat |] ==> m div n : nat"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
314 |
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
760 | 315 |
qed "div_type"; |
0 | 316 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
317 |
goal Arith.thy "!!m n. [| 0<n; m<n |] ==> m div n = 0"; |
0 | 318 |
by (rtac (div_def RS def_transrec RS trans) 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
319 |
by (asm_simp_tac div_ss 1); |
760 | 320 |
qed "div_less"; |
0 | 321 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
322 |
goal Arith.thy |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
323 |
"!!m n. [| 0<n; n le m; m:nat |] ==> m div n = succ((m#-n) div n)"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
324 |
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
0 | 325 |
by (rtac (div_def RS def_transrec RS trans) 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
326 |
by (asm_simp_tac div_ss 1); |
760 | 327 |
qed "div_geq"; |
0 | 328 |
|
1609 | 329 |
(*A key result*) |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
330 |
goal Arith.thy |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
331 |
"!!m n. [| 0<n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
332 |
by (etac complete_induct 1); |
437 | 333 |
by (excluded_middle_tac "x<n" 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
334 |
(*case x<n*) |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
335 |
by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
336 |
(*case n le x*) |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
337 |
by (asm_full_simp_tac |
435 | 338 |
(arith_ss addsimps [not_lt_iff_le, nat_into_Ord, |
1461 | 339 |
mod_geq, div_geq, add_assoc, |
340 |
div_termination RS ltD, add_diff_inverse]) 1); |
|
760 | 341 |
qed "mod_div_equality"; |
0 | 342 |
|
1609 | 343 |
(*** Further facts about mod (mainly for mutilated checkerboard ***) |
344 |
||
345 |
goal Arith.thy |
|
346 |
"!!m n. [| 0<n; m:nat; n:nat |] ==> \ |
|
347 |
\ succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))"; |
|
348 |
by (etac complete_induct 1); |
|
349 |
by (excluded_middle_tac "succ(x)<n" 1); |
|
350 |
(*case x<n*) |
|
351 |
by (asm_simp_tac (arith_ss addsimps [mod_less, nat_le_refl RS lt_trans, |
|
352 |
succ_neq_self]) 2); |
|
353 |
by (asm_simp_tac (arith_ss addsimps [ltD RS mem_imp_not_eq]) 2); |
|
354 |
(*case n le x*) |
|
355 |
by (asm_full_simp_tac |
|
356 |
(arith_ss addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1); |
|
357 |
be leE 1; |
|
358 |
by (asm_simp_tac (arith_ss addsimps [div_termination RS ltD, diff_succ, |
|
359 |
mod_geq]) 1); |
|
360 |
by (asm_simp_tac (arith_ss addsimps [mod_less, diff_self_eq_0]) 1); |
|
361 |
qed "mod_succ"; |
|
362 |
||
363 |
goal Arith.thy "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n < n"; |
|
364 |
by (etac complete_induct 1); |
|
365 |
by (excluded_middle_tac "x<n" 1); |
|
366 |
(*case x<n*) |
|
367 |
by (asm_simp_tac (arith_ss addsimps [mod_less]) 2); |
|
368 |
(*case n le x*) |
|
369 |
by (asm_full_simp_tac |
|
370 |
(arith_ss addsimps [not_lt_iff_le, nat_into_Ord, |
|
371 |
mod_geq, div_termination RS ltD]) 1); |
|
372 |
qed "mod_less_divisor"; |
|
373 |
||
374 |
||
375 |
goal Arith.thy |
|
376 |
"!!k b. [| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = if(b=1,0,1)"; |
|
377 |
by (subgoal_tac "k mod 2: 2" 1); |
|
378 |
by (asm_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD]) 2); |
|
379 |
by (dresolve_tac [ltD] 1); |
|
380 |
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
|
381 |
by (fast_tac ZF_cs 1); |
|
382 |
qed "mod2_cases"; |
|
383 |
||
384 |
goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2"; |
|
385 |
by (subgoal_tac "m mod 2: 2" 1); |
|
386 |
by (asm_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD]) 2); |
|
387 |
by (asm_simp_tac (arith_ss addsimps [mod_succ] setloop step_tac ZF_cs) 1); |
|
388 |
qed "mod2_succ_succ"; |
|
389 |
||
390 |
goal Arith.thy "!!m. m:nat ==> (m#+m) mod 2 = 0"; |
|
391 |
by (eresolve_tac [nat_induct] 1); |
|
392 |
by (simp_tac (arith_ss addsimps [mod_less]) 1); |
|
393 |
by (asm_simp_tac (arith_ss addsimps [mod2_succ_succ, add_succ_right]) 1); |
|
394 |
qed "mod2_add_self"; |
|
395 |
||
0 | 396 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
397 |
(**** Additional theorems about "le" ****) |
0 | 398 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
399 |
goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m le m #+ n"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
400 |
by (etac nat_induct 1); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
401 |
by (ALLGOALS (asm_simp_tac arith_ss)); |
760 | 402 |
qed "add_le_self"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
403 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
404 |
goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m le n #+ m"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
405 |
by (rtac (add_commute RS ssubst) 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
406 |
by (REPEAT (ares_tac [add_le_self] 1)); |
760 | 407 |
qed "add_le_self2"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
408 |
|
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
409 |
(** Monotonicity of addition **) |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
410 |
|
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
411 |
(*strict, in 1st argument*) |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
412 |
goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
413 |
by (forward_tac [lt_nat_in_nat] 1); |
127 | 414 |
by (assume_tac 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
415 |
by (etac succ_lt_induct 1); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
416 |
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI]))); |
760 | 417 |
qed "add_lt_mono1"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
418 |
|
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
419 |
(*strict, in both arguments*) |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
420 |
goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
421 |
by (rtac (add_lt_mono1 RS lt_trans) 1); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
422 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
423 |
by (EVERY [rtac (add_commute RS ssubst) 1, |
1461 | 424 |
rtac (add_commute RS ssubst) 3, |
425 |
rtac add_lt_mono1 5]); |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
426 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
760 | 427 |
qed "add_lt_mono"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
428 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
429 |
(*A [clumsy] way of lifting < monotonicity to le monotonicity *) |
435 | 430 |
val lt_mono::ford::prems = goal Ordinal.thy |
1461 | 431 |
"[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \ |
432 |
\ !!i. i:k ==> Ord(f(i)); \ |
|
433 |
\ i le j; j:k \ |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
434 |
\ |] ==> f(i) le f(j)"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
435 |
by (cut_facts_tac prems 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
436 |
by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1); |
760 | 437 |
qed "Ord_lt_mono_imp_le_mono"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
438 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
439 |
(*le monotonicity, 1st argument*) |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
440 |
goal Arith.thy |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
441 |
"!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
442 |
by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1); |
435 | 443 |
by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1)); |
760 | 444 |
qed "add_le_mono1"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
445 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
446 |
(* le monotonicity, BOTH arguments*) |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
447 |
goal Arith.thy |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
448 |
"!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"; |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
449 |
by (rtac (add_le_mono1 RS le_trans) 1); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
450 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
451 |
by (EVERY [rtac (add_commute RS ssubst) 1, |
1461 | 452 |
rtac (add_commute RS ssubst) 3, |
453 |
rtac add_le_mono1 5]); |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
454 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
760 | 455 |
qed "add_le_mono"; |
1609 | 456 |
|
457 |
val arith_ss0 = arith_ss |
|
458 |
and arith_ss = arith_ss addsimps [add_0_right, add_succ_right, |
|
459 |
mult_0_right, mult_succ_right, |
|
460 |
mod_less, mod_geq, div_less, div_geq]; |