author  berghofe 
Fri, 21 Jun 1996 13:51:09 +0200  
changeset 1823  e1458e1a9f80 
parent 1817  3994d37b16ae 
child 1824  44254696843a 
permissions  rwrr 
1465  1 
(* Title: HOL/nat 
923  2 
ID: $Id$ 
1465  3 
Author: Tobias Nipkow, Cambridge University Computer Laboratory 
923  4 
Copyright 1991 University of Cambridge 
5 

6 
For nat.thy. Type nat is defined as a set (Nat) over the type ind. 

7 
*) 

8 

9 
open Nat; 

10 

11 
goal Nat.thy "mono(%X. {Zero_Rep} Un (Suc_Rep``X))"; 

12 
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1)); 

13 
qed "Nat_fun_mono"; 

14 

15 
val Nat_unfold = Nat_fun_mono RS (Nat_def RS def_lfp_Tarski); 

16 

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

18 
goal Nat.thy "Zero_Rep: Nat"; 

19 
by (rtac (Nat_unfold RS ssubst) 1); 

20 
by (rtac (singletonI RS UnI1) 1); 

21 
qed "Zero_RepI"; 

22 

23 
val prems = goal Nat.thy "i: Nat ==> Suc_Rep(i) : Nat"; 

24 
by (rtac (Nat_unfold RS ssubst) 1); 

25 
by (rtac (imageI RS UnI2) 1); 

26 
by (resolve_tac prems 1); 

27 
qed "Suc_RepI"; 

28 

29 
(*** Induction ***) 

30 

31 
val major::prems = goal Nat.thy 

32 
"[ i: Nat; P(Zero_Rep); \ 

33 
\ !!j. [ j: Nat; P(j) ] ==> P(Suc_Rep(j)) ] ==> P(i)"; 

34 
by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

35 
by (fast_tac (!claset addIs prems) 1); 
923  36 
qed "Nat_induct"; 
37 

38 
val prems = goalw Nat.thy [Zero_def,Suc_def] 

39 
"[ P(0); \ 

40 
\ !!k. P(k) ==> P(Suc(k)) ] ==> P(n)"; 

41 
by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*) 

42 
by (rtac (Rep_Nat RS Nat_induct) 1); 

43 
by (REPEAT (ares_tac prems 1 

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

45 
qed "nat_induct"; 

46 

47 
(*Perform induction on n. *) 

48 
fun nat_ind_tac a i = 

49 
EVERY [res_inst_tac [("n",a)] nat_induct i, 

1465  50 
rename_last_tac a ["1"] (i+1)]; 
923  51 

52 
(*A special form of induction for reasoning about m<n and mn*) 

53 
val prems = goal Nat.thy 

54 
"[ !!x. P x 0; \ 

55 
\ !!y. P 0 (Suc y); \ 

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

57 
\ ] ==> P m n"; 

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

59 
by (nat_ind_tac "n" 1); 

60 
by (rtac allI 2); 

61 
by (nat_ind_tac "x" 2); 

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

63 
qed "diff_induct"; 

64 

65 
(*Case analysis on the natural numbers*) 

66 
val prems = goal Nat.thy 

67 
"[ n=0 ==> P; !!x. n = Suc(x) ==> P ] ==> P"; 

68 
by (subgoal_tac "n=0  (EX x. n = Suc(x))" 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

69 
by (fast_tac (!claset addSEs prems) 1); 
923  70 
by (nat_ind_tac "n" 1); 
71 
by (rtac (refl RS disjI1) 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

72 
by (Fast_tac 1); 
923  73 
qed "natE"; 
74 

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

76 

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

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

79 

80 
goal Nat.thy "inj(Rep_Nat)"; 

81 
by (rtac inj_inverseI 1); 

82 
by (rtac Rep_Nat_inverse 1); 

83 
qed "inj_Rep_Nat"; 

84 

85 
goal Nat.thy "inj_onto Abs_Nat Nat"; 

86 
by (rtac inj_onto_inverseI 1); 

87 
by (etac Abs_Nat_inverse 1); 

88 
qed "inj_onto_Abs_Nat"; 

89 

90 
(*** Distinctness of constructors ***) 

91 

92 
goalw Nat.thy [Zero_def,Suc_def] "Suc(m) ~= 0"; 

93 
by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1); 

94 
by (rtac Suc_Rep_not_Zero_Rep 1); 

95 
by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1)); 

