1open HolKernel Parse boolLib boolSimps bossLib 2 numLib Prim_rec pred_setTheory BasicProvers 3 metisLib dividesTheory arithmeticTheory 4 combinTheory 5 6fun ARITH q = EQT_ELIM (ARITH_CONV (Parse.Term q)); 7 8val _ = new_theory "bag"; 9 10val _ = set_grammar_ancestry ["list", "divides"] 11 12val _ = type_abbrev("bag", ���:'a -> num���) 13val _ = type_abbrev("multiset", ���:'a -> num���) 14 15val _ = print "Defining basic bag operations\n" 16 17val EMPTY_BAG = new_definition ( 18 "EMPTY_BAG", 19 ``(EMPTY_BAG:'a bag) = K 0``); 20 21val EMPTY_BAG_alt = store_thm ( 22 "EMPTY_BAG_alt", 23 ``EMPTY_BAG:'a bag = \x.0``, 24 SIMP_TAC std_ss [EMPTY_BAG, FUN_EQ_THM]); 25 26val BAG_INN = new_definition( 27 "BAG_INN", 28 ``BAG_INN (e:'a) n b <=> b e >= n``); 29 30val SUB_BAG = Q.new_definition ( 31 "SUB_BAG", 32 `SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2`); 33 34val PSUB_BAG = Q.new_definition ( 35 "PSUB_BAG", 36 `PSUB_BAG b1 b2 <=> SUB_BAG b1 b2 /\ ~(b1 = b2)`); 37 38 39val BAG_IN = new_definition ( 40 "BAG_IN", 41 ``BAG_IN (e:'a) b <=> BAG_INN e 1 b``); 42 43val _ = set_fixity "<:" (Infix(NONASSOC, 425)) 44val _ = overload_on ("<:", ``BAG_IN``) 45val _ = Unicode.unicode_version {tmnm = "<:", u = UTF8.chr 0x22F2} 46 (* U+22F2 looks like ��� in your current font; unfortunately this (UOK) 47 symbol doesn't seem to correspond to anything in LaTeX... *) 48val _ = TeX_notation {hol = "<:", TeX = ("\\HOLTokenIn{}:",2)} 49val _ = TeX_notation {hol = UTF8.chr 0x22F2, TeX = ("\\HOLTokenIn{}:",2)} 50 51val BAG_UNION = new_definition ("BAG_UNION", 52 ``BAG_UNION b (c:'a bag) = \x. b x + c x``); 53val _ = overload_on ("+", ``BAG_UNION``) 54val _ = send_to_back_overload "+" {Name = "BAG_UNION", Thy = "bag"} 55val _ = set_fixity (UTF8.chr 0x228E) (Infixl 500) (* LaTeX's \uplus *) 56val _ = overload_on (UTF8.chr 0x228E, ``BAG_UNION``) 57val _ = TeX_notation {hol = UTF8.chr 0x228E, TeX = ("\\ensuremath{\\uplus}", 1)} 58 59val BAG_DIFF = new_definition ( 60 "BAG_DIFF", 61 ``BAG_DIFF b1 (b2:'a bag) = \x. b1 x - b2 x``); 62val _ = overload_on ("-", ``BAG_DIFF``) 63val _ = send_to_back_overload "-" {Name = "BAG_DIFF", Thy = "bag"} 64 65val BAG_INSERT = new_definition ( 66 "BAG_INSERT", 67 Term`BAG_INSERT (e:'a) b = (\x. if (x = e) then b e + 1 else b x)`); 68 69val _ = add_listform {cons = "BAG_INSERT", nilstr = "EMPTY_BAG", 70 separator = [TOK ";", BreakSpace(1,0)], 71 leftdelim = [TOK "{|"], rightdelim = [TOK "|}"], 72 block_info = (PP.INCONSISTENT, 2)}; 73val _ = TeX_notation { hol = "{|", TeX = ("\\HOLTokenBagLeft{}", 1) } 74val _ = TeX_notation { hol = "|}", TeX = ("\\HOLTokenBagRight{}", 1) } 75 76val BAG_cases = Q.store_thm( 77 "BAG_cases", 78 `!b. (b = EMPTY_BAG) \/ (?b0 e. b = BAG_INSERT e b0)`, 79 SIMP_TAC std_ss [EMPTY_BAG, BAG_INSERT, FUN_EQ_THM] THEN Q.X_GEN_TAC `b` THEN 80 Q.ASM_CASES_TAC `!x. b x = 0` THEN SRW_TAC [][] THEN 81 FULL_SIMP_TAC std_ss [] THEN MAP_EVERY Q.EXISTS_TAC [ 82 `\y. if (y = x) then b x - 1 else b y`, `x` 83 ] THEN SRW_TAC [ARITH_ss][]); 84 85val BAG_INTER = Q.new_definition( 86 "BAG_INTER", 87 `BAG_INTER b1 b2 = (\x. if (b1 x < b2 x) then b1 x else b2 x)`); 88 89 90val _ = print "Properties and definition of BAG_MERGE\n" 91 92val BAG_MERGE = Q.new_definition( 93 "BAG_MERGE", 94 `BAG_MERGE b1 b2 = (\x. if (b1 x < b2 x) then b2 x else b1 x)`); 95 96val BAG_MERGE_IDEM = store_thm ( 97 "BAG_MERGE_IDEM", 98 ``!b. BAG_MERGE b b = b``, 99 SIMP_TAC std_ss [BAG_MERGE, FUN_EQ_THM]); 100val _ = export_rewrites ["BAG_MERGE_IDEM"] 101 102Theorem BAG_MERGE_SUB_BAG_UNION: 103 !s t. (SUB_BAG (BAG_MERGE s t) (s + t)) 104Proof simp[SUB_BAG,BAG_MERGE,BAG_UNION,BAG_INN] 105QED 106 107Theorem BAG_MERGE_EMPTY[simp]: 108 !b. ((BAG_MERGE {||} b) = b) /\ ((BAG_MERGE b {||}) = b) 109Proof rw[BAG_MERGE,FUN_EQ_THM,EMPTY_BAG] 110QED 111 112Theorem BAG_MERGE_ELBAG_SUB_BAG_INSERT: 113 !A b. SUB_BAG (BAG_MERGE {|A|} b) (BAG_INSERT A b) 114Proof 115 rw[] >> simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,SUB_BAG,BAG_INN] >> rw[] 116QED 117 118Theorem BAG_MERGE_EQ_EMPTY[simp]: 119 !a b. (BAG_MERGE a b = {||}) <=> (a = {||}) /\ (b = {||}) 120Proof 121 rw[BAG_MERGE,EMPTY_BAG,FUN_EQ_THM] >> 122 EQ_TAC >> 123 rw[] >> 124 first_x_assum (qspec_then `x` mp_tac) >> 125 simp[] 126QED 127 128Theorem BAG_INSERT_EQ_MERGE_DIFF: 129 !a b c e. (BAG_INSERT e a = BAG_MERGE b c) 130 ==> ((BAG_MERGE b c = BAG_INSERT e (BAG_MERGE (b - {|e|}) (c - {|e|})))) 131Proof 132 rw[BAG_DIFF] >> 133 fs[BAG_INSERT,BAG_MERGE,EMPTY_BAG,FUN_EQ_THM] >> 134 reverse(rw[]) 135 >- (`b e - 1 + 1 = b e` suffices_by simp[EQ_SYM_EQ] >> 136 irule arithmeticTheory.SUB_ADD >> 137 `c e <= b e` by simp[] >> 138 first_x_assum (qspec_then `e` mp_tac) >> 139 rw[]) >> 140 fs[] 141QED 142 143Theorem BAG_MERGE_BAG_INSERT: 144 !e a b. 145 ((a e <= b e) 146 ==> ((BAG_MERGE a (BAG_INSERT e b)) = (BAG_INSERT e (BAG_MERGE a b)))) /\ 147 ((b e < a e) ==> ((BAG_MERGE a (BAG_INSERT e b)) = (BAG_MERGE a b))) /\ 148 ((a e < b e) ==> ((BAG_MERGE (BAG_INSERT e a) b) = ((BAG_MERGE a b)))) /\ 149 ((b e <= a e) 150 ==> ((BAG_MERGE (BAG_INSERT e a) b) = (BAG_INSERT e (BAG_MERGE a b)))) /\ 151 ((a e = b e) 152 ==> ((BAG_MERGE (BAG_INSERT e a) (BAG_INSERT e b)) 153 = (BAG_INSERT e (BAG_MERGE a b)))) 154Proof 155 rw[] 156 >- (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >> 157 rw[] >- (Cases_on `x=e` >> fs[]) >> fs[]) 158 >- (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >> 159 reverse (rw[]) >- (Cases_on `x=e` >> fs[]) >> fs[]) 160 >- (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >> 161 rw[] >- (Cases_on `x=e` >> fs[]) >> fs[]) 162 >> (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >> 163 rw[] >> fs[]) 164QED 165 166val _ = print "Properties relating BAG_IN(N) to other functions\n" 167val BAG_INN_0 = store_thm ( 168 "BAG_INN_0", 169 ``!b e:'a. BAG_INN e 0 b``, 170 SIMP_TAC arith_ss [BAG_INN]); 171val _ = export_rewrites ["BAG_INN_0"] 172 173val BAG_INN_LESS = Q.store_thm( 174 "BAG_INN_LESS", 175 `!b e n m. BAG_INN e n b /\ m < n ==> BAG_INN e m b`, 176 SIMP_TAC arith_ss [BAG_INN]); 177 178Theorem BAG_IN_BAG_INSERT[simp]: 179 !b e1 e2:'a. 180 BAG_IN e1 (BAG_INSERT e2 b) <=> (e1 = e2) \/ BAG_IN e1 b 181Proof 182 SIMP_TAC arith_ss [BAG_IN, BAG_INN, BAG_INSERT] THEN 183 REPEAT GEN_TAC THEN COND_CASES_TAC THEN SIMP_TAC arith_ss [] 184QED 185 186Theorem BAG_INN_BAG_INSERT: 187 !b e1 e2:'a. BAG_INN e1 n (BAG_INSERT e2 b) <=> 188 BAG_INN e1 (n - 1) b /\ (e1 = e2) \/ 189 BAG_INN e1 n b 190Proof SRW_TAC [ARITH_ss][BAG_INSERT, BAG_INN] 191QED 192 193Theorem BAG_INN_BAG_INSERT_STRONG: 194 !b n e1 e2. 195 BAG_INN e1 n (BAG_INSERT e2 b) <=> 196 BAG_INN e1 (n - 1) b /\ (e1 = e2) \/ 197 BAG_INN e1 n b /\ e1 <> e2 198Proof 199 REWRITE_TAC [BAG_INN_BAG_INSERT] THEN 200 SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][] THEN 201 `(n = 0) \/ ?m. n = SUC m` by (Cases_on `n` THEN METIS_TAC []) THEN 202 SRW_TAC [][] THEN 203 `m < SUC m` by DECIDE_TAC THEN 204 PROVE_TAC[BAG_INN_LESS] 205QED 206 207val BAG_UNION_EQ_LCANCEL1 = store_thm( 208 "BAG_UNION_EQ_LCANCEL1[simp]", 209 ``(b = BAG_UNION b c) <=> (c = {||})``, 210 rw[BAG_UNION, EMPTY_BAG, FUN_EQ_THM, DECIDE ``(x:num = x + y) <=> (y = 0)``]) 211 212val BAG_UNION_EQ_RCANCEL1 = store_thm( 213 "BAG_UNION_EQ_RCANCEL1[simp]", 214 ``(b = BAG_UNION c b) <=> (c = {||})``, 215 rw[BAG_UNION, EMPTY_BAG, FUN_EQ_THM, DECIDE ``(x:num = x + y) <=> (y = 0)``]) 216 217Theorem BAG_IN_BAG_UNION[simp]: 218 !b1 b2 e. BAG_IN e (BAG_UNION b1 b2) <=> BAG_IN e b1 \/ BAG_IN e b2 219Proof SRW_TAC [ARITH_ss][BAG_IN, BAG_UNION, BAG_INN] 220QED 221 222val BAG_INN_BAG_UNION = Q.store_thm( 223 "BAG_INN_BAG_UNION", 224 `!n e b1 b2. BAG_INN e n (BAG_UNION b1 b2) = 225 ?m1 m2. (n = m1 + m2) /\ BAG_INN e m1 b1 /\ BAG_INN e m2 b2`, 226 SRW_TAC [ARITH_ss][BAG_INN, BAG_UNION, GREATER_EQ, EQ_IMP_THM] THEN 227 Induct_on `n` THEN1 SRW_TAC [][] THEN 228 STRIP_TAC THEN 229 `n <= b1 e + b2 e` by DECIDE_TAC THEN 230 FULL_SIMP_TAC (srw_ss()) [] THEN 231 `m1 < b1 e \/ m2 < b2 e` by DECIDE_TAC THENL [ 232 MAP_EVERY Q.EXISTS_TAC [`SUC m1`, `m2`] THEN DECIDE_TAC, 233 MAP_EVERY Q.EXISTS_TAC [`m1`, `SUC m2`] THEN DECIDE_TAC 234 ]); 235 236val BAG_INN_BAG_MERGE = Q.store_thm ( 237 "BAG_INN_BAG_MERGE", 238 `!n e b1 b2. (BAG_INN e n (BAG_MERGE b1 b2)) = 239 (BAG_INN e n b1 \/ BAG_INN e n b2)`, 240 SIMP_TAC arith_ss [BAG_INN, BAG_MERGE]); 241 242 243Theorem BAG_IN_BAG_MERGE[simp]: 244 !e b1 b2. BAG_IN e (BAG_MERGE b1 b2) <=> BAG_IN e b1 \/ BAG_IN e b2 245Proof SIMP_TAC std_ss [BAG_IN, BAG_INN_BAG_MERGE] 246QED 247 248val geq_refl = ARITH_PROVE ``m >= m`` 249 250val BAG_EXTENSION = store_thm( 251 "BAG_EXTENSION", 252 ``!b1 b2. (b1 = b2) = (!n e:'a. BAG_INN e n b1 = BAG_INN e n b2)``, 253 SRW_TAC [][BAG_INN, FUN_EQ_THM, GREATER_EQ] THEN 254 EQ_TAC THEN1 SRW_TAC [][] THEN 255 METIS_TAC [ 256 ARITH_PROVE ``(x = y) <=> (x <= y) /\ (y <= x)``, 257 LESS_EQ_REFL 258 ]); 259 260val _ = print "Properties of BAG_INSERT\n" 261 262val BAG_UNION_INSERT = Q.store_thm( 263 "BAG_UNION_INSERT", 264 `!e b1 b2. 265 (BAG_UNION (BAG_INSERT e b1) b2 = BAG_INSERT e (BAG_UNION b1 b2)) /\ 266 (BAG_UNION b1 (BAG_INSERT e b2) = BAG_INSERT e (BAG_UNION b1 b2))`, 267 SRW_TAC [ARITH_ss][FUN_EQ_THM, BAG_INSERT, BAG_UNION] THEN 268 SRW_TAC [ARITH_ss][]); 269 270val BAG_INSERT_DIFF = store_thm ( 271 "BAG_INSERT_DIFF", 272 ``!x b. ~(BAG_INSERT x b = b)``, 273 SRW_TAC [COND_elim_ss][FUN_EQ_THM, BAG_INSERT]); 274val _ = export_rewrites ["BAG_INSERT_DIFF"] 275 276val BAG_INSERT_NOT_EMPTY = store_thm ( 277 "BAG_INSERT_NOT_EMPTY", 278 ``!x b. ~(BAG_INSERT x b = EMPTY_BAG)``, 279 SRW_TAC [COND_elim_ss][FUN_EQ_THM, BAG_INSERT, EMPTY_BAG, EXISTS_OR_THM]); 280val _ = export_rewrites ["BAG_INSERT_NOT_EMPTY"] 281 282val or_cong = REWRITE_RULE [GSYM AND_IMP_INTRO] OR_CONG 283val BAG_INSERT_ONE_ONE = store_thm( 284 "BAG_INSERT_ONE_ONE", 285 ``!b1 b2 x:'a. 286 (BAG_INSERT x b1 = BAG_INSERT x b2) = (b1 = b2)``, 287 SIMP_TAC (srw_ss() ++ COND_elim_ss) [BAG_INSERT, FUN_EQ_THM, EQ_IMP_THM, 288 Cong or_cong, FORALL_AND_THM] THEN 289 METIS_TAC []); 290val _ = export_rewrites ["BAG_INSERT_ONE_ONE"] 291 292val C_BAG_INSERT_ONE_ONE = store_thm( 293 "C_BAG_INSERT_ONE_ONE", 294 ``!x y b. (BAG_INSERT x b = BAG_INSERT y b) = (x = y)``, 295 SIMP_TAC (srw_ss() ++ COND_elim_ss ++ ARITH_ss) 296 [BAG_INSERT, FUN_EQ_THM, Cong or_cong] THEN 297 METIS_TAC []); 298val _ = export_rewrites ["C_BAG_INSERT_ONE_ONE"] 299 300val BAG_INSERT_commutes = store_thm( 301 "BAG_INSERT_commutes", 302 ``!b e1 e2. BAG_INSERT e1 (BAG_INSERT e2 b) = 303 BAG_INSERT e2 (BAG_INSERT e1 b)``, 304 SIMP_TAC (srw_ss()) [BAG_INSERT, FUN_EQ_THM] THEN 305 REPEAT GEN_TAC THEN 306 REPEAT (COND_CASES_TAC THEN ASM_SIMP_TAC (srw_ss()) []) THEN 307 SRW_TAC [][]); 308 309val BAG_DECOMPOSE = store_thm 310("BAG_DECOMPOSE", 311 ``!e b. BAG_IN e b ==> ?b'. b = BAG_INSERT e b'``, 312 REPEAT STRIP_TAC THEN 313 Q.EXISTS_TAC `b - {|e|}` THEN POP_ASSUM MP_TAC THEN 314 SRW_TAC [ARITH_ss, COND_elim_ss] 315 [BAG_INSERT,BAG_DIFF,EMPTY_BAG,FUN_EQ_THM,BAG_IN,BAG_INN]); 316 317val _ = print "Properties of BAG_UNION\n"; 318 319val BAG_UNION_LEFT_CANCEL = store_thm( 320 "BAG_UNION_LEFT_CANCEL", 321 ``!b b1 b2:'a -> num. (BAG_UNION b b1 = BAG_UNION b b2) = (b1 = b2)``, 322 SIMP_TAC arith_ss [BAG_UNION,FUN_EQ_THM]); 323val _ = export_rewrites ["BAG_UNION_LEFT_CANCEL"] 324 325val COMM_BAG_UNION = store_thm( 326 "COMM_BAG_UNION", 327 ``!b1 b2. BAG_UNION b1 b2 = BAG_UNION b2 b1``, 328 SRW_TAC [ARITH_ss][BAG_UNION, FUN_EQ_THM]); 329val bu_comm = COMM_BAG_UNION; 330 331val BAG_UNION_RIGHT_CANCEL = store_thm( 332 "BAG_UNION_RIGHT_CANCEL", 333 ``!b b1 b2:'a bag. (BAG_UNION b1 b = BAG_UNION b2 b) = (b1 = b2)``, 334 METIS_TAC [bu_comm, BAG_UNION_LEFT_CANCEL]); 335val _ = export_rewrites ["BAG_UNION_RIGHT_CANCEL"] 336 337val ASSOC_BAG_UNION = store_thm( 338 "ASSOC_BAG_UNION", 339 ``!b1 b2 b3. BAG_UNION b1 (BAG_UNION b2 b3) 340 = 341 BAG_UNION (BAG_UNION b1 b2) b3``, 342 SRW_TAC [ARITH_ss][BAG_UNION, FUN_EQ_THM]); 343 344Theorem BAG_UNION_EMPTY[simp]: 345 (!b. b + {||} = b) /\ 346 (!b. {||} + b = b) /\ 347 (!b1 b2. (b1 + b2 = {||}) <=> (b1 = {||}) /\ (b2 = {||})) 348Proof SRW_TAC [][BAG_UNION, EMPTY_BAG, FUN_EQ_THM] THEN METIS_TAC [] 349QED 350 351val _ = print "Definition and properties of BAG_DELETE\n" 352val BAG_DELETE = new_definition ( 353 "BAG_DELETE", 354 ``BAG_DELETE b0 (e:'a) b = (b0 = BAG_INSERT e b)``); 355 356val BAG_DELETE_EMPTY = store_thm( 357 "BAG_DELETE_EMPTY", 358 ``!(e:'a) b. ~(BAG_DELETE EMPTY_BAG e b)``, 359 SIMP_TAC std_ss [BAG_DELETE] THEN 360 ACCEPT_TAC (GSYM BAG_INSERT_NOT_EMPTY)); 361 362val BAG_DELETE_commutes = store_thm( 363 "BAG_DELETE_commutes", 364 ``!b0 b1 b2 e1 e2:'a. 365 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b1 e2 b2 ==> 366 ?b'. BAG_DELETE b0 e2 b' /\ BAG_DELETE b' e1 b2``, 367 SIMP_TAC std_ss [BAG_DELETE] THEN 368 ACCEPT_TAC BAG_INSERT_commutes); 369 370val BAG_DELETE_11 = store_thm( 371 "BAG_DELETE_11", 372 ``!b0 (e1:'a) e2 b1 b2. 373 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 ==> 374 ((e1 = e2) = (b1 = b2))``, 375 SRW_TAC [][BAG_DELETE, EQ_IMP_THM] THEN 376 FULL_SIMP_TAC (srw_ss()) []); 377 378val BAG_INN_BAG_DELETE = store_thm( 379 "BAG_INN_BAG_DELETE", 380 Term`!b n e. BAG_INN e n b /\ n > 0 ==> ?b'. BAG_DELETE b e b'`, 381 SRW_TAC [][BAG_DELETE] THEN MATCH_MP_TAC BAG_DECOMPOSE THEN 382 SRW_TAC [][BAG_IN] THEN 383 `(n = 1) \/ 1 < n` by DECIDE_TAC THEN 384 METIS_TAC [BAG_INN_LESS]); 385 386val BAG_IN_BAG_DELETE = store_thm( 387 "BAG_IN_BAG_DELETE", 388 Term`!b e:'a. BAG_IN e b ==> ?b'. BAG_DELETE b e b'`, 389 METIS_TAC [BAG_INN_BAG_DELETE, ARITH_PROVE (Term`1 > 0`), BAG_IN]); 390 391val ELIM_TAC = BasicProvers.VAR_EQ_TAC 392val ARWT = SRW_TAC [ARITH_ss][] 393open mesonLib 394 395val BAG_DELETE_INSERT = Q.store_thm( 396 "BAG_DELETE_INSERT", 397 `!x y b1 b2. 398 BAG_DELETE (BAG_INSERT x b1) y b2 ==> 399 (x = y) /\ (b1 = b2) \/ (?b3. BAG_DELETE b1 y b3) /\ ~(x = y)`, 400 SIMP_TAC std_ss [BAG_DELETE] THEN REPEAT STRIP_TAC THEN 401 Q.ASM_CASES_TAC `x = y` THEN ARWT THENL [ 402 FULL_SIMP_TAC std_ss [BAG_INSERT_ONE_ONE], 403 Q.SUBGOAL_THEN `BAG_IN y b1` 404 (STRIP_ASSUME_TAC o 405 MATCH_MP (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE)) 406 THENL [ 407 ASM_MESON_TAC [BAG_IN_BAG_INSERT], 408 ELIM_TAC THEN SIMP_TAC std_ss [BAG_INSERT_ONE_ONE] 409 ] 410 ]); 411 412val BAG_DELETE_BAG_IN_up = store_thm( 413 "BAG_DELETE_BAG_IN_up", 414 ``!b0 b e:'a. BAG_DELETE b0 e b ==> 415 !e'. BAG_IN e' b ==> BAG_IN e' b0``, 416 REWRITE_TAC [BAG_DELETE] THEN REPEAT STRIP_TAC THEN ELIM_TAC THEN 417 ASM_REWRITE_TAC [BAG_IN_BAG_INSERT]); 418 419val BAG_DELETE_BAG_IN_down = store_thm( 420 "BAG_DELETE_BAG_IN_down", 421 ``!b0 b e1 e2:'a. 422 BAG_DELETE b0 e1 b /\ ~(e1 = e2) /\ BAG_IN e2 b0 ==> 423 BAG_IN e2 b``, 424 SIMP_TAC std_ss [BAG_DELETE, BAG_IN_BAG_INSERT, LEFT_AND_OVER_OR, 425 DISJ_IMP_THM]); 426 427val BAG_DELETE_BAG_IN = store_thm( 428 "BAG_DELETE_BAG_IN", 429 ``!b0 b e:'a. BAG_DELETE b0 e b ==> BAG_IN e b0``, 430 SIMP_TAC std_ss [BAG_IN_BAG_INSERT, BAG_DELETE]); 431 432Theorem BAG_DELETE_concrete: 433 !b0 b e. BAG_DELETE b0 e b <=> 434 b0 e > 0 /\ (b = \x. if (x = e) then b0 e - 1 else b0 x) 435Proof 436 SRW_TAC [ARITH_ss][FUN_EQ_THM, BAG_DELETE, BAG_INSERT, EQ_IMP_THM] THEN 437 SRW_TAC [][] 438QED 439 440val add_eq_conv_diff = prove( 441 ``(M + {|a|} = N + {|b|}) <=> 442 (M = N) /\ (a = b) \/ 443 (M = N - {|a|} + {|b|}) /\ (N = M - {|b|} + {|a|})``, 444 SRW_TAC [][BAG_UNION, BAG_DIFF, FUN_EQ_THM, BAG_INSERT, EMPTY_BAG] THEN 445 Cases_on `a = b` THEN SRW_TAC [][] THENL [ 446 EQ_TAC THEN1 SRW_TAC [][] THEN STRIP_TAC THEN 447 Q.X_GEN_TAC `x` THEN 448 REPEAT (POP_ASSUM (Q.SPEC_THEN `x` MP_TAC)) THEN SRW_TAC [][] THEN 449 DECIDE_TAC, 450 451 EQ_TAC THEN STRIP_TAC THEN REPEAT CONJ_TAC THEN 452 Q.X_GEN_TAC `x` THEN 453 REPEAT (FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC)) THEN 454 SRW_TAC [][] THEN DECIDE_TAC 455 ]); 456 457val insert_diffM2 = prove( 458 ``BAG_IN x M ==> (M - {|x|} + {|x|} = M)``, 459 SRW_TAC [][BAG_UNION, BAG_DIFF, BAG_INSERT, EMPTY_BAG, FUN_EQ_THM, BAG_IN, 460 BAG_INN] THEN 461 SRW_TAC [][] THEN DECIDE_TAC); 462 463val BAG_UNION_DIFF_eliminate = store_thm( 464 "BAG_UNION_DIFF_eliminate", 465 ``(BAG_DIFF (BAG_UNION b c) c = b) /\ 466 (BAG_DIFF (BAG_UNION c b) c = b)``, 467 SRW_TAC [][BAG_DIFF, BAG_UNION, FUN_EQ_THM]); 468val _ = export_rewrites ["BAG_UNION_DIFF_eliminate"] 469 470val add_eq_conv_ex = prove( 471 ���(M + {|a|} = N + {|b|}) <=> 472 (M = N) /\ (a = b) \/ 473 ?k. (M = k + {|b|}) /\ (N = k + {|a|})���, 474 SRW_TAC [][add_eq_conv_diff] THEN Cases_on `a = b` THENL [ 475 SRW_TAC [][EQ_IMP_THM] THEN 476 FULL_SIMP_TAC (srw_ss()) [insert_diffM2] THEN 477 POP_ASSUM ACCEPT_TAC, 478 479 SRW_TAC [][] THEN EQ_TAC THEN STRIP_TAC THENL [ 480 POP_ASSUM SUBST_ALL_TAC THEN SRW_TAC [][] THEN 481 `BAG_IN b M` by METIS_TAC [BAG_IN_BAG_UNION, BAG_IN_BAG_INSERT] THEN 482 SRW_TAC [][insert_diffM2], 483 484 SRW_TAC [][] 485 ] 486 ]); 487 488val BAG_INSERT_EQUAL = save_thm( 489 "BAG_INSERT_EQUAL", 490 SIMP_RULE (srw_ss()) [BAG_UNION_INSERT] add_eq_conv_ex) 491 492val BAG_DELETE_TWICE = store_thm( 493 "BAG_DELETE_TWICE", 494 ``!b0 e1 e2 b1 b2. 495 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 /\ ~(b1 = b2) ==> 496 ?b. BAG_DELETE b1 e2 b /\ BAG_DELETE b2 e1 b``, 497 SRW_TAC [][BAG_DELETE] THEN 498 `b2 + {|e2|} = b1 + {|e1|}` by SRW_TAC [][BAG_UNION_INSERT] THEN 499 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [add_eq_conv_ex]) THEN 500 FULL_SIMP_TAC (srw_ss()) [] THEN 501 SRW_TAC [][BAG_UNION_INSERT]); 502 503val SING_BAG = new_definition( 504 "SING_BAG", 505 ``SING_BAG (b:'a->num) = ?x. b = BAG_INSERT x EMPTY_BAG``); 506 507val SING_BAG_THM = store_thm( 508 "SING_BAG_THM", 509 ``!e:'a. SING_BAG (BAG_INSERT e EMPTY_BAG)``, 510 MESON_TAC [SING_BAG]); 511 512val EL_BAG = new_definition( 513 "EL_BAG", 514 ``EL_BAG (e:'a) = BAG_INSERT e EMPTY_BAG``); 515 516val EL_BAG_11 = store_thm( 517 "EL_BAG_11", 518 ``!x y. (EL_BAG x = EL_BAG y) ==> (x = y)``, 519 SRW_TAC [][EL_BAG]); 520 521val EL_BAG_INSERT_squeeze = store_thm( 522 "EL_BAG_INSERT_squeeze", 523 ``!x b y. (EL_BAG x = BAG_INSERT y b) ==> (x = y) /\ (b = EMPTY_BAG)``, 524 SIMP_TAC (srw_ss()) [EL_BAG, BAG_INSERT_EQUAL]); 525 526val SING_EL_BAG = store_thm( 527 "SING_EL_BAG", 528 ``!e:'a. SING_BAG (EL_BAG e)``, 529 REWRITE_TAC [EL_BAG, SING_BAG_THM]); 530 531val BAG_INSERT_UNION = store_thm( 532 "BAG_INSERT_UNION", 533 ``!b e. BAG_INSERT e b = BAG_UNION (EL_BAG e) b``, 534 SRW_TAC [][EL_BAG, BAG_UNION_INSERT]); 535 536val BAG_INSERT_EQ_UNION = Q.store_thm( 537 "BAG_INSERT_EQ_UNION", 538 `!e b1 b2 b. (BAG_INSERT e b = BAG_UNION b1 b2) ==> 539 BAG_IN e b1 \/ BAG_IN e b2`, 540 REPEAT STRIP_TAC THEN POP_ASSUM (MP_TAC o Q.AP_TERM `BAG_IN e`) THEN 541 SRW_TAC [][]); 542 543val BAG_DELETE_SING = store_thm( 544 "BAG_DELETE_SING", 545 ``!b e. BAG_DELETE b e EMPTY_BAG ==> SING_BAG b``, 546 MESON_TAC [SING_BAG, BAG_DELETE]); 547 548val NOT_IN_EMPTY_BAG = store_thm( 549 "NOT_IN_EMPTY_BAG", 550 ``!x:'a. ~(BAG_IN x EMPTY_BAG)``, 551 SIMP_TAC std_ss [BAG_IN, BAG_INN, EMPTY_BAG]) 552val _ = export_rewrites ["NOT_IN_EMPTY_BAG"]; 553 554val BAG_INN_EMPTY_BAG = Q.store_thm( 555 "BAG_INN_EMPTY_BAG", 556 `!e n. BAG_INN e n EMPTY_BAG = (n = 0)`, 557 SIMP_TAC arith_ss [BAG_INN, EMPTY_BAG, EQ_IMP_THM]) 558val _ = export_rewrites ["BAG_INN_EMPTY_BAG"]; 559 560val MEMBER_NOT_EMPTY = store_thm( 561 "MEMBER_NOT_EMPTY", 562 ``!b. (?x. BAG_IN x b) = ~(b = EMPTY_BAG)``, 563 METIS_TAC [BAG_cases, BAG_IN_BAG_INSERT, NOT_IN_EMPTY_BAG]); 564 565val _ = print "Properties of SUB_BAG\n" 566 567val _ = overload_on ("<=", ``SUB_BAG``) 568val _ = overload_on ("<", ``PSUB_BAG``) 569val _ = send_to_back_overload "<=" {Name = "SUB_BAG", Thy = "bag"} 570val _ = send_to_back_overload "<" {Name = "PSUB_BAG", Thy = "bag"} 571 572val SUB_BAG_LEQ = store_thm ( 573 "SUB_BAG_LEQ", 574 ``SUB_BAG b1 b2 = !x. b1 x <= b2 x``, 575 SRW_TAC [][SUB_BAG, BAG_INN, EQ_IMP_THM] THENL [ 576 POP_ASSUM (Q.SPECL_THEN [`x`, `b1 x`] MP_TAC) THEN DECIDE_TAC, 577 FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN DECIDE_TAC 578 ]); 579 580val SUB_BAG_EMPTY = store_thm ( 581 "SUB_BAG_EMPTY[simp]", 582 ``(!b:'a->num. SUB_BAG {||} b) /\ 583 (!b:'a->num. SUB_BAG b {||} = (b = {||}))``, 584 SRW_TAC [][SUB_BAG_LEQ, EMPTY_BAG, FUN_EQ_THM]); 585 586val SUB_BAG_REFL = store_thm( 587 "SUB_BAG_REFL[simp]", 588 ``!(b:'a -> num). SUB_BAG b b``, 589 REWRITE_TAC [SUB_BAG]); 590 591val PSUB_BAG_IRREFL = store_thm( 592 "PSUB_BAG_IRREFL", 593 ``!(b:'a -> num). ~(PSUB_BAG b b)``, 594 REWRITE_TAC [PSUB_BAG]); 595 596val SUB_BAG_ANTISYM = store_thm( 597 "SUB_BAG_ANTISYM", 598 ``!(b1:'a -> num) b2. SUB_BAG b1 b2 /\ SUB_BAG b2 b1 ==> (b1 = b2)``, 599 SRW_TAC [][SUB_BAG_LEQ, FUN_EQ_THM, 600 DECIDE ``(x:num = y) <=> x <= y /\ y <= x``]); 601 602val PSUB_BAG_ANTISYM = store_thm( 603 "PSUB_BAG_ANTISYM", 604 ``!(b1:'a -> num) b2. ~(PSUB_BAG b1 b2 /\ PSUB_BAG b2 b1)``, 605 MESON_TAC [PSUB_BAG, SUB_BAG_ANTISYM]); 606 607val SUB_BAG_TRANS = store_thm( 608 "SUB_BAG_TRANS", 609 ``!b1 b2 b3. SUB_BAG (b1:'a->num) b2 /\ SUB_BAG b2 b3 ==> 610 SUB_BAG b1 b3``, 611 MESON_TAC [SUB_BAG, BAG_INN]); 612 613val PSUB_BAG_TRANS = store_thm( 614 "PSUB_BAG_TRANS", 615 ``!(b1:'a -> num) b2 b3. PSUB_BAG b1 b2 /\ PSUB_BAG b2 b3 ==> 616 PSUB_BAG b1 b3``, 617 MESON_TAC [PSUB_BAG, SUB_BAG_TRANS, SUB_BAG_ANTISYM]); 618 619val PSUB_BAG_SUB_BAG = store_thm( 620 "PSUB_BAG_SUB_BAG", 621 ``!(b1:'a->num) b2. PSUB_BAG b1 b2 ==> SUB_BAG b1 b2``, 622 SIMP_TAC std_ss [PSUB_BAG]); 623 624val PSUB_BAG_NOT_EQ = store_thm( 625 "PSUB_BAG_NOT_EQ", 626 ``!(b1:'a -> num) b2. PSUB_BAG b1 b2 ==> ~(b1 = b2)``, 627 SIMP_TAC std_ss [PSUB_BAG]); 628 629val _ = print "Properties of BAG_DIFF\n"; 630 631val BAG_DIFF_EMPTY = store_thm( 632 "BAG_DIFF_EMPTY", 633 ``(!b. b - b = {||}) /\ 634 (!b. b - {||} = b) /\ 635 (!b. {||} - b = {||}) /\ 636 (!b1 b2. 637 b1 <= b2 ==> (b1 - b2 = {||}))``, 638 SRW_TAC [][SUB_BAG_LEQ, BAG_DIFF, EMPTY_BAG, FUN_EQ_THM]); 639 640val BAG_DIFF_EMPTY_simple = save_thm( 641 "BAG_DIFF_EMPTY_simple", 642 LIST_CONJ (List.take(CONJUNCTS BAG_DIFF_EMPTY, 3))) 643val _ = export_rewrites ["BAG_DIFF_EMPTY_simple"]; 644 645val BAG_DIFF_EQ_EMPTY = store_thm( 646 "BAG_DIFF_EQ_EMPTY[simp]", 647 ``(b - c = {||}) <=> b <= c``, 648 simp[BAG_DIFF, FUN_EQ_THM, SUB_BAG_LEQ, EMPTY_BAG]); 649 650val BAG_DIFF_INSERT_same = store_thm( 651 "BAG_DIFF_INSERT_same", 652 ``!x b1 b2. BAG_DIFF (BAG_INSERT x b1) (BAG_INSERT x b2) = 653 BAG_DIFF b1 b2``, 654 SRW_TAC [COND_elim_ss, ARITH_ss][BAG_DIFF, FUN_EQ_THM, BAG_INSERT]); 655val _ = export_rewrites ["BAG_DIFF_INSERT_same"]; 656 657val BAG_DIFF_INSERT = Q.store_thm( 658 "BAG_DIFF_INSERT", 659 `!x b1 b2. 660 ~BAG_IN x b1 ==> 661 (BAG_DIFF (BAG_INSERT x b2) b1 = BAG_INSERT x (BAG_DIFF b2 b1))`, 662 SRW_TAC [COND_elim_ss, ARITH_ss][FUN_EQ_THM, BAG_DIFF, BAG_INSERT, 663 Cong or_cong, BAG_IN, BAG_INN]); 664 665val NOT_IN_BAG_DIFF = Q.store_thm( 666 "NOT_IN_BAG_DIFF", 667 `!x b1 b2. ~BAG_IN x b1 ==> 668 (BAG_DIFF b1 (BAG_INSERT x b2) = BAG_DIFF b1 b2)`, 669 SRW_TAC [COND_elim_ss, ARITH_ss][FUN_EQ_THM, BAG_IN, BAG_INN, BAG_INSERT, 670 BAG_DIFF]); 671 672val BAG_IN_DIFF_I = Q.store_thm( 673 "BAG_IN_DIFF_I", 674 `e <: b1 /\ ~(e <: b2) ==> e <: b1 - b2`, 675 SRW_TAC [ARITH_ss][BAG_IN,BAG_DIFF,BAG_INN] ); 676 677val BAG_IN_DIFF_E = Q.store_thm( 678"BAG_IN_DIFF_E", 679`e <: b1 - b2 ==> e <: b1`, 680SRW_TAC [ARITH_ss][BAG_IN,BAG_INN,BAG_DIFF]); 681 682val BAG_UNION_DIFF = store_thm( 683 "BAG_UNION_DIFF", 684 ``!X Y Z. 685 SUB_BAG Z Y ==> 686 (BAG_UNION X (BAG_DIFF Y Z) = BAG_DIFF (BAG_UNION X Y) Z) /\ 687 (BAG_UNION (BAG_DIFF Y Z) X = BAG_DIFF (BAG_UNION X Y) Z)``, 688 SRW_TAC [][SUB_BAG_LEQ, BAG_UNION, BAG_DIFF, FUN_EQ_THM] THEN 689 POP_ASSUM (fn th => SIMP_TAC arith_ss [SPEC_ALL th])); 690 691val BAG_DIFF_2L = store_thm( 692 "BAG_DIFF_2L", 693 ``!X Y Z:'a->num. 694 BAG_DIFF (BAG_DIFF X Y) Z = BAG_DIFF X (BAG_UNION Y Z)``, 695 SIMP_TAC arith_ss [BAG_UNION,BAG_INN,SUB_BAG,BAG_DIFF]); 696 697val BAG_DIFF_2R = store_thm( 698 "BAG_DIFF_2R", 699 ``!A B C:'a->num. 700 SUB_BAG C B ==> 701 (BAG_DIFF A (BAG_DIFF B C) = BAG_DIFF (BAG_UNION A C) B)``, 702 SRW_TAC [][BAG_UNION, BAG_DIFF, SUB_BAG_LEQ, FUN_EQ_THM] THEN 703 ASSUM_LIST (fn thl => SIMP_TAC arith_ss (map SPEC_ALL thl))); 704 705val std_ss = arith_ss 706val SUB_BAG_BAG_DIFF = store_thm( 707 "SUB_BAG_BAG_DIFF", 708 ``!X Y Y' Z W:'a->num. 709 SUB_BAG (BAG_DIFF X Y) (BAG_DIFF Z W) ==> 710 SUB_BAG (BAG_DIFF X (BAG_UNION Y Y')) 711 (BAG_DIFF Z (BAG_UNION W Y'))``, 712 SIMP_TAC std_ss [ 713 BAG_DIFF, SUB_BAG_LEQ, BAG_INN, BAG_UNION, 714 DISJ_IMP_THM] THEN 715 REPEAT STRIP_TAC THEN 716 FIRST_ASSUM (Q.SPEC_THEN `x` (STRIP_ASSUME_TAC o SIMP_RULE std_ss [])) THEN 717 ASM_SIMP_TAC std_ss []); 718 719local 720 fun bdf (b1, b2) (b3, b4) = 721 let val (b1v, b2v, b3v, b4v) = 722 case map (C (curry mk_var) (==`:'a->num`==)) [b1, b2, b3, b4] of 723 [b1v, b2v, b3v, b4v] => (b1v, b2v, b3v, b4v) 724 | _ => raise Match 725 in 726 ``BAG_DIFF (BAG_UNION ^b1v ^b2v) (BAG_UNION ^b3v ^b4v) = 727 BAG_DIFF b2 b3`` 728 end 729in 730 val BAG_DIFF_UNION_eliminate = store_thm( 731 "BAG_DIFF_UNION_eliminate", 732 ``!(b1:'a->num) (b2:'a->num) (b3:'a->num). 733 ^(bdf ("b1", "b2") ("b1", "b3")) /\ 734 ^(bdf ("b1", "b2") ("b3", "b1")) /\ 735 ^(bdf ("b2", "b1") ("b1", "b3")) /\ 736 ^(bdf ("b2", "b1") ("b3", "b1"))``, 737 REPEAT STRIP_TAC THEN 738 SIMP_TAC std_ss [BAG_DIFF, BAG_UNION, FUN_EQ_THM]) 739 val _ = export_rewrites ["BAG_DIFF_UNION_eliminate"] 740end; 741 742local 743 fun bdf (b1, b2) (b3, b4) = 744 let val (b1v, b2v, b3v, b4v) = 745 case map (C (curry mk_var) (==`:'a->num`==)) [b1, b2, b3, b4] of 746 [b1v, b2v, b3v, b4v] => (b1v, b2v, b3v, b4v) 747 | _ => raise Match 748 in 749 ``SUB_BAG (BAG_UNION ^b1v ^b2v) (BAG_UNION ^b3v ^b4v) = 750 SUB_BAG (b2:'a->num) b3`` 751 end 752in 753 val SUB_BAG_UNION_eliminate = store_thm( 754 "SUB_BAG_UNION_eliminate", 755 ``!(b1:'a->num) (b2:'a->num) (b3:'a->num). 756 ^(bdf ("b1", "b2") ("b1", "b3")) /\ 757 ^(bdf ("b1", "b2") ("b3", "b1")) /\ 758 ^(bdf ("b2", "b1") ("b1", "b3")) /\ 759 ^(bdf ("b2", "b1") ("b3", "b1"))``, 760 SIMP_TAC std_ss [SUB_BAG_LEQ, BAG_UNION, BAG_INN] THEN 761 REPEAT STRIP_TAC THEN EQ_TAC THEN 762 STRIP_TAC THEN 763 POP_ASSUM (fn th => SIMP_TAC std_ss [SPEC_ALL th])) 764 val _ = export_rewrites ["SUB_BAG_UNION_eliminate"] 765end; 766 767val move_BAG_UNION_over_eq = store_thm( 768 "move_BAG_UNION_over_eq", 769 ``!X Y Z:'a->num. (BAG_UNION X Y = Z) ==> (X = BAG_DIFF Z Y)``, 770 SIMP_TAC (std_ss ++ ETA_ss) [BAG_UNION, BAG_DIFF]); 771 772val std_bag_tac = 773 SIMP_TAC std_ss [BAG_UNION, SUB_BAG_LEQ, BAG_INN] THEN 774 REPEAT STRIP_TAC THEN 775 ASSUM_LIST (fn thl => SIMP_TAC std_ss (map SPEC_ALL thl)) 776 777fun bag_thm t = prove(Term t, std_bag_tac); 778 779val simplest_cases = map bag_thm [ 780 `!b1 b2:'a->num. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b2 b)`, 781 `!b1 b2:'a->num. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b b2)` 782]; 783 784val one_from_assocl = map bag_thm [ 785 `!b1 b2 b3:'a->num. 786 SUB_BAG b1 (BAG_UNION b2 b3) ==> 787 !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b2 b) b3)`, 788 `!b1 b2 b3:'a->num. 789 SUB_BAG b1 (BAG_UNION b2 b3) ==> 790 !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b b2) b3)`] 791 792val one_from_assocr = 793 map (ONCE_REWRITE_RULE [bu_comm]) one_from_assocl; 794 795val one_from_assoc = one_from_assocl @ one_from_assocr; 796 797val union_from_union = map bag_thm [ 798 `!b1 b2 b3 b4:'a->num. 799 SUB_BAG b1 b3 ==> SUB_BAG b2 b4 ==> 800 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)`, 801 `!b1 b2 b3 b4:'a->num. 802 SUB_BAG b1 b4 ==> SUB_BAG b2 b3 ==> 803 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)`]; 804 805val union_union2_assocl = map bag_thm [ 806 `!b1 b2 b3 b4 b5:'a->num. 807 SUB_BAG b1 (BAG_UNION b3 b5) ==> SUB_BAG b2 b4 ==> 808 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`, 809 `!b1 b2 b3 b4 b5:'a->num. 810 SUB_BAG b1 (BAG_UNION b4 b5) ==> SUB_BAG b2 b3 ==> 811 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`, 812 `!b1 b2 b3 b4 b5:'a->num. 813 SUB_BAG b2 (BAG_UNION b3 b5) ==> SUB_BAG b1 b4 ==> 814 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`, 815 `!b1 b2 b3 b4 b5:'a->num. 816 SUB_BAG b2 (BAG_UNION b4 b5) ==> SUB_BAG b1 b3 ==> 817 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`]; 818 819val union_union2_assocr = 820 map (ONCE_REWRITE_RULE [bu_comm]) union_union2_assocl; 821 822val union_union2_assoc = union_union2_assocl @ union_union2_assocr; 823 824val union2_union_assocl = map bag_thm [ 825 `!b1 b2 b3 b4 b5:'a->num. 826 SUB_BAG (BAG_UNION b1 b2) b4 ==> SUB_BAG b3 b5 ==> 827 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`, 828 `!b1 b2 b3 b4 b5:'a->num. 829 SUB_BAG (BAG_UNION b1 b2) b5 ==> SUB_BAG b3 b4 ==> 830 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`, 831 `!b1 b2 b3 b4 b5:'a->num. 832 SUB_BAG (BAG_UNION b3 b2) b4 ==> SUB_BAG b1 b5 ==> 833 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`, 834 `!b1 b2 b3 b4 b5:'a->num. 835 SUB_BAG (BAG_UNION b3 b2) b5 ==> SUB_BAG b1 b4 ==> 836 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`]; 837 838val union2_union_assocr = 839 map (ONCE_REWRITE_RULE [bu_comm]) union2_union_assocl; 840 841val union2_union_assoc = union2_union_assocl @ union2_union_assocr; 842 843val SUB_BAG_UNION = save_thm( 844 "SUB_BAG_UNION", 845 LIST_CONJ (simplest_cases @ one_from_assoc @ union_from_union @ 846 union_union2_assoc @ union2_union_assoc)); 847 848val SUB_BAG_EL_BAG = Q.store_thm( 849 "SUB_BAG_EL_BAG", 850 `!e b. SUB_BAG (EL_BAG e) b = BAG_IN e b`, 851 SRW_TAC [COND_elim_ss, ARITH_ss] 852 [SUB_BAG_LEQ, EL_BAG, BAG_IN, BAG_INN, BAG_INSERT, EMPTY_BAG]); 853 854val SUB_BAG_INSERT = Q.store_thm( 855 "SUB_BAG_INSERT", 856 `!e b1 b2. SUB_BAG (BAG_INSERT e b1) (BAG_INSERT e b2) = 857 SUB_BAG b1 b2`, 858 SRW_TAC [ARITH_ss][BAG_INSERT, SUB_BAG_LEQ, EQ_IMP_THM] THEN 859 POP_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN SRW_TAC [ARITH_ss][]); 860 861val SUB_BAG_INSERT_I = store_thm( 862 "SUB_BAG_INSERT_I", 863 ``!b c e. SUB_BAG b c ==> SUB_BAG b (BAG_INSERT e c)``, 864 SRW_TAC[][BAG_INSERT, SUB_BAG_LEQ] THEN 865 POP_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN SRW_TAC[ARITH_ss][]); 866 867val NOT_IN_SUB_BAG_INSERT = Q.store_thm( 868 "NOT_IN_SUB_BAG_INSERT", 869 `!b1 b2 e. ~(BAG_IN e b1) ==> 870 (SUB_BAG b1 (BAG_INSERT e b2) = SUB_BAG b1 b2)`, 871 SIMP_TAC std_ss [SUB_BAG, BAG_INN_BAG_INSERT, BAG_IN] THEN 872 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 873 RES_TAC THEN ELIM_TAC THEN 874 STRIP_ASSUME_TAC (ARITH_PROVE (Term`(n = 0) \/ (n = 1) \/ (1 < n)`)) 875 THENL [ 876 FULL_SIMP_TAC std_ss [], 877 FULL_SIMP_TAC std_ss [], 878 ASM_MESON_TAC [BAG_INN_LESS] 879 ], 880 ASM_MESON_TAC [] 881 ]); 882 883val SUB_BAG_BAG_IN = Q.store_thm( 884 "SUB_BAG_BAG_IN", 885 `!x b1 b2. SUB_BAG (BAG_INSERT x b1) b2 ==> BAG_IN x b2`, 886 SIMP_TAC std_ss [SUB_BAG_LEQ, BAG_INSERT, BAG_IN, BAG_INN] THEN 887 REPEAT GEN_TAC THEN 888 DISCH_THEN (Q.SPEC_THEN `x` (ASSUME_TAC o SIMP_RULE std_ss [])) THEN 889 ASM_SIMP_TAC std_ss []); 890 891val SUB_BAG_EXISTS = store_thm( 892 "SUB_BAG_EXISTS", 893 ``!b1 b2:'a->num. SUB_BAG b1 b2 = ?b. b2 = BAG_UNION b1 b``, 894 SRW_TAC [][SUB_BAG_LEQ, BAG_UNION, FUN_EQ_THM, EQ_IMP_THM] THENL [ 895 Q.EXISTS_TAC `\x. b2 x - b1 x` THEN 896 POP_ASSUM (fn th => SIMP_TAC std_ss [SPEC_ALL th]), 897 ASM_SIMP_TAC std_ss [] 898 ]); 899 900val SUB_BAG_UNION_DIFF = store_thm( 901 "SUB_BAG_UNION_DIFF", 902 ``!b1 b2 b3:'a->num. 903 SUB_BAG b1 b3 ==> 904 (SUB_BAG b2 (BAG_DIFF b3 b1) = SUB_BAG (BAG_UNION b1 b2) b3) 905 ``, 906 SIMP_TAC std_ss [SUB_BAG_LEQ,BAG_DIFF,BAG_UNION] THEN 907 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN 908 REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN DECIDE_TAC); 909 910val SUB_BAG_UNION_down = store_thm( 911 "SUB_BAG_UNION_down", 912 ``!b1 b2 b3:'a->num. SUB_BAG (BAG_UNION b1 b2) b3 ==> 913 SUB_BAG b1 b3 /\ SUB_BAG b2 b3``, 914 SIMP_TAC std_ss [BAG_UNION, SUB_BAG_LEQ] THEN 915 REPEAT STRIP_TAC THEN 916 ASSUM_LIST (fn thl => SIMP_TAC std_ss (map SPEC_ALL thl))); 917 918val SUB_BAG_DIFF = store_thm( 919 "SUB_BAG_DIFF", 920 ``(!b1 b2:'a->num. SUB_BAG b1 b2 ==> 921 (!b3. SUB_BAG (BAG_DIFF b1 b3) b2)) /\ 922 (!b1 b2 b3 b4:'a->num. 923 SUB_BAG b2 b1 ==> SUB_BAG b4 b3 ==> 924 (SUB_BAG (BAG_DIFF b1 b2) (BAG_DIFF b3 b4) = 925 SUB_BAG (BAG_UNION b1 b4) (BAG_UNION b2 b3)))``, 926 SRW_TAC [ARITH_ss][BAG_DIFF, BAG_UNION, SUB_BAG_LEQ, EQ_IMP_THM] THEN 927 REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN DECIDE_TAC); 928 929val SUB_BAG_PSUB_BAG = store_thm( 930 "SUB_BAG_PSUB_BAG", 931 ``!(b1:'a -> num) b2. 932 SUB_BAG b1 b2 = PSUB_BAG b1 b2 \/ (b1 = b2)``, 933 METIS_TAC [PSUB_BAG, SUB_BAG_REFL]); 934 935val mono_cond = COND_RAND 936val mono_cond2 = COND_RATOR 937 938val BAG_DELETE_PSUB_BAG = store_thm( 939 "BAG_DELETE_PSUB_BAG", 940 ``!b0 (e:'a) b. BAG_DELETE b0 e b ==> PSUB_BAG b b0``, 941 SIMP_TAC std_ss [BAG_DELETE, SUB_BAG, PSUB_BAG, BAG_INSERT_DIFF, 942 BAG_INN_BAG_INSERT]); 943 944val _ = print "Relating bags to (pred)sets\n"; 945 946val SET_OF_BAG = new_definition( 947 "SET_OF_BAG", 948 ``SET_OF_BAG (b:'a->num) = \x. BAG_IN x b``); 949 950val BAG_OF_SET = new_definition( 951 "BAG_OF_SET", 952 ``BAG_OF_SET (P:'a->bool) = \x. if x IN P then 1 else 0``); 953 954Theorem BAG_OF_SET_UNION: 955 !b b'. BAG_OF_SET (b UNION b') = (BAG_MERGE (BAG_OF_SET b) (BAG_OF_SET b')) 956Proof 957 rw[UNION_DEF,BAG_OF_SET,BAG_MERGE,FUN_EQ_THM] >> rw[] >> fs[] 958QED 959 960Theorem BAG_OF_SET_INSERT: 961 !e s. BAG_OF_SET (e INSERT s) = BAG_MERGE {|e|} (BAG_OF_SET s) 962Proof 963 rw[BAG_OF_SET,INSERT_DEF,BAG_MERGE,EMPTY_BAG,FUN_EQ_THM,BAG_INSERT] >> 964 rw[IN_DEF] 965 >- (fs[] >> 966 `s e = F` by metis_tac[] >> 967 fs[COND_CLAUSES]) 968 >- (`(x = e) = F` by metis_tac[] >> 969 fs[COND_CLAUSES]) 970 >- (`(x = e) = F` by metis_tac[] >> 971 `(s x) = T` by metis_tac[] >> 972 fs[COND_CLAUSES]) 973QED 974 975Theorem BAG_OF_SET_BAG_DIFF_DIFF: 976 !b s. (BAG_OF_SET s) - b = (BAG_OF_SET (s DIFF (SET_OF_BAG b))) 977Proof 978 simp[BAG_OF_SET,DIFF_DEF,FUN_EQ_THM,BAG_DIFF,SET_OF_BAG] >> 979 rw[BAG_IN,BAG_INN,IN_DEF] >> fs[] 980QED 981 982val SET_OF_EMPTY = store_thm ( 983 "SET_OF_EMPTY", 984 ``BAG_OF_SET (EMPTY:'a->bool) = EMPTY_BAG``, 985 SIMP_TAC (srw_ss()) [BAG_OF_SET, EMPTY_BAG, FUN_EQ_THM]) 986val _ = export_rewrites ["SET_OF_EMPTY"]; 987 988Theorem SET_OF_SINGLETON_BAG[simp]: 989 !e. SET_OF_BAG {|e|} = {e} 990Proof rw[SET_OF_BAG,FUN_EQ_THM] 991QED 992 993Theorem BAG_IN_BAG_OF_SET[simp]: 994 !P p. BAG_IN p (BAG_OF_SET P) <=> p IN P 995Proof SIMP_TAC std_ss [BAG_OF_SET, BAG_IN, BAG_INN, COND_RAND, COND_RATOR] 996QED 997 998val BAG_OF_EMPTY = store_thm ( 999 "BAG_OF_EMPTY", 1000 ``SET_OF_BAG (EMPTY_BAG:'a->num) = EMPTY``, 1001 SIMP_TAC std_ss [FUN_EQ_THM, SET_OF_BAG, NOT_IN_EMPTY_BAG, EMPTY_DEF]) 1002val _ = export_rewrites ["BAG_OF_EMPTY"] 1003 1004val SET_BAG_I = store_thm ( 1005 "SET_BAG_I", 1006 ``!s:'a->bool. SET_OF_BAG (BAG_OF_SET s) = s``, 1007 SRW_TAC [][SET_OF_BAG, BAG_OF_SET, FUN_EQ_THM, BAG_IN, BAG_INN, IN_DEF] THEN 1008 SRW_TAC [][]); 1009val _ = export_rewrites ["SET_BAG_I"] 1010 1011val SUB_BAG_SET = store_thm ( 1012 "SUB_BAG_SET", 1013 ``!b1 b2:'a->num. 1014 SUB_BAG b1 b2 ==> (SET_OF_BAG b1) SUBSET (SET_OF_BAG b2)``, 1015 SIMP_TAC std_ss [SUB_BAG, SET_OF_BAG, BAG_IN, SPECIFICATION, 1016 SUBSET_DEF]); 1017 1018val SET_OF_BAG_UNION = store_thm( 1019 "SET_OF_BAG_UNION", 1020 ``!b1 b2:'a->num. SET_OF_BAG (BAG_UNION b1 b2) = 1021 SET_OF_BAG b1 UNION SET_OF_BAG b2``, 1022 SRW_TAC [][SET_OF_BAG, EXTENSION] THEN SRW_TAC [][IN_DEF]); 1023 1024val SET_OF_BAG_MERGE = store_thm ( 1025 "SET_OF_BAG_MERGE", 1026 ``!b1 b2. SET_OF_BAG (BAG_MERGE b1 b2) = 1027 SET_OF_BAG b1 UNION SET_OF_BAG b2``, 1028 ONCE_REWRITE_TAC[EXTENSION] THEN 1029 SIMP_TAC std_ss [SET_OF_BAG, IN_UNION, IN_ABS, 1030 BAG_IN_BAG_MERGE]); 1031 1032val SET_OF_BAG_INSERT = Q.store_thm( 1033 "SET_OF_BAG_INSERT", 1034 `!e b. SET_OF_BAG (BAG_INSERT e b) = e INSERT (SET_OF_BAG b)`, 1035 SIMP_TAC std_ss [SET_OF_BAG, BAG_INSERT, INSERT_DEF, BAG_IN, 1036 EXTENSION, GSPECIFICATION, BAG_INN] THEN 1037 SIMP_TAC std_ss [SPECIFICATION] THEN REPEAT GEN_TAC THEN 1038 COND_CASES_TAC THEN SIMP_TAC std_ss []); 1039 1040Theorem SET_OF_EL_BAG[simp]: 1041 !e. SET_OF_BAG (EL_BAG e) = {e} 1042Proof SIMP_TAC std_ss [EL_BAG, SET_OF_BAG_INSERT, BAG_OF_EMPTY] 1043QED 1044 1045val SET_OF_BAG_DIFF_SUBSET_down = Q.store_thm( 1046 "SET_OF_BAG_DIFF_SUBSET_down", 1047 `!b1 b2. (SET_OF_BAG b1) DIFF (SET_OF_BAG b2) SUBSET 1048 SET_OF_BAG (BAG_DIFF b1 b2)`, 1049 SIMP_TAC std_ss [SUBSET_DEF, IN_DIFF, BAG_DIFF, SET_OF_BAG, BAG_IN, 1050 BAG_INN] THEN 1051 SIMP_TAC std_ss [SPECIFICATION]); 1052 1053val SET_OF_BAG_DIFF_SUBSET_up = Q.store_thm( 1054 "SET_OF_BAG_DIFF_SUBSET_up", 1055 `!b1 b2. SET_OF_BAG (BAG_DIFF b1 b2) SUBSET SET_OF_BAG b1`, 1056 SIMP_TAC std_ss [SUBSET_DEF, BAG_DIFF, SET_OF_BAG, BAG_IN, BAG_INN] 1057 THEN SIMP_TAC std_ss [SPECIFICATION]); 1058 1059Theorem IN_SET_OF_BAG[simp]: 1060 !x b. x IN SET_OF_BAG b <=> BAG_IN x b 1061Proof SIMP_TAC std_ss [SET_OF_BAG, SPECIFICATION] 1062QED 1063 1064val SET_OF_BAG_EQ_EMPTY = store_thm( 1065 "SET_OF_BAG_EQ_EMPTY", 1066 ``!b. (({} = SET_OF_BAG b) = (b = {||})) /\ 1067 ((SET_OF_BAG b = {}) = (b = {||}))``, 1068 GEN_TAC THEN 1069 Q.SPEC_THEN `b` STRIP_ASSUME_TAC BAG_cases THEN 1070 SRW_TAC [][SET_OF_BAG_INSERT]) 1071 before 1072 export_rewrites ["SET_OF_BAG_EQ_EMPTY"]; 1073 1074Theorem BAG_OF_SET_EQ_INSERT: 1075 !e b s. (BAG_INSERT e b = BAG_OF_SET s) ==> (?s'. s = (e INSERT s')) 1076Proof 1077 rw[] >> 1078 qexists_tac `s DELETE e` >> 1079 rw[INSERT_DEF,DELETE_DEF] >> 1080 simp[FUN_EQ_THM] >> 1081 rw[IN_DEF] >> 1082 EQ_TAC 1083 >- simp[] 1084 >- (rw[] >> 1085 `?t. s = (e INSERT t)` 1086 by metis_tac[DECOMPOSITION, BAG_IN_BAG_OF_SET, BAG_IN_BAG_INSERT] >> 1087 fs[]) 1088QED 1089 1090 1091val _ = print "Bag disjointness\n" 1092val BAG_DISJOINT = new_definition( 1093 "BAG_DISJOINT", 1094 ``BAG_DISJOINT (b1:'a->num) b2 = 1095 DISJOINT (SET_OF_BAG b1) (SET_OF_BAG b2)``); 1096 1097val BAG_DISJOINT_EMPTY = store_thm( 1098 "BAG_DISJOINT_EMPTY[simp]", 1099 ``!b:'a->num. 1100 BAG_DISJOINT b EMPTY_BAG /\ BAG_DISJOINT EMPTY_BAG b``, 1101 REWRITE_TAC [BAG_OF_EMPTY, BAG_DISJOINT, DISJOINT_EMPTY]); 1102 1103val BAG_DISJOINT_DIFF = store_thm( 1104 "BAG_DISJOINT_DIFF", 1105 ``!B1 B2:'a->num. 1106 BAG_DISJOINT (BAG_DIFF B1 B2) (BAG_DIFF B2 B1)``, 1107 SIMP_TAC std_ss [INTER_DEF, DISJOINT_DEF, BAG_DISJOINT, BAG_DIFF, 1108 SET_OF_BAG, BAG_IN, BAG_INN, EXTENSION, 1109 GSPECIFICATION, NOT_IN_EMPTY] THEN 1110 SIMP_TAC std_ss [SPECIFICATION]); 1111 1112val BAG_DISJOINT_BAG_IN = store_thm ( 1113 "BAG_DISJOINT_BAG_IN", 1114 ``!b1 b2. BAG_DISJOINT b1 b2 = 1115 !e. ~(BAG_IN e b1) \/ ~(BAG_IN e b2)``, 1116 SIMP_TAC std_ss [BAG_DISJOINT, DISJOINT_DEF, 1117 EXTENSION, NOT_IN_EMPTY, 1118 IN_INTER, IN_SET_OF_BAG]); 1119 1120val BAG_DISJOINT_BAG_INSERT = store_thm ( 1121 "BAG_DISJOINT_BAG_INSERT", 1122 ``(!b1 b2 e1. 1123 BAG_DISJOINT (BAG_INSERT e1 b1) b2 = 1124 (~(BAG_IN e1 b2) /\ (BAG_DISJOINT b1 b2))) /\ 1125 (!b1 b2 e2. 1126 BAG_DISJOINT b1 (BAG_INSERT e2 b2) = 1127 (~(BAG_IN e2 b1) /\ (BAG_DISJOINT b1 b2)))``, 1128 SIMP_TAC std_ss [BAG_DISJOINT_BAG_IN, 1129 BAG_IN_BAG_INSERT] THEN 1130 METIS_TAC[]); 1131 1132val BAG_DISJOINT_BAG_UNION = store_thm( 1133 "BAG_DISJOINT_BAG_UNION[simp]", 1134 ``(BAG_DISJOINT b1 (BAG_UNION b2 b3) <=> 1135 BAG_DISJOINT b1 b2 /\ BAG_DISJOINT b1 b3) /\ 1136 (BAG_DISJOINT (BAG_UNION b1 b2) b3 <=> 1137 BAG_DISJOINT b1 b3 /\ BAG_DISJOINT b2 b3)``, 1138 SIMP_TAC (srw_ss()) [BAG_DISJOINT, SET_OF_BAG_UNION] THEN 1139 METIS_TAC[DISJOINT_SYM]); 1140 1141val _ = print "Developing theory of finite bags\n" 1142 1143val FINITE_BAG = Q.new_definition( 1144 "FINITE_BAG", 1145 `FINITE_BAG (b:'a->num) = 1146 !P. P EMPTY_BAG /\ (!b. P b ==> (!e. P (BAG_INSERT e b))) ==> 1147 P b`); 1148 1149val FINITE_EMPTY_BAG = Q.store_thm( 1150 "FINITE_EMPTY_BAG", 1151 `FINITE_BAG EMPTY_BAG`, 1152 SIMP_TAC std_ss [FINITE_BAG]); 1153 1154val FINITE_BAG_INSERT = Q.store_thm( 1155 "FINITE_BAG_INSERT", 1156 `!b. FINITE_BAG b ==> (!e. FINITE_BAG (BAG_INSERT e b))`, 1157 REWRITE_TAC [FINITE_BAG] THEN MESON_TAC []); 1158 1159val FINITE_BAG_INDUCT = Q.store_thm( 1160 "FINITE_BAG_INDUCT", 1161 `!P. P EMPTY_BAG /\ 1162 (!b. P b ==> (!e. P (BAG_INSERT e b))) ==> 1163 (!b. FINITE_BAG b ==> P b)`, 1164 SIMP_TAC std_ss [FINITE_BAG]); 1165 1166val STRONG_FINITE_BAG_INDUCT = save_thm( 1167 "STRONG_FINITE_BAG_INDUCT", 1168 FINITE_BAG_INDUCT 1169 |> Q.SPEC `\b. FINITE_BAG b /\ P b` 1170 |> SIMP_RULE std_ss [FINITE_EMPTY_BAG, FINITE_BAG_INSERT] 1171 |> GEN_ALL) 1172 1173val _ = IndDefLib.export_rule_induction "STRONG_FINITE_BAG_INDUCT"; 1174 1175val FINITE_BAG_INSERT_down' = prove( 1176 ``!b. FINITE_BAG b ==> (!e b0. (b = BAG_INSERT e b0) ==> FINITE_BAG b0)``, 1177 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1178 SIMP_TAC std_ss [BAG_INSERT_NOT_EMPTY] THEN 1179 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `e = e'` THENL [ 1180 ELIM_TAC THEN IMP_RES_TAC BAG_INSERT_ONE_ONE THEN ELIM_TAC THEN 1181 ASM_SIMP_TAC std_ss [], 1182 ALL_TAC 1183 ] THEN Q.SUBGOAL_THEN `?b'. b = BAG_INSERT e' b'` STRIP_ASSUME_TAC 1184 THENL [ 1185 SIMP_TAC std_ss [GSYM BAG_DELETE] THEN 1186 MATCH_MP_TAC BAG_IN_BAG_DELETE THEN 1187 FULL_SIMP_TAC (srw_ss()) [BAG_INSERT_EQUAL], 1188 RES_TAC THEN ELIM_TAC THEN 1189 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [BAG_INSERT_commutes]) THEN 1190 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][FINITE_BAG_INSERT] 1191 ]) 1192 1193val FINITE_BAG_INSERT = Q.prove( 1194`!e b. FINITE_BAG (BAG_INSERT e b) = FINITE_BAG b`, 1195 MESON_TAC [FINITE_BAG_INSERT, FINITE_BAG_INSERT_down']) 1196 1197val FINITE_BAG_THM = save_thm( 1198 "FINITE_BAG_THM", 1199 CONJ FINITE_EMPTY_BAG FINITE_BAG_INSERT) 1200 before 1201 export_rewrites ["FINITE_BAG_THM"]; 1202 1203val FINITE_BAG_DIFF = Q.store_thm( 1204 "FINITE_BAG_DIFF", 1205 `!b1. FINITE_BAG b1 ==> !b2. FINITE_BAG (BAG_DIFF b1 b2)`, 1206 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1207 SIMP_TAC std_ss [BAG_DIFF_EMPTY, FINITE_BAG_THM] THEN 1208 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [ 1209 IMP_RES_TAC (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE) THEN 1210 ASM_SIMP_TAC std_ss [BAG_DIFF_INSERT_same], 1211 ASM_SIMP_TAC std_ss [BAG_DIFF_INSERT, FINITE_BAG_THM] 1212 ]); 1213 1214val FINITE_BAG_DIFF_dual = Q.store_thm( 1215 "FINITE_BAG_DIFF_dual", 1216 `!b1. FINITE_BAG b1 ==> 1217 !b2. FINITE_BAG (BAG_DIFF b2 b1) ==> FINITE_BAG b2`, 1218 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1219 REWRITE_TAC [BAG_DIFF_EMPTY] THEN 1220 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [ 1221 IMP_RES_TAC (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE) THEN 1222 ELIM_TAC THEN ASM_MESON_TAC [FINITE_BAG_THM, BAG_DIFF_INSERT_same], 1223 ASM_MESON_TAC [NOT_IN_BAG_DIFF] 1224 ]); 1225 1226val FINITE_BAG_UNION_1 = prove( 1227 Term`!b1. FINITE_BAG b1 ==> 1228 !b2. FINITE_BAG b2 ==> FINITE_BAG (BAG_UNION b1 b2)`, 1229 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1230 SIMP_TAC std_ss [FINITE_BAG_THM, BAG_UNION_EMPTY, BAG_UNION_INSERT]); 1231val FINITE_BAG_UNION_2 = prove( 1232 ``!b. FINITE_BAG b ==> 1233 !b1 b2. (b = BAG_UNION b1 b2) ==> FINITE_BAG b1 /\ FINITE_BAG b2``, 1234 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN 1235 MAP_EVERY IMP_RES_TAC [BAG_INSERT_EQ_UNION, 1236 REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE] THEN 1237 ELIM_TAC THEN 1238 FULL_SIMP_TAC std_ss [BAG_UNION_INSERT, BAG_INSERT_ONE_ONE, 1239 FINITE_BAG_THM] THEN METIS_TAC []); 1240 1241Theorem FINITE_BAG_UNION[simp]: 1242 !b1 b2. FINITE_BAG (BAG_UNION b1 b2) <=> 1243 FINITE_BAG b1 /\ FINITE_BAG b2 1244Proof MESON_TAC [FINITE_BAG_UNION_1, FINITE_BAG_UNION_2] 1245QED 1246 1247val FINITE_SUB_BAG = Q.store_thm( 1248 "FINITE_SUB_BAG", 1249 `!b1. FINITE_BAG b1 ==> !b2. SUB_BAG b2 b1 ==> FINITE_BAG b2`, 1250 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1251 SIMP_TAC std_ss [SUB_BAG_EMPTY, FINITE_BAG_THM] THEN 1252 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [ 1253 IMP_RES_TAC (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE) THEN 1254 ELIM_TAC THEN FULL_SIMP_TAC std_ss [SUB_BAG_INSERT, FINITE_BAG_THM], 1255 ASM_MESON_TAC [NOT_IN_SUB_BAG_INSERT] 1256 ]); 1257 1258Theorem FINITE_BAG_MERGE[simp]: 1259 !a b. FINITE_BAG (BAG_MERGE a b) <=> FINITE_BAG a /\ FINITE_BAG b 1260Proof 1261 rw[] >> 1262 reverse(EQ_TAC) 1263 >- (`BAG_MERGE a b <= a + b` by metis_tac[BAG_MERGE_SUB_BAG_UNION] >> 1264 rw[] >> 1265 `FINITE_BAG (a + b)` by metis_tac[FINITE_BAG_UNION] >> 1266 metis_tac[FINITE_SUB_BAG]) 1267 >- (`!c:'a bag. FINITE_BAG c ==> !a b. (c = BAG_MERGE a b) 1268 ==> FINITE_BAG a /\ FINITE_BAG b` suffices_by metis_tac[] >> 1269 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT >> 1270 rw[] >> 1271 `BAG_MERGE a b = BAG_INSERT e (BAG_MERGE (a - {|e|}) (b - {|e|}))` 1272 by metis_tac[BAG_INSERT_EQ_MERGE_DIFF] >> 1273 fs[] >> 1274 rw[] >> 1275 first_x_assum (qspecl_then [`a - {|e|}`,`b - {|e|}`] mp_tac) >> 1276 rw[] >> 1277 metis_tac[FINITE_BAG_DIFF_dual,FINITE_BAG]) 1278QED 1279 1280val _ = print "Developing theory of bag cardinality\n" 1281 1282val BAG_CARD_RELn = Q.new_definition( 1283 "BAG_CARD_RELn", 1284 `BAG_CARD_RELn (b:'a->num) n = 1285 !P. P EMPTY_BAG 0 /\ 1286 (!b n. P b n ==> (!e. P (BAG_INSERT e b) (SUC n))) ==> 1287 P b n`); 1288 1289val BCARD_imps = prove( 1290 Term`(BAG_CARD_RELn EMPTY_BAG 0) /\ 1291 (!b n. BAG_CARD_RELn b n ==> 1292 (!e. BAG_CARD_RELn (BAG_INSERT e b) (n + 1)))`, 1293 REWRITE_TAC [BAG_CARD_RELn, arithmeticTheory.ADD1] THEN MESON_TAC []) 1294 1295val BCARD_induct = prove( 1296 Term`!P. P EMPTY_BAG 0 /\ 1297 (!b n. P b n ==> (!e. P (BAG_INSERT e b) (n + 1))) ==> 1298 (!b n. BAG_CARD_RELn b n ==> P b n)`, 1299 REWRITE_TAC [BAG_CARD_RELn, arithmeticTheory.ADD1] THEN MESON_TAC []); 1300 1301val strong_BCARD_induct = 1302 BCARD_induct |> Q.SPEC `\b n. BAG_CARD_RELn b n /\ P b n` 1303 |> SIMP_RULE std_ss [BCARD_imps] 1304 1305val BCARD_R_cases = prove( 1306 Term`!b n. BAG_CARD_RELn b n ==> 1307 (b = EMPTY_BAG) /\ (n = 0) \/ 1308 (?b0 e m. (b = BAG_INSERT e b0) /\ 1309 BAG_CARD_RELn b0 m /\ (n = m + 1))`, 1310 HO_MATCH_MP_TAC BCARD_induct THEN SIMP_TAC std_ss [] THEN 1311 REPEAT STRIP_TAC THEN ELIM_TAC THEN ASM_MESON_TAC [BCARD_imps]); 1312 1313val BCARD_rwts = prove( 1314 Term`!b n. BAG_CARD_RELn b n <=> 1315 (b = EMPTY_BAG) /\ (n = 0) \/ 1316 (?b0 e m. (b = BAG_INSERT e b0) /\ (n = m + 1) /\ 1317 BAG_CARD_RELn b0 m)`, 1318 METIS_TAC [BCARD_R_cases, BCARD_imps]); 1319 1320val BCARD_BINSERT_indifferent = prove( 1321 Term`!b n. BAG_CARD_RELn b n ==> 1322 !b0 e. (b = BAG_INSERT e b0) ==> 1323 BAG_CARD_RELn b0 (n - 1) /\ ~(n = 0)`, 1324 HO_MATCH_MP_TAC strong_BCARD_induct THEN SRW_TAC [][] THEN 1325 FULL_SIMP_TAC (srw_ss()) [BAG_INSERT_EQUAL] THEN1 SRW_TAC [][] THEN 1326 `BAG_CARD_RELn k (n - 1) /\ n <> 0` by METIS_TAC [] THEN 1327 `n = (n - 1) + 1` by DECIDE_TAC THEN METIS_TAC [BCARD_imps]); 1328 1329val BCARD_BINSERT' = 1330 SIMP_RULE bool_ss [GSYM RIGHT_FORALL_IMP_THM] BCARD_BINSERT_indifferent 1331 1332val BCARD_EMPTY = prove( 1333 Term`!n. BAG_CARD_RELn EMPTY_BAG n = (n = 0)`, 1334 ONCE_REWRITE_TAC [BCARD_rwts] THEN 1335 SIMP_TAC std_ss [BAG_INSERT_NOT_EMPTY]); 1336 1337val BCARD_BINSERT = prove( 1338 Term`!b e n. BAG_CARD_RELn (BAG_INSERT e b) n = 1339 (?m. (n = m + 1) /\ BAG_CARD_RELn b m)`, 1340 SRW_TAC [][EQ_IMP_THM] THENL [ 1341 IMP_RES_TAC BCARD_BINSERT' THEN Q.EXISTS_TAC `n - 1` THEN 1342 ASM_SIMP_TAC std_ss [], 1343 ASM_MESON_TAC [BCARD_imps] 1344 ]); 1345 1346val BCARD_RWT = CONJ BCARD_EMPTY BCARD_BINSERT 1347 1348val BCARD_R_det = prove( 1349 Term`!b n. BAG_CARD_RELn b n ==> 1350 !n'. BAG_CARD_RELn b n' ==> (n' = n)`, 1351 HO_MATCH_MP_TAC BCARD_induct THEN CONJ_TAC THENL [ 1352 ONCE_REWRITE_TAC [BCARD_rwts] THEN 1353 SIMP_TAC std_ss [BAG_INSERT_NOT_EMPTY], 1354 REPEAT STRIP_TAC THEN IMP_RES_TAC BCARD_BINSERT THEN RES_TAC THEN 1355 ASM_SIMP_TAC std_ss [] 1356 ]); 1357 1358val FINITE_BAGS_BCARD = prove( 1359 Term`!b. FINITE_BAG b ==> ?n. BAG_CARD_RELn b n`, 1360 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN MESON_TAC [BCARD_imps]); 1361 1362val BAG_CARD = new_specification 1363 ("BAG_CARD",["BAG_CARD"], 1364 CONV_RULE SKOLEM_CONV ( 1365 SIMP_RULE std_ss 1366 [GSYM boolTheory.RIGHT_EXISTS_IMP_THM] FINITE_BAGS_BCARD)); 1367 1368val BAG_CARD_EMPTY = 1369 BAG_CARD |> Q.SPEC `EMPTY_BAG` 1370 |> SIMP_RULE std_ss [FINITE_EMPTY_BAG] 1371 |> ONCE_REWRITE_RULE [BCARD_rwts] 1372 |> SIMP_RULE std_ss [BAG_INSERT_NOT_EMPTY] 1373val _ = save_thm("BAG_CARD_EMPTY", BAG_CARD_EMPTY); 1374val _ = export_rewrites ["BAG_CARD_EMPTY"]; 1375 1376val BCARD_0 = Q.store_thm( 1377 "BCARD_0", 1378 `!b. FINITE_BAG b ==> ((BAG_CARD b = 0) = (b = EMPTY_BAG))`, 1379 GEN_TAC THEN STRIP_TAC THEN EQ_TAC THEN 1380 SIMP_TAC std_ss [BAG_CARD_EMPTY] THEN 1381 IMP_RES_TAC BAG_CARD THEN DISCH_THEN SUBST_ALL_TAC THEN 1382 FULL_SIMP_TAC (srw_ss()) [Once BCARD_rwts]); 1383 1384val BAG_CARD_EL_BAG = prove( 1385 Term`!e. BAG_CARD (EL_BAG e) = 1`, 1386 GEN_TAC THEN SIMP_TAC std_ss [EL_BAG] THEN 1387 Q.SUBGOAL_THEN `FINITE_BAG (BAG_INSERT e EMPTY_BAG)` ASSUME_TAC 1388 THENL [MESON_TAC [FINITE_BAG_INSERT, FINITE_EMPTY_BAG], 1389 ALL_TAC] THEN IMP_RES_TAC BAG_CARD THEN 1390 FULL_SIMP_TAC std_ss [BCARD_RWT]) 1391 1392val BAG_CARD_INSERT = prove( 1393 Term`!b. FINITE_BAG b ==> 1394 !e. BAG_CARD (BAG_INSERT e b) = BAG_CARD b + 1`, 1395 REPEAT STRIP_TAC THEN 1396 Q.SUBGOAL_THEN `FINITE_BAG (BAG_INSERT e b)` ASSUME_TAC THENL [ 1397 ASM_MESON_TAC [FINITE_BAG_INSERT], ALL_TAC] THEN 1398 IMP_RES_TAC BAG_CARD THEN 1399 FULL_SIMP_TAC std_ss [BCARD_RWT] THEN IMP_RES_TAC BCARD_R_det); 1400 1401val BAG_CARD_THM = save_thm( 1402 "BAG_CARD_THM", 1403 CONJ BAG_CARD_EMPTY BAG_CARD_INSERT); 1404 1405val BAG_CARD_UNION = store_thm ( 1406 "BAG_CARD_UNION", 1407 Term `!b1 b2. FINITE_BAG b1 /\ FINITE_BAG b2 ==> 1408 (BAG_CARD (BAG_UNION b1 b2) = 1409 (BAG_CARD b1) + (BAG_CARD b2))`, 1410 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN 1411 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1412 SIMP_TAC arith_ss [BAG_UNION_INSERT, BAG_UNION_EMPTY, 1413 BAG_CARD_THM, FINITE_BAG_UNION]); 1414val _ = export_rewrites ["BAG_CARD_UNION"] 1415 1416 1417val BCARD_SUC = Q.store_thm( 1418 "BCARD_SUC", 1419 `!b. FINITE_BAG b ==> 1420 !n. (BAG_CARD b = SUC n) = 1421 (?b0 e. (b = BAG_INSERT e b0) /\ (BAG_CARD b0 = n))`, 1422 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `b` BAG_cases) THEN 1423 SIMP_TAC std_ss [BAG_CARD_THM, BAG_INSERT_NOT_EMPTY, 1424 FINITE_BAG_THM, arithmeticTheory.ADD1] THEN 1425 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 1426 ASM_MESON_TAC [], 1427 FIRST_ASSUM (MP_TAC o Q.AP_TERM `BAG_CARD`) THEN 1428 ASM_SIMP_TAC std_ss [BAG_CARD_THM] THEN 1429 Q.SUBGOAL_THEN `FINITE_BAG b0'` ASSUME_TAC THENL [ 1430 ASM_MESON_TAC [FINITE_BAG_THM], 1431 ASM_SIMP_TAC std_ss [BAG_CARD_THM] 1432 ] 1433 ]); 1434 1435val BAG_CARD_BAG_INN = Q.store_thm( 1436 "BAG_CARD_BAG_INN", 1437 `!b. FINITE_BAG b ==> !n e. BAG_INN e n b ==> n <= BAG_CARD b`, 1438 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1439 SIMP_TAC std_ss [BAG_CARD_THM, BAG_INN_BAG_INSERT, 1440 BAG_INN_EMPTY_BAG] THEN REPEAT STRIP_TAC 1441 THENL [ 1442 ELIM_TAC THEN RES_TAC THEN ASM_SIMP_TAC std_ss [], 1443 RES_TAC THEN ASM_SIMP_TAC std_ss [] 1444 ]); 1445 1446val SUB_BAG_DIFF_EQ = Q.store_thm 1447("SUB_BAG_DIFF_EQ", 1448 `!b1 b2. SUB_BAG b1 b2 ==> (b2 = BAG_UNION b1 (BAG_DIFF b2 b1))`, 1449 RW_TAC bool_ss [SUB_BAG,BAG_UNION,BAG_DIFF,BAG_INN,FUN_EQ_THM] 1450 THEN MATCH_MP_TAC (ARITH `a >= b ==> (a = b + (a - b))`) 1451 THEN POP_ASSUM (MP_TAC o Q.SPECL [`x`, `b1 x`]) 1452 THEN RW_TAC arith_ss []); 1453 1454val SUB_BAG_DIFF_EXISTS = Q.prove 1455(`!b1 b2. SUB_BAG b1 b2 ==> ?d. b2 = BAG_UNION b1 d`, 1456 PROVE_TAC [SUB_BAG_DIFF_EQ]); 1457 1458val SUB_BAG_CARD = Q.store_thm 1459("SUB_BAG_CARD", 1460`!b1 b2:'a bag. FINITE_BAG b2 /\ SUB_BAG b1 b2 ==> BAG_CARD b1 <= BAG_CARD b2`, 1461RW_TAC bool_ss [] 1462 THEN `?d. b2 = BAG_UNION b1 d` by PROVE_TAC [SUB_BAG_DIFF_EQ] 1463 THEN RW_TAC bool_ss [] 1464 THEN `FINITE_BAG d /\ FINITE_BAG b1` by PROVE_TAC [FINITE_BAG_UNION] 1465 THEN Q.PAT_X_ASSUM `SUB_BAG x y` (K ALL_TAC) 1466 THEN Q.PAT_X_ASSUM `FINITE_BAG (BAG_UNION x y)` (K ALL_TAC) 1467 THEN REPEAT (POP_ASSUM MP_TAC) 1468 THEN Q.ID_SPEC_TAC `d` 1469 THEN HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT 1470 THEN RW_TAC arith_ss [BAG_UNION_EMPTY,BAG_UNION_INSERT] 1471 THEN PROVE_TAC [BAG_CARD_THM,FINITE_BAG_UNION,ARITH `x <=y ==> x <= y+1`]); 1472 1473Theorem BAG_MERGE_CARD: 1474 !a b. FINITE_BAG a /\ FINITE_BAG b ==> 1475 BAG_CARD (BAG_MERGE a b) <= (BAG_CARD a + BAG_CARD b) 1476Proof 1477 rw[] >> 1478 `(BAG_MERGE a b) <= (a + b)` 1479 by metis_tac[BAG_MERGE_SUB_BAG_UNION] >> 1480 `FINITE_BAG (a + b)` by metis_tac[FINITE_BAG_UNION] >> 1481 `BAG_CARD (BAG_MERGE a b) <= BAG_CARD (a + b)` 1482 by metis_tac[SUB_BAG_CARD] >> 1483 metis_tac[BAG_CARD_UNION] 1484QED 1485 1486val _ = ParseExtras.temp_tight_equality() 1487val BAG_CARD_DIFF = store_thm( 1488 "BAG_CARD_DIFF", 1489 ``!b. FINITE_BAG b ==> 1490 !c. c <= b ==> BAG_CARD (b - c) = BAG_CARD b - BAG_CARD c``, 1491 Induct_on `FINITE_BAG` >> simp[BAG_CARD_THM] >> qx_gen_tac `b` >> strip_tac >> 1492 map_every qx_gen_tac [`e`, `c`] >> strip_tac >> 1493 `FINITE_BAG c` by metis_tac[FINITE_BAG_THM, FINITE_SUB_BAG] >> 1494 Cases_on `BAG_IN e c` 1495 >- (`?c0. c = BAG_INSERT e c0` by metis_tac[BAG_DECOMPOSE] >> 1496 lfs[BAG_CARD_THM, SUB_BAG_INSERT]) >> 1497 simp[BAG_DIFF_INSERT, BAG_CARD_THM, FINITE_BAG_DIFF] >> 1498 lfs[NOT_IN_SUB_BAG_INSERT] >> 1499 `BAG_CARD c <= BAG_CARD b` by simp[SUB_BAG_CARD] >> simp[]); 1500 1501(* -------------------------------------------------------------------- 1502 FILTER for bags (alternatively, intersection with a set) 1503 ---------------------------------------------------------------------- *) 1504 1505val BAG_FILTER_DEF = new_definition( 1506 "BAG_FILTER_DEF", 1507 ``BAG_FILTER P (b :'a bag) : 'a bag = \e. if P e then b e else 0``); 1508 1509val BAG_FILTER_EMPTY = store_thm( 1510 "BAG_FILTER_EMPTY", 1511 ``BAG_FILTER P {||} = {||}``, 1512 SRW_TAC [][BAG_FILTER_DEF, FUN_EQ_THM] THEN 1513 SRW_TAC [][EMPTY_BAG]) 1514 before 1515 export_rewrites ["BAG_FILTER_EMPTY"]; 1516 1517val BAG_FILTER_BAG_INSERT = store_thm( 1518 "BAG_FILTER_BAG_INSERT", 1519 ``BAG_FILTER P (BAG_INSERT e b) = if P e then BAG_INSERT e (BAG_FILTER P b) 1520 else BAG_FILTER P b``, 1521 SRW_TAC [][BAG_FILTER_DEF, FUN_EQ_THM] THEN 1522 SRW_TAC [][BAG_INSERT] THEN RES_TAC) 1523 before 1524 export_rewrites ["BAG_FILTER_BAG_INSERT"]; 1525 1526val FINITE_BAG_FILTER = store_thm( 1527 "FINITE_BAG_FILTER", 1528 ``!b. FINITE_BAG b ==> FINITE_BAG (BAG_FILTER P b)``, 1529 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN 1530 SRW_TAC [][]) 1531 before 1532 export_rewrites ["FINITE_BAG_FILTER"]; 1533 1534val BAG_INN_BAG_FILTER = store_thm( 1535 "BAG_INN_BAG_FILTER", 1536 ``BAG_INN e n (BAG_FILTER P b) <=> (n = 0) \/ P e /\ BAG_INN e n b``, 1537 SRW_TAC [numSimps.ARITH_ss][BAG_FILTER_DEF, BAG_INN]); 1538val _ = export_rewrites ["BAG_INN_BAG_FILTER"] 1539 1540val BAG_IN_BAG_FILTER = store_thm( 1541 "BAG_IN_BAG_FILTER", 1542 ``BAG_IN e (BAG_FILTER P b) <=> P e /\ BAG_IN e b``, 1543 SRW_TAC [][BAG_IN]) 1544 before 1545 export_rewrites ["BAG_IN_BAG_FILTER"]; 1546 1547val BAG_FILTER_FILTER = store_thm( 1548 "BAG_FILTER_FILTER", 1549 ``BAG_FILTER P (BAG_FILTER Q b) = BAG_FILTER (\a. P a /\ Q a) b``, 1550 simp[BAG_FILTER_DEF] >> simp[FUN_EQ_THM] >> rw[] >> fs[]); 1551 1552val BAG_FILTER_SUB_BAG = store_thm( 1553 "BAG_FILTER_SUB_BAG[simp]", 1554 ``!P b. BAG_FILTER P b <= b``, 1555 dsimp[BAG_FILTER_DEF, SUB_BAG]); 1556 1557Theorem BAG_OF_SET_DIFF: 1558 !b b'. BAG_OF_SET (b DIFF b') = BAG_FILTER (COMPL b') (BAG_OF_SET b) 1559Proof 1560 rw[DIFF_DEF,BAG_OF_SET,BAG_FILTER_DEF] >> metis_tac[] 1561QED 1562 1563val SET_OF_BAG_EQ_INSERT = store_thm( 1564 "SET_OF_BAG_EQ_INSERT", 1565 ``!b e s. 1566 (e INSERT s = SET_OF_BAG b) = 1567 ?b0 eb. (b = BAG_UNION eb b0) /\ 1568 (s = SET_OF_BAG b0) /\ 1569 (!e'. BAG_IN e' eb ==> (e' = e)) /\ 1570 (~(e IN s) ==> BAG_IN e eb)``, 1571 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 1572 `BAG_IN e b` by METIS_TAC [IN_INSERT, IN_SET_OF_BAG] THEN 1573 Cases_on `e IN s` THENL [ 1574 MAP_EVERY Q.EXISTS_TAC [`b`, `{||}`] THEN 1575 SRW_TAC [][] THEN METIS_TAC [ABSORPTION], 1576 MAP_EVERY Q.EXISTS_TAC [`BAG_FILTER ((~) o (=) e) b`, 1577 `BAG_FILTER ((=) e) b`] THEN 1578 REPEAT CONJ_TAC THENL [ 1579 SRW_TAC [boolSimps.DNF_ss, boolSimps.CONJ_ss] 1580 [BAG_EXTENSION, BAG_INN_BAG_UNION] THEN 1581 PROVE_TAC [BAG_INN_0], 1582 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN PROVE_TAC [], 1583 SRW_TAC [][], 1584 SRW_TAC [][] 1585 ] 1586 ], 1587 SRW_TAC [][EXTENSION, BAG_IN_BAG_UNION] THEN 1588 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [] 1589 ]); 1590 1591val FINITE_SET_OF_BAG = store_thm( 1592 "FINITE_SET_OF_BAG", 1593 ``!b. FINITE (SET_OF_BAG b) = FINITE_BAG b``, 1594 Q_TAC SUFF_TAC 1595 `(!b:'a bag. FINITE_BAG b ==> FINITE (SET_OF_BAG b)) /\ 1596 (!s:'a set. FINITE s ==> 1597 !b. (s = SET_OF_BAG b) ==> FINITE_BAG b)` THEN1 1598 METIS_TAC [] THEN CONJ_TAC 1599 THENL [ 1600 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1601 SRW_TAC [][SET_OF_BAG_INSERT], 1602 HO_MATCH_MP_TAC FINITE_INDUCT THEN 1603 SRW_TAC [][SET_OF_BAG_EQ_INSERT, SET_OF_BAG_EQ_EMPTY] THEN 1604 SRW_TAC [][FINITE_BAG_UNION] THEN 1605 Q_TAC SUFF_TAC `!n b e. (b e = n) /\ (!e'. BAG_IN e' b ==> (e' = e)) ==> 1606 FINITE_BAG b` THEN1 METIS_TAC [] THEN 1607 REPEAT (POP_ASSUM (K ALL_TAC)) THEN Induct THENL [ 1608 REPEAT STRIP_TAC THEN 1609 Q_TAC SUFF_TAC `b = {||}` THEN1 SRW_TAC [][] THEN 1610 SRW_TAC [][BAG_EXTENSION] THEN 1611 FULL_SIMP_TAC (srw_ss()) [BAG_INN, BAG_IN] THEN EQ_TAC THENL [ 1612 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 1613 `b e' >= 1` 1614 by PROVE_TAC [numLib.ARITH_PROVE 1615 ``x >= n /\ ~(n = 0) ==> x >= 1n``] THEN 1616 `b e' = 0` by PROVE_TAC [] THEN 1617 FULL_SIMP_TAC (srw_ss()) [], 1618 SIMP_TAC (srw_ss()) [] 1619 ], 1620 REPEAT STRIP_TAC THEN 1621 `BAG_IN e b` by SRW_TAC [numSimps.ARITH_ss][BAG_IN, BAG_INN] THEN 1622 `?b0. b = BAG_INSERT e b0` 1623 by PROVE_TAC [BAG_IN_BAG_DELETE, BAG_DELETE] THEN 1624 POP_ASSUM SUBST_ALL_TAC THEN 1625 FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM] THEN 1626 `b0 e = n` 1627 by FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) [BAG_INSERT] THEN 1628 PROVE_TAC [] 1629 ] 1630 ]) 1631 before 1632 export_rewrites ["FINITE_SET_OF_BAG"]; 1633 1634Theorem FINITE_BAG_OF_SET[simp]: 1635 !s. FINITE_BAG (BAG_OF_SET s) <=> FINITE s 1636Proof 1637 rw[] >> EQ_TAC 1638 >- (`!c. FINITE_BAG c ==> !s. (c = BAG_OF_SET s) ==> FINITE s` 1639 suffices_by metis_tac[] >> 1640 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT >> 1641 rw[] 1642 >- (Cases_on `s={}` >- rw[] >> 1643 `?e. e IN s` by simp[pred_setTheory.MEMBER_NOT_EMPTY] >> 1644 fs[BAG_OF_SET,EMPTY_BAG_alt,FUN_EQ_THM] >> 1645 first_x_assum (qspec_then `e` mp_tac) >> 1646 rw[]) 1647 >- (`e IN s` 1648 by metis_tac[BAG_IN_BAG_OF_SET, 1649 BAG_DECOMPOSE,BAG_IN_BAG_INSERT] >> 1650 `?t. s = (e INSERT t)` 1651 by metis_tac[DECOMPOSITION] >> 1652 fs[BAG_OF_SET_INSERT] >> 1653 `(BAG_MERGE {|e|} (BAG_OF_SET t)) 1654 = (BAG_INSERT e 1655 (BAG_MERGE ({|e|}-{|e|}) ((BAG_OF_SET t)-{|e|})))` 1656 by metis_tac[BAG_INSERT_EQ_MERGE_DIFF] >> 1657 fs[BAG_MERGE_EMPTY] >> 1658 `BAG_OF_SET t - {|e|} = BAG_OF_SET (t DIFF {e})` 1659 by (simp[BAG_OF_SET_BAG_DIFF_DIFF] >> 1660 metis_tac[SET_OF_EL_BAG,EL_BAG]) >> 1661 first_x_assum (qspec_then `t DIFF {e}` mp_tac) >> DISCH_TAC >> 1662 metis_tac[FINITE_DIFF_down,FINITE_DEF])) 1663 >- (rw[] >> 1664 Induct_on `s` >> 1665 simp[SET_OF_EMPTY] >> 1666 rw[] >> 1667 simp[BAG_OF_SET_INSERT] >> 1668 simp[FINITE_BAG_MERGE]) 1669QED 1670 1671 1672(* ---------------------------------------------------------------------- 1673 IMAGE for bags. 1674 1675 This is complicated by the fact that a taking the image of a 1676 non-injective function over an infinite bag might produce a bag that 1677 wanted to have an infinite number of some element. For example, 1678 BAG_IMAGE (\e. 1) (BAG_OF_SET (UNIV : num set)) 1679 would want to populate a bag with an infinite number of ones. 1680 1681 BAG_IMAGE is "safe" if the input bag is finite, or if the function is 1682 only finitely non-injective. I don't want to have these side conditions 1683 hanging around on my theorems, so I've decided to simply make BAG_IMAGE 1684 take elements that want to be infinite to one instead. 1685 ---------------------------------------------------------------------- *) 1686 1687val _ = augment_srw_ss [simpLib.rewrites [LET_THM]] 1688val BAG_IMAGE_DEF = new_definition( 1689 "BAG_IMAGE_DEF", 1690 ``BAG_IMAGE f b = \e. let sb = BAG_FILTER (\e0. f e0 = e) b 1691 in 1692 if FINITE_BAG sb then BAG_CARD sb 1693 else 1``); 1694 1695val BAG_IMAGE_EMPTY = store_thm( 1696 "BAG_IMAGE_EMPTY", 1697 ``!f. BAG_IMAGE f {||} = {||}``, 1698 SRW_TAC [][BAG_IMAGE_DEF] THEN SRW_TAC [][EMPTY_BAG_alt]) 1699 before 1700 export_rewrites ["BAG_IMAGE_EMPTY"]; 1701 1702val BAG_IMAGE_FINITE_INSERT = store_thm( 1703 "BAG_IMAGE_FINITE_INSERT", 1704 ``!b f e. FINITE_BAG b ==> 1705 (BAG_IMAGE f (BAG_INSERT e b) = BAG_INSERT (f e) (BAG_IMAGE f b))``, 1706 SRW_TAC [][BAG_IMAGE_DEF] THEN 1707 SRW_TAC [][FUN_EQ_THM] THEN 1708 REPEAT GEN_TAC THEN 1709 Cases_on `f e = e'` THENL [ 1710 SRW_TAC [][BAG_CARD_THM] THEN SRW_TAC [][BAG_INSERT], 1711 SRW_TAC [][] THEN SRW_TAC [][BAG_INSERT] 1712 ]) 1713 before 1714 export_rewrites ["BAG_IMAGE_FINITE_INSERT"]; 1715 1716val BAG_IMAGE_FINITE_UNION = store_thm ( 1717 "BAG_IMAGE_FINITE_UNION", 1718 ``!b1 b2 f. (FINITE_BAG b1 /\ FINITE_BAG b2) 1719 ==> (BAG_IMAGE f (BAG_UNION b1 b2) 1720 = (BAG_UNION (BAG_IMAGE f b1) (BAG_IMAGE f b2)))``, 1721 REPEAT STRIP_TAC THEN 1722 Q.PAT_X_ASSUM `FINITE_BAG b1` MP_TAC THEN 1723 Q.SPEC_TAC (`b1`, `b1`) THEN 1724 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1725 ASM_SIMP_TAC std_ss [BAG_UNION_INSERT, BAG_UNION_EMPTY, BAG_IMAGE_EMPTY, 1726 BAG_IMAGE_FINITE_INSERT, FINITE_BAG_UNION]) before 1727 export_rewrites ["BAG_IMAGE_FINITE_UNION"]; 1728 1729val BAG_IMAGE_FINITE = store_thm( 1730 "BAG_IMAGE_FINITE", 1731 ``!b. FINITE_BAG b ==> FINITE_BAG (BAG_IMAGE f b)``, 1732 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][]) 1733 before 1734 export_rewrites ["BAG_IMAGE_FINITE"]; 1735 1736val BAG_IMAGE_COMPOSE = store_thm ( 1737 "BAG_IMAGE_COMPOSE", 1738 ``!f g b. FINITE_BAG b ==> 1739 ((BAG_IMAGE (f o g) b = BAG_IMAGE f (BAG_IMAGE g b)))``, 1740 GEN_TAC THEN GEN_TAC THEN 1741 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 1742 SIMP_TAC std_ss [BAG_IMAGE_EMPTY, BAG_IMAGE_FINITE_INSERT, 1743 BAG_IMAGE_FINITE]); 1744 1745val BAG_IMAGE_FINITE_I = store_thm( 1746 "BAG_IMAGE_FINITE_I", 1747 ``!b. FINITE_BAG b ==> (BAG_IMAGE I b = b)``, 1748 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][]) 1749 before 1750 export_rewrites ["BAG_IMAGE_FINITE_I"]; 1751 1752Theorem BAG_IN_FINITE_BAG_IMAGE[simp]: 1753 FINITE_BAG b ==> 1754 (BAG_IN x (BAG_IMAGE f b) = ?y. (f y = x) /\ BAG_IN y b) 1755Proof 1756 SRW_TAC [][BAG_IMAGE_DEF] THEN EQ_TAC THEN STRIP_TAC THENL [ 1757 FULL_SIMP_TAC (srw_ss()) [BAG_IN, BAG_INN] THEN 1758 Q.ABBREV_TAC `bf = BAG_FILTER (\e0. f e0 = x) b` THEN 1759 `FINITE_BAG bf` by (Q.UNABBREV_TAC `bf` THEN SRW_TAC [][]) THEN 1760 `0 < BAG_CARD bf` by SRW_TAC [numSimps.ARITH_ss][] THEN 1761 `?m. BAG_CARD bf = SUC m` 1762 by PROVE_TAC [arithmeticTheory.num_CASES, 1763 arithmeticTheory.NOT_ZERO_LT_ZERO] THEN 1764 `?e bf0. (bf = BAG_INSERT e bf0)` by PROVE_TAC [BCARD_SUC] THEN 1765 `BAG_IN e bf` by simp[] THEN 1766 `BAG_IN e (BAG_FILTER (\e0. f e0 = x) b)` by PROVE_TAC [] THEN 1767 POP_ASSUM (STRIP_ASSUME_TAC o SIMP_RULE bool_ss [BAG_IN_BAG_FILTER]) THEN 1768 PROVE_TAC [BAG_IN, BAG_INN], 1769 `?b0. BAG_DELETE b y b0` by PROVE_TAC [BAG_IN_BAG_DELETE] THEN 1770 `b = BAG_INSERT y b0` by PROVE_TAC [BAG_DELETE] THEN 1771 SIMP_TAC (srw_ss()) [BAG_IN, BAG_INN] THEN SRW_TAC [][] THEN 1772 FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) [BAG_CARD_THM] 1773 ] 1774QED 1775 1776val BAG_IMAGE_EQ_EMPTY = store_thm( 1777 "BAG_IMAGE_EQ_EMPTY", 1778 ``FINITE_BAG b ==> ((BAG_IMAGE f b = {||}) <=> (b = {||}))``, 1779 qid_spec_tac `b` >> ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >> 1780 simp[]); 1781val _ = export_rewrites ["BAG_IMAGE_EQ_EMPTY"] 1782 1783(*--------------------------------------------------------------------------- 1784 CHOICE and REST for bags. 1785 ---------------------------------------------------------------------------*) 1786 1787val BAG_CHOICE_DEF = new_specification 1788 ("BAG_CHOICE_DEF",["BAG_CHOICE"], 1789 Q.prove(`?ch:('a -> num) -> 'a. !b. ~(b = {||}) ==> BAG_IN (ch b) b`, 1790 PROVE_TAC [MEMBER_NOT_EMPTY])); 1791 1792 1793(* ===================================================================== *) 1794(* The REST of a bag after removing a chosen element. *) 1795(* ===================================================================== *) 1796 1797val BAG_REST_DEF = Q.new_definition 1798 ("BAG_REST_DEF", 1799 `BAG_REST b = BAG_DIFF b (EL_BAG (BAG_CHOICE b))`); 1800 1801 1802val BAG_INSERT_CHOICE_REST = Q.store_thm 1803("BAG_INSERT_CHOICE_REST", 1804 `!b:'a bag. ~(b = {||}) ==> (b = BAG_INSERT (BAG_CHOICE b) (BAG_REST b))`, 1805 REPEAT STRIP_TAC 1806 THEN IMP_RES_THEN MP_TAC BAG_CHOICE_DEF 1807 THEN NORM_TAC arith_ss 1808 [BAG_INSERT,BAG_REST_DEF,BAG_DIFF,EL_BAG,BAG_IN,BAG_INN, 1809 EMPTY_BAG,combinTheory.K_DEF,FUN_EQ_THM]); 1810 1811val BAG_CHOICE_SING = Q.store_thm 1812("BAG_CHOICE_SING", 1813 `BAG_CHOICE {|x|} = x`, 1814 Q.SPEC_THEN `{|x|}` MP_TAC BAG_CHOICE_DEF THEN SRW_TAC [][]) 1815before export_rewrites ["BAG_CHOICE_SING"]; 1816 1817val BAG_REST_SING = Q.store_thm 1818("BAG_REST_SING", 1819 `BAG_REST {|x|} = {||}`, 1820 SRW_TAC [][BAG_REST_DEF,EL_BAG]) 1821before export_rewrites ["BAG_REST_SING"]; 1822 1823val SUB_BAG_REST = Q.store_thm 1824("SUB_BAG_REST", 1825 `!b:'a bag. SUB_BAG (BAG_REST b) b`, 1826 NORM_TAC arith_ss [BAG_REST_DEF,SUB_BAG,BAG_INN,BAG_DIFF,EL_BAG,BAG_INSERT, 1827 arithmeticTheory.GREATER_EQ]); 1828 1829val PSUB_BAG_REST = Q.store_thm 1830("PSUB_BAG_REST", 1831 `!b:'a bag. ~(b = {||}) ==> PSUB_BAG (BAG_REST b) b`, 1832 REPEAT STRIP_TAC 1833 THEN IMP_RES_THEN MP_TAC BAG_CHOICE_DEF 1834 THEN NORM_TAC arith_ss [BAG_REST_DEF,PSUB_BAG, SUB_BAG,BAG_IN, BAG_INN, 1835 BAG_DIFF,EL_BAG,BAG_INSERT,EMPTY_BAG,combinTheory.K_DEF,FUN_EQ_THM] 1836 THENL [ALL_TAC, Q.EXISTS_TAC `BAG_CHOICE b`] 1837 THEN RW_TAC arith_ss []); 1838 1839 1840 1841val BAG_UNION_STABLE = Q.prove 1842(`!b1 b2. (b1 = BAG_UNION b1 b2) = (b2 = {||})`, 1843 RW_TAC bool_ss [BAG_UNION,EMPTY_BAG_alt,FUN_EQ_THM] THEN 1844 EQ_TAC THEN DISCH_THEN (fn th => GEN_TAC THEN MP_TAC(SPEC_ALL th)) THEN 1845 RW_TAC arith_ss []); 1846 1847val SUB_BAG_UNION_MONO_0 = prove( 1848 ``!x y. SUB_BAG x (BAG_UNION x y)``, 1849 RW_TAC arith_ss [SUB_BAG,BAG_UNION,BAG_INN]); 1850val SUB_BAG_UNION_MONO = save_thm( 1851 "SUB_BAG_UNION_MONO", 1852 CONJ SUB_BAG_UNION_MONO_0 1853 (ONCE_REWRITE_RULE [COMM_BAG_UNION] SUB_BAG_UNION_MONO_0)) 1854val _ = export_rewrites ["SUB_BAG_UNION_MONO"] 1855 1856val PSUB_BAG_CARD = Q.store_thm 1857("PSUB_BAG_CARD", 1858`!b1 b2:'a bag. FINITE_BAG b2 /\ PSUB_BAG b1 b2 ==> BAG_CARD b1 < BAG_CARD b2`, 1859RW_TAC bool_ss [PSUB_BAG] 1860 THEN `?d. b2 = BAG_UNION b1 d` by PROVE_TAC [SUB_BAG_DIFF_EQ] 1861 THEN RW_TAC bool_ss [] 1862 THEN `~(d = {||})` by PROVE_TAC [BAG_UNION_STABLE] 1863 THEN STRIP_ASSUME_TAC (Q.SPEC`d` BAG_cases) 1864 THEN RW_TAC bool_ss [BAG_UNION_INSERT] 1865 THEN POP_ASSUM (K ALL_TAC) 1866 THEN `FINITE_BAG (BAG_UNION b1 b0)` 1867 by PROVE_TAC[FINITE_BAG_UNION, BAG_UNION_INSERT, FINITE_BAG_THM] 1868 THEN PROVE_TAC [BAG_CARD_THM, ARITH `x < y + 1n <=> x <= y`, 1869 SUB_BAG_CARD, SUB_BAG_UNION_MONO]); 1870 1871val EL_BAG_BAG_INSERT = store_thm( 1872 "EL_BAG_BAG_INSERT[simp]", 1873 ``{|x|} = BAG_INSERT y b <=> x = y /\ b = {||}``, 1874 simp[EQ_IMP_THM] >> 1875 simp[BAG_EXTENSION, BAG_INN, BAG_INSERT, EMPTY_BAG] >> 1876 strip_tac >> 1877 `x = y` 1878 by (spose_not_then assume_tac >> 1879 first_x_assum (qspecl_then [`1`, `y`] mp_tac) >> 1880 simp[]) >> rw[] >> 1881 simp[EQ_IMP_THM] >> spose_not_then strip_assume_tac >> Cases_on `e = x` 1882 >- (rw[] >> first_x_assum (qspecl_then [`n+1`, `e`] mp_tac) >> 1883 simp[]) >> 1884 first_x_assum (qspecl_then [`n`, `e`] mp_tac) >> simp[]); 1885 1886val EL_BAG_SUB_BAG = store_thm( 1887 "EL_BAG_SUB_BAG[simp]", 1888 ``{| x |} <= b <=> BAG_IN x b``, 1889 simp_tac (srw_ss() ++ COND_elim_ss ++ DNF_ss) 1890 [SUB_BAG, BAG_INN, BAG_IN, BAG_INSERT, EMPTY_BAG, EQ_IMP_THM, 1891 arithmeticTheory.GREATER_EQ] >> simp[]); 1892 1893 1894 1895(* ---------------------------------------------------------------------- 1896 A "fold"-like operation for bags, ITBAG, by analogy with the set 1897 theory's ITSET. 1898 ---------------------------------------------------------------------- *) 1899 1900val ITBAG_defn = Defn.Hol_defn "ITBAG" 1901 `ITBAG (b: 'a bag) (acc: 'b) = 1902 if FINITE_BAG b then 1903 if b = {||} then acc 1904 else ITBAG (BAG_REST b) (f (BAG_CHOICE b) acc) 1905 else ARB`; 1906 1907(* Termination of above *) 1908val (ITBAG_eqn0, ITBAG_IND) = 1909 Defn.tprove(ITBAG_defn, 1910 TotalDefn.WF_REL_TAC `measure (BAG_CARD o FST)` THEN 1911 PROVE_TAC [PSUB_BAG_CARD, PSUB_BAG_REST]); 1912 1913(* derive the desired recursion equation: 1914 FINITE_BAG b ==> 1915 (ITBAG f b a = if b = {||} then a 1916 else ITBAG f (BAG_REST b) (f (BAG_CHOICE b) a)) 1917*) 1918val ITBAG_THM = 1919 GENL [``b: 'a -> num``, ``f:'a -> 'b -> 'b``, ``acc:'b``] 1920 (DISCH_ALL (ASM_REWRITE_RULE [Q.ASSUME `FINITE_BAG b`] ITBAG_eqn0)) 1921 1922val _ = save_thm("ITBAG_IND", ITBAG_IND); 1923val _ = save_thm("ITBAG_THM", ITBAG_THM); 1924 1925val ITBAG_EMPTY = save_thm( 1926 "ITBAG_EMPTY", 1927 REWRITE_RULE [] (MATCH_MP (Q.SPEC `{||}` ITBAG_THM) FINITE_EMPTY_BAG)) 1928 before 1929 export_rewrites ["ITBAG_EMPTY"]; 1930 1931val ITBAG_INSERT = save_thm( 1932 "ITBAG_INSERT", 1933 SIMP_RULE (srw_ss())[] (Q.SPEC `BAG_INSERT x b` ITBAG_THM)) 1934 1935val COMMUTING_ITBAG_INSERT = store_thm( 1936 "COMMUTING_ITBAG_INSERT", 1937 ``!f b. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==> 1938 !x a. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a)``, 1939 REPEAT GEN_TAC THEN STRIP_TAC THEN 1940 completeInduct_on `BAG_CARD b` THEN 1941 FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] THEN 1942 SRW_TAC [][ITBAG_INSERT, BAG_REST_DEF, EL_BAG] THEN 1943 Q.ABBREV_TAC `c = BAG_CHOICE (BAG_INSERT x b)` THEN 1944 `BAG_IN c (BAG_INSERT x b)` 1945 by PROVE_TAC [BAG_CHOICE_DEF, BAG_INSERT_NOT_EMPTY] THEN 1946 `(c = x) \/ BAG_IN c b` by PROVE_TAC [BAG_IN_BAG_INSERT] THENL [ 1947 SRW_TAC [][], 1948 `?b0. b = BAG_INSERT c b0` 1949 by PROVE_TAC [BAG_IN_BAG_DELETE, BAG_DELETE] THEN 1950 `BAG_DIFF (BAG_INSERT x b) {| c |} = BAG_INSERT x b0` 1951 by SRW_TAC [][BAG_INSERT_commutes] THEN 1952 ASM_REWRITE_TAC [] THEN 1953 `FINITE_BAG b0` by FULL_SIMP_TAC (srw_ss()) [] THEN 1954 `BAG_CARD b0 < BAG_CARD b` 1955 by SRW_TAC [numSimps.ARITH_ss][BAG_CARD_THM] THEN 1956 SRW_TAC [][] 1957 ]); 1958 1959val COMMUTING_ITBAG_RECURSES = store_thm( 1960 "COMMUTING_ITBAG_RECURSES", 1961 ``!f e b a. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==> 1962 (ITBAG f (BAG_INSERT e b) a = f e (ITBAG f b a))``, 1963 Q_TAC SUFF_TAC 1964 `!f. (!x y z. f x (f y z) = f y (f x z)) ==> 1965 !b. FINITE_BAG b ==> 1966 !e a. ITBAG f (BAG_INSERT e b) a = f e (ITBAG f b a)` THEN1 1967 PROVE_TAC [] THEN 1968 GEN_TAC THEN STRIP_TAC THEN 1969 ASM_SIMP_TAC (srw_ss()) [COMMUTING_ITBAG_INSERT] THEN 1970 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN CONJ_TAC THENL [ 1971 SRW_TAC [][ITBAG_EMPTY], 1972 SRW_TAC [][COMMUTING_ITBAG_INSERT] 1973 ]); 1974 1975(*---------------------------------------------------------------------------*) 1976(* Sums and products on finite bags *) 1977(*---------------------------------------------------------------------------*) 1978 1979val BAG_GEN_SUM_def = 1980 new_definition 1981 ("BAG_GEN_SUM_def", 1982 ``BAG_GEN_SUM bag (n:num) = ITBAG (+) bag n``); 1983 1984val BAG_GEN_PROD_def = 1985 new_definition 1986 ("BAG_GEN_PROD_def", 1987 ``BAG_GEN_PROD bag n = ITBAG $* bag n``); 1988 1989val BAG_GEN_SUM_EMPTY = store_thm 1990("BAG_GEN_SUM_EMPTY", 1991 ``!n. BAG_GEN_SUM {||} n = n``, 1992 RW_TAC bool_ss [BAG_GEN_SUM_def,ITBAG_EMPTY]); 1993 1994val BAG_GEN_PROD_EMPTY = store_thm 1995("BAG_GEN_PROD_EMPTY", 1996 ``!n. BAG_GEN_PROD {||} n = n``, 1997 RW_TAC bool_ss [BAG_GEN_PROD_def,ITBAG_EMPTY]); 1998 1999val BAG_GEN_SUM_TAILREC = store_thm 2000("BAG_GEN_SUM_TAILREC", 2001 ``!b. FINITE_BAG b ==> 2002 !x a. BAG_GEN_SUM (BAG_INSERT x b) a = BAG_GEN_SUM b (x + a)``, 2003 GEN_TAC THEN STRIP_TAC THEN 2004 SIMP_TAC bool_ss [BAG_GEN_SUM_def] THEN 2005 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_INSERT) THEN 2006 RW_TAC std_ss []); 2007 2008val BAG_GEN_SUM_REC = store_thm 2009("BAG_GEN_SUM_REC", 2010 ``!b. FINITE_BAG b ==> 2011 !x a. BAG_GEN_SUM (BAG_INSERT x b) a = x + BAG_GEN_SUM b a``, 2012 GEN_TAC THEN REPEAT STRIP_TAC THEN 2013 SIMP_TAC bool_ss [BAG_GEN_SUM_def] THEN 2014 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_RECURSES) THEN 2015 RW_TAC std_ss []); 2016 2017val BAG_GEN_PROD_TAILREC = store_thm 2018("BAG_GEN_PROD_TAILREC", 2019 ``!b. FINITE_BAG b ==> 2020 !x a. BAG_GEN_PROD (BAG_INSERT x b) a = BAG_GEN_PROD b (x * a)``, 2021 GEN_TAC THEN STRIP_TAC THEN 2022 SIMP_TAC bool_ss [BAG_GEN_PROD_def] THEN 2023 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_INSERT) THEN 2024 RW_TAC std_ss []); 2025 2026val BAG_GEN_PROD_REC = store_thm 2027("BAG_GEN_PROD_REC", 2028 ``!b. FINITE_BAG b ==> 2029 !x a. BAG_GEN_PROD (BAG_INSERT x b) a = x * BAG_GEN_PROD b a``, 2030 GEN_TAC THEN REPEAT STRIP_TAC THEN 2031 SIMP_TAC bool_ss [BAG_GEN_PROD_def] THEN 2032 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_RECURSES) THEN 2033 RW_TAC std_ss []); 2034 2035val BAG_GEN_PROD_EQ_1 = Q.store_thm 2036("BAG_GEN_PROD_EQ_1", 2037 `!b. FINITE_BAG b ==> !e. (BAG_GEN_PROD b e = 1) ==> (e=1)`, 2038 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN REPEAT STRIP_TAC THENL 2039 [METIS_TAC [BAG_GEN_PROD_EMPTY], 2040 Q.PAT_X_ASSUM `p=q` MP_TAC THEN 2041 RW_TAC std_ss [Once BAG_GEN_PROD_TAILREC] THEN 2042 RES_TAC THEN FULL_SIMP_TAC std_ss []]); 2043 2044val BAG_GEN_PROD_ALL_ONES = Q.store_thm 2045("BAG_GEN_PROD_ALL_ONES", 2046 `!b. FINITE_BAG b ==> (BAG_GEN_PROD b 1 = 1) ==> !x. BAG_IN x b ==> (x=1)`, 2047 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN REPEAT STRIP_TAC THENL 2048 [METIS_TAC [NOT_IN_EMPTY_BAG], 2049 Q.PAT_X_ASSUM `p=q` MP_TAC THEN 2050 RW_TAC std_ss [BAG_GEN_PROD_TAILREC] THEN 2051 `e=1` by METIS_TAC [BAG_GEN_PROD_EQ_1] THEN RW_TAC std_ss [] THEN 2052 `!x. BAG_IN x b ==> (x = 1)` by METIS_TAC[] THEN 2053 METIS_TAC [BAG_IN_BAG_INSERT]]); 2054 2055val BAG_GEN_PROD_POSITIVE = Q.store_thm 2056("BAG_GEN_PROD_POSITIVE", 2057 `!b. FINITE_BAG b ==> (!x. BAG_IN x b ==> 0 < x) ==> 0 < BAG_GEN_PROD b 1`, 2058 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN REPEAT STRIP_TAC THENL 2059 [METIS_TAC [BAG_GEN_PROD_EMPTY,ARITH `0<1`], 2060 RW_TAC std_ss [BAG_GEN_PROD_REC] THEN 2061 `0 < e` by METIS_TAC [BAG_IN_BAG_INSERT] THEN 2062 `0 < BAG_GEN_PROD b 1` by METIS_TAC [BAG_IN_BAG_INSERT] THEN 2063 METIS_TAC [arithmeticTheory.LESS_MULT2]]); 2064 2065val BAG_EVERY = 2066 new_definition 2067 ("BAG_EVERY", 2068 ``BAG_EVERY P b = !e. BAG_IN e b ==> P e``); 2069 2070val BAG_EVERY_THM = store_thm ("BAG_EVERY_THM", 2071``(!P. BAG_EVERY P EMPTY_BAG) /\ 2072 (!P e b. BAG_EVERY P (BAG_INSERT e b) <=> P e /\ BAG_EVERY P b)``, 2073SIMP_TAC (srw_ss()) [BAG_EVERY] THEN METIS_TAC []); 2074val _ = export_rewrites ["BAG_EVERY_THM"] 2075 2076val BAG_EVERY_UNION = Q.store_thm( 2077"BAG_EVERY_UNION", 2078`BAG_EVERY P (b1 + b2) <=> BAG_EVERY P b1 /\ BAG_EVERY P b2`, 2079SRW_TAC [][BAG_EVERY] THEN METIS_TAC []); 2080val _ = export_rewrites["BAG_EVERY_UNION"]; 2081 2082val BAG_EVERY_MERGE = Q.store_thm( 2083"BAG_EVERY_MERGE", 2084`BAG_EVERY P (BAG_MERGE b1 b2) <=> BAG_EVERY P b1 /\ BAG_EVERY P b2`, 2085SRW_TAC [][BAG_EVERY, DISJ_IMP_THM, FORALL_AND_THM]); 2086val _ = export_rewrites ["BAG_EVERY_MERGE"] 2087 2088val BAG_EVERY_SET = Q.store_thm( 2089"BAG_EVERY_SET", 2090`BAG_EVERY P b <=> SET_OF_BAG b SUBSET {x | P x}`, 2091SRW_TAC [][BAG_EVERY, SET_OF_BAG, SUBSET_DEF]); 2092 2093val BAG_FILTER_EQ_EMPTY = Q.store_thm( 2094 "BAG_FILTER_EQ_EMPTY", 2095 `(BAG_FILTER P b = {||}) <=> BAG_EVERY ($~ o P) b`, 2096 SRW_TAC [][BAG_EXTENSION,BAG_INN_BAG_FILTER,BAG_EVERY,BAG_IN,EQ_IMP_THM] THEN1 2097 (FIRST_X_ASSUM (Q.SPECL_THEN [`1`,`e`] MP_TAC) 2098 THEN SRW_TAC [][] ) THEN 2099 FIRST_X_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN 2100 SRW_TAC [][] THEN 2101 Cases_on `n < 1` THEN1 DECIDE_TAC THEN 2102 (BAG_INN_LESS |> Q.SPECL [`b`,`e`,`n`,`1`] |> CONTRAPOS |> IMP_RES_TAC) THEN 2103 FULL_SIMP_TAC (srw_ss()) [] THEN 2104 `n = 1` by DECIDE_TAC THEN 2105 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []); 2106 2107Theorem SET_OF_BAG_IMAGE[simp]: 2108 SET_OF_BAG (BAG_IMAGE f b) = IMAGE f (SET_OF_BAG b) 2109Proof 2110 SRW_TAC[][EXTENSION, BAG_IMAGE_DEF, BAG_IN, BAG_INN] >> 2111 Q.ABBREV_TAC `bf = BAG_FILTER (\e0. f e0 = x) b` >> 2112 qspec_then ���bf��� mp_tac BAG_cases THEN 2113 SRW_TAC [][] THEN SRW_TAC [][] THENL [ 2114 FULL_SIMP_TAC (srw_ss()) [BAG_FILTER_EQ_EMPTY,BAG_EVERY,BAG_IN,BAG_INN] THEN 2115 PROVE_TAC [], 2116 fs[BAG_CARD_THM], 2117 FULL_SIMP_TAC (srw_ss()) [], 2118 ALL_TAC 2119 ] THEN 2120 `~BAG_EVERY ($~ o (\e0. f e0 = x)) b` 2121 by PROVE_TAC [BAG_FILTER_EQ_EMPTY,BAG_INSERT_NOT_EMPTY] THEN 2122 FULL_SIMP_TAC (srw_ss()) [BAG_EVERY,BAG_IN,BAG_INN] THEN 2123 PROVE_TAC [] 2124QED 2125 2126val BAG_IMAGE_FINITE_RESTRICTED_I = store_thm( 2127 "BAG_IMAGE_FINITE_RESTRICTED_I", 2128 ``!b. FINITE_BAG b /\ BAG_EVERY (\e. f e = e) b ==> (BAG_IMAGE f b = b)``, 2129 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN 2130 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][]); 2131 2132val BAG_ALL_DISTINCT = new_definition ("BAG_ALL_DISTINCT", 2133 ``BAG_ALL_DISTINCT b = (!e. b e <= 1:num)``); 2134 2135val BAG_ALL_DISTINCT_THM = store_thm ("BAG_ALL_DISTINCT_THM", 2136 ``BAG_ALL_DISTINCT EMPTY_BAG /\ 2137 !e b. BAG_ALL_DISTINCT (BAG_INSERT e b) <=> 2138 ~BAG_IN e b /\ BAG_ALL_DISTINCT b``, 2139 `(!x. ((x + 1 <= 1) = (x = 0)) /\ (~(x >= 1) = (x = 0))) /\ 0n <= 1` 2140 by bossLib.DECIDE_TAC THEN 2141 SRW_TAC [COND_elim_ss, DNF_ss] 2142 [BAG_ALL_DISTINCT, EMPTY_BAG, BAG_INSERT, BAG_IN, BAG_INN, 2143 EQ_IMP_THM] THEN METIS_TAC []); 2144val _ = export_rewrites ["BAG_ALL_DISTINCT_THM"] 2145 2146val forall_eq_thm = prove (``(!s:'a. (P s = Q s)) ==> ((!s. P s) = (!s. Q s))``, 2147 STRIP_TAC THEN ASM_REWRITE_TAC[]); 2148 2149val BAG_ALL_DISTINCT_BAG_MERGE = store_thm ( 2150 "BAG_ALL_DISTINCT_BAG_MERGE", 2151 ``!b1 b2. BAG_ALL_DISTINCT (BAG_MERGE b1 b2) = 2152 (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2)``, 2153 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_MERGE, 2154 GSYM FORALL_AND_THM, COND_RAND, COND_RATOR, 2155 COND_EXPAND_IMP] THEN 2156 REPEAT STRIP_TAC THEN 2157 HO_MATCH_MP_TAC forall_eq_thm THEN 2158 GEN_TAC THEN bossLib.DECIDE_TAC); 2159 2160 2161val BAG_ALL_DISTINCT_BAG_UNION = store_thm ( 2162 "BAG_ALL_DISTINCT_BAG_UNION", 2163 ``!b1 b2. 2164 BAG_ALL_DISTINCT (BAG_UNION b1 b2) = 2165 (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2 /\ 2166 BAG_DISJOINT b1 b2)``, 2167 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_UNION, 2168 BAG_DISJOINT, DISJOINT_DEF, EXTENSION, 2169 NOT_IN_EMPTY, IN_INTER, 2170 IN_SET_OF_BAG, BAG_IN, 2171 BAG_INN, GSYM FORALL_AND_THM] THEN 2172 REPEAT STRIP_TAC THEN 2173 HO_MATCH_MP_TAC forall_eq_thm THEN 2174 GEN_TAC THEN bossLib.DECIDE_TAC); 2175 2176val BAG_ALL_DISTINCT_DIFF = store_thm ( 2177 "BAG_ALL_DISTINCT_DIFF", 2178 ``!b1 b2. 2179 BAG_ALL_DISTINCT b1 ==> 2180 BAG_ALL_DISTINCT (BAG_DIFF b1 b2)``, 2181 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_DIFF] THEN 2182 REPEAT STRIP_TAC THEN 2183 `b1 e <= 1` by PROVE_TAC[] THEN 2184 bossLib.DECIDE_TAC); 2185 2186 2187val BAG_ALL_DISTINCT_DELETE = store_thm( 2188 "BAG_ALL_DISTINCT_DELETE", 2189 ``BAG_ALL_DISTINCT b = !e. e <: b ==> ~(e <: b - {|e|})``, 2190 SRW_TAC [][BAG_ALL_DISTINCT, BAG_IN, BAG_INN, BAG_DIFF, BAG_INSERT, 2191 EMPTY_BAG, EQ_IMP_THM] THEN 2192 FIRST_X_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN DECIDE_TAC); 2193 2194val BAG_ALL_DISTINCT_SET = store_thm( 2195 "BAG_ALL_DISTINCT_SET", 2196 ``BAG_ALL_DISTINCT b <=> (BAG_OF_SET (SET_OF_BAG b) = b)``, 2197 SRW_TAC [][BAG_ALL_DISTINCT, FUN_EQ_THM, SET_OF_BAG, 2198 BAG_INN, BAG_IN, BAG_INSERT, EMPTY_BAG, BAG_OF_SET] THEN 2199 EQ_TAC THEN STRIP_TAC THEN Q.X_GEN_TAC `e` THEN 2200 POP_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN DECIDE_TAC); 2201 2202val BAG_ALL_DISTINCT_BAG_OF_SET = store_thm( 2203 "BAG_ALL_DISTINCT_BAG_OF_SET", 2204 ``BAG_ALL_DISTINCT (BAG_OF_SET s)``, 2205 SRW_TAC [][BAG_ALL_DISTINCT_SET]); 2206val _ = export_rewrites ["BAG_ALL_DISTINCT_BAG_OF_SET"] 2207 2208 2209val BAG_IN_BAG_DIFF_ALL_DISTINCT = store_thm ( 2210 "BAG_IN_BAG_DIFF_ALL_DISTINCT", 2211 ``!b1 b2 e. BAG_ALL_DISTINCT b1 ==> 2212 (BAG_IN e (BAG_DIFF b1 b2) <=> BAG_IN e b1 /\ ~BAG_IN e b2)``, 2213 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_IN, BAG_INN, BAG_DIFF] THEN 2214 REPEAT STRIP_TAC THEN `b1 e <= 1` by PROVE_TAC[] THEN DECIDE_TAC); 2215 2216val SUB_BAG_ALL_DISTINCT = store_thm ( 2217 "SUB_BAG_ALL_DISTINCT", 2218 ``!b1 b2. BAG_ALL_DISTINCT b1 ==> 2219 (SUB_BAG b1 b2 = (!x. BAG_IN x b1 ==> BAG_IN x b2))``, 2220 SIMP_TAC std_ss [BAG_ALL_DISTINCT, SUB_BAG, BAG_INN, BAG_IN] THEN 2221 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 2222 PROVE_TAC[], 2223 2224 REPEAT STRIP_TAC THEN 2225 Cases_on `n = 0` THEN FULL_SIMP_TAC std_ss [] THEN 2226 Q.PAT_X_ASSUM `!e. b1 e <= 1` (ASSUME_TAC o Q.SPEC `x`) THEN 2227 `n = 1` by DECIDE_TAC THEN 2228 FULL_SIMP_TAC std_ss [] 2229 ]); 2230 2231val BAG_ALL_DISTINCT_BAG_INN = store_thm ( 2232 "BAG_ALL_DISTINCT_BAG_INN", 2233 ``!b n e. BAG_ALL_DISTINCT b ==> 2234 (BAG_INN e n b <=> n = 0 \/ n = 1 /\ BAG_IN e b)``, 2235 SIMP_TAC std_ss [BAG_INN, BAG_ALL_DISTINCT, BAG_IN] THEN 2236 REPEAT STRIP_TAC THEN 2237 Cases_on `n = 0` THEN ASM_SIMP_TAC std_ss [] THEN 2238 Cases_on `n = 1` THEN1 ASM_SIMP_TAC std_ss [] THEN 2239 `b e <= 1` by PROVE_TAC[] THEN 2240 DECIDE_TAC); 2241 2242 2243val BAG_ALL_DISTINCT_EXTENSION = store_thm ( 2244 "BAG_ALL_DISTINCT_EXTENSION", 2245 ``!b1 b2. (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2) ==> 2246 ((b1 = b2) = (!x. BAG_IN x b1 = BAG_IN x b2))``, 2247 SIMP_TAC std_ss [BAG_EXTENSION, BAG_ALL_DISTINCT_BAG_INN] THEN 2248 SIMP_TAC (std_ss++EQUIV_EXTRACT_ss) []) 2249 2250Theorem BAG_ALL_DISTINCT_SUB_BAG: 2251 !s t. s <= t /\ BAG_ALL_DISTINCT t ==> BAG_ALL_DISTINCT s 2252Proof 2253 rw[BAG_ALL_DISTINCT,SUB_BAG,BAG_INN] >> 2254 CCONTR_TAC >> `s e >= 2` by fs[] >> 2255 metis_tac[DECIDE ���y >= 2 ==> ~(y <= 1)���] 2256QED 2257 2258Theorem BAG_DISJOINT_SUB_BAG: 2259 !b1 b2 b3. b1 <= b2 /\ BAG_DISJOINT b2 b3 ==> BAG_DISJOINT b1 b3 2260Proof 2261 rw [BAG_DISJOINT_BAG_IN] \\ metis_tac [SUB_BAG, BAG_IN] 2262QED 2263 2264Theorem BAG_DISJOINT_SYM: 2265 !b1 b2. BAG_DISJOINT b1 b2 <=> BAG_DISJOINT b2 b1 2266Proof simp [BAG_DISJOINT, DISJOINT_SYM] 2267QED 2268 2269Theorem MONOID_BAG_UNION_EMPTY_BAG: MONOID $+ {||} 2270Proof simp [MONOID_DEF, RIGHT_ID_DEF, LEFT_ID_DEF, ASSOC_DEF, ASSOC_BAG_UNION] 2271QED 2272 2273Theorem BAG_DISJOINT_FOLDR_BAG_UNION: 2274 !ls b0 b1. 2275 BAG_DISJOINT b1 (FOLDR BAG_UNION b0 ls) <=> EVERY (BAG_DISJOINT b1) (b0::ls) 2276Proof Induct \\ rw[] \\ metis_tac[] 2277QED 2278 2279val NOT_BAG_IN = Q.store_thm 2280("NOT_BAG_IN", 2281 `!b x. (b x = 0) = ~BAG_IN x b`, 2282 RW_TAC arith_ss [EQ_IMP_THM] THENL 2283 [STRIP_TAC THEN 2284 `?b'. b = BAG_INSERT x b'` by METIS_TAC[BAG_DECOMPOSE] THEN 2285 RW_TAC arith_ss [] THEN FULL_SIMP_TAC arith_ss [BAG_INSERT], 2286 FULL_SIMP_TAC arith_ss [BAG_IN,BAG_INN]]); 2287 2288val BAG_UNION_EQ_LEFT = Q.store_thm 2289("BAG_UNION_EQ_LEFT", 2290 `!b c d. (BAG_UNION b c = BAG_UNION b d) ==> (c=d)`, 2291 RW_TAC arith_ss [BAG_UNION,FUN_EQ_THM]); 2292 2293val lem = Q.prove 2294(`!b. FINITE_BAG b ==> !x a. BAG_IN x b ==> divides x (BAG_GEN_PROD b a)`, 2295 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 2296 RW_TAC arith_ss [NOT_IN_EMPTY_BAG,BAG_IN_BAG_INSERT] THENL 2297 [RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN 2298 METIS_TAC[DIVIDES_REFL,DIVIDES_MULT], 2299 `divides x (BAG_GEN_PROD b a)` by METIS_TAC[] THEN 2300 RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN 2301 METIS_TAC[DIVIDES_MULT,MULT_SYM]]); 2302 2303val BAG_IN_DIVIDES = Q.store_thm 2304("BAG_IN_DIVIDES", 2305 `!b x a. FINITE_BAG b /\ BAG_IN x b ==> divides x (BAG_GEN_PROD b a)`, 2306 METIS_TAC [lem]); 2307 2308val BAG_GEN_PROD_UNION_LEM = Q.store_thm 2309("BAG_GEN_PROD_UNION_LEM", 2310 `!b1. FINITE_BAG b1 ==> 2311 !b2 a b. FINITE_BAG b2 ==> 2312 (BAG_GEN_PROD (BAG_UNION b1 b2) (a * b) = 2313 BAG_GEN_PROD b1 a * BAG_GEN_PROD b2 b)`, 2314 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN CONJ_TAC THENL 2315 [RW_TAC arith_ss [BAG_GEN_PROD_EMPTY,BAG_UNION_EMPTY] THEN 2316 Q.ID_SPEC_TAC `b` THEN Q.ID_SPEC_TAC `a` THEN 2317 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `b2` THEN 2318 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN 2319 RW_TAC arith_ss [BAG_GEN_PROD_EMPTY,BAG_UNION_EMPTY] THEN 2320 RW_TAC arith_ss [BAG_GEN_PROD_REC], 2321 REPEAT STRIP_TAC THEN 2322 RW_TAC arith_ss [BAG_GEN_PROD_REC,BAG_UNION_INSERT] THEN 2323 `FINITE_BAG (BAG_UNION b1 b2)` by METIS_TAC [FINITE_BAG_UNION] THEN 2324 RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN 2325 METIS_TAC [MULT_ASSOC]]); 2326 2327val BAG_GEN_PROD_UNION = Q.store_thm 2328("BAG_GEN_PROD_UNION", 2329 `!b1 b2. FINITE_BAG b1 /\ FINITE_BAG b2 ==> 2330 (BAG_GEN_PROD (BAG_UNION b1 b2) 1 = 2331 BAG_GEN_PROD b1 1 * BAG_GEN_PROD b2 1)`, 2332 METIS_TAC [BAG_GEN_PROD_UNION_LEM, ARITH `1 * 1 = 1`]); 2333 2334(* BIG_BAG_UNION: the union of all bags in a finite set *) 2335 2336val BIG_BAG_UNION_def = Define` 2337 BIG_BAG_UNION sob = \x. SIGMA (\b. b x) sob`; 2338 2339val BIG_BAG_UNION_EMPTY = Q.store_thm( 2340"BIG_BAG_UNION_EMPTY", 2341`BIG_BAG_UNION {} = {||}`, 2342SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,EMPTY_BAG,FUN_EQ_THM]); 2343val _ = export_rewrites ["BIG_BAG_UNION_EMPTY"]; 2344 2345val BIG_BAG_UNION_INSERT = Q.store_thm( 2346"BIG_BAG_UNION_INSERT", 2347`FINITE sob ==> 2348 (BIG_BAG_UNION (b INSERT sob) = b + BIG_BAG_UNION (sob DELETE b))`, 2349SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,BAG_UNION,FUN_EQ_THM]); 2350 2351val BIG_BAG_UNION_DELETE = Q.store_thm( 2352"BIG_BAG_UNION_DELETE", 2353`FINITE sob ==> 2354(BIG_BAG_UNION (sob DELETE b) 2355 = if b IN sob then BAG_DIFF (BIG_BAG_UNION sob) b else BIG_BAG_UNION sob)`, 2356SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM, 2357 SUM_IMAGE_DELETE,BAG_UNION,BAG_DIFF,FUN_EQ_THM] THEN 2358FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT]); 2359 2360val BIG_BAG_UNION_ITSET_BAG_UNION = Q.store_thm( 2361"BIG_BAG_UNION_ITSET_BAG_UNION", 2362`!sob. FINITE sob ==> (BIG_BAG_UNION sob = ITSET BAG_UNION sob {||})`, 2363HO_MATCH_MP_TAC FINITE_INDUCT THEN 2364SRW_TAC [][ITSET_EMPTY] THEN 2365(COMMUTING_ITSET_RECURSES 2366 |> Q.ISPECL_THEN [`BAG_UNION`,`e`,`sob`,`{||}`] MP_TAC) THEN 2367FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT] THEN 2368SRW_TAC [][BIG_BAG_UNION_INSERT] THEN 2369FIRST_X_ASSUM (MATCH_MP_TAC o GSYM) THEN 2370METIS_TAC [COMM_BAG_UNION,ASSOC_BAG_UNION]); 2371 2372val FINITE_BIG_BAG_UNION = Q.store_thm( 2373"FINITE_BIG_BAG_UNION", 2374`!sob. FINITE sob /\ (!b. b IN sob ==> FINITE_BAG b) ==> FINITE_BAG 2375(BIG_BAG_UNION sob)`, 2376SIMP_TAC bool_ss [GSYM AND_IMP_INTRO] THEN 2377 HO_MATCH_MP_TAC FINITE_INDUCT THEN 2378 SRW_TAC [][BIG_BAG_UNION_INSERT] THEN 2379 FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT]); 2380 2381val BAG_IN_BIG_BAG_UNION = Q.store_thm( 2382"BAG_IN_BIG_BAG_UNION", 2383`FINITE P ==> (e <: BIG_BAG_UNION P <=> ?b. e <: b /\ b IN P)`, 2384SRW_TAC [][BIG_BAG_UNION_def,BAG_IN,BAG_INN,EQ_IMP_THM] THEN1 ( 2385 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2386 (SUM_IMAGE_upper_bound 2387 |> Q.GEN `f` 2388 |> Q.ISPEC_THEN `\b:'a bag. b e` (Q.ISPEC_THEN `P` MP_TAC)) THEN 2389 SRW_TAC [][] THEN 2390 Q.EXISTS_TAC `0` THEN 2391 SRW_TAC [ARITH_ss][] THEN 2392 FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN 2393 SRW_TAC [ARITH_ss][] ) THEN 2394FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.GREATER_EQ] THEN 2395`1 <= SIGMA (\b. b e) {b}` by SRW_TAC [][SUM_IMAGE_THM] THEN 2396MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS THEN 2397Q.EXISTS_TAC `SIGMA (\b.b e) {b}` THEN 2398SRW_TAC [][] THEN 2399MATCH_MP_TAC SUM_IMAGE_SUBSET_LE THEN 2400SRW_TAC [][]); 2401val _ = export_rewrites ["BAG_IN_BIG_BAG_UNION"]; 2402 2403val BIG_BAG_UNION_EQ_EMPTY_BAG = Q.store_thm( 2404"BIG_BAG_UNION_EQ_EMPTY_BAG", 2405`!sob. FINITE sob ==> 2406((BIG_BAG_UNION sob = {||}) <=> (!b. b IN sob ==> (b = {||})))`, 2407HO_MATCH_MP_TAC FINITE_INDUCT THEN 2408SRW_TAC [][BIG_BAG_UNION_INSERT] THEN 2409FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT] THEN 2410PROVE_TAC []); 2411 2412val BIG_BAG_UNION_UNION = Q.store_thm( 2413"BIG_BAG_UNION_UNION", 2414`FINITE s1 /\ FINITE s2 ==> 2415(BIG_BAG_UNION (s1 UNION s2) 2416 = BIG_BAG_UNION s1 + BIG_BAG_UNION s2 - BIG_BAG_UNION (s1 INTER s2))`, 2417SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_UNION,FUN_EQ_THM,BAG_UNION,BAG_DIFF]); 2418 2419Theorem BIG_BAG_UNION_EQ_ELEMENT: 2420 FINITE sob /\ b IN sob ==> 2421 (BIG_BAG_UNION sob = b <=> !b'. b' IN sob ==> b' = b \/ b' = {||}) 2422Proof 2423 Cases_on ���sob��� >> 2424 simp[BIG_BAG_UNION_def, SUM_IMAGE_THM, DELETE_NON_ELEMENT_RWT, 2425 DISJ_IMP_THM, FORALL_AND_THM] >> rw[] 2426 >- (simp[SimpLHS, FUN_EQ_THM, SUM_IMAGE_ZERO] >> 2427 rename [���b NOTIN sob���] >> 2428 ���!x. x IN sob ==> x <> b��� by metis_tac[] >> simp[] >> 2429 simp[FUN_EQ_THM, EMPTY_BAG] >> metis_tac[]) >> 2430 rename [���b NOTIN s���, ���a IN s���, ���_ = a���] >> 2431 ���a <> b��� by metis_tac[] >> simp[] >> 2432 ���?s0. s = a INSERT s0 /\ a NOTIN s0��� by metis_tac[DECOMPOSITION] >> 2433 fs[SUM_IMAGE_THM, DELETE_NON_ELEMENT_RWT] >> 2434 simp[SimpLHS, FUN_EQ_THM] >> simp[DISJ_IMP_THM, SUM_IMAGE_ZERO] >> 2435 ���!c. c IN s0 ==> c <> a��� by metis_tac[] >> simp[] >> 2436 simp[EMPTY_BAG, FUN_EQ_THM] >> metis_tac[] 2437QED 2438 2439(* ---------------------------------------------------------------------- 2440 Multiset ordering 2441 2442 Taken from Isabelle development of same. 2443 ---------------------------------------------------------------------- *) 2444 2445(* The 1 is from the fact that is one step of the relation, other uses 2446 might want to take the transitive closure of this (overloaded below). *) 2447val mlt1_def = new_definition( 2448 "mlt1_def", 2449 ``mlt1 r b1 b2 <=> FINITE_BAG b1 /\ FINITE_BAG b2 /\ 2450 ?e rep res. (b1 = rep + res) /\ (b2 = res + {|e|}) /\ 2451 !e'. BAG_IN e' rep ==> r e' e``); 2452 2453val _ = overload_on ("mlt", ``\R. TC (mlt1 R)``); 2454 2455val BAG_NOT_LESS_EMPTY = store_thm( 2456 "BAG_NOT_LESS_EMPTY", 2457 ``~mlt1 r b {||}``, 2458 SRW_TAC [][mlt1_def]); 2459val _ = export_rewrites ["BAG_NOT_LESS_EMPTY"] 2460 2461val NOT_mlt_EMPTY = store_thm( 2462 "NOT_mlt_EMPTY", 2463 ``~mlt R b {||}``, 2464 simp[Once relationTheory.TC_CASES2]) 2465val _ = export_rewrites ["NOT_mlt_EMPTY"] 2466 2467val BAG_LESS_ADD = store_thm( 2468 "BAG_LESS_ADD", 2469 ``mlt1 r N (M0 + {|a|}) ==> 2470 (?M. mlt1 r M M0 /\ (N = M + {|a|})) \/ 2471 (?KK. (!b. BAG_IN b KK ==> r b a) /\ (N = M0 + KK))``, 2472 SRW_TAC [][mlt1_def] THEN 2473 FULL_SIMP_TAC (srw_ss()) [Once add_eq_conv_ex] THENL [ 2474 DISJ2_TAC THEN Q.EXISTS_TAC `rep` THEN 2475 METIS_TAC [COMM_BAG_UNION], 2476 2477 SRW_TAC [DNF_ss][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2478 METIS_TAC [ASSOC_BAG_UNION] 2479 ]); 2480 2481val bag_insert_union = prove( 2482 ``BAG_INSERT e b = b + {|e|}``, 2483 SRW_TAC [][FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG] THEN 2484 SRW_TAC [bossLib.ARITH_ss][]); 2485 2486val tedious_reasoning = prove( 2487 ``!M0 a. 2488 WFP (mlt1 R) M0 /\ 2489 (!b. R b a ==> !M. WFP (mlt1 R) M ==> WFP (mlt1 R) (M + {|b|})) /\ 2490 (!M. mlt1 R M M0 ==> WFP (mlt1 R) (M + {|a|})) 2491 ==> 2492 WFP (mlt1 R) (M0 + {|a|})``, 2493 REPEAT STRIP_TAC THEN MATCH_MP_TAC relationTheory.WFP_RULES THEN 2494 REPEAT STRIP_TAC THEN 2495 `FINITE_BAG y` by FULL_SIMP_TAC (srw_ss()) [mlt1_def] THEN 2496 FIRST_X_ASSUM (STRIP_ASSUME_TAC o MATCH_MP BAG_LESS_ADD) 2497 THEN1 METIS_TAC [] THEN 2498 SRW_TAC [][] THEN 2499 POP_ASSUM MP_TAC THEN 2500 FULL_SIMP_TAC (srw_ss()) [] THEN 2501 Q.PAT_X_ASSUM `FINITE_BAG KK` MP_TAC THEN 2502 Q.ID_SPEC_TAC `KK` THEN 2503 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN 2504 `R e a` by SRW_TAC [][] THEN 2505 `!M. WFP (mlt1 R) M ==> WFP (mlt1 R) (M + {|e|})` by METIS_TAC [] THEN 2506 `WFP (mlt1 R) (M0 + KK)` by METIS_TAC [] THEN 2507 `WFP (mlt1 R) (M0 + KK + {|e|})` by METIS_TAC [] THEN 2508 Q_TAC SUFF_TAC `M0 + BAG_INSERT e KK = M0 + KK + {|e|}` 2509 THEN1 METIS_TAC [] THEN 2510 SRW_TAC [][BAG_UNION, FUN_EQ_THM, BAG_INSERT, EMPTY_BAG] THEN 2511 SRW_TAC [bossLib.ARITH_ss][]); 2512 2513 2514val mlt1_all_accessible = store_thm( 2515 "mlt1_all_accessible", 2516 ``WF R ==> !M. WFP (mlt1 R) M``, 2517 STRIP_TAC THEN Q.X_GEN_TAC `M` THEN Cases_on `FINITE_BAG M` THENL [ 2518 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `M` THEN 2519 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN 2520 CONJ_TAC THEN1 2521 (MATCH_MP_TAC relationTheory.WFP_RULES THEN SRW_TAC [][]) THEN 2522 Q_TAC SUFF_TAC 2523 `!a M. WFP (mlt1 R) M ==> WFP (mlt1 R) (BAG_INSERT a M)` 2524 THEN1 METIS_TAC [] THEN 2525 FIRST_X_ASSUM 2526 (HO_MATCH_MP_TAC o MATCH_MP relationTheory.WF_INDUCTION_THM) THEN 2527 Q.X_GEN_TAC `a` THEN 2528 DISCH_THEN (ASSUME_TAC o CONV_RULE (RENAME_VARS_CONV ["b"])) THEN 2529 HO_MATCH_MP_TAC relationTheory.WFP_STRONG_INDUCT THEN 2530 ASSUME_TAC tedious_reasoning THEN 2531 FULL_SIMP_TAC (srw_ss()) [GSYM bag_insert_union], 2532 2533 MATCH_MP_TAC relationTheory.WFP_RULES THEN 2534 SRW_TAC [][mlt1_def] 2535 ]); 2536 2537val WF_mlt1 = store_thm( 2538 "WF_mlt1", 2539 ``WF R ==> WF (mlt1 R)``, 2540 METIS_TAC [relationTheory.WF_EQ_WFP, mlt1_all_accessible]); 2541 2542val TC_mlt1_FINITE_BAG = store_thm( 2543 "TC_mlt1_FINITE_BAG", 2544 ``!b1 b2. TC (mlt1 R) b1 b2 ==> FINITE_BAG b1 /\ FINITE_BAG b2``, 2545 HO_MATCH_MP_TAC relationTheory.TC_INDUCT THEN SRW_TAC [][] THEN 2546 FULL_SIMP_TAC (srw_ss()) [mlt1_def]); 2547 2548val TC_mlt1_UNION2_I = store_thm( 2549 "TC_mlt1_UNION2_I", 2550 ``!b2 b1. FINITE_BAG b2 /\ FINITE_BAG b1 /\ b2 <> {||} ==> 2551 (mlt1 R)^+ b1 (b1 + b2)``, 2552 Q_TAC SUFF_TAC 2553 `!b2. FINITE_BAG b2 ==> !b1. FINITE_BAG b1 /\ b2 <> {||} ==> 2554 (mlt1 R)^+ b1 (b1 + b2)` THEN1 METIS_TAC [] THEN 2555 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN 2556 Cases_on `b2 = {||}` THENL [ 2557 SRW_TAC [][] THEN 2558 MATCH_MP_TAC relationTheory.TC_SUBSET THEN 2559 SRW_TAC [][mlt1_def] THEN METIS_TAC [BAG_UNION_EMPTY, NOT_IN_EMPTY_BAG], 2560 2561 `(mlt1 R)^+ b1 (b1 + b2)` by METIS_TAC [] THEN 2562 MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.TC_RULES)) THEN 2563 Q.EXISTS_TAC `b1 + b2` THEN SRW_TAC [][] THEN 2564 MATCH_MP_TAC relationTheory.TC_SUBSET THEN 2565 SRW_TAC [][mlt1_def] THEN 2566 MAP_EVERY Q.EXISTS_TAC [`e`, `{||}`, `b1 + b2`] THEN SRW_TAC [][] THEN 2567 METIS_TAC [EL_BAG, BAG_INSERT_UNION, COMM_BAG_UNION, ASSOC_BAG_UNION] 2568 ]); 2569 2570val TC_mlt1_UNION1_I = store_thm( 2571 "TC_mlt1_UNION1_I", 2572 ``!b2 b1. FINITE_BAG b2 /\ FINITE_BAG b1 /\ b1 <> {||} ==> 2573 (mlt1 R)^+ b2 (b1 + b2)``, 2574 METIS_TAC [COMM_BAG_UNION,TC_mlt1_UNION2_I]); 2575 2576val mlt_NOT_REFL = store_thm( 2577 "mlt_NOT_REFL[simp]", 2578 ``WF R ==> ~(mlt R a a)``, 2579 metis_tac[WF_mlt1, relationTheory.WF_TC_EQN, 2580 relationTheory.WF_NOT_REFL]); 2581 2582val mlt_INSERT_CANCEL_I = store_thm( 2583 "mlt_INSERT_CANCEL_I", 2584 ``!a b. mlt R a b ==> mlt R (BAG_INSERT e a) (BAG_INSERT e b)``, 2585 ho_match_mp_tac relationTheory.TC_lifts_monotonicities >> 2586 simp[mlt1_def] >> rw[] >> 2587 map_every qexists_tac [`e'`, `rep`, `BAG_INSERT e res`] >> 2588 simp[BAG_UNION_INSERT]); 2589 2590val mlt1_INSERT_CANCEL = store_thm( 2591 "mlt1_INSERT_CANCEL", 2592 ``WF R ==> (mlt1 R (BAG_INSERT e a) (BAG_INSERT e b) <=> mlt1 R a b)``, 2593 simp[mlt1_def, EQ_IMP_THM] >> rpt strip_tac >> dsimp[] 2594 >- (Cases_on `e = e'` 2595 >- (fs[BAG_UNION_INSERT] >> 2596 `~(BAG_IN e' rep)` by metis_tac [relationTheory.WF_NOT_REFL] >> 2597 `BAG_IN e' res` by metis_tac[BAG_IN_BAG_UNION, BAG_IN_BAG_INSERT] >> 2598 `?b0. res = BAG_INSERT e' b0` by metis_tac[BAG_DECOMPOSE] >> 2599 fs[BAG_UNION_INSERT] >> metis_tac[]) >> 2600 `BAG_IN e res` by metis_tac[BAG_IN_BAG_UNION, BAG_IN_BAG_INSERT, 2601 NOT_IN_EMPTY_BAG] >> 2602 `?b0. res = BAG_INSERT e b0` by metis_tac [BAG_DECOMPOSE] >> 2603 fs[BAG_UNION_INSERT] >> fs[Once BAG_INSERT_commutes] >> 2604 metis_tac[]) >> 2605 map_every qexists_tac [`e'`, `rep`, `BAG_INSERT e res`] >> 2606 simp[BAG_UNION_INSERT]); 2607 2608(* dominates R b1 b2 should be read as "b2 dominates b1 wrt relation R" *) 2609val dominates_def = Define` 2610 dominates R s1 s2 = !x. x IN s1 ==> ?y. y IN s2 /\ R x y 2611`; 2612 2613val _ = overload_on ("bdominates", 2614 ``\R b1 b2. dominates R (SET_OF_BAG b1) (SET_OF_BAG b2)``) 2615 2616val dominates_EMPTY = store_thm( 2617 "dominates_EMPTY[simp]", 2618 ``dominates R {} b``, 2619 simp[dominates_def]); 2620 2621val cycles_exist = prove( 2622 ``!X. FINITE X ==> (!x. x IN X ==> f x IN X) /\ X <> {} 2623 ==> 2624 ?x n. 0 < n /\ x IN X /\ (FUNPOW f n x = x)``, 2625 strip_tac >> completeInduct_on `CARD X` >> 2626 full_simp_tac (srw_ss() ++ boolSimps.DNF_ss) [AND_IMP_INTRO] >> rw[] >> 2627 `?e X0. (X = e INSERT X0) /\ e NOTIN X0` by metis_tac[SET_CASES] >> 2628 rw[] >> fs[] >> 2629 Cases_on `?m. FUNPOW f m (f e) = e` 2630 >- (pop_assum strip_assume_tac >> 2631 map_every qexists_tac [`e`, `SUC m`] >> simp[FUNPOW]) >> 2632 fs[] >> 2633 `f e <> e` by (pop_assum (qspec_then `0` mp_tac) >> simp[]) >> 2634 `!n. FUNPOW f n (f e) IN X0` 2635 by (Induct >> simp[] >- metis_tac[] >> metis_tac[FUNPOW_SUC]) >> 2636 qabbrev_tac `XX = { FUNPOW f n (f e) | n | T }` >> 2637 `XX SUBSET X0` by dsimp[Abbr`XX`, SUBSET_DEF] >> 2638 `FINITE XX /\ CARD XX <= CARD X0` 2639 by metis_tac[SUBSET_FINITE, CARD_SUBSET] >> 2640 `CARD XX < SUC (CARD X0)` by decide_tac >> 2641 `!x. x IN XX ==> f x IN XX` 2642 by (dsimp[Abbr`XX`] >> qx_gen_tac `p` >> qexists_tac `SUC p` >> 2643 simp[FUNPOW_SUC]) >> 2644 `XX <> {}` by simp[Abbr`XX`, EXTENSION] >> 2645 metis_tac[SUBSET_DEF]); 2646 2647val dominates_SUBSET = store_thm( 2648 "dominates_SUBSET", 2649 ``transitive R /\ FINITE Y /\ dominates R Y X /\ X SUBSET Y /\ X <> {} ==> 2650 ?x. x IN X /\ R x x``, 2651 simp[dominates_def] >> rpt strip_tac >> 2652 `?f. !x. x IN Y ==> f x IN X /\ R x (f x)` by metis_tac[] >> 2653 `!x. x IN Y ==> f x IN Y` by metis_tac[SUBSET_DEF] >> 2654 `Y <> {}` by (strip_tac >> fs[]) >> 2655 qspec_then `Y` mp_tac cycles_exist >> simp[] >> 2656 strip_tac >> qexists_tac `x` >> 2657 `!p. 0 < p ==> FUNPOW f p x IN X /\ R x (FUNPOW f p x)` 2658 by (Induct >> simp[FUNPOW_SUC] >> 2659 Cases_on `p` >> fs[FUNPOW_SUC] >> 2660 metis_tac[SUBSET_DEF, relationTheory.transitive_def]) >> 2661 metis_tac[]) 2662 2663(* the transitivity requirement can be seen in the following example. 2664 Imagine R is (\m n. n = SUC m), whose transitive closure is <. 2665 Then we have 2666 mlt R {|0|} {|2|} 2667 because the first step removes 2 and replaces it with a 1. The next step 2668 then replaces the 1 with a 0. 2669 2670 But the alternative "definition" of mlt below is not satisfied because x has to 2671 be {|2|} and y has to be {|0|}. But y is not dominated by x, because there is 2672 nothing in x that is R-bigger than 0. 2673*) 2674val mlt_dominates_thm1 = store_thm( 2675 "mlt_dominates_thm1", 2676 ``transitive R ==> 2677 !b1 b2. mlt R b1 b2 <=> 2678 FINITE_BAG b1 /\ FINITE_BAG b2 /\ 2679 ?x y. x <> {||} /\ SUB_BAG x b2 /\ 2680 (b1 = (b2 - x) + y) /\ 2681 bdominates R y x``, 2682 simp[EQ_IMP_THM, FORALL_AND_THM] >> strip_tac >> conj_tac 2683 >- (ho_match_mp_tac relationTheory.TC_STRONG_INDUCT_LEFT1 >> 2684 conj_tac 2685 >- (simp[mlt1_def, dominates_def] >> map_every qx_gen_tac [`b1`, `b2`] >> 2686 strip_tac >> map_every qexists_tac [`{|e|}`, `rep`] >> 2687 simp[COMM_BAG_UNION]) >> 2688 rpt strip_tac >> 2689 qmatch_assum_rename_tac `mlt1 R B0 B1` >> 2690 qmatch_assum_rename_tac `mlt R B1 B2` >> 2691 fs[mlt1_def] >> 2692 qmatch_assum_rename_tac `!e'. BAG_IN e' Rep ==> R e' E` >> 2693 qmatch_assum_rename_tac `(B2 - X) + Y = Res + {|E|}` >> 2694 Cases_on `BAG_IN E Y` 2695 >- (map_every qexists_tac [`X`, `Y - {| E |} + Rep`] >> 2696 simp[] >> reverse conj_tac 2697 >- (fs[dominates_def] >> 2698 metis_tac [BAG_IN_DIFF_E, relationTheory.transitive_def]) >> 2699 pop_assum mp_tac >> 2700 qpat_x_assum `B2 - X + Y = Res + {|E|}` mp_tac >> 2701 simp[BAG_DIFF, FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG, 2702 BAG_IN, BAG_INN] >> 2703 disch_then (fn allth => disch_then 2704 (fn YE => qx_gen_tac `ee` >> 2705 qspec_then `ee` mp_tac allth >> 2706 mp_tac YE)) >> 2707 COND_CASES_TAC >> simp[]) >> 2708 map_every qexists_tac [`BAG_INSERT E X`, `Y + Rep`] >> simp[] >> 2709 reverse (rpt conj_tac) 2710 >- (fs[dominates_def] >> metis_tac[]) 2711 >- (pop_assum mp_tac >> 2712 qpat_x_assum `B2 - X + Y = Res + {|E|}` mp_tac >> 2713 simp[BAG_DIFF, FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG, 2714 BAG_IN, BAG_INN] >> 2715 disch_then (fn allth => disch_then 2716 (fn YE => qx_gen_tac `ee` >> 2717 qspec_then `ee` mp_tac allth >> 2718 mp_tac YE)) >> 2719 COND_CASES_TAC >> simp[]) >> 2720 pop_assum mp_tac >> 2721 qpat_x_assum `X <= B2` mp_tac >> 2722 qpat_x_assum `B2 - X + Y = Res + {|E|}` mp_tac >> 2723 simp[BAG_DIFF, FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG, 2724 BAG_IN, BAG_INN, SUB_BAG_LEQ] >> 2725 disch_then 2726 (fn allth1 => disch_then 2727 (fn allth2 => disch_then 2728 (fn YE => qx_gen_tac `ee` >> 2729 qspec_then `ee` mp_tac allth1 >> 2730 qspec_then `ee` mp_tac allth2 >> 2731 mp_tac YE))) >> 2732 COND_CASES_TAC >> simp[]) >> 2733 rpt strip_tac >> rw[] >> 2734 `FINITE_BAG x` by metis_tac[FINITE_SUB_BAG] >> 2735 fs[] >> map_every (C qpat_x_assum mp_tac) [ 2736 `FINITE_BAG b2`, `FINITE_BAG y`, `bdominates R y x`, 2737 `x <= b2`, `x <> {||}`] >> 2738 map_every qid_spec_tac [`b2`, `y`] >> pop_assum mp_tac >> 2739 pop_assum kall_tac >> qid_spec_tac `x` >> 2740 ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >> simp[] >> rpt strip_tac >> 2741 Cases_on `x = {||}` 2742 >- (rw[] >> fs[dominates_def] >> 2743 match_mp_tac relationTheory.TC_SUBSET >> 2744 simp[mlt1_def, FINITE_BAG_DIFF] >> 2745 map_every qexists_tac [`e`, `y`, `b2 - {|e|}`] >> 2746 simp[COMM_BAG_UNION, SUB_BAG_DIFF_EQ]) >> 2747 match_mp_tac (relationTheory.TC_RULES |> SPEC_ALL |> CONJUNCT2) >> 2748 qexists_tac `b2 - {|e|} + BAG_FILTER (\x. R x e) y` >> reverse conj_tac 2749 >- (match_mp_tac relationTheory.TC_SUBSET >> simp[mlt1_def, FINITE_BAG_DIFF]>> 2750 map_every qexists_tac [`e`, `BAG_FILTER (\x. R x e) y`, `b2 - {|e|}`] >> 2751 simp[] >> simp[COMM_BAG_UNION] >> match_mp_tac SUB_BAG_DIFF_EQ >> 2752 simp[] >> metis_tac[SUB_BAG_BAG_IN]) >> 2753 `b2 - BAG_INSERT e x + y = 2754 b2 - {|e|} + BAG_FILTER (\x. R x e) y - x + BAG_FILTER (\x. ~R x e) y` 2755 by (qpat_x_assum `BAG_INSERT e x <= b2` mp_tac >> 2756 simp_tac bool_ss [FUN_EQ_THM, SUB_BAG_LEQ, BAG_DIFF, BAG_UNION, 2757 EMPTY_BAG, BAG_INSERT, BAG_FILTER_DEF] >> simp[] >> 2758 strip_tac >> qx_gen_tac `a` >> pop_assum (qspec_then `a` mp_tac) >> 2759 rpt COND_CASES_TAC >> simp[] >> fs[]) >> 2760 fs[AND_IMP_INTRO] >> first_x_assum match_mp_tac >> simp[FINITE_BAG_DIFF] >> 2761 conj_tac 2762 >- (fs[SUB_BAG_LEQ, BAG_INSERT, EMPTY_BAG, BAG_FILTER_DEF, BAG_DIFF, 2763 BAG_UNION] >> qx_gen_tac `a` >> 2764 first_x_assum (qspec_then `a` mp_tac) >> 2765 COND_CASES_TAC >> simp[] >> decide_tac) >> 2766 fs[dominates_def] >> metis_tac[]) 2767 2768val dominates_DIFF = store_thm( 2769 "dominates_DIFF", 2770 ``WF R /\ transitive R /\ dominates R x y /\ FINITE i /\ 2771 i SUBSET x /\ i SUBSET y ==> 2772 dominates R (x DIFF i) (y DIFF i)``, 2773 map_every Cases_on [`WF R`, `transitive R`, `dominates R x y`, `FINITE i`] >> 2774 simp[] >> 2775 pop_assum mp_tac >> qid_spec_tac `i` >> Induct_on `FINITE i` >> 2776 simp[] >> qx_gen_tac `i` >> strip_tac >> qx_gen_tac `e` >> strip_tac >> 2777 strip_tac >> simp[dominates_def] >> fs[] >> 2778 qx_gen_tac `a` >> strip_tac >> 2779 `?b. b IN y /\ b NOTIN i /\ R a b` by (fs[dominates_def] >> metis_tac[]) >> 2780 Cases_on `b = e` 2781 >- (pop_assum SUBST_ALL_TAC >> 2782 `?c. c IN y /\ c NOTIN i /\ R e c` 2783 by (fs[dominates_def] >> metis_tac[]) >> 2784 `c <> e` by metis_tac[relationTheory.WF_NOT_REFL] >> 2785 metis_tac[relationTheory.transitive_def]) >> 2786 metis_tac[]); 2787 2788val BAG_INSERT_SUB_BAG_E = store_thm( 2789 "BAG_INSERT_SUB_BAG_E", 2790 ``BAG_INSERT e b <= c ==> BAG_IN e c /\ b <= c``, 2791 simp[SUB_BAG_LEQ, BAG_INSERT, BAG_IN, BAG_INN] >> strip_tac >> conj_tac 2792 >- (first_x_assum (qspec_then `e` mp_tac) >> simp[]) >> 2793 qx_gen_tac `a` >> first_x_assum (qspec_then `a` mp_tac) >> rw[] >> simp[]); 2794 2795val bdominates_BAG_DIFF = store_thm( 2796 "bdominates_BAG_DIFF", 2797 ``WF R /\ transitive R /\ bdominates R x y /\ 2798 FINITE_BAG i /\ i <= x /\ i <= y ==> 2799 bdominates R (x - i) (y - i)``, 2800 map_every Cases_on [`WF R`, `transitive R`, `bdominates R x y`, 2801 `FINITE_BAG i`] >> 2802 simp[] >> 2803 pop_assum mp_tac >> qid_spec_tac `i` >> Induct_on `FINITE_BAG i` >> 2804 simp[] >> qx_gen_tac `i` >> strip_tac >> qx_gen_tac `e` >> strip_tac >> 2805 imp_res_tac BAG_INSERT_SUB_BAG_E >> fs[] >> simp[dominates_def] >> 2806 qx_gen_tac `a` >> strip_tac >> 2807 `BAG_IN a (x - i)` 2808 by (pop_assum mp_tac >> simp[BAG_IN, BAG_INN, BAG_INSERT, BAG_DIFF] >> 2809 rw[] >> simp[]) >> 2810 `?b. BAG_IN b (y - i) /\ R a b` by metis_tac[dominates_def, IN_SET_OF_BAG] >> 2811 reverse (Cases_on `b = e`) 2812 >- (qexists_tac `b` >> 2813 `y - BAG_INSERT e i = y - i - {| e |}` 2814 by (simp[FUN_EQ_THM, BAG_DIFF, BAG_INSERT, EMPTY_BAG] >> rw[] >> 2815 simp[]) >> 2816 pop_assum SUBST_ALL_TAC >> simp[] >> 2817 match_mp_tac BAG_IN_DIFF_I >> simp[]) >> 2818 pop_assum SUBST_ALL_TAC >> 2819 `BAG_IN e (x - i)` 2820 by (qpat_x_assum `BAG_INSERT e i <= x` mp_tac >> 2821 simp[BAG_DIFF, BAG_INSERT, SUB_BAG_LEQ, BAG_IN, 2822 BAG_INN] >> disch_then (qspec_then `e` mp_tac) >> 2823 simp[]) >> 2824 `?c. BAG_IN c (y - i) /\ R e c` by metis_tac[dominates_def, IN_SET_OF_BAG] >> 2825 `c <> e` by metis_tac[relationTheory.WF_NOT_REFL] >> 2826 `R a c` by metis_tac[relationTheory.transitive_def] >> 2827 qexists_tac `c` >> 2828 `y - BAG_INSERT e i = y - i - {| e |}` 2829 by (simp[FUN_EQ_THM, BAG_DIFF, BAG_INSERT, EMPTY_BAG] >> rw[] >> 2830 simp[]) >> 2831 pop_assum SUBST_ALL_TAC >> simp[] >> 2832 match_mp_tac BAG_IN_DIFF_I >> simp[]) 2833 2834val BAG_INTER_SUB_BAG = store_thm( 2835 "BAG_INTER_SUB_BAG[simp]", 2836 ``SUB_BAG (BAG_INTER b1 b2) b1 /\ SUB_BAG (BAG_INTER b1 b2) b2``, 2837 simp[BAG_INTER, SUB_BAG_LEQ]); 2838 2839val BAG_INTER_FINITE = store_thm( 2840 "BAG_INTER_FINITE", 2841 ``FINITE_BAG b1 \/ FINITE_BAG b2 ==> FINITE_BAG (BAG_INTER b1 b2)``, 2842 metis_tac[FINITE_SUB_BAG, BAG_INTER_SUB_BAG]); 2843 2844val mlt_dominates_thm2 = store_thm( 2845 "mlt_dominates_thm2", 2846 ``WF R /\ transitive R ==> 2847 !b1 b2. mlt R b1 b2 <=> 2848 FINITE_BAG b1 /\ FINITE_BAG b2 /\ 2849 ?x y. x <> {||} /\ SUB_BAG x b2 /\ 2850 BAG_DISJOINT x y /\ 2851 (b1 = (b2 - x) + y) /\ 2852 bdominates R y x``, 2853 rpt strip_tac >> simp[mlt_dominates_thm1] >> 2854 map_every Cases_on [`FINITE_BAG b1`, `FINITE_BAG b2`] >> simp[] >> 2855 reverse eq_tac >> strip_tac >- metis_tac[] >> 2856 qabbrev_tac `II = BAG_INTER x y` >> 2857 map_every qexists_tac [`x - II`, `y - II`] >> 2858 `x - II <= b2` by simp[SUB_BAG_DIFF] >> 2859 `II <= x /\ II <= y` by simp[Abbr`II`, BAG_INTER, SUB_BAG_LEQ] >> 2860 simp[] >> 2861 `~(x <= II)` 2862 by (strip_tac >> 2863 `x = II` by simp[SUB_BAG_ANTISYM] >> rw[] >> 2864 qspecl_then [`R`, `SET_OF_BAG II`, `SET_OF_BAG y`] mp_tac 2865 (Q.GENL [`R`, `X`, `Y`] dominates_SUBSET) >> simp[] >> 2866 fs[SUB_BAG_SET] >> qx_gen_tac `e` >> Cases_on `BAG_IN e II` >> 2867 simp[] >> metis_tac[relationTheory.WF_NOT_REFL]) >> 2868 simp[] >> 2869 `BAG_DISJOINT (x - II) (y - II)` 2870 by (simp[BAG_DISJOINT, DISJOINT_DEF, EXTENSION] >> 2871 qx_gen_tac `e` >> Cases_on `BAG_IN e (x - II)` >> simp[] >> 2872 pop_assum mp_tac >> 2873 simp[Abbr`II`, BAG_IN, BAG_INN, BAG_INTER, BAG_DIFF]) >> 2874 simp[] >> 2875 `bdominates R (y - II) (x - II)` 2876 by (match_mp_tac (GEN_ALL bdominates_BAG_DIFF) >> simp[] >> 2877 simp[Abbr`II`] >> metis_tac[FINITE_SUB_BAG, BAG_INTER_FINITE]) >> 2878 simp[] >> 2879 map_every (fn q => qpat_x_assum q mp_tac) 2880 [`x <= b2`, `II <= x`, `II <= y`] >> 2881 simp_tac bool_ss [BAG_DIFF, SUB_BAG_LEQ, BAG_UNION, FUN_EQ_THM] >> 2882 ntac 3 strip_tac >> qx_gen_tac `a` >> 2883 ntac 3 (pop_assum (qspec_then `a` mp_tac)) >> simp[]) 2884 2885val BAG_DIFF_INSERT_SUB_BAG = store_thm( 2886 "BAG_DIFF_INSERT_SUB_BAG", 2887 ``c <= b ==> (BAG_INSERT e b - c = BAG_INSERT e (b - c))``, 2888 simp[SUB_BAG_LEQ, BAG_INSERT, BAG_DIFF, FUN_EQ_THM] >> strip_tac >> 2889 qx_gen_tac `e2` >> pop_assum (qspec_then `e2` mp_tac) >> rw[] >> 2890 simp[]); 2891 2892val mlt_INSERT_CANCEL = store_thm( 2893 "mlt_INSERT_CANCEL", 2894 ``transitive R /\ WF R ==> 2895 (mlt R (BAG_INSERT e a) (BAG_INSERT e b) <=> mlt R a b)``, 2896 simp[mlt_dominates_thm2] >> strip_tac >> eq_tac >> strip_tac >> simp[] 2897 >- (map_every qexists_tac [`x`, `y`] >> simp[] >> 2898 `x <= b` 2899 by (qpat_x_assum `x <= BAG_INSERT e b` mp_tac >> 2900 simp[SUB_BAG_LEQ, BAG_INSERT] >> strip_tac >> 2901 qx_gen_tac `e2` >> pop_assum (qspec_then `e2` mp_tac) >> rw[] >> 2902 spose_not_then strip_assume_tac >> 2903 `x e = b e + 1` by decide_tac >> 2904 `BAG_IN e x` by simp[BAG_IN, BAG_INN] >> 2905 `~BAG_IN e (BAG_INSERT e b - x)` 2906 by simp[BAG_IN, BAG_INSERT, BAG_DIFF, BAG_INN] >> 2907 `BAG_IN e y` by metis_tac[BAG_IN_BAG_INSERT, BAG_IN_BAG_UNION] >> 2908 metis_tac[BAG_DISJOINT_BAG_IN]) >> 2909 `BAG_INSERT e b - x + y = BAG_INSERT e (b - x + y)` suffices_by 2910 metis_tac[BAG_INSERT_ONE_ONE] >> 2911 `BAG_INSERT e b - x = BAG_INSERT e (b - x)` 2912 by metis_tac[BAG_DIFF_INSERT_SUB_BAG] >> 2913 pop_assum SUBST_ALL_TAC >> simp[BAG_UNION_INSERT]) >> 2914 map_every qexists_tac [`x`, `y`] >> 2915 simp[BAG_DIFF_INSERT_SUB_BAG, BAG_UNION_INSERT, SUB_BAG_INSERT_I]); 2916 2917val mlt_UNION_RCANCEL_I = store_thm( 2918 "mlt_UNION_RCANCEL_I", 2919 ``mlt R a b /\ FINITE_BAG c ==> 2920 mlt R (BAG_UNION a c) (BAG_UNION b c)``, 2921 `mlt R a b ==> 2922 !c. FINITE_BAG c ==> 2923 mlt R (BAG_UNION a c) (BAG_UNION b c)` 2924 suffices_by metis_tac[] >> strip_tac >> 2925 ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >> 2926 simp[BAG_UNION_INSERT, mlt_INSERT_CANCEL_I]); 2927 2928val mlt_UNION_RCANCEL = store_thm( 2929 "mlt_UNION_RCANCEL[simp]", 2930 ``WF R /\ transitive R ==> 2931 (mlt R (BAG_UNION a c) (BAG_UNION b c) <=> mlt R a b /\ FINITE_BAG c)``, 2932 strip_tac >> reverse (Cases_on `FINITE_BAG c`) >> simp[] 2933 >- (strip_tac >> imp_res_tac TC_mlt1_FINITE_BAG >> fs[]) >> 2934 map_every qid_spec_tac [`a`, `b`] >> pop_assum mp_tac >> 2935 qid_spec_tac `c` >> ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >> 2936 simp[BAG_UNION_INSERT, mlt_INSERT_CANCEL]); 2937 2938val mlt_UNION_LCANCEL_I = save_thm( 2939 "mlt_UNION_LCANCEL_I", 2940 ONCE_REWRITE_RULE [COMM_BAG_UNION] mlt_UNION_RCANCEL_I); 2941 2942val mlt_UNION_LCANCEL = save_thm( 2943 "mlt_UNION_LCANCEL[simp]", 2944 ONCE_REWRITE_RULE [COMM_BAG_UNION] mlt_UNION_RCANCEL) 2945 2946val mlt_UNION_lemma = prove( 2947 ``WF R ==> 2948 (mlt R b1 (BAG_UNION b1 b2) <=> 2949 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||})``, 2950 strip_tac >> `WF (mlt R)` by simp[relationTheory.WF_TC_EQN, WF_mlt1] >> 2951 reverse eq_tac >- simp[TC_mlt1_UNION2_I] >> 2952 strip_tac >> imp_res_tac TC_mlt1_FINITE_BAG >> 2953 fs[] >> strip_tac >> fs[] >> metis_tac[relationTheory.WF_NOT_REFL]); 2954 2955val mlt_UNION_CANCEL_EQN = store_thm( 2956 "mlt_UNION_CANCEL_EQN[simp]", 2957 ``WF R ==> 2958 (mlt R b1 (BAG_UNION b1 b2) <=> 2959 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||}) /\ 2960 (mlt R b1 (BAG_UNION b2 b1) <=> 2961 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||})``, 2962 metis_tac[COMM_BAG_UNION, mlt_UNION_lemma]) 2963 2964val mlt_UNION_EMPTY_EQN = save_thm( 2965 "mlt_UNION_EMPTY_EQN", 2966 mlt_UNION_CANCEL_EQN |> Q.INST [`b1` |-> `{||}`] 2967 |> SIMP_RULE (srw_ss()) []); 2968 2969val SUB_BAG_SING = store_thm( 2970 "SUB_BAG_SING[simp]", 2971 ``b <= {|e|} <=> (b = {||}) \/ (b = {|e|})``, 2972 simp[SUB_BAG_LEQ, FUN_EQ_THM, EMPTY_BAG, BAG_INSERT, EQ_IMP_THM] >> 2973 rpt strip_tac >> simp[] >> Cases_on `b e = 1` 2974 >- (disj2_tac >> rw[] >> first_x_assum (qspec_then `x` mp_tac) >> simp[]) >> 2975 disj1_tac >> qx_gen_tac `x` >> first_x_assum (qspec_then `x` mp_tac) >> 2976 rw[] >> simp[]); 2977 2978val SUB_BAG_DIFF_simple = store_thm( 2979 "SUB_BAG_DIFF_simple[simp]", 2980 ``b - c <= b:'a bag``, 2981 simp[SUB_BAG_DIFF]); 2982 2983val mltLT_SING0 = store_thm( 2984 "mltLT_SING0", 2985 ``mlt (<) {|0:num|} b <=> FINITE_BAG b /\ b <> {|0|} /\ b <> {||}``, 2986 reverse eq_tac 2987 >- (strip_tac >> simp[mlt_dominates_thm1, relationTheory.transitive_def] >> 2988 Cases_on `BAG_IN 0 b` 2989 >- (map_every qexists_tac [`b - {|0|}`, `{||}`] >> 2990 simp[] >> 2991 qpat_x_assum`BAG_IN 0 b` mp_tac >> 2992 simp[BAG_IN, BAG_INN, FUN_EQ_THM, EMPTY_BAG, 2993 BAG_INSERT, BAG_DIFF] >> rw[] >> rw[] >> 2994 simp[]) >> 2995 map_every qexists_tac [`b`, `{|0|}`] >> simp[] >> 2996 simp[dominates_def] >> 2997 `?e b0. b = BAG_INSERT e b0` by metis_tac [BAG_cases] >> 2998 metis_tac[BAG_IN_BAG_INSERT, DECIDE ``x <> 0 <=> 0 < x``]) >> 2999 simp[mlt_dominates_thm2, relationTheory.transitive_def] >> 3000 rpt strip_tac 3001 >- (fs[] >> fs[] >> rw[] >> fs[] >> rw[] >> 3002 metis_tac[BAG_DISJOINT_BAG_IN, BAG_IN_BAG_INSERT]) >> 3003 fs[]); 3004 3005(*---------------------------------------------------------------------------*) 3006(* Size of a finite multiset is taken to be the sum of the sizes of all the *) 3007(* elements, plus the number of elements. *) 3008(*---------------------------------------------------------------------------*) 3009 3010val bag_size_def = 3011 Define 3012 `bag_size eltsize b = ITBAG (\e acc. 1 + eltsize e + acc) b 0`; 3013 3014val BAG_SIZE_EMPTY = Q.store_thm 3015("BAG_SIZE_EMPTY", 3016 `bag_size eltsize {||} = 0`, 3017 METIS_TAC [ITBAG_THM,bag_size_def,FINITE_EMPTY_BAG]); 3018 3019(*---------------------------------------------------------------------------*) 3020(* BAG_SIZE_INSERT = *) 3021(* |- FINITE_BAG b ==> *) 3022(* bag_size eltsize (BAG_INSERT e b) = 1 + eltsize e + bag_size eltsize b *) 3023(*---------------------------------------------------------------------------*) 3024 3025val BAG_SIZE_INSERT = save_thm 3026("BAG_SIZE_INSERT", 3027 let val f = ``\(e:'a) acc. 1 + eltsize e + acc`` 3028 val LCOMM_INCR = Q.prove 3029 (`!x y z. ^f x (^f y z) = ^f y (^f x z)`, RW_TAC arith_ss []) 3030 in COMMUTING_ITBAG_RECURSES 3031 |> ISPEC f 3032 |> SIMP_RULE bool_ss [LCOMM_INCR] 3033 |> (ISPEC``0n`` o Q.ID_SPEC o Q.ID_SPEC) 3034 |> SIMP_RULE bool_ss [GSYM bag_size_def] 3035 end); 3036 3037val _ = print "Unibags (bags made all distinct)\n" 3038 3039val _ = overload_on ("unibag", ``\b. BAG_OF_SET (SET_OF_BAG b)``); 3040 3041val unibag_thm = save_thm("unibag_thm", CONJ BAG_OF_SET SET_OF_BAG); 3042 3043Theorem unibag_INSERT: 3044 !a b. (unibag (BAG_INSERT a b)) = BAG_MERGE {|a|} (unibag b) 3045Proof rw[BAG_OF_SET_INSERT,SET_OF_BAG_INSERT] 3046QED 3047 3048Theorem unibag_UNION: 3049 !a b. unibag (a + b) = BAG_MERGE (unibag a) (unibag b) 3050Proof rw[SET_OF_BAG_UNION,BAG_OF_SET_UNION] 3051QED 3052 3053Theorem unibag_EQ_BAG_INSERT: 3054 !e b b'. (unibag b = BAG_INSERT e b') ==> ?c. (b' = unibag c) 3055Proof 3056 rw[] >> 3057 fs[unibag_thm,BAG_INSERT,FUN_EQ_THM,BAG_IN,BAG_INN] >> 3058 qexists_tac `b'` >> 3059 rw[] >> 3060 first_x_assum (qspec_then `x` mp_tac) >> 3061 rw[] >> 3062 Induct_on `b' e` >> 3063 rw[] 3064QED 3065 3066Theorem unibag_FINITE: 3067 !b. FINITE_BAG (unibag b) = FINITE_BAG b 3068Proof 3069 rw[] >> EQ_TAC >> metis_tac[FINITE_SET_OF_BAG, FINITE_BAG_OF_SET] 3070QED 3071 3072Theorem unibag_ALL_DISTINCT: 3073 !b. BAG_ALL_DISTINCT (unibag b) 3074Proof rw[BAG_ALL_DISTINCT] 3075QED 3076 3077Theorem BAG_IN_unibag[simp]: 3078 !e b. BAG_IN e (unibag b) <=> BAG_IN e b 3079Proof rw[BAG_IN] 3080QED 3081 3082Theorem unibag_EL_MERGE_cases: 3083 !e b. ((BAG_IN e b) ==> (BAG_MERGE {|e|} (unibag b) = (unibag b))) /\ 3084 (~(BAG_IN e b) ==> (BAG_MERGE {|e|} (unibag b) = BAG_INSERT e (unibag b))) 3085Proof 3086 rw[] 3087 >- (`BAG_ALL_DISTINCT (unibag b)` by metis_tac[unibag_ALL_DISTINCT] >> 3088 `BAG_ALL_DISTINCT {|e|}` by simp[BAG_ALL_DISTINCT_THM] >> 3089 `BAG_ALL_DISTINCT (BAG_MERGE {|e|} (unibag b))` 3090 by simp[BAG_ALL_DISTINCT_BAG_MERGE] >> 3091 qspecl_then [`BAG_MERGE {|e|} (unibag b)`,`unibag b`] mp_tac 3092 BAG_ALL_DISTINCT_EXTENSION >> 3093 rw[] >> 3094 metis_tac[]) 3095 >- (`BAG_ALL_DISTINCT (unibag b)` by metis_tac[unibag_ALL_DISTINCT] >> 3096 `BAG_ALL_DISTINCT {|e|}` by simp[BAG_ALL_DISTINCT_THM] >> 3097 `BAG_ALL_DISTINCT (BAG_MERGE {|e|} (unibag b))` 3098 by simp[BAG_ALL_DISTINCT_BAG_MERGE] >> 3099 `BAG_ALL_DISTINCT (BAG_INSERT e (unibag b))` 3100 by simp[BAG_ALL_DISTINCT] >> 3101 qspecl_then [`BAG_MERGE {|e|} (unibag b)`,`BAG_INSERT e (unibag b)`] 3102 mp_tac BAG_ALL_DISTINCT_EXTENSION >> 3103 rw[]) 3104QED 3105 3106Theorem unibag_DECOMPOSE: 3107 unibag g <> g ==> ?A g0. g = {|A;A|} + g0 3108Proof 3109 simp[unibag_thm] >> 3110 simp[SimpL ``$==>``,FUN_EQ_THM,PULL_EXISTS] >> 3111 rw[] 3112 >- (qexists_tac `x` >> 3113 qexists_tac `g (| x |-> g x - 2 |)` >> 3114 fs[BAG_IN,BAG_INN] >> 3115 simp[FUN_EQ_THM,BAG_UNION, 3116 BAG_INSERT,EMPTY_BAG,combinTheory.APPLY_UPDATE_THM] >> 3117 qx_gen_tac `y` >> 3118 Cases_on `x=y` >> 3119 rw[]) 3120 >- fs[BAG_IN,BAG_INN] 3121QED 3122 3123Theorem unibag_SUB_BAG: 3124 !b. unibag b <= b 3125Proof rw[unibag_thm,SUB_BAG,BAG_IN,BAG_INN] 3126QED 3127 3128 3129 3130(*---------------------------------------------------------------------------*) 3131(* Add multiset type to the TypeBase. *) 3132(*---------------------------------------------------------------------------*) 3133 3134val _ = TypeBase.export [ 3135 TypeBasePure.mk_nondatatype_info 3136 (���:'a -> num���, 3137 {nchotomy = SOME BAG_cases, 3138 induction = SOME STRONG_FINITE_BAG_INDUCT, 3139 size = NONE, 3140 encode=NONE}) 3141 ] 3142 3143val _ = export_theory(); 3144