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