1open List_conv;
2
3LIST_CONV (--`SNOC h []:'a list`--);
4LIST_CONV (--`SNOC h (CONS h t):'a list`--);
5
6LIST_CONV (--`NULL ([]:'a list)`--);
7LIST_CONV (--`NULL (CONS h t:'a list)`--);
8LIST_CONV (--`NULL (SNOC h t:'a list)`--);
9LIST_CONV (--`NULL (APPEND l1 l2 :'a list)`--);
10LIST_CONV (--`NULL [1;2;3]`--);
11LIST_CONV (--`NULL (REVERSE (l:bool list))`--);
12LIST_CONV (--`NULL (FLAT (l:'a list list))`--);
13
14LIST_CONV (--`LENGTH ([]:'a list)`--);
15LIST_CONV (--`LENGTH (CONS h t:'a list)`--);
16LIST_CONV (--`LENGTH (CONS h []:'a list)`--);
17LIST_CONV (--`LENGTH (SNOC h t:'a list)`--);
18LIST_CONV (--`LENGTH (SNOC h []:'a list)`--);
19LIST_CONV (--`LENGTH (APPEND l1 l2 :'a list)`--);
20LIST_CONV (--`LENGTH [1;2;3]`--);
21LIST_CONV (--`LENGTH (SNOC 1 (SNOC 2 (SNOC 3 [])))`--);
22LIST_CONV (--`LENGTH (FLAT (l :num list list))`--);
23LIST_CONV (--`LENGTH (FLAT (l :'a list list))`--);
24
25LIST_CONV (--`MAP (P:'a list -> 'a) []`--);
26LIST_CONV (--`MAP (P:'a list -> 'a) (CONS h t)`--);
27LIST_CONV (--`MAP (P:'a list -> 'a) (CONS h [])`--);
28LIST_CONV (--`MAP (P:'a list -> 'a) (SNOC h t)`--);
29LIST_CONV (--`MAP (P:'a list -> 'a) (SNOC h [])`--);
30LIST_CONV (--`MAP (P:'a list -> 'a) [x;y;z]`--);
31LIST_CONV (--`MAP (P:num list ->num) (APPEND l1 l2)`--);
32LIST_CONV (--`MAP (f:'a ->'b) (FLAT l)`--);
33LIST_CONV (--`MAP (f:num ->num) (FLAT l)`--);
34
35LIST_CONV (--`FILTER (g:'b ->bool) []`--);
36LIST_CONV (--`FILTER (g:'b ->bool) (CONS h t)`--);
37LIST_CONV (--`FILTER (g:'b ->bool) (SNOC h t)`--);
38LIST_CONV (--`FILTER (P:num list -> bool) (APPEND l1 l2)`--);
39LIST_CONV (--`FILTER (f:'a  -> bool) (FLAT l)`--);
40
41LIST_CONV (--`APPEND (l1:'a list) []`--);
42LIST_CONV (--`APPEND [] (l1:'a list)`--);
43LIST_CONV (--`APPEND (l1:'a list) (CONS h t)`--);
44(* LIST_CONV (--`APPEND (l1:'a list) (APPEND l2 l3)`--)
45   handle e => Raise e; BLOCKED *)
46LIST_CONV (--`APPEND (APPEND l2 l3)(l1:'a list)`--);
47LIST_CONV (--`APPEND (l1:'a list) (SNOC h t)`--);
48(* LIST_CONV (--`APPEND (SNOC h t) (l1:'a list)`--)
49   handle e => Raise e; BLOCKED *)
50LIST_CONV (--`APPEND [1;2;3] [4;5;6]`--);
51LIST_CONV (--`APPEND (SNOC 1 (SNOC 2 (SNOC 3 []))) [4;5;6]`--);
52LIST_CONV (--`APPEND  [4;5;6] (SNOC 1 (SNOC 2 (SNOC 3 [])))`--);
53LIST_CONV (--`APPEND [x] (l1:'a list)`--);
54LIST_CONV (--`APPEND (CONS h t) ((CONS h t):'a list)`--);
55LIST_CONV (--`APPEND (CONS h1 t1) ((SNOC h2 t2):'a list)`--);
56LIST_CONV (--`APPEND (CONS h t) (l1:'a list)`--);
57LIST_CONV (--`APPEND (l1:'a list) (CONS h t)`--);
58
59LIST_CONV (--`FLAT (CONS h t :'a list list)`--);
60LIST_CONV (--`FLAT (SNOC h t :'a list list)`--);
61LIST_CONV (--`FLAT ([] :'a list list)`--);
62LIST_CONV (--`FLAT (FLAT (l :'a list list list))`--);
63LIST_CONV (--`FLAT (APPEND l1 l2 :'a list list)`--);
64LIST_CONV (--`FLAT ([[h]] :'a list list)`--);
65
66LIST_CONV (--`ALL_EL P ([]:'a list)`--);
67LIST_CONV (--`ALL_EL P (CONS h t:'a list)`--);
68LIST_CONV (--`ALL_EL P (SNOC h t:'a list)`--);
69LIST_CONV (--`ALL_EL P (APPEND l1 l2:'a list)`--);
70LIST_CONV (--`ALL_EL P (REVERSE (l:num list))`--);
71LIST_CONV (--`ALL_EL P (FLAT (l:'a list list))`--);
72
73LIST_CONV (--`SOME_EL P ([]:'a list)`--);
74LIST_CONV (--`SOME_EL P (CONS h t:'a list)`--);
75LIST_CONV (--`SOME_EL P (SNOC h t:'a list)`--);
76LIST_CONV (--`SOME_EL P (APPEND l1 l2:'a list)`--);
77LIST_CONV (--`SOME_EL P (REVERSE (l:'a list))`--);
78LIST_CONV (--`SOME_EL P (FLAT (l:'a list list))`--);
79
80LIST_CONV (--`IS_EL P ([]:'a list)`--);
81LIST_CONV (--`IS_EL P (CONS h t:'a list)`--);
82LIST_CONV (--`IS_EL P (SNOC h t:'a list)`--);
83LIST_CONV (--`IS_EL P (APPEND l1 l2:'a list)`--);
84LIST_CONV (--`IS_EL x (REVERSE (l:'a list))`--);
85LIST_CONV (--`IS_EL P (FLAT (l:'a list list))`--);
86
87LIST_CONV (--`SUM []`--);
88LIST_CONV (--`SUM (CONS h t)`--);
89LIST_CONV (--`SUM (SNOC h t)`--);
90LIST_CONV (--`SUM (APPEND l1 l2)`--);
91LIST_CONV (--`SUM (REVERSE (l:num list))`--);
92LIST_CONV (--`SUM (FLAT l)`--);
93
94LIST_CONV (--`AND_EL []`--);
95LIST_CONV (--`AND_EL (CONS h t)`--);
96LIST_CONV (--`AND_EL (SNOC h t)`--);
97LIST_CONV (--`AND_EL (APPEND l1 l2)`--);
98LIST_CONV (--`AND_EL (REVERSE l)`--);
99LIST_CONV (--`AND_EL (FLAT l)`--);
100
101LIST_CONV (--`OR_EL []`--);
102LIST_CONV (--`OR_EL (CONS h t)`--);
103LIST_CONV (--`OR_EL (SNOC h t)`--);
104LIST_CONV (--`OR_EL (APPEND l1 l2)`--);
105LIST_CONV (--`OR_EL (REVERSE l)`--);
106LIST_CONV (--`OR_EL (FLAT l)`--);
107
108
109LIST_CONV (--`REVERSE ([]:'a list)`--);
110LIST_CONV (--`REVERSE (CONS h t:'a list)`--);
111LIST_CONV (--`REVERSE (SNOC h t:'a list)`--);
112LIST_CONV (--`REVERSE (APPEND l1 l2:'a list)`--);
113LIST_CONV (--`REVERSE (FLAT l:'a list list)`--);
114
115LIST_CONV (--`PREFIX P ([]:'a list)`--);
116LIST_CONV (--`PREFIX P (CONS x l:'a list)`--);
117
118LIST_CONV (--`SUFFIX P ([]:'a list)`--);
119LIST_CONV (--`SUFFIX P (SNOC x l:'a list)`--);
120
121LIST_CONV (--`(FLAT o REVERSE) ([]:'a list list)`--);
122LIST_CONV (--`(FLAT o REVERSE) (CONS x l:'a list list)`--);
123LIST_CONV (--`(FLAT o REVERSE) (APPEND l1 l2:'a list list)`--);
124LIST_CONV (--`(FLAT o REVERSE) (FLAT l:'a list list)`--);
125
126val db = list_thm_database ();
127
128val COMM_ADD = prove((--`COMM $+`--),
129   REWRITE_TAC[definition "operator" "COMM_DEF"] THEN
130   REPEAT GEN_TAC THEN
131   SUBST1_TAC(SPECL[(--`x:num`--),(--`y:num`--)]
132                   (theorem "arithmetic"  "ADD_SYM")) THEN
133   REWRITE_TAC[]);
134
135val ASSOC_DEF = definition "operator" "ASSOC_DEF";
136val RIGHT_ID_DEF = definition "operator" "RIGHT_ID_DEF";
137val LEFT_ID_DEF = definition "operator" "LEFT_ID_DEF";
138val MONOID_DEF = definition "operator" "MONOID_DEF";
139
140val ADD_SYM = theorem "arithmetic"   "ADD_SYM";
141val ADD_ASSOC = theorem "arithmetic" "ADD_ASSOC";
142val ADD = definition "arithmetic"  "ADD";
143val ADD_CLAUSES = theorem "arithmetic"  "ADD_CLAUSES";
144
145val ASSOC_ADD = TAC_PROOF(([],    --`ASSOC $+`--),
146    REWRITE_TAC[ASSOC_DEF,ADD_ASSOC]);
147
148val RIGHT_ID_ADD_0 = TAC_PROOF(([], --`RIGHT_ID $+ 0`--),
149    REWRITE_TAC[RIGHT_ID_DEF,ADD_CLAUSES]);
150
151val LEFT_ID_ADD_0 = TAC_PROOF(([],    --`LEFT_ID $+ 0`--),
152    REWRITE_TAC[LEFT_ID_DEF,ADD_CLAUSES]);
153
154val MONOID_ADD_0 = TAC_PROOF(([],  --`MONOID $+ 0`--),
155    REWRITE_TAC[MONOID_DEF,ASSOC_ADD,
156        LEFT_ID_ADD_0,RIGHT_ID_ADD_0]);
157
158
159set_list_thm_database
160     {Fold_thms =[theorem "List" "SUM_FOLDR", theorem "List" "SUM_FOLDL"],
161      Aux_thms = [MONOID_ADD_0, COMM_ADD]};
162
163LIST_CONV (--`SUM []`--);
164LIST_CONV (--`SUM (CONS h t)`--);
165LIST_CONV (--`SUM (SNOC h t)`--);
166LIST_CONV (--`SUM (APPEND l1 l2)`--);
167LIST_CONV (--`SUM (REVERSE (l:num list))`--);
168LIST_CONV (--`SUM (FLAT l)`--);
169
170set_list_thm_database {Fold_thms = [],  Aux_thms = []};
171
172X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []}
173               (--`SUM []`--);
174X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []}
175               (--`SUM (CONS h t)`--);
176X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDL"], Aux_thms = []}
177               (--`SUM (SNOC h t)`--);
178X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"],
179                Aux_thms = [MONOID_ADD_0]}
180              (--`SUM (APPEND l1 l2)`--);
181X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"],
182                Aux_thms = [MONOID_ADD_0]}
183              (--`SUM (FLAT l)`--);
184
185
186set_list_thm_database(db);
187
188LIST_CONV (--`SUM []`--);
189LIST_CONV (--`SUM (CONS h t)`--);
190LIST_CONV (--`SUM (SNOC h t)`--);
191LIST_CONV (--`SUM (APPEND l1 l2)`--);
192LIST_CONV (--`SUM (REVERSE (l:num list))`--);
193LIST_CONV (--`SUM (FLAT l)`--);
194
195
196PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []}
197               (--`SUM []`--);
198PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []}
199               (--`SUM (CONS h t)`--);
200PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDL"], Aux_thms = []}
201               (--`SUM (SNOC h t)`--);
202PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"],
203                Aux_thms = [MONOID_ADD_0]}
204              (--`SUM (APPEND l1 l2)`--);
205PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"],
206                Aux_thms = [MONOID_ADD_0]}
207              (--`SUM (FLAT l)`--);
208
209
210
211
212
213
214(*
215new_theory "foo";
216val MULTL_FOLDR = new_definition ("MULTL_FOLDR",
217       (--`MULTL l = FOLDR $* 1 l`--)
218      );
219val MULTL_FOLDL = new_definition ("MULTL_FOLDL",
220       (--`MULTL_FOLDL l = FOLDL $* 1 l`--)
221      );
222
223?? ML type errors
224LIST_CONV ([MULTL_FOLDR], []) (--`MULTL []`--);
225LIST_CONV ([MULTL_FOLDR], []) (--`MULTL (CONS h t)`--);
226LIST_CONV ([MULTL_FOLDL], []) (--`MULTL_FOLDL (SNOC h t)`--);
227*)
228
229
230
231(* EVALUATION CONVERSIONS *)
232
233SUM_CONV (--`SUM []`--);
234SUM_CONV (--`SUM [1]`--);
235SUM_CONV (--`SUM [1;2;3;4]`--);
236
237
238EL_CONV (--`EL 0 ([]:num list)`--);
239EL_CONV (--`EL 0 [0]`--);
240EL_CONV (--`EL 0 [0;1;2;3]`--);
241EL_CONV (--`EL 1 [0;1;2;3]`--);
242EL_CONV (--`EL 3 [0;1;2;3]`--);
243EL_CONV (--`EL 3 [T;F;F;T]`--);
244
245ELL_CONV (--`ELL 0 ([0]:num list)`--);
246ELL_CONV (--`ELL 0 ([0;1;2;3]:num list)`--);
247ELL_CONV (--`ELL 1 ([0;1;2;3]:num list)`--);
248ELL_CONV (--`ELL 3 ([0;1;2;3]:num list)`--);
249ELL_CONV (--`ELL 3 [T;F;F;T]`--);
250
251FLAT_CONV (--`FLAT [[1;2;3;4];[2;3;4];[3;4]]`--);
252FLAT_CONV (--`FLAT [[];[];([]:'a list)]`--);
253FLAT_CONV (--`FLAT [[];[1];[]]`--);
254
255APPEND_CONV (--`APPEND [1;2;3;4] [2;3;4]`--);
256
257LENGTH_CONV (--`LENGTH [1;2;3;4]`--);
258REVERSE_CONV(--`REVERSE [1;2;3;4]`--);
259REVERSE_CONV(--`REVERSE [1]`--);
260REVERSE_CONV(--`REVERSE ([]:'a list)`--);
261
262SNOC_CONV(--`SNOC 5 []`--);
263SNOC_CONV(--`SNOC 5 [1;2;3;4]`--);
264
265LAST_CONV (--`LAST [1;2;3;4]`--);
266BUTLAST_CONV (--`BUTLAST [1;2;3;4]`--);
267
268SEG_CONV (--`SEG 2 3 [0;1;2;3;4;5;6]`--);
269SEG_CONV (--`SEG 4 3 [0;1;2;3;4;5;6]`--);
270SEG_CONV (--`SEG 4 0 [0;1;2;3;4;5;6]`--);
271
272REPLICATE_CONV (--`REPLICATE 4 4`--);
273REPLICATE_CONV (--`REPLICATE 0 4`--);
274
275REPLICATE_CONV (--`REPLICATE 3 (x:bool)`--);
276REPLICATE_CONV (--`REPLICATE 3 (SUC 3)`--);
277REPLICATE_CONV (--`REPLICATE 3 T`--);
278REPLICATE_CONV (--`REPLICATE 3 (1 + (2+ 3))`--);
279REPLICATE_CONV (--`REPLICATE 3 [1;2;3]`--);
280REPLICATE_CONV (--`REPLICATE 0 [1;2;3]`--);
281
282
283FIRSTN_CONV(--`FIRSTN 2 [1;2;3;4]`--);
284FIRSTN_CONV(--`FIRSTN 3 [1;2;3;4]`--);
285
286BUTLASTN_CONV (--`BUTLASTN 2 [1;2;3;4]`--);
287
288BUTFIRSTN_CONV (--`BUTFIRSTN 2 [1;2;3;4]`--);
289
290LASTN_CONV (--`LASTN 2 [1;2;3;4]`--);
291LASTN_CONV (--`LASTN 1 [1;2;3;4]`--);
292
293MAP_CONV LENGTH_CONV (--`MAP LENGTH [[1;2;3;4];[2;3;4];[3;4]]`--);
294
295FOLDR_CONV APPEND_CONV (--`FOLDR APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--);
296FOLDL_CONV APPEND_CONV (--`FOLDL APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--);
297
298GENLIST_CONV (BETA_CONV THENC (TOP_DEPTH_CONV num_CONV))
299             (--`GENLIST (\n . SUC n) 4`--);
300
301SCANL_CONV APPEND_CONV (--`SCANL APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--);
302SCANR_CONV APPEND_CONV (--`SCANR APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--);
303
304MAP2_CONV APPEND_CONV
305     (--`MAP2 APPEND  [[1;2;3;4];[2;3;4];[3;4]] [[1;2;3;4];[2;3;4];[3;4]]`--);
306
307FILTER_CONV BETA_CONV (--`FILTER (\x. T) [1;2;3;4]`--);
308FILTER_CONV BETA_CONV (--`FILTER (\x. F) [1;2;3;4]`--);
309
310ALL_EL_CONV BETA_CONV (--`ALL_EL (\x. F) [1;2;3;4]`--);
311ALL_EL_CONV BETA_CONV (--`ALL_EL (\x. T) [1;2;3;4]`--);
312ALL_EL_CONV BETA_CONV (--`ALL_EL (\x. T) ([]:num list)`--);
313ALL_EL_CONV (BETA_CONV THENC bool_EQ_CONV) (--`ALL_EL (\x. x = F) [T;T;F;F]`--);
314ALL_EL_CONV (BETA_CONV THENC bool_EQ_CONV) (--`ALL_EL (\x. x = T) [T;T;F;F]`--);
315ALL_EL_CONV (BETA_CONV THENC bool_EQ_CONV) (--`ALL_EL (\x. x = T) [T;T;T]`--);
316
317SOME_EL_CONV BETA_CONV (--`SOME_EL (\x. F) [1;2;3;4]`--);
318SOME_EL_CONV BETA_CONV (--`SOME_EL (\x. T) [1;2;3;4]`--);
319SOME_EL_CONV BETA_CONV (--`SOME_EL (\x. T) ([]:num list)`--);
320
321IS_EL_CONV bool_EQ_CONV (--`IS_EL T [F;F;F;F]`--);
322IS_EL_CONV bool_EQ_CONV (--`IS_EL F [T;T;F;F]`--);
323IS_EL_CONV bool_EQ_CONV (--`IS_EL F []`--);
324
325AND_EL_CONV (--`AND_EL []`--);
326AND_EL_CONV (--`AND_EL [T]`--);
327AND_EL_CONV (--`AND_EL [F]`--);
328AND_EL_CONV (--`AND_EL [T;F;T;F]`--);
329AND_EL_CONV (--`AND_EL [F;F;F;F]`--);
330
331OR_EL_CONV (--`OR_EL []`--);
332OR_EL_CONV (--`OR_EL [T]`--);
333OR_EL_CONV (--`OR_EL [F]`--);
334OR_EL_CONV (--`OR_EL [T;F;T;F]`--);
335OR_EL_CONV (--`OR_EL [F;F;F;F]`--);
336
337
338(*
339NULL_CONV (--`NULL ([]:'a list)`--);
340NULL_CONV (--`NULL [T]`--);
341NULL_CONV (--`NULL [1;2;3]`--);
342NULL_CONV (--`NULL [[1;2;3];[1]]`--);
343
344HD_CONV (--`HD [1]`--);
345HD_CONV (--`HD [1;2;3]`--);
346
347TL_CONV (--`TL [1]`--);
348TL_CONV (--`TL [1;2;3]`--);
349*)
350
351
352list_EQ_CONV bool_EQ_CONV (--`[] = ([]:bool list)`--);
353list_EQ_CONV bool_EQ_CONV (--`[T] = [F]`--);
354list_EQ_CONV bool_EQ_CONV (--`[T;F;T;F] = [F;T;F;F]`--);
355
356list_EQ_CONV bool_EQ_CONV (--`[T;F;T;F] = [F]`--); (* FAILS *)
357list_EQ_CONV bool_EQ_CONV (--`[T;F;T;F] = [T;F;T]`--); (* FAILS *)
358list_EQ_CONV bool_EQ_CONV (--`[T] = []`--); (* FAILS *)
359list_EQ_CONV bool_EQ_CONV (--`[] = [T]`--); (* FAILS *)
360
361(*
362g `!l. APPEND [1] l = CONS 1 l`;
363e SNOC_INDUCT_TAC;
364b();
365e LIST_INDUCT_TAC;
366
367g `!l1 l2.( LENGTH l1 = LENGTH l2) ==> (APPEND [1] l1 = CONS 1 l2)`;
368e EQ_LENGTH_INDUCT_TAC;
369b();
370e EQ_LENGTH_SNOC_INDUCT_TAC;
371*)
372
373
374(* (KLS) The following is unnecessary, since "define_type" has not been
375   changed. But anyway, we'll leave it.
376
377new_theory "temp";
378
379val void_Axiom = define_type{name="void_Axiom" ,
380                             type_spec= `void = Void`,
381                             fixities = [Prefix]};
382
383val pair = define_type{name="pair",
384                       type_spec= `pair = CONST of 'a#'b`,
385                       fixities = [Prefix]};
386
387val onetest = define_type{name="onetest",
388                          type_spec=`onetest = OOOO of one`,
389                          fixities = [Prefix]};
390
391val tri_Axiom =  define_type{name="tri_Axiom",
392                            type_spec=`tri = Hi | Lo | Fl`,
393                            fixities = [Prefix,Prefix,Prefix]};
394
395val iso_Axiom =  define_type{name="iso_Axiom",
396                             type_spec=`iso = ISO of 'a`,
397                             fixities = [Prefix]};
398
399val List_Axiom = define_type{name="List_Axiom",
400                             type_spec=`List = Nil | CCC of 'a => List`,
401                             fixities = [Prefix,Infix 40]};
402
403val ty_Axiom = define_type{name="ty_Axiom",
404        type_spec = `ty = C1 of 'a
405                        | C2
406                        | C3 of 'a => 'b => ty
407                        | C4 of ty => 'c => ty => 'a => 'b
408                        | C5 of ty => ty`,
409        fixities = [Prefix, Prefix, Prefix, Prefix, Prefix]};
410
411define_type{name="bintree",
412            type_spec=`bintree = LEAF of 'a
413                               | TREE of bintree => bintree`,
414            fixities = [Prefix,Prefix]};
415
416define_type{name="seven",
417            type_spec= `typ = C of one
418                                   => (one#one)
419                                   => (one -> one-> 'a list)
420                                   => ('a,one#one,'a list) ty`,
421            fixities = [Prefix]};
422
423define_type{name="seven'",
424            type_spec= `Typ = D of one # (one#one) # (one -> one -> 'a list)
425                                   # ('a,one#one,'a list) ty`,
426            fixities = [Prefix]};
427*)
428