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