author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10231  178a272bceeb 
child 10706  f02834001fca 
permissions  rwrr 
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 

5069  7 
Goal "mono(%X. {Zero_Rep} Un (Suc_Rep``X))"; 
2608  8 
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1)); 
9 
qed "Nat_fun_mono"; 

10 

10186  11 
bind_thm ("Nat_unfold", Nat_fun_mono RS (Nat_def RS def_lfp_unfold)); 
2608  12 

13 
(* Zero is a natural number  this also justifies the type definition*) 

5069  14 
Goal "Zero_Rep: Nat"; 
2608  15 
by (stac Nat_unfold 1); 
16 
by (rtac (singletonI RS UnI1) 1); 

17 
qed "Zero_RepI"; 

18 

5316  19 
Goal "i: Nat ==> Suc_Rep(i) : Nat"; 
2608  20 
by (stac Nat_unfold 1); 
21 
by (rtac (imageI RS UnI2) 1); 

5316  22 
by (assume_tac 1); 
2608  23 
qed "Suc_RepI"; 
24 

25 
(*** Induction ***) 

26 

5316  27 
val major::prems = Goal 
2608  28 
"[ i: Nat; P(Zero_Rep); \ 
29 
\ !!j. [ j: Nat; P(j) ] ==> P(Suc_Rep(j)) ] ==> P(i)"; 

10202  30 
by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_lfp_induct) 1); 
4089  31 
by (blast_tac (claset() addIs prems) 1); 
2608  32 
qed "Nat_induct"; 
33 

5316  34 
val prems = Goalw [Zero_def,Suc_def] 
2608  35 
"[ P(0); \ 
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3023
diff
changeset

36 
\ !!n. P(n) ==> P(Suc(n)) ] ==> P(n)"; 
2608  37 
by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*) 
38 
by (rtac (Rep_Nat RS Nat_induct) 1); 

39 
by (REPEAT (ares_tac prems 1 

40 
ORELSE eresolve_tac [Abs_Nat_inverse RS subst] 1)); 

41 
qed "nat_induct"; 

42 

43 
(*Perform induction on n. *) 

5187
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
5148
diff
changeset

44 
fun nat_ind_tac a i = 
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
5148
diff
changeset

45 
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

46 

2608  47 
(*A special form of induction for reasoning about m<n and mn*) 
5316  48 
val prems = Goal 
2608  49 
"[ !!x. P x 0; \ 
50 
\ !!y. P 0 (Suc y); \ 

51 
\ !!x y. [ P x y ] ==> P (Suc x) (Suc y) \ 

52 
\ ] ==> P m n"; 

53 
by (res_inst_tac [("x","m")] spec 1); 

54 
by (nat_ind_tac "n" 1); 

55 
by (rtac allI 2); 

56 
by (nat_ind_tac "x" 2); 

57 
by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1)); 

58 
qed "diff_induct"; 

59 

60 
(*** Isomorphisms: Abs_Nat and Rep_Nat ***) 

61 

62 
(*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat), 

63 
since we assume the isomorphism equations will one day be given by Isabelle*) 

64 

5069  65 
Goal "inj(Rep_Nat)"; 
2608  66 
by (rtac inj_inverseI 1); 
67 
by (rtac Rep_Nat_inverse 1); 

68 
qed "inj_Rep_Nat"; 

69 

5069  70 
Goal "inj_on Abs_Nat Nat"; 
4830  71 
by (rtac inj_on_inverseI 1); 
2608  72 
by (etac Abs_Nat_inverse 1); 
4830  73 
qed "inj_on_Abs_Nat"; 
2608  74 

75 
(*** Distinctness of constructors ***) 

76 

5069  77 
Goalw [Zero_def,Suc_def] "Suc(m) ~= 0"; 
4830  78 
by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1); 
2608  79 
by (rtac Suc_Rep_not_Zero_Rep 1); 
80 
by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1)); 

81 
qed "Suc_not_Zero"; 

82 

83 
bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym); 

84 

85 
AddIffs [Suc_not_Zero,Zero_not_Suc]; 

86 

87 
bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE)); 

9108  88 
bind_thm ("Zero_neq_Suc", sym RS Suc_neq_Zero); 
2608  89 

90 
(** Injectiveness of Suc **) 

91 

5069  92 
Goalw [Suc_def] "inj(Suc)"; 
2608  93 
by (rtac injI 1); 
4830  94 
by (dtac (inj_on_Abs_Nat RS inj_onD) 1); 
2608  95 
by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1)); 
96 
by (dtac (inj_Suc_Rep RS injD) 1); 

