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