1(*****************************************************************************) 2(* FILE : tautLib.sml *) 3(* DESCRIPTION : Boolean tautology checking (by SAT solver proof replay) *) 4(* *) 5(* READS FILES : Temporary files output by SAT solver. Deleted. *) 6(* WRITES FILES : Temporary input file to solver. Deleted. *) 7(*****************************************************************************) 8 9structure tautLib :> tautLib = 10struct 11 12open HolKernel Parse boolLib Abbrev boolSyntax HolSatLib 13 14val ERR = mk_HOL_ERR "tautLib" 15 16 17(*--------------------------------------------------------------------------- 18 Set the parsers to a fixed grammar for the duration of this file. 19 ---------------------------------------------------------------------------*) 20 21(* Fix the grammar used by this file *) 22structure Parse = struct 23 open Parse 24 val (Type,Term) = parse_from_grammars boolTheory.bool_grammars 25end 26open Parse 27 28 29(*===========================================================================*) 30(* Discriminator functions for T (true) and F (false) *) 31(*===========================================================================*) 32 33fun is_T tm = same_const tm T 34fun is_F tm = same_const tm F 35 36(*---------------------------------------------------------------------------*) 37(* TAUT_CHECK_CONV : conv *) 38(* *) 39(* Given a propositional term with all variables universally quantified, *) 40(* e.g. `!x1 ... xn. f[x1,...,xn]`, this conversion proves the term to be *) 41(* either true or false, i.e. it returns one of: *) 42(* *) 43(* |- (!x1 ... xn. f[x1,...,xn]) = T *) 44(* |- (!x1 ... xn. f[x1,...,xn]) = F *) 45(*---------------------------------------------------------------------------*) 46 47fun TAUT_CHECK_CONV tm = 48 let val (vars,tm') = strip_forall tm 49 in EQT_INTRO (GENL vars (SAT_PROVE tm')) end 50 handle HolSatLib.SAT_cex th => 51 let val (vars,tm') = strip_forall tm 52 val g = list_mk_exists(vars,mk_neg tm') 53 val cxm = List.foldl (fn (v, cxm) => 54 if is_neg v then Redblackmap.insert (cxm, dest_neg v, F) 55 else Redblackmap.insert (cxm, v, T)) 56 (Redblackmap.mkDict Term.compare) 57 (strip_conj (fst (dest_imp (concl th)))) 58 val cex = List.map (fn v => Redblackmap.find (cxm, v) 59 handle NotFound => T) vars 60 val th1 = prove(g, MAP_EVERY EXISTS_TAC cex THEN REWRITE_TAC []) 61 val th2 = CONV_RULE (REPEATC (LAST_EXISTS_CONV EXISTS_NOT_CONV)) th1 62 in EQF_INTRO th2 end 63 handle HOL_ERR _ => raise ERR "TAUT_CHECK_CONV" "" 64 65(*---------------------------------------------------------------------------*) 66(* PTAUT_CONV : conv *) 67(* *) 68(* Given a propositional term with all variables universally quantified, *) 69(* e.g. `!x1 ... xn. f[x1,...,xn]`, this conversion proves the term to be *) 70(* either true or false, i.e. it returns one of: *) 71(* *) 72(* |- (!x1 ... xn. f[x1,...,xn]) = T *) 73(* |- (!x1 ... xn. f[x1,...,xn]) = F *) 74(* *) 75(* It accepts propositional terms that are not fully universally quantified. *) 76(* However, for such a term, the conversion will fail if it is not true. *) 77(* Consider the term `!x2 ... xn. f[x1,...,xn]`. TAUT_CHECK_CONV proves *) 78(* one of: *) 79(* *) 80(* |- (!x1 ... xn. f[x1,...,xn]) = T *) 81(* |- (!x1 ... xn. f[x1,...,xn]) = F *) 82(* *) 83(* The former can be manipulated as follows: *) 84(* *) 85(* |- (!x1 ... xn. f[x1,...,xn]) = T *) 86(* |- !x1 ... xn. f[x1,...,xn] *) 87(* |- !x2 ... xn. f[x1,...,xn] *) 88(* |- (!x2 ... xn. f[x1,...,xn]) = T *) 89(* *) 90(* However when the fully quantified term is false, we have: *) 91(* *) 92(* |- (!x1 ... xn. f[x1,...,xn]) = F *) 93(* |- ~(!x1 ... xn. f[x1,...,xn]) *) 94(* |- ?x1. ~(!x2 ... xn. f[x1,...,xn]) *) 95(* |- ?x1. ((!x2 ... xn. f[x1,...,xn]) = F) *) 96(* *) 97(* whereas we want: *) 98(* *) 99(* |- !x1. ((!x2 ... xn. f[x1,...,xn]) = F) *) 100(* *) 101(* i.e., *) 102(* *) 103(* |- (!x2 ... xn. f[x1,...,xn]) = F *) 104(* *) 105(* The conversions given here are not capable of proving the latter theorem *) 106(* since it is not purely propositional. *) 107(*---------------------------------------------------------------------------*) 108 109fun PTAUT_CONV tm = 110 let val vars = free_vars tm 111 val th = TAUT_CHECK_CONV (list_mk_forall (vars,tm)) 112 in if null vars then th else 113 if is_F (rhs (concl th)) 114 then raise ERR "PTAUT_CONV" "false for at least one interpretation" 115 else (EQT_INTRO o (SPECL vars) o EQT_ELIM) th 116 end 117 118(*---------------------------------------------------------------------------*) 119(* PTAUT_TAC : tactic *) 120(* *) 121(* Tactic for solving propositional terms. *) 122(*---------------------------------------------------------------------------*) 123 124val PTAUT_TAC = CONV_TAC PTAUT_CONV 125 126(*---------------------------------------------------------------------------*) 127(* PTAUT_PROVE : term -> thm *) 128(* *) 129(* Given a propositional term `t`, this function returns the theorem |- t if *) 130(* `t` is a tautology. Otherwise it fails. *) 131(*---------------------------------------------------------------------------*) 132 133fun PTAUT_PROVE tm = 134 EQT_ELIM (PTAUT_CONV tm) 135 handle e => raise (wrap_exn "tautLib" "PTAUT_PROVE" e) 136 137(*===========================================================================*) 138(* Tautology checking including instances of propositional tautologies *) 139(*===========================================================================*) 140 141(* ---------------------------------------------------------------------- 142 non_prop_terms : term -> term set 143 144 Computes a set of subterms of a term that are either variables or 145 Boolean valued non-propositional terms. 146 ---------------------------------------------------------------------- *) 147local 148open Rsyntax 149in 150fun non_prop_terms tm = let 151 fun non_prop_args acc tmlist = 152 case tmlist of 153 [] => acc 154 | tm::ts => let 155 val (opp,args) = ((#Name o dest_const) ## I) (strip_comb tm) 156 handle HOL_ERR _ => ("", []) 157 in 158 if mem opp ["T","F","~","/\\","\\/","==>"] then 159 non_prop_args acc (args @ ts) 160 else if mem opp ["=","COND"] andalso 161 all (fn t => type_of t = bool) args 162 then 163 non_prop_args acc (args @ ts) 164 else if type_of tm = bool then 165 non_prop_args (HOLset.add(acc, tm)) ts 166 else raise ERR "non_prop_terms" "Not a boolean term" 167 end 168in 169 non_prop_args empty_tmset [tm] 170end 171end 172 173(*---------------------------------------------------------------------------*) 174(* TAUT_CONV : conv *) 175(* *) 176(* Given a term, `t`, that is a valid propositional formula or valid instance*) 177(* of a propositional formula, this conversion returns the theorem |- t = T. *) 178(* The variables in `t` do not have to be universally quantified. *) 179(* *) 180(* Example: *) 181(* *) 182(* TAUT_CONV `!x n y z. x \/ ~(n < 0) \/ y \/ z \/ (n < 0)` ---> *) 183(* |- (!x n y z. x \/ ~n < 0 \/ y \/ z \/ n < 0) = T *) 184(*---------------------------------------------------------------------------*) 185 186fun TAUT_CONV tm = 187 let val (univs,tm') = strip_forall tm 188 val insts = HOLset.listItems (non_prop_terms tm') 189 val vars = map (fn t => genvar bool) insts 190 val theta = map2 (curry (op |->)) insts vars 191 val tm'' = list_mk_forall (vars,subst theta tm') 192 in EQT_INTRO (GENL univs (SPECL insts (PTAUT_PROVE tm''))) 193 end 194 handle e => raise (wrap_exn "tautLib" "TAUT_CONV" e) 195 196(*---------------------------------------------------------------------------*) 197(* TAUT_TAC : tactic *) 198(* *) 199(* Tactic for solving propositional formulae and instances of propositional *) 200(* formulae. *) 201(*---------------------------------------------------------------------------*) 202 203val TAUT_TAC = CONV_TAC TAUT_CONV 204 205(*---------------------------------------------------------------------------*) 206(* ASM_TAUT_TAC : tactic *) 207(* *) 208(* Same as TAUT_TAC, except that it takes the assumptions of the goal into *) 209(* account. *) 210(*---------------------------------------------------------------------------*) 211 212val ASM_TAUT_TAC = REPEAT (POP_ASSUM MP_TAC) THEN TAUT_TAC 213 214(*---------------------------------------------------------------------------*) 215(* TAUT_PROVE : term -> thm *) 216(* *) 217(* Given a valid propositional formula, or a valid instance of a *) 218(* propositional formula, `t`, this function returns the theorem |- t. *) 219(*---------------------------------------------------------------------------*) 220 221fun TAUT_PROVE tm = 222 EQT_ELIM (TAUT_CONV tm) handle HOL_ERR _ => raise ERR "TAUT_PROVE" "" 223 224fun TAUT q = TAUT_PROVE (Term q) 225 226end (* tautLib *) 227