97 
by (etac (inj_Rep_Nat RS injD) 1); 

98 
qed "inj_Suc"; 

99 

9108  100 
bind_thm ("Suc_inject", inj_Suc RS injD); 
2608  101 

5069  102 
Goal "(Suc(m)=Suc(n)) = (m=n)"; 
2608  103 
by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
104 
qed "Suc_Suc_eq"; 

105 

106 
AddIffs [Suc_Suc_eq]; 

107 

5069  108 
Goal "n ~= Suc(n)"; 
2608  109 
by (nat_ind_tac "n" 1); 
110 
by (ALLGOALS Asm_simp_tac); 

111 
qed "n_not_Suc_n"; 

112 

113 
bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym); 

114 

5187
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
5148
diff
changeset

115 
(*** Basic properties of "less than" ***) 
2608  116 

5069  117 
Goalw [wf_def, pred_nat_def] "wf(pred_nat)"; 
3718  118 
by (Clarify_tac 1); 
2608  119 
by (nat_ind_tac "x" 1); 
3236  120 
by (ALLGOALS Blast_tac); 
2608  121 
qed "wf_pred_nat"; 
122 

3378  123 
(*Used in TFL/post.sml*) 
5069  124 
Goalw [less_def] "(m,n) : pred_nat^+ = (m<n)"; 
3378  125 
by (rtac refl 1); 
126 
qed "less_eq"; 

127 

2608  128 
(** Introduction properties **) 
129 

5316  130 
Goalw [less_def] "[ i<j; j<k ] ==> i<(k::nat)"; 
2608  131 
by (rtac (trans_trancl RS transD) 1); 
5316  132 
by (assume_tac 1); 
133 
by (assume_tac 1); 

2608  134 
qed "less_trans"; 
135 

5069  136 
Goalw [less_def, pred_nat_def] "n < Suc(n)"; 
4089  137 
by (simp_tac (simpset() addsimps [r_into_trancl]) 1); 
2608  138 
qed "lessI"; 
139 
AddIffs [lessI]; 

140 

141 
(* i<j ==> i<Suc(j) *) 

142 
bind_thm("less_SucI", lessI RSN (2, less_trans)); 

143 

5069  144 
Goal "0 < Suc(n)"; 
2608  145 
by (nat_ind_tac "n" 1); 
146 
by (rtac lessI 1); 

147 
by (etac less_trans 1); 

148 
by (rtac lessI 1); 

149 
qed "zero_less_Suc"; 

150 
AddIffs [zero_less_Suc]; 

151 

152 
(** Elimination properties **) 

153 

5316  154 
Goalw [less_def] "n<m ==> ~ m<(n::nat)"; 
155 
by (blast_tac (claset() addIs [wf_pred_nat, wf_trancl RS wf_asym])1); 

2608  156 
qed "less_not_sym"; 
157 

5474
a2109bb8ce2b
wellformed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset

158 
(* [ n<m; ~P ==> m<n ] ==> P *) 
10231  159 
bind_thm ("less_asym", less_not_sym RS contrapos_np); 
2608  160 

5069  161 
Goalw [less_def] "~ n<(n::nat)"; 
9160  162 
by (rtac (wf_pred_nat RS wf_trancl RS wf_not_refl) 1); 
2608  163 
qed "less_not_refl"; 
164 

165 
(* n<n ==> R *) 

9160  166 
bind_thm ("less_irrefl", less_not_refl RS notE); 
5474
a2109bb8ce2b
wellformed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset

167 
AddSEs [less_irrefl]; 
2608  168 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

169 
Goal "n<m ==> m ~= (n::nat)"; 
5474
a2109bb8ce2b
wellformed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset

170 
by (Blast_tac 1); 
2608  171 
qed "less_not_refl2"; 
172 

5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

173 
(* s < t ==> s ~= t *) 
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

174 
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

175 

2608  176 

5316  177 
val major::prems = Goalw [less_def, pred_nat_def] 
2608  178 
"[ i<k; k=Suc(i) ==> P; !!j. [ i<j; k=Suc(j) ] ==> P \ 
179 
\ ] ==> P"; 

180 
by (rtac (major RS tranclE) 1); 

3236  181 
by (ALLGOALS Full_simp_tac); 
2608  182 
by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE' 
3236  183 
eresolve_tac (prems@[asm_rl, Pair_inject]))); 
2608  184 
qed "lessE"; 
185 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset

