1(* non-interactive mode
2*)
3open HolKernel Parse boolLib;
4val _ = new_theory "extra_bool";
5
6(* interactive mode
7show_assums := true;
8loadPath := union ["../finished"] (!loadPath);
9app load
10  ["bossLib", "arithmeticTheory", "dividesTheory", "gcdTheory",
11   "primeTheory", "res_quan2Theory", "pred_setTheory", "subtypeTheory",
12   "res_quanTools", "subtypeTools", "ho_proverTools", "numContext",
13   "millerTools", "extra_numTheory", "ho_basicTools",
14   "prob_extraTheory"];
15installPP subtypeTools.pp_precontext;
16installPP subtypeTools.pp_context;
17*)
18
19open bossLib res_quanTheory pred_setTheory subtypeTheory
20     res_quanTools subtypeTools ho_proverTools HurdUseful
21     ho_basicTools boolContext combinTheory;
22
23infixr 0 ++ << || THENC ORELSEC ORELSER ##;
24infix 1 >>;
25
26val !! = REPEAT;
27val op++ = op THEN;
28val op<< = op THENL;
29val op|| = op ORELSE;
30val op>> = op THEN1;
31
32(* ------------------------------------------------------------------------- *)
33(* Tools.                                                                    *)
34(* ------------------------------------------------------------------------- *)
35
36val S_TAC = !! (POP_ASSUM MP_TAC) ++ !! RESQ_STRIP_TAC;
37
38val (R_TAC, AR_TAC, R_TAC', AR_TAC') = SIMPLIFY_TACS bool_c;
39
40val Strip = S_TAC;
41val Simplify = R_TAC;
42val Suff = SUFF_TAC;
43val Know = KNOW_TAC;
44
45(* ------------------------------------------------------------------------- *)
46(* Definitions.                                                              *)
47(* ------------------------------------------------------------------------- *)
48
49(* ------------------------------------------------------------------------- *)
50(* Theorems.                                                                 *)
51(* ------------------------------------------------------------------------- *)
52
53val RAND_THM = store_thm
54  ("RAND_THM",
55   ``!f x y. (x = y) ==> (f x = f y)``,
56   RW_TAC std_ss []);
57
58val K_PARTIAL = store_thm
59  ("K_PARTIAL",
60   ``!x. K x = \z. x``,
61   RW_TAC std_ss [K_DEF]);
62
63val SELECT_EXISTS_UNIQUE = store_thm
64  ("SELECT_EXISTS_UNIQUE",
65   ``!P n. $? P /\ (!m. P m ==> (m = n)) ==> ($@ P = n)``,
66   RW_TAC std_ss [boolTheory.EXISTS_DEF]);
67
68val CONJ_EQ_IMP = store_thm
69  ("CONJ_EQ_IMP",
70   ``!a b c. (a ==> (b = c)) ==> (a /\ b = a /\ c)``,
71   PROVE_TAC []);
72
73(* non-interactive mode
74*)
75val _ = export_theory ();
76