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