186 
Goal "~ n < (0::nat)"; 
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset

187 
by (blast_tac (claset() addEs [lessE]) 1); 
2608  188 
qed "not_less0"; 
189 
AddIffs [not_less0]; 

190 

191 
(* n<0 ==> R *) 

192 
bind_thm ("less_zeroE", not_less0 RS notE); 

193 

5316  194 
val [major,less,eq] = Goal 
2608  195 
"[ m < Suc(n); m<n ==> P; m=n ==> P ] ==> P"; 
196 
by (rtac (major RS lessE) 1); 

197 
by (rtac eq 1); 

2891  198 
by (Blast_tac 1); 
2608  199 
by (rtac less 1); 
2891  200 
by (Blast_tac 1); 
2608  201 
qed "less_SucE"; 
202 

5069  203 
Goal "(m < Suc(n)) = (m < n  m = n)"; 
4089  204 
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); 
2608  205 
qed "less_Suc_eq"; 
206 

5069  207 
Goal "(n<1) = (n=0)"; 
4089  208 
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

209 
qed "less_one"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

210 
AddIffs [less_one]; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

211 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

212 
Goal "m<n ==> Suc(m) < Suc(n)"; 
2608  213 
by (etac rev_mp 1); 
214 
by (nat_ind_tac "n" 1); 

5474
a2109bb8ce2b
wellformed asym rules; also adds less_irrefl, le_refl since order_refl
paulson
parents:
5354
diff
changeset

215 
by (ALLGOALS (fast_tac (claset() addEs [less_trans, lessE]))); 
2608  216 
qed "Suc_mono"; 
217 

218 
(*"Less than" is a linear ordering*) 

5069  219 
Goal "m<n  m=n  n<(m::nat)"; 
2608  220 
by (nat_ind_tac "m" 1); 
221 
by (nat_ind_tac "n" 1); 

222 
by (rtac (refl RS disjI1 RS disjI2) 1); 

223 
by (rtac (zero_less_Suc RS disjI1) 1); 

4089  224 
by (blast_tac (claset() addIs [Suc_mono, less_SucI] addEs [lessE]) 1); 
2608  225 
qed "less_linear"; 
226 

5069  227 
Goal "!!m::nat. (m ~= n) = (m<n  n<m)"; 
4737  228 
by (cut_facts_tac [less_linear] 1); 
5500  229 
by (Blast_tac 1); 
4737  230 
qed "nat_neq_iff"; 
231 

7030  232 
val [major,eqCase,lessCase] = Goal 
233 
"[ (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m ] ==> P n m"; 

234 
by (rtac (less_linear RS disjE) 1); 

235 
by (etac disjE 2); 

236 
by (etac lessCase 1); 

237 
by (etac (sym RS eqCase) 1); 

238 
by (etac major 1); 

239 
qed "nat_less_cases"; 

2608  240 

4745  241 

242 
(** Inductive (?) properties **) 

243 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

244 
Goal "[ m<n; Suc m ~= n ] ==> Suc(m) < n"; 
4745  245 
by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); 
246 
by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1); 

247 
qed "Suc_lessI"; 

248 

5316  249 
Goal "Suc(m) < n ==> m<n"; 
250 
by (etac rev_mp 1); 

4745  251 
by (nat_ind_tac "n" 1); 
252 
by (ALLGOALS (fast_tac (claset() addSIs [lessI RS less_SucI] 

253 
addEs [less_trans, lessE]))); 

254 
qed "Suc_lessD"; 

255 

5316  256 
val [major,minor] = Goal 
4745  257 
"[ Suc(i)<k; !!j. [ i<j; k=Suc(j) ] ==> P \ 
258 
\ ] ==> P"; 

259 
by (rtac (major RS lessE) 1); 

260 
by (etac (lessI RS minor) 1); 

261 
by (etac (Suc_lessD RS minor) 1); 

262 
by (assume_tac 1); 

263 
qed "Suc_lessE"; 

264 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

265 
Goal "Suc(m) < Suc(n) ==> m<n"; 
4745  266 
by (blast_tac (claset() addEs [lessE, make_elim Suc_lessD]) 1); 
267 
qed "Suc_less_SucD"; 

268 

269 

5069  270 
Goal "(Suc(m) < Suc(n)) = (m<n)"; 
4745  271 
by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]); 
272 
qed "Suc_less_eq"; 

