1open HolKernel Parse boolLib;
2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->;
3infixr -->;
4
5
6val _ = new_theory "more_list";
7
8
9(*
10app load [
11          "numTheory", "listTheory", "rich_listTheory", "listLib", "pred_setLib",
12          "more_setTheory",
13          "arithLib", "Psyntax" ];
14*)
15
16open combinTheory numTheory arithmeticTheory
17     listTheory rich_listTheory listLib more_setTheory
18     numLib Psyntax ;
19
20
21open tactics;
22
23
24
25val MAP2_APPEND = store_thm
26   ("MAP2_APPEND",
27    ���!s1 s2 t1 t2 (f:'a->'b->'c).
28          (LENGTH s1 = LENGTH s2) ==>
29          (MAP2 f (APPEND s1 t1) (APPEND s2 t2) =
30          APPEND (MAP2 f s1 s2) (MAP2 f t1 t2))���,
31    LIST_INDUCT_TAC
32    THENL
33       [ LIST_INDUCT_TAC
34         THEN REWRITE_TAC[LENGTH,APPEND,MAP2,SUC_NOT],
35
36         GEN_TAC
37         THEN LIST_INDUCT_TAC
38         THEN REWRITE_TAC[LENGTH,NOT_SUC]
39         THEN REWRITE_TAC[ADD1,EQ_MONO_ADD_EQ]
40         THEN REWRITE_TAC[APPEND,MAP2]
41         THEN REPEAT GEN_TAC
42         THEN DISCH_TAC
43         THEN RES_TAC
44         THEN ASM_REWRITE_TAC[]
45      ]
46   );
47
48val AND_EL = store_thm
49   ("AND_EL",
50    ���(AND_EL [] = T) /\
51        (!x l. AND_EL (CONS x l) = (x /\ AND_EL l))���,
52    REWRITE_TAC[AND_EL_DEF]
53    THEN REWRITE_TAC[ALL_EL]
54    THEN REWRITE_TAC[combinTheory.I_THM]
55   );
56
57val AND_EL_APPEND = store_thm
58   ("AND_EL_APPEND",
59    ���!s t. AND_EL (APPEND s t) = (AND_EL s /\ AND_EL t)���,
60    REWRITE_TAC[AND_EL_DEF]
61    THEN LIST_INDUCT_TAC
62    THEN REWRITE_TAC[APPEND,ALL_EL]
63    THEN ASM_REWRITE_TAC[CONJ_ASSOC]
64   );
65
66(* =============================================================== *)
67(* LENGTH_FILTER says that if we filter a list into two using P    *)
68(* as a predicate, then the sum of the lengths of the two parts    *)
69(* must equal the length of the whole.                             *)
70(* =============================================================== *)
71
72val LENGTH_FILTER = store_thm
73   ("LENGTH_FILTER",
74    ���!(l:'a list) P.
75          LENGTH (FILTER P l) + LENGTH (FILTER ($~ o P) l) = LENGTH l���,
76    LIST_INDUCT_TAC
77    THEN REWRITE_TAC[FILTER]
78    THENL
79       [ REWRITE_TAC[LENGTH,ADD_0],
80
81         REWRITE_TAC[o_THM]
82         THEN REPEAT GEN_TAC
83         THEN COND_CASES_TAC
84         THEN ASM_REWRITE_TAC[LENGTH,ADD_CLAUSES]
85      ]
86   );
87
88(* =============================================================== *)
89(* Applying LENGTH_FILTER to a specific filter, we can calculate   *)
90(* the length of the partitions of num lists where the partition   *)
91(* separates the bottom of a range from the larger members.        *)
92(* For all lists of numbers l, the number of elements of value n   *)
93(* or more equals the number of elements of value n plus the       *)
94(* number of elements of value more than n.                        *)
95(* =============================================================== *)
96
97Theorem LENGTH_FILTER_LESS_EQ:
98  !l n.  LENGTH (FILTER (\y. n = y) l) + LENGTH (FILTER (\y. n < y) l) =
99         LENGTH (FILTER (\y. n <= y) l)
100Proof
101    REWRITE_TAC
102    [(GENL [���l:num list���,���n:num���]
103      o REWRITE_RULE[ARITH_PROVE ��� (n=y) /\ (n <= y) <=> (n = y)���,
104                     ARITH_PROVE ���~(n=y) /\ (n <= y) <=> (n < y)���]
105      o CONV_RULE (DEPTH_CONV BETA_CONV)
106      o REWRITE_RULE[FILTER_FILTER,o_THM]
107      o ISPECL[���FILTER (\y. n <= y) l���,���\y:num. n = y���])
108     LENGTH_FILTER]
109QED
110
111
112(*
113FILTER_MAP;
114    |- !f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 o f2) l)
115*)
116
117
118val SL =
119    new_recursive_definition
120      {rec_axiom = listTheory.list_Axiom,
121       name      = "SL",
122       def       = ���(SL NIL = {}) /\
123                       (SL (CONS (y:'a) l) = y INSERT (SL l))���};
124
125
126val SL_APPEND = store_thm
127  ("SL_APPEND",
128 ���!(l1: 'a list) l2. SL (APPEND l1 l2) = (SL l1 UNION SL l2)���,
129    LIST_INDUCT_TAC
130    THEN ASM_REWRITE_TAC[APPEND,SL,UNION]
131   );
132
133
134val SL_FLAT = store_thm
135  ("SL_FLAT",
136 ���!(l: 'a list list). SL (FLAT l) = UNION_SET (SL (MAP SL l))���,
137    LIST_INDUCT_TAC
138    THEN REWRITE_TAC[FLAT,MAP,SL,UNION_SET]
139    THEN ASM_REWRITE_TAC[SL_APPEND]
140   );
141
142val SL_MAP = store_thm
143  ("SL_MAP",
144 ���!l (f: 'a->'b). SL (MAP f l) = IMAGE f (SL l)���,
145    LIST_INDUCT_TAC
146    THEN ASM_REWRITE_TAC[MAP,SL,IMAGE]
147   );
148
149val DELETE_DIFF_SL =
150 store_thm
151  ("DELETE_DIFF_SL",
152   ���!xs s (e:'a).
153        s DELETE e DIFF SL xs = s DIFF SL (e::xs)���,
154   LIST_INDUCT_TAC
155   THEN REWRITE_TAC[SL,DIFFF]
156  );
157
158
159val DL =
160    new_recursive_definition
161      {rec_axiom = listTheory.list_Axiom,
162       name      = "DL",
163       def       = ���(DL NIL = T) /\
164                       (DL (CONS (y:'a) l) = (~(y IN SL l) /\ DL l))���};
165
166
167
168val _ = export_theory();
169
170val _ = print_theory_to_file "-" "more_list.lst";
171
172val _ = html_theory "more_list";
173