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