1 |
|
2 (** legacy ML bindings **) |
|
3 |
|
4 val Cons_eq_appendI = thm "Cons_eq_appendI"; |
|
5 val Cons_in_lex = thm "Cons_in_lex"; |
|
6 val Nil2_notin_lex = thm "Nil2_notin_lex"; |
|
7 val Nil_eq_concat_conv = thm "Nil_eq_concat_conv"; |
|
8 val Nil_is_append_conv = thm "Nil_is_append_conv"; |
|
9 val Nil_is_map_conv = thm "Nil_is_map_conv"; |
|
10 val Nil_is_rev_conv = thm "Nil_is_rev_conv"; |
|
11 val Nil_notin_lex = thm "Nil_notin_lex"; |
|
12 val all_nth_imp_all_set = thm "all_nth_imp_all_set"; |
|
13 val all_set_conv_all_nth = thm "all_set_conv_all_nth"; |
|
14 val append1_eq_conv = thm "append1_eq_conv"; |
|
15 val append_Cons = thm "append_Cons"; |
|
16 val append_Nil = thm "append_Nil"; |
|
17 val append_Nil2 = thm "append_Nil2"; |
|
18 val append_assoc = thm "append_assoc"; |
|
19 val append_butlast_last_id = thm "append_butlast_last_id"; |
|
20 val append_eq_appendI = thm "append_eq_appendI"; |
|
21 val append_eq_append_conv = thm "append_eq_append_conv"; |
|
22 val append_eq_conv_conj = thm "append_eq_conv_conj"; |
|
23 val append_in_lists_conv = thm "append_in_lists_conv"; |
|
24 val append_is_Nil_conv = thm "append_is_Nil_conv"; |
|
25 val append_same_eq = thm "append_same_eq"; |
|
26 val append_self_conv = thm "append_self_conv"; |
|
27 val append_self_conv2 = thm "append_self_conv2"; |
|
28 val append_take_drop_id = thm "append_take_drop_id"; |
|
29 val butlast_append = thm "butlast_append"; |
|
30 val butlast_snoc = thm "butlast_snoc"; |
|
31 val concat_append = thm "concat_append"; |
|
32 val concat_eq_Nil_conv = thm "concat_eq_Nil_conv"; |
|
33 val distinct_append = thm "distinct_append"; |
|
34 val distinct_filter = thm "distinct_filter"; |
|
35 val distinct_remdups = thm "distinct_remdups"; |
|
36 val dropWhile_append1 = thm "dropWhile_append1"; |
|
37 val dropWhile_append2 = thm "dropWhile_append2"; |
|
38 val drop_0 = thm "drop_0"; |
|
39 val drop_Cons = thm "drop_Cons"; |
|
40 val drop_Cons' = thm "drop_Cons'"; |
|
41 val drop_Nil = thm "drop_Nil"; |
|
42 val drop_Suc_Cons = thm "drop_Suc_Cons"; |
|
43 val drop_all = thm "drop_all"; |
|
44 val drop_append = thm "drop_append"; |
|
45 val drop_drop = thm "drop_drop"; |
|
46 val drop_map = thm "drop_map"; |
|
47 val elem_le_sum = thm "elem_le_sum"; |
|
48 val eq_Nil_appendI = thm "eq_Nil_appendI"; |
|
49 val filter_False = thm "filter_False"; |
|
50 val filter_True = thm "filter_True"; |
|
51 val filter_append = thm "filter_append"; |
|
52 val filter_concat = thm "filter_concat"; |
|
53 val filter_filter = thm "filter_filter"; |
|
54 val filter_is_subset = thm "filter_is_subset"; |
|
55 val finite_set = thm "finite_set"; |
|
56 val foldl_Cons = thm "foldl_Cons"; |
|
57 val foldl_Nil = thm "foldl_Nil"; |
|
58 val foldl_append = thm "foldl_append"; |
|
59 val hd_Cons_tl = thm "hd_Cons_tl"; |
|
60 val hd_append = thm "hd_append"; |
|
61 val hd_append2 = thm "hd_append2"; |
|
62 val hd_replicate = thm "hd_replicate"; |
|
63 val in_listsD = thm "in_listsD"; |
|
64 val in_listsI = thm "in_listsI"; |
|
65 val in_lists_conv_set = thm "in_lists_conv_set"; |
|
66 val in_set_butlastD = thm "in_set_butlastD"; |
|
67 val in_set_butlast_appendI = thm "in_set_butlast_appendI"; |
|
68 val in_set_conv_decomp = thm "in_set_conv_decomp"; |
|
69 val in_set_replicateD = thm "in_set_replicateD"; |
|
70 val inj_map = thm "inj_map"; |
|
71 val inj_mapD = thm "inj_mapD"; |
|
72 val inj_mapI = thm "inj_mapI"; |
|
73 val last_replicate = thm "last_replicate"; |
|
74 val last_snoc = thm "last_snoc"; |
|
75 val length_0_conv = thm "length_0_conv"; |
|
76 val length_Suc_conv = thm "length_Suc_conv"; |
|
77 val length_append = thm "length_append"; |
|
78 val length_butlast = thm "length_butlast"; |
|
79 val length_drop = thm "length_drop"; |
|
80 val length_filter_le = thm "length_filter_le"; |
|
81 val length_greater_0_conv = thm "length_greater_0_conv"; |
|
82 val length_induct = thm "length_induct"; |
|
83 val length_list_update = thm "length_list_update"; |
|
84 val length_map = thm "length_map"; |
|
85 val length_replicate = thm "length_replicate"; |
|
86 val length_rev = thm "length_rev"; |
|
87 val length_take = thm "length_take"; |
|
88 val length_tl = thm "length_tl"; |
|
89 val length_upt = thm "length_upt"; |
|
90 val length_zip = thm "length_zip"; |
|
91 val lex_conv = thm "lex_conv"; |
|
92 val lex_def = thm "lex_def"; |
|
93 val lenlex_conv = thm "lenlex_conv"; |
|
94 val lenlex_def = thm "lenlex_def"; |
|
95 val lexn_conv = thm "lexn_conv"; |
|
96 val lexn_length = thm "lexn_length"; |
|
97 val list_all2_Cons = thm "list_all2_Cons"; |
|
98 val list_all2_Cons1 = thm "list_all2_Cons1"; |
|
99 val list_all2_Cons2 = thm "list_all2_Cons2"; |
|
100 val list_all2_Nil = thm "list_all2_Nil"; |
|
101 val list_all2_Nil2 = thm "list_all2_Nil2"; |
|
102 val list_all2_append1 = thm "list_all2_append1"; |
|
103 val list_all2_append2 = thm "list_all2_append2"; |
|
104 val list_all2_conv_all_nth = thm "list_all2_conv_all_nth"; |
|
105 val list_all2_def = thm "list_all2_def"; |
|
106 val list_all2_lengthD = thm "list_all2_lengthD"; |
|
107 val list_all2_rev = thm "list_all2_rev"; |
|
108 val list_all2_trans = thm "list_all2_trans"; |
|
109 val list_all_append = thm "list_all_append"; |
|
110 val list_all_iff = thm "list_all_iff"; |
|
111 val list_ball_nth = thm "list_ball_nth"; |
|
112 val list_update_overwrite = thm "list_update_overwrite"; |
|
113 val list_update_same_conv = thm "list_update_same_conv"; |
|
114 val listsE = thm "listsE"; |
|
115 val lists_IntI = thm "lists_IntI"; |
|
116 val lists_Int_eq = thm "lists_Int_eq"; |
|
117 val lists_mono = thm "lists_mono"; |
|
118 val map_Suc_upt = thm "map_Suc_upt"; |
|
119 val map_append = thm "map_append"; |
|
120 val map_compose = thm "map_compose"; |
|
121 val map_concat = thm "map_concat"; |
|
122 val map_cong = thm "map_cong"; |
|
123 val map_eq_Cons_conv = thm "map_eq_Cons_conv"; |
|
124 val map_ext = thm "map_ext"; |
|
125 val map_ident = thm "map_ident"; |
|
126 val map_injective = thm "map_injective"; |
|
127 val map_is_Nil_conv = thm "map_is_Nil_conv"; |
|
128 val map_replicate = thm "map_replicate"; |
|
129 val neq_Nil_conv = thm "neq_Nil_conv"; |
|
130 val not_Cons_self = thm "not_Cons_self"; |
|
131 val not_Cons_self2 = thm "not_Cons_self2"; |
|
132 val nth_Cons = thm "nth_Cons"; |
|
133 val nth_Cons' = thm "nth_Cons'"; |
|
134 val nth_Cons_0 = thm "nth_Cons_0"; |
|
135 val nth_Cons_Suc = thm "nth_Cons_Suc"; |
|
136 val nth_append = thm "nth_append"; |
|
137 val nth_drop = thm "nth_drop"; |
|
138 val nth_equalityI = thm "nth_equalityI"; |
|
139 val nth_list_update = thm "nth_list_update"; |
|
140 val nth_list_update_eq = thm "nth_list_update_eq"; |
|
141 val nth_list_update_neq = thm "nth_list_update_neq"; |
|
142 val nth_map_upt = thm "nth_map_upt"; |
|
143 val nth_mem = thm "nth_mem"; |
|
144 val nth_replicate = thm "nth_replicate"; |
|
145 val nth_take = thm "nth_take"; |
|
146 val nth_take_lemma = thm "nth_take_lemma"; |
|
147 val nth_upt = thm "nth_upt"; |
|
148 val nth_zip = thm "nth_zip"; |
|
149 val replicate_0 = thm "replicate_0"; |
|
150 val replicate_Suc = thm "replicate_Suc"; |
|
151 val replicate_add = thm "replicate_add"; |
|
152 val replicate_app_Cons_same = thm "replicate_app_Cons_same"; |
|
153 val rev_append = thm "rev_append"; |
|
154 val rev_concat = thm "rev_concat"; |
|
155 val rev_drop = thm "rev_drop"; |
|
156 val rev_exhaust = thm "rev_exhaust"; |
|
157 val rev_induct = thm "rev_induct"; |
|
158 val rev_is_Nil_conv = thm "rev_is_Nil_conv"; |
|
159 val rev_is_rev_conv = thm "rev_is_rev_conv"; |
|
160 val rev_map = thm "rev_map"; |
|
161 val rev_replicate = thm "rev_replicate"; |
|
162 val rev_rev_ident = thm "rev_rev_ident"; |
|
163 val rev_take = thm "rev_take"; |
|
164 val same_append_eq = thm "same_append_eq"; |
|
165 val self_append_conv = thm "self_append_conv"; |
|
166 val self_append_conv2 = thm "self_append_conv2"; |
|
167 val set_append = thm "set_append"; |
|
168 val set_concat = thm "set_concat"; |
|
169 val set_conv_nth = thm "set_conv_nth"; |
|
170 val set_empty = thm "set_empty"; |
|
171 val set_filter = thm "set_filter"; |
|
172 val set_map = thm "set_map"; |
|
173 val mem_ii = thm "mem_iff"; |
|
174 val set_remdups = thm "set_remdups"; |
|
175 val set_replicate = thm "set_replicate"; |
|
176 val set_replicate_conv_if = thm "set_replicate_conv_if"; |
|
177 val set_rev = thm "set_rev"; |
|
178 val set_subset_Cons = thm "set_subset_Cons"; |
|
179 val set_take_whileD = thm "set_take_whileD"; |
|
180 val set_update_subsetI = thm "set_update_subsetI"; |
|
181 val set_update_subset_insert = thm "set_update_subset_insert"; |
|
182 val set_upt = thm "set_upt"; |
|
183 val set_zip = thm "set_zip"; |
|
184 val start_le_sum = thm "start_le_sum"; |
|
185 val sublist_Cons = thm "sublist_Cons"; |
|
186 val sublist_append = thm "sublist_append"; |
|
187 val sublist_def = thm "sublist_def"; |
|
188 val sublist_empty = thm "sublist_empty"; |
|
189 val sublist_nil = thm "sublist_nil"; |
|
190 val sublist_shift_lemma = thm "sublist_shift_lemma"; |
|
191 val sublist_singleton = thm "sublist_singleton"; |
|
192 val sublist_upt_eq_take = thm "sublist_upt_eq_take"; |
|
193 val sum_eq_0_conv = thm "sum_eq_0_conv"; |
|
194 val takeWhile_append1 = thm "takeWhile_append1"; |
|
195 val takeWhile_append2 = thm "takeWhile_append2"; |
|
196 val takeWhile_dropWhile_id = thm "takeWhile_dropWhile_id"; |
|
197 val takeWhile_tail = thm "takeWhile_tail"; |
|
198 val take_0 = thm "take_0"; |
|
199 val take_Cons = thm "take_Cons"; |
|
200 val take_Cons' = thm "take_Cons'"; |
|
201 val take_Nil = thm "take_Nil"; |
|
202 val take_Suc_Cons = thm "take_Suc_Cons"; |
|
203 val take_all = thm "take_all"; |
|
204 val take_append = thm "take_append"; |
|
205 val take_drop = thm "take_drop"; |
|
206 val take_equalityI = thm "take_equalityI"; |
|
207 val take_map = thm "take_map"; |
|
208 val take_take = thm "take_take"; |
|
209 val take_upt = thm "take_upt"; |
|
210 val tl_append = thm "tl_append"; |
|
211 val tl_append2 = thm "tl_append2"; |
|
212 val tl_replicate = thm "tl_replicate"; |
|
213 val update_zip = thm "update_zip"; |
|
214 val upt_0 = thm "upt_0"; |
|
215 val upt_Suc = thm "upt_Suc"; |
|
216 val upt_Suc_append = thm "upt_Suc_append"; |
|
217 val upt_add_eq_append = thm "upt_add_eq_append"; |
|
218 val upt_conv_Cons = thm "upt_conv_Cons"; |
|
219 val upt_conv_Nil = thm "upt_conv_Nil"; |
|
220 val upt_rec = thm "upt_rec"; |
|
221 val wf_lex = thm "wf_lex"; |
|
222 val wf_lenlex = thm "wf_lenlex"; |
|
223 val wf_lexn = thm "wf_lexn"; |
|
224 val zip_Cons_Cons = thm "zip_Cons_Cons"; |
|
225 val zip_Nil = thm "zip_Nil"; |
|
226 val zip_append = thm "zip_append"; |
|
227 val zip_append1 = thm "zip_append1"; |
|
228 val zip_append2 = thm "zip_append2"; |
|
229 val zip_replicate = thm "zip_replicate"; |
|
230 val zip_rev = thm "zip_rev"; |
|
231 val zip_update = thm "zip_update"; |
|