author | wenzelm |
Tue, 24 Nov 1998 12:03:09 +0100 | |
changeset 5953 | d6017ce6b93e |
parent 5529 | 4a54acae6a15 |
child 6068 | 2d8f3e1f1151 |
permissions | -rw-r--r-- |
1793 | 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 |
||
5067 | 25 |
Goal "rec(0,a,b) = a"; |
0 | 26 |
by (rtac rec_trans 1); |
27 |
by (rtac nat_case_0 1); |
|
760 | 28 |
qed "rec_0"; |
0 | 29 |
|
5067 | 30 |
Goal "rec(succ(m),a,b) = b(m, rec(m,a,b))"; |
0 | 31 |
by (rtac rec_trans 1); |
2469 | 32 |
by (Simp_tac 1); |
760 | 33 |
qed "rec_succ"; |
0 | 34 |
|
2469 | 35 |
Addsimps [rec_0, rec_succ]; |
36 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5147
diff
changeset
|
37 |
val major::prems = Goal |
0 | 38 |
"[| n: nat; \ |
39 |
\ a: C(0); \ |
|
40 |
\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \ |
|
41 |
\ |] ==> rec(n,a,b) : C(n)"; |
|
42 |
by (rtac (major RS nat_induct) 1); |
|
43 |
by (ALLGOALS |
|
4091 | 44 |
(asm_simp_tac (simpset() addsimps prems))); |
760 | 45 |
qed "rec_type"; |
0 | 46 |
|
2469 | 47 |
Addsimps [rec_type, nat_0_le, nat_le_refl]; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
48 |
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]; |
0 | 49 |
|
5137 | 50 |
Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)"; |
1708 | 51 |
by (etac rev_mp 1); |
52 |
by (etac nat_induct 1); |
|
2469 | 53 |
by (Simp_tac 1); |
3016 | 54 |
by (Blast_tac 1); |
1708 | 55 |
val lemma = result(); |
56 |
||
57 |
(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *) |
|
58 |
bind_thm ("zero_lt_natE", lemma RS bexE); |
|
59 |
||
60 |
||
0 | 61 |
(** Addition **) |
62 |
||
760 | 63 |
qed_goalw "add_type" Arith.thy [add_def] |
0 | 64 |
"[| m:nat; n:nat |] ==> m #+ n : nat" |
65 |
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); |
|
66 |
||
760 | 67 |
qed_goalw "add_0" Arith.thy [add_def] |
0 | 68 |
"0 #+ n = n" |
69 |
(fn _ => [ (rtac rec_0 1) ]); |
|
70 |
||
760 | 71 |
qed_goalw "add_succ" Arith.thy [add_def] |
0 | 72 |
"succ(m) #+ n = succ(m #+ n)" |
73 |
(fn _=> [ (rtac rec_succ 1) ]); |
|
74 |
||
2469 | 75 |
Addsimps [add_0, add_succ]; |
76 |
||
0 | 77 |
(** Multiplication **) |
78 |
||
760 | 79 |
qed_goalw "mult_type" Arith.thy [mult_def] |
0 | 80 |
"[| m:nat; n:nat |] ==> m #* n : nat" |
81 |
(fn prems=> |
|
82 |
[ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]); |
|
83 |
||
760 | 84 |
qed_goalw "mult_0" Arith.thy [mult_def] |
0 | 85 |
"0 #* n = 0" |
86 |
(fn _ => [ (rtac rec_0 1) ]); |
|
87 |
||
760 | 88 |
qed_goalw "mult_succ" Arith.thy [mult_def] |
0 | 89 |
"succ(m) #* n = n #+ (m #* n)" |
90 |
(fn _ => [ (rtac rec_succ 1) ]); |
|
91 |
||
2469 | 92 |
Addsimps [mult_0, mult_succ]; |
93 |
||
0 | 94 |
(** Difference **) |
95 |
||
760 | 96 |
qed_goalw "diff_type" Arith.thy [diff_def] |
0 | 97 |
"[| m:nat; n:nat |] ==> m #- n : nat" |
98 |
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); |
|
99 |
||
760 | 100 |
qed_goalw "diff_0" Arith.thy [diff_def] |
0 | 101 |
"m #- 0 = m" |
102 |
(fn _ => [ (rtac rec_0 1) ]); |
|
103 |
||
760 | 104 |
qed_goalw "diff_0_eq_0" Arith.thy [diff_def] |
0 | 105 |
"n:nat ==> 0 #- n = 0" |
106 |
(fn [prem]=> |
|
107 |
[ (rtac (prem RS nat_induct) 1), |
|
2469 | 108 |
(ALLGOALS (Asm_simp_tac)) ]); |
0 | 109 |
|
110 |
(*Must simplify BEFORE the induction!! (Else we get a critical pair) |
|
111 |
succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *) |
|
760 | 112 |
qed_goalw "diff_succ_succ" Arith.thy [diff_def] |
0 | 113 |
"[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n" |
114 |
(fn prems=> |
|
4091 | 115 |
[ (asm_simp_tac (simpset() addsimps prems) 1), |
0 | 116 |
(nat_ind_tac "n" prems 1), |
4091 | 117 |
(ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); |
2469 | 118 |
|
119 |
Addsimps [diff_0, diff_0_eq_0, diff_succ_succ]; |
|
0 | 120 |
|
121 |
val prems = goal Arith.thy |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
122 |
"[| 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
|
123 |
by (rtac (prems MRS diff_induct) 1); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
124 |
by (etac leE 3); |
0 | 125 |
by (ALLGOALS |
5529 | 126 |
(asm_simp_tac (simpset() addsimps prems @ [le_iff, nat_into_Ord]))); |
760 | 127 |
qed "diff_le_self"; |
0 | 128 |
|
129 |
(*** Simplification over add, mult, diff ***) |
|
130 |
||
131 |
val arith_typechecks = [add_type, mult_type, diff_type]; |
|
2469 | 132 |
Addsimps arith_typechecks; |
0 | 133 |
|
134 |
||
135 |
(*** Addition ***) |
|
136 |
||
137 |
(*Associative law for addition*) |
|
760 | 138 |
qed_goal "add_assoc" Arith.thy |
0 | 139 |
"m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)" |
140 |
(fn prems=> |
|
141 |
[ (nat_ind_tac "m" prems 1), |
|
4091 | 142 |
(ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); |
0 | 143 |
|
144 |
(*The following two lemmas are used for add_commute and sometimes |
|
145 |
elsewhere, since they are safe for rewriting.*) |
|
760 | 146 |
qed_goal "add_0_right" Arith.thy |
0 | 147 |
"m:nat ==> m #+ 0 = m" |
148 |
(fn prems=> |
|
149 |
[ (nat_ind_tac "m" prems 1), |
|
4091 | 150 |
(ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); |
0 | 151 |
|
760 | 152 |
qed_goal "add_succ_right" Arith.thy |
0 | 153 |
"m:nat ==> m #+ succ(n) = succ(m #+ n)" |
154 |
(fn prems=> |
|
155 |
[ (nat_ind_tac "m" prems 1), |
|
4091 | 156 |
(ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); |
2469 | 157 |
|
158 |
Addsimps [add_0_right, add_succ_right]; |
|
0 | 159 |
|
160 |
(*Commutative law for addition*) |
|
760 | 161 |
qed_goal "add_commute" Arith.thy |
435 | 162 |
"!!m n. [| m:nat; n:nat |] ==> m #+ n = n #+ m" |
163 |
(fn _ => |
|
164 |
[ (nat_ind_tac "n" [] 1), |
|
2469 | 165 |
(ALLGOALS Asm_simp_tac) ]); |
435 | 166 |
|
437 | 167 |
(*for a/c rewriting*) |
760 | 168 |
qed_goal "add_left_commute" Arith.thy |
437 | 169 |
"!!m n k. [| m:nat; n:nat |] ==> m#+(n#+k)=n#+(m#+k)" |
4091 | 170 |
(fn _ => [asm_simp_tac(simpset() addsimps [add_assoc RS sym, add_commute]) 1]); |
435 | 171 |
|
172 |
(*Addition is an AC-operator*) |
|
173 |
val add_ac = [add_assoc, add_commute, add_left_commute]; |
|
0 | 174 |
|
175 |
(*Cancellation law on the left*) |
|
437 | 176 |
val [eqn,knat] = goal Arith.thy |
177 |
"[| k #+ m = k #+ n; k:nat |] ==> m=n"; |
|
0 | 178 |
by (rtac (eqn RS rev_mp) 1); |
179 |
by (nat_ind_tac "k" [knat] 1); |
|
2469 | 180 |
by (ALLGOALS (Simp_tac)); |
760 | 181 |
qed "add_left_cancel"; |
0 | 182 |
|
183 |
(*** Multiplication ***) |
|
184 |
||
185 |
(*right annihilation in product*) |
|
760 | 186 |
qed_goal "mult_0_right" Arith.thy |
435 | 187 |
"!!m. m:nat ==> m #* 0 = 0" |
188 |
(fn _=> |
|
189 |
[ (nat_ind_tac "m" [] 1), |
|
2469 | 190 |
(ALLGOALS (Asm_simp_tac)) ]); |
0 | 191 |
|
192 |
(*right successor law for multiplication*) |
|
760 | 193 |
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
|
194 |
"!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)" |
435 | 195 |
(fn _ => |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
196 |
[ (nat_ind_tac "m" [] 1), |
4091 | 197 |
(ALLGOALS (asm_simp_tac (simpset() addsimps add_ac))) ]); |
2469 | 198 |
|
199 |
Addsimps [mult_0_right, mult_succ_right]; |
|
0 | 200 |
|
5137 | 201 |
Goal "n:nat ==> 1 #* n = n"; |
2469 | 202 |
by (Asm_simp_tac 1); |
1793 | 203 |
qed "mult_1"; |
204 |
||
5137 | 205 |
Goal "n:nat ==> n #* 1 = n"; |
2469 | 206 |
by (Asm_simp_tac 1); |
1793 | 207 |
qed "mult_1_right"; |
208 |
||
0 | 209 |
(*Commutative law for multiplication*) |
760 | 210 |
qed_goal "mult_commute" Arith.thy |
2469 | 211 |
"!!m n. [| m:nat; n:nat |] ==> m #* n = n #* m" |
212 |
(fn _=> |
|
213 |
[ (nat_ind_tac "m" [] 1), |
|
214 |
(ALLGOALS Asm_simp_tac) ]); |
|
0 | 215 |
|
216 |
(*addition distributes over multiplication*) |
|
760 | 217 |
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
|
218 |
"!!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
|
219 |
(fn _=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
220 |
[ (etac nat_induct 1), |
4091 | 221 |
(ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))) ]); |
0 | 222 |
|
223 |
(*Distributive law on the left; requires an extra typing premise*) |
|
760 | 224 |
qed_goal "add_mult_distrib_left" Arith.thy |
435 | 225 |
"!!m. [| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" |
0 | 226 |
(fn prems=> |
435 | 227 |
[ (nat_ind_tac "m" [] 1), |
2469 | 228 |
(Asm_simp_tac 1), |
4091 | 229 |
(asm_simp_tac (simpset() addsimps add_ac) 1) ]); |
0 | 230 |
|
231 |
(*Associative law for multiplication*) |
|
760 | 232 |
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
|
233 |
"!!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
|
234 |
(fn _=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
235 |
[ (etac nat_induct 1), |
4091 | 236 |
(ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))) ]); |
0 | 237 |
|
437 | 238 |
(*for a/c rewriting*) |
760 | 239 |
qed_goal "mult_left_commute" Arith.thy |
437 | 240 |
"!!m n k. [| m:nat; n:nat; k:nat |] ==> m #* (n #* k) = n #* (m #* k)" |
241 |
(fn _ => [rtac (mult_commute RS trans) 1, |
|
242 |
rtac (mult_assoc RS trans) 3, |
|
1461 | 243 |
rtac (mult_commute RS subst_context) 6, |
244 |
REPEAT (ares_tac [mult_type] 1)]); |
|
437 | 245 |
|
246 |
val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; |
|
247 |
||
0 | 248 |
|
249 |
(*** Difference ***) |
|
250 |
||
760 | 251 |
qed_goal "diff_self_eq_0" Arith.thy |
0 | 252 |
"m:nat ==> m #- m = 0" |
253 |
(fn prems=> |
|
254 |
[ (nat_ind_tac "m" prems 1), |
|
4091 | 255 |
(ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); |
0 | 256 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
257 |
(*Addition is the inverse of subtraction*) |
5137 | 258 |
Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
259 |
by (forward_tac [lt_nat_in_nat] 1); |
127 | 260 |
by (etac nat_succI 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
261 |
by (etac rev_mp 1); |
0 | 262 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
2469 | 263 |
by (ALLGOALS Asm_simp_tac); |
760 | 264 |
qed "add_diff_inverse"; |
0 | 265 |
|
5504 | 266 |
Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m"; |
267 |
by (forward_tac [lt_nat_in_nat] 1); |
|
268 |
by (etac nat_succI 1); |
|
269 |
by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1); |
|
270 |
qed "add_diff_inverse2"; |
|
271 |
||
1609 | 272 |
(*Proof is IDENTICAL to that above*) |
5137 | 273 |
Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)"; |
1609 | 274 |
by (forward_tac [lt_nat_in_nat] 1); |
275 |
by (etac nat_succI 1); |
|
276 |
by (etac rev_mp 1); |
|
277 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
2469 | 278 |
by (ALLGOALS Asm_simp_tac); |
1609 | 279 |
qed "diff_succ"; |
280 |
||
5341 | 281 |
Goal "[| m: nat; n: nat |] ==> 0 < n #- m <-> m<n"; |
282 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
283 |
by (ALLGOALS Asm_simp_tac); |
|
284 |
qed "zero_less_diff"; |
|
285 |
Addsimps [zero_less_diff]; |
|
286 |
||
287 |
||
1708 | 288 |
(** Subtraction is the inverse of addition. **) |
289 |
||
0 | 290 |
val [mnat,nnat] = goal Arith.thy |
437 | 291 |
"[| m:nat; n:nat |] ==> (n#+m) #- n = m"; |
0 | 292 |
by (rtac (nnat RS nat_induct) 1); |
4091 | 293 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat]))); |
760 | 294 |
qed "diff_add_inverse"; |
0 | 295 |
|
5137 | 296 |
Goal "[| m:nat; n:nat |] ==> (m#+n) #- n = m"; |
437 | 297 |
by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1); |
298 |
by (REPEAT (ares_tac [diff_add_inverse] 1)); |
|
760 | 299 |
qed "diff_add_inverse2"; |
437 | 300 |
|
5137 | 301 |
Goal "[| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n"; |
1708 | 302 |
by (nat_ind_tac "k" [] 1); |
2469 | 303 |
by (ALLGOALS Asm_simp_tac); |
1708 | 304 |
qed "diff_cancel"; |
305 |
||
5137 | 306 |
Goal "[| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n"; |
1708 | 307 |
val add_commute_k = read_instantiate [("n","k")] add_commute; |
4091 | 308 |
by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1); |
1708 | 309 |
qed "diff_cancel2"; |
310 |
||
0 | 311 |
val [mnat,nnat] = goal Arith.thy |
312 |
"[| m:nat; n:nat |] ==> n #- (n#+m) = 0"; |
|
313 |
by (rtac (nnat RS nat_induct) 1); |
|
4091 | 314 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat]))); |
760 | 315 |
qed "diff_add_0"; |
0 | 316 |
|
1708 | 317 |
(** Difference distributes over multiplication **) |
318 |
||
5137 | 319 |
Goal "[| m:nat; n: nat; k:nat |] ==> (m #- n) #* k = (m #* k) #- (n #* k)"; |
1708 | 320 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
4091 | 321 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel]))); |
1708 | 322 |
qed "diff_mult_distrib" ; |
323 |
||
5137 | 324 |
Goal "[| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)"; |
1708 | 325 |
val mult_commute_k = read_instantiate [("m","k")] mult_commute; |
4091 | 326 |
by (asm_simp_tac (simpset() addsimps |
1793 | 327 |
[mult_commute_k, diff_mult_distrib]) 1); |
1708 | 328 |
qed "diff_mult_distrib2" ; |
329 |
||
0 | 330 |
(*** Remainder ***) |
331 |
||
5137 | 332 |
Goal "[| 0<n; n le m; m:nat |] ==> m #- n < m"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
333 |
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
0 | 334 |
by (etac rev_mp 1); |
335 |
by (etac rev_mp 1); |
|
336 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
4091 | 337 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self,diff_succ_succ]))); |
760 | 338 |
qed "div_termination"; |
0 | 339 |
|
1461 | 340 |
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
|
341 |
nat_typechecks @ |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
342 |
[Ord_transrec_type, apply_type, div_termination RS ltD, if_type, |
435 | 343 |
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
|
344 |
|
4091 | 345 |
val div_ss = (simpset()) addsimps [nat_into_Ord, div_termination RS ltD, |
2493 | 346 |
not_lt_iff_le RS iffD2]; |
0 | 347 |
|
348 |
(*Type checking depends upon termination!*) |
|
5137 | 349 |
Goalw [mod_def] "[| 0<n; m:nat; n:nat |] ==> m mod n : nat"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
350 |
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
760 | 351 |
qed "mod_type"; |
0 | 352 |
|
5137 | 353 |
Goal "[| 0<n; m<n |] ==> m mod n = m"; |
0 | 354 |
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
|
355 |
by (asm_simp_tac div_ss 1); |
760 | 356 |
qed "mod_less"; |
0 | 357 |
|
5137 | 358 |
Goal "[| 0<n; n le m; m:nat |] ==> m mod n = (m#-n) mod n"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
359 |
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
0 | 360 |
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
|
361 |
by (asm_simp_tac div_ss 1); |
760 | 362 |
qed "mod_geq"; |
0 | 363 |
|
2469 | 364 |
Addsimps [mod_type, mod_less, mod_geq]; |
365 |
||
0 | 366 |
(*** Quotient ***) |
367 |
||
368 |
(*Type checking depends upon termination!*) |
|
5067 | 369 |
Goalw [div_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
370 |
"[| 0<n; m:nat; n:nat |] ==> m div n : nat"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
371 |
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
760 | 372 |
qed "div_type"; |
0 | 373 |
|
5137 | 374 |
Goal "[| 0<n; m<n |] ==> m div n = 0"; |
0 | 375 |
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
|
376 |
by (asm_simp_tac div_ss 1); |
760 | 377 |
qed "div_less"; |
0 | 378 |
|
5137 | 379 |
Goal "[| 0<n; n le m; m:nat |] ==> m div n = succ((m#-n) div n)"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
380 |
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
0 | 381 |
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
|
382 |
by (asm_simp_tac div_ss 1); |
760 | 383 |
qed "div_geq"; |
0 | 384 |
|
2469 | 385 |
Addsimps [div_type, div_less, div_geq]; |
386 |
||
1609 | 387 |
(*A key result*) |
5137 | 388 |
Goal "[| 0<n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
389 |
by (etac complete_induct 1); |
437 | 390 |
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
|
391 |
(*case x<n*) |
2469 | 392 |
by (Asm_simp_tac 2); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
393 |
(*case n le x*) |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
394 |
by (asm_full_simp_tac |
4091 | 395 |
(simpset() addsimps [not_lt_iff_le, nat_into_Ord, add_assoc, |
1461 | 396 |
div_termination RS ltD, add_diff_inverse]) 1); |
760 | 397 |
qed "mod_div_equality"; |
0 | 398 |
|
1609 | 399 |
(*** Further facts about mod (mainly for mutilated checkerboard ***) |
400 |
||
5137 | 401 |
Goal "[| 0<n; m:nat; n:nat |] ==> \ |
1609 | 402 |
\ succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))"; |
403 |
by (etac complete_induct 1); |
|
404 |
by (excluded_middle_tac "succ(x)<n" 1); |
|
1623 | 405 |
(* case succ(x) < n *) |
4091 | 406 |
by (asm_simp_tac (simpset() addsimps [mod_less, nat_le_refl RS lt_trans, |
1623 | 407 |
succ_neq_self]) 2); |
4091 | 408 |
by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2); |
1623 | 409 |
(* case n le succ(x) *) |
1609 | 410 |
by (asm_full_simp_tac |
4091 | 411 |
(simpset() addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1); |
1623 | 412 |
by (etac leE 1); |
4091 | 413 |
by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ, |
1623 | 414 |
mod_geq]) 1); |
4091 | 415 |
by (asm_simp_tac (simpset() addsimps [mod_less, diff_self_eq_0]) 1); |
1609 | 416 |
qed "mod_succ"; |
417 |
||
5137 | 418 |
Goal "[| 0<n; m:nat; n:nat |] ==> m mod n < n"; |
1609 | 419 |
by (etac complete_induct 1); |
420 |
by (excluded_middle_tac "x<n" 1); |
|
421 |
(*case x<n*) |
|
4091 | 422 |
by (asm_simp_tac (simpset() addsimps [mod_less]) 2); |
1609 | 423 |
(*case n le x*) |
424 |
by (asm_full_simp_tac |
|
4091 | 425 |
(simpset() addsimps [not_lt_iff_le, nat_into_Ord, |
1609 | 426 |
mod_geq, div_termination RS ltD]) 1); |
427 |
qed "mod_less_divisor"; |
|
428 |
||
429 |
||
5137 | 430 |
Goal "[| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = if(b=1,0,1)"; |
1609 | 431 |
by (subgoal_tac "k mod 2: 2" 1); |
4091 | 432 |
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); |
1623 | 433 |
by (dtac ltD 1); |
5137 | 434 |
by Auto_tac; |
1609 | 435 |
qed "mod2_cases"; |
436 |
||
5137 | 437 |
Goal "m:nat ==> succ(succ(m)) mod 2 = m mod 2"; |
1609 | 438 |
by (subgoal_tac "m mod 2: 2" 1); |
4091 | 439 |
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); |
440 |
by (asm_simp_tac (simpset() addsimps [mod_succ] setloop Step_tac) 1); |
|
1609 | 441 |
qed "mod2_succ_succ"; |
442 |
||
5137 | 443 |
Goal "m:nat ==> (m#+m) mod 2 = 0"; |
1623 | 444 |
by (etac nat_induct 1); |
4091 | 445 |
by (simp_tac (simpset() addsimps [mod_less]) 1); |
446 |
by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1); |
|
1609 | 447 |
qed "mod2_add_self"; |
448 |
||
0 | 449 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
450 |
(**** Additional theorems about "le" ****) |
0 | 451 |
|
5137 | 452 |
Goal "[| m:nat; n:nat |] ==> m le m #+ n"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
453 |
by (etac nat_induct 1); |
2469 | 454 |
by (ALLGOALS Asm_simp_tac); |
760 | 455 |
qed "add_le_self"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
456 |
|
5137 | 457 |
Goal "[| m:nat; n:nat |] ==> m le n #+ m"; |
2033 | 458 |
by (stac add_commute 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
459 |
by (REPEAT (ares_tac [add_le_self] 1)); |
760 | 460 |
qed "add_le_self2"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
461 |
|
1708 | 462 |
(*** Monotonicity of Addition ***) |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
463 |
|
1708 | 464 |
(*strict, in 1st argument; proof is by rule induction on 'less than'*) |
5137 | 465 |
Goal "[| i<j; j:nat; k:nat |] ==> i#+k < j#+k"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
466 |
by (forward_tac [lt_nat_in_nat] 1); |
127 | 467 |
by (assume_tac 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
468 |
by (etac succ_lt_induct 1); |
4091 | 469 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI]))); |
760 | 470 |
qed "add_lt_mono1"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
471 |
|
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
472 |
(*strict, in both arguments*) |
5137 | 473 |
Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
474 |
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
|
475 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
2033 | 476 |
by (EVERY [stac add_commute 1, |
477 |
stac add_commute 3, |
|
1461 | 478 |
rtac add_lt_mono1 5]); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
479 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
760 | 480 |
qed "add_lt_mono"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
481 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
482 |
(*A [clumsy] way of lifting < monotonicity to le monotonicity *) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5147
diff
changeset
|
483 |
val lt_mono::ford::prems = Goal |
1461 | 484 |
"[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \ |
485 |
\ !!i. i:k ==> Ord(f(i)); \ |
|
486 |
\ i le j; j:k \ |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
487 |
\ |] ==> 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
|
488 |
by (cut_facts_tac prems 1); |
3016 | 489 |
by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1); |
760 | 490 |
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
|
491 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
492 |
(*le monotonicity, 1st argument*) |
5137 | 493 |
Goal "[| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; |
3840 | 494 |
by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1); |
435 | 495 |
by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1)); |
760 | 496 |
qed "add_le_mono1"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
497 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
498 |
(* le monotonicity, BOTH arguments*) |
5137 | 499 |
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
500 |
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
|
501 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
2033 | 502 |
by (EVERY [stac add_commute 1, |
503 |
stac add_commute 3, |
|
1461 | 504 |
rtac add_le_mono1 5]); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
505 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
760 | 506 |
qed "add_le_mono"; |
1609 | 507 |
|
1708 | 508 |
(*** Monotonicity of Multiplication ***) |
509 |
||
5137 | 510 |
Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k"; |
1708 | 511 |
by (forward_tac [lt_nat_in_nat] 1); |
512 |
by (nat_ind_tac "k" [] 2); |
|
4091 | 513 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); |
1708 | 514 |
qed "mult_le_mono1"; |
515 |
||
516 |
(* le monotonicity, BOTH arguments*) |
|
5137 | 517 |
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l"; |
1708 | 518 |
by (rtac (mult_le_mono1 RS le_trans) 1); |
519 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
|
2033 | 520 |
by (EVERY [stac mult_commute 1, |
521 |
stac mult_commute 3, |
|
1708 | 522 |
rtac mult_le_mono1 5]); |
523 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
|
524 |
qed "mult_le_mono"; |
|
525 |
||
526 |
(*strict, in 1st argument; proof is by induction on k>0*) |
|
5137 | 527 |
Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j"; |
1793 | 528 |
by (etac zero_lt_natE 1); |
1708 | 529 |
by (forward_tac [lt_nat_in_nat] 2); |
2469 | 530 |
by (ALLGOALS Asm_simp_tac); |
1708 | 531 |
by (nat_ind_tac "x" [] 1); |
4091 | 532 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono]))); |
1708 | 533 |
qed "mult_lt_mono2"; |
534 |
||
5137 | 535 |
Goal "[| i<j; 0<c; i:nat; j:nat; c:nat |] ==> i#*c < j#*c"; |
4839 | 536 |
by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1); |
537 |
qed "mult_lt_mono1"; |
|
538 |
||
5137 | 539 |
Goal "[| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n"; |
4091 | 540 |
by (best_tac (claset() addEs [natE] addss (simpset())) 1); |
1708 | 541 |
qed "zero_lt_mult_iff"; |
542 |
||
5137 | 543 |
Goal "[| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1"; |
4091 | 544 |
by (best_tac (claset() addEs [natE] addss (simpset())) 1); |
1793 | 545 |
qed "mult_eq_1_iff"; |
546 |
||
1708 | 547 |
(*Cancellation law for division*) |
5137 | 548 |
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n"; |
1708 | 549 |
by (eres_inst_tac [("i","m")] complete_induct 1); |
550 |
by (excluded_middle_tac "x<n" 1); |
|
4091 | 551 |
by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, |
1793 | 552 |
mult_lt_mono2]) 2); |
1708 | 553 |
by (asm_full_simp_tac |
4091 | 554 |
(simpset() addsimps [not_lt_iff_le, nat_into_Ord, |
1708 | 555 |
zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq, |
556 |
diff_mult_distrib2 RS sym, |
|
1793 | 557 |
div_termination RS ltD]) 1); |
1708 | 558 |
qed "div_cancel"; |
559 |
||
5137 | 560 |
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \ |
1708 | 561 |
\ (k#*m) mod (k#*n) = k #* (m mod n)"; |
562 |
by (eres_inst_tac [("i","m")] complete_induct 1); |
|
563 |
by (excluded_middle_tac "x<n" 1); |
|
4091 | 564 |
by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, |
1793 | 565 |
mult_lt_mono2]) 2); |
1708 | 566 |
by (asm_full_simp_tac |
4091 | 567 |
(simpset() addsimps [not_lt_iff_le, nat_into_Ord, |
1708 | 568 |
zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq, |
569 |
diff_mult_distrib2 RS sym, |
|
1793 | 570 |
div_termination RS ltD]) 1); |
1708 | 571 |
qed "mult_mod_distrib"; |
572 |
||
1793 | 573 |
(** Lemma for gcd **) |
1708 | 574 |
|
1793 | 575 |
val mono_lemma = (nat_into_Ord RS Ord_0_lt) RSN (2,mult_lt_mono2); |
576 |
||
5137 | 577 |
Goal "[| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0"; |
1793 | 578 |
by (rtac disjCI 1); |
579 |
by (dtac sym 1); |
|
580 |
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I])); |
|
4091 | 581 |
by (fast_tac (claset() addss (simpset())) 1); |
2469 | 582 |
by (fast_tac (le_cs addDs [mono_lemma] |
4091 | 583 |
addss (simpset() addsimps [mult_1_right])) 1); |
1793 | 584 |
qed "mult_eq_self_implies_10"; |
1708 | 585 |
|
2469 | 586 |
|
587 |
(*Thanks to Sten Agerholm*) |
|
5504 | 588 |
Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k"; |
2493 | 589 |
by (etac rev_mp 1); |
3016 | 590 |
by (eres_inst_tac [("n","n")] nat_induct 1); |
2469 | 591 |
by (Asm_simp_tac 1); |
3736
39ee3d31cfbc
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
paulson
parents:
3207
diff
changeset
|
592 |
by Safe_tac; |
4091 | 593 |
by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1); |
2469 | 594 |
by (etac lt_asym 1); |
595 |
by (assume_tac 1); |
|
596 |
by (Asm_full_simp_tac 1); |
|
4091 | 597 |
by (asm_full_simp_tac (simpset() addsimps [le_iff, nat_into_Ord]) 1); |
3016 | 598 |
by (Blast_tac 1); |
2469 | 599 |
qed "add_le_elim1"; |
600 |
||
5504 | 601 |
Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)"; |
602 |
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1); |
|
603 |
be rev_mp 1; |
|
604 |
by (etac nat_induct 1); |
|
605 |
by (ALLGOALS (simp_tac (simpset() addsimps [le_iff]))); |
|
606 |
by (blast_tac (claset() addSEs [leE] |
|
607 |
addSIs [add_0_right RS sym, add_succ_right RS sym]) 1); |
|
608 |
qed_spec_mp "less_imp_Suc_add"; |