1 (* Title: HOL/Nat.ML |
|
2 ID: $Id$ |
|
3 *) |
|
4 |
|
5 (** legacy ML bindings **) |
|
6 |
|
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 Least_Suc = thm "Least_Suc"; |
|
21 val Least_Suc2 = thm "Least_Suc2"; |
|
22 val One_nat_def = thm "One_nat_def"; |
|
23 val Suc_Suc_eq = thm "Suc_Suc_eq"; |
|
24 val Suc_def = thm "Suc_def"; |
|
25 val Suc_diff_diff = thm "Suc_diff_diff"; |
|
26 val Suc_diff_le = thm "Suc_diff_le"; |
|
27 val Suc_inject = thm "Suc_inject"; |
|
28 val Suc_leD = thm "Suc_leD"; |
|
29 val Suc_leI = thm "Suc_leI"; |
|
30 val Suc_le_D = thm "Suc_le_D"; |
|
31 val Suc_le_eq = thm "Suc_le_eq"; |
|
32 val Suc_le_lessD = thm "Suc_le_lessD"; |
|
33 val Suc_le_mono = thm "Suc_le_mono"; |
|
34 val Suc_lessD = thm "Suc_lessD"; |
|
35 val Suc_lessE = thm "Suc_lessE"; |
|
36 val Suc_lessI = thm "Suc_lessI"; |
|
37 val Suc_less_SucD = thm "Suc_less_SucD"; |
|
38 val Suc_less_eq = thm "Suc_less_eq"; |
|
39 val Suc_mono = thm "Suc_mono"; |
|
40 val Suc_mult_cancel1 = thm "Suc_mult_cancel1"; |
|
41 val Suc_mult_le_cancel1 = thm "Suc_mult_le_cancel1"; |
|
42 val Suc_mult_less_cancel1 = thm "Suc_mult_less_cancel1"; |
|
43 val Suc_n_not_le_n = thm "Suc_n_not_le_n"; |
|
44 val Suc_n_not_n = thm "Suc_n_not_n"; |
|
45 val Suc_neq_Zero = thm "Suc_neq_Zero"; |
|
46 val Suc_not_Zero = thm "Suc_not_Zero"; |
|
47 val Suc_pred = thm "Suc_pred"; |
|
48 val Zero_nat_def = thm "Zero_nat_def"; |
|
49 val Zero_neq_Suc = thm "Zero_neq_Suc"; |
|
50 val Zero_not_Suc = thm "Zero_not_Suc"; |
|
51 val add_0 = thm "add_0"; |
|
52 val add_0_right = thm "add_0_right"; |
|
53 val add_Suc = thm "add_Suc"; |
|
54 val add_Suc_right = thm "add_Suc_right"; |
|
55 val add_ac = thms "add_ac"; |
|
56 val add_assoc = thm "add_assoc"; |
|
57 val add_commute = thm "add_commute"; |
|
58 val add_diff_inverse = thm "add_diff_inverse"; |
|
59 val add_eq_self_zero = thm "add_eq_self_zero"; |
|
60 val add_gr_0 = thm "add_gr_0"; |
|
61 val add_is_0 = thm "add_is_0"; |
|
62 val add_is_1 = thm "add_is_1"; |
|
63 val add_leD1 = thm "add_leD1"; |
|
64 val add_leD2 = thm "add_leD2"; |
|
65 val add_leE = thm "add_leE"; |
|
66 val add_le_mono = thm "add_le_mono"; |
|
67 val add_le_mono1 = thm "add_le_mono1"; |
|
68 val nat_add_left_cancel = thm "nat_add_left_cancel"; |
|
69 val nat_add_left_cancel_le = thm "nat_add_left_cancel_le"; |
|
70 val nat_add_left_cancel_less = thm "nat_add_left_cancel_less"; |
|
71 val add_left_commute = thm "add_left_commute"; |
|
72 val add_lessD1 = thm "add_lessD1"; |
|
73 val add_less_mono = thm "add_less_mono"; |
|
74 val add_less_mono1 = thm "add_less_mono1"; |
|
75 val add_mult_distrib = thm "add_mult_distrib"; |
|
76 val add_mult_distrib2 = thm "add_mult_distrib2"; |
|
77 val nat_add_right_cancel = thm "nat_add_right_cancel"; |
|
78 val def_nat_rec_0 = thm "def_nat_rec_0"; |
|
79 val def_nat_rec_Suc = thm "def_nat_rec_Suc"; |
|
80 val diff_0 = thm "diff_0"; |
|
81 val diff_0_eq_0 = thm "diff_0_eq_0"; |
|
82 val diff_Suc = thm "diff_Suc"; |
|
83 val diff_Suc_Suc = thm "diff_Suc_Suc"; |
|
84 val diff_Suc_less = thm "diff_Suc_less"; |
|
85 val diff_add_0 = thm "diff_add_0"; |
|
86 val diff_add_assoc = thm "diff_add_assoc"; |
|
87 val diff_add_assoc2 = thm "diff_add_assoc2"; |
|
88 val diff_add_inverse = thm "diff_add_inverse"; |
|
89 val diff_add_inverse2 = thm "diff_add_inverse2"; |
|
90 val diff_cancel = thm "diff_cancel"; |
|
91 val diff_cancel2 = thm "diff_cancel2"; |
|
92 val diff_commute = thm "diff_commute"; |
|
93 val diff_diff_left = thm "diff_diff_left"; |
|
94 val diff_induct = thm "diff_induct"; |
|
95 val diff_is_0_eq = thm "diff_is_0_eq"; |
|
96 val diff_le_self = thm "diff_le_self"; |
|
97 val diff_less_Suc = thm "diff_less_Suc"; |
|
98 val diff_mult_distrib = thm "diff_mult_distrib"; |
|
99 val diff_mult_distrib2 = thm "diff_mult_distrib2"; |
|
100 val diff_self_eq_0 = thm "diff_self_eq_0"; |
|
101 val eq_imp_le = thm "eq_imp_le"; |
|
102 val gr0I = thm "gr0I"; |
|
103 val gr0_conv_Suc = thm "gr0_conv_Suc"; |
|
104 val gr_implies_not0 = thm "gr_implies_not0"; |
|
105 val inj_Suc = thm "inj_Suc"; |
|
106 val le0 = thm "le0"; |
|
107 val le_0_eq = thm "le_0_eq"; |
|
108 val le_SucE = thm "le_SucE"; |
|
109 val le_SucI = thm "le_SucI"; |
|
110 val le_Suc_eq = thm "le_Suc_eq"; |
|
111 val le_add1 = thm "le_add1"; |
|
112 val le_add2 = thm "le_add2"; |
|
113 val le_add_diff_inverse = thm "le_add_diff_inverse"; |
|
114 val le_add_diff_inverse2 = thm "le_add_diff_inverse2"; |
|
115 val le_anti_sym = thm "le_anti_sym"; |
|
116 val le_def = thm "le_def"; |
|
117 val le_eq_less_or_eq = thm "le_eq_less_or_eq"; |
|
118 val le_imp_diff_is_add = thm "le_imp_diff_is_add"; |
|
119 val le_imp_less_Suc = thm "le_imp_less_Suc"; |
|
120 val le_imp_less_or_eq = thm "le_imp_less_or_eq"; |
|
121 val le_less_trans = thm "le_less_trans"; |
|
122 val le_neq_implies_less = thm "le_neq_implies_less"; |
|
123 val le_refl = thm "le_refl"; |
|
124 val le_simps = thms "le_simps"; |
|
125 val le_trans = thm "le_trans"; |
|
126 val lessE = thm "lessE"; |
|
127 val lessI = thm "lessI"; |
|
128 val less_Suc0 = thm "less_Suc0"; |
|
129 val less_SucE = thm "less_SucE"; |
|
130 val less_SucI = thm "less_SucI"; |
|
131 val less_Suc_eq = thm "less_Suc_eq"; |
|
132 val less_Suc_eq_0_disj = thm "less_Suc_eq_0_disj"; |
|
133 val less_Suc_eq_le = thm "less_Suc_eq_le"; |
|
134 val less_add_Suc1 = thm "less_add_Suc1"; |
|
135 val less_add_Suc2 = thm "less_add_Suc2"; |
|
136 val less_add_eq_less = thm "less_add_eq_less"; |
|
137 val less_asym = thm "less_asym"; |
|
138 val less_def = thm "less_def"; |
|
139 val less_eq = thm "less_eq"; |
|
140 val less_iff_Suc_add = thm "less_iff_Suc_add"; |
|
141 val less_imp_Suc_add = thm "less_imp_Suc_add"; |
|
142 val less_imp_add_positive = thm "less_imp_add_positive"; |
|
143 val less_imp_diff_less = thm "less_imp_diff_less"; |
|
144 val less_imp_le = thm "less_imp_le"; |
|
145 val less_irrefl = thm "less_irrefl"; |
|
146 val less_le_trans = thm "less_le_trans"; |
|
147 val less_linear = thm "less_linear"; |
|
148 val less_mono_imp_le_mono = thm "less_mono_imp_le_mono"; |
|
149 val less_not_refl = thm "less_not_refl"; |
|
150 val less_not_refl2 = thm "less_not_refl2"; |
|
151 val less_not_refl3 = thm "less_not_refl3"; |
|
152 val less_not_sym = thm "less_not_sym"; |
|
153 val less_one = thm "less_one"; |
|
154 val less_or_eq_imp_le = thm "less_or_eq_imp_le"; |
|
155 val less_trans = thm "less_trans"; |
|
156 val less_trans_Suc = thm "less_trans_Suc"; |
|
157 val less_zeroE = thm "less_zeroE"; |
|
158 val max_0L = thm "max_0L"; |
|
159 val max_0R = thm "max_0R"; |
|
160 val max_Suc_Suc = thm "max_Suc_Suc"; |
|
161 val min_0L = thm "min_0L"; |
|
162 val min_0R = thm "min_0R"; |
|
163 val min_Suc_Suc = thm "min_Suc_Suc"; |
|
164 val mult_0 = thm "mult_0"; |
|
165 val mult_0_right = thm "mult_0_right"; |
|
166 val mult_1 = thm "mult_1"; |
|
167 val mult_1_right = thm "mult_1_right"; |
|
168 val mult_Suc = thm "mult_Suc"; |
|
169 val mult_Suc_right = thm "mult_Suc_right"; |
|
170 val mult_ac = thms "mult_ac"; |
|
171 val mult_assoc = thm "mult_assoc"; |
|
172 val mult_cancel1 = thm "mult_cancel1"; |
|
173 val mult_cancel2 = thm "mult_cancel2"; |
|
174 val mult_commute = thm "mult_commute"; |
|
175 val mult_eq_1_iff = thm "mult_eq_1_iff"; |
|
176 val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10"; |
|
177 val mult_is_0 = thm "mult_is_0"; |
|
178 val mult_le_cancel1 = thm "mult_le_cancel1"; |
|
179 val mult_le_cancel2 = thm "mult_le_cancel2"; |
|
180 val mult_le_mono = thm "mult_le_mono"; |
|
181 val mult_le_mono1 = thm "mult_le_mono1"; |
|
182 val mult_le_mono2 = thm "mult_le_mono2"; |
|
183 val mult_left_commute = thm "mult_left_commute"; |
|
184 val mult_less_cancel1 = thm "mult_less_cancel1"; |
|
185 val mult_less_cancel2 = thm "mult_less_cancel2"; |
|
186 val mult_less_mono1 = thm "mult_less_mono1"; |
|
187 val mult_less_mono2 = thm "mult_less_mono2"; |
|
188 val n_not_Suc_n = thm "n_not_Suc_n"; |
|
189 val nat_distrib = thms "nat_distrib"; |
|
190 val nat_induct = thm "nat_induct"; |
|
191 val nat_induct2 = thm "nat_induct2"; |
|
192 val nat_le_linear = thm "nat_le_linear"; |
|
193 val nat_less_cases = thm "nat_less_cases"; |
|
194 val nat_less_induct = thm "nat_less_induct"; |
|
195 val nat_less_le = thm "nat_less_le"; |
|
196 val nat_neq_iff = thm "nat_neq_iff"; |
|
197 val nat_not_singleton = thm "nat_not_singleton"; |
|
198 val neq0_conv = thm "neq0_conv"; |
|
199 val not0_implies_Suc = thm "not0_implies_Suc"; |
|
200 val not_add_less1 = thm "not_add_less1"; |
|
201 val not_add_less2 = thm "not_add_less2"; |
|
202 val not_gr0 = thm "not_gr0"; |
|
203 val not_leE = thm "not_leE"; |
|
204 val not_less0 = thm "not_less0"; |
|
205 val not_less_eq = thm "not_less_eq"; |
|
206 val not_less_less_Suc_eq = thm "not_less_less_Suc_eq"; |
|
207 val not_less_simps = thms "not_less_simps"; |
|
208 val one_eq_mult_iff = thm "one_eq_mult_iff"; |
|
209 val one_is_add = thm "one_is_add"; |
|
210 val one_le_mult_iff = thm "one_le_mult_iff"; |
|
211 val one_reorient = thm "one_reorient"; |
|
212 val pred_nat_def = thm "pred_nat_def"; |
|
213 val trans_le_add1 = thm "trans_le_add1"; |
|
214 val trans_le_add2 = thm "trans_le_add2"; |
|
215 val trans_less_add1 = thm "trans_less_add1"; |
|
216 val trans_less_add2 = thm "trans_less_add2"; |
|
217 val wf_less = thm "wf_less"; |
|
218 val wf_pred_nat = thm "wf_pred_nat"; |
|
219 val zero_induct = thm "zero_induct"; |
|
220 val zero_induct_lemma = thm "zero_induct_lemma"; |
|
221 val zero_less_Suc = thm "zero_less_Suc"; |
|
222 val zero_less_diff = thm "zero_less_diff"; |
|
223 val zero_less_mult_iff = thm "zero_less_mult_iff"; |
|
224 val zero_reorient = thm "zero_reorient"; |
|
225 val linorder_neqE_nat = thm "linorder_neqE_nat"; |
|