1 (* Title: HOL/Nat.ML |
1 (* Title: HOL/Nat.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1997 TU Muenchen |
4 Copyright 1997 TU Muenchen |
5 *) |
5 *) |
|
6 |
|
7 (** conversion rules for nat_rec **) |
|
8 |
|
9 val [nat_rec_0, nat_rec_Suc] = nat.recs; |
|
10 |
|
11 (*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) |
|
12 val prems = goal thy |
|
13 "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c"; |
|
14 by (simp_tac (simpset() addsimps prems) 1); |
|
15 qed "def_nat_rec_0"; |
|
16 |
|
17 val prems = goal thy |
|
18 "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)"; |
|
19 by (simp_tac (simpset() addsimps prems) 1); |
|
20 qed "def_nat_rec_Suc"; |
|
21 |
|
22 val [nat_case_0, nat_case_Suc] = nat.cases; |
|
23 |
|
24 Goal "n ~= 0 ==> EX m. n = Suc m"; |
|
25 by (exhaust_tac "n" 1); |
|
26 by (REPEAT (Blast_tac 1)); |
|
27 qed "not0_implies_Suc"; |
|
28 |
|
29 val prems = goal thy "m<n ==> n ~= 0"; |
|
30 by (exhaust_tac "n" 1); |
|
31 by (cut_facts_tac prems 1); |
|
32 by (ALLGOALS Asm_full_simp_tac); |
|
33 qed "gr_implies_not0"; |
|
34 |
|
35 Goal "(n ~= 0) = (0 < n)"; |
|
36 by (exhaust_tac "n" 1); |
|
37 by (Blast_tac 1); |
|
38 by (Blast_tac 1); |
|
39 qed "neq0_conv"; |
|
40 AddIffs [neq0_conv]; |
|
41 |
|
42 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) |
|
43 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); |
|
44 |
|
45 Goal "(~(0 < n)) = (n=0)"; |
|
46 by (rtac iffI 1); |
|
47 by (etac swap 1); |
|
48 by (ALLGOALS Asm_full_simp_tac); |
|
49 qed "not_gr0"; |
|
50 Addsimps [not_gr0]; |
|
51 |
|
52 Goal "m<n ==> 0 < n"; |
|
53 by (dtac gr_implies_not0 1); |
|
54 by (Asm_full_simp_tac 1); |
|
55 qed "gr_implies_gr0"; |
|
56 Addsimps [gr_implies_gr0]; |
|
57 |
|
58 qed_goalw "Least_Suc" thy [Least_nat_def] |
|
59 "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
|
60 (fn _ => [ |
|
61 rtac select_equality 1, |
|
62 fold_goals_tac [Least_nat_def], |
|
63 safe_tac (claset() addSEs [LeastI]), |
|
64 rename_tac "j" 1, |
|
65 exhaust_tac "j" 1, |
|
66 Blast_tac 1, |
|
67 blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1, |
|
68 rename_tac "k n" 1, |
|
69 exhaust_tac "k" 1, |
|
70 Blast_tac 1, |
|
71 hyp_subst_tac 1, |
|
72 rewtac Least_nat_def, |
|
73 rtac (select_equality RS arg_cong RS sym) 1, |
|
74 Safe_tac, |
|
75 dtac Suc_mono 1, |
|
76 Blast_tac 1, |
|
77 cut_facts_tac [less_linear] 1, |
|
78 Safe_tac, |
|
79 atac 2, |
|
80 Blast_tac 2, |
|
81 dtac Suc_mono 1, |
|
82 Blast_tac 1]); |
|
83 |
|
84 qed_goal "nat_induct2" thy |
|
85 "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [ |
|
86 cut_facts_tac prems 1, |
|
87 rtac less_induct 1, |
|
88 exhaust_tac "n" 1, |
|
89 hyp_subst_tac 1, |
|
90 atac 1, |
|
91 hyp_subst_tac 1, |
|
92 exhaust_tac "nat" 1, |
|
93 hyp_subst_tac 1, |
|
94 atac 1, |
|
95 hyp_subst_tac 1, |
|
96 resolve_tac prems 1, |
|
97 dtac spec 1, |
|
98 etac mp 1, |
|
99 rtac (lessI RS less_trans) 1, |
|
100 rtac (lessI RS Suc_mono) 1]); |
6 |
101 |
7 Goal "min 0 n = 0"; |
102 Goal "min 0 n = 0"; |
8 by (rtac min_leastL 1); |
103 by (rtac min_leastL 1); |
9 by (trans_tac 1); |
104 by (trans_tac 1); |
10 qed "min_0L"; |
105 qed "min_0L"; |