96 
qed "Suc_not_Zero"; 

97 

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

99 

1301  100 
Addsimps [Suc_not_Zero,Zero_not_Suc]; 
101 

923  102 
bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE)); 
103 
val Zero_neq_Suc = sym RS Suc_neq_Zero; 

104 

105 
(** Injectiveness of Suc **) 

106 

107 
goalw Nat.thy [Suc_def] "inj(Suc)"; 

108 
by (rtac injI 1); 

109 
by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1); 

110 
by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1)); 

111 
by (dtac (inj_Suc_Rep RS injD) 1); 

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

113 
qed "inj_Suc"; 

114 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1024
diff
changeset

115 
val Suc_inject = inj_Suc RS injD; 
923  116 

117 
goal Nat.thy "(Suc(m)=Suc(n)) = (m=n)"; 

118 
by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 

119 
qed "Suc_Suc_eq"; 

120 

121 
goal Nat.thy "n ~= Suc(n)"; 

122 
by (nat_ind_tac "n" 1); 

1301  123 
by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq]))); 
923  124 
qed "n_not_Suc_n"; 
125 

1618  126 
bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym); 
923  127 

128 
(*** nat_case  the selection operator for nat ***) 

129 

130 
goalw Nat.thy [nat_case_def] "nat_case a f 0 = a"; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

131 
by (fast_tac (!claset addIs [select_equality] addEs [Zero_neq_Suc]) 1); 
923  132 
qed "nat_case_0"; 
133 

134 
goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)"; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

135 
by (fast_tac (!claset addIs [select_equality] 
1465  136 
addEs [make_elim Suc_inject, Suc_neq_Zero]) 1); 
923  137 
qed "nat_case_Suc"; 
138 

139 
(** Introduction rules for 'pred_nat' **) 

140 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
962
diff
changeset

141 
goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat"; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

142 
by (Fast_tac 1); 
923  143 
qed "pred_natI"; 
144 

145 
val major::prems = goalw Nat.thy [pred_nat_def] 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
962
diff
changeset

146 
"[ p : pred_nat; !!x n. [ p = (n, Suc(n)) ] ==> R \ 
923  147 
\ ] ==> R"; 
148 
by (rtac (major RS CollectE) 1); 

149 
by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1)); 

150 
qed "pred_natE"; 

151 

152 
goalw Nat.thy [wf_def] "wf(pred_nat)"; 

153 
by (strip_tac 1); 

154 
by (nat_ind_tac "x" 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

155 
by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, 
1465  156 
make_elim Suc_inject]) 2); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

157 
by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1); 
923  158 
qed "wf_pred_nat"; 
159 

160 

161 
(*** nat_rec  by wf recursion on pred_nat ***) 

162 

1475  163 
(* The unrolling rule for nat_rec *) 
164 
goal Nat.thy 

165 
"(%n. nat_rec n c d) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))"; 

166 
by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1); 

167 
bind_thm("nat_rec_unfold", wf_pred_nat RS 

168 
((result() RS eq_reflection) RS def_wfrec)); 

169 

170 
(* 

171 
* Old: 

172 
* bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); 

173 
**) 

923  174 

175 
(** conversion rules **) 

176 

177 
goal Nat.thy "nat_rec 0 c h = c"; 

178 
by (rtac (nat_rec_unfold RS trans) 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1024
diff
changeset

179 
by (simp_tac (!simpset addsimps [nat_case_0]) 1); 
923  180 
qed "nat_rec_0"; 
181 

182 
goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)"; 

183 
by (rtac (nat_rec_unfold RS trans) 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1024
diff
changeset

184 
by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1); 
923  185 
qed "nat_rec_Suc"; 
186 

187 
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) 

188 
val [rew] = goal Nat.thy 

189 
"[ !!n. f(n) == nat_rec n c h ] ==> f(0) = c"; 

190 
by (rewtac rew); 

191 
by (rtac nat_rec_0 1); 

192 
qed "def_nat_rec_0"; 

193 

194 
val [rew] = goal Nat.thy 

195 
"[ !!n. f(n) == nat_rec n c h ] ==> f(Suc(n)) = h n (f n)"; 

196 
by (rewtac rew); 

197 
by (rtac nat_rec_Suc 1); 

198 
qed "def_nat_rec_Suc"; 

199 

200 
fun nat_recs def = 

