containerScript.sml

1(*---------------------------------------------------------------------------
2       Mapping finite sets (and bags) into lists. Needs a constraint
3       that the set (bag) is finite. One might think to introduce this
4       function via a constant specification, but in this case,
5       TFL technology makes an easy job of it.
6 ---------------------------------------------------------------------------*)
7Theory container
8Ancestors
9  pred_set list bag sorting finite_map
10Libs
11  Defn TotalDefn BasicProvers listSimps
12
13
14(* ---------------------------------------------------------------------*)
15(* Create the new theory.                                               *)
16(* ---------------------------------------------------------------------*)
17
18(* this theory may be for the chop; the set-related theorems are now all
19     in listTheory.  The bag-related ones might end up there too if we
20     decided to allow bag to move back in the build order.  Alternatively,
21     the bag-related theorems could just go into bagTheory... *)
22
23Theorem SET_TO_LIST_THM = listTheory.SET_TO_LIST_THM
24Theorem SET_TO_LIST_IND = listTheory.SET_TO_LIST_IND;
25
26(*---------------------------------------------------------------------------
27      Map a list into a set.
28 ---------------------------------------------------------------------------*)
29
30Theorem LIST_TO_SET_THM = listTheory.LIST_TO_SET_THM
31
32(*---------------------------------------------------------------------------
33            Some consequences
34 ---------------------------------------------------------------------------*)
35
36Theorem SET_TO_LIST_INV = listTheory.SET_TO_LIST_INV
37Theorem SET_TO_LIST_CARD = listTheory.SET_TO_LIST_CARD
38Theorem SET_TO_LIST_IN_MEM =
39                                  listTheory.SET_TO_LIST_IN_MEM
40Theorem MEM_SET_TO_LIST = listTheory.MEM_SET_TO_LIST
41Theorem SET_TO_LIST_SING = listTheory.SET_TO_LIST_SING
42Theorem UNION_APPEND = listTheory.UNION_APPEND;
43Theorem LIST_TO_SET_APPEND =
44                                  listTheory.LIST_TO_SET_APPEND
45Theorem FINITE_LIST_TO_SET =
46                                  listTheory.FINITE_LIST_TO_SET
47
48(*---------------------------------------------------------------------------
49    Lists and bags. Note that we also have SET_OF_BAG and BAG_OF_SET
50    in bagTheory.
51 ---------------------------------------------------------------------------*)
52
53Definition LIST_TO_BAG_def[simp]:
54     (LIST_TO_BAG [] = {||})
55 /\  (LIST_TO_BAG (h::t) = BAG_INSERT h (LIST_TO_BAG t))
56End
57
58Theorem LIST_TO_BAG_alt:
59    !l x. LIST_TO_BAG l x = LENGTH (FILTER ($= x) l)
60Proof
61  EVERY [ REPEAT GEN_TAC, Induct_on `l`,
62    SIMP_TAC list_ss [LIST_TO_BAG_def, EMPTY_BAG_alt, BAG_INSERT],
63    GEN_TAC, COND_CASES_TAC THENL [ BasicProvers.VAR_EQ_TAC, ALL_TAC],
64    ASM_SIMP_TAC arith_ss [LENGTH] ]
65QED
66
67val BAG_TO_LIST = Hol_defn "BAG_TO_LIST"
68    `BAG_TO_LIST bag =
69       if FINITE_BAG bag
70         then if bag = EMPTY_BAG then []
71              else BAG_CHOICE bag :: BAG_TO_LIST (BAG_REST bag)
72         else ARB`;
73
74val (BAG_TO_LIST_EQN,BAG_TO_LIST_IND) =
75Defn.tprove
76 (BAG_TO_LIST,
77  WF_REL_TAC `measure BAG_CARD`
78   THEN PROVE_TAC [PSUB_BAG_CARD, PSUB_BAG_REST]);
79
80Theorem BAG_TO_LIST_THM =
81 DISCH_ALL (ASM_REWRITE_RULE [ASSUME ``FINITE_BAG bag``] BAG_TO_LIST_EQN);
82
83Theorem BAG_TO_LIST_IND = BAG_TO_LIST_IND;
84
85(*---------------------------------------------------------------------------
86       Some consequences.
87 ---------------------------------------------------------------------------*)
88
89Theorem BAG_TO_LIST_INV:
90 !b. FINITE_BAG b ==> (LIST_TO_BAG(BAG_TO_LIST b) = b)
91Proof
92 recInduct BAG_TO_LIST_IND
93   THEN RW_TAC bool_ss []
94   THEN ONCE_REWRITE_TAC [UNDISCH BAG_TO_LIST_THM]
95   THEN RW_TAC bool_ss [LIST_TO_BAG_def]
96   THEN PROVE_TAC [BAG_INSERT_CHOICE_REST,FINITE_SUB_BAG,SUB_BAG_REST]
97QED
98
99Theorem BAG_IN_MEM:
100 !b. FINITE_BAG b ==> !x. BAG_IN x b = MEM x (BAG_TO_LIST b)
101Proof
102 recInduct BAG_TO_LIST_IND
103   THEN RW_TAC bool_ss []
104   THEN ONCE_REWRITE_TAC [UNDISCH BAG_TO_LIST_THM]
105   THEN RW_TAC bool_ss [listTheory.MEM,NOT_IN_EMPTY_BAG]
106   THEN PROVE_TAC [FINITE_SUB_BAG,SUB_BAG_REST,
107                   BAG_INSERT_CHOICE_REST,BAG_IN_BAG_INSERT]
108QED
109
110(* version with the equation the "rewrite" way round *)
111Theorem MEM_BAG_TO_LIST[simp]:
112  !b. FINITE_BAG b ==> !x. MEM x (BAG_TO_LIST b) = BAG_IN x b
113Proof
114  PROVE_TAC [BAG_IN_MEM]
115QED
116
117
118Theorem FINITE_LIST_TO_BAG[simp]:
119 FINITE_BAG (LIST_TO_BAG ls)
120Proof
121Induct_on `ls` THEN SRW_TAC [][LIST_TO_BAG_def]
122QED
123
124
125Theorem EVERY_LIST_TO_BAG:
126 BAG_EVERY P (LIST_TO_BAG ls) <=> EVERY P ls
127Proof
128Induct_on `ls` THEN SRW_TAC [][LIST_TO_BAG_def]
129QED
130
131
132Theorem LIST_TO_BAG_APPEND:
133  !l1 l2.
134LIST_TO_BAG (l1 ++ l2) =
135BAG_UNION (LIST_TO_BAG l1) (LIST_TO_BAG l2)
136Proof
137Induct_on `l1` THENL [
138  SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_UNION_EMPTY],
139  ASM_SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_UNION_INSERT]
140]
141QED
142
143Theorem LIST_TO_BAG_MAP:
144    LIST_TO_BAG (MAP f b) = BAG_IMAGE f (LIST_TO_BAG b)
145Proof
146  EVERY [ Induct_on `b`,
147    ASM_SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_IMAGE_EMPTY],
148    GEN_TAC, irule (GSYM BAG_IMAGE_FINITE_INSERT),
149    irule FINITE_LIST_TO_BAG]
150QED
151
152Theorem LIST_TO_BAG_FILTER:
153    LIST_TO_BAG (FILTER f b) = BAG_FILTER f (LIST_TO_BAG b)
154Proof
155  EVERY [ Induct_on `b`,
156    ASM_SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_FILTER_EMPTY],
157    GEN_TAC, COND_CASES_TAC,
158    ASM_SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_FILTER_BAG_INSERT] ]
159QED
160
161
162Theorem INN_LIST_TO_BAG:
163  !n h l. BAG_INN h n (LIST_TO_BAG l) = (LENGTH (FILTER ($= h) l) >= n)
164Proof
165Induct_on `l` THENL [
166  SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_INN_EMPTY_BAG],
167  ASM_SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_INN_BAG_INSERT, COND_RAND, COND_RATOR]
168]
169QED
170
171
172Theorem IN_LIST_TO_BAG:
173  !h l. BAG_IN h (LIST_TO_BAG l) = MEM h l
174Proof
175Induct_on `l` THENL [
176  SIMP_TAC list_ss [LIST_TO_BAG_def, NOT_IN_EMPTY_BAG],
177  ASM_SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_IN_BAG_INSERT]
178]
179QED
180
181Theorem LIST_TO_BAG_DISTINCT:
182    BAG_ALL_DISTINCT (LIST_TO_BAG b) = ALL_DISTINCT b
183Proof
184  Induct_on `b` THEN
185    ASM_SIMP_TAC (srw_ss ()) [LIST_TO_BAG_def, IN_LIST_TO_BAG]
186QED
187
188Theorem LIST_TO_BAG_EQ_EMPTY:
189  !l. (LIST_TO_BAG l = EMPTY_BAG) = (l = [])
190Proof
191Cases_on `l` THEN
192SIMP_TAC list_ss [LIST_TO_BAG_def, BAG_INSERT_NOT_EMPTY]
193QED
194
195
196Theorem PERM_LIST_TO_BAG:
197    !l1 l2. (LIST_TO_BAG l1 = LIST_TO_BAG l2) = PERM l1 l2
198Proof
199  REPEAT GEN_TAC THEN SIMP_TAC std_ss [PERM_DEF] THEN EQ_TAC THENL [
200    EVERY [ REPEAT STRIP_TAC,
201      POP_ASSUM (fn th => ASSUME_TAC (Q.AP_THM th `x`)),
202      FULL_SIMP_TAC std_ss [LIST_TO_BAG_alt],
203      ONCE_REWRITE_TAC [FILTER_EQ_REP], ASM_SIMP_TAC std_ss [] ],
204    DISCH_TAC THEN irule EQ_EXT THEN ASM_SIMP_TAC std_ss [LIST_TO_BAG_alt] ]
205QED
206
207Theorem CARD_LIST_TO_BAG[simp]:
208  BAG_CARD (LIST_TO_BAG ls) = LENGTH ls
209Proof
210  Induct_on `ls` THEN SRW_TAC [][BAG_CARD_THM,arithmeticTheory.ADD1]
211QED
212
213val EQ_TRANS' = REWRITE_RULE [GSYM AND_IMP_INTRO] EQ_TRANS ;
214val th = MATCH_MP EQ_TRANS' (SYM CARD_LIST_TO_BAG) ;
215
216Theorem BAG_TO_LIST_CARD:
217    !b. FINITE_BAG b ==> (LENGTH (BAG_TO_LIST b) = BAG_CARD b)
218Proof
219  EVERY [REPEAT STRIP_TAC, irule th,
220    ASM_SIMP_TAC bool_ss [BAG_TO_LIST_INV] ]
221QED
222
223Theorem BAG_TO_LIST_EQ_NIL[simp]:
224FINITE_BAG b ==>
225 (([] = BAG_TO_LIST b) <=> (b = {||})) /\
226 ((BAG_TO_LIST b = []) <=> (b = {||}))
227Proof
228Q.SPEC_THEN `b` STRUCT_CASES_TAC BAG_cases THEN
229SRW_TAC [][BAG_TO_LIST_THM]
230QED
231
232local open rich_listTheory arithmeticTheory in
233Theorem LIST_ELEM_COUNT_LIST_TO_BAG:
234     LIST_ELEM_COUNT e ls = LIST_TO_BAG ls e
235Proof
236    Induct_on `ls` THEN SRW_TAC [][LIST_ELEM_COUNT_THM,EMPTY_BAG] THEN
237    Cases_on `h = e` THEN SRW_TAC [][LIST_ELEM_COUNT_THM,BAG_INSERT,ADD1]
238QED
239end
240
241Theorem LIST_TO_BAG_SUB_BAG_FLAT_suff:
242  !ls1 ls2. LIST_REL (\l1 l2. LIST_TO_BAG l1 <= LIST_TO_BAG l2) ls1 ls2 ==>
243            LIST_TO_BAG (FLAT ls1) <= LIST_TO_BAG (FLAT ls2)
244Proof
245  Induct_on ‘LIST_REL’ >> srw_tac [bagLib.SBAG_SOLVE_ss] [LIST_TO_BAG_APPEND]
246QED
247
248Theorem LIST_TO_BAG_SUBSET:
249  !l1 l2. LIST_TO_BAG l1 <= LIST_TO_BAG l2 ==> set l1 SUBSET set l2
250Proof
251  Induct >> rw[LIST_TO_BAG_def] >> imp_res_tac BAG_INSERT_SUB_BAG_E >>
252  imp_res_tac IN_LIST_TO_BAG >> fs[]
253QED
254
255Theorem LIST_TO_BAG_SET_TO_LIST:
256  !s. FINITE s ==>
257      LIST_TO_BAG (SET_TO_LIST s) = BAG_OF_SET s
258Proof
259  ho_match_mp_tac FINITE_INDUCT
260  \\ rw[BAG_OF_SET_INSERT_NON_ELEMENT]
261  \\ irule EQ_TRANS
262  \\ qexists_tac`LIST_TO_BAG (e :: SET_TO_LIST s)`
263  \\ conj_tac
264  >- (
265    simp[PERM_LIST_TO_BAG]
266    \\ drule PERM_SET_TO_LIST_INSERT
267    \\ disch_then(qspec_then`e`mp_tac) \\ simp[] )
268  \\ simp[]
269QED
270
271(*---------------------------------------------------------------------------*)
272(* Following packaging of multiset order applied to lists is easier to use   *)
273(* in some termination proofs, typically those of worklist algorithms, where *)
274(* the head of the list is replaced by a list of smaller elements.           *)
275(*---------------------------------------------------------------------------*)
276
277Definition mlt_list_def[tfl_termsimp]:
278  mlt_list R =
279     \l1 l2.
280       ?h t list.
281         (l1 = list ++ t) /\
282         (l2 = h::t) /\
283         (!e. MEM e list ==> R e h)
284End
285
286Theorem WF_mlt_list[tfl_WF]:
287  !R. WF(R) ==> WF (mlt_list R)
288Proof
289  REPEAT STRIP_TAC THEN MATCH_MP_TAC relationTheory.WF_SUBSET THEN
290  Q.EXISTS_TAC `inv_image (mlt1 R) LIST_TO_BAG` THEN
291  CONJ_TAC THENL
292  [METIS_TAC [relationTheory.WF_inv_image,bagTheory.WF_mlt1],
293   RW_TAC list_ss [mlt_list_def, relationTheory.inv_image_thm,bagTheory.mlt1_def]
294   THENL
295   [METIS_TAC [FINITE_LIST_TO_BAG],
296    METIS_TAC [FINITE_LIST_TO_BAG],
297    MAP_EVERY Q.EXISTS_TAC [`h`, `LIST_TO_BAG list`, `LIST_TO_BAG t`]
298     THEN RW_TAC std_ss [BAG_INSERT_UNION,LIST_TO_BAG_APPEND,LIST_TO_BAG_def]
299      THENL [METIS_TAC [COMM_BAG_UNION,ASSOC_BAG_UNION,BAG_UNION_EMPTY],
300             METIS_TAC [IN_LIST_TO_BAG]]]]
301QED
302
303(*---------------------------------------------------------------------------
304    finite maps and bags.
305 ---------------------------------------------------------------------------*)
306
307Definition BAG_OF_FMAP:   BAG_OF_FMAP f b =
308  \x. CARD (\k. (k IN FDOM b) /\ (x = f k (b ' k)))
309End
310
311
312Theorem BAG_OF_FMAP_THM:
313  (!f. (BAG_OF_FMAP f FEMPTY = EMPTY_BAG)) /\
314  (!f b k v. (BAG_OF_FMAP f (b |+ (k, v)) =
315             BAG_INSERT (f k v) (BAG_OF_FMAP f (b \\ k))))
316Proof
317SIMP_TAC std_ss [BAG_OF_FMAP, FDOM_FEMPTY, NOT_IN_EMPTY, EMPTY_BAG,
318                 combinTheory.K_DEF,
319                 BAG_INSERT, FDOM_FUPDATE, IN_INSERT,
320                 GSYM EMPTY_DEF, CARD_EMPTY] THEN
321ONCE_REWRITE_TAC [FUN_EQ_THM] THEN
322REPEAT GEN_TAC THEN SIMP_TAC std_ss [] THEN
323Cases_on `x = f k v` THENL [
324   ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) [
325     FAPPLY_FUPDATE_THM, FDOM_DOMSUB, IN_DELETE,
326     DOMSUB_FAPPLY_THM] THEN
327   `(\k'. ((k' = k) \/ k' IN FDOM b) /\
328           (f k v = f k' ((if k' = k then v else b ' k')))) =
329           k INSERT (\k'. (k' IN FDOM b /\ ~(k' = k)) /\ (f k v = f k' (b ' k')))` by (
330     SIMP_TAC std_ss [EXTENSION, IN_INSERT, IN_ABS] THEN
331     GEN_TAC THEN Cases_on `x' = k` THEN ASM_REWRITE_TAC[]
332   ) THEN
333   ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN
334   Q.ABBREV_TAC `ks = (\k'. (k' IN FDOM b /\ k' <> k) /\ (f k v = f k' (b ' k')))` THEN
335   `FINITE ks` by (
336      `ks = ks INTER FDOM b` suffices_by (
337         STRIP_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN
338         MATCH_MP_TAC FINITE_INTER THEN
339         REWRITE_TAC[FDOM_FINITE]
340      ) THEN
341      Q.UNABBREV_TAC `ks` THEN
342      SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_ABS] THEN
343      PROVE_TAC[]
344   ) THEN
345   `~(k IN ks)` by (
346      Q.UNABBREV_TAC `ks` THEN
347      SIMP_TAC std_ss [IN_ABS]
348   ) THEN
349   ASM_SIMP_TAC arith_ss [CARD_INSERT],
350
351
352   FULL_SIMP_TAC (std_ss++boolSimps.CONJ_ss) [
353      FAPPLY_FUPDATE_THM, FDOM_DOMSUB, IN_DELETE,
354      DOMSUB_FAPPLY_THM] THEN
355   AP_TERM_TAC THEN
356   ONCE_REWRITE_TAC [FUN_EQ_THM] THEN
357   GEN_TAC THEN SIMP_TAC std_ss [] THEN
358   Cases_on `x' = k` THEN (
359      ASM_SIMP_TAC std_ss []
360   )
361]
362QED
363
364Theorem BAG_IN_BAG_OF_FMAP:
365  !x f b. BAG_IN x (BAG_OF_FMAP f b) <=>
366           ?k. k IN FDOM b /\ (x = f k (b ' k))
367Proof
368  SIMP_TAC std_ss [BAG_OF_FMAP, BAG_IN, BAG_INN] THEN
369  `!X. (X >= (1:num)) = ~(X = 0)` by bossLib.DECIDE_TAC THEN
370  ONCE_ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
371  REPEAT GEN_TAC THEN
372  `FINITE (\k. k IN FDOM b /\ (x = f k (b ' k)))` by (
373     `(\k. k IN FDOM b /\ (x = f k (b ' k))) =
374      (\k. k IN FDOM b /\ (x = f k (b ' k))) INTER (FDOM b)` by (
375        SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_ABS] THEN
376        METIS_TAC[]
377     ) THEN
378     ONCE_ASM_REWRITE_TAC[] THEN
379     MATCH_MP_TAC FINITE_INTER THEN
380     REWRITE_TAC[FDOM_FINITE]
381  ) THEN
382  SRW_TAC[][CARD_EQ_0, EXTENSION] THEN METIS_TAC[]
383QED
384
385Theorem FINITE_BAG_OF_FMAP:
386  !f b. FINITE_BAG (BAG_OF_FMAP f b)
387Proof
388GEN_TAC THEN HO_MATCH_MP_TAC fmap_INDUCT THEN
389SIMP_TAC std_ss [BAG_OF_FMAP_THM, FINITE_EMPTY_BAG,
390                 DOMSUB_NOT_IN_DOM, FINITE_BAG_INSERT]
391QED