1(* ------------------------------------------------------------------------- *) 2(* Some miscellaneous tools that come in useful in the probability *) 3(* development. *) 4(* ------------------------------------------------------------------------- *) 5 6structure extra_pred_setTools :> extra_pred_setTools = 7struct 8 9open HolKernel Parse boolLib; 10open bossLib pred_setTheory HurdUseful subtypeTheory extra_pred_setTheory; 11 12infixr 0 ++ || ORELSEC ## THENC -->; 13infix 1 >> |->; 14nonfix THEN ORELSE; 15 16val op++ = op THEN; 17val op|| = op ORELSE; 18val op>> = op THEN1; 19 20(* ------------------------------------------------------------------------- *) 21(* Set simplification. *) 22(* ------------------------------------------------------------------------- *) 23 24val set_rewrs 25 = [INTER_EMPTY, INTER_UNIV, UNION_EMPTY, UNION_UNIV, DISJOINT_UNION, 26 DISJOINT_INSERT, DISJOINT_EMPTY, GSYM DISJOINT_EMPTY_REFL, 27 DISJOINT_BIGUNION, INTER_SUBSET, INTER_IDEMPOT, UNION_IDEMPOT, 28 SUBSET_UNION]; 29 30val elt_rewrs 31 = [SUBSET_DEF, IN_COMPL, IN_DIFF, IN_UNIV, NOT_IN_EMPTY, IN_UNION, 32 IN_INTER, IN_IMAGE, IN_FUNSET, IN_DFUNSET, GSPECIFICATION, 33 DISJOINT_DEF, IN_BIGUNION, IN_BIGINTER, IN_COUNT, IN_o, 34 IN_UNIONL, IN_DELETE, IN_PREIMAGE, IN_SING, IN_INSERT]; 35 36fun rewr_ss ths = 37 simpLib.++ 38 (std_ss, 39 simpLib.SSFRAG 40 {ac = [], 41 name = NONE, 42 convs = [], 43 dprocs = [], 44 filter = NONE, 45 rewrs = set_rewrs @ elt_rewrs, 46 congs = []}); 47 48val pset_set_ss = rewr_ss set_rewrs; 49val pset_elt_ss = rewr_ss elt_rewrs; 50val pset_ss = rewr_ss (set_rewrs @ elt_rewrs); 51 52fun PSET_TAC ths = 53 REPEAT (POP_ASSUM MP_TAC) 54 ++ RW_TAC pset_set_ss ths 55 ++ REPEAT (POP_ASSUM MP_TAC) 56 ++ RW_TAC pset_elt_ss ths; 57 58end; 59