201 
[standard (def RS def_nat_rec_0), 

202 
standard (def RS def_nat_rec_Suc)]; 

203 

204 

205 
(*** Basic properties of "less than" ***) 

206 

207 
(** Introduction properties **) 

208 

209 
val prems = goalw Nat.thy [less_def] "[ i<j; j<k ] ==> i<(k::nat)"; 

210 
by (rtac (trans_trancl RS transD) 1); 

211 
by (resolve_tac prems 1); 

212 
by (resolve_tac prems 1); 

213 
qed "less_trans"; 

214 

215 
goalw Nat.thy [less_def] "n < Suc(n)"; 

216 
by (rtac (pred_natI RS r_into_trancl) 1); 

217 
qed "lessI"; 

1301  218 
Addsimps [lessI]; 
923  219 

1618  220 
(* i<j ==> i<Suc(j) *) 
923  221 
val less_SucI = lessI RSN (2, less_trans); 
222 

223 
goal Nat.thy "0 < Suc(n)"; 

224 
by (nat_ind_tac "n" 1); 

225 
by (rtac lessI 1); 

226 
by (etac less_trans 1); 

227 
by (rtac lessI 1); 

228 
qed "zero_less_Suc"; 

1301  229 
Addsimps [zero_less_Suc]; 
923  230 

231 
(** Elimination properties **) 

232 

233 
val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)"; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

234 
by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); 
923  235 
qed "less_not_sym"; 
236 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
962
diff
changeset

237 
(* [ n(m; m(n ] ==> R *) 
923  238 
bind_thm ("less_asym", (less_not_sym RS notE)); 
239 

240 
goalw Nat.thy [less_def] "~ n<(n::nat)"; 

241 
by (rtac notI 1); 

1618  242 
by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1); 
923  243 
qed "less_not_refl"; 
244 

1817  245 
(* n<n ==> R *) 
1618  246 
bind_thm ("less_irrefl", (less_not_refl RS notE)); 
923  247 

248 
goal Nat.thy "!!m. n<m ==> m ~= (n::nat)"; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

249 
by (fast_tac (!claset addEs [less_irrefl]) 1); 
923  250 
qed "less_not_refl2"; 
251 

252 

253 
val major::prems = goalw Nat.thy [less_def] 

254 
"[ i<k; k=Suc(i) ==> P; !!j. [ i<j; k=Suc(j) ] ==> P \ 

255 
\ ] ==> P"; 

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

1024  257 
by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE' 
1465  258 
eresolve_tac (prems@[pred_natE, Pair_inject]))); 
1024  259 
by (rtac refl 1); 
923  260 
qed "lessE"; 
261 

262 
goal Nat.thy "~ n<0"; 

263 
by (rtac notI 1); 

264 
by (etac lessE 1); 

265 
by (etac Zero_neq_Suc 1); 

266 
by (etac Zero_neq_Suc 1); 

267 
qed "not_less0"; 

1301  268 
Addsimps [not_less0]; 
923  269 

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

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

272 

273 
val [major,less,eq] = goal Nat.thy 

274 
"[ m < Suc(n); m<n ==> P; m=n ==> P ] ==> P"; 

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

