author | paulson |
Fri, 18 Feb 2000 15:35:29 +0100 | |
changeset 8255 | 38f96394c099 |
parent 8201 | a81d18b0a9b1 |
child 8551 | 5c22595bc599 |
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"; |
1708 | 249 |
val add_commute_k = read_instantiate [("n","k")] add_commute; |
4091 | 250 |
by (asm_simp_tac (simpset() addsimps [add_commute_k, 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)"; |
1708 | 266 |
val mult_commute_k = read_instantiate [("m","k")] mult_commute; |
4091 | 267 |
by (asm_simp_tac (simpset() addsimps |
1793 | 268 |
[mult_commute_k, diff_mult_distrib]) 1); |
1708 | 269 |
qed "diff_mult_distrib2" ; |
270 |
||
0 | 271 |
(*** Remainder ***) |
272 |
||
5137 | 273 |
Goal "[| 0<n; n le m; m:nat |] ==> m #- n < m"; |
7499 | 274 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); |
0 | 275 |
by (etac rev_mp 1); |
276 |
by (etac rev_mp 1); |
|
277 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
6070 | 278 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self]))); |
760 | 279 |
qed "div_termination"; |
0 | 280 |
|
1461 | 281 |
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
|
282 |
nat_typechecks @ |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
283 |
[Ord_transrec_type, apply_type, div_termination RS ltD, if_type, |
435 | 284 |
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
|
285 |
|
8201 | 286 |
val div_ss = simpset() addsimps [div_termination RS ltD, |
6070 | 287 |
not_lt_iff_le RS iffD2]; |
0 | 288 |
|
289 |
(*Type checking depends upon termination!*) |
|
5137 | 290 |
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
|
291 |
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
760 | 292 |
qed "mod_type"; |
6153 | 293 |
AddTCs [mod_type]; |
0 | 294 |
|
5137 | 295 |
Goal "[| 0<n; m<n |] ==> m mod n = m"; |
0 | 296 |
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
|
297 |
by (asm_simp_tac div_ss 1); |
760 | 298 |
qed "mod_less"; |
0 | 299 |
|
5137 | 300 |
Goal "[| 0<n; n le m; m:nat |] ==> m mod n = (m#-n) mod n"; |
7499 | 301 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); |
0 | 302 |
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
|
303 |
by (asm_simp_tac div_ss 1); |
760 | 304 |
qed "mod_geq"; |
0 | 305 |
|
2469 | 306 |
Addsimps [mod_type, mod_less, mod_geq]; |
307 |
||
0 | 308 |
(*** Quotient ***) |
309 |
||
310 |
(*Type checking depends upon termination!*) |
|
5067 | 311 |
Goalw [div_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
312 |
"[| 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
|
313 |
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
760 | 314 |
qed "div_type"; |
6153 | 315 |
AddTCs [div_type]; |
0 | 316 |
|
5137 | 317 |
Goal "[| 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 |
|
5137 | 322 |
Goal "[| 0<n; n le m; m:nat |] ==> m div n = succ((m#-n) div n)"; |
7499 | 323 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); |
0 | 324 |
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
|
325 |
by (asm_simp_tac div_ss 1); |
760 | 326 |
qed "div_geq"; |
0 | 327 |
|
2469 | 328 |
Addsimps [div_type, div_less, div_geq]; |
329 |
||
1609 | 330 |
(*A key result*) |
5137 | 331 |
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
|
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*) |
2469 | 335 |
by (Asm_simp_tac 2); |
25
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 |
8201 | 338 |
(simpset() addsimps [not_lt_iff_le, add_assoc, |
1461 | 339 |
div_termination RS ltD, add_diff_inverse]) 1); |
760 | 340 |
qed "mod_div_equality"; |
0 | 341 |
|
6068 | 342 |
|
343 |
(*** Further facts about mod (mainly for mutilated chess board) ***) |
|
1609 | 344 |
|
6068 | 345 |
Goal "[| 0<n; m:nat; n:nat |] \ |
346 |
\ ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"; |
|
1609 | 347 |
by (etac complete_induct 1); |
348 |
by (excluded_middle_tac "succ(x)<n" 1); |
|
1623 | 349 |
(* case succ(x) < n *) |
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
350 |
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
|
351 |
succ_neq_self]) 2); |
4091 | 352 |
by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2); |
1623 | 353 |
(* case n le succ(x) *) |
8201 | 354 |
by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1); |
1623 | 355 |
by (etac leE 1); |
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
356 |
(*equality case*) |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
357 |
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
|
358 |
by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ]) 1); |
1609 | 359 |
qed "mod_succ"; |
360 |
||
5137 | 361 |
Goal "[| 0<n; m:nat; n:nat |] ==> m mod n < n"; |
1609 | 362 |
by (etac complete_induct 1); |
363 |
by (excluded_middle_tac "x<n" 1); |
|
364 |
(*case x<n*) |
|
4091 | 365 |
by (asm_simp_tac (simpset() addsimps [mod_less]) 2); |
1609 | 366 |
(*case n le x*) |
367 |
by (asm_full_simp_tac |
|
8201 | 368 |
(simpset() addsimps [not_lt_iff_le, mod_geq, div_termination RS ltD]) 1); |
1609 | 369 |
qed "mod_less_divisor"; |
370 |
||
371 |
||
6068 | 372 |
Goal "[| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"; |
1609 | 373 |
by (subgoal_tac "k mod 2: 2" 1); |
4091 | 374 |
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); |
1623 | 375 |
by (dtac ltD 1); |
5137 | 376 |
by Auto_tac; |
1609 | 377 |
qed "mod2_cases"; |
378 |
||
5137 | 379 |
Goal "m:nat ==> succ(succ(m)) mod 2 = m mod 2"; |
1609 | 380 |
by (subgoal_tac "m mod 2: 2" 1); |
4091 | 381 |
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); |
382 |
by (asm_simp_tac (simpset() addsimps [mod_succ] setloop Step_tac) 1); |
|
1609 | 383 |
qed "mod2_succ_succ"; |
384 |
||
5137 | 385 |
Goal "m:nat ==> (m#+m) mod 2 = 0"; |
6070 | 386 |
by (induct_tac "m" 1); |
4091 | 387 |
by (simp_tac (simpset() addsimps [mod_less]) 1); |
388 |
by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1); |
|
1609 | 389 |
qed "mod2_add_self"; |
390 |
||
0 | 391 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
392 |
(**** Additional theorems about "le" ****) |
0 | 393 |
|
5137 | 394 |
Goal "[| m:nat; n:nat |] ==> m le m #+ n"; |
6070 | 395 |
by (induct_tac "m" 1); |
2469 | 396 |
by (ALLGOALS Asm_simp_tac); |
760 | 397 |
qed "add_le_self"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
398 |
|
5137 | 399 |
Goal "[| m:nat; n:nat |] ==> m le n #+ m"; |
2033 | 400 |
by (stac add_commute 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
401 |
by (REPEAT (ares_tac [add_le_self] 1)); |
760 | 402 |
qed "add_le_self2"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
403 |
|
1708 | 404 |
(*** Monotonicity of Addition ***) |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
405 |
|
1708 | 406 |
(*strict, in 1st argument; proof is by rule induction on 'less than'*) |
5137 | 407 |
Goal "[| i<j; j:nat; k:nat |] ==> i#+k < j#+k"; |
7499 | 408 |
by (ftac lt_nat_in_nat 1); |
127 | 409 |
by (assume_tac 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
410 |
by (etac succ_lt_induct 1); |
8201 | 411 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI]))); |
760 | 412 |
qed "add_lt_mono1"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
413 |
|
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
414 |
(*strict, in both arguments*) |
5137 | 415 |
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
|
416 |
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
|
417 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
2033 | 418 |
by (EVERY [stac add_commute 1, |
419 |
stac add_commute 3, |
|
1461 | 420 |
rtac add_lt_mono1 5]); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
421 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
760 | 422 |
qed "add_lt_mono"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
423 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
424 |
(*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
|
425 |
val lt_mono::ford::prems = Goal |
1461 | 426 |
"[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \ |
427 |
\ !!i. i:k ==> Ord(f(i)); \ |
|
428 |
\ i le j; j:k \ |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
429 |
\ |] ==> 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
|
430 |
by (cut_facts_tac prems 1); |
3016 | 431 |
by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1); |
760 | 432 |
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
|
433 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
434 |
(*le monotonicity, 1st argument*) |
5137 | 435 |
Goal "[| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; |
3840 | 436 |
by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1); |
435 | 437 |
by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1)); |
760 | 438 |
qed "add_le_mono1"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
439 |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
440 |
(* le monotonicity, BOTH arguments*) |
5137 | 441 |
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
|
442 |
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
|
443 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
2033 | 444 |
by (EVERY [stac add_commute 1, |
445 |
stac add_commute 3, |
|
1461 | 446 |
rtac add_le_mono1 5]); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
447 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
760 | 448 |
qed "add_le_mono"; |
1609 | 449 |
|
1708 | 450 |
(*** Monotonicity of Multiplication ***) |
451 |
||
5137 | 452 |
Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k"; |
7499 | 453 |
by (ftac lt_nat_in_nat 1); |
6070 | 454 |
by (induct_tac "k" 2); |
4091 | 455 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); |
1708 | 456 |
qed "mult_le_mono1"; |
457 |
||
458 |
(* le monotonicity, BOTH arguments*) |
|
5137 | 459 |
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l"; |
1708 | 460 |
by (rtac (mult_le_mono1 RS le_trans) 1); |
461 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
|
2033 | 462 |
by (EVERY [stac mult_commute 1, |
463 |
stac mult_commute 3, |
|
1708 | 464 |
rtac mult_le_mono1 5]); |
465 |
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
|
466 |
qed "mult_le_mono"; |
|
467 |
||
468 |
(*strict, in 1st argument; proof is by induction on k>0*) |
|
5137 | 469 |
Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j"; |
1793 | 470 |
by (etac zero_lt_natE 1); |
7499 | 471 |
by (ftac lt_nat_in_nat 2); |
2469 | 472 |
by (ALLGOALS Asm_simp_tac); |
6070 | 473 |
by (induct_tac "x" 1); |
4091 | 474 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono]))); |
1708 | 475 |
qed "mult_lt_mono2"; |
476 |
||
5137 | 477 |
Goal "[| i<j; 0<c; i:nat; j:nat; c:nat |] ==> i#*c < j#*c"; |
4839 | 478 |
by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1); |
479 |
qed "mult_lt_mono1"; |
|
480 |
||
5137 | 481 |
Goal "[| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n"; |
4091 | 482 |
by (best_tac (claset() addEs [natE] addss (simpset())) 1); |
1708 | 483 |
qed "zero_lt_mult_iff"; |
484 |
||
5137 | 485 |
Goal "[| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1"; |
4091 | 486 |
by (best_tac (claset() addEs [natE] addss (simpset())) 1); |
1793 | 487 |
qed "mult_eq_1_iff"; |
488 |
||
1708 | 489 |
(*Cancellation law for division*) |
5137 | 490 |
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n"; |
1708 | 491 |
by (eres_inst_tac [("i","m")] complete_induct 1); |
492 |
by (excluded_middle_tac "x<n" 1); |
|
4091 | 493 |
by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, |
1793 | 494 |
mult_lt_mono2]) 2); |
1708 | 495 |
by (asm_full_simp_tac |
8201 | 496 |
(simpset() addsimps [not_lt_iff_le, |
1708 | 497 |
zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq, |
498 |
diff_mult_distrib2 RS sym, |
|
1793 | 499 |
div_termination RS ltD]) 1); |
1708 | 500 |
qed "div_cancel"; |
501 |
||
5137 | 502 |
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \ |
1708 | 503 |
\ (k#*m) mod (k#*n) = k #* (m mod n)"; |
504 |
by (eres_inst_tac [("i","m")] complete_induct 1); |
|
505 |
by (excluded_middle_tac "x<n" 1); |
|
4091 | 506 |
by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, |
1793 | 507 |
mult_lt_mono2]) 2); |
1708 | 508 |
by (asm_full_simp_tac |
8201 | 509 |
(simpset() addsimps [not_lt_iff_le, |
1708 | 510 |
zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq, |
511 |
diff_mult_distrib2 RS sym, |
|
1793 | 512 |
div_termination RS ltD]) 1); |
1708 | 513 |
qed "mult_mod_distrib"; |
514 |
||
6070 | 515 |
(*Lemma for gcd*) |
5137 | 516 |
Goal "[| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0"; |
1793 | 517 |
by (rtac disjCI 1); |
518 |
by (dtac sym 1); |
|
519 |
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I])); |
|
6070 | 520 |
by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 2); |
521 |
by Auto_tac; |
|
1793 | 522 |
qed "mult_eq_self_implies_10"; |
1708 | 523 |
|
2469 | 524 |
(*Thanks to Sten Agerholm*) |
5504 | 525 |
Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k"; |
2493 | 526 |
by (etac rev_mp 1); |
6070 | 527 |
by (induct_tac "m" 1); |
2469 | 528 |
by (Asm_simp_tac 1); |
3736
39ee3d31cfbc
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
paulson
parents:
3207
diff
changeset
|
529 |
by Safe_tac; |
8201 | 530 |
by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt]) 1); |
2469 | 531 |
qed "add_le_elim1"; |
532 |
||
5504 | 533 |
Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)"; |
7499 | 534 |
by (ftac lt_nat_in_nat 1 THEN assume_tac 1); |
6163 | 535 |
by (etac rev_mp 1); |
6070 | 536 |
by (induct_tac "n" 1); |
5504 | 537 |
by (ALLGOALS (simp_tac (simpset() addsimps [le_iff]))); |
538 |
by (blast_tac (claset() addSEs [leE] |
|
539 |
addSIs [add_0_right RS sym, add_succ_right RS sym]) 1); |
|
540 |
qed_spec_mp "less_imp_Suc_add"; |