8555
17325ee838ab
Suc_less_eq now with AddIffs. How could this have been overlooked?
paulson
parents:
7064
diff
changeset

273 
AddIffs [Suc_less_eq]; 
4745  274 

6109  275 
(*Goal "~(Suc(n) < n)"; 
4745  276 
by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1); 
277 
qed "not_Suc_n_less_n"; 

6109  278 
Addsimps [not_Suc_n_less_n];*) 
4745  279 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

280 
Goal "i<j ==> j<k > Suc i < k"; 
4745  281 
by (nat_ind_tac "k" 1); 
282 
by (ALLGOALS (asm_simp_tac (simpset()))); 

283 
by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); 

284 
by (blast_tac (claset() addDs [Suc_lessD]) 1); 

285 
qed_spec_mp "less_trans_Suc"; 

286 

2608  287 
(*Can be used with less_Suc_eq to get n=m  n<m *) 
5069  288 
Goal "(~ m < n) = (n < Suc(m))"; 
2608  289 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
290 
by (ALLGOALS Asm_simp_tac); 

291 
qed "not_less_eq"; 

292 

293 
(*Complete induction, aka courseofvalues induction*) 

5316  294 
val prems = Goalw [less_def] 
9160  295 
"[ !!n. [ ALL m::nat. m<n > P(m) ] ==> P(n) ] ==> P(n)"; 
2608  296 
by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); 
297 
by (eresolve_tac prems 1); 

9870  298 
qed "nat_less_induct"; 
2608  299 

300 
(*** Properties of <= ***) 

301 

5500  302 
(*Was le_eq_less_Suc, but this orientation is more useful*) 
303 
Goalw [le_def] "(m < Suc n) = (m <= n)"; 

304 
by (rtac (not_less_eq RS sym) 1); 

305 
qed "less_Suc_eq_le"; 

2608  306 

3343  307 
(* m<=n ==> m < Suc n *) 
5500  308 
bind_thm ("le_imp_less_Suc", less_Suc_eq_le RS iffD2); 
3343  309 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset

310 
Goalw [le_def] "(0::nat) <= n"; 
2608  311 
by (rtac not_less0 1); 
312 
qed "le0"; 

6075  313 
AddIffs [le0]; 
2608  314 

5069  315 
Goalw [le_def] "~ Suc n <= n"; 
2608  316 
by (Simp_tac 1); 
317 
qed "Suc_n_not_le_n"; 

318 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8741
diff
changeset

319 
Goalw [le_def] "!!i::nat. (i <= 0) = (i = 0)"; 
2608  320 
by (nat_ind_tac "i" 1); 
321 
by (ALLGOALS Asm_simp_tac); 

322 
qed "le_0_eq"; 

4614  323 
AddIffs [le_0_eq]; 
2608  324 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

325 
Goal "(m <= Suc(n)) = (m<=n  m = Suc n)"; 
5500  326 
by (simp_tac (simpset() delsimps [less_Suc_eq_le] 
327 
addsimps [less_Suc_eq_le RS sym, less_Suc_eq]) 1); 

3355  328 
qed "le_Suc_eq"; 
329 

4614  330 
(* [ m <= Suc n; m <= n ==> R; m = Suc n ==> R ] ==> R *) 
331 
bind_thm ("le_SucE", le_Suc_eq RS iffD1 RS disjE); 

332 

5316  333 
Goalw [le_def] "~n<m ==> m<=(n::nat)"; 
334 
by (assume_tac 1); 

2608  335 
qed "leI"; 
336 

5316  337 
Goalw [le_def] "m<=n ==> ~ n < (m::nat)"; 
338 
by (assume_tac 1); 

2608  339 
qed "leD"; 
340 

9108  341 
bind_thm ("leE", make_elim leD); 
2608  342 

5069  343 
Goal "(~n<m) = (m<=(n::nat))"; 
4089  344 
by (blast_tac (claset() addIs [leI] addEs [leE]) 1); 
2608  345 
qed "not_less_iff_le"; 
346 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

347 
Goalw [le_def] "~ m <= n ==> n<(m::nat)"; 
2891  348 
by (Blast_tac 1); 
2608  349 
qed "not_leE"; 
350 

5069  351 
Goalw [le_def] "(~n<=m) = (m<(n::nat))"; 
4599  352 
by (Simp_tac 1); 
353 
qed "not_le_iff_less"; 

354 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

355 
Goalw [le_def] "m < n ==> Suc(m) <= n"; 
4089  356 
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
357 
by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1); 