276 
by (rtac eq 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

277 
by (fast_tac (!claset addSDs [Suc_inject]) 1); 
923  278 
by (rtac less 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

279 
by (fast_tac (!claset addSDs [Suc_inject]) 1); 
923  280 
qed "less_SucE"; 
281 

282 
goal Nat.thy "(m < Suc(n)) = (m < n  m = n)"; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

283 
by (fast_tac (!claset addSIs [lessI] 
1465  284 
addEs [less_trans, less_SucE]) 1); 
923  285 
qed "less_Suc_eq"; 
286 

1301  287 
val prems = goal Nat.thy "m<n ==> n ~= 0"; 
1552  288 
by (res_inst_tac [("n","n")] natE 1); 
289 
by (cut_facts_tac prems 1); 

290 
by (ALLGOALS Asm_full_simp_tac); 

1301  291 
qed "gr_implies_not0"; 
292 
Addsimps [gr_implies_not0]; 

923  293 

1660  294 
qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [ 
295 
rtac iffI 1, 

296 
etac gr_implies_not0 1, 

297 
rtac natE 1, 

298 
contr_tac 1, 

299 
etac ssubst 1, 

300 
rtac zero_less_Suc 1]); 

301 

923  302 
(** Inductive (?) properties **) 
303 

304 
val [prem] = goal Nat.thy "Suc(m) < n ==> m<n"; 

305 
by (rtac (prem RS rev_mp) 1); 

306 
by (nat_ind_tac "n" 1); 

307 
by (rtac impI 1); 

308 
by (etac less_zeroE 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

309 
by (fast_tac (!claset addSIs [lessI RS less_SucI] 
1465  310 
addSDs [Suc_inject] 
311 
addEs [less_trans, lessE]) 1); 

923  312 
qed "Suc_lessD"; 
313 

314 
val [major,minor] = goal Nat.thy 

315 
"[ Suc(i)<k; !!j. [ i<j; k=Suc(j) ] ==> P \ 

316 
\ ] ==> P"; 

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

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

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

320 
by (assume_tac 1); 

321 
qed "Suc_lessE"; 

322 

323 
val [major] = goal Nat.thy "Suc(m) < Suc(n) ==> m<n"; 

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

325 
by (REPEAT (rtac lessI 1 

326 
ORELSE eresolve_tac [make_elim Suc_inject, ssubst, Suc_lessD] 1)); 

327 
qed "Suc_less_SucD"; 

328 

329 
val prems = goal Nat.thy "m<n ==> Suc(m) < Suc(n)"; 

330 
by (subgoal_tac "m<n > Suc(m) < Suc(n)" 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

331 
by (fast_tac (!claset addIs prems) 1); 
923  332 
by (nat_ind_tac "n" 1); 
333 
by (rtac impI 1); 

334 
by (etac less_zeroE 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

335 
by (fast_tac (!claset addSIs [lessI] 
1465  336 
addSDs [Suc_inject] 
337 
addEs [less_trans, lessE]) 1); 

923  338 
qed "Suc_mono"; 
339 

1672
2c109cd2fdd0
repaired critical proofs depending on the order inside nonconfluent SimpSets,
oheimb
parents:
1660
diff
changeset

340 

923  341 
goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)"; 
342 
by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]); 

343 
qed "Suc_less_eq"; 

1301  344 
Addsimps [Suc_less_eq]; 
923  345 

346 
goal Nat.thy "~(Suc(n) < n)"; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

347 
by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1); 
923  348 
qed "not_Suc_n_less_n"; 
1301  349 
Addsimps [not_Suc_n_less_n]; 
350 

351 
goal Nat.thy "!!i. i<j ==> j<k > Suc i < k"; 

1552  352 
by (nat_ind_tac "k" 1); 
1660  353 
by (ALLGOALS (asm_simp_tac (!simpset))); 
354 
by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

355 
by (fast_tac (!claset addDs [Suc_lessD]) 1); 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

356 
qed_spec_mp "less_trans_Suc"; 
923  357 

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

359 
goal Nat.thy "m<n  m=n  n<(m::nat)"; 

360 
by (nat_ind_tac "m" 1); 

361 
by (nat_ind_tac "n" 1); 

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

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

364 
by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1); 
923  365 
qed "less_linear"; 
366 

1660  367 
qed_goal "nat_less_cases" Nat.thy 
368 
"[ (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m ] ==> P n m" 

369 
( fn prems => 

370 
[ 

371 
(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1), 

372 
(etac disjE 2), 

373 
(etac (hd (tl (tl prems))) 1), 

374 
(etac (sym RS hd (tl prems)) 1), 

375 
(etac (hd prems) 1) 

376 
]); 

377 

923  378 
(*Can be used with less_Suc_eq to get n=m  n<m *) 
379 
goal Nat.thy "(~ m < n) = (n < Suc(m))"; 

380 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 

1552  381 
by (ALLGOALS Asm_simp_tac); 
923  382 
qed "not_less_eq"; 
383 

384 
(*Complete induction, aka courseofvalues induction*) 

385 
val prems = goalw Nat.thy [less_def] 

386 
"[ !!n. [ ! m::nat. m<n > P(m) ] ==> P(n) ] ==> P(n)"; 

387 
by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); 

388 
by (eresolve_tac prems 1); 

389 
qed "less_induct"; 

390 

391 

392 
(*** Properties of <= ***) 

393 

394 
goalw Nat.thy [le_def] "0 <= n"; 

395 
by (rtac not_less0 1); 

396 
qed "le0"; 

397 

1301  398 
goalw Nat.thy [le_def] "~ Suc n <= n"; 
1552  399 
by (Simp_tac 1); 
1301  400 
qed "Suc_n_not_le_n"; 
401 

