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