1(* non-interactive mode
2*)
3structure boolContext :> boolContext =
4struct
5open HolKernel Parse boolLib;
6
7(* interactive mode
8if !show_assums then () else
9 (loadPath := ".."::"../../prob"::(!loadPath);
10  load "bossLib";
11  load "pred_setTheory";
12  load "millerTools";
13  load "miller_extraTheory";
14  show_assums := true);
15*)
16
17open pairTheory pred_setTheory
18     res_quanTheory HurdUseful ho_proverTools res_quanTools subtypeTools
19     subtypeTheory;
20
21infixr 0 ++ || ORELSEC ## THENC THEN_TCL ORELSE_TCL;
22infix 1 >>;
23nonfix THEN THENL ORELSE;
24
25val op++ = op THEN;
26val op|| = op ORELSE;
27val op>> = op THEN1;
28
29(* --------------------------------------------------------------------- *)
30(* Subtype checking.                                                     *)
31(* --------------------------------------------------------------------- *)
32
33val bool_sc =
34  map SC_SIMPLIFICATION
35  [PAIR_UNIV, FUNSET_DFUNSET, IN_INTER, IN_UNION, IN_COMPL, SUBSET_INTER,
36   SUBSET_K, K_SUBSET] @
37  map SC_JUDGEMENT
38  [IN_UNIV, IN_PAIR, SUBSET_THM] @
39  map SC_SUBTYPE
40  [DEFAULT_SUBTYPE, COMB_SUBTYPE, ABS_SUBTYPE,
41   COND_SUBTYPE, RES_ABSTRACT_SUBTYPE, UNCURRY_SUBTYPE];
42
43(* --------------------------------------------------------------------- *)
44(* Contextual rewriting.                                                 *)
45(* --------------------------------------------------------------------- *)
46
47(* Rules *)
48
49val forall_rule = pattern_rule (``!x. P x``, wrap o var_GENVAR_SPEC);
50
51val conj_rule = pattern_rule (``a /\ b``, var_CONJUNCTS);
52
53val res_forall_rule =
54  pattern_rule (``!x :: P. M x``, wrap o (I ## CONV_RULE RES_FORALL_CONV));
55
56(* Rewrites *)
57
58val beta_rewr = pattern_rewr (``(\x. (y : 'a -> 'b) x) z``, K (K BETA_CONV));
59val neg_t_rewr =
60  pattern_rewr (``~T``, K (K (REWR_CONV (ho_PROVE [] ``~T = F``))));
61val neg_f_rewr =
62  pattern_rewr (``~F``, K (K (REWR_CONV (ho_PROVE [] ``~F = T``))));
63
64val basic_bool_rewrs =
65  map (prove o add_snd (ho_PROVE_TAC []))
66  [``!a:bool. ~~a = a``,
67   ``!a. (a = T) = a``,
68   ``!a. (a = F) = ~a``,
69   ``!a. (T = a) = a``,
70   ``!a. (F = a) = ~a``,
71   ``!a : bool. (a = ~a) = F``,
72   ``!a : bool. (~a = a) = F``,
73   ``!a. F /\ a = F``,
74   ``!a. a /\ F = F``,
75   ``!a. T /\ a = a``,
76   ``!a. a /\ T = a``,
77   ``!a. a /\ a = a``,
78   ``!a. ~a /\ a = F``,
79   ``!a. a /\ ~a = F``,
80   ``!a. T \/ a = T``,
81   ``!a. a \/ T = T``,
82   ``!a. F \/ a = a``,
83   ``!a. a \/ F = a``,
84   ``!a. a \/ a = a``,
85   ``!a. ~a \/ a = T``,
86   ``!a. a \/ ~a = T``,
87   ``!a b. ~(a \/ b) = ~a /\ ~b``,
88   ``!a. a ==> a = T``,
89   ``!a. a ==> T = T``,
90   ``!a. a ==> F = ~a``,
91   ``!a. T ==> a = a``,
92   ``!a. F ==> a = T``,
93   ``!a b. ~(a ==> b) = a /\ ~b``,
94   ``!a : 'a. (a = a) = T``,
95   ``!a b : bool. (~a = ~b) = (a = b)``,
96   ``!(a : 'a) b. (if T then a else b) = a``,
97   ``!(a : 'a) b. (if F then a else b) = b``,
98   ``!p. ~(!x. p x) = ?x. ~p x``,
99   ``!p. ~(?x. p x) = !x. ~p x``,
100   ``!p. (!(x : 'a). p) = p``,
101   ``!p. (?(x : 'a). p) = p``];
102
103(* The precontext *)
104
105val bool_pc = precontext_add
106  ("bool",
107   map C_RULE
108   [forall_rule, conj_rule, res_forall_rule] @
109   map C_CONG
110   [comb_cong, abs_cong, conj_cong, disj_cong, imp_cong, cond_cong,
111    res_forall_cong, res_exists_cong, res_select_cong, res_abstract_cong,
112    uncurry_cong] @
113   map C_REWR
114   [beta_rewr, neg_t_rewr, neg_f_rewr] @
115   map C_THM
116   [PAIRED_BETA_THM, FST, SND, CLOSED_PAIR_EQ,
117    RES_ABSTRACT_IDEMPOT, RES_ABSTRACT, IN_UNIV, NOT_IN_EMPTY, IN_SING,
118    EMPTY_FUNSET, FUNSET_EMPTY, RES_FORALL_EMPTY,
119    RES_EXISTS_EMPTY, RES_SELECT_EMPTY, RES_EXISTS_UNIQUE_EMPTY,
120    RES_FORALL_UNIV, RES_EXISTS_UNIV, RES_SELECT_UNIV, RES_EXISTS_UNIQUE_UNIV,
121    RES_FORALL_NULL, RES_EXISTS_NULL, RES_EXISTS_UNIQUE_NULL] @
122   map C_THM basic_bool_rewrs @
123   map C_SUBTYPE bool_sc)
124  empty_precontext;
125
126(* The context *)
127
128val bool_c = precontext_compile bool_pc;
129
130(*
131try prove
132(``!p. ((!x. p x) = T) ==> !y. p y``,
133 SIMPLIFY_TAC bool_c []);
134
135reset_traces ();
136allow_trace "SIMPLIFY_TYPECHECK: (tm, res)";
137
138try prove (``!x. ~x \/ ~~x``, SIMPLIFY_TAC bool_c []);
139
140try prove (``!a :: p. (\x :: p. T) a``, SIMPLIFY_TAC bool_c []);
141*)
142
143(* non-interactive mode
144*)
145end;
146