402 
goalw Nat.thy [le_def] "(i <= 0) = (i = 0)"; 

1552  403 
by (nat_ind_tac "i" 1); 
404 
by (ALLGOALS Asm_simp_tac); 

1777
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

405 
qed "le_0_eq"; 
1301  406 

407 
Addsimps [less_not_refl, 

1777
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

408 
(*less_Suc_eq, makes simpset nonconfluent*) le0, le_0_eq, 
1301  409 
Suc_Suc_eq, Suc_n_not_le_n, 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1024
diff
changeset

410 
n_not_Suc_n, Suc_n_not_n, 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1024
diff
changeset

411 
nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; 
923  412 

1777
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

413 
(* 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

414 
goal Nat.thy "(Suc m < n  Suc m = n) = (m < n)"; 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

415 
by(stac (less_Suc_eq RS sym) 1); 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

416 
by(rtac Suc_less_eq 1); 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

417 
qed "Suc_le_eq"; 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

418 

47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

419 
this could make the simpset (with less_Suc_eq added again) more confluent, 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

420 
but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...) 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

421 
*) 
47c47b7d7aa8
renamed le_0 to le_0_eq, to avoid confusion with le0,
oheimb
parents:
1760
diff
changeset

422 

923  423 
(*Prevents simplification of f and g: much faster*) 
424 
qed_goal "nat_case_weak_cong" Nat.thy 

425 
"m=n ==> nat_case a f m = nat_case a f n" 

426 
(fn [prem] => [rtac (prem RS arg_cong) 1]); 

427 

428 
qed_goal "nat_rec_weak_cong" Nat.thy 

429 
"m=n ==> nat_rec m a f = nat_rec n a f" 

430 
(fn [prem] => [rtac (prem RS arg_cong) 1]); 

431 

1618  432 
val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)"; 
923  433 
by (resolve_tac prems 1); 
434 
qed "leI"; 

435 

1618  436 
val prems = goalw Nat.thy [le_def] "m<=n ==> ~ n < (m::nat)"; 
923  437 
by (resolve_tac prems 1); 
438 
qed "leD"; 

439 

440 
val leE = make_elim leD; 

441 

1618  442 
goal Nat.thy "(~n<m) = (m<=(n::nat))"; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

443 
by (fast_tac (!claset addIs [leI] addEs [leE]) 1); 
1618  444 
qed "not_less_iff_le"; 
445 

923  446 
goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)"; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

447 
by (Fast_tac 1); 
923  448 
qed "not_leE"; 
449 

450 
goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n"; 

1660  451 
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

452 
by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); 
923  453 
qed "lessD"; 
454 

455 
goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; 

1660  456 
by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

457 
by (Fast_tac 1); 
923  458 
qed "Suc_leD"; 
459 

1817  460 
(* stronger version of Suc_leD *) 
461 
goalw Nat.thy [le_def] 

462 
"!!m. Suc m <= n ==> m < n"; 

463 
by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); 

464 
by (cut_facts_tac [less_linear] 1); 

1823  465 
by (Fast_tac 1); 
1817  466 
qed "Suc_le_lessD"; 
467 

468 
goal Nat.thy "(Suc m <= n) = (m < n)"; 

469 
by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1); 

470 
qed "Suc_le_eq"; 

471 

1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

472 
goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n"; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

473 
by (fast_tac (!claset addDs [Suc_lessD]) 1); 
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

474 
qed "le_SucI"; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

475 
Addsimps[le_SucI]; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

476 

923  477 
goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)"; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

478 
by (fast_tac (!claset addEs [less_asym]) 1); 
923  479 
qed "less_imp_le"; 
480 

481 
goalw Nat.thy [le_def] "!!m. m <= n ==> m < n  m=(n::nat)"; 

482 
by (cut_facts_tac [less_linear] 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

483 
by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); 
923  484 
qed "le_imp_less_or_eq"; 
485 

486 
goalw Nat.thy [le_def] "!!m. m<n  m=n ==> m <=(n::nat)"; 

487 
by (cut_facts_tac [less_linear] 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

488 
by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); 
923  489 
by (flexflex_tac); 
490 
qed "less_or_eq_imp_le"; 

491 

492 
goal Nat.thy "(x <= (y::nat)) = (x < y  x=y)"; 

493 
by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); 

