author | wenzelm |
Mon, 12 Jul 1999 22:27:20 +0200 | |
changeset 6981 | eaade7e398a7 |
parent 6805 | 52b13dfbe954 |
child 7058 | 8dfea70eb6b7 |
permissions | -rw-r--r-- |
2441 | 1 |
(* Title: HOL/Nat.ML |
923 | 2 |
ID: $Id$ |
2608 | 3 |
Author: Tobias Nipkow |
4 |
Copyright 1997 TU Muenchen |
|
923 | 5 |
*) |
6 |
||
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
7 |
(** conversion rules for nat_rec **) |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
8 |
|
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
9 |
val [nat_rec_0, nat_rec_Suc] = nat.recs; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
10 |
|
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
11 |
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) |
5316 | 12 |
val prems = Goal |
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
13 |
"[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
14 |
by (simp_tac (simpset() addsimps prems) 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
15 |
qed "def_nat_rec_0"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
16 |
|
5316 | 17 |
val prems = Goal |
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
18 |
"[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
19 |
by (simp_tac (simpset() addsimps prems) 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
20 |
qed "def_nat_rec_Suc"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
21 |
|
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
22 |
val [nat_case_0, nat_case_Suc] = nat.cases; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
23 |
|
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
24 |
Goal "n ~= 0 ==> EX m. n = Suc m"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
25 |
by (exhaust_tac "n" 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
26 |
by (REPEAT (Blast_tac 1)); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
27 |
qed "not0_implies_Suc"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
28 |
|
5316 | 29 |
Goal "m<n ==> n ~= 0"; |
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
30 |
by (exhaust_tac "n" 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
31 |
by (ALLGOALS Asm_full_simp_tac); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
32 |
qed "gr_implies_not0"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
33 |
|
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
34 |
Goal "(n ~= 0) = (0 < n)"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
35 |
by (exhaust_tac "n" 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
36 |
by (Blast_tac 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
37 |
by (Blast_tac 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
38 |
qed "neq0_conv"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
39 |
AddIffs [neq0_conv]; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
40 |
|
5644 | 41 |
Goal "(0 ~= n) = (0 < n)"; |
6301 | 42 |
by (exhaust_tac "n" 1); |
43 |
by (Auto_tac); |
|
5644 | 44 |
qed "zero_neq_conv"; |
45 |
AddIffs [zero_neq_conv]; |
|
46 |
||
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
47 |
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
48 |
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
49 |
|
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
50 |
Goal "(~(0 < n)) = (n=0)"; |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
51 |
by (rtac iffI 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
52 |
by (etac swap 1); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
53 |
by (ALLGOALS Asm_full_simp_tac); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
54 |
qed "not_gr0"; |
6109 | 55 |
AddIffs [not_gr0]; |
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
56 |
|
6805 | 57 |
(*Useful in certain inductive arguments*) |
58 |
Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))"; |
|
59 |
by (exhaust_tac "m" 1); |
|
60 |
by Auto_tac; |
|
61 |
qed "less_Suc_eq_0_disj"; |
|
62 |
||
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
63 |
qed_goalw "Least_Suc" thy [Least_nat_def] |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
64 |
"!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
65 |
(fn _ => [ |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
66 |
rtac select_equality 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
67 |
fold_goals_tac [Least_nat_def], |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
68 |
safe_tac (claset() addSEs [LeastI]), |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
69 |
rename_tac "j" 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
70 |
exhaust_tac "j" 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
71 |
Blast_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
72 |
blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
73 |
rename_tac "k n" 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
74 |
exhaust_tac "k" 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
75 |
Blast_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
76 |
hyp_subst_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
77 |
rewtac Least_nat_def, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
78 |
rtac (select_equality RS arg_cong RS sym) 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
79 |
Safe_tac, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
80 |
dtac Suc_mono 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
81 |
Blast_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
82 |
cut_facts_tac [less_linear] 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
83 |
Safe_tac, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
84 |
atac 2, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
85 |
Blast_tac 2, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
86 |
dtac Suc_mono 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
87 |
Blast_tac 1]); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
88 |
|
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
89 |
qed_goal "nat_induct2" thy |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
90 |
"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [ |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
91 |
cut_facts_tac prems 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
92 |
rtac less_induct 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
93 |
exhaust_tac "n" 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
94 |
hyp_subst_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
95 |
atac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
96 |
hyp_subst_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
97 |
exhaust_tac "nat" 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
98 |
hyp_subst_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
99 |
atac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
100 |
hyp_subst_tac 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
101 |
resolve_tac prems 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
102 |
dtac spec 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
103 |
etac mp 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
104 |
rtac (lessI RS less_trans) 1, |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
105 |
rtac (lessI RS Suc_mono) 1]); |
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
106 |
|
5069 | 107 |
Goal "min 0 n = 0"; |
3023 | 108 |
by (rtac min_leastL 1); |
5983 | 109 |
by (Simp_tac 1); |
2608 | 110 |
qed "min_0L"; |
1301 | 111 |
|
5069 | 112 |
Goal "min n 0 = 0"; |
3023 | 113 |
by (rtac min_leastR 1); |
5983 | 114 |
by (Simp_tac 1); |
2608 | 115 |
qed "min_0R"; |
923 | 116 |
|
5069 | 117 |
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)"; |
3023 | 118 |
by (Simp_tac 1); |
2608 | 119 |
qed "min_Suc_Suc"; |
1660 | 120 |
|
2608 | 121 |
Addsimps [min_0L,min_0R,min_Suc_Suc]; |
6433 | 122 |
|
123 |
Goalw [max_def] "max 0 n = n"; |
|
124 |
by (Simp_tac 1); |
|
125 |
qed "max_0L"; |
|
126 |
||
127 |
Goalw [max_def] "max n 0 = n"; |
|
128 |
by (Simp_tac 1); |
|
129 |
qed "max_0R"; |
|
130 |
||
131 |
Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)"; |
|
132 |
by (Simp_tac 1); |
|
133 |
qed "max_Suc_Suc"; |
|
134 |
||
135 |
Addsimps [max_0L,max_0R,max_Suc_Suc]; |