3343  358 
qed "Suc_leI"; (*formerly called lessD*) 
2608  359 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

360 
Goalw [le_def] "Suc(m) <= n ==> m <= n"; 
4089  361 
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
2608  362 
qed "Suc_leD"; 
363 

364 
(* stronger version of Suc_leD *) 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

365 
Goalw [le_def] "Suc m <= n ==> m < n"; 
4089  366 
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
2608  367 
by (cut_facts_tac [less_linear] 1); 
2891  368 
by (Blast_tac 1); 
2608  369 
qed "Suc_le_lessD"; 
370 

5069  371 
Goal "(Suc m <= n) = (m < n)"; 
4089  372 
by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1); 
2608  373 
qed "Suc_le_eq"; 
374 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

375 
Goalw [le_def] "m <= n ==> m <= Suc n"; 
4089  376 
by (blast_tac (claset() addDs [Suc_lessD]) 1); 
2608  377 
qed "le_SucI"; 
378 

6109  379 
(*bind_thm ("le_Suc", not_Suc_n_less_n RS leI);*) 
2608  380 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

381 
Goalw [le_def] "m < n ==> m <= (n::nat)"; 
4089  382 
by (blast_tac (claset() addEs [less_asym]) 1); 
2608  383 
qed "less_imp_le"; 
384 

5591  385 
(*For instance, (Suc m < Suc n) = (Suc m <= n) = (m<n) *) 
9108  386 
bind_thms ("le_simps", [less_imp_le, less_Suc_eq_le, Suc_le_eq]); 
5591  387 

5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

388 

3343  389 
(** Equivalence of m<=n and m<n  m=n **) 
390 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

391 
Goalw [le_def] "m <= n ==> m < n  m=(n::nat)"; 
2608  392 
by (cut_facts_tac [less_linear] 1); 
4089  393 
by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1); 
2608  394 
qed "le_imp_less_or_eq"; 
395 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

396 
Goalw [le_def] "m<n  m=n ==> m <=(n::nat)"; 
2608  397 
by (cut_facts_tac [less_linear] 1); 
4089  398 
by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1); 
2608  399 
qed "less_or_eq_imp_le"; 
400 

5069  401 
Goal "(m <= (n::nat)) = (m < n  m=n)"; 
2608  402 
by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); 
403 
qed "le_eq_less_or_eq"; 

404 

4635  405 
(*Useful with Blast_tac. m=n ==> m<=n *) 
406 
bind_thm ("eq_imp_le", disjI2 RS less_or_eq_imp_le); 

407 

5069  408 
Goal "n <= (n::nat)"; 
4089  409 
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); 
2608  410 
qed "le_refl"; 
411 

5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

412 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

413 
Goal "[ i <= j; j < k ] ==> i < (k::nat)"; 
4468  414 
by (blast_tac (claset() addSDs [le_imp_less_or_eq] 
415 
addIs [less_trans]) 1); 

2608  416 
qed "le_less_trans"; 
417 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

418 
Goal "[ i < j; j <= k ] ==> i < (k::nat)"; 
4468  419 
by (blast_tac (claset() addSDs [le_imp_less_or_eq] 
420 
addIs [less_trans]) 1); 

2608  421 
qed "less_le_trans"; 
422 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

423 
Goal "[ i <= j; j <= k ] ==> i <= (k::nat)"; 
4468  424 
by (blast_tac (claset() addSDs [le_imp_less_or_eq] 
425 
addIs [less_or_eq_imp_le, less_trans]) 1); 

2608  426 
qed "le_trans"; 
427 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

428 
Goal "[ m <= n; n <= m ] ==> m = (n::nat)"; 
4468  429 
(*order_less_irrefl could make this proof fail*) 
430 
by (blast_tac (claset() addSDs [le_imp_less_or_eq] 

431 
addSEs [less_irrefl] addEs [less_asym]) 1); 

2608  432 
qed "le_anti_sym"; 
433 

5069  434 
Goal "(Suc(n) <= Suc(m)) = (n <= m)"; 
5500  435 
by (simp_tac (simpset() addsimps le_simps) 1); 
2608  436 
qed "Suc_le_mono"; 
437 

438 
AddIffs [Suc_le_mono]; 

439 

5500  440 
(* Axiom 'order_less_le' of class 'order': *) 
5069  441 
Goal "(m::nat) < n = (m <= n & m ~= n)"; 
4737  442 
by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1); 
443 
by (blast_tac (claset() addSEs [less_asym]) 1); 