494 
qed "le_eq_less_or_eq"; 

495 

496 
goal Nat.thy "n <= (n::nat)"; 

1552  497 
by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); 
923  498 
qed "le_refl"; 
499 

500 
val prems = goal Nat.thy "!!i. [ i <= j; j < k ] ==> i < (k::nat)"; 

501 
by (dtac le_imp_less_or_eq 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

502 
by (fast_tac (!claset addIs [less_trans]) 1); 
923  503 
qed "le_less_trans"; 
504 

505 
goal Nat.thy "!!i. [ i < j; j <= k ] ==> i < (k::nat)"; 

506 
by (dtac le_imp_less_or_eq 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

507 
by (fast_tac (!claset addIs [less_trans]) 1); 
923  508 
qed "less_le_trans"; 
509 

510 
goal Nat.thy "!!i. [ i <= j; j <= k ] ==> i <= (k::nat)"; 

511 
by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

512 
rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]); 
923  513 
qed "le_trans"; 
514 

515 
val prems = goal Nat.thy "!!m. [ m <= n; n <= m ] ==> m = (n::nat)"; 

516 
by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

517 
fast_tac (!claset addEs [less_irrefl,less_asym])]); 
923  518 
qed "le_anti_sym"; 
519 

520 
goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)"; 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1024
diff
changeset

521 
by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); 
923  522 
qed "Suc_le_mono"; 
523 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1024
diff
changeset

524 
Addsimps [le_refl,Suc_le_mono]; 
1531  525 

526 

527 
(** LEAST  the least number operator **) 

528 

529 
val [prem1,prem2] = goalw Nat.thy [Least_def] 

530 
"[ P(k); !!x. x<k ==> ~P(x) ] ==> (LEAST x.P(x)) = k"; 

531 
by (rtac select_equality 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

532 
by (fast_tac (!claset addSIs [prem1,prem2]) 1); 
1531  533 
by (cut_facts_tac [less_linear] 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

534 
by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1); 
1531  535 
qed "Least_equality"; 
536 

537 
val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))"; 

538 
by (rtac (prem RS rev_mp) 1); 

539 
by (res_inst_tac [("n","k")] less_induct 1); 

540 
by (rtac impI 1); 

541 
by (rtac classical 1); 

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

543 
by (assume_tac 1); 

544 
by (assume_tac 2); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

545 
by (Fast_tac 1); 
1531  546 
qed "LeastI"; 
547 

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

549 
val [prem] = goal Nat.thy "P(k) ==> (LEAST x.P(x)) <= k"; 

550 
by (rtac (prem RS rev_mp) 1); 

551 
by (res_inst_tac [("n","k")] less_induct 1); 

552 
by (rtac impI 1); 

553 
by (rtac classical 1); 

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

555 
by (assume_tac 1); 

556 
by (rtac le_refl 2); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

557 
by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1); 
1531  558 
qed "Least_le"; 
559 

560 
val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)"; 

561 
by (rtac notI 1); 

562 
by (etac (rewrite_rule [le_def] Least_le RS notE) 1); 

563 
by (rtac prem 1); 

564 
qed "not_less_Least"; 

1660  565 

566 
qed_goalw "Least_Suc" Nat.thy [Least_def] 

567 
"[ ? n. P (Suc n); ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P (Suc m))" 

568 
(fn prems => [ 

569 
cut_facts_tac prems 1, 

570 
rtac select_equality 1, 

571 
fold_goals_tac [Least_def], 

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1777
diff
changeset

572 
safe_tac (!claset addSEs [LeastI]), 
1660  573 
res_inst_tac [("n","j")] natE 1, 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

574 
Fast_tac 1, 
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

575 
fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1, 
1660  576 
res_inst_tac [("n","k")] natE 1, 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

577 
Fast_tac 1, 
1660  578 
hyp_subst_tac 1, 
579 
rewtac Least_def, 

580 
rtac (select_equality RS arg_cong RS sym) 1, 

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1777
diff
changeset

581 
safe_tac (!claset), 
1660  582 
dtac Suc_mono 1, 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

583 
Fast_tac 1, 
1660  584 
cut_facts_tac [less_linear] 1, 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1777
diff
changeset

585 
safe_tac (!claset), 
1660  586 
atac 2, 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

587 
Fast_tac 2, 
1660  588 
dtac Suc_mono 1, 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1679
diff
changeset

589 
Fast_tac 1]); 