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