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