more standard file/module names;
authorwenzelm
Sat Feb 01 21:09:53 2014 +0100 (2014-02-01)
changeset 5523997921d23ebe3
parent 55237 1e341728bae9
child 55240 efc4c0e0e14a
more standard file/module names;
src/HOL/HOL.thy
src/HOL/SAT.thy
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/cnf.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/sat.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Feb 01 20:46:19 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Feb 01 21:09:53 2014 +0100
     1.3 @@ -1690,7 +1690,8 @@
     1.4  val trans = @{thm trans}
     1.5  *}
     1.6  
     1.7 -ML_file "Tools/cnf_funcs.ML"
     1.8 +ML_file "Tools/cnf.ML"
     1.9 +
    1.10  
    1.11  subsection {* Code generator setup *}
    1.12  
     2.1 --- a/src/HOL/SAT.thy	Sat Feb 01 20:46:19 2014 +0100
     2.2 +++ b/src/HOL/SAT.thy	Sat Feb 01 21:09:53 2014 +0100
     2.3 @@ -13,14 +13,12 @@
     2.4  
     2.5  ML_file "Tools/prop_logic.ML"
     2.6  ML_file "Tools/sat_solver.ML"
     2.7 -ML_file "Tools/sat_funcs.ML"
     2.8 +ML_file "Tools/sat.ML"
     2.9  
    2.10 -ML {* structure sat = SATFunc(cnf) *}
    2.11 -
    2.12 -method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
    2.13 +method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac) *}
    2.14    "SAT solver"
    2.15  
    2.16 -method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
    2.17 +method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac) *}
    2.18    "SAT solver (with definitional CNF)"
    2.19  
    2.20  end
     3.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Feb 01 20:46:19 2014 +0100
     3.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sat Feb 01 21:09:53 2014 +0100
     3.3 @@ -222,7 +222,7 @@
     3.4  
     3.5  fun to_definitional_cnf_with_quantifiers ctxt th =
     3.6    let
     3.7 -    val eqth = cnf.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
     3.8 +    val eqth = CNF.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
     3.9      val eqth = eqth RS @{thm eq_reflection}
    3.10      val eqth = eqth RS @{thm TruepropI}
    3.11    in Thm.equal_elim eqth th end
     4.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 20:46:19 2014 +0100
     4.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 21:09:53 2014 +0100
     4.3 @@ -245,7 +245,7 @@
     4.4    (if exists (Meson.has_too_many_clauses ctxt)
     4.5               (Logic.prems_of_goal (prop_of st0) 1) then
     4.6       Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1
     4.7 -     THEN cnf.cnfx_rewrite_tac ctxt 1
     4.8 +     THEN CNF.cnfx_rewrite_tac ctxt 1
     4.9     else
    4.10       all_tac) st0
    4.11  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/cnf.ML	Sat Feb 01 21:09:53 2014 +0100
     5.3 @@ -0,0 +1,579 @@
     5.4 +(*  Title:      HOL/Tools/cnf.ML
     5.5 +    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     5.6 +    Author:     Tjark Weber, TU Muenchen
     5.7 +
     5.8 +FIXME: major overlaps with the code in meson.ML
     5.9 +
    5.10 +Functions and tactics to transform a formula into Conjunctive Normal
    5.11 +Form (CNF).
    5.12 +
    5.13 +A formula in CNF is of the following form:
    5.14 +
    5.15 +    (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
    5.16 +    False
    5.17 +    True
    5.18 +
    5.19 +where each xij is a literal (a positive or negative atomic Boolean
    5.20 +term), i.e. the formula is a conjunction of disjunctions of literals,
    5.21 +or "False", or "True".
    5.22 +
    5.23 +A (non-empty) disjunction of literals is referred to as "clause".
    5.24 +
    5.25 +For the purpose of SAT proof reconstruction, we also make use of
    5.26 +another representation of clauses, which we call the "raw clauses".
    5.27 +Raw clauses are of the form
    5.28 +
    5.29 +    [..., x1', x2', ..., xn'] |- False ,
    5.30 +
    5.31 +where each xi is a literal, and each xi' is the negation normal form
    5.32 +of ~xi.
    5.33 +
    5.34 +Literals are successively removed from the hyps of raw clauses by
    5.35 +resolution during SAT proof reconstruction.
    5.36 +*)
    5.37 +
    5.38 +signature CNF =
    5.39 +sig
    5.40 +  val is_atom: term -> bool
    5.41 +  val is_literal: term -> bool
    5.42 +  val is_clause: term -> bool
    5.43 +  val clause_is_trivial: term -> bool
    5.44 +
    5.45 +  val clause2raw_thm: thm -> thm
    5.46 +  val make_nnf_thm: theory -> term -> thm
    5.47 +
    5.48 +  val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
    5.49 +
    5.50 +  val make_cnf_thm: Proof.context -> term -> thm
    5.51 +  val make_cnfx_thm: Proof.context -> term -> thm
    5.52 +  val cnf_rewrite_tac: Proof.context -> int -> tactic  (* converts all prems of a subgoal to CNF *)
    5.53 +  val cnfx_rewrite_tac: Proof.context -> int -> tactic
    5.54 +    (* converts all prems of a subgoal to (almost) definitional CNF *)
    5.55 +end;
    5.56 +
    5.57 +structure CNF : CNF =
    5.58 +struct
    5.59 +
    5.60 +val clause2raw_notE      = @{lemma "[| P; ~P |] ==> False" by auto};
    5.61 +val clause2raw_not_disj  = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
    5.62 +val clause2raw_not_not   = @{lemma "P ==> ~~P" by auto};
    5.63 +
    5.64 +val iff_refl             = @{lemma "(P::bool) = P" by auto};
    5.65 +val iff_trans            = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
    5.66 +val conj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
    5.67 +val disj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
    5.68 +
    5.69 +val make_nnf_imp         = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
    5.70 +val make_nnf_iff         = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
    5.71 +val make_nnf_not_false   = @{lemma "(~False) = True" by auto};
    5.72 +val make_nnf_not_true    = @{lemma "(~True) = False" by auto};
    5.73 +val make_nnf_not_conj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
    5.74 +val make_nnf_not_disj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
    5.75 +val make_nnf_not_imp     = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
    5.76 +val make_nnf_not_iff     = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
    5.77 +val make_nnf_not_not     = @{lemma "P = P' ==> (~~P) = P'" by auto};
    5.78 +
    5.79 +val simp_TF_conj_True_l  = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
    5.80 +val simp_TF_conj_True_r  = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
    5.81 +val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
    5.82 +val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
    5.83 +val simp_TF_disj_True_l  = @{lemma "P = True ==> (P | Q) = True" by auto};
    5.84 +val simp_TF_disj_True_r  = @{lemma "Q = True ==> (P | Q) = True" by auto};
    5.85 +val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
    5.86 +val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
    5.87 +
    5.88 +val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
    5.89 +val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
    5.90 +
    5.91 +val make_cnfx_disj_ex_l  = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
    5.92 +val make_cnfx_disj_ex_r  = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
    5.93 +val make_cnfx_newlit     = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
    5.94 +val make_cnfx_ex_cong    = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
    5.95 +
    5.96 +val weakening_thm        = @{lemma "[| P; Q |] ==> Q" by auto};
    5.97 +
    5.98 +val cnftac_eq_imp        = @{lemma "[| P = Q; P |] ==> Q" by auto};
    5.99 +
   5.100 +fun is_atom (Const (@{const_name False}, _)) = false
   5.101 +  | is_atom (Const (@{const_name True}, _)) = false
   5.102 +  | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
   5.103 +  | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
   5.104 +  | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
   5.105 +  | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
   5.106 +  | is_atom (Const (@{const_name Not}, _) $ _) = false
   5.107 +  | is_atom _ = true;
   5.108 +
   5.109 +fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   5.110 +  | is_literal x = is_atom x;
   5.111 +
   5.112 +fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
   5.113 +  | is_clause x = is_literal x;
   5.114 +
   5.115 +(* ------------------------------------------------------------------------- *)
   5.116 +(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
   5.117 +(*      and the atom's negation                                              *)
   5.118 +(* ------------------------------------------------------------------------- *)
   5.119 +
   5.120 +fun clause_is_trivial c =
   5.121 +  let
   5.122 +    fun dual (Const (@{const_name Not}, _) $ x) = x
   5.123 +      | dual x = HOLogic.Not $ x
   5.124 +    fun has_duals [] = false
   5.125 +      | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
   5.126 +  in
   5.127 +    has_duals (HOLogic.disjuncts c)
   5.128 +  end;
   5.129 +
   5.130 +(* ------------------------------------------------------------------------- *)
   5.131 +(* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
   5.132 +(*        [...] |- x1 | ... | xn                                             *)
   5.133 +(*      (where each xi is a literal) is translated to                        *)
   5.134 +(*        [..., x1', ..., xn'] |- False ,                                    *)
   5.135 +(*      where each xi' is the negation normal form of ~xi                    *)
   5.136 +(* ------------------------------------------------------------------------- *)
   5.137 +
   5.138 +fun clause2raw_thm clause =
   5.139 +  let
   5.140 +    (* eliminates negated disjunctions from the i-th premise, possibly *)
   5.141 +    (* adding new premises, then continues with the (i+1)-th premise   *)
   5.142 +    (* int -> Thm.thm -> Thm.thm *)
   5.143 +    fun not_disj_to_prem i thm =
   5.144 +      if i > nprems_of thm then
   5.145 +        thm
   5.146 +      else
   5.147 +        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
   5.148 +    (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
   5.149 +    (* becomes "[..., A1, ..., An] |- B"                                   *)
   5.150 +    (* Thm.thm -> Thm.thm *)
   5.151 +    fun prems_to_hyps thm =
   5.152 +      fold (fn cprem => fn thm' =>
   5.153 +        Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
   5.154 +  in
   5.155 +    (* [...] |- ~(x1 | ... | xn) ==> False *)
   5.156 +    (clause2raw_notE OF [clause])
   5.157 +    (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
   5.158 +    |> not_disj_to_prem 1
   5.159 +    (* [...] |- x1' ==> ... ==> xn' ==> False *)
   5.160 +    |> Seq.hd o TRYALL (rtac clause2raw_not_not)
   5.161 +    (* [..., x1', ..., xn'] |- False *)
   5.162 +    |> prems_to_hyps
   5.163 +  end;
   5.164 +
   5.165 +(* ------------------------------------------------------------------------- *)
   5.166 +(* inst_thm: instantiates a theorem with a list of terms                     *)
   5.167 +(* ------------------------------------------------------------------------- *)
   5.168 +
   5.169 +fun inst_thm thy ts thm =
   5.170 +  instantiate' [] (map (SOME o cterm_of thy) ts) thm;
   5.171 +
   5.172 +(* ------------------------------------------------------------------------- *)
   5.173 +(*                         Naive CNF transformation                          *)
   5.174 +(* ------------------------------------------------------------------------- *)
   5.175 +
   5.176 +(* ------------------------------------------------------------------------- *)
   5.177 +(* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
   5.178 +(*      negation normal form (i.e. negation only occurs in front of atoms)   *)
   5.179 +(*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
   5.180 +(*      eliminated (possibly causing an exponential blowup)                  *)
   5.181 +(* ------------------------------------------------------------------------- *)
   5.182 +
   5.183 +fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   5.184 +      let
   5.185 +        val thm1 = make_nnf_thm thy x
   5.186 +        val thm2 = make_nnf_thm thy y
   5.187 +      in
   5.188 +        conj_cong OF [thm1, thm2]
   5.189 +      end
   5.190 +  | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   5.191 +      let
   5.192 +        val thm1 = make_nnf_thm thy x
   5.193 +        val thm2 = make_nnf_thm thy y
   5.194 +      in
   5.195 +        disj_cong OF [thm1, thm2]
   5.196 +      end
   5.197 +  | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
   5.198 +      let
   5.199 +        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   5.200 +        val thm2 = make_nnf_thm thy y
   5.201 +      in
   5.202 +        make_nnf_imp OF [thm1, thm2]
   5.203 +      end
   5.204 +  | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
   5.205 +      let
   5.206 +        val thm1 = make_nnf_thm thy x
   5.207 +        val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   5.208 +        val thm3 = make_nnf_thm thy y
   5.209 +        val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   5.210 +      in
   5.211 +        make_nnf_iff OF [thm1, thm2, thm3, thm4]
   5.212 +      end
   5.213 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
   5.214 +      make_nnf_not_false
   5.215 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
   5.216 +      make_nnf_not_true
   5.217 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
   5.218 +      let
   5.219 +        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   5.220 +        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   5.221 +      in
   5.222 +        make_nnf_not_conj OF [thm1, thm2]
   5.223 +      end
   5.224 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
   5.225 +      let
   5.226 +        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   5.227 +        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   5.228 +      in
   5.229 +        make_nnf_not_disj OF [thm1, thm2]
   5.230 +      end
   5.231 +  | make_nnf_thm thy
   5.232 +      (Const (@{const_name Not}, _) $
   5.233 +        (Const (@{const_name HOL.implies}, _) $ x $ y)) =
   5.234 +      let
   5.235 +        val thm1 = make_nnf_thm thy x
   5.236 +        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   5.237 +      in
   5.238 +        make_nnf_not_imp OF [thm1, thm2]
   5.239 +      end
   5.240 +  | make_nnf_thm thy
   5.241 +      (Const (@{const_name Not}, _) $
   5.242 +        (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   5.243 +      let
   5.244 +        val thm1 = make_nnf_thm thy x
   5.245 +        val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   5.246 +        val thm3 = make_nnf_thm thy y
   5.247 +        val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   5.248 +      in
   5.249 +        make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
   5.250 +      end
   5.251 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
   5.252 +      let
   5.253 +        val thm1 = make_nnf_thm thy x
   5.254 +      in
   5.255 +        make_nnf_not_not OF [thm1]
   5.256 +      end
   5.257 +  | make_nnf_thm thy t = inst_thm thy [t] iff_refl;
   5.258 +
   5.259 +val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
   5.260 +val eq_reflection = @{thm eq_reflection}
   5.261 +
   5.262 +fun make_under_quantifiers ctxt make t =
   5.263 +  let
   5.264 +    val thy = Proof_Context.theory_of ctxt
   5.265 +    fun conv ctxt ct =
   5.266 +      case term_of ct of
   5.267 +        Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
   5.268 +      | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
   5.269 +      | Const _ => Conv.all_conv ct
   5.270 +      | t => make t RS eq_reflection
   5.271 +  in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
   5.272 +
   5.273 +fun make_nnf_thm_under_quantifiers ctxt =
   5.274 +  make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
   5.275 +
   5.276 +(* ------------------------------------------------------------------------- *)
   5.277 +(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
   5.278 +(*      t, but simplified wrt. the following theorems:                       *)
   5.279 +(*        (True & x) = x                                                     *)
   5.280 +(*        (x & True) = x                                                     *)
   5.281 +(*        (False & x) = False                                                *)
   5.282 +(*        (x & False) = False                                                *)
   5.283 +(*        (True | x) = True                                                  *)
   5.284 +(*        (x | True) = True                                                  *)
   5.285 +(*        (False | x) = x                                                    *)
   5.286 +(*        (x | False) = x                                                    *)
   5.287 +(*      No simplification is performed below connectives other than & and |. *)
   5.288 +(*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
   5.289 +(*      simplified only if the left-hand side does not simplify to False     *)
   5.290 +(*      (True, respectively).                                                *)
   5.291 +(* ------------------------------------------------------------------------- *)
   5.292 +
   5.293 +(* Theory.theory -> Term.term -> Thm.thm *)
   5.294 +
   5.295 +fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   5.296 +      let
   5.297 +        val thm1 = simp_True_False_thm thy x
   5.298 +        val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   5.299 +      in
   5.300 +        if x' = @{term False} then
   5.301 +          simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
   5.302 +        else
   5.303 +          let
   5.304 +            val thm2 = simp_True_False_thm thy y
   5.305 +            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   5.306 +          in
   5.307 +            if x' = @{term True} then
   5.308 +              simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
   5.309 +            else if y' = @{term False} then
   5.310 +              simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
   5.311 +            else if y' = @{term True} then
   5.312 +              simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
   5.313 +            else
   5.314 +              conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
   5.315 +          end
   5.316 +      end
   5.317 +  | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   5.318 +      let
   5.319 +        val thm1 = simp_True_False_thm thy x
   5.320 +        val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   5.321 +      in
   5.322 +        if x' = @{term True} then
   5.323 +          simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
   5.324 +        else
   5.325 +          let
   5.326 +            val thm2 = simp_True_False_thm thy y
   5.327 +            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   5.328 +          in
   5.329 +            if x' = @{term False} then
   5.330 +              simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
   5.331 +            else if y' = @{term True} then
   5.332 +              simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
   5.333 +            else if y' = @{term False} then
   5.334 +              simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
   5.335 +            else
   5.336 +              disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   5.337 +          end
   5.338 +      end
   5.339 +  | simp_True_False_thm thy t = inst_thm thy [t] iff_refl;  (* t = t *)
   5.340 +
   5.341 +(* ------------------------------------------------------------------------- *)
   5.342 +(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
   5.343 +(*      is in conjunction normal form.  May cause an exponential blowup      *)
   5.344 +(*      in the length of the term.                                           *)
   5.345 +(* ------------------------------------------------------------------------- *)
   5.346 +
   5.347 +fun make_cnf_thm ctxt t =
   5.348 +  let
   5.349 +    val thy = Proof_Context.theory_of ctxt
   5.350 +    fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
   5.351 +          let
   5.352 +            val thm1 = make_cnf_thm_from_nnf x
   5.353 +            val thm2 = make_cnf_thm_from_nnf y
   5.354 +          in
   5.355 +            conj_cong OF [thm1, thm2]
   5.356 +          end
   5.357 +      | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
   5.358 +          let
   5.359 +            (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
   5.360 +            fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
   5.361 +                  let
   5.362 +                    val thm1 = make_cnf_disj_thm x1 y'
   5.363 +                    val thm2 = make_cnf_disj_thm x2 y'
   5.364 +                  in
   5.365 +                    make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   5.366 +                  end
   5.367 +              | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
   5.368 +                  let
   5.369 +                    val thm1 = make_cnf_disj_thm x' y1
   5.370 +                    val thm2 = make_cnf_disj_thm x' y2
   5.371 +                  in
   5.372 +                    make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   5.373 +                  end
   5.374 +              | make_cnf_disj_thm x' y' =
   5.375 +                  inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   5.376 +            val thm1 = make_cnf_thm_from_nnf x
   5.377 +            val thm2 = make_cnf_thm_from_nnf y
   5.378 +            val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   5.379 +            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   5.380 +            val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   5.381 +          in
   5.382 +            iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
   5.383 +          end
   5.384 +      | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl
   5.385 +    (* convert 't' to NNF first *)
   5.386 +    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
   5.387 +(*###
   5.388 +    val nnf_thm = make_nnf_thm thy t
   5.389 +*)
   5.390 +    val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   5.391 +    (* then simplify wrt. True/False (this should preserve NNF) *)
   5.392 +    val simp_thm = simp_True_False_thm thy nnf
   5.393 +    val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   5.394 +    (* finally, convert to CNF (this should preserve the simplification) *)
   5.395 +    val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp
   5.396 +(* ###
   5.397 +    val cnf_thm = make_cnf_thm_from_nnf simp
   5.398 +*)
   5.399 +  in
   5.400 +    iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
   5.401 +  end;
   5.402 +
   5.403 +(* ------------------------------------------------------------------------- *)
   5.404 +(*            CNF transformation by introducing new literals                 *)
   5.405 +(* ------------------------------------------------------------------------- *)
   5.406 +
   5.407 +(* ------------------------------------------------------------------------- *)
   5.408 +(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
   5.409 +(*      t' is almost in conjunction normal form, except that conjunctions    *)
   5.410 +(*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
   5.411 +(*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
   5.412 +(*      introduce new (existentially bound) literals.  Note: the current     *)
   5.413 +(*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
   5.414 +(*      in the case of nested equivalences.                                  *)
   5.415 +(* ------------------------------------------------------------------------- *)
   5.416 +
   5.417 +fun make_cnfx_thm ctxt t =
   5.418 +  let
   5.419 +    val thy = Proof_Context.theory_of ctxt
   5.420 +    val var_id = Unsynchronized.ref 0  (* properly initialized below *)
   5.421 +    fun new_free () =
   5.422 +      Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
   5.423 +    fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
   5.424 +          let
   5.425 +            val thm1 = make_cnfx_thm_from_nnf x
   5.426 +            val thm2 = make_cnfx_thm_from_nnf y
   5.427 +          in
   5.428 +            conj_cong OF [thm1, thm2]
   5.429 +          end
   5.430 +      | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
   5.431 +          if is_clause x andalso is_clause y then
   5.432 +            inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
   5.433 +          else if is_literal y orelse is_literal x then
   5.434 +            let
   5.435 +              (* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
   5.436 +              (* almost in CNF, and x' or y' is a literal                      *)
   5.437 +              fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
   5.438 +                    let
   5.439 +                      val thm1 = make_cnfx_disj_thm x1 y'
   5.440 +                      val thm2 = make_cnfx_disj_thm x2 y'
   5.441 +                    in
   5.442 +                      make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   5.443 +                    end
   5.444 +                | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
   5.445 +                    let
   5.446 +                      val thm1 = make_cnfx_disj_thm x' y1
   5.447 +                      val thm2 = make_cnfx_disj_thm x' y2
   5.448 +                    in
   5.449 +                      make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   5.450 +                    end
   5.451 +                | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
   5.452 +                    let
   5.453 +                      val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
   5.454 +                      val var = new_free ()
   5.455 +                      val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
   5.456 +                      val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   5.457 +                      val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   5.458 +                      val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   5.459 +                    in
   5.460 +                      iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   5.461 +                    end
   5.462 +                | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
   5.463 +                    let
   5.464 +                      val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   5.465 +                      val var = new_free ()
   5.466 +                      val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
   5.467 +                      val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   5.468 +                      val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   5.469 +                      val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   5.470 +                    in
   5.471 +                      iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
   5.472 +                    end
   5.473 +                | make_cnfx_disj_thm x' y' =
   5.474 +                    inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   5.475 +              val thm1 = make_cnfx_thm_from_nnf x
   5.476 +              val thm2 = make_cnfx_thm_from_nnf y
   5.477 +              val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   5.478 +              val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   5.479 +              val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   5.480 +            in
   5.481 +              iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
   5.482 +            end
   5.483 +          else
   5.484 +            let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
   5.485 +              val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
   5.486 +              val var = new_free ()
   5.487 +              val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
   5.488 +              val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
   5.489 +              val thm3 = Thm.forall_intr (cterm_of thy var) thm2  (* !!v. (x | v) & (y | ~v) = body' *)
   5.490 +              val thm4 = Thm.strip_shyps (thm3 COMP allI)         (* ALL v. (x | v) & (y | ~v) = body' *)
   5.491 +              val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
   5.492 +            in
   5.493 +              iff_trans OF [thm1, thm5]
   5.494 +            end
   5.495 +      | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl
   5.496 +    (* convert 't' to NNF first *)
   5.497 +    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
   5.498 +(* ###
   5.499 +    val nnf_thm = make_nnf_thm thy t
   5.500 +*)
   5.501 +    val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   5.502 +    (* then simplify wrt. True/False (this should preserve NNF) *)
   5.503 +    val simp_thm = simp_True_False_thm thy nnf
   5.504 +    val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   5.505 +    (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
   5.506 +    val _ = (var_id := fold (fn free => fn max =>
   5.507 +      let
   5.508 +        val (name, _) = dest_Free free
   5.509 +        val idx =
   5.510 +          if String.isPrefix "cnfx_" name then
   5.511 +            (Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
   5.512 +          else
   5.513 +            NONE
   5.514 +      in
   5.515 +        Int.max (max, the_default 0 idx)
   5.516 +      end) (Misc_Legacy.term_frees simp) 0)
   5.517 +    (* finally, convert to definitional CNF (this should preserve the simplification) *)
   5.518 +    val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
   5.519 +(*###
   5.520 +    val cnfx_thm = make_cnfx_thm_from_nnf simp
   5.521 +*)
   5.522 +  in
   5.523 +    iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
   5.524 +  end;
   5.525 +
   5.526 +(* ------------------------------------------------------------------------- *)
   5.527 +(*                                  Tactics                                  *)
   5.528 +(* ------------------------------------------------------------------------- *)
   5.529 +
   5.530 +(* ------------------------------------------------------------------------- *)
   5.531 +(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
   5.532 +(* ------------------------------------------------------------------------- *)
   5.533 +
   5.534 +fun weakening_tac i =
   5.535 +  dtac weakening_thm i THEN atac (i+1);
   5.536 +
   5.537 +(* ------------------------------------------------------------------------- *)
   5.538 +(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
   5.539 +(*      (possibly causing an exponential blowup in the length of each        *)
   5.540 +(*      premise)                                                             *)
   5.541 +(* ------------------------------------------------------------------------- *)
   5.542 +
   5.543 +fun cnf_rewrite_tac ctxt i =
   5.544 +  (* cut the CNF formulas as new premises *)
   5.545 +  Subgoal.FOCUS (fn {prems, ...} =>
   5.546 +    let
   5.547 +      val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
   5.548 +      val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
   5.549 +    in
   5.550 +      cut_facts_tac cut_thms 1
   5.551 +    end) ctxt i
   5.552 +  (* remove the original premises *)
   5.553 +  THEN SELECT_GOAL (fn thm =>
   5.554 +    let
   5.555 +      val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   5.556 +    in
   5.557 +      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   5.558 +    end) i;
   5.559 +
   5.560 +(* ------------------------------------------------------------------------- *)
   5.561 +(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
   5.562 +(*      (possibly introducing new literals)                                  *)
   5.563 +(* ------------------------------------------------------------------------- *)
   5.564 +
   5.565 +fun cnfx_rewrite_tac ctxt i =
   5.566 +  (* cut the CNF formulas as new premises *)
   5.567 +  Subgoal.FOCUS (fn {prems, ...} =>
   5.568 +    let
   5.569 +      val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems
   5.570 +      val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
   5.571 +    in
   5.572 +      cut_facts_tac cut_thms 1
   5.573 +    end) ctxt i
   5.574 +  (* remove the original premises *)
   5.575 +  THEN SELECT_GOAL (fn thm =>
   5.576 +    let
   5.577 +      val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   5.578 +    in
   5.579 +      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   5.580 +    end) i;
   5.581 +
   5.582 +end;
     6.1 --- a/src/HOL/Tools/cnf_funcs.ML	Sat Feb 01 20:46:19 2014 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,579 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/cnf_funcs.ML
     6.5 -    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     6.6 -    Author:     Tjark Weber, TU Muenchen
     6.7 -
     6.8 -FIXME: major overlaps with the code in meson.ML
     6.9 -
    6.10 -Functions and tactics to transform a formula into Conjunctive Normal
    6.11 -Form (CNF).
    6.12 -
    6.13 -A formula in CNF is of the following form:
    6.14 -
    6.15 -    (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
    6.16 -    False
    6.17 -    True
    6.18 -
    6.19 -where each xij is a literal (a positive or negative atomic Boolean
    6.20 -term), i.e. the formula is a conjunction of disjunctions of literals,
    6.21 -or "False", or "True".
    6.22 -
    6.23 -A (non-empty) disjunction of literals is referred to as "clause".
    6.24 -
    6.25 -For the purpose of SAT proof reconstruction, we also make use of
    6.26 -another representation of clauses, which we call the "raw clauses".
    6.27 -Raw clauses are of the form
    6.28 -
    6.29 -    [..., x1', x2', ..., xn'] |- False ,
    6.30 -
    6.31 -where each xi is a literal, and each xi' is the negation normal form
    6.32 -of ~xi.
    6.33 -
    6.34 -Literals are successively removed from the hyps of raw clauses by
    6.35 -resolution during SAT proof reconstruction.
    6.36 -*)
    6.37 -
    6.38 -signature CNF =
    6.39 -sig
    6.40 -  val is_atom: term -> bool
    6.41 -  val is_literal: term -> bool
    6.42 -  val is_clause: term -> bool
    6.43 -  val clause_is_trivial: term -> bool
    6.44 -
    6.45 -  val clause2raw_thm: thm -> thm
    6.46 -  val make_nnf_thm: theory -> term -> thm
    6.47 -
    6.48 -  val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
    6.49 -
    6.50 -  val make_cnf_thm: Proof.context -> term -> thm
    6.51 -  val make_cnfx_thm: Proof.context -> term -> thm
    6.52 -  val cnf_rewrite_tac: Proof.context -> int -> tactic  (* converts all prems of a subgoal to CNF *)
    6.53 -  val cnfx_rewrite_tac: Proof.context -> int -> tactic
    6.54 -    (* converts all prems of a subgoal to (almost) definitional CNF *)
    6.55 -end;
    6.56 -
    6.57 -structure cnf : CNF =
    6.58 -struct
    6.59 -
    6.60 -val clause2raw_notE      = @{lemma "[| P; ~P |] ==> False" by auto};
    6.61 -val clause2raw_not_disj  = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
    6.62 -val clause2raw_not_not   = @{lemma "P ==> ~~P" by auto};
    6.63 -
    6.64 -val iff_refl             = @{lemma "(P::bool) = P" by auto};
    6.65 -val iff_trans            = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
    6.66 -val conj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
    6.67 -val disj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
    6.68 -
    6.69 -val make_nnf_imp         = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
    6.70 -val make_nnf_iff         = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
    6.71 -val make_nnf_not_false   = @{lemma "(~False) = True" by auto};
    6.72 -val make_nnf_not_true    = @{lemma "(~True) = False" by auto};
    6.73 -val make_nnf_not_conj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
    6.74 -val make_nnf_not_disj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
    6.75 -val make_nnf_not_imp     = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
    6.76 -val make_nnf_not_iff     = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
    6.77 -val make_nnf_not_not     = @{lemma "P = P' ==> (~~P) = P'" by auto};
    6.78 -
    6.79 -val simp_TF_conj_True_l  = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
    6.80 -val simp_TF_conj_True_r  = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
    6.81 -val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
    6.82 -val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
    6.83 -val simp_TF_disj_True_l  = @{lemma "P = True ==> (P | Q) = True" by auto};
    6.84 -val simp_TF_disj_True_r  = @{lemma "Q = True ==> (P | Q) = True" by auto};
    6.85 -val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
    6.86 -val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
    6.87 -
    6.88 -val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
    6.89 -val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
    6.90 -
    6.91 -val make_cnfx_disj_ex_l  = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
    6.92 -val make_cnfx_disj_ex_r  = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
    6.93 -val make_cnfx_newlit     = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
    6.94 -val make_cnfx_ex_cong    = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
    6.95 -
    6.96 -val weakening_thm        = @{lemma "[| P; Q |] ==> Q" by auto};
    6.97 -
    6.98 -val cnftac_eq_imp        = @{lemma "[| P = Q; P |] ==> Q" by auto};
    6.99 -
   6.100 -fun is_atom (Const (@{const_name False}, _)) = false
   6.101 -  | is_atom (Const (@{const_name True}, _)) = false
   6.102 -  | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
   6.103 -  | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
   6.104 -  | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
   6.105 -  | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
   6.106 -  | is_atom (Const (@{const_name Not}, _) $ _) = false
   6.107 -  | is_atom _ = true;
   6.108 -
   6.109 -fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   6.110 -  | is_literal x = is_atom x;
   6.111 -
   6.112 -fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
   6.113 -  | is_clause x = is_literal x;
   6.114 -
   6.115 -(* ------------------------------------------------------------------------- *)
   6.116 -(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
   6.117 -(*      and the atom's negation                                              *)
   6.118 -(* ------------------------------------------------------------------------- *)
   6.119 -
   6.120 -fun clause_is_trivial c =
   6.121 -  let
   6.122 -    fun dual (Const (@{const_name Not}, _) $ x) = x
   6.123 -      | dual x = HOLogic.Not $ x
   6.124 -    fun has_duals [] = false
   6.125 -      | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
   6.126 -  in
   6.127 -    has_duals (HOLogic.disjuncts c)
   6.128 -  end;
   6.129 -
   6.130 -(* ------------------------------------------------------------------------- *)
   6.131 -(* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
   6.132 -(*        [...] |- x1 | ... | xn                                             *)
   6.133 -(*      (where each xi is a literal) is translated to                        *)
   6.134 -(*        [..., x1', ..., xn'] |- False ,                                    *)
   6.135 -(*      where each xi' is the negation normal form of ~xi                    *)
   6.136 -(* ------------------------------------------------------------------------- *)
   6.137 -
   6.138 -fun clause2raw_thm clause =
   6.139 -  let
   6.140 -    (* eliminates negated disjunctions from the i-th premise, possibly *)
   6.141 -    (* adding new premises, then continues with the (i+1)-th premise   *)
   6.142 -    (* int -> Thm.thm -> Thm.thm *)
   6.143 -    fun not_disj_to_prem i thm =
   6.144 -      if i > nprems_of thm then
   6.145 -        thm
   6.146 -      else
   6.147 -        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
   6.148 -    (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
   6.149 -    (* becomes "[..., A1, ..., An] |- B"                                   *)
   6.150 -    (* Thm.thm -> Thm.thm *)
   6.151 -    fun prems_to_hyps thm =
   6.152 -      fold (fn cprem => fn thm' =>
   6.153 -        Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
   6.154 -  in
   6.155 -    (* [...] |- ~(x1 | ... | xn) ==> False *)
   6.156 -    (clause2raw_notE OF [clause])
   6.157 -    (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
   6.158 -    |> not_disj_to_prem 1
   6.159 -    (* [...] |- x1' ==> ... ==> xn' ==> False *)
   6.160 -    |> Seq.hd o TRYALL (rtac clause2raw_not_not)
   6.161 -    (* [..., x1', ..., xn'] |- False *)
   6.162 -    |> prems_to_hyps
   6.163 -  end;
   6.164 -
   6.165 -(* ------------------------------------------------------------------------- *)
   6.166 -(* inst_thm: instantiates a theorem with a list of terms                     *)
   6.167 -(* ------------------------------------------------------------------------- *)
   6.168 -
   6.169 -fun inst_thm thy ts thm =
   6.170 -  instantiate' [] (map (SOME o cterm_of thy) ts) thm;
   6.171 -
   6.172 -(* ------------------------------------------------------------------------- *)
   6.173 -(*                         Naive CNF transformation                          *)
   6.174 -(* ------------------------------------------------------------------------- *)
   6.175 -
   6.176 -(* ------------------------------------------------------------------------- *)
   6.177 -(* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
   6.178 -(*      negation normal form (i.e. negation only occurs in front of atoms)   *)
   6.179 -(*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
   6.180 -(*      eliminated (possibly causing an exponential blowup)                  *)
   6.181 -(* ------------------------------------------------------------------------- *)
   6.182 -
   6.183 -fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   6.184 -      let
   6.185 -        val thm1 = make_nnf_thm thy x
   6.186 -        val thm2 = make_nnf_thm thy y
   6.187 -      in
   6.188 -        conj_cong OF [thm1, thm2]
   6.189 -      end
   6.190 -  | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   6.191 -      let
   6.192 -        val thm1 = make_nnf_thm thy x
   6.193 -        val thm2 = make_nnf_thm thy y
   6.194 -      in
   6.195 -        disj_cong OF [thm1, thm2]
   6.196 -      end
   6.197 -  | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
   6.198 -      let
   6.199 -        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   6.200 -        val thm2 = make_nnf_thm thy y
   6.201 -      in
   6.202 -        make_nnf_imp OF [thm1, thm2]
   6.203 -      end
   6.204 -  | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
   6.205 -      let
   6.206 -        val thm1 = make_nnf_thm thy x
   6.207 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   6.208 -        val thm3 = make_nnf_thm thy y
   6.209 -        val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   6.210 -      in
   6.211 -        make_nnf_iff OF [thm1, thm2, thm3, thm4]
   6.212 -      end
   6.213 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
   6.214 -      make_nnf_not_false
   6.215 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
   6.216 -      make_nnf_not_true
   6.217 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
   6.218 -      let
   6.219 -        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   6.220 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   6.221 -      in
   6.222 -        make_nnf_not_conj OF [thm1, thm2]
   6.223 -      end
   6.224 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
   6.225 -      let
   6.226 -        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   6.227 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   6.228 -      in
   6.229 -        make_nnf_not_disj OF [thm1, thm2]
   6.230 -      end
   6.231 -  | make_nnf_thm thy
   6.232 -      (Const (@{const_name Not}, _) $
   6.233 -        (Const (@{const_name HOL.implies}, _) $ x $ y)) =
   6.234 -      let
   6.235 -        val thm1 = make_nnf_thm thy x
   6.236 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   6.237 -      in
   6.238 -        make_nnf_not_imp OF [thm1, thm2]
   6.239 -      end
   6.240 -  | make_nnf_thm thy
   6.241 -      (Const (@{const_name Not}, _) $
   6.242 -        (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   6.243 -      let
   6.244 -        val thm1 = make_nnf_thm thy x
   6.245 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   6.246 -        val thm3 = make_nnf_thm thy y
   6.247 -        val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   6.248 -      in
   6.249 -        make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
   6.250 -      end
   6.251 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
   6.252 -      let
   6.253 -        val thm1 = make_nnf_thm thy x
   6.254 -      in
   6.255 -        make_nnf_not_not OF [thm1]
   6.256 -      end
   6.257 -  | make_nnf_thm thy t = inst_thm thy [t] iff_refl;
   6.258 -
   6.259 -val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
   6.260 -val eq_reflection = @{thm eq_reflection}
   6.261 -
   6.262 -fun make_under_quantifiers ctxt make t =
   6.263 -  let
   6.264 -    val thy = Proof_Context.theory_of ctxt
   6.265 -    fun conv ctxt ct =
   6.266 -      case term_of ct of
   6.267 -        Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
   6.268 -      | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
   6.269 -      | Const _ => Conv.all_conv ct
   6.270 -      | t => make t RS eq_reflection
   6.271 -  in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
   6.272 -
   6.273 -fun make_nnf_thm_under_quantifiers ctxt =
   6.274 -  make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
   6.275 -
   6.276 -(* ------------------------------------------------------------------------- *)
   6.277 -(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
   6.278 -(*      t, but simplified wrt. the following theorems:                       *)
   6.279 -(*        (True & x) = x                                                     *)
   6.280 -(*        (x & True) = x                                                     *)
   6.281 -(*        (False & x) = False                                                *)
   6.282 -(*        (x & False) = False                                                *)
   6.283 -(*        (True | x) = True                                                  *)
   6.284 -(*        (x | True) = True                                                  *)
   6.285 -(*        (False | x) = x                                                    *)
   6.286 -(*        (x | False) = x                                                    *)
   6.287 -(*      No simplification is performed below connectives other than & and |. *)
   6.288 -(*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
   6.289 -(*      simplified only if the left-hand side does not simplify to False     *)
   6.290 -(*      (True, respectively).                                                *)
   6.291 -(* ------------------------------------------------------------------------- *)
   6.292 -
   6.293 -(* Theory.theory -> Term.term -> Thm.thm *)
   6.294 -
   6.295 -fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   6.296 -      let
   6.297 -        val thm1 = simp_True_False_thm thy x
   6.298 -        val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   6.299 -      in
   6.300 -        if x' = @{term False} then
   6.301 -          simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
   6.302 -        else
   6.303 -          let
   6.304 -            val thm2 = simp_True_False_thm thy y
   6.305 -            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   6.306 -          in
   6.307 -            if x' = @{term True} then
   6.308 -              simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
   6.309 -            else if y' = @{term False} then
   6.310 -              simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
   6.311 -            else if y' = @{term True} then
   6.312 -              simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
   6.313 -            else
   6.314 -              conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
   6.315 -          end
   6.316 -      end
   6.317 -  | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   6.318 -      let
   6.319 -        val thm1 = simp_True_False_thm thy x
   6.320 -        val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   6.321 -      in
   6.322 -        if x' = @{term True} then
   6.323 -          simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
   6.324 -        else
   6.325 -          let
   6.326 -            val thm2 = simp_True_False_thm thy y
   6.327 -            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   6.328 -          in
   6.329 -            if x' = @{term False} then
   6.330 -              simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
   6.331 -            else if y' = @{term True} then
   6.332 -              simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
   6.333 -            else if y' = @{term False} then
   6.334 -              simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
   6.335 -            else
   6.336 -              disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   6.337 -          end
   6.338 -      end
   6.339 -  | simp_True_False_thm thy t = inst_thm thy [t] iff_refl;  (* t = t *)
   6.340 -
   6.341 -(* ------------------------------------------------------------------------- *)
   6.342 -(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
   6.343 -(*      is in conjunction normal form.  May cause an exponential blowup      *)
   6.344 -(*      in the length of the term.                                           *)
   6.345 -(* ------------------------------------------------------------------------- *)
   6.346 -
   6.347 -fun make_cnf_thm ctxt t =
   6.348 -  let
   6.349 -    val thy = Proof_Context.theory_of ctxt
   6.350 -    fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
   6.351 -          let
   6.352 -            val thm1 = make_cnf_thm_from_nnf x
   6.353 -            val thm2 = make_cnf_thm_from_nnf y
   6.354 -          in
   6.355 -            conj_cong OF [thm1, thm2]
   6.356 -          end
   6.357 -      | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
   6.358 -          let
   6.359 -            (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
   6.360 -            fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
   6.361 -                  let
   6.362 -                    val thm1 = make_cnf_disj_thm x1 y'
   6.363 -                    val thm2 = make_cnf_disj_thm x2 y'
   6.364 -                  in
   6.365 -                    make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   6.366 -                  end
   6.367 -              | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
   6.368 -                  let
   6.369 -                    val thm1 = make_cnf_disj_thm x' y1
   6.370 -                    val thm2 = make_cnf_disj_thm x' y2
   6.371 -                  in
   6.372 -                    make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   6.373 -                  end
   6.374 -              | make_cnf_disj_thm x' y' =
   6.375 -                  inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   6.376 -            val thm1 = make_cnf_thm_from_nnf x
   6.377 -            val thm2 = make_cnf_thm_from_nnf y
   6.378 -            val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   6.379 -            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   6.380 -            val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   6.381 -          in
   6.382 -            iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
   6.383 -          end
   6.384 -      | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl
   6.385 -    (* convert 't' to NNF first *)
   6.386 -    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
   6.387 -(*###
   6.388 -    val nnf_thm = make_nnf_thm thy t
   6.389 -*)
   6.390 -    val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   6.391 -    (* then simplify wrt. True/False (this should preserve NNF) *)
   6.392 -    val simp_thm = simp_True_False_thm thy nnf
   6.393 -    val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   6.394 -    (* finally, convert to CNF (this should preserve the simplification) *)
   6.395 -    val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp
   6.396 -(* ###
   6.397 -    val cnf_thm = make_cnf_thm_from_nnf simp
   6.398 -*)
   6.399 -  in
   6.400 -    iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
   6.401 -  end;
   6.402 -
   6.403 -(* ------------------------------------------------------------------------- *)
   6.404 -(*            CNF transformation by introducing new literals                 *)
   6.405 -(* ------------------------------------------------------------------------- *)
   6.406 -
   6.407 -(* ------------------------------------------------------------------------- *)
   6.408 -(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
   6.409 -(*      t' is almost in conjunction normal form, except that conjunctions    *)
   6.410 -(*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
   6.411 -(*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
   6.412 -(*      introduce new (existentially bound) literals.  Note: the current     *)
   6.413 -(*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
   6.414 -(*      in the case of nested equivalences.                                  *)
   6.415 -(* ------------------------------------------------------------------------- *)
   6.416 -
   6.417 -fun make_cnfx_thm ctxt t =
   6.418 -  let
   6.419 -    val thy = Proof_Context.theory_of ctxt
   6.420 -    val var_id = Unsynchronized.ref 0  (* properly initialized below *)
   6.421 -    fun new_free () =
   6.422 -      Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
   6.423 -    fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
   6.424 -          let
   6.425 -            val thm1 = make_cnfx_thm_from_nnf x
   6.426 -            val thm2 = make_cnfx_thm_from_nnf y
   6.427 -          in
   6.428 -            conj_cong OF [thm1, thm2]
   6.429 -          end
   6.430 -      | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
   6.431 -          if is_clause x andalso is_clause y then
   6.432 -            inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
   6.433 -          else if is_literal y orelse is_literal x then
   6.434 -            let
   6.435 -              (* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
   6.436 -              (* almost in CNF, and x' or y' is a literal                      *)
   6.437 -              fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
   6.438 -                    let
   6.439 -                      val thm1 = make_cnfx_disj_thm x1 y'
   6.440 -                      val thm2 = make_cnfx_disj_thm x2 y'
   6.441 -                    in
   6.442 -                      make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   6.443 -                    end
   6.444 -                | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
   6.445 -                    let
   6.446 -                      val thm1 = make_cnfx_disj_thm x' y1
   6.447 -                      val thm2 = make_cnfx_disj_thm x' y2
   6.448 -                    in
   6.449 -                      make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   6.450 -                    end
   6.451 -                | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
   6.452 -                    let
   6.453 -                      val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
   6.454 -                      val var = new_free ()
   6.455 -                      val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
   6.456 -                      val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   6.457 -                      val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   6.458 -                      val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   6.459 -                    in
   6.460 -                      iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   6.461 -                    end
   6.462 -                | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
   6.463 -                    let
   6.464 -                      val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   6.465 -                      val var = new_free ()
   6.466 -                      val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
   6.467 -                      val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   6.468 -                      val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   6.469 -                      val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   6.470 -                    in
   6.471 -                      iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
   6.472 -                    end
   6.473 -                | make_cnfx_disj_thm x' y' =
   6.474 -                    inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   6.475 -              val thm1 = make_cnfx_thm_from_nnf x
   6.476 -              val thm2 = make_cnfx_thm_from_nnf y
   6.477 -              val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   6.478 -              val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   6.479 -              val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   6.480 -            in
   6.481 -              iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
   6.482 -            end
   6.483 -          else
   6.484 -            let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
   6.485 -              val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
   6.486 -              val var = new_free ()
   6.487 -              val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
   6.488 -              val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
   6.489 -              val thm3 = Thm.forall_intr (cterm_of thy var) thm2  (* !!v. (x | v) & (y | ~v) = body' *)
   6.490 -              val thm4 = Thm.strip_shyps (thm3 COMP allI)         (* ALL v. (x | v) & (y | ~v) = body' *)
   6.491 -              val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
   6.492 -            in
   6.493 -              iff_trans OF [thm1, thm5]
   6.494 -            end
   6.495 -      | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl
   6.496 -    (* convert 't' to NNF first *)
   6.497 -    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
   6.498 -(* ###
   6.499 -    val nnf_thm = make_nnf_thm thy t
   6.500 -*)
   6.501 -    val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   6.502 -    (* then simplify wrt. True/False (this should preserve NNF) *)
   6.503 -    val simp_thm = simp_True_False_thm thy nnf
   6.504 -    val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   6.505 -    (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
   6.506 -    val _ = (var_id := fold (fn free => fn max =>
   6.507 -      let
   6.508 -        val (name, _) = dest_Free free
   6.509 -        val idx =
   6.510 -          if String.isPrefix "cnfx_" name then
   6.511 -            (Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
   6.512 -          else
   6.513 -            NONE
   6.514 -      in
   6.515 -        Int.max (max, the_default 0 idx)
   6.516 -      end) (Misc_Legacy.term_frees simp) 0)
   6.517 -    (* finally, convert to definitional CNF (this should preserve the simplification) *)
   6.518 -    val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
   6.519 -(*###
   6.520 -    val cnfx_thm = make_cnfx_thm_from_nnf simp
   6.521 -*)
   6.522 -  in
   6.523 -    iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
   6.524 -  end;
   6.525 -
   6.526 -(* ------------------------------------------------------------------------- *)
   6.527 -(*                                  Tactics                                  *)
   6.528 -(* ------------------------------------------------------------------------- *)
   6.529 -
   6.530 -(* ------------------------------------------------------------------------- *)
   6.531 -(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
   6.532 -(* ------------------------------------------------------------------------- *)
   6.533 -
   6.534 -fun weakening_tac i =
   6.535 -  dtac weakening_thm i THEN atac (i+1);
   6.536 -
   6.537 -(* ------------------------------------------------------------------------- *)
   6.538 -(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
   6.539 -(*      (possibly causing an exponential blowup in the length of each        *)
   6.540 -(*      premise)                                                             *)
   6.541 -(* ------------------------------------------------------------------------- *)
   6.542 -
   6.543 -fun cnf_rewrite_tac ctxt i =
   6.544 -  (* cut the CNF formulas as new premises *)
   6.545 -  Subgoal.FOCUS (fn {prems, ...} =>
   6.546 -    let
   6.547 -      val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
   6.548 -      val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
   6.549 -    in
   6.550 -      cut_facts_tac cut_thms 1
   6.551 -    end) ctxt i
   6.552 -  (* remove the original premises *)
   6.553 -  THEN SELECT_GOAL (fn thm =>
   6.554 -    let
   6.555 -      val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   6.556 -    in
   6.557 -      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   6.558 -    end) i;
   6.559 -
   6.560 -(* ------------------------------------------------------------------------- *)
   6.561 -(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
   6.562 -(*      (possibly introducing new literals)                                  *)
   6.563 -(* ------------------------------------------------------------------------- *)
   6.564 -
   6.565 -fun cnfx_rewrite_tac ctxt i =
   6.566 -  (* cut the CNF formulas as new premises *)
   6.567 -  Subgoal.FOCUS (fn {prems, ...} =>
   6.568 -    let
   6.569 -      val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems
   6.570 -      val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
   6.571 -    in
   6.572 -      cut_facts_tac cut_thms 1
   6.573 -    end) ctxt i
   6.574 -  (* remove the original premises *)
   6.575 -  THEN SELECT_GOAL (fn thm =>
   6.576 -    let
   6.577 -      val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   6.578 -    in
   6.579 -      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   6.580 -    end) i;
   6.581 -
   6.582 -end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/sat.ML	Sat Feb 01 21:09:53 2014 +0100
     7.3 @@ -0,0 +1,474 @@
     7.4 +(*  Title:      HOL/Tools/sat.ML
     7.5 +    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     7.6 +    Author:     Tjark Weber, TU Muenchen
     7.7 +
     7.8 +Proof reconstruction from SAT solvers.
     7.9 +
    7.10 +  Description:
    7.11 +    This file defines several tactics to invoke a proof-producing
    7.12 +    SAT solver on a propositional goal in clausal form.
    7.13 +
    7.14 +    We use a sequent presentation of clauses to speed up resolution
    7.15 +    proof reconstruction.
    7.16 +    We call such clauses "raw clauses", which are of the form
    7.17 +          [x1, ..., xn, P] |- False
    7.18 +    (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
    7.19 +    where each xi is a literal (see also comments in cnf.ML).
    7.20 +
    7.21 +    This does not work for goals containing schematic variables!
    7.22 +
    7.23 +      The tactic produces a clause representation of the given goal
    7.24 +      in DIMACS format and invokes a SAT solver, which should return
    7.25 +      a proof consisting of a sequence of resolution steps, indicating
    7.26 +      the two input clauses, and resulting in new clauses, leading to
    7.27 +      the empty clause (i.e. "False").  The tactic replays this proof
    7.28 +      in Isabelle and thus solves the overall goal.
    7.29 +
    7.30 +  There are three SAT tactics available.  They differ in the CNF transformation
    7.31 +  used. "sat_tac" uses naive CNF transformation to transform the theorem to be
    7.32 +  proved before giving it to the SAT solver.  The naive transformation in the
    7.33 +  worst case can lead to an exponential blow up in formula size.  Another
    7.34 +  tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
    7.35 +  produce a formula of linear size increase compared to the input formula, at
    7.36 +  the cost of possibly introducing new variables.  See cnf.ML for more
    7.37 +  comments on the CNF transformation.  "rawsat_tac" should be used with
    7.38 +  caution: no CNF transformation is performed, and the tactic's behavior is
    7.39 +  undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
    7.40 +  where each Ci is a disjunction.
    7.41 +
    7.42 +  The SAT solver to be used can be set via the "solver" reference.  See
    7.43 +  sat_solvers.ML for possible values, and etc/settings for required (solver-
    7.44 +  dependent) configuration settings.  To replay SAT proofs in Isabelle, you
    7.45 +  must of course use a proof-producing SAT solver in the first place.
    7.46 +
    7.47 +  Proofs are replayed only if "quick_and_dirty" is false.  If
    7.48 +  "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
    7.49 +  negation to be unsatisfiable) is proved via an oracle.
    7.50 +*)
    7.51 +
    7.52 +signature SAT =
    7.53 +sig
    7.54 +  val trace_sat: bool Unsynchronized.ref    (* input: print trace messages *)
    7.55 +  val solver: string Unsynchronized.ref  (* input: name of SAT solver to be used *)
    7.56 +  val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
    7.57 +  val rawsat_thm: Proof.context -> cterm list -> thm
    7.58 +  val rawsat_tac: Proof.context -> int -> tactic
    7.59 +  val sat_tac: Proof.context -> int -> tactic
    7.60 +  val satx_tac: Proof.context -> int -> tactic
    7.61 +end
    7.62 +
    7.63 +structure SAT : SAT =
    7.64 +struct
    7.65 +
    7.66 +val trace_sat = Unsynchronized.ref false;
    7.67 +
    7.68 +val solver = Unsynchronized.ref "zchaff_with_proofs";
    7.69 +  (*see HOL/Tools/sat_solver.ML for possible values*)
    7.70 +
    7.71 +val counter = Unsynchronized.ref 0;
    7.72 +
    7.73 +val resolution_thm =
    7.74 +  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
    7.75 +
    7.76 +val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
    7.77 +
    7.78 +(* ------------------------------------------------------------------------- *)
    7.79 +(* lit_ord: an order on integers that considers their absolute values only,  *)
    7.80 +(*      thereby treating integers that represent the same atom (positively   *)
    7.81 +(*      or negatively) as equal                                              *)
    7.82 +(* ------------------------------------------------------------------------- *)
    7.83 +
    7.84 +fun lit_ord (i, j) = int_ord (abs i, abs j);
    7.85 +
    7.86 +(* ------------------------------------------------------------------------- *)
    7.87 +(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
    7.88 +(*      distinguished:                                                       *)
    7.89 +(*      1. NO_CLAUSE: clause not proved (yet)                                *)
    7.90 +(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
    7.91 +(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
    7.92 +(*         (a mapping from int's to its literals) for faster proof           *)
    7.93 +(*         reconstruction                                                    *)
    7.94 +(* ------------------------------------------------------------------------- *)
    7.95 +
    7.96 +datatype CLAUSE =
    7.97 +    NO_CLAUSE
    7.98 +  | ORIG_CLAUSE of thm
    7.99 +  | RAW_CLAUSE of thm * (int * cterm) list;
   7.100 +
   7.101 +(* ------------------------------------------------------------------------- *)
   7.102 +(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
   7.103 +(*      resolution over the list (starting with its head), i.e. with two raw *)
   7.104 +(*      clauses                                                              *)
   7.105 +(*        [P, x1, ..., a, ..., xn] |- False                                  *)
   7.106 +(*      and                                                                  *)
   7.107 +(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
   7.108 +(*      (where a and a' are dual to each other), we convert the first clause *)
   7.109 +(*      to                                                                   *)
   7.110 +(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
   7.111 +(*      the second clause to                                                 *)
   7.112 +(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
   7.113 +(*      and then perform resolution with                                     *)
   7.114 +(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
   7.115 +(*      to produce                                                           *)
   7.116 +(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
   7.117 +(*      Each clause is accompanied with an association list mapping integers *)
   7.118 +(*      (positive for positive literals, negative for negative literals, and *)
   7.119 +(*      the same absolute value for dual literals) to the actual literals as *)
   7.120 +(*      cterms.                                                              *)
   7.121 +(* ------------------------------------------------------------------------- *)
   7.122 +
   7.123 +fun resolve_raw_clauses _ [] =
   7.124 +      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   7.125 +  | resolve_raw_clauses ctxt (c::cs) =
   7.126 +      let
   7.127 +        (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
   7.128 +        fun merge xs [] = xs
   7.129 +          | merge [] ys = ys
   7.130 +          | merge (x :: xs) (y :: ys) =
   7.131 +              (case (lit_ord o pairself fst) (x, y) of
   7.132 +                LESS => x :: merge xs (y :: ys)
   7.133 +              | EQUAL => x :: merge xs ys
   7.134 +              | GREATER => y :: merge (x :: xs) ys)
   7.135 +
   7.136 +        (* find out which two hyps are used in the resolution *)
   7.137 +        fun find_res_hyps ([], _) _ =
   7.138 +              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   7.139 +          | find_res_hyps (_, []) _ =
   7.140 +              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   7.141 +          | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
   7.142 +              (case (lit_ord o pairself fst) (h1, h2) of
   7.143 +                LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
   7.144 +              | EQUAL =>
   7.145 +                  let
   7.146 +                    val (i1, chyp1) = h1
   7.147 +                    val (i2, chyp2) = h2
   7.148 +                  in
   7.149 +                    if i1 = ~ i2 then
   7.150 +                      (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
   7.151 +                    else (* i1 = i2 *)
   7.152 +                      find_res_hyps (hyps1, hyps2) (h1 :: acc)
   7.153 +                  end
   7.154 +          | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
   7.155 +
   7.156 +        fun resolution (c1, hyps1) (c2, hyps2) =
   7.157 +          let
   7.158 +            val _ =
   7.159 +              if ! trace_sat then  (* FIXME !? *)
   7.160 +                tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
   7.161 +                  " (hyps: " ^ ML_Syntax.print_list
   7.162 +                    (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
   7.163 +                  ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
   7.164 +                  " (hyps: " ^ ML_Syntax.print_list
   7.165 +                    (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
   7.166 +              else ()
   7.167 +
   7.168 +            (* the two literals used for resolution *)
   7.169 +            val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
   7.170 +
   7.171 +            val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
   7.172 +            val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
   7.173 +
   7.174 +            val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
   7.175 +              let
   7.176 +                val cLit =
   7.177 +                  snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
   7.178 +              in
   7.179 +                Thm.instantiate ([], [(cP, cLit)]) resolution_thm
   7.180 +              end
   7.181 +
   7.182 +            val _ =
   7.183 +              if !trace_sat then
   7.184 +                tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
   7.185 +              else ()
   7.186 +
   7.187 +            (* Gamma1, Gamma2 |- False *)
   7.188 +            val c_new =
   7.189 +              Thm.implies_elim
   7.190 +                (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
   7.191 +                (if hyp1_is_neg then c1' else c2')
   7.192 +
   7.193 +            val _ =
   7.194 +              if !trace_sat then
   7.195 +                tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
   7.196 +                  " (hyps: " ^ ML_Syntax.print_list
   7.197 +                      (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
   7.198 +              else ()
   7.199 +            val _ = Unsynchronized.inc counter
   7.200 +          in
   7.201 +            (c_new, new_hyps)
   7.202 +          end
   7.203 +        in
   7.204 +          fold resolution cs c
   7.205 +        end;
   7.206 +
   7.207 +(* ------------------------------------------------------------------------- *)
   7.208 +(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
   7.209 +(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
   7.210 +(*      'clauses' array with derived clauses, and returns the derived clause *)
   7.211 +(*      at index 'empty_id' (which should just be "False" if proof           *)
   7.212 +(*      reconstruction was successful, with the used clauses as hyps).       *)
   7.213 +(*      'atom_table' must contain an injective mapping from all atoms that   *)
   7.214 +(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
   7.215 +(* ------------------------------------------------------------------------- *)
   7.216 +
   7.217 +fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
   7.218 +  let
   7.219 +    fun index_of_literal chyp =
   7.220 +      (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
   7.221 +        (Const (@{const_name Not}, _) $ atom) =>
   7.222 +          SOME (~ (the (Termtab.lookup atom_table atom)))
   7.223 +      | atom => SOME (the (Termtab.lookup atom_table atom)))
   7.224 +      handle TERM _ => NONE;  (* 'chyp' is not a literal *)
   7.225 +
   7.226 +    fun prove_clause id =
   7.227 +      (case Array.sub (clauses, id) of
   7.228 +        RAW_CLAUSE clause => clause
   7.229 +      | ORIG_CLAUSE thm =>
   7.230 +          (* convert the original clause *)
   7.231 +          let
   7.232 +            val _ =
   7.233 +              if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
   7.234 +            val raw = CNF.clause2raw_thm thm
   7.235 +            val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
   7.236 +              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
   7.237 +            val clause = (raw, hyps)
   7.238 +            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   7.239 +          in
   7.240 +            clause
   7.241 +          end
   7.242 +      | NO_CLAUSE =>
   7.243 +          (* prove the clause, using information from 'clause_table' *)
   7.244 +          let
   7.245 +            val _ =
   7.246 +              if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
   7.247 +            val ids = the (Inttab.lookup clause_table id)
   7.248 +            val clause = resolve_raw_clauses ctxt (map prove_clause ids)
   7.249 +            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   7.250 +            val _ =
   7.251 +              if !trace_sat then
   7.252 +                tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
   7.253 +              else ()
   7.254 +          in
   7.255 +            clause
   7.256 +          end)
   7.257 +
   7.258 +    val _ = counter := 0
   7.259 +    val empty_clause = fst (prove_clause empty_id)
   7.260 +    val _ =
   7.261 +      if !trace_sat then
   7.262 +        tracing ("Proof reconstruction successful; " ^
   7.263 +          string_of_int (!counter) ^ " resolution step(s) total.")
   7.264 +      else ()
   7.265 +  in
   7.266 +    empty_clause
   7.267 +  end;
   7.268 +
   7.269 +(* ------------------------------------------------------------------------- *)
   7.270 +(* string_of_prop_formula: return a human-readable string representation of  *)
   7.271 +(*      a 'prop_formula' (just for tracing)                                  *)
   7.272 +(* ------------------------------------------------------------------------- *)
   7.273 +
   7.274 +fun string_of_prop_formula Prop_Logic.True = "True"
   7.275 +  | string_of_prop_formula Prop_Logic.False = "False"
   7.276 +  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
   7.277 +  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
   7.278 +  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
   7.279 +      "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   7.280 +  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
   7.281 +      "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
   7.282 +
   7.283 +(* ------------------------------------------------------------------------- *)
   7.284 +(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   7.285 +(*      a proof from the resulting proof trace of the SAT solver.  The       *)
   7.286 +(*      theorem returned is just "False" (with some of the given clauses as  *)
   7.287 +(*      hyps).                                                               *)
   7.288 +(* ------------------------------------------------------------------------- *)
   7.289 +
   7.290 +fun rawsat_thm ctxt clauses =
   7.291 +  let
   7.292 +    (* remove premises that equal "True" *)
   7.293 +    val clauses' = filter (fn clause =>
   7.294 +      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
   7.295 +        handle TERM ("dest_Trueprop", _) => true) clauses
   7.296 +    (* remove non-clausal premises -- of course this shouldn't actually   *)
   7.297 +    (* remove anything as long as 'rawsat_tac' is only called after the   *)
   7.298 +    (* premises have been converted to clauses                            *)
   7.299 +    val clauses'' = filter (fn clause =>
   7.300 +      ((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
   7.301 +        handle TERM ("dest_Trueprop", _) => false)
   7.302 +      orelse (
   7.303 +        warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
   7.304 +        false)) clauses'
   7.305 +    (* remove trivial clauses -- this is necessary because zChaff removes *)
   7.306 +    (* trivial clauses during preprocessing, and otherwise our clause     *)
   7.307 +    (* numbering would be off                                             *)
   7.308 +    val nontrivial_clauses =
   7.309 +      filter (not o CNF.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
   7.310 +    (* sort clauses according to the term order -- an optimization,       *)
   7.311 +    (* useful because forming the union of hypotheses, as done by         *)
   7.312 +    (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
   7.313 +    (* terms sorted in descending order, while only linear for terms      *)
   7.314 +    (* sorted in ascending order                                          *)
   7.315 +    val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   7.316 +    val _ =
   7.317 +      if !trace_sat then
   7.318 +        tracing ("Sorted non-trivial clauses:\n" ^
   7.319 +          cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
   7.320 +      else ()
   7.321 +    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
   7.322 +    val (fms, atom_table) =
   7.323 +      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
   7.324 +        sorted_clauses Termtab.empty
   7.325 +    val _ =
   7.326 +      if !trace_sat then
   7.327 +        tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
   7.328 +      else ()
   7.329 +    val fm = Prop_Logic.all fms
   7.330 +    fun make_quick_and_dirty_thm () =
   7.331 +      let
   7.332 +        val _ =
   7.333 +          if !trace_sat then
   7.334 +            tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   7.335 +          else ()
   7.336 +        val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
   7.337 +      in
   7.338 +        (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   7.339 +        (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
   7.340 +        (* clauses in ascending order (which is linear for                  *)
   7.341 +        (* 'Conjunction.intr_balanced', used below)                         *)
   7.342 +        fold Thm.weaken (rev sorted_clauses) False_thm
   7.343 +      end
   7.344 +  in
   7.345 +    case
   7.346 +      let val the_solver = ! solver
   7.347 +      in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
   7.348 +    of
   7.349 +      SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
   7.350 +       (if !trace_sat then
   7.351 +          tracing ("Proof trace from SAT solver:\n" ^
   7.352 +            "clauses: " ^ ML_Syntax.print_list
   7.353 +              (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
   7.354 +              (Inttab.dest clause_table) ^ "\n" ^
   7.355 +            "empty clause: " ^ string_of_int empty_id)
   7.356 +        else ();
   7.357 +        if Config.get ctxt quick_and_dirty then
   7.358 +          make_quick_and_dirty_thm ()
   7.359 +        else
   7.360 +          let
   7.361 +            (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
   7.362 +            (*               this avoids accumulation of hypotheses during resolution    *)
   7.363 +            (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
   7.364 +            val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
   7.365 +            (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
   7.366 +            val cnf_cterm = cprop_of clauses_thm
   7.367 +            val cnf_thm = Thm.assume cnf_cterm
   7.368 +            (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
   7.369 +            val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
   7.370 +            (* initialize the clause array with the given clauses *)
   7.371 +            val max_idx = fst (the (Inttab.max clause_table))
   7.372 +            val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
   7.373 +            val _ =
   7.374 +              fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
   7.375 +                cnf_clauses 0
   7.376 +            (* replay the proof to derive the empty clause *)
   7.377 +            (* [c_1 && ... && c_n] |- False *)
   7.378 +            val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
   7.379 +          in
   7.380 +            (* [c_1, ..., c_n] |- False *)
   7.381 +            Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
   7.382 +          end)
   7.383 +    | SatSolver.UNSATISFIABLE NONE =>
   7.384 +        if Config.get ctxt quick_and_dirty then
   7.385 +         (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
   7.386 +          make_quick_and_dirty_thm ())
   7.387 +        else
   7.388 +          raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
   7.389 +    | SatSolver.SATISFIABLE assignment =>
   7.390 +        let
   7.391 +          val msg =
   7.392 +            "SAT solver found a countermodel:\n" ^
   7.393 +            (commas o map (fn (term, idx) =>
   7.394 +                Syntax.string_of_term_global @{theory} term ^ ": " ^
   7.395 +                  (case assignment idx of NONE => "arbitrary"
   7.396 +                  | SOME true => "true" | SOME false => "false")))
   7.397 +              (Termtab.dest atom_table)
   7.398 +        in
   7.399 +          raise THM (msg, 0, [])
   7.400 +        end
   7.401 +    | SatSolver.UNKNOWN =>
   7.402 +        raise THM ("SAT solver failed to decide the formula", 0, [])
   7.403 +  end;
   7.404 +
   7.405 +(* ------------------------------------------------------------------------- *)
   7.406 +(* Tactics                                                                   *)
   7.407 +(* ------------------------------------------------------------------------- *)
   7.408 +
   7.409 +(* ------------------------------------------------------------------------- *)
   7.410 +(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
   7.411 +(*      should be of the form                                                *)
   7.412 +(*        [| c1; c2; ...; ck |] ==> False                                    *)
   7.413 +(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
   7.414 +(*      or "True"                                                            *)
   7.415 +(* ------------------------------------------------------------------------- *)
   7.416 +
   7.417 +fun rawsat_tac ctxt i =
   7.418 +  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
   7.419 +    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
   7.420 +
   7.421 +(* ------------------------------------------------------------------------- *)
   7.422 +(* pre_cnf_tac: converts the i-th subgoal                                    *)
   7.423 +(*        [| A1 ; ... ; An |] ==> B                                          *)
   7.424 +(*      to                                                                   *)
   7.425 +(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
   7.426 +(*      (handling meta-logical connectives in B properly before negating),   *)
   7.427 +(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
   7.428 +(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
   7.429 +(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
   7.430 +(*      subgoal                                                              *)
   7.431 +(* ------------------------------------------------------------------------- *)
   7.432 +
   7.433 +fun pre_cnf_tac ctxt =
   7.434 +  rtac ccontr THEN'
   7.435 +  Object_Logic.atomize_prems_tac ctxt THEN'
   7.436 +  CONVERSION Drule.beta_eta_conversion;
   7.437 +
   7.438 +(* ------------------------------------------------------------------------- *)
   7.439 +(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
   7.440 +(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
   7.441 +(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
   7.442 +(*      subgoal                                                              *)
   7.443 +(* ------------------------------------------------------------------------- *)
   7.444 +
   7.445 +fun cnfsat_tac ctxt i =
   7.446 +  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
   7.447 +
   7.448 +(* ------------------------------------------------------------------------- *)
   7.449 +(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   7.450 +(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
   7.451 +(*      CNF formula becomes a separate premise) and existential quantifiers, *)
   7.452 +(*      then applies 'rawsat_tac' to solve the subgoal                       *)
   7.453 +(* ------------------------------------------------------------------------- *)
   7.454 +
   7.455 +fun cnfxsat_tac ctxt i =
   7.456 +  (etac FalseE i) ORELSE
   7.457 +    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
   7.458 +
   7.459 +(* ------------------------------------------------------------------------- *)
   7.460 +(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
   7.461 +(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
   7.462 +(*      an exponential blowup.                                               *)
   7.463 +(* ------------------------------------------------------------------------- *)
   7.464 +
   7.465 +fun sat_tac ctxt i =
   7.466 +  pre_cnf_tac ctxt i THEN CNF.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
   7.467 +
   7.468 +(* ------------------------------------------------------------------------- *)
   7.469 +(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   7.470 +(*      arbitrary formula.  The input is translated to CNF, possibly         *)
   7.471 +(*      introducing new literals.                                            *)
   7.472 +(* ------------------------------------------------------------------------- *)
   7.473 +
   7.474 +fun satx_tac ctxt i =
   7.475 +  pre_cnf_tac ctxt i THEN CNF.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
   7.476 +
   7.477 +end;
     8.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Feb 01 20:46:19 2014 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,474 +0,0 @@
     8.4 -(*  Title:      HOL/Tools/sat_funcs.ML
     8.5 -    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     8.6 -    Author:     Tjark Weber, TU Muenchen
     8.7 -
     8.8 -Proof reconstruction from SAT solvers.
     8.9 -
    8.10 -  Description:
    8.11 -    This file defines several tactics to invoke a proof-producing
    8.12 -    SAT solver on a propositional goal in clausal form.
    8.13 -
    8.14 -    We use a sequent presentation of clauses to speed up resolution
    8.15 -    proof reconstruction.
    8.16 -    We call such clauses "raw clauses", which are of the form
    8.17 -          [x1, ..., xn, P] |- False
    8.18 -    (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
    8.19 -    where each xi is a literal (see also comments in cnf_funcs.ML).
    8.20 -
    8.21 -    This does not work for goals containing schematic variables!
    8.22 -
    8.23 -      The tactic produces a clause representation of the given goal
    8.24 -      in DIMACS format and invokes a SAT solver, which should return
    8.25 -      a proof consisting of a sequence of resolution steps, indicating
    8.26 -      the two input clauses, and resulting in new clauses, leading to
    8.27 -      the empty clause (i.e. "False").  The tactic replays this proof
    8.28 -      in Isabelle and thus solves the overall goal.
    8.29 -
    8.30 -  There are three SAT tactics available.  They differ in the CNF transformation
    8.31 -  used. "sat_tac" uses naive CNF transformation to transform the theorem to be
    8.32 -  proved before giving it to the SAT solver.  The naive transformation in the
    8.33 -  worst case can lead to an exponential blow up in formula size.  Another
    8.34 -  tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
    8.35 -  produce a formula of linear size increase compared to the input formula, at
    8.36 -  the cost of possibly introducing new variables.  See cnf_funcs.ML for more
    8.37 -  comments on the CNF transformation.  "rawsat_tac" should be used with
    8.38 -  caution: no CNF transformation is performed, and the tactic's behavior is
    8.39 -  undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
    8.40 -  where each Ci is a disjunction.
    8.41 -
    8.42 -  The SAT solver to be used can be set via the "solver" reference.  See
    8.43 -  sat_solvers.ML for possible values, and etc/settings for required (solver-
    8.44 -  dependent) configuration settings.  To replay SAT proofs in Isabelle, you
    8.45 -  must of course use a proof-producing SAT solver in the first place.
    8.46 -
    8.47 -  Proofs are replayed only if "quick_and_dirty" is false.  If
    8.48 -  "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
    8.49 -  negation to be unsatisfiable) is proved via an oracle.
    8.50 -*)
    8.51 -
    8.52 -signature SAT =
    8.53 -sig
    8.54 -  val trace_sat: bool Unsynchronized.ref    (* input: print trace messages *)
    8.55 -  val solver: string Unsynchronized.ref  (* input: name of SAT solver to be used *)
    8.56 -  val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
    8.57 -  val rawsat_thm: Proof.context -> cterm list -> thm
    8.58 -  val rawsat_tac: Proof.context -> int -> tactic
    8.59 -  val sat_tac: Proof.context -> int -> tactic
    8.60 -  val satx_tac: Proof.context -> int -> tactic
    8.61 -end
    8.62 -
    8.63 -functor SATFunc(cnf : CNF) : SAT =
    8.64 -struct
    8.65 -
    8.66 -val trace_sat = Unsynchronized.ref false;
    8.67 -
    8.68 -val solver = Unsynchronized.ref "zchaff_with_proofs";
    8.69 -  (*see HOL/Tools/sat_solver.ML for possible values*)
    8.70 -
    8.71 -val counter = Unsynchronized.ref 0;
    8.72 -
    8.73 -val resolution_thm =
    8.74 -  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
    8.75 -
    8.76 -val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
    8.77 -
    8.78 -(* ------------------------------------------------------------------------- *)
    8.79 -(* lit_ord: an order on integers that considers their absolute values only,  *)
    8.80 -(*      thereby treating integers that represent the same atom (positively   *)
    8.81 -(*      or negatively) as equal                                              *)
    8.82 -(* ------------------------------------------------------------------------- *)
    8.83 -
    8.84 -fun lit_ord (i, j) = int_ord (abs i, abs j);
    8.85 -
    8.86 -(* ------------------------------------------------------------------------- *)
    8.87 -(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
    8.88 -(*      distinguished:                                                       *)
    8.89 -(*      1. NO_CLAUSE: clause not proved (yet)                                *)
    8.90 -(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
    8.91 -(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
    8.92 -(*         (a mapping from int's to its literals) for faster proof           *)
    8.93 -(*         reconstruction                                                    *)
    8.94 -(* ------------------------------------------------------------------------- *)
    8.95 -
    8.96 -datatype CLAUSE =
    8.97 -    NO_CLAUSE
    8.98 -  | ORIG_CLAUSE of thm
    8.99 -  | RAW_CLAUSE of thm * (int * cterm) list;
   8.100 -
   8.101 -(* ------------------------------------------------------------------------- *)
   8.102 -(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
   8.103 -(*      resolution over the list (starting with its head), i.e. with two raw *)
   8.104 -(*      clauses                                                              *)
   8.105 -(*        [P, x1, ..., a, ..., xn] |- False                                  *)
   8.106 -(*      and                                                                  *)
   8.107 -(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
   8.108 -(*      (where a and a' are dual to each other), we convert the first clause *)
   8.109 -(*      to                                                                   *)
   8.110 -(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
   8.111 -(*      the second clause to                                                 *)
   8.112 -(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
   8.113 -(*      and then perform resolution with                                     *)
   8.114 -(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
   8.115 -(*      to produce                                                           *)
   8.116 -(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
   8.117 -(*      Each clause is accompanied with an association list mapping integers *)
   8.118 -(*      (positive for positive literals, negative for negative literals, and *)
   8.119 -(*      the same absolute value for dual literals) to the actual literals as *)
   8.120 -(*      cterms.                                                              *)
   8.121 -(* ------------------------------------------------------------------------- *)
   8.122 -
   8.123 -fun resolve_raw_clauses _ [] =
   8.124 -      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   8.125 -  | resolve_raw_clauses ctxt (c::cs) =
   8.126 -      let
   8.127 -        (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
   8.128 -        fun merge xs [] = xs
   8.129 -          | merge [] ys = ys
   8.130 -          | merge (x :: xs) (y :: ys) =
   8.131 -              (case (lit_ord o pairself fst) (x, y) of
   8.132 -                LESS => x :: merge xs (y :: ys)
   8.133 -              | EQUAL => x :: merge xs ys
   8.134 -              | GREATER => y :: merge (x :: xs) ys)
   8.135 -
   8.136 -        (* find out which two hyps are used in the resolution *)
   8.137 -        fun find_res_hyps ([], _) _ =
   8.138 -              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   8.139 -          | find_res_hyps (_, []) _ =
   8.140 -              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   8.141 -          | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
   8.142 -              (case (lit_ord o pairself fst) (h1, h2) of
   8.143 -                LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
   8.144 -              | EQUAL =>
   8.145 -                  let
   8.146 -                    val (i1, chyp1) = h1
   8.147 -                    val (i2, chyp2) = h2
   8.148 -                  in
   8.149 -                    if i1 = ~ i2 then
   8.150 -                      (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
   8.151 -                    else (* i1 = i2 *)
   8.152 -                      find_res_hyps (hyps1, hyps2) (h1 :: acc)
   8.153 -                  end
   8.154 -          | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
   8.155 -
   8.156 -        fun resolution (c1, hyps1) (c2, hyps2) =
   8.157 -          let
   8.158 -            val _ =
   8.159 -              if ! trace_sat then  (* FIXME !? *)
   8.160 -                tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
   8.161 -                  " (hyps: " ^ ML_Syntax.print_list
   8.162 -                    (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
   8.163 -                  ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
   8.164 -                  " (hyps: " ^ ML_Syntax.print_list
   8.165 -                    (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
   8.166 -              else ()
   8.167 -
   8.168 -            (* the two literals used for resolution *)
   8.169 -            val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
   8.170 -
   8.171 -            val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
   8.172 -            val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
   8.173 -
   8.174 -            val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
   8.175 -              let
   8.176 -                val cLit =
   8.177 -                  snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
   8.178 -              in
   8.179 -                Thm.instantiate ([], [(cP, cLit)]) resolution_thm
   8.180 -              end
   8.181 -
   8.182 -            val _ =
   8.183 -              if !trace_sat then
   8.184 -                tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
   8.185 -              else ()
   8.186 -
   8.187 -            (* Gamma1, Gamma2 |- False *)
   8.188 -            val c_new =
   8.189 -              Thm.implies_elim
   8.190 -                (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
   8.191 -                (if hyp1_is_neg then c1' else c2')
   8.192 -
   8.193 -            val _ =
   8.194 -              if !trace_sat then
   8.195 -                tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
   8.196 -                  " (hyps: " ^ ML_Syntax.print_list
   8.197 -                      (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
   8.198 -              else ()
   8.199 -            val _ = Unsynchronized.inc counter
   8.200 -          in
   8.201 -            (c_new, new_hyps)
   8.202 -          end
   8.203 -        in
   8.204 -          fold resolution cs c
   8.205 -        end;
   8.206 -
   8.207 -(* ------------------------------------------------------------------------- *)
   8.208 -(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
   8.209 -(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
   8.210 -(*      'clauses' array with derived clauses, and returns the derived clause *)
   8.211 -(*      at index 'empty_id' (which should just be "False" if proof           *)
   8.212 -(*      reconstruction was successful, with the used clauses as hyps).       *)
   8.213 -(*      'atom_table' must contain an injective mapping from all atoms that   *)
   8.214 -(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
   8.215 -(* ------------------------------------------------------------------------- *)
   8.216 -
   8.217 -fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
   8.218 -  let
   8.219 -    fun index_of_literal chyp =
   8.220 -      (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
   8.221 -        (Const (@{const_name Not}, _) $ atom) =>
   8.222 -          SOME (~ (the (Termtab.lookup atom_table atom)))
   8.223 -      | atom => SOME (the (Termtab.lookup atom_table atom)))
   8.224 -      handle TERM _ => NONE;  (* 'chyp' is not a literal *)
   8.225 -
   8.226 -    fun prove_clause id =
   8.227 -      (case Array.sub (clauses, id) of
   8.228 -        RAW_CLAUSE clause => clause
   8.229 -      | ORIG_CLAUSE thm =>
   8.230 -          (* convert the original clause *)
   8.231 -          let
   8.232 -            val _ =
   8.233 -              if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
   8.234 -            val raw = cnf.clause2raw_thm thm
   8.235 -            val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
   8.236 -              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
   8.237 -            val clause = (raw, hyps)
   8.238 -            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   8.239 -          in
   8.240 -            clause
   8.241 -          end
   8.242 -      | NO_CLAUSE =>
   8.243 -          (* prove the clause, using information from 'clause_table' *)
   8.244 -          let
   8.245 -            val _ =
   8.246 -              if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
   8.247 -            val ids = the (Inttab.lookup clause_table id)
   8.248 -            val clause = resolve_raw_clauses ctxt (map prove_clause ids)
   8.249 -            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   8.250 -            val _ =
   8.251 -              if !trace_sat then
   8.252 -                tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
   8.253 -              else ()
   8.254 -          in
   8.255 -            clause
   8.256 -          end)
   8.257 -
   8.258 -    val _ = counter := 0
   8.259 -    val empty_clause = fst (prove_clause empty_id)
   8.260 -    val _ =
   8.261 -      if !trace_sat then
   8.262 -        tracing ("Proof reconstruction successful; " ^
   8.263 -          string_of_int (!counter) ^ " resolution step(s) total.")
   8.264 -      else ()
   8.265 -  in
   8.266 -    empty_clause
   8.267 -  end;
   8.268 -
   8.269 -(* ------------------------------------------------------------------------- *)
   8.270 -(* string_of_prop_formula: return a human-readable string representation of  *)
   8.271 -(*      a 'prop_formula' (just for tracing)                                  *)
   8.272 -(* ------------------------------------------------------------------------- *)
   8.273 -
   8.274 -fun string_of_prop_formula Prop_Logic.True = "True"
   8.275 -  | string_of_prop_formula Prop_Logic.False = "False"
   8.276 -  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
   8.277 -  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
   8.278 -  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
   8.279 -      "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   8.280 -  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
   8.281 -      "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
   8.282 -
   8.283 -(* ------------------------------------------------------------------------- *)
   8.284 -(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   8.285 -(*      a proof from the resulting proof trace of the SAT solver.  The       *)
   8.286 -(*      theorem returned is just "False" (with some of the given clauses as  *)
   8.287 -(*      hyps).                                                               *)
   8.288 -(* ------------------------------------------------------------------------- *)
   8.289 -
   8.290 -fun rawsat_thm ctxt clauses =
   8.291 -  let
   8.292 -    (* remove premises that equal "True" *)
   8.293 -    val clauses' = filter (fn clause =>
   8.294 -      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
   8.295 -        handle TERM ("dest_Trueprop", _) => true) clauses
   8.296 -    (* remove non-clausal premises -- of course this shouldn't actually   *)
   8.297 -    (* remove anything as long as 'rawsat_tac' is only called after the   *)
   8.298 -    (* premises have been converted to clauses                            *)
   8.299 -    val clauses'' = filter (fn clause =>
   8.300 -      ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
   8.301 -        handle TERM ("dest_Trueprop", _) => false)
   8.302 -      orelse (
   8.303 -        warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
   8.304 -        false)) clauses'
   8.305 -    (* remove trivial clauses -- this is necessary because zChaff removes *)
   8.306 -    (* trivial clauses during preprocessing, and otherwise our clause     *)
   8.307 -    (* numbering would be off                                             *)
   8.308 -    val nontrivial_clauses =
   8.309 -      filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
   8.310 -    (* sort clauses according to the term order -- an optimization,       *)
   8.311 -    (* useful because forming the union of hypotheses, as done by         *)
   8.312 -    (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
   8.313 -    (* terms sorted in descending order, while only linear for terms      *)
   8.314 -    (* sorted in ascending order                                          *)
   8.315 -    val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   8.316 -    val _ =
   8.317 -      if !trace_sat then
   8.318 -        tracing ("Sorted non-trivial clauses:\n" ^
   8.319 -          cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
   8.320 -      else ()
   8.321 -    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
   8.322 -    val (fms, atom_table) =
   8.323 -      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
   8.324 -        sorted_clauses Termtab.empty
   8.325 -    val _ =
   8.326 -      if !trace_sat then
   8.327 -        tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
   8.328 -      else ()
   8.329 -    val fm = Prop_Logic.all fms
   8.330 -    fun make_quick_and_dirty_thm () =
   8.331 -      let
   8.332 -        val _ =
   8.333 -          if !trace_sat then
   8.334 -            tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   8.335 -          else ()
   8.336 -        val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
   8.337 -      in
   8.338 -        (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   8.339 -        (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
   8.340 -        (* clauses in ascending order (which is linear for                  *)
   8.341 -        (* 'Conjunction.intr_balanced', used below)                         *)
   8.342 -        fold Thm.weaken (rev sorted_clauses) False_thm
   8.343 -      end
   8.344 -  in
   8.345 -    case
   8.346 -      let val the_solver = ! solver
   8.347 -      in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
   8.348 -    of
   8.349 -      SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
   8.350 -       (if !trace_sat then
   8.351 -          tracing ("Proof trace from SAT solver:\n" ^
   8.352 -            "clauses: " ^ ML_Syntax.print_list
   8.353 -              (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
   8.354 -              (Inttab.dest clause_table) ^ "\n" ^
   8.355 -            "empty clause: " ^ string_of_int empty_id)
   8.356 -        else ();
   8.357 -        if Config.get ctxt quick_and_dirty then
   8.358 -          make_quick_and_dirty_thm ()
   8.359 -        else
   8.360 -          let
   8.361 -            (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
   8.362 -            (*               this avoids accumulation of hypotheses during resolution    *)
   8.363 -            (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
   8.364 -            val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
   8.365 -            (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
   8.366 -            val cnf_cterm = cprop_of clauses_thm
   8.367 -            val cnf_thm = Thm.assume cnf_cterm
   8.368 -            (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
   8.369 -            val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
   8.370 -            (* initialize the clause array with the given clauses *)
   8.371 -            val max_idx = fst (the (Inttab.max clause_table))
   8.372 -            val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
   8.373 -            val _ =
   8.374 -              fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
   8.375 -                cnf_clauses 0
   8.376 -            (* replay the proof to derive the empty clause *)
   8.377 -            (* [c_1 && ... && c_n] |- False *)
   8.378 -            val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
   8.379 -          in
   8.380 -            (* [c_1, ..., c_n] |- False *)
   8.381 -            Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
   8.382 -          end)
   8.383 -    | SatSolver.UNSATISFIABLE NONE =>
   8.384 -        if Config.get ctxt quick_and_dirty then
   8.385 -         (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
   8.386 -          make_quick_and_dirty_thm ())
   8.387 -        else
   8.388 -          raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
   8.389 -    | SatSolver.SATISFIABLE assignment =>
   8.390 -        let
   8.391 -          val msg =
   8.392 -            "SAT solver found a countermodel:\n" ^
   8.393 -            (commas o map (fn (term, idx) =>
   8.394 -                Syntax.string_of_term_global @{theory} term ^ ": " ^
   8.395 -                  (case assignment idx of NONE => "arbitrary"
   8.396 -                  | SOME true => "true" | SOME false => "false")))
   8.397 -              (Termtab.dest atom_table)
   8.398 -        in
   8.399 -          raise THM (msg, 0, [])
   8.400 -        end
   8.401 -    | SatSolver.UNKNOWN =>
   8.402 -        raise THM ("SAT solver failed to decide the formula", 0, [])
   8.403 -  end;
   8.404 -
   8.405 -(* ------------------------------------------------------------------------- *)
   8.406 -(* Tactics                                                                   *)
   8.407 -(* ------------------------------------------------------------------------- *)
   8.408 -
   8.409 -(* ------------------------------------------------------------------------- *)
   8.410 -(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
   8.411 -(*      should be of the form                                                *)
   8.412 -(*        [| c1; c2; ...; ck |] ==> False                                    *)
   8.413 -(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
   8.414 -(*      or "True"                                                            *)
   8.415 -(* ------------------------------------------------------------------------- *)
   8.416 -
   8.417 -fun rawsat_tac ctxt i =
   8.418 -  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
   8.419 -    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
   8.420 -
   8.421 -(* ------------------------------------------------------------------------- *)
   8.422 -(* pre_cnf_tac: converts the i-th subgoal                                    *)
   8.423 -(*        [| A1 ; ... ; An |] ==> B                                          *)
   8.424 -(*      to                                                                   *)
   8.425 -(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
   8.426 -(*      (handling meta-logical connectives in B properly before negating),   *)
   8.427 -(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
   8.428 -(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
   8.429 -(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
   8.430 -(*      subgoal                                                              *)
   8.431 -(* ------------------------------------------------------------------------- *)
   8.432 -
   8.433 -fun pre_cnf_tac ctxt =
   8.434 -  rtac ccontr THEN'
   8.435 -  Object_Logic.atomize_prems_tac ctxt THEN'
   8.436 -  CONVERSION Drule.beta_eta_conversion;
   8.437 -
   8.438 -(* ------------------------------------------------------------------------- *)
   8.439 -(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
   8.440 -(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
   8.441 -(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
   8.442 -(*      subgoal                                                              *)
   8.443 -(* ------------------------------------------------------------------------- *)
   8.444 -
   8.445 -fun cnfsat_tac ctxt i =
   8.446 -  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
   8.447 -
   8.448 -(* ------------------------------------------------------------------------- *)
   8.449 -(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   8.450 -(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
   8.451 -(*      CNF formula becomes a separate premise) and existential quantifiers, *)
   8.452 -(*      then applies 'rawsat_tac' to solve the subgoal                       *)
   8.453 -(* ------------------------------------------------------------------------- *)
   8.454 -
   8.455 -fun cnfxsat_tac ctxt i =
   8.456 -  (etac FalseE i) ORELSE
   8.457 -    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
   8.458 -
   8.459 -(* ------------------------------------------------------------------------- *)
   8.460 -(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
   8.461 -(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
   8.462 -(*      an exponential blowup.                                               *)
   8.463 -(* ------------------------------------------------------------------------- *)
   8.464 -
   8.465 -fun sat_tac ctxt i =
   8.466 -  pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
   8.467 -
   8.468 -(* ------------------------------------------------------------------------- *)
   8.469 -(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   8.470 -(*      arbitrary formula.  The input is translated to CNF, possibly         *)
   8.471 -(*      introducing new literals.                                            *)
   8.472 -(* ------------------------------------------------------------------------- *)
   8.473 -
   8.474 -fun satx_tac ctxt i =
   8.475 -  pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
   8.476 -
   8.477 -end;
     9.1 --- a/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 20:46:19 2014 +0100
     9.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 21:09:53 2014 +0100
     9.3 @@ -8,9 +8,9 @@
     9.4  theory SAT_Examples imports Main
     9.5  begin
     9.6  
     9.7 -(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
     9.8 -(* ML {* sat.solver := "minisat_with_proofs"; *} *)
     9.9 -ML {* sat.trace_sat := true; *}
    9.10 +(* ML {* SAT.solver := "zchaff_with_proofs"; *} *)
    9.11 +(* ML {* SAT.solver := "minisat_with_proofs"; *} *)
    9.12 +ML {* SAT.trace_sat := true; *}
    9.13  declare [[quick_and_dirty]]
    9.14  
    9.15  lemma "True"
    9.16 @@ -24,13 +24,13 @@
    9.17  
    9.18  lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    9.19  (*
    9.20 -apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    9.21 +apply (tactic {* CNF.cnf_rewrite_tac 1 *})
    9.22  *)
    9.23  by sat
    9.24  
    9.25  lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    9.26  (*
    9.27 -apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    9.28 +apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
    9.29  apply (erule exE | erule conjE)+
    9.30  *)
    9.31  by satx
    9.32 @@ -38,14 +38,14 @@
    9.33  lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
    9.34    \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    9.35  (*
    9.36 -apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    9.37 +apply (tactic {* CNF.cnf_rewrite_tac 1 *})
    9.38  *)
    9.39  by sat
    9.40  
    9.41  lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
    9.42    \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    9.43  (*
    9.44 -apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    9.45 +apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
    9.46  apply (erule exE | erule conjE)+
    9.47  *)
    9.48  by satx
    9.49 @@ -77,11 +77,11 @@
    9.50  lemma "(ALL x. P x) | ~ All P"
    9.51  by sat
    9.52  
    9.53 -ML {* sat.trace_sat := false; *}
    9.54 +ML {* SAT.trace_sat := false; *}
    9.55  declare [[quick_and_dirty = false]]
    9.56  
    9.57  method_setup rawsat = {*
    9.58 -  Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
    9.59 +  Scan.succeed (SIMPLE_METHOD' o SAT.rawsat_tac)
    9.60  *} "SAT solver (no preprocessing)"
    9.61  
    9.62  (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
    9.63 @@ -520,26 +520,26 @@
    9.64  *}
    9.65  
    9.66  (* ML {*
    9.67 -sat.solver := "zchaff_with_proofs";
    9.68 -sat.trace_sat := false;
    9.69 +SAT.solver := "zchaff_with_proofs";
    9.70 +SAT.trace_sat := false;
    9.71  *}
    9.72  declare [[quick_and_dirty = false]]
    9.73  *)
    9.74  
    9.75  ML {*
    9.76 -fun benchmark dimacsfile =
    9.77 -let
    9.78 -  val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
    9.79 -  fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
    9.80 -    | and_to_list fm acc = rev (fm :: acc)
    9.81 -  val clauses = and_to_list prop_fm []
    9.82 -  val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
    9.83 -  val cterms = map (Thm.cterm_of @{theory}) terms
    9.84 -  val start = Timing.start ()
    9.85 -  val _ = sat.rawsat_thm @{context} cterms
    9.86 -in
    9.87 -  (Timing.result start, ! sat.counter)
    9.88 -end;
    9.89 +  fun benchmark dimacsfile =
    9.90 +    let
    9.91 +      val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
    9.92 +      fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
    9.93 +        | and_to_list fm acc = rev (fm :: acc)
    9.94 +      val clauses = and_to_list prop_fm []
    9.95 +      val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
    9.96 +      val cterms = map (Thm.cterm_of @{theory}) terms
    9.97 +      val start = Timing.start ()
    9.98 +      val _ = SAT.rawsat_thm @{context} cterms
    9.99 +    in
   9.100 +      (Timing.result start, ! SAT.counter)
   9.101 +    end;
   9.102  *}
   9.103  
   9.104  end