2608  444 
qed "nat_less_le"; 
445 

5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

446 
(* [ m <= n; m ~= n ] ==> m < n *) 
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

447 
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

448 

4640  449 
(* Axiom 'linorder_linear' of class 'linorder': *) 
5069  450 
Goal "(m::nat) <= n  n <= m"; 
4640  451 
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); 
452 
by (cut_facts_tac [less_linear] 1); 

5132  453 
by (Blast_tac 1); 
4640  454 
qed "nat_le_linear"; 
455 

5354
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

456 
Goal "~ n < m ==> (n < Suc m) = (n = m)"; 
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

457 
by (blast_tac (claset() addSEs [less_SucE]) 1); 
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

458 
qed "not_less_less_Suc_eq"; 
da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

459 

da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

460 

da63d9b35caf
new theorems; adds [le_refl, less_imp_le] as simprules
paulson
parents:
5316
diff
changeset

461 
(*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

462 
Not suitable as default simprules because they often lead to looping*) 
9108  463 
bind_thms ("not_less_simps", [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq]); 
4640  464 

2608  465 
(** LEAST  the least number operator **) 
466 

9160  467 
Goal "(ALL m::nat. P m > n <= m) = (ALL m. m < n > ~ P m)"; 
4089  468 
by (blast_tac (claset() addIs [leI] addEs [leE]) 1); 
3143
d60e49b86c6a
Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents:
3085
diff
changeset

469 
val lemma = result(); 
d60e49b86c6a
Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents:
3085
diff
changeset

470 

d60e49b86c6a
Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents:
3085
diff
changeset

471 
(* This is an old def of Least for nat, which is derived for compatibility *) 
5069  472 
Goalw [Least_def] 
3143
d60e49b86c6a
Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents:
3085
diff
changeset

473 
"(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n > ~P(m)))"; 
4089  474 
by (simp_tac (simpset() addsimps [lemma]) 1); 
3143
d60e49b86c6a
Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents:
3085
diff
changeset

475 
qed "Least_nat_def"; 
d60e49b86c6a
Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents:
3085
diff
changeset

476 

5316  477 
val [prem1,prem2] = Goalw [Least_nat_def] 
3842  478 
"[ P(k::nat); !!x. x<k ==> ~P(x) ] ==> (LEAST x. P(x)) = k"; 
9969  479 
by (rtac some_equality 1); 
4089  480 
by (blast_tac (claset() addSIs [prem1,prem2]) 1); 
2608  481 
by (cut_facts_tac [less_linear] 1); 
4089  482 
by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1); 
2608  483 
qed "Least_equality"; 
484 

5316  485 
Goal "P(k::nat) ==> P(LEAST x. P(x))"; 
486 
by (etac rev_mp 1); 

9870  487 
by (res_inst_tac [("n","k")] nat_less_induct 1); 
2608  488 
by (rtac impI 1); 
489 
by (rtac classical 1); 

490 
by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); 

491 
by (assume_tac 1); 

492 
by (assume_tac 2); 

2891  493 
by (Blast_tac 1); 
2608  494 
qed "LeastI"; 
495 

496 
(*Proof is almost identical to the one above!*) 

5316  497 
Goal "P(k::nat) ==> (LEAST x. P(x)) <= k"; 
498 
by (etac rev_mp 1); 

9870  499 
by (res_inst_tac [("n","k")] nat_less_induct 1); 
2608  500 
by (rtac impI 1); 
501 
by (rtac classical 1); 

502 
by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); 

503 
by (assume_tac 1); 

504 
by (rtac le_refl 2); 

4089  505 
by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1); 
2608  506 
qed "Least_le"; 
507 

5316  508 
Goal "k < (LEAST x. P(x)) ==> ~P(k::nat)"; 
2608  509 
by (rtac notI 1); 
5316  510 
by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1); 
2608  511 
qed "not_less_Least"; 
512 

5983  513 
(* [ m ~= n; m < n ==> P; n < m ==> P ] ==> P *) 
4737  514 
bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE); 
7064  515 

9160  516 
Goal "(S::nat set) ~= {} ==> EX x:S. ALL y:S. x <= y"; 
7064  517 
by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1); 
518 
by (dres_inst_tac [("x","S")] spec 1); 

519 
by (Asm_full_simp_tac 1); 

520 
by (etac impE 1); 

521 
by (Force_tac 1); 

522 
by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1); 

523 
qed "nonempty_has_least"; 