1(* non-interactive mode
2*)
3open HolKernel Parse boolLib;
4val _ = new_theory "extra_list";
5
6(* interactive mode
7val () = loadPath := union ["..", "../finished"] (!loadPath);
8val () = app load
9  ["bossLib",
10   "pred_setTheory",
11   "realLib",
12   "pairTheory",
13   "combinTheory",
14   "res_quanLib",
15   "dividesTheory",
16   "primeTheory",
17   "gcdTheory",
18   "prob_extraTools",
19   "millerTools"];
20val () = show_assums := true;
21*)
22
23open bossLib listTheory numTheory arithmeticTheory HurdUseful
24     pred_setTheory subtypeTheory extra_numTheory rich_listTheory;
25
26infixr 0 ++ << || THENC ORELSEC ORELSER ##;
27infix 1 >>;
28
29val op++ = op THEN;
30val op<< = op THENL;
31val op|| = op ORELSE;
32val op>> = op THEN1;
33
34(* ------------------------------------------------------------------------- *)
35(* Definitions.                                                              *)
36(* ------------------------------------------------------------------------- *)
37
38val sum_def = Define `(sum [] = (0:num)) /\ (sum (n :: ns) = n + sum ns)`;
39
40val prod_def = Define `(prod [] = (1:num)) /\ (prod (n :: ns) = n * prod ns)`;
41
42val kill_dups_def = Define
43  `kill_dups = FOLDR (\(h:'a) t. if MEM h t then t else h::t) []`;
44
45val list_def = Define `list = (EVERY : ('a -> bool) -> 'a list -> bool)`;
46
47val gtlist_def = Define `gtlist n l = n < LENGTH l`;
48
49(* ------------------------------------------------------------------------- *)
50(* Theorems.                                                                 *)
51(* ------------------------------------------------------------------------- *)
52
53val MEM_NIL = store_thm
54  ("MEM_NIL",
55   ``!l. (!(x:'a). ~MEM x l) = (l = [])``,
56   Cases >> RW_TAC std_ss [MEM]
57   ++ RW_TAC std_ss [MEM]
58   ++ PROVE_TAC []);
59
60val MAP_ID = store_thm
61  ("MAP_ID",
62   ``!(l:'a list). MAP (\x. x) l = l``,
63   Induct >> RW_TAC list_ss []
64   ++ RW_TAC list_ss []);
65
66val MAP_MEM = store_thm
67  ("MAP_MEM",
68   ``!(f:'a->'b) l x. MEM x (MAP f l) = ?y. MEM y l /\ (x = f y)``,
69   Induct_on `l` >> RW_TAC list_ss [MEM]
70   ++ RW_TAC list_ss [MEM]
71   ++ EQ_TAC <<
72   [RW_TAC list_ss [] <<
73    [PROVE_TAC [],
74     PROVE_TAC []],
75    PROVE_TAC []]);
76
77val APPEND_MEM = store_thm
78  ("APPEND_MEM",
79   ``!(x:'a) l1 l2. MEM x (APPEND l1 l2) = (MEM x l1 \/ MEM x l2)``,
80   Induct_on `l1` >> RW_TAC list_ss [MEM]
81   ++ RW_TAC list_ss [MEM]
82   ++ PROVE_TAC []);
83
84val MEM_NIL_MAP_CONS = store_thm
85  ("MEM_NIL_MAP_CONS",
86   ``!(x:'a) l. ~MEM [] (MAP (CONS x) l)``,
87   STRIP_TAC
88   ++ Induct >> RW_TAC list_ss [MEM]
89   ++ RW_TAC list_ss [MEM]);
90
91val FILTER_TRUE = store_thm
92  ("FILTER_TRUE",
93   ``!(l:'a list). FILTER (\x. T) l = l``,
94   Induct >> RW_TAC list_ss [FILTER]
95   ++ RW_TAC list_ss [FILTER]);
96
97val FILTER_FALSE = store_thm
98  ("FILTER_FALSE",
99   ``!(l:'a list). FILTER (\x. F) l = []``,
100   Induct >> RW_TAC list_ss [FILTER]
101   ++ RW_TAC list_ss [FILTER]);
102
103val LENGTH_FILTER = store_thm
104  ("LENGTH_FILTER",
105   ``!P (l:'a list). LENGTH (FILTER P l) <= LENGTH l``,
106   GEN_TAC
107   ++ Induct_on `l`
108   ++ RW_TAC list_ss [FILTER]);
109
110val FILTER_MEM = store_thm
111  ("FILTER_MEM",
112   ``!P (x:'a) l. MEM x (FILTER P l) ==> P x``,
113   NTAC 2 STRIP_TAC
114   ++ Induct >> RW_TAC std_ss [MEM, FILTER]
115   ++ (RW_TAC std_ss [MEM, FILTER] ++ PROVE_TAC []));
116
117val MEM_FILTER = store_thm
118  ("MEM_FILTER",
119   ``!P l (x:'a). MEM x (FILTER P l) ==> MEM x l``,
120   STRIP_TAC
121   ++ Induct >> RW_TAC list_ss [FILTER]
122   ++ RW_TAC list_ss [FILTER, MEM]
123   ++ PROVE_TAC []);
124
125val FILTER_OUT_ELT = store_thm
126  ("FILTER_OUT_ELT",
127   ``!(x:'a) l. MEM x l \/ (FILTER (\y. ~(y = x)) l = l)``,
128   STRIP_TAC
129   ++ Induct >> RW_TAC list_ss [FILTER]
130   ++ (RW_TAC list_ss [MEM, FILTER]
131         ++ PROVE_TAC []));
132
133val IS_PREFIX_NIL = store_thm
134  ("IS_PREFIX_NIL",
135   ``!(x:'a list). IS_PREFIX x [] /\ (IS_PREFIX [] x = (x = []))``,
136   STRIP_TAC
137   ++ Cases_on `x`
138   ++ RW_TAC list_ss [IS_PREFIX]);
139
140val IS_PREFIX_REFL = store_thm
141  ("IS_PREFIX_REFL",
142   ``!(x:'a list). IS_PREFIX x x``,
143   Induct ++ RW_TAC list_ss [IS_PREFIX]);
144
145val IS_PREFIX_ANTISYM = store_thm
146  ("IS_PREFIX_ANTISYM",
147   ``!(x:'a list) y. IS_PREFIX y x /\ IS_PREFIX x y ==> (x = y)``,
148    Induct >> RW_TAC list_ss [IS_PREFIX_NIL]
149    ++ Cases_on `y` >> RW_TAC list_ss [IS_PREFIX_NIL]
150    ++ ONCE_REWRITE_TAC [IS_PREFIX]
151    ++ PROVE_TAC []);
152
153val IS_PREFIX_TRANS = store_thm
154  ("IS_PREFIX_TRANS",
155   ``!(x:'a list) y z. IS_PREFIX x y /\ IS_PREFIX y z ==> IS_PREFIX x z``,
156   Induct >> PROVE_TAC [IS_PREFIX_NIL]
157   ++ Cases_on `y` >> RW_TAC list_ss [IS_PREFIX_NIL, IS_PREFIX]
158   ++ Cases_on `z` >> RW_TAC list_ss [IS_PREFIX_NIL, IS_PREFIX]
159   ++ RW_TAC list_ss [IS_PREFIX]
160   ++ PROVE_TAC []);
161
162val IS_PREFIX_BUTLAST = store_thm
163  ("IS_PREFIX_BUTLAST",
164   ``!x:'a y. IS_PREFIX (x::y) (BUTLAST (x::y))``,
165   Induct_on `y`
166     >> RW_TAC list_ss [BUTLAST_CONS, IS_PREFIX]
167   ++ RW_TAC list_ss [BUTLAST_CONS, IS_PREFIX]);
168
169val IS_PREFIX_LENGTH = store_thm
170  ("IS_PREFIX_LENGTH",
171   ``!(x:'a list) y. IS_PREFIX y x ==> LENGTH x <= LENGTH y``,
172   Induct >> RW_TAC list_ss [LENGTH]
173   ++ Cases_on `y` >> RW_TAC list_ss [IS_PREFIX_NIL]
174   ++ RW_TAC list_ss [IS_PREFIX, LENGTH]);
175
176val IS_PREFIX_LENGTH_ANTI = store_thm
177  ("IS_PREFIX_LENGTH_ANTI",
178   ``!(x:'a list) y. IS_PREFIX y x /\ (LENGTH x = LENGTH y) ==> (x = y)``,
179   Induct >> PROVE_TAC [LENGTH_NIL]
180   ++ Cases_on `y` >> RW_TAC list_ss [LENGTH_NIL]
181   ++ RW_TAC list_ss [IS_PREFIX, LENGTH]);
182
183val IS_PREFIX_SNOC = store_thm
184  ("IS_PREFIX_SNOC",
185   ``!(x:'a) y z. IS_PREFIX (SNOC x y) z = IS_PREFIX y z \/ (z = SNOC x y)``,
186   Induct_on `y`
187     >> (Cases_on `z`
188         ++ RW_TAC list_ss [SNOC, IS_PREFIX_NIL, IS_PREFIX]
189         ++ PROVE_TAC [])
190   ++ Cases_on `z` >> RW_TAC list_ss [IS_PREFIX]
191   ++ RW_TAC list_ss [SNOC, IS_PREFIX]
192   ++ PROVE_TAC []);
193
194val FOLDR_MAP = store_thm
195  ("FOLDR_MAP",
196   ``!(f :'b -> 'c -> 'c) (e :'c) (g :'a -> 'b) (l :'a list).
197         FOLDR f e (MAP g l) = FOLDR (\x y. f (g x) y) e l``,
198   RW_TAC list_ss []
199   ++ Induct_on `l` >> RW_TAC list_ss [MAP, FOLDR]
200   ++ RW_TAC list_ss [MAP, FOLDR]);
201
202val LAST_MEM = store_thm
203  ("LAST_MEM",
204   ``!(h:'a) t. MEM (LAST (h::t)) (h::t)``,
205   Induct_on `t` >> RW_TAC list_ss [MEM, LAST_CONS]
206   ++ RW_TAC std_ss [LAST_CONS]
207   ++ ONCE_REWRITE_TAC [MEM]
208   ++ RW_TAC std_ss []);
209
210val LAST_MAP_CONS = store_thm
211  ("LAST_MAP_CONS",
212   ``!(b:bool) h t. ?x. LAST (MAP (CONS b) (h::t)) = b::x``,
213   Induct_on `t` >> RW_TAC list_ss [LAST_CONS]
214   ++ POP_ASSUM MP_TAC
215   ++ RW_TAC list_ss [LAST_CONS]);
216
217val EXISTS_LONGEST = store_thm
218  ("EXISTS_LONGEST",
219   ``!(x:'a list) y. ?z. MEM z (x::y)
220                    /\ (!w. MEM w (x::y) ==> LENGTH w <= LENGTH z)``,
221   Induct_on `y` >> RW_TAC list_ss [MEM]
222   ++ ONCE_REWRITE_TAC [MEM]
223   ++ REPEAT STRIP_TAC
224   ++ POP_ASSUM (MP_TAC o SPEC ``h:'a list``)
225   ++ STRIP_TAC
226   ++ EXISTS_TAC ``if LENGTH z <= LENGTH x then x else (z:'a list)``
227   ++ ZAP_TAC std_ss [LESS_EQ_TRANS]);
228
229val SUM_CONST = store_thm
230  ("SUM_CONST",
231   ``!l c. (!x. MEM x l ==> (x = c)) ==> (sum l = LENGTH l * c)``,
232   Induct >> RW_TAC arith_ss [LENGTH, sum_def]
233   ++ RW_TAC std_ss [LENGTH, sum_def, MEM, MULT]
234   ++ PROVE_TAC [ADD_COMM]);
235
236val MEM_KILL_DUPS = store_thm
237  ("MEM_KILL_DUPS",
238   ``!l (x:'a). MEM x (kill_dups l) = MEM x l``,
239   Induct >> RW_TAC list_ss [MEM, kill_dups_def, FOLDR]
240   ++ REWRITE_TAC [kill_dups_def, FOLDR]
241   ++ RW_TAC std_ss [GSYM kill_dups_def, MEM]
242   ++ Cases_on `x = h` >> RW_TAC std_ss []
243   ++ RW_TAC std_ss []);
244
245val IN_LIST = store_thm
246  ("IN_LIST",
247   ``!(h:'a) t p.
248       ([] IN list p) /\ ((h::t) IN list p = h IN p /\ t IN list p)``,
249   RW_TAC std_ss [list_def, SPECIFICATION, EVERY_DEF]);
250
251val IN_GTLIST = store_thm
252  ("IN_GTLIST",
253   ``!n (l:'a list). l IN gtlist n = n < LENGTH l``,
254   RW_TAC std_ss [gtlist_def, SPECIFICATION]);
255
256val LIST_UNIV = store_thm
257  ("LIST_UNIV",
258   ``list (UNIV : 'a -> bool) = UNIV``,
259   SET_EQ_TAC
260   ++ Induct >> RW_TAC std_ss [IN_LIST, IN_UNIV]
261   ++ RW_TAC std_ss [IN_LIST, IN_UNIV]);
262
263val LIST_SUBSET = store_thm
264  ("LIST_SUBSET",
265   ``!p q. p SUBSET q ==> list p SUBSET list q``,
266   RW_TAC std_ss [SUBSET_DEF]
267   ++ Induct_on `x` >> RW_TAC std_ss [IN_LIST]
268   ++ RW_TAC std_ss [IN_LIST]);
269
270val NIL_SUBTYPE = store_thm
271  ("NIL_SUBTYPE",
272   ``!(x : 'a -> bool). [] IN list x``,
273   RW_TAC std_ss [IN_LIST, LENGTH, IN_INTER]);
274
275val CONS_SUBTYPE = store_thm
276  ("CONS_SUBTYPE",
277   ``!(x : 'a -> bool).
278       CONS IN ((x -> list x -> list x) INTER (UNIV -> UNIV -> gtlist 0) INTER
279                (UNIV -> gtlist 0 -> gtlist 1))``,
280   RW_TAC arith_ss [IN_FUNSET, IN_LIST, IN_GTLIST, LENGTH, IN_INTER]);
281
282val MAP_SUBTYPE = store_thm
283  ("MAP_SUBTYPE",
284   ``!(x:'a->bool) (y:'b->bool) n.
285       MAP IN (((x -> y) -> list x -> list y) INTER
286               (UNIV -> gtlist n -> gtlist n))``,
287   RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST, LENGTH_MAP]
288   ++ Induct_on `x''` >> RW_TAC std_ss [MAP, IN_LIST]
289   ++ RW_TAC std_ss [MAP, IN_LIST]);
290
291val HD_SUBTYPE = store_thm
292  ("HD_SUBTYPE",
293   ``!x.  HD IN ((gtlist 0 INTER list x) -> x)``,
294   RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST]
295   ++ Cases_on `x'`
296   >> (Q.PAT_X_ASSUM `0 < LENGTH []` MP_TAC
297       ++ RW_TAC arith_ss [LENGTH])
298   ++ POP_ASSUM MP_TAC
299   ++ RW_TAC std_ss [IN_LIST, HD]);
300
301val TL_SUBTYPE = store_thm
302  ("TL_SUBTYPE",
303   ``!x.  TL IN (((gtlist 0 INTER list x) -> list x) INTER
304                 (gtlist 1 -> gtlist 0))``,
305   RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST] <<
306   [Cases_on `x'`
307   >> (Q.PAT_X_ASSUM `0 < LENGTH []` MP_TAC
308       ++ RW_TAC arith_ss [LENGTH])
309    ++ POP_ASSUM MP_TAC
310    ++ RW_TAC std_ss [IN_LIST, TL],
311    POP_ASSUM MP_TAC
312    ++ Cases_on `x` >> RW_TAC arith_ss [LENGTH]
313    ++ Cases_on `t` >> RW_TAC arith_ss [LENGTH]
314    ++ RW_TAC arith_ss [LENGTH, TL]]);
315
316val LENGTH_SUBTYPE = store_thm
317  ("LENGTH_SUBTYPE",
318   ``LENGTH IN ((gtlist 0 -> gtnum 0) INTER (gtlist 1 -> gtnum 1))``,
319   RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST, IN_GTNUM]);
320
321val GTLIST0_SUBTYPE_REWRITE = store_thm
322  ("GTLIST0_SUBTYPE_REWRITE",
323   ``!l. l IN gtlist 0 ==> ~(l = []) /\ ~([] = l)``,
324   Cases
325   ++ RW_TAC arith_ss [IN_GTLIST, LENGTH]);
326
327val GTLIST1_SUBTYPE_REWRITE = store_thm
328  ("GTLIST1_SUBTYPE_REWRITE",
329   ``!l h. l IN gtlist 1 ==> ~(l = [h]) /\ ~([h] = l)``,
330   Cases >> RW_TAC arith_ss [IN_GTLIST, LENGTH]
331   ++ Cases_on `t`
332   ++ RW_TAC arith_ss [IN_GTLIST, LENGTH]);
333
334val GTLIST0_SUBTYPE_JUDGEMENT = store_thm
335  ("GTLIST0_SUBTYPE_JUDGEMENT",
336   ``!l m.
337       LENGTH l IN gtnum 0 \/ ~([] = l) \/ ~(l = []) ==> l IN gtlist 0``,
338   Cases
339   ++ RW_TAC std_ss [IN_GTLIST, IN_GTNUM, LENGTH]
340   ++ DECIDE_TAC);
341
342val GTLIST1_SUBTYPE_JUDGEMENT = store_thm
343  ("GTLIST1_SUBTYPE_JUDGEMENT",
344   ``!l m. LENGTH l IN gtnum 1 ==> l IN gtlist 1``,
345   RW_TAC std_ss [IN_GTLIST, IN_GTNUM]
346   ++ DECIDE_TAC);
347
348val GTLIST1_SUBSET_GTLIST0 = store_thm
349  ("GTLIST1_SUBSET_GTLIST0",
350   ``gtlist 1 SUBSET gtlist 0``,
351   RW_TAC std_ss [SUBSET_DEF, IN_GTLIST]
352   ++ DECIDE_TAC);
353
354(* non-interactive mode
355*)
356val _ = export_theory ();
357