| author | paulson |
| Fri, 29 Oct 2004 15:16:02 +0200 | |
| changeset 15270 | 8b3f707a78a7 |
| parent 14331 | 8dbbb7cf3637 |
| child 15341 | 254f6f00b60e |
| permissions | -rw-r--r-- |
| 2441 | 1 |
(* Title: HOL/Nat.ML |
| 923 | 2 |
ID: $Id$ |
3 |
*) |
|
4 |
||
| 13450 | 5 |
(** legacy ML bindings **) |
|
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
6 |
|
| 13450 | 7 |
structure nat = |
8 |
struct |
|
9 |
val distinct = thms "nat.distinct"; |
|
10 |
val inject = thms "nat.inject"; |
|
11 |
val exhaust = thm "nat.exhaust"; |
|
12 |
val cases = thms "nat.cases"; |
|
13 |
val split = thm "nat.split"; |
|
14 |
val split_asm = thm "nat.split_asm"; |
|
15 |
val induct = thm "nat.induct"; |
|
16 |
val recs = thms "nat.recs"; |
|
17 |
val simps = thms "nat.simps"; |
|
18 |
end; |
|
19 |
||
20 |
val [nat_rec_0, nat_rec_Suc] = thms "nat.recs"; |
|
| 9108 | 21 |
bind_thm ("nat_rec_0", nat_rec_0);
|
22 |
bind_thm ("nat_rec_Suc", nat_rec_Suc);
|
|
|
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
23 |
|
| 13450 | 24 |
val [nat_case_0, nat_case_Suc] = thms "nat.cases"; |
| 9108 | 25 |
bind_thm ("nat_case_0", nat_case_0);
|
26 |
bind_thm ("nat_case_Suc", nat_case_Suc);
|
|
|
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset
|
27 |
|
| 13450 | 28 |
val LeastI = thm "LeastI"; |
29 |
val Least_Suc = thm "Least_Suc"; |
|
30 |
val Least_Suc2 = thm "Least_Suc2"; |
|
31 |
val Least_le = thm "Least_le"; |
|
32 |
val One_nat_def = thm "One_nat_def"; |
|
33 |
val Suc_Suc_eq = thm "Suc_Suc_eq"; |
|
34 |
val Suc_def = thm "Suc_def"; |
|
35 |
val Suc_diff_diff = thm "Suc_diff_diff"; |
|
36 |
val Suc_diff_le = thm "Suc_diff_le"; |
|
37 |
val Suc_inject = thm "Suc_inject"; |
|
38 |
val Suc_leD = thm "Suc_leD"; |
|
39 |
val Suc_leI = thm "Suc_leI"; |
|
40 |
val Suc_le_D = thm "Suc_le_D"; |
|
41 |
val Suc_le_eq = thm "Suc_le_eq"; |
|
42 |
val Suc_le_lessD = thm "Suc_le_lessD"; |
|
43 |
val Suc_le_mono = thm "Suc_le_mono"; |
|
44 |
val Suc_lessD = thm "Suc_lessD"; |
|
45 |
val Suc_lessE = thm "Suc_lessE"; |
|
46 |
val Suc_lessI = thm "Suc_lessI"; |
|
47 |
val Suc_less_SucD = thm "Suc_less_SucD"; |
|
48 |
val Suc_less_eq = thm "Suc_less_eq"; |
|
49 |
val Suc_mono = thm "Suc_mono"; |
|
50 |
val Suc_mult_cancel1 = thm "Suc_mult_cancel1"; |
|
51 |
val Suc_mult_le_cancel1 = thm "Suc_mult_le_cancel1"; |
|
52 |
val Suc_mult_less_cancel1 = thm "Suc_mult_less_cancel1"; |
|
53 |
val Suc_n_not_le_n = thm "Suc_n_not_le_n"; |
|
54 |
val Suc_n_not_n = thm "Suc_n_not_n"; |
|
55 |
val Suc_neq_Zero = thm "Suc_neq_Zero"; |
|
56 |
val Suc_not_Zero = thm "Suc_not_Zero"; |
|
57 |
val Suc_pred = thm "Suc_pred"; |
|
58 |
val Zero_nat_def = thm "Zero_nat_def"; |
|
59 |
val Zero_neq_Suc = thm "Zero_neq_Suc"; |
|
60 |
val Zero_not_Suc = thm "Zero_not_Suc"; |
|
61 |
val add_0 = thm "add_0"; |
|
62 |
val add_0_right = thm "add_0_right"; |
|
63 |
val add_Suc = thm "add_Suc"; |
|
64 |
val add_Suc_right = thm "add_Suc_right"; |
|
65 |
val add_ac = thms "add_ac"; |
|
66 |
val add_assoc = thm "add_assoc"; |
|
67 |
val add_commute = thm "add_commute"; |
|
68 |
val add_diff_inverse = thm "add_diff_inverse"; |
|
69 |
val add_eq_self_zero = thm "add_eq_self_zero"; |
|
70 |
val add_gr_0 = thm "add_gr_0"; |
|
71 |
val add_is_0 = thm "add_is_0"; |
|
72 |
val add_is_1 = thm "add_is_1"; |
|
73 |
val add_leD1 = thm "add_leD1"; |
|
74 |
val add_leD2 = thm "add_leD2"; |
|
75 |
val add_leE = thm "add_leE"; |
|
76 |
val add_le_mono = thm "add_le_mono"; |
|
77 |
val add_le_mono1 = thm "add_le_mono1"; |
|
| 14331 | 78 |
val nat_add_left_cancel = thm "nat_add_left_cancel"; |
79 |
val nat_add_left_cancel_le = thm "nat_add_left_cancel_le"; |
|
80 |
val nat_add_left_cancel_less = thm "nat_add_left_cancel_less"; |
|
| 13450 | 81 |
val add_left_commute = thm "add_left_commute"; |
82 |
val add_lessD1 = thm "add_lessD1"; |
|
83 |
val add_less_mono = thm "add_less_mono"; |
|
84 |
val add_less_mono1 = thm "add_less_mono1"; |
|
85 |
val add_mult_distrib = thm "add_mult_distrib"; |
|
86 |
val add_mult_distrib2 = thm "add_mult_distrib2"; |
|
| 14331 | 87 |
val nat_add_right_cancel = thm "nat_add_right_cancel"; |
| 13450 | 88 |
val def_nat_rec_0 = thm "def_nat_rec_0"; |
89 |
val def_nat_rec_Suc = thm "def_nat_rec_Suc"; |
|
90 |
val diff_0 = thm "diff_0"; |
|
91 |
val diff_0_eq_0 = thm "diff_0_eq_0"; |
|
92 |
val diff_Suc = thm "diff_Suc"; |
|
93 |
val diff_Suc_Suc = thm "diff_Suc_Suc"; |
|
94 |
val diff_Suc_less = thm "diff_Suc_less"; |
|
95 |
val diff_add_0 = thm "diff_add_0"; |
|
96 |
val diff_add_assoc = thm "diff_add_assoc"; |
|
97 |
val diff_add_assoc2 = thm "diff_add_assoc2"; |
|
98 |
val diff_add_inverse = thm "diff_add_inverse"; |
|
99 |
val diff_add_inverse2 = thm "diff_add_inverse2"; |
|
100 |
val diff_cancel = thm "diff_cancel"; |
|
101 |
val diff_cancel2 = thm "diff_cancel2"; |
|
102 |
val diff_commute = thm "diff_commute"; |
|
103 |
val diff_diff_left = thm "diff_diff_left"; |
|
104 |
val diff_induct = thm "diff_induct"; |
|
105 |
val diff_is_0_eq = thm "diff_is_0_eq"; |
|
106 |
val diff_le_self = thm "diff_le_self"; |
|
107 |
val diff_less_Suc = thm "diff_less_Suc"; |
|
108 |
val diff_mult_distrib = thm "diff_mult_distrib"; |
|
109 |
val diff_mult_distrib2 = thm "diff_mult_distrib2"; |
|
110 |
val diff_self_eq_0 = thm "diff_self_eq_0"; |
|
111 |
val eq_imp_le = thm "eq_imp_le"; |
|
112 |
val gr0I = thm "gr0I"; |
|
113 |
val gr0_conv_Suc = thm "gr0_conv_Suc"; |
|
114 |
val gr_implies_not0 = thm "gr_implies_not0"; |
|
115 |
val inj_Rep_Nat = thm "inj_Rep_Nat"; |
|
116 |
val inj_Suc = thm "inj_Suc"; |
|
117 |
val inj_on_Abs_Nat = thm "inj_on_Abs_Nat"; |
|
118 |
val le0 = thm "le0"; |
|
119 |
val leD = thm "leD"; |
|
120 |
val leE = thm "leE"; |
|
121 |
val leI = thm "leI"; |
|
122 |
val le_0_eq = thm "le_0_eq"; |
|
123 |
val le_SucE = thm "le_SucE"; |
|
124 |
val le_SucI = thm "le_SucI"; |
|
125 |
val le_Suc_eq = thm "le_Suc_eq"; |
|
126 |
val le_add1 = thm "le_add1"; |
|
127 |
val le_add2 = thm "le_add2"; |
|
128 |
val le_add_diff_inverse = thm "le_add_diff_inverse"; |
|
129 |
val le_add_diff_inverse2 = thm "le_add_diff_inverse2"; |
|
130 |
val le_anti_sym = thm "le_anti_sym"; |
|
131 |
val le_def = thm "le_def"; |
|
132 |
val le_eq_less_or_eq = thm "le_eq_less_or_eq"; |
|
133 |
val le_imp_diff_is_add = thm "le_imp_diff_is_add"; |
|
134 |
val le_imp_less_Suc = thm "le_imp_less_Suc"; |
|
135 |
val le_imp_less_or_eq = thm "le_imp_less_or_eq"; |
|
136 |
val le_less_trans = thm "le_less_trans"; |
|
137 |
val le_neq_implies_less = thm "le_neq_implies_less"; |
|
138 |
val le_refl = thm "le_refl"; |
|
139 |
val le_simps = thms "le_simps"; |
|
140 |
val le_trans = thm "le_trans"; |
|
141 |
val lessE = thm "lessE"; |
|
142 |
val lessI = thm "lessI"; |
|
143 |
val less_Suc0 = thm "less_Suc0"; |
|
144 |
val less_SucE = thm "less_SucE"; |
|
145 |
val less_SucI = thm "less_SucI"; |
|
146 |
val less_Suc_eq = thm "less_Suc_eq"; |
|
147 |
val less_Suc_eq_0_disj = thm "less_Suc_eq_0_disj"; |
|
148 |
val less_Suc_eq_le = thm "less_Suc_eq_le"; |
|
149 |
val less_add_Suc1 = thm "less_add_Suc1"; |
|
150 |
val less_add_Suc2 = thm "less_add_Suc2"; |
|
151 |
val less_add_eq_less = thm "less_add_eq_less"; |
|
152 |
val less_asym = thm "less_asym"; |
|
153 |
val less_def = thm "less_def"; |
|
154 |
val less_eq = thm "less_eq"; |
|
155 |
val less_iff_Suc_add = thm "less_iff_Suc_add"; |
|
156 |
val less_imp_Suc_add = thm "less_imp_Suc_add"; |
|
157 |
val less_imp_add_positive = thm "less_imp_add_positive"; |
|
158 |
val less_imp_diff_less = thm "less_imp_diff_less"; |
|
159 |
val less_imp_le = thm "less_imp_le"; |
|
160 |
val less_irrefl = thm "less_irrefl"; |
|
161 |
val less_le_trans = thm "less_le_trans"; |
|
162 |
val less_linear = thm "less_linear"; |
|
163 |
val less_mono_imp_le_mono = thm "less_mono_imp_le_mono"; |
|
164 |
val less_not_refl = thm "less_not_refl"; |
|
165 |
val less_not_refl2 = thm "less_not_refl2"; |
|
166 |
val less_not_refl3 = thm "less_not_refl3"; |
|
167 |
val less_not_sym = thm "less_not_sym"; |
|
168 |
val less_one = thm "less_one"; |
|
169 |
val less_or_eq_imp_le = thm "less_or_eq_imp_le"; |
|
170 |
val less_trans = thm "less_trans"; |
|
171 |
val less_trans_Suc = thm "less_trans_Suc"; |
|
172 |
val less_zeroE = thm "less_zeroE"; |
|
173 |
val max_0L = thm "max_0L"; |
|
174 |
val max_0R = thm "max_0R"; |
|
175 |
val max_Suc_Suc = thm "max_Suc_Suc"; |
|
176 |
val min_0L = thm "min_0L"; |
|
177 |
val min_0R = thm "min_0R"; |
|
178 |
val min_Suc_Suc = thm "min_Suc_Suc"; |
|
179 |
val mult_0 = thm "mult_0"; |
|
180 |
val mult_0_right = thm "mult_0_right"; |
|
181 |
val mult_1 = thm "mult_1"; |
|
182 |
val mult_1_right = thm "mult_1_right"; |
|
183 |
val mult_Suc = thm "mult_Suc"; |
|
184 |
val mult_Suc_right = thm "mult_Suc_right"; |
|
185 |
val mult_ac = thms "mult_ac"; |
|
186 |
val mult_assoc = thm "mult_assoc"; |
|
187 |
val mult_cancel1 = thm "mult_cancel1"; |
|
188 |
val mult_cancel2 = thm "mult_cancel2"; |
|
189 |
val mult_commute = thm "mult_commute"; |
|
190 |
val mult_eq_1_iff = thm "mult_eq_1_iff"; |
|
191 |
val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10"; |
|
192 |
val mult_is_0 = thm "mult_is_0"; |
|
193 |
val mult_le_cancel1 = thm "mult_le_cancel1"; |
|
194 |
val mult_le_cancel2 = thm "mult_le_cancel2"; |
|
195 |
val mult_le_mono = thm "mult_le_mono"; |
|
196 |
val mult_le_mono1 = thm "mult_le_mono1"; |
|
197 |
val mult_le_mono2 = thm "mult_le_mono2"; |
|
198 |
val mult_left_commute = thm "mult_left_commute"; |
|
199 |
val mult_less_cancel1 = thm "mult_less_cancel1"; |
|
200 |
val mult_less_cancel2 = thm "mult_less_cancel2"; |
|
201 |
val mult_less_mono1 = thm "mult_less_mono1"; |
|
202 |
val mult_less_mono2 = thm "mult_less_mono2"; |
|
203 |
val n_not_Suc_n = thm "n_not_Suc_n"; |
|
204 |
val nat_distrib = thms "nat_distrib"; |
|
205 |
val nat_induct = thm "nat_induct"; |
|
206 |
val nat_induct2 = thm "nat_induct2"; |
|
207 |
val nat_le_linear = thm "nat_le_linear"; |
|
208 |
val nat_less_cases = thm "nat_less_cases"; |
|
209 |
val nat_less_induct = thm "nat_less_induct"; |
|
210 |
val nat_less_le = thm "nat_less_le"; |
|
211 |
val nat_neq_iff = thm "nat_neq_iff"; |
|
212 |
val nat_not_singleton = thm "nat_not_singleton"; |
|
213 |
val neq0_conv = thm "neq0_conv"; |
|
214 |
val not0_implies_Suc = thm "not0_implies_Suc"; |
|
215 |
val not_add_less1 = thm "not_add_less1"; |
|
216 |
val not_add_less2 = thm "not_add_less2"; |
|
217 |
val not_gr0 = thm "not_gr0"; |
|
218 |
val not_leE = thm "not_leE"; |
|
219 |
val not_le_iff_less = thm "not_le_iff_less"; |
|
220 |
val not_less0 = thm "not_less0"; |
|
221 |
val not_less_Least = thm "not_less_Least"; |
|
222 |
val not_less_eq = thm "not_less_eq"; |
|
223 |
val not_less_iff_le = thm "not_less_iff_le"; |
|
224 |
val not_less_less_Suc_eq = thm "not_less_less_Suc_eq"; |
|
225 |
val not_less_simps = thms "not_less_simps"; |
|
226 |
val one_eq_mult_iff = thm "one_eq_mult_iff"; |
|
227 |
val one_is_add = thm "one_is_add"; |
|
228 |
val one_le_mult_iff = thm "one_le_mult_iff"; |
|
229 |
val one_reorient = thm "one_reorient"; |
|
230 |
val powerI = thm "powerI"; |
|
231 |
val pred_nat_def = thm "pred_nat_def"; |
|
232 |
val trans_le_add1 = thm "trans_le_add1"; |
|
233 |
val trans_le_add2 = thm "trans_le_add2"; |
|
234 |
val trans_less_add1 = thm "trans_less_add1"; |
|
235 |
val trans_less_add2 = thm "trans_less_add2"; |
|
236 |
val wf_less = thm "wf_less"; |
|
237 |
val wf_pred_nat = thm "wf_pred_nat"; |
|
238 |
val zero_induct = thm "zero_induct"; |
|
239 |
val zero_induct_lemma = thm "zero_induct_lemma"; |
|
240 |
val zero_less_Suc = thm "zero_less_Suc"; |
|
241 |
val zero_less_diff = thm "zero_less_diff"; |
|
242 |
val zero_less_mult_iff = thm "zero_less_mult_iff"; |
|
243 |
val zero_reorient = thm "zero_reorient"; |