author | paulson |
Mon, 06 Aug 2001 12:42:43 +0200 | |
changeset 11461 | ffeac9aa1967 |
parent 11338 | 779d289255f7 |
child 11464 | ddea204de5bc |
permissions | -rw-r--r-- |
2608 | 1 |
(* Title: HOL/NatDef.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
*) |
|
6 |
||
11326
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
11135
diff
changeset
|
7 |
val rew = rewrite_rule [symmetric Nat_def]; |
2608 | 8 |
|
9 |
(*** Induction ***) |
|
10 |
||
5316 | 11 |
val prems = Goalw [Zero_def,Suc_def] |
2608 | 12 |
"[| P(0); \ |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3023
diff
changeset
|
13 |
\ !!n. P(n) ==> P(Suc(n)) |] ==> P(n)"; |
2608 | 14 |
by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*) |
11326
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
11135
diff
changeset
|
15 |
by (rtac (Rep_Nat RS rew Nat'.induct) 1); |
2608 | 16 |
by (REPEAT (ares_tac prems 1 |
17 |
ORELSE eresolve_tac [Abs_Nat_inverse RS subst] 1)); |
|
18 |
qed "nat_induct"; |
|
19 |
||
20 |
(*Perform induction on n. *) |
|
5187
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
5148
diff
changeset
|
21 |
fun nat_ind_tac a i = |
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
5148
diff
changeset
|
22 |
res_inst_tac [("n",a)] nat_induct i THEN rename_last_tac a [""] (i+1); |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3023
diff
changeset
|
23 |
|
2608 | 24 |
(*A special form of induction for reasoning about m<n and m-n*) |
5316 | 25 |
val prems = Goal |
2608 | 26 |
"[| !!x. P x 0; \ |
27 |
\ !!y. P 0 (Suc y); \ |
|
28 |
\ !!x y. [| P x y |] ==> P (Suc x) (Suc y) \ |
|
29 |
\ |] ==> P m n"; |
|
30 |
by (res_inst_tac [("x","m")] spec 1); |
|
31 |
by (nat_ind_tac "n" 1); |
|
32 |
by (rtac allI 2); |
|
33 |
by (nat_ind_tac "x" 2); |
|
34 |
by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1)); |
|
35 |
qed "diff_induct"; |
|
36 |
||
37 |
(*** Isomorphisms: Abs_Nat and Rep_Nat ***) |
|
38 |
||
39 |
(*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat), |
|
40 |
since we assume the isomorphism equations will one day be given by Isabelle*) |
|
41 |
||
5069 | 42 |
Goal "inj(Rep_Nat)"; |
2608 | 43 |
by (rtac inj_inverseI 1); |
44 |
by (rtac Rep_Nat_inverse 1); |
|
45 |
qed "inj_Rep_Nat"; |
|
46 |
||
5069 | 47 |
Goal "inj_on Abs_Nat Nat"; |
4830 | 48 |
by (rtac inj_on_inverseI 1); |
2608 | 49 |
by (etac Abs_Nat_inverse 1); |
4830 | 50 |
qed "inj_on_Abs_Nat"; |
2608 | 51 |
|
52 |
(*** Distinctness of constructors ***) |
|
53 |
||
5069 | 54 |
Goalw [Zero_def,Suc_def] "Suc(m) ~= 0"; |
4830 | 55 |
by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1); |
2608 | 56 |
by (rtac Suc_Rep_not_Zero_Rep 1); |
11326
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
11135
diff
changeset
|
57 |
by (REPEAT (resolve_tac [Rep_Nat, rew Nat'.Suc_RepI, rew Nat'.Zero_RepI] 1)); |
2608 | 58 |
qed "Suc_not_Zero"; |
59 |
||
60 |
bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym); |
|
61 |
||
62 |
AddIffs [Suc_not_Zero,Zero_not_Suc]; |
|
63 |
||
64 |
bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE)); |
|
9108 | 65 |
bind_thm ("Zero_neq_Suc", sym RS Suc_neq_Zero); |
2608 | 66 |
|
67 |
(** Injectiveness of Suc **) |
|
68 |
||
5069 | 69 |
Goalw [Suc_def] "inj(Suc)"; |
2608 | 70 |
by (rtac injI 1); |
4830 | 71 |
by (dtac (inj_on_Abs_Nat RS inj_onD) 1); |
11326
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
11135
diff
changeset
|
72 |
by (REPEAT (resolve_tac [Rep_Nat, rew Nat'.Suc_RepI] 1)); |
2608 | 73 |
by (dtac (inj_Suc_Rep RS injD) 1); |
74 |
by (etac (inj_Rep_Nat RS injD) 1); |
|
75 |
qed "inj_Suc"; |
|
76 |
||
9108 | 77 |
bind_thm ("Suc_inject", inj_Suc RS injD); |
2608 | 78 |
|
5069 | 79 |
Goal "(Suc(m)=Suc(n)) = (m=n)"; |
2608 | 80 |
by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); |
81 |
qed "Suc_Suc_eq"; |
|
82 |
||
83 |
AddIffs [Suc_Suc_eq]; |
|
84 |
||
5069 | 85 |
Goal "n ~= Suc(n)"; |
2608 | 86 |
by (nat_ind_tac "n" 1); |
87 |
by (ALLGOALS Asm_simp_tac); |
|
88 |
qed "n_not_Suc_n"; |
|
89 |
||
90 |
bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym); |
|
91 |
||
11461 | 92 |
Goal "(ALL x. x = (0::nat)) = False"; |
11338 | 93 |
by Auto_tac; |
94 |
qed "nat_not_singleton"; |
|
95 |
||
5187
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
5148
diff
changeset
|
96 |
(*** Basic properties of "less than" ***) |
2608 | 97 |
|
11135 | 98 |
Goalw [wf_def, pred_nat_def] "wf pred_nat"; |
3718 | 99 |
by (Clarify_tac 1); |
2608 | 100 |
by (nat_ind_tac "x" 1); |
3236 | 101 |
by (ALLGOALS Blast_tac); |
2608 | 102 |
qed "wf_pred_nat"; |
103 |
||
11135 | 104 |
Goalw [less_def] "wf {(x,y::nat). x<y}"; |
105 |
by (rtac (wf_pred_nat RS wf_trancl RS wf_subset) 1); |
|
106 |
by (Blast_tac 1); |
|
107 |
qed "wf_less"; |
|
108 |
||
3378 | 109 |
(*Used in TFL/post.sml*) |
5069 | 110 |
Goalw [less_def] "(m,n) : pred_nat^+ = (m<n)"; |
3378 | 111 |
by (rtac refl 1); |
112 |
qed "less_eq"; |
|
113 |
||
2608 | 114 |
(** Introduction properties **) |
115 |
||
5316 | 116 |
Goalw [less_def] "[| i<j; j<k |] ==> i<(k::nat)"; |
2608 | 117 |
by (rtac (trans_trancl RS transD) 1); |
5316 | 118 |
by (assume_tac 1); |
119 |
by (assume_tac 1); |
|
2608 | 120 |
qed "less_trans"; |
121 |
||
5069 | 122 |
Goalw [less_def, pred_nat_def] "n < Suc(n)"; |
4089 | 123 |
by (simp_tac (simpset() addsimps [r_into_trancl]) 1); |
2608 | 124 |
qed "lessI"; |
125 |
AddIffs [lessI]; |
|
126 |
||
127 |
(* i<j ==> i<Suc(j) *) |
|
128 |
bind_thm("less_SucI", lessI RSN (2, less_trans)); |
|
129 |
||
5069 | 130 |
Goal "0 < Suc(n)"; |
2608 | 131 |
by (nat_ind_tac "n" 1); |
132 |
by (rtac lessI 1); |
|
133 |
by (etac less_trans 1); |
|
134 |
by (rtac lessI 1); |
|
135 |
qed "zero_less_Suc"; |
|
136 |
AddIffs [zero_less_Suc]; |
|
137 |
||
138 |
(** Elimination properties **) |
|
139 |
||
5316 | 140 |
Goalw [less_def] "n<m ==> ~ m<(n::nat)"; |
141 |
by (blast_tac (claset() addIs [wf_pred_nat, wf_trancl RS wf_asym])1); |
|
2608 | 142 |
qed "less_not_sym"; |
143 |
||
5474
a2109bb8ce2b
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset
|
144 |
(* [| n<m; ~P ==> m<n |] ==> P *) |
10231 | 145 |
bind_thm ("less_asym", less_not_sym RS contrapos_np); |
2608 | 146 |
|
5069 | 147 |
Goalw [less_def] "~ n<(n::nat)"; |
9160 | 148 |
by (rtac (wf_pred_nat RS wf_trancl RS wf_not_refl) 1); |
2608 | 149 |
qed "less_not_refl"; |
150 |
||
151 |
(* n<n ==> R *) |
|
9160 | 152 |
bind_thm ("less_irrefl", less_not_refl RS notE); |
5474
a2109bb8ce2b
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset
|
153 |
AddSEs [less_irrefl]; |
2608 | 154 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
155 |
Goal "n<m ==> m ~= (n::nat)"; |
5474
a2109bb8ce2b
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset
|
156 |
by (Blast_tac 1); |
2608 | 157 |
qed "less_not_refl2"; |
158 |
||
5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
159 |
(* s < t ==> s ~= t *) |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
160 |
bind_thm ("less_not_refl3", less_not_refl2 RS not_sym); |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
161 |
|
2608 | 162 |
|
5316 | 163 |
val major::prems = Goalw [less_def, pred_nat_def] |
2608 | 164 |
"[| i<k; k=Suc(i) ==> P; !!j. [| i<j; k=Suc(j) |] ==> P \ |
165 |
\ |] ==> P"; |
|
166 |
by (rtac (major RS tranclE) 1); |
|
3236 | 167 |
by (ALLGOALS Full_simp_tac); |
2608 | 168 |
by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE' |
3236 | 169 |
eresolve_tac (prems@[asm_rl, Pair_inject]))); |
2608 | 170 |
qed "lessE"; |
171 |
||
8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset
|
172 |
Goal "~ n < (0::nat)"; |
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset
|
173 |
by (blast_tac (claset() addEs [lessE]) 1); |
2608 | 174 |
qed "not_less0"; |
175 |
AddIffs [not_less0]; |
|
176 |
||
177 |
(* n<0 ==> R *) |
|
178 |
bind_thm ("less_zeroE", not_less0 RS notE); |
|
179 |
||
5316 | 180 |
val [major,less,eq] = Goal |
2608 | 181 |
"[| m < Suc(n); m<n ==> P; m=n ==> P |] ==> P"; |
182 |
by (rtac (major RS lessE) 1); |
|
183 |
by (rtac eq 1); |
|
2891 | 184 |
by (Blast_tac 1); |
2608 | 185 |
by (rtac less 1); |
2891 | 186 |
by (Blast_tac 1); |
2608 | 187 |
qed "less_SucE"; |
188 |
||
5069 | 189 |
Goal "(m < Suc(n)) = (m < n | m = n)"; |
4089 | 190 |
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); |
2608 | 191 |
qed "less_Suc_eq"; |
192 |
||
5069 | 193 |
Goal "(n<1) = (n=0)"; |
4089 | 194 |
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset
|
195 |
qed "less_one"; |
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset
|
196 |
AddIffs [less_one]; |
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset
|
197 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
198 |
Goal "m<n ==> Suc(m) < Suc(n)"; |
2608 | 199 |
by (etac rev_mp 1); |
200 |
by (nat_ind_tac "n" 1); |
|
5474
a2109bb8ce2b
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset
|
201 |
by (ALLGOALS (fast_tac (claset() addEs [less_trans, lessE]))); |
2608 | 202 |
qed "Suc_mono"; |
203 |
||
204 |
(*"Less than" is a linear ordering*) |
|
5069 | 205 |
Goal "m<n | m=n | n<(m::nat)"; |
2608 | 206 |
by (nat_ind_tac "m" 1); |
207 |
by (nat_ind_tac "n" 1); |
|
208 |
by (rtac (refl RS disjI1 RS disjI2) 1); |
|
209 |
by (rtac (zero_less_Suc RS disjI1) 1); |
|
4089 | 210 |
by (blast_tac (claset() addIs [Suc_mono, less_SucI] addEs [lessE]) 1); |
2608 | 211 |
qed "less_linear"; |
212 |
||
5069 | 213 |
Goal "!!m::nat. (m ~= n) = (m<n | n<m)"; |
4737 | 214 |
by (cut_facts_tac [less_linear] 1); |
5500 | 215 |
by (Blast_tac 1); |
4737 | 216 |
qed "nat_neq_iff"; |
217 |
||
7030 | 218 |
val [major,eqCase,lessCase] = Goal |
219 |
"[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"; |
|
220 |
by (rtac (less_linear RS disjE) 1); |
|
221 |
by (etac disjE 2); |
|
222 |
by (etac lessCase 1); |
|
223 |
by (etac (sym RS eqCase) 1); |
|
224 |
by (etac major 1); |
|
225 |
qed "nat_less_cases"; |
|
2608 | 226 |
|
4745 | 227 |
|
228 |
(** Inductive (?) properties **) |
|
229 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
230 |
Goal "[| m<n; Suc m ~= n |] ==> Suc(m) < n"; |
4745 | 231 |
by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); |
232 |
by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1); |
|
233 |
qed "Suc_lessI"; |
|
234 |
||
5316 | 235 |
Goal "Suc(m) < n ==> m<n"; |
236 |
by (etac rev_mp 1); |
|
4745 | 237 |
by (nat_ind_tac "n" 1); |
238 |
by (ALLGOALS (fast_tac (claset() addSIs [lessI RS less_SucI] |
|
239 |
addEs [less_trans, lessE]))); |
|
240 |
qed "Suc_lessD"; |
|
241 |
||
5316 | 242 |
val [major,minor] = Goal |
4745 | 243 |
"[| Suc(i)<k; !!j. [| i<j; k=Suc(j) |] ==> P \ |
244 |
\ |] ==> P"; |
|
245 |
by (rtac (major RS lessE) 1); |
|
246 |
by (etac (lessI RS minor) 1); |
|
247 |
by (etac (Suc_lessD RS minor) 1); |
|
248 |
by (assume_tac 1); |
|
249 |
qed "Suc_lessE"; |
|
250 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
251 |
Goal "Suc(m) < Suc(n) ==> m<n"; |
4745 | 252 |
by (blast_tac (claset() addEs [lessE, make_elim Suc_lessD]) 1); |
253 |
qed "Suc_less_SucD"; |
|
254 |
||
255 |
||
5069 | 256 |
Goal "(Suc(m) < Suc(n)) = (m<n)"; |
4745 | 257 |
by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]); |
258 |
qed "Suc_less_eq"; |
|
8555
17325ee838ab
Suc_less_eq now with AddIffs. How could this have been overlooked?
paulson
parents:
7064
diff
changeset
|
259 |
AddIffs [Suc_less_eq]; |
4745 | 260 |
|
6109 | 261 |
(*Goal "~(Suc(n) < n)"; |
4745 | 262 |
by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1); |
263 |
qed "not_Suc_n_less_n"; |
|
6109 | 264 |
Addsimps [not_Suc_n_less_n];*) |
4745 | 265 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
266 |
Goal "i<j ==> j<k --> Suc i < k"; |
4745 | 267 |
by (nat_ind_tac "k" 1); |
268 |
by (ALLGOALS (asm_simp_tac (simpset()))); |
|
269 |
by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
|
270 |
by (blast_tac (claset() addDs [Suc_lessD]) 1); |
|
271 |
qed_spec_mp "less_trans_Suc"; |
|
272 |
||
2608 | 273 |
(*Can be used with less_Suc_eq to get n=m | n<m *) |
5069 | 274 |
Goal "(~ m < n) = (n < Suc(m))"; |
2608 | 275 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
276 |
by (ALLGOALS Asm_simp_tac); |
|
277 |
qed "not_less_eq"; |
|
278 |
||
279 |
(*Complete induction, aka course-of-values induction*) |
|
5316 | 280 |
val prems = Goalw [less_def] |
9160 | 281 |
"[| !!n. [| ALL m::nat. m<n --> P(m) |] ==> P(n) |] ==> P(n)"; |
2608 | 282 |
by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); |
283 |
by (eresolve_tac prems 1); |
|
9870 | 284 |
qed "nat_less_induct"; |
2608 | 285 |
|
286 |
(*** Properties of <= ***) |
|
287 |
||
5500 | 288 |
(*Was le_eq_less_Suc, but this orientation is more useful*) |
289 |
Goalw [le_def] "(m < Suc n) = (m <= n)"; |
|
290 |
by (rtac (not_less_eq RS sym) 1); |
|
291 |
qed "less_Suc_eq_le"; |
|
2608 | 292 |
|
3343 | 293 |
(* m<=n ==> m < Suc n *) |
5500 | 294 |
bind_thm ("le_imp_less_Suc", less_Suc_eq_le RS iffD2); |
3343 | 295 |
|
8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset
|
296 |
Goalw [le_def] "(0::nat) <= n"; |
2608 | 297 |
by (rtac not_less0 1); |
298 |
qed "le0"; |
|
6075 | 299 |
AddIffs [le0]; |
2608 | 300 |
|
5069 | 301 |
Goalw [le_def] "~ Suc n <= n"; |
2608 | 302 |
by (Simp_tac 1); |
303 |
qed "Suc_n_not_le_n"; |
|
304 |
||
8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset
|
305 |
Goalw [le_def] "!!i::nat. (i <= 0) = (i = 0)"; |
2608 | 306 |
by (nat_ind_tac "i" 1); |
307 |
by (ALLGOALS Asm_simp_tac); |
|
308 |
qed "le_0_eq"; |
|
4614 | 309 |
AddIffs [le_0_eq]; |
2608 | 310 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
311 |
Goal "(m <= Suc(n)) = (m<=n | m = Suc n)"; |
5500 | 312 |
by (simp_tac (simpset() delsimps [less_Suc_eq_le] |
313 |
addsimps [less_Suc_eq_le RS sym, less_Suc_eq]) 1); |
|
3355 | 314 |
qed "le_Suc_eq"; |
315 |
||
4614 | 316 |
(* [| m <= Suc n; m <= n ==> R; m = Suc n ==> R |] ==> R *) |
317 |
bind_thm ("le_SucE", le_Suc_eq RS iffD1 RS disjE); |
|
318 |
||
5316 | 319 |
Goalw [le_def] "~n<m ==> m<=(n::nat)"; |
320 |
by (assume_tac 1); |
|
2608 | 321 |
qed "leI"; |
322 |
||
5316 | 323 |
Goalw [le_def] "m<=n ==> ~ n < (m::nat)"; |
324 |
by (assume_tac 1); |
|
2608 | 325 |
qed "leD"; |
326 |
||
9108 | 327 |
bind_thm ("leE", make_elim leD); |
2608 | 328 |
|
5069 | 329 |
Goal "(~n<m) = (m<=(n::nat))"; |
4089 | 330 |
by (blast_tac (claset() addIs [leI] addEs [leE]) 1); |
2608 | 331 |
qed "not_less_iff_le"; |
332 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
333 |
Goalw [le_def] "~ m <= n ==> n<(m::nat)"; |
2891 | 334 |
by (Blast_tac 1); |
2608 | 335 |
qed "not_leE"; |
336 |
||
5069 | 337 |
Goalw [le_def] "(~n<=m) = (m<(n::nat))"; |
4599 | 338 |
by (Simp_tac 1); |
339 |
qed "not_le_iff_less"; |
|
340 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
341 |
Goalw [le_def] "m < n ==> Suc(m) <= n"; |
4089 | 342 |
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
343 |
by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1); |
|
3343 | 344 |
qed "Suc_leI"; (*formerly called lessD*) |
2608 | 345 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
346 |
Goalw [le_def] "Suc(m) <= n ==> m <= n"; |
4089 | 347 |
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
2608 | 348 |
qed "Suc_leD"; |
349 |
||
350 |
(* stronger version of Suc_leD *) |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
351 |
Goalw [le_def] "Suc m <= n ==> m < n"; |
4089 | 352 |
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
2608 | 353 |
by (cut_facts_tac [less_linear] 1); |
2891 | 354 |
by (Blast_tac 1); |
2608 | 355 |
qed "Suc_le_lessD"; |
356 |
||
5069 | 357 |
Goal "(Suc m <= n) = (m < n)"; |
4089 | 358 |
by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1); |
2608 | 359 |
qed "Suc_le_eq"; |
360 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
361 |
Goalw [le_def] "m <= n ==> m <= Suc n"; |
4089 | 362 |
by (blast_tac (claset() addDs [Suc_lessD]) 1); |
2608 | 363 |
qed "le_SucI"; |
364 |
||
6109 | 365 |
(*bind_thm ("le_Suc", not_Suc_n_less_n RS leI);*) |
2608 | 366 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
367 |
Goalw [le_def] "m < n ==> m <= (n::nat)"; |
4089 | 368 |
by (blast_tac (claset() addEs [less_asym]) 1); |
2608 | 369 |
qed "less_imp_le"; |
370 |
||
5591 | 371 |
(*For instance, (Suc m < Suc n) = (Suc m <= n) = (m<n) *) |
9108 | 372 |
bind_thms ("le_simps", [less_imp_le, less_Suc_eq_le, Suc_le_eq]); |
5591 | 373 |
|
5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
374 |
|
3343 | 375 |
(** Equivalence of m<=n and m<n | m=n **) |
376 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
377 |
Goalw [le_def] "m <= n ==> m < n | m=(n::nat)"; |
2608 | 378 |
by (cut_facts_tac [less_linear] 1); |
4089 | 379 |
by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1); |
2608 | 380 |
qed "le_imp_less_or_eq"; |
381 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
382 |
Goalw [le_def] "m<n | m=n ==> m <=(n::nat)"; |
2608 | 383 |
by (cut_facts_tac [less_linear] 1); |
4089 | 384 |
by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1); |
2608 | 385 |
qed "less_or_eq_imp_le"; |
386 |
||
5069 | 387 |
Goal "(m <= (n::nat)) = (m < n | m=n)"; |
2608 | 388 |
by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); |
389 |
qed "le_eq_less_or_eq"; |
|
390 |
||
4635 | 391 |
(*Useful with Blast_tac. m=n ==> m<=n *) |
392 |
bind_thm ("eq_imp_le", disjI2 RS less_or_eq_imp_le); |
|
393 |
||
5069 | 394 |
Goal "n <= (n::nat)"; |
4089 | 395 |
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
2608 | 396 |
qed "le_refl"; |
397 |
||
5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
398 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
399 |
Goal "[| i <= j; j < k |] ==> i < (k::nat)"; |
4468 | 400 |
by (blast_tac (claset() addSDs [le_imp_less_or_eq] |
401 |
addIs [less_trans]) 1); |
|
2608 | 402 |
qed "le_less_trans"; |
403 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
404 |
Goal "[| i < j; j <= k |] ==> i < (k::nat)"; |
4468 | 405 |
by (blast_tac (claset() addSDs [le_imp_less_or_eq] |
406 |
addIs [less_trans]) 1); |
|
2608 | 407 |
qed "less_le_trans"; |
408 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
409 |
Goal "[| i <= j; j <= k |] ==> i <= (k::nat)"; |
4468 | 410 |
by (blast_tac (claset() addSDs [le_imp_less_or_eq] |
411 |
addIs [less_or_eq_imp_le, less_trans]) 1); |
|
2608 | 412 |
qed "le_trans"; |
413 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
414 |
Goal "[| m <= n; n <= m |] ==> m = (n::nat)"; |
4468 | 415 |
(*order_less_irrefl could make this proof fail*) |
416 |
by (blast_tac (claset() addSDs [le_imp_less_or_eq] |
|
417 |
addSEs [less_irrefl] addEs [less_asym]) 1); |
|
2608 | 418 |
qed "le_anti_sym"; |
419 |
||
5069 | 420 |
Goal "(Suc(n) <= Suc(m)) = (n <= m)"; |
5500 | 421 |
by (simp_tac (simpset() addsimps le_simps) 1); |
2608 | 422 |
qed "Suc_le_mono"; |
423 |
||
424 |
AddIffs [Suc_le_mono]; |
|
425 |
||
5500 | 426 |
(* Axiom 'order_less_le' of class 'order': *) |
5069 | 427 |
Goal "(m::nat) < n = (m <= n & m ~= n)"; |
4737 | 428 |
by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1); |
429 |
by (blast_tac (claset() addSEs [less_asym]) 1); |
|
2608 | 430 |
qed "nat_less_le"; |
431 |
||
5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
432 |
(* [| m <= n; m ~= n |] ==> m < n *) |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
433 |
bind_thm ("le_neq_implies_less", [nat_less_le, conjI] MRS iffD2); |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
434 |
|
4640 | 435 |
(* Axiom 'linorder_linear' of class 'linorder': *) |
5069 | 436 |
Goal "(m::nat) <= n | n <= m"; |
4640 | 437 |
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
438 |
by (cut_facts_tac [less_linear] 1); |
|
5132 | 439 |
by (Blast_tac 1); |
4640 | 440 |
qed "nat_le_linear"; |
441 |
||
5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
442 |
Goal "~ n < m ==> (n < Suc m) = (n = m)"; |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
443 |
by (blast_tac (claset() addSEs [less_SucE]) 1); |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
444 |
qed "not_less_less_Suc_eq"; |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
445 |
|
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
446 |
|
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
447 |
(*Rewrite (n < Suc m) to (n=m) if ~ n<m or m<=n hold. |
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset
|
448 |
Not suitable as default simprules because they often lead to looping*) |
9108 | 449 |
bind_thms ("not_less_simps", [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq]); |
4640 | 450 |
|
10706 | 451 |
|
452 |
(** Re-orientation of the equations 0=x and Suc n = x. * |
|
453 |
||
454 |
The condition "True" is a hack to prevent looping for e.g. Suc m = Suc n. |
|
455 |
Conditional rewrite rules are tried after unconditional ones. |
|
456 |
**) |
|
457 |
||
10711
a9f6994fb906
generalized the re-orientation 0f 0=... to all types
paulson
parents:
10706
diff
changeset
|
458 |
(*Polymorphic, not just for "nat"*) |
a9f6994fb906
generalized the re-orientation 0f 0=... to all types
paulson
parents:
10706
diff
changeset
|
459 |
Goal "True ==> (0 = x) = (x = 0)"; |
10706 | 460 |
by Auto_tac; |
461 |
qed "zero_reorient"; |
|
462 |
Addsimps [zero_reorient]; |
|
463 |
||
464 |
Goal "True ==> (1 = x) = (x = 1)"; |
|
465 |
by Auto_tac; |
|
466 |
qed "one_reorient"; |
|
467 |
Addsimps [one_reorient]; |
|
468 |
||
469 |
Goal "True ==> (2 = x) = (x = 2)"; |
|
470 |
by Auto_tac; |
|
471 |
qed "two_reorient"; |
|
472 |
Addsimps [two_reorient]; |