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