1structure bagSimpleLib :> bagSimpleLib = 2struct 3 4open HolKernel boolLib bossLib 5 6local open bagTheory in end 7 8open bagSyntax 9 10 11 12(******************************************************************************) 13(* This file contains tools to handle "simple" bags. *) 14(* *) 15(* In the context of this file, a "simple" bag is a bag, that just consists *) 16(* of insertions into the empty bag. For example *) 17(* *) 18(* {|x1;x2;x3;x4|}, {||}, {|x1|} are simple bags *) 19(* *) 20(* BAG_UNION {|x1;x2|} {|x3;x4|}, BAG_INSERT e b are not *) 21(* *) 22(******************************************************************************) 23 24val is_simple = can dest_bag; 25 26 27(******************************************************************************) 28(* Resorting bags *) 29(* *) 30(* The insert of bags commutes. Therefore, there order can be easily changed. *) 31(* For example: {|x0; x1; x2; x3; x4|} = {|x0; x3; x2; x1; x4|} *) 32(* *) 33(* This conversion provides a way of doing such resorts. It gets a list *) 34(* of integers that represent the positions of elements in the original list; *) 35(* counting starts with zero. It then sorts these elements to the front of *) 36(* the new bag. Any remaining elements are placed behind them. It's *) 37(* assumed that the elements of this list of integers are pairwise distinct. *) 38(* *) 39(* For example: *) 40(* BAG_RESORT_CONV [0,3,2] ``{|x0; x1; x2; x3; x4|}`` results in *) 41(* {|x0; x3; x2; x1; x4|} *) 42(******************************************************************************) 43 44 45local 46 fun BAG_RESORT___BRING_TO_FRONT_CONV 0 b = REFL b 47 | BAG_RESORT___BRING_TO_FRONT_CONV n b = 48 let 49 (*remove frist element and 50 bring to front in rest of the bag*) 51 val (e1,b') = bagSyntax.dest_insert b; 52 val thm0 = BAG_RESORT___BRING_TO_FRONT_CONV (n-1) b'; 53 54 (*add first element again*) 55 val thm1 = AP_TERM (rator b) thm0; 56 57 (*swap the first two elements*) 58 val (e2, b'') = bagSyntax.dest_insert (rhs (concl thm0)); 59 val thm2 = ISPECL [b'', e1, e2] bagTheory.BAG_INSERT_commutes 60 val thm3 = TRANS thm1 thm2 61 in 62 thm3 63 end; 64 65in 66 fun BAG_RESORT_CONV [] b = REFL b (*nothing to do*) 67 | BAG_RESORT_CONV [n] b = BAG_RESORT___BRING_TO_FRONT_CONV n b (*that's simple :-)*) 68 | BAG_RESORT_CONV (n::n2::ns) b = 69 let 70 (*first bring the first element, i.e. n, to the front*) 71 val thm0 = BAG_RESORT___BRING_TO_FRONT_CONV n b; 72 73 (*remove first element*) 74 val (insert_e1,b') = dest_comb (rhs (concl thm0)); 75 76 (*resort the rest of the bag 77 elements that occur before the one just moved to the front have the 78 some position in b' as they had in b. The others moved one position to 79 the front *) 80 val ns' = map (fn m => if (n < m) then (m - 1) else m) (n2::ns); 81 val thm1 = BAG_RESORT_CONV ns' b'; 82 83 (*combine again*) 84 val thm2 = AP_TERM insert_e1 thm1; 85 val thm3 = TRANS thm0 thm2 86 in 87 thm3 88 end; 89end 90 91 92 93 94(******************************************************************************) 95(* BAG_IMAGE_CONV *) 96(* *) 97(* Moves BAG_IMAGE over very simple bags that consists of repeatedly *) 98(* inserting elements into the empty bag. For these bags, it's very easy to *) 99(* show that they are finite. *) 100(* *) 101(* For example: *) 102(* BAG_IMAGE_CONV ``BAG_IMAGE f {|x0; x1; x2; x3; x4|}`` results in *) 103(* {|f x0; f x1; f x2; f x3; f x4|} *) 104(******************************************************************************) 105 106fun BAG_IMAGE_CONV___FINITE t = 107 let val (f,b) = dest_image t in 108 if (is_empty b) then 109 let 110 val bag_type = bagSyntax.base_type b 111 val finite_thm = INST_TYPE [alpha |-> bag_type] bagTheory.FINITE_EMPTY_BAG; 112 val bag_thm = ISPEC f bagTheory.BAG_IMAGE_EMPTY 113 in 114 (finite_thm, bag_thm) 115 end 116 else if (is_union b) then 117 let 118 val (b1,b2) = dest_union b; 119 val t1 = mk_image (f, b1) 120 val t2 = mk_image (f, b2) 121 val (finite_thm1, bag_thm1) = BAG_IMAGE_CONV___FINITE t1; 122 val (finite_thm2, bag_thm2) = BAG_IMAGE_CONV___FINITE t2; 123 val finite_thm12 = CONJ finite_thm1 finite_thm2 124 125 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION)) 126 finite_thm12 127 val bag_thm' = MP (ISPECL [b1,b2,f] bagTheory.BAG_IMAGE_FINITE_UNION) finite_thm12 128 val bag_thm'' = CONV_RULE (RHS_CONV ( 129 ((RATOR_CONV o RAND_CONV) (K bag_thm1)) THENC 130 ((RAND_CONV) (K bag_thm2)))) bag_thm' 131 in 132 (finite_thm, bag_thm'') 133 end 134 else 135 let 136 val (e,b') = dest_insert b; 137 val t' = mk_image (f, b') 138 val (finite_thm, bag_thm) = BAG_IMAGE_CONV___FINITE t'; 139 val finite_thm2 = SPEC e (MP (ISPEC b' bagTheory.FINITE_BAG_INSERT) finite_thm); 140 val bag_thm' = MP (ISPECL [b',f,e] 141 (bagTheory.BAG_IMAGE_FINITE_INSERT)) finite_thm 142 val bag_thm2 = CONV_RULE (RHS_CONV (RAND_CONV 143 (K bag_thm))) bag_thm' 144 in 145 (finite_thm2, bag_thm2) 146 end 147 end handle HOL_ERR _ => raise UNCHANGED; 148 149 150val BAG_IMAGE_CONV = snd o BAG_IMAGE_CONV___FINITE; 151 152 153(******************************************************************************) 154(* BAG_CARD_CONV *) 155(* *) 156(* Moves BAG_IMAGE over very simple bags that consists of repeatedly *) 157(* inserting elements into the empty bag. For these bags, it's very easy to *) 158(* show that they are finite. *) 159(* *) 160(* For example: *) 161(* BAG_IMAGE_CONV ``BAG_IMAGE f {|x0; x1; x2; x3; x4|}`` results in *) 162(* {|f x0; f x1; f x2; f x3; f x4|} *) 163(******************************************************************************) 164 165local 166 val card_empty_thm = CONJUNCT1 bagTheory.BAG_CARD_THM 167 val card_insert_thm = CONV_RULE (DEPTH_CONV RIGHT_IMP_FORALL_CONV) 168 (CONJUNCT2 bagTheory.BAG_CARD_THM) 169 val eval_num_RULE = CONV_RULE (RHS_CONV numLib.REDUCE_CONV) 170 171 fun BAG_CARD_CONV___FINITE b = 172 (if (is_empty b) then 173 let 174 val bag_type = bagSyntax.base_type b 175 val finite_thm = INST_TYPE [alpha |-> bag_type] bagTheory.FINITE_EMPTY_BAG; 176 val card_thm = INST_TYPE [alpha |-> bag_type] card_empty_thm; 177 in 178 (finite_thm, card_thm) 179 end 180 else if (is_union b) then 181 let 182 val (b1,b2) = dest_union b; 183 val (finite_thm1, card_thm1) = BAG_CARD_CONV___FINITE b1; 184 val (finite_thm2, card_thm2) = BAG_CARD_CONV___FINITE b2; 185 val finite_thm12 = CONJ finite_thm1 finite_thm2 186 187 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION)) 188 finite_thm12 189 val card_thm' = MP (ISPECL [b1,b2] bagTheory.BAG_CARD_UNION) finite_thm12 190 val card_thm'' = CONV_RULE (RHS_CONV ( 191 ((RATOR_CONV o RAND_CONV) (K card_thm1)) THENC 192 ((RAND_CONV) (K card_thm2)))) card_thm' 193 in 194 (finite_thm, eval_num_RULE card_thm'') 195 end 196 else 197 let 198 val (e,b') = dest_insert b; 199 val (finite_thm, card_thm) = BAG_CARD_CONV___FINITE b'; 200 201 val finite_thm2 = SPEC e (MP (ISPEC b' bagTheory.FINITE_BAG_INSERT) finite_thm); 202 val card_thm' = MP (ISPECL [b',e] card_insert_thm) finite_thm 203 val card_thm2 = CONV_RULE (RHS_CONV ( 204 (RATOR_CONV o RAND_CONV) (K card_thm))) card_thm' 205 in 206 (finite_thm2, eval_num_RULE card_thm2) 207 end 208 ) handle HOL_ERR _ => raise UNCHANGED; 209in 210 fun BAG_CARD_CONV tm = 211 let 212 val b = dest_card tm 213 val (_, thm) = BAG_CARD_CONV___FINITE b 214 in 215 thm 216 end; 217end 218 219 220(******************************************************************************) 221(* GET_BAG_IN_THMS *) 222(* *) 223(* Generates BAG_IN theorems for all elements of very simple bags that *) 224(* consists of repeatedly inserting elements into the empty bag. *) 225(* show that they are finite. *) 226(* *) 227(* For example: *) 228(* GET_BAG_IN_THMS ``{|x0; x1; x2|}`` results in *) 229(* *) 230(* [ |- BAG_IN x0 {|x0; x1; x2|}, *) 231(* |- BAG_IN x1 {|x0; x1; x2|}, *) 232(* |- BAG_IN x2 {|x0; x1; x2|}] *) 233(* *) 234(******************************************************************************) 235 236local 237 val BAG_EVERY_BAG_IN_THM = prove ( 238 ``!b:'a -> num. BAG_EVERY (\e. BAG_IN e b) b``, 239 REWRITE_TAC [bagTheory.BAG_EVERY] THEN 240 BETA_TAC THEN REWRITE_TAC[]) 241 242 val BAG_EVERY_STEP_CONV = (PART_MATCH lhs (CONJUNCT2 bagTheory.BAG_EVERY_THM)) 243 244 fun BAG_EVERY_TO_LIST l thm = 245 let 246 val thm0 = CONV_RULE BAG_EVERY_STEP_CONV thm 247 val thm1 = BETA_RULE (CONJUNCT1 thm0) 248 in 249 BAG_EVERY_TO_LIST (thm1::l) (CONJUNCT2 thm0) 250 end handle HOL_ERR _ => rev l 251in 252 fun GET_BAG_IN_THMS b = 253 BAG_EVERY_TO_LIST [] (ISPEC b BAG_EVERY_BAG_IN_THM) 254end; 255 256 257 258 259(******************************************************************************) 260(* GET_PRED_PAIR_LIST *) 261(* *) 262(* Given two bag that just consists of INSERTS and EMPTY_BAG, this functions *) 263(* destructs these bags and searches for pairs of elements that satisfy *) 264(* a given predicate. It returns two lists of element numbers that represent *) 265(* the positions of the found pairs. These lists are suitable to be given to *) 266(* BAG_RESORT_CONV. This function is useful to find pairs and sort them to *) 267(* the front of two bags. It is for example used by SUB_BAG_INSERT_CANCEL_CONV*) 268(******************************************************************************) 269 270local 271fun find_pairs p nl1 nl2 n [] l2 = (rev nl1, rev nl2) 272 | find_pairs p nl1 nl2 n (e::l1) l2 = 273 let 274 val found_opt = first_opt (fn n2 => fn e2 => 275 if (not (mem n2 nl2)) andalso (p e e2) then 276 SOME n2 277 else NONE) l2 278 val (nl1', nl2') = if isSome found_opt then 279 (n::nl1, (valOf found_opt)::nl2) else (nl1, nl2) 280 in 281 find_pairs p nl1' nl2' (n+1) l1 l2 282 end; 283in 284 fun get_resort_lists___pred_pair p b1 b2 = 285 let 286 val l1 = fst (strip_insert b1); 287 val l2 = fst (strip_insert b2); 288 in 289 find_pairs p [] [] 0 l1 l2 290 end 291end; 292 293fun get_resort_positions___pred_pair P b1 b2 = 294let 295 val l1 = fst (strip_insert b1); 296 val l2 = fst (strip_insert b2); 297 298 val found_opt = first_opt (fn n1 => fn e1 => 299 SOME (n1, valOf (first_opt ( 300 fn n2 => fn e2 => if (P e1 e2) then SOME n2 else NONE) l2))) l1 301in 302 found_opt 303end; 304 305local 306 fun get_resort_list___pred_int p n nL [] = rev nL 307 | get_resort_list___pred_int p n nL (t::ts) = 308 let val nL' = if (p t) then (n::nL) else nL in 309 get_resort_list___pred_int p (n+1) nL' ts 310 end 311in 312 fun get_resort_list___pred p t = 313 let 314 val tl = fst (strip_insert t) 315 in 316 get_resort_list___pred_int p 0 [] tl 317 end 318end; 319 320fun get_resort_position___pred p t = 321 first_opt (fn n => fn e => if (p e) then SOME n else NONE) (fst (strip_insert t)); 322 323 324 325 326 327 328(******************************************************************************) 329(* SUB_BAG_INSERT_CANCEL_CONV *) 330(* *) 331(* Eleminates common elements from the two heaps. While bagSimps.CANCEL_CONV *) 332(* eliminates common parts joined with BAG_UNION, this conversion handles *) 333(* BAG_INSERT. *) 334(* *) 335(* For example: *) 336(* SUB_BAG_INSERT_CANCEL_CONV ``SUB_BAG {|x1;x0;x2'|} {|x0;x1;x2;x3|}`` *) 337(* results in *) 338(* *) 339(* |- SUB_BAG {|x1;x0;x2'|} {|x0;x1;x2;x3|} = *) 340(* SUB_BAG {| x2'|} {| x2;x3|} = *) 341(* *) 342(******************************************************************************) 343local 344 val sub_bag_empty1 = prove ( 345 ``!b:'a->num. SUB_BAG EMPTY_BAG b = T``, REWRITE_TAC [bagTheory.SUB_BAG_EMPTY]) 346 val sub_bag_empty2 = CONJUNCT2 bagTheory.SUB_BAG_EMPTY; 347 val sub_bag_refl = prove ( 348 ``!b:'a -> num. SUB_BAG b b = T``, REWRITE_TAC [bagTheory.SUB_BAG_REFL]) 349 350 val conv2 = TRY_CONV (PART_MATCH lhs bagTheory.SUB_BAG_INSERT) 351 val conv3 = TRY_CONV (PART_MATCH lhs sub_bag_empty1) 352 val conv4 = TRY_CONV (PART_MATCH lhs sub_bag_empty2) 353 val conv5 = TRY_CONV (PART_MATCH lhs sub_bag_refl) 354in 355 356fun SUB_BAG_INSERT_CANCEL_CONV tm = 357 let 358 val (b1,b2) = bagSyntax.dest_sub_bag tm 359 val (n1L,n2L) = get_resort_lists___pred_pair aconv b1 b2 360 val _ = if null n1L then raise UNCHANGED else (); 361 362 val conv1 = ((RATOR_CONV o RAND_CONV) 363 (BAG_RESORT_CONV n1L)) THENC 364 (RAND_CONV 365 (BAG_RESORT_CONV n2L)) 366 in 367 (conv1 THENC REPEATC conv2 THENC conv3 THENC conv4 THENC conv5) tm 368 end handle HOL_ERR _ => raise UNCHANGED; 369end 370 371 372(******************************************************************************) 373(* BAG_DIFF_INSERT_CANCEL_CONV *) 374(* *) 375(* Eleminates common elements from the two heaps. While bagSimps.CANCEL_CONV *) 376(* eliminates common parts joined with BAG_UNION, this conversion handles *) 377(* BAG_INSERT. *) 378(* *) 379(* For example: *) 380(* BAG_DIFF_INSERT_CANCEL_CONV ``BAG_DIFF {|x0;x1;x2;x3|} {|x1;x0;x2'|}`` *) 381(* results in *) 382(* *) 383(* |- BAG_DIFF {|x0;x1;x2;x3|} {|x1;x0;x2'|} = *) 384(* BAG_DIFF {| x2;x3|} {| x2'|} *) 385(* *) 386(* The empty bag is removed as a parameter of diff as well, so *) 387(* BAG_DIFF_INSERT_CANCEL_CONV ``BAG_DIFF {|x0;x1;x2;x3|} {|x1;x0;x2|}`` *) 388(* results in *) 389(* *) 390(* |- BAG_DIFF {|x0;x1;x2;x3|} {|x1;x0;x2|} = *) 391(* {| x3|} *) 392(******************************************************************************) 393 394local 395 val empty_thmL = CONJUNCTS bagTheory.BAG_DIFF_EMPTY 396 val empty_thm1 = el 2 empty_thmL 397 val empty_thm2 = el 3 empty_thmL 398in 399fun BAG_DIFF_INSERT_CANCEL_CONV tm = 400 let 401 val (b1,b2) = bagSyntax.dest_diff tm 402 val (n1L,n2L) = get_resort_lists___pred_pair aconv b1 b2 403 val _ = if null n1L andalso not (bagSyntax.is_empty b1) 404 andalso not (bagSyntax.is_empty b2) then raise UNCHANGED else (); 405 406 val conv1 = ((RATOR_CONV o RAND_CONV) 407 (BAG_RESORT_CONV n1L)) THENC 408 (RAND_CONV 409 (BAG_RESORT_CONV n2L)) 410 val conv2 = PART_MATCH lhs bagTheory.BAG_DIFF_INSERT_same 411 val conv3 = TRY_CONV (PART_MATCH lhs empty_thm1) 412 val conv4 = TRY_CONV (PART_MATCH lhs empty_thm2) 413 414 in 415 (conv1 THENC REPEATC conv2 THENC conv3 THENC conv4) tm 416 end handle HOL_ERR _ => raise UNCHANGED; 417end 418 419 420 421 422 423(******************************************************************************) 424(* SIMPLE_BAG_NORMALISE_CONV *) 425(* *) 426(* Combines the conversions for BAG_IMAGE, BAG_DIFF und simplifacations for *) 427(* BAG_UNION to simplifiy bags. The goal is to get a simple bag as the reuslt.*) 428(******************************************************************************) 429 430local 431 val empty_thmL = CONJUNCTS bagTheory.BAG_DIFF_EMPTY 432 val empty_thm1 = el 2 empty_thmL 433 val empty_thm2 = el 3 empty_thmL 434 435 fun BIN_OP_CONV c = 436 RAND_CONV c THENC (RATOR_CONV o RAND_CONV) c 437 438 val bag_union_insert_thmL = CONJUNCTS ( 439 CONV_RULE (DEPTH_CONV FORALL_AND_CONV) bagTheory.BAG_UNION_INSERT) 440 val bag_union_empty_thmL = CONJUNCTS bagTheory.BAG_UNION_EMPTY 441 442 val bag_union_thm1a = el 1 bag_union_insert_thmL 443 val bag_union_thm1b = el 2 bag_union_empty_thmL 444 val bag_union_thm2a = el 2 bag_union_insert_thmL 445 val bag_union_thm2b = el 1 bag_union_empty_thmL 446 447 val bag_union_conv_step = 448 FIRST_CONV [ 449 PART_MATCH lhs bag_union_thm2b, 450 PART_MATCH lhs bag_union_thm1a, 451 PART_MATCH lhs bag_union_thm1b, 452 PART_MATCH lhs bag_union_thm2a] 453 454 fun bag_union_conv tm = 455 (bag_union_conv_step THENC 456 TRY_CONV (RAND_CONV bag_union_conv)) tm 457 458in 459fun SIMPLE_BAG_NORMALISE_CONV tm = 460 if bagSyntax.is_union tm then 461 ((BIN_OP_CONV SIMPLE_BAG_NORMALISE_CONV) THENC 462 bag_union_conv) tm 463 else if (bagSyntax.is_diff tm) then 464 ((BIN_OP_CONV SIMPLE_BAG_NORMALISE_CONV) THENC 465 BAG_DIFF_INSERT_CANCEL_CONV) tm 466 else if (bagSyntax.is_insert tm) then 467 RAND_CONV SIMPLE_BAG_NORMALISE_CONV tm 468 else if (bagSyntax.is_image tm) then 469 ((RAND_CONV SIMPLE_BAG_NORMALISE_CONV) THENC 470 BAG_IMAGE_CONV) tm 471 else raise UNCHANGED; 472end 473 474 475 476(******************************************************************************) 477(* BAG_EQ_INSERT_CANCEL_CONV *) 478(******************************************************************************) 479 480local 481 val bag_card_eq_thm = prove ( 482 ``!(b1:'a -> num) b2. ~(BAG_CARD b1 = BAG_CARD b2) ==> ((b1 = b2) = F)``, 483 REPEAT GEN_TAC THEN Cases_on `b1 = b2` THEN ASM_REWRITE_TAC[]) 484in 485fun BAG_EQ_INSERT_CANCEL_CONV tm = 486 let 487 val (b1,b2) = dest_eq tm 488 val b1_thm = SIMPLE_BAG_NORMALISE_CONV b1 handle UNCHANGED => REFL b1 489 val b2_thm = SIMPLE_BAG_NORMALISE_CONV b2 handle UNCHANGED => REFL b2 490 491 val b1' = rhs (concl b1_thm) 492 val b2' = rhs (concl b2_thm) 493 494 val thm_simp = ((RAND_CONV (K b2_thm)) THENC 495 ((RATOR_CONV o RAND_CONV) (K b1_thm))) tm 496 497 val (b1L,b1_rest) = strip_insert b1' 498 val (b2L,b2_rest) = strip_insert b2' 499 in 500 if (not (length b1L = length b2L) andalso 501 (bagSyntax.is_empty b1_rest) andalso 502 (bagSyntax.is_empty b2_rest)) then 503 let 504 val thm0 = ISPECL [b1',b2'] bag_card_eq_thm 505 val precond = (fst o dest_imp o concl) thm0; 506 507 val precond_thm = EQT_ELIM ( 508 ((DEPTH_CONV BAG_CARD_CONV) THENC 509 numLib.REDUCE_CONV) precond) 510 val thm1 = MP thm0 precond_thm 511 in 512 TRANS thm_simp thm1 513 end else let 514 val (n1L,n2L) = get_resort_lists___pred_pair aconv b1' b2' 515 val _ = if null n1L then raise UNCHANGED else (); 516 val conv1 = ((RATOR_CONV o RAND_CONV) 517 (BAG_RESORT_CONV n1L)) THENC 518 (RAND_CONV (BAG_RESORT_CONV n2L)) 519 val conv2 = PART_MATCH lhs bagTheory.BAG_INSERT_ONE_ONE 520 fun conv3 t = let 521 val (t1,t2) = dest_eq t; 522 val _ = if (aconv t1 t2) then () else raise UNCHANGED; 523 in 524 EQT_INTRO (REFL t1) 525 end handle HOL_ERR _ => raise UNCHANGED; 526 in 527 CONV_RULE (RHS_CONV 528 (conv1 THENC REPEATC conv2 THENC conv3)) thm_simp 529 end 530 end handle HOL_ERR _ => raise UNCHANGED; 531end 532 533 534(******************************************************************************) 535(* SUB_BAG_INSERT_SOLVE *) 536(* *) 537(* Calls SUB_BAG_INSERT_CANCEL_CONV and assumes that the left heap becomes *) 538(* emty. It then tries to apply SUB_BAG_EMPTY *) 539(* *) 540(******************************************************************************) 541 542local 543 val empty_thm = CONJUNCT1 bagTheory.SUB_BAG_EMPTY 544in 545 fun SUB_BAG_INSERT_SOLVE tm = 546 let 547 val _ = if bagSyntax.is_sub_bag tm then () else Feedback.fail(); 548 549 val thm0 = (RAND_CONV SIMPLE_BAG_NORMALISE_CONV THENC 550 (RATOR_CONV o RAND_CONV) SIMPLE_BAG_NORMALISE_CONV) tm 551 handle UNCHANGED => REFL tm 552 553 554 val thm1 = CONV_RULE (RHS_CONV SUB_BAG_INSERT_CANCEL_CONV) thm0 555 in 556 EQT_ELIM thm1 557 end; 558end; 559 560 561end; 562