merged
authorwenzelm
Sat Feb 01 22:02:20 2014 +0100 (2014-02-01)
changeset 55241ef601c60ccbe
parent 55238 7ddb889e23bd
parent 55240 efc4c0e0e14a
child 55242 413ec965f95d
merged
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/sat_funcs.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Feb 01 20:38:29 2014 +0000
     1.2 +++ b/src/HOL/HOL.thy	Sat Feb 01 22:02:20 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/ROOT	Sat Feb 01 20:38:29 2014 +0000
     2.2 +++ b/src/HOL/ROOT	Sat Feb 01 22:02:20 2014 +0100
     2.3 @@ -572,8 +572,7 @@
     2.4      Sudoku
     2.5  (* FIXME
     2.6  (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
     2.7 -(*global side-effects ahead!*)
     2.8 -try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
     2.9 +    SAT_Examples
    2.10  *)
    2.11    files "document/root.bib" "document/root.tex"
    2.12  
     3.1 --- a/src/HOL/SAT.thy	Sat Feb 01 20:38:29 2014 +0000
     3.2 +++ b/src/HOL/SAT.thy	Sat Feb 01 22:02:20 2014 +0100
     3.3 @@ -13,14 +13,12 @@
     3.4  
     3.5  ML_file "Tools/prop_logic.ML"
     3.6  ML_file "Tools/sat_solver.ML"
     3.7 -ML_file "Tools/sat_funcs.ML"
     3.8 +ML_file "Tools/sat.ML"
     3.9  
    3.10 -ML {* structure sat = SATFunc(cnf) *}
    3.11 -
    3.12 -method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
    3.13 +method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac) *}
    3.14    "SAT solver"
    3.15  
    3.16 -method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
    3.17 +method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac) *}
    3.18    "SAT solver (with definitional CNF)"
    3.19  
    3.20  end
     4.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Feb 01 20:38:29 2014 +0000
     4.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sat Feb 01 22:02:20 2014 +0100
     4.3 @@ -222,7 +222,7 @@
     4.4  
     4.5  fun to_definitional_cnf_with_quantifiers ctxt th =
     4.6    let
     4.7 -    val eqth = cnf.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
     4.8 +    val eqth = CNF.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
     4.9      val eqth = eqth RS @{thm eq_reflection}
    4.10      val eqth = eqth RS @{thm TruepropI}
    4.11    in Thm.equal_elim eqth th end
     5.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 20:38:29 2014 +0000
     5.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 22:02:20 2014 +0100
     5.3 @@ -245,7 +245,7 @@
     5.4    (if exists (Meson.has_too_many_clauses ctxt)
     5.5               (Logic.prems_of_goal (prop_of st0) 1) then
     5.6       Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1
     5.7 -     THEN cnf.cnfx_rewrite_tac ctxt 1
     5.8 +     THEN CNF.cnfx_rewrite_tac ctxt 1
     5.9     else
    5.10       all_tac) st0
    5.11  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/cnf.ML	Sat Feb 01 22:02:20 2014 +0100
     6.3 @@ -0,0 +1,579 @@
     6.4 +(*  Title:      HOL/Tools/cnf.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 --- a/src/HOL/Tools/cnf_funcs.ML	Sat Feb 01 20:38:29 2014 +0000
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,579 +0,0 @@
     7.4 -(*  Title:      HOL/Tools/cnf_funcs.ML
     7.5 -    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     7.6 -    Author:     Tjark Weber, TU Muenchen
     7.7 -
     7.8 -FIXME: major overlaps with the code in meson.ML
     7.9 -
    7.10 -Functions and tactics to transform a formula into Conjunctive Normal
    7.11 -Form (CNF).
    7.12 -
    7.13 -A formula in CNF is of the following form:
    7.14 -
    7.15 -    (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
    7.16 -    False
    7.17 -    True
    7.18 -
    7.19 -where each xij is a literal (a positive or negative atomic Boolean
    7.20 -term), i.e. the formula is a conjunction of disjunctions of literals,
    7.21 -or "False", or "True".
    7.22 -
    7.23 -A (non-empty) disjunction of literals is referred to as "clause".
    7.24 -
    7.25 -For the purpose of SAT proof reconstruction, we also make use of
    7.26 -another representation of clauses, which we call the "raw clauses".
    7.27 -Raw clauses are of the form
    7.28 -
    7.29 -    [..., x1', x2', ..., xn'] |- False ,
    7.30 -
    7.31 -where each xi is a literal, and each xi' is the negation normal form
    7.32 -of ~xi.
    7.33 -
    7.34 -Literals are successively removed from the hyps of raw clauses by
    7.35 -resolution during SAT proof reconstruction.
    7.36 -*)
    7.37 -
    7.38 -signature CNF =
    7.39 -sig
    7.40 -  val is_atom: term -> bool
    7.41 -  val is_literal: term -> bool
    7.42 -  val is_clause: term -> bool
    7.43 -  val clause_is_trivial: term -> bool
    7.44 -
    7.45 -  val clause2raw_thm: thm -> thm
    7.46 -  val make_nnf_thm: theory -> term -> thm
    7.47 -
    7.48 -  val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
    7.49 -
    7.50 -  val make_cnf_thm: Proof.context -> term -> thm
    7.51 -  val make_cnfx_thm: Proof.context -> term -> thm
    7.52 -  val cnf_rewrite_tac: Proof.context -> int -> tactic  (* converts all prems of a subgoal to CNF *)
    7.53 -  val cnfx_rewrite_tac: Proof.context -> int -> tactic
    7.54 -    (* converts all prems of a subgoal to (almost) definitional CNF *)
    7.55 -end;
    7.56 -
    7.57 -structure cnf : CNF =
    7.58 -struct
    7.59 -
    7.60 -val clause2raw_notE      = @{lemma "[| P; ~P |] ==> False" by auto};
    7.61 -val clause2raw_not_disj  = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
    7.62 -val clause2raw_not_not   = @{lemma "P ==> ~~P" by auto};
    7.63 -
    7.64 -val iff_refl             = @{lemma "(P::bool) = P" by auto};
    7.65 -val iff_trans            = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
    7.66 -val conj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
    7.67 -val disj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
    7.68 -
    7.69 -val make_nnf_imp         = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
    7.70 -val make_nnf_iff         = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
    7.71 -val make_nnf_not_false   = @{lemma "(~False) = True" by auto};
    7.72 -val make_nnf_not_true    = @{lemma "(~True) = False" by auto};
    7.73 -val make_nnf_not_conj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
    7.74 -val make_nnf_not_disj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
    7.75 -val make_nnf_not_imp     = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
    7.76 -val make_nnf_not_iff     = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
    7.77 -val make_nnf_not_not     = @{lemma "P = P' ==> (~~P) = P'" by auto};
    7.78 -
    7.79 -val simp_TF_conj_True_l  = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
    7.80 -val simp_TF_conj_True_r  = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
    7.81 -val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
    7.82 -val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
    7.83 -val simp_TF_disj_True_l  = @{lemma "P = True ==> (P | Q) = True" by auto};
    7.84 -val simp_TF_disj_True_r  = @{lemma "Q = True ==> (P | Q) = True" by auto};
    7.85 -val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
    7.86 -val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
    7.87 -
    7.88 -val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
    7.89 -val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
    7.90 -
    7.91 -val make_cnfx_disj_ex_l  = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
    7.92 -val make_cnfx_disj_ex_r  = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
    7.93 -val make_cnfx_newlit     = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
    7.94 -val make_cnfx_ex_cong    = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
    7.95 -
    7.96 -val weakening_thm        = @{lemma "[| P; Q |] ==> Q" by auto};
    7.97 -
    7.98 -val cnftac_eq_imp        = @{lemma "[| P = Q; P |] ==> Q" by auto};
    7.99 -
   7.100 -fun is_atom (Const (@{const_name False}, _)) = false
   7.101 -  | is_atom (Const (@{const_name True}, _)) = false
   7.102 -  | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
   7.103 -  | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
   7.104 -  | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
   7.105 -  | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
   7.106 -  | is_atom (Const (@{const_name Not}, _) $ _) = false
   7.107 -  | is_atom _ = true;
   7.108 -
   7.109 -fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   7.110 -  | is_literal x = is_atom x;
   7.111 -
   7.112 -fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
   7.113 -  | is_clause x = is_literal x;
   7.114 -
   7.115 -(* ------------------------------------------------------------------------- *)
   7.116 -(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
   7.117 -(*      and the atom's negation                                              *)
   7.118 -(* ------------------------------------------------------------------------- *)
   7.119 -
   7.120 -fun clause_is_trivial c =
   7.121 -  let
   7.122 -    fun dual (Const (@{const_name Not}, _) $ x) = x
   7.123 -      | dual x = HOLogic.Not $ x
   7.124 -    fun has_duals [] = false
   7.125 -      | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
   7.126 -  in
   7.127 -    has_duals (HOLogic.disjuncts c)
   7.128 -  end;
   7.129 -
   7.130 -(* ------------------------------------------------------------------------- *)
   7.131 -(* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
   7.132 -(*        [...] |- x1 | ... | xn                                             *)
   7.133 -(*      (where each xi is a literal) is translated to                        *)
   7.134 -(*        [..., x1', ..., xn'] |- False ,                                    *)
   7.135 -(*      where each xi' is the negation normal form of ~xi                    *)
   7.136 -(* ------------------------------------------------------------------------- *)
   7.137 -
   7.138 -fun clause2raw_thm clause =
   7.139 -  let
   7.140 -    (* eliminates negated disjunctions from the i-th premise, possibly *)
   7.141 -    (* adding new premises, then continues with the (i+1)-th premise   *)
   7.142 -    (* int -> Thm.thm -> Thm.thm *)
   7.143 -    fun not_disj_to_prem i thm =
   7.144 -      if i > nprems_of thm then
   7.145 -        thm
   7.146 -      else
   7.147 -        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
   7.148 -    (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
   7.149 -    (* becomes "[..., A1, ..., An] |- B"                                   *)
   7.150 -    (* Thm.thm -> Thm.thm *)
   7.151 -    fun prems_to_hyps thm =
   7.152 -      fold (fn cprem => fn thm' =>
   7.153 -        Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
   7.154 -  in
   7.155 -    (* [...] |- ~(x1 | ... | xn) ==> False *)
   7.156 -    (clause2raw_notE OF [clause])
   7.157 -    (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
   7.158 -    |> not_disj_to_prem 1
   7.159 -    (* [...] |- x1' ==> ... ==> xn' ==> False *)
   7.160 -    |> Seq.hd o TRYALL (rtac clause2raw_not_not)
   7.161 -    (* [..., x1', ..., xn'] |- False *)
   7.162 -    |> prems_to_hyps
   7.163 -  end;
   7.164 -
   7.165 -(* ------------------------------------------------------------------------- *)
   7.166 -(* inst_thm: instantiates a theorem with a list of terms                     *)
   7.167 -(* ------------------------------------------------------------------------- *)
   7.168 -
   7.169 -fun inst_thm thy ts thm =
   7.170 -  instantiate' [] (map (SOME o cterm_of thy) ts) thm;
   7.171 -
   7.172 -(* ------------------------------------------------------------------------- *)
   7.173 -(*                         Naive CNF transformation                          *)
   7.174 -(* ------------------------------------------------------------------------- *)
   7.175 -
   7.176 -(* ------------------------------------------------------------------------- *)
   7.177 -(* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
   7.178 -(*      negation normal form (i.e. negation only occurs in front of atoms)   *)
   7.179 -(*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
   7.180 -(*      eliminated (possibly causing an exponential blowup)                  *)
   7.181 -(* ------------------------------------------------------------------------- *)
   7.182 -
   7.183 -fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   7.184 -      let
   7.185 -        val thm1 = make_nnf_thm thy x
   7.186 -        val thm2 = make_nnf_thm thy y
   7.187 -      in
   7.188 -        conj_cong OF [thm1, thm2]
   7.189 -      end
   7.190 -  | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   7.191 -      let
   7.192 -        val thm1 = make_nnf_thm thy x
   7.193 -        val thm2 = make_nnf_thm thy y
   7.194 -      in
   7.195 -        disj_cong OF [thm1, thm2]
   7.196 -      end
   7.197 -  | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
   7.198 -      let
   7.199 -        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   7.200 -        val thm2 = make_nnf_thm thy y
   7.201 -      in
   7.202 -        make_nnf_imp OF [thm1, thm2]
   7.203 -      end
   7.204 -  | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
   7.205 -      let
   7.206 -        val thm1 = make_nnf_thm thy x
   7.207 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   7.208 -        val thm3 = make_nnf_thm thy y
   7.209 -        val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   7.210 -      in
   7.211 -        make_nnf_iff OF [thm1, thm2, thm3, thm4]
   7.212 -      end
   7.213 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
   7.214 -      make_nnf_not_false
   7.215 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
   7.216 -      make_nnf_not_true
   7.217 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
   7.218 -      let
   7.219 -        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   7.220 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   7.221 -      in
   7.222 -        make_nnf_not_conj OF [thm1, thm2]
   7.223 -      end
   7.224 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
   7.225 -      let
   7.226 -        val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   7.227 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   7.228 -      in
   7.229 -        make_nnf_not_disj OF [thm1, thm2]
   7.230 -      end
   7.231 -  | make_nnf_thm thy
   7.232 -      (Const (@{const_name Not}, _) $
   7.233 -        (Const (@{const_name HOL.implies}, _) $ x $ y)) =
   7.234 -      let
   7.235 -        val thm1 = make_nnf_thm thy x
   7.236 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   7.237 -      in
   7.238 -        make_nnf_not_imp OF [thm1, thm2]
   7.239 -      end
   7.240 -  | make_nnf_thm thy
   7.241 -      (Const (@{const_name Not}, _) $
   7.242 -        (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   7.243 -      let
   7.244 -        val thm1 = make_nnf_thm thy x
   7.245 -        val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   7.246 -        val thm3 = make_nnf_thm thy y
   7.247 -        val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   7.248 -      in
   7.249 -        make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
   7.250 -      end
   7.251 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
   7.252 -      let
   7.253 -        val thm1 = make_nnf_thm thy x
   7.254 -      in
   7.255 -        make_nnf_not_not OF [thm1]
   7.256 -      end
   7.257 -  | make_nnf_thm thy t = inst_thm thy [t] iff_refl;
   7.258 -
   7.259 -val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
   7.260 -val eq_reflection = @{thm eq_reflection}
   7.261 -
   7.262 -fun make_under_quantifiers ctxt make t =
   7.263 -  let
   7.264 -    val thy = Proof_Context.theory_of ctxt
   7.265 -    fun conv ctxt ct =
   7.266 -      case term_of ct of
   7.267 -        Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
   7.268 -      | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
   7.269 -      | Const _ => Conv.all_conv ct
   7.270 -      | t => make t RS eq_reflection
   7.271 -  in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
   7.272 -
   7.273 -fun make_nnf_thm_under_quantifiers ctxt =
   7.274 -  make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
   7.275 -
   7.276 -(* ------------------------------------------------------------------------- *)
   7.277 -(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
   7.278 -(*      t, but simplified wrt. the following theorems:                       *)
   7.279 -(*        (True & x) = x                                                     *)
   7.280 -(*        (x & True) = x                                                     *)
   7.281 -(*        (False & x) = False                                                *)
   7.282 -(*        (x & False) = False                                                *)
   7.283 -(*        (True | x) = True                                                  *)
   7.284 -(*        (x | True) = True                                                  *)
   7.285 -(*        (False | x) = x                                                    *)
   7.286 -(*        (x | False) = x                                                    *)
   7.287 -(*      No simplification is performed below connectives other than & and |. *)
   7.288 -(*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
   7.289 -(*      simplified only if the left-hand side does not simplify to False     *)
   7.290 -(*      (True, respectively).                                                *)
   7.291 -(* ------------------------------------------------------------------------- *)
   7.292 -
   7.293 -(* Theory.theory -> Term.term -> Thm.thm *)
   7.294 -
   7.295 -fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   7.296 -      let
   7.297 -        val thm1 = simp_True_False_thm thy x
   7.298 -        val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   7.299 -      in
   7.300 -        if x' = @{term False} then
   7.301 -          simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
   7.302 -        else
   7.303 -          let
   7.304 -            val thm2 = simp_True_False_thm thy y
   7.305 -            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   7.306 -          in
   7.307 -            if x' = @{term True} then
   7.308 -              simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
   7.309 -            else if y' = @{term False} then
   7.310 -              simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
   7.311 -            else if y' = @{term True} then
   7.312 -              simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
   7.313 -            else
   7.314 -              conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
   7.315 -          end
   7.316 -      end
   7.317 -  | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   7.318 -      let
   7.319 -        val thm1 = simp_True_False_thm thy x
   7.320 -        val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   7.321 -      in
   7.322 -        if x' = @{term True} then
   7.323 -          simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
   7.324 -        else
   7.325 -          let
   7.326 -            val thm2 = simp_True_False_thm thy y
   7.327 -            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   7.328 -          in
   7.329 -            if x' = @{term False} then
   7.330 -              simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
   7.331 -            else if y' = @{term True} then
   7.332 -              simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
   7.333 -            else if y' = @{term False} then
   7.334 -              simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
   7.335 -            else
   7.336 -              disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   7.337 -          end
   7.338 -      end
   7.339 -  | simp_True_False_thm thy t = inst_thm thy [t] iff_refl;  (* t = t *)
   7.340 -
   7.341 -(* ------------------------------------------------------------------------- *)
   7.342 -(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
   7.343 -(*      is in conjunction normal form.  May cause an exponential blowup      *)
   7.344 -(*      in the length of the term.                                           *)
   7.345 -(* ------------------------------------------------------------------------- *)
   7.346 -
   7.347 -fun make_cnf_thm ctxt t =
   7.348 -  let
   7.349 -    val thy = Proof_Context.theory_of ctxt
   7.350 -    fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
   7.351 -          let
   7.352 -            val thm1 = make_cnf_thm_from_nnf x
   7.353 -            val thm2 = make_cnf_thm_from_nnf y
   7.354 -          in
   7.355 -            conj_cong OF [thm1, thm2]
   7.356 -          end
   7.357 -      | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
   7.358 -          let
   7.359 -            (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
   7.360 -            fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
   7.361 -                  let
   7.362 -                    val thm1 = make_cnf_disj_thm x1 y'
   7.363 -                    val thm2 = make_cnf_disj_thm x2 y'
   7.364 -                  in
   7.365 -                    make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   7.366 -                  end
   7.367 -              | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
   7.368 -                  let
   7.369 -                    val thm1 = make_cnf_disj_thm x' y1
   7.370 -                    val thm2 = make_cnf_disj_thm x' y2
   7.371 -                  in
   7.372 -                    make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   7.373 -                  end
   7.374 -              | make_cnf_disj_thm x' y' =
   7.375 -                  inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   7.376 -            val thm1 = make_cnf_thm_from_nnf x
   7.377 -            val thm2 = make_cnf_thm_from_nnf y
   7.378 -            val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   7.379 -            val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   7.380 -            val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   7.381 -          in
   7.382 -            iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
   7.383 -          end
   7.384 -      | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl
   7.385 -    (* convert 't' to NNF first *)
   7.386 -    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
   7.387 -(*###
   7.388 -    val nnf_thm = make_nnf_thm thy t
   7.389 -*)
   7.390 -    val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   7.391 -    (* then simplify wrt. True/False (this should preserve NNF) *)
   7.392 -    val simp_thm = simp_True_False_thm thy nnf
   7.393 -    val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   7.394 -    (* finally, convert to CNF (this should preserve the simplification) *)
   7.395 -    val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp
   7.396 -(* ###
   7.397 -    val cnf_thm = make_cnf_thm_from_nnf simp
   7.398 -*)
   7.399 -  in
   7.400 -    iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
   7.401 -  end;
   7.402 -
   7.403 -(* ------------------------------------------------------------------------- *)
   7.404 -(*            CNF transformation by introducing new literals                 *)
   7.405 -(* ------------------------------------------------------------------------- *)
   7.406 -
   7.407 -(* ------------------------------------------------------------------------- *)
   7.408 -(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
   7.409 -(*      t' is almost in conjunction normal form, except that conjunctions    *)
   7.410 -(*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
   7.411 -(*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
   7.412 -(*      introduce new (existentially bound) literals.  Note: the current     *)
   7.413 -(*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
   7.414 -(*      in the case of nested equivalences.                                  *)
   7.415 -(* ------------------------------------------------------------------------- *)
   7.416 -
   7.417 -fun make_cnfx_thm ctxt t =
   7.418 -  let
   7.419 -    val thy = Proof_Context.theory_of ctxt
   7.420 -    val var_id = Unsynchronized.ref 0  (* properly initialized below *)
   7.421 -    fun new_free () =
   7.422 -      Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
   7.423 -    fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
   7.424 -          let
   7.425 -            val thm1 = make_cnfx_thm_from_nnf x
   7.426 -            val thm2 = make_cnfx_thm_from_nnf y
   7.427 -          in
   7.428 -            conj_cong OF [thm1, thm2]
   7.429 -          end
   7.430 -      | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
   7.431 -          if is_clause x andalso is_clause y then
   7.432 -            inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
   7.433 -          else if is_literal y orelse is_literal x then
   7.434 -            let
   7.435 -              (* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
   7.436 -              (* almost in CNF, and x' or y' is a literal                      *)
   7.437 -              fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
   7.438 -                    let
   7.439 -                      val thm1 = make_cnfx_disj_thm x1 y'
   7.440 -                      val thm2 = make_cnfx_disj_thm x2 y'
   7.441 -                    in
   7.442 -                      make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   7.443 -                    end
   7.444 -                | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
   7.445 -                    let
   7.446 -                      val thm1 = make_cnfx_disj_thm x' y1
   7.447 -                      val thm2 = make_cnfx_disj_thm x' y2
   7.448 -                    in
   7.449 -                      make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   7.450 -                    end
   7.451 -                | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
   7.452 -                    let
   7.453 -                      val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
   7.454 -                      val var = new_free ()
   7.455 -                      val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
   7.456 -                      val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   7.457 -                      val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   7.458 -                      val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   7.459 -                    in
   7.460 -                      iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   7.461 -                    end
   7.462 -                | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
   7.463 -                    let
   7.464 -                      val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   7.465 -                      val var = new_free ()
   7.466 -                      val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
   7.467 -                      val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   7.468 -                      val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   7.469 -                      val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   7.470 -                    in
   7.471 -                      iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
   7.472 -                    end
   7.473 -                | make_cnfx_disj_thm x' y' =
   7.474 -                    inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   7.475 -              val thm1 = make_cnfx_thm_from_nnf x
   7.476 -              val thm2 = make_cnfx_thm_from_nnf y
   7.477 -              val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   7.478 -              val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   7.479 -              val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   7.480 -            in
   7.481 -              iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
   7.482 -            end
   7.483 -          else
   7.484 -            let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
   7.485 -              val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
   7.486 -              val var = new_free ()
   7.487 -              val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
   7.488 -              val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
   7.489 -              val thm3 = Thm.forall_intr (cterm_of thy var) thm2  (* !!v. (x | v) & (y | ~v) = body' *)
   7.490 -              val thm4 = Thm.strip_shyps (thm3 COMP allI)         (* ALL v. (x | v) & (y | ~v) = body' *)
   7.491 -              val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
   7.492 -            in
   7.493 -              iff_trans OF [thm1, thm5]
   7.494 -            end
   7.495 -      | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl
   7.496 -    (* convert 't' to NNF first *)
   7.497 -    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
   7.498 -(* ###
   7.499 -    val nnf_thm = make_nnf_thm thy t
   7.500 -*)
   7.501 -    val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   7.502 -    (* then simplify wrt. True/False (this should preserve NNF) *)
   7.503 -    val simp_thm = simp_True_False_thm thy nnf
   7.504 -    val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   7.505 -    (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
   7.506 -    val _ = (var_id := fold (fn free => fn max =>
   7.507 -      let
   7.508 -        val (name, _) = dest_Free free
   7.509 -        val idx =
   7.510 -          if String.isPrefix "cnfx_" name then
   7.511 -            (Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
   7.512 -          else
   7.513 -            NONE
   7.514 -      in
   7.515 -        Int.max (max, the_default 0 idx)
   7.516 -      end) (Misc_Legacy.term_frees simp) 0)
   7.517 -    (* finally, convert to definitional CNF (this should preserve the simplification) *)
   7.518 -    val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
   7.519 -(*###
   7.520 -    val cnfx_thm = make_cnfx_thm_from_nnf simp
   7.521 -*)
   7.522 -  in
   7.523 -    iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
   7.524 -  end;
   7.525 -
   7.526 -(* ------------------------------------------------------------------------- *)
   7.527 -(*                                  Tactics                                  *)
   7.528 -(* ------------------------------------------------------------------------- *)
   7.529 -
   7.530 -(* ------------------------------------------------------------------------- *)
   7.531 -(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
   7.532 -(* ------------------------------------------------------------------------- *)
   7.533 -
   7.534 -fun weakening_tac i =
   7.535 -  dtac weakening_thm i THEN atac (i+1);
   7.536 -
   7.537 -(* ------------------------------------------------------------------------- *)
   7.538 -(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
   7.539 -(*      (possibly causing an exponential blowup in the length of each        *)
   7.540 -(*      premise)                                                             *)
   7.541 -(* ------------------------------------------------------------------------- *)
   7.542 -
   7.543 -fun cnf_rewrite_tac ctxt i =
   7.544 -  (* cut the CNF formulas as new premises *)
   7.545 -  Subgoal.FOCUS (fn {prems, ...} =>
   7.546 -    let
   7.547 -      val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
   7.548 -      val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
   7.549 -    in
   7.550 -      cut_facts_tac cut_thms 1
   7.551 -    end) ctxt i
   7.552 -  (* remove the original premises *)
   7.553 -  THEN SELECT_GOAL (fn thm =>
   7.554 -    let
   7.555 -      val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   7.556 -    in
   7.557 -      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   7.558 -    end) i;
   7.559 -
   7.560 -(* ------------------------------------------------------------------------- *)
   7.561 -(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
   7.562 -(*      (possibly introducing new literals)                                  *)
   7.563 -(* ------------------------------------------------------------------------- *)
   7.564 -
   7.565 -fun cnfx_rewrite_tac ctxt i =
   7.566 -  (* cut the CNF formulas as new premises *)
   7.567 -  Subgoal.FOCUS (fn {prems, ...} =>
   7.568 -    let
   7.569 -      val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems
   7.570 -      val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
   7.571 -    in
   7.572 -      cut_facts_tac cut_thms 1
   7.573 -    end) ctxt i
   7.574 -  (* remove the original premises *)
   7.575 -  THEN SELECT_GOAL (fn thm =>
   7.576 -    let
   7.577 -      val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   7.578 -    in
   7.579 -      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   7.580 -    end) i;
   7.581 -
   7.582 -end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/sat.ML	Sat Feb 01 22:02:20 2014 +0100
     8.3 @@ -0,0 +1,465 @@
     8.4 +(*  Title:      HOL/Tools/sat.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.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.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: bool Config.T  (* print trace messages *)
    8.55 +  val solver: string Config.T  (* 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 +structure SAT : SAT =
    8.64 +struct
    8.65 +
    8.66 +val trace = Attrib.setup_config_bool @{binding sat_trace} (K false);
    8.67 +
    8.68 +fun cond_tracing ctxt msg =
    8.69 +  if Config.get ctxt trace then tracing (msg ()) else ();
    8.70 +
    8.71 +val solver = Attrib.setup_config_string @{binding sat_solver} (K "zchaff_with_proofs");
    8.72 +  (*see HOL/Tools/sat_solver.ML for possible values*)
    8.73 +
    8.74 +val counter = Unsynchronized.ref 0;
    8.75 +
    8.76 +val resolution_thm =
    8.77 +  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
    8.78 +
    8.79 +val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
    8.80 +
    8.81 +(* ------------------------------------------------------------------------- *)
    8.82 +(* lit_ord: an order on integers that considers their absolute values only,  *)
    8.83 +(*      thereby treating integers that represent the same atom (positively   *)
    8.84 +(*      or negatively) as equal                                              *)
    8.85 +(* ------------------------------------------------------------------------- *)
    8.86 +
    8.87 +fun lit_ord (i, j) = int_ord (abs i, abs j);
    8.88 +
    8.89 +(* ------------------------------------------------------------------------- *)
    8.90 +(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
    8.91 +(*      distinguished:                                                       *)
    8.92 +(*      1. NO_CLAUSE: clause not proved (yet)                                *)
    8.93 +(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
    8.94 +(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
    8.95 +(*         (a mapping from int's to its literals) for faster proof           *)
    8.96 +(*         reconstruction                                                    *)
    8.97 +(* ------------------------------------------------------------------------- *)
    8.98 +
    8.99 +datatype CLAUSE =
   8.100 +    NO_CLAUSE
   8.101 +  | ORIG_CLAUSE of thm
   8.102 +  | RAW_CLAUSE of thm * (int * cterm) list;
   8.103 +
   8.104 +(* ------------------------------------------------------------------------- *)
   8.105 +(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
   8.106 +(*      resolution over the list (starting with its head), i.e. with two raw *)
   8.107 +(*      clauses                                                              *)
   8.108 +(*        [P, x1, ..., a, ..., xn] |- False                                  *)
   8.109 +(*      and                                                                  *)
   8.110 +(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
   8.111 +(*      (where a and a' are dual to each other), we convert the first clause *)
   8.112 +(*      to                                                                   *)
   8.113 +(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
   8.114 +(*      the second clause to                                                 *)
   8.115 +(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
   8.116 +(*      and then perform resolution with                                     *)
   8.117 +(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
   8.118 +(*      to produce                                                           *)
   8.119 +(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
   8.120 +(*      Each clause is accompanied with an association list mapping integers *)
   8.121 +(*      (positive for positive literals, negative for negative literals, and *)
   8.122 +(*      the same absolute value for dual literals) to the actual literals as *)
   8.123 +(*      cterms.                                                              *)
   8.124 +(* ------------------------------------------------------------------------- *)
   8.125 +
   8.126 +fun resolve_raw_clauses _ [] =
   8.127 +      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   8.128 +  | resolve_raw_clauses ctxt (c::cs) =
   8.129 +      let
   8.130 +        (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
   8.131 +        fun merge xs [] = xs
   8.132 +          | merge [] ys = ys
   8.133 +          | merge (x :: xs) (y :: ys) =
   8.134 +              (case (lit_ord o pairself fst) (x, y) of
   8.135 +                LESS => x :: merge xs (y :: ys)
   8.136 +              | EQUAL => x :: merge xs ys
   8.137 +              | GREATER => y :: merge (x :: xs) ys)
   8.138 +
   8.139 +        (* find out which two hyps are used in the resolution *)
   8.140 +        fun find_res_hyps ([], _) _ =
   8.141 +              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   8.142 +          | find_res_hyps (_, []) _ =
   8.143 +              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   8.144 +          | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
   8.145 +              (case (lit_ord o pairself fst) (h1, h2) of
   8.146 +                LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
   8.147 +              | EQUAL =>
   8.148 +                  let
   8.149 +                    val (i1, chyp1) = h1
   8.150 +                    val (i2, chyp2) = h2
   8.151 +                  in
   8.152 +                    if i1 = ~ i2 then
   8.153 +                      (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
   8.154 +                    else (* i1 = i2 *)
   8.155 +                      find_res_hyps (hyps1, hyps2) (h1 :: acc)
   8.156 +                  end
   8.157 +          | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
   8.158 +
   8.159 +        fun resolution (c1, hyps1) (c2, hyps2) =
   8.160 +          let
   8.161 +            val _ =
   8.162 +              cond_tracing ctxt (fn () =>
   8.163 +                "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
   8.164 +                " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^
   8.165 +                ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
   8.166 +                " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")")
   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 +              cond_tracing ctxt
   8.184 +                (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
   8.185 +
   8.186 +            (* Gamma1, Gamma2 |- False *)
   8.187 +            val c_new =
   8.188 +              Thm.implies_elim
   8.189 +                (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
   8.190 +                (if hyp1_is_neg then c1' else c2')
   8.191 +
   8.192 +            val _ =
   8.193 +              cond_tracing ctxt (fn () =>
   8.194 +                "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
   8.195 +                " (hyps: " ^
   8.196 +                ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")")
   8.197 +
   8.198 +            val _ = Unsynchronized.inc counter
   8.199 +          in
   8.200 +            (c_new, new_hyps)
   8.201 +          end
   8.202 +        in
   8.203 +          fold resolution cs c
   8.204 +        end;
   8.205 +
   8.206 +(* ------------------------------------------------------------------------- *)
   8.207 +(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
   8.208 +(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
   8.209 +(*      'clauses' array with derived clauses, and returns the derived clause *)
   8.210 +(*      at index 'empty_id' (which should just be "False" if proof           *)
   8.211 +(*      reconstruction was successful, with the used clauses as hyps).       *)
   8.212 +(*      'atom_table' must contain an injective mapping from all atoms that   *)
   8.213 +(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
   8.214 +(* ------------------------------------------------------------------------- *)
   8.215 +
   8.216 +fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
   8.217 +  let
   8.218 +    fun index_of_literal chyp =
   8.219 +      (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
   8.220 +        (Const (@{const_name Not}, _) $ atom) =>
   8.221 +          SOME (~ (the (Termtab.lookup atom_table atom)))
   8.222 +      | atom => SOME (the (Termtab.lookup atom_table atom)))
   8.223 +      handle TERM _ => NONE;  (* 'chyp' is not a literal *)
   8.224 +
   8.225 +    fun prove_clause id =
   8.226 +      (case Array.sub (clauses, id) of
   8.227 +        RAW_CLAUSE clause => clause
   8.228 +      | ORIG_CLAUSE thm =>
   8.229 +          (* convert the original clause *)
   8.230 +          let
   8.231 +            val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id)
   8.232 +            val raw = CNF.clause2raw_thm thm
   8.233 +            val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
   8.234 +              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
   8.235 +            val clause = (raw, hyps)
   8.236 +            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   8.237 +          in
   8.238 +            clause
   8.239 +          end
   8.240 +      | NO_CLAUSE =>
   8.241 +          (* prove the clause, using information from 'clause_table' *)
   8.242 +          let
   8.243 +            val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...")
   8.244 +            val ids = the (Inttab.lookup clause_table id)
   8.245 +            val clause = resolve_raw_clauses ctxt (map prove_clause ids)
   8.246 +            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   8.247 +            val _ =
   8.248 +              cond_tracing ctxt
   8.249 +                (fn () => "Replay chain successful; clause stored at #" ^ string_of_int id)
   8.250 +          in
   8.251 +            clause
   8.252 +          end)
   8.253 +
   8.254 +    val _ = counter := 0
   8.255 +    val empty_clause = fst (prove_clause empty_id)
   8.256 +    val _ =
   8.257 +      cond_tracing ctxt (fn () =>
   8.258 +        "Proof reconstruction successful; " ^
   8.259 +        string_of_int (!counter) ^ " resolution step(s) total.")
   8.260 +  in
   8.261 +    empty_clause
   8.262 +  end;
   8.263 +
   8.264 +(* ------------------------------------------------------------------------- *)
   8.265 +(* string_of_prop_formula: return a human-readable string representation of  *)
   8.266 +(*      a 'prop_formula' (just for tracing)                                  *)
   8.267 +(* ------------------------------------------------------------------------- *)
   8.268 +
   8.269 +fun string_of_prop_formula Prop_Logic.True = "True"
   8.270 +  | string_of_prop_formula Prop_Logic.False = "False"
   8.271 +  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
   8.272 +  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
   8.273 +  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
   8.274 +      "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   8.275 +  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
   8.276 +      "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
   8.277 +
   8.278 +(* ------------------------------------------------------------------------- *)
   8.279 +(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   8.280 +(*      a proof from the resulting proof trace of the SAT solver.  The       *)
   8.281 +(*      theorem returned is just "False" (with some of the given clauses as  *)
   8.282 +(*      hyps).                                                               *)
   8.283 +(* ------------------------------------------------------------------------- *)
   8.284 +
   8.285 +fun rawsat_thm ctxt clauses =
   8.286 +  let
   8.287 +    (* remove premises that equal "True" *)
   8.288 +    val clauses' = filter (fn clause =>
   8.289 +      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
   8.290 +        handle TERM ("dest_Trueprop", _) => true) clauses
   8.291 +    (* remove non-clausal premises -- of course this shouldn't actually   *)
   8.292 +    (* remove anything as long as 'rawsat_tac' is only called after the   *)
   8.293 +    (* premises have been converted to clauses                            *)
   8.294 +    val clauses'' = filter (fn clause =>
   8.295 +      ((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
   8.296 +        handle TERM ("dest_Trueprop", _) => false)
   8.297 +      orelse (
   8.298 +        warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
   8.299 +        false)) clauses'
   8.300 +    (* remove trivial clauses -- this is necessary because zChaff removes *)
   8.301 +    (* trivial clauses during preprocessing, and otherwise our clause     *)
   8.302 +    (* numbering would be off                                             *)
   8.303 +    val nontrivial_clauses =
   8.304 +      filter (not o CNF.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
   8.305 +    (* sort clauses according to the term order -- an optimization,       *)
   8.306 +    (* useful because forming the union of hypotheses, as done by         *)
   8.307 +    (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
   8.308 +    (* terms sorted in descending order, while only linear for terms      *)
   8.309 +    (* sorted in ascending order                                          *)
   8.310 +    val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   8.311 +    val _ =
   8.312 +      cond_tracing ctxt (fn () =>
   8.313 +        "Sorted non-trivial clauses:\n" ^
   8.314 +        cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
   8.315 +    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
   8.316 +    val (fms, atom_table) =
   8.317 +      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
   8.318 +        sorted_clauses Termtab.empty
   8.319 +    val _ =
   8.320 +      cond_tracing ctxt
   8.321 +        (fn () => "Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
   8.322 +    val fm = Prop_Logic.all fms
   8.323 +    fun make_quick_and_dirty_thm () =
   8.324 +      let
   8.325 +        val _ =
   8.326 +          cond_tracing ctxt
   8.327 +            (fn () => "quick_and_dirty is set: proof reconstruction skipped, using oracle instead")
   8.328 +        val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
   8.329 +      in
   8.330 +        (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   8.331 +        (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
   8.332 +        (* clauses in ascending order (which is linear for                  *)
   8.333 +        (* 'Conjunction.intr_balanced', used below)                         *)
   8.334 +        fold Thm.weaken (rev sorted_clauses) False_thm
   8.335 +      end
   8.336 +  in
   8.337 +    case
   8.338 +      let val the_solver = Config.get ctxt solver
   8.339 +      in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
   8.340 +    of
   8.341 +      SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
   8.342 +       (cond_tracing ctxt (fn () =>
   8.343 +          "Proof trace from SAT solver:\n" ^
   8.344 +          "clauses: " ^ ML_Syntax.print_list
   8.345 +            (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
   8.346 +            (Inttab.dest clause_table) ^ "\n" ^
   8.347 +          "empty clause: " ^ string_of_int empty_id);
   8.348 +        if Config.get ctxt quick_and_dirty then
   8.349 +          make_quick_and_dirty_thm ()
   8.350 +        else
   8.351 +          let
   8.352 +            (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
   8.353 +            (*               this avoids accumulation of hypotheses during resolution    *)
   8.354 +            (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
   8.355 +            val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
   8.356 +            (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
   8.357 +            val cnf_cterm = cprop_of clauses_thm
   8.358 +            val cnf_thm = Thm.assume cnf_cterm
   8.359 +            (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
   8.360 +            val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
   8.361 +            (* initialize the clause array with the given clauses *)
   8.362 +            val max_idx = fst (the (Inttab.max clause_table))
   8.363 +            val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
   8.364 +            val _ =
   8.365 +              fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
   8.366 +                cnf_clauses 0
   8.367 +            (* replay the proof to derive the empty clause *)
   8.368 +            (* [c_1 && ... && c_n] |- False *)
   8.369 +            val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
   8.370 +          in
   8.371 +            (* [c_1, ..., c_n] |- False *)
   8.372 +            Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
   8.373 +          end)
   8.374 +    | SatSolver.UNSATISFIABLE NONE =>
   8.375 +        if Config.get ctxt quick_and_dirty then
   8.376 +         (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
   8.377 +          make_quick_and_dirty_thm ())
   8.378 +        else
   8.379 +          raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
   8.380 +    | SatSolver.SATISFIABLE assignment =>
   8.381 +        let
   8.382 +          val msg =
   8.383 +            "SAT solver found a countermodel:\n" ^
   8.384 +            (commas o map (fn (term, idx) =>
   8.385 +                Syntax.string_of_term_global @{theory} term ^ ": " ^
   8.386 +                  (case assignment idx of NONE => "arbitrary"
   8.387 +                  | SOME true => "true" | SOME false => "false")))
   8.388 +              (Termtab.dest atom_table)
   8.389 +        in
   8.390 +          raise THM (msg, 0, [])
   8.391 +        end
   8.392 +    | SatSolver.UNKNOWN =>
   8.393 +        raise THM ("SAT solver failed to decide the formula", 0, [])
   8.394 +  end;
   8.395 +
   8.396 +(* ------------------------------------------------------------------------- *)
   8.397 +(* Tactics                                                                   *)
   8.398 +(* ------------------------------------------------------------------------- *)
   8.399 +
   8.400 +(* ------------------------------------------------------------------------- *)
   8.401 +(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
   8.402 +(*      should be of the form                                                *)
   8.403 +(*        [| c1; c2; ...; ck |] ==> False                                    *)
   8.404 +(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
   8.405 +(*      or "True"                                                            *)
   8.406 +(* ------------------------------------------------------------------------- *)
   8.407 +
   8.408 +fun rawsat_tac ctxt i =
   8.409 +  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
   8.410 +    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
   8.411 +
   8.412 +(* ------------------------------------------------------------------------- *)
   8.413 +(* pre_cnf_tac: converts the i-th subgoal                                    *)
   8.414 +(*        [| A1 ; ... ; An |] ==> B                                          *)
   8.415 +(*      to                                                                   *)
   8.416 +(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
   8.417 +(*      (handling meta-logical connectives in B properly before negating),   *)
   8.418 +(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
   8.419 +(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
   8.420 +(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
   8.421 +(*      subgoal                                                              *)
   8.422 +(* ------------------------------------------------------------------------- *)
   8.423 +
   8.424 +fun pre_cnf_tac ctxt =
   8.425 +  rtac ccontr THEN'
   8.426 +  Object_Logic.atomize_prems_tac ctxt THEN'
   8.427 +  CONVERSION Drule.beta_eta_conversion;
   8.428 +
   8.429 +(* ------------------------------------------------------------------------- *)
   8.430 +(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
   8.431 +(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
   8.432 +(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
   8.433 +(*      subgoal                                                              *)
   8.434 +(* ------------------------------------------------------------------------- *)
   8.435 +
   8.436 +fun cnfsat_tac ctxt i =
   8.437 +  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
   8.438 +
   8.439 +(* ------------------------------------------------------------------------- *)
   8.440 +(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   8.441 +(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
   8.442 +(*      CNF formula becomes a separate premise) and existential quantifiers, *)
   8.443 +(*      then applies 'rawsat_tac' to solve the subgoal                       *)
   8.444 +(* ------------------------------------------------------------------------- *)
   8.445 +
   8.446 +fun cnfxsat_tac ctxt i =
   8.447 +  (etac FalseE i) ORELSE
   8.448 +    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
   8.449 +
   8.450 +(* ------------------------------------------------------------------------- *)
   8.451 +(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
   8.452 +(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
   8.453 +(*      an exponential blowup.                                               *)
   8.454 +(* ------------------------------------------------------------------------- *)
   8.455 +
   8.456 +fun sat_tac ctxt i =
   8.457 +  pre_cnf_tac ctxt i THEN CNF.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
   8.458 +
   8.459 +(* ------------------------------------------------------------------------- *)
   8.460 +(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   8.461 +(*      arbitrary formula.  The input is translated to CNF, possibly         *)
   8.462 +(*      introducing new literals.                                            *)
   8.463 +(* ------------------------------------------------------------------------- *)
   8.464 +
   8.465 +fun satx_tac ctxt i =
   8.466 +  pre_cnf_tac ctxt i THEN CNF.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
   8.467 +
   8.468 +end;
     9.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Feb 01 20:38:29 2014 +0000
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,474 +0,0 @@
     9.4 -(*  Title:      HOL/Tools/sat_funcs.ML
     9.5 -    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     9.6 -    Author:     Tjark Weber, TU Muenchen
     9.7 -
     9.8 -Proof reconstruction from SAT solvers.
     9.9 -
    9.10 -  Description:
    9.11 -    This file defines several tactics to invoke a proof-producing
    9.12 -    SAT solver on a propositional goal in clausal form.
    9.13 -
    9.14 -    We use a sequent presentation of clauses to speed up resolution
    9.15 -    proof reconstruction.
    9.16 -    We call such clauses "raw clauses", which are of the form
    9.17 -          [x1, ..., xn, P] |- False
    9.18 -    (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
    9.19 -    where each xi is a literal (see also comments in cnf_funcs.ML).
    9.20 -
    9.21 -    This does not work for goals containing schematic variables!
    9.22 -
    9.23 -      The tactic produces a clause representation of the given goal
    9.24 -      in DIMACS format and invokes a SAT solver, which should return
    9.25 -      a proof consisting of a sequence of resolution steps, indicating
    9.26 -      the two input clauses, and resulting in new clauses, leading to
    9.27 -      the empty clause (i.e. "False").  The tactic replays this proof
    9.28 -      in Isabelle and thus solves the overall goal.
    9.29 -
    9.30 -  There are three SAT tactics available.  They differ in the CNF transformation
    9.31 -  used. "sat_tac" uses naive CNF transformation to transform the theorem to be
    9.32 -  proved before giving it to the SAT solver.  The naive transformation in the
    9.33 -  worst case can lead to an exponential blow up in formula size.  Another
    9.34 -  tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
    9.35 -  produce a formula of linear size increase compared to the input formula, at
    9.36 -  the cost of possibly introducing new variables.  See cnf_funcs.ML for more
    9.37 -  comments on the CNF transformation.  "rawsat_tac" should be used with
    9.38 -  caution: no CNF transformation is performed, and the tactic's behavior is
    9.39 -  undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
    9.40 -  where each Ci is a disjunction.
    9.41 -
    9.42 -  The SAT solver to be used can be set via the "solver" reference.  See
    9.43 -  sat_solvers.ML for possible values, and etc/settings for required (solver-
    9.44 -  dependent) configuration settings.  To replay SAT proofs in Isabelle, you
    9.45 -  must of course use a proof-producing SAT solver in the first place.
    9.46 -
    9.47 -  Proofs are replayed only if "quick_and_dirty" is false.  If
    9.48 -  "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
    9.49 -  negation to be unsatisfiable) is proved via an oracle.
    9.50 -*)
    9.51 -
    9.52 -signature SAT =
    9.53 -sig
    9.54 -  val trace_sat: bool Unsynchronized.ref    (* input: print trace messages *)
    9.55 -  val solver: string Unsynchronized.ref  (* input: name of SAT solver to be used *)
    9.56 -  val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
    9.57 -  val rawsat_thm: Proof.context -> cterm list -> thm
    9.58 -  val rawsat_tac: Proof.context -> int -> tactic
    9.59 -  val sat_tac: Proof.context -> int -> tactic
    9.60 -  val satx_tac: Proof.context -> int -> tactic
    9.61 -end
    9.62 -
    9.63 -functor SATFunc(cnf : CNF) : SAT =
    9.64 -struct
    9.65 -
    9.66 -val trace_sat = Unsynchronized.ref false;
    9.67 -
    9.68 -val solver = Unsynchronized.ref "zchaff_with_proofs";
    9.69 -  (*see HOL/Tools/sat_solver.ML for possible values*)
    9.70 -
    9.71 -val counter = Unsynchronized.ref 0;
    9.72 -
    9.73 -val resolution_thm =
    9.74 -  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
    9.75 -
    9.76 -val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
    9.77 -
    9.78 -(* ------------------------------------------------------------------------- *)
    9.79 -(* lit_ord: an order on integers that considers their absolute values only,  *)
    9.80 -(*      thereby treating integers that represent the same atom (positively   *)
    9.81 -(*      or negatively) as equal                                              *)
    9.82 -(* ------------------------------------------------------------------------- *)
    9.83 -
    9.84 -fun lit_ord (i, j) = int_ord (abs i, abs j);
    9.85 -
    9.86 -(* ------------------------------------------------------------------------- *)
    9.87 -(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
    9.88 -(*      distinguished:                                                       *)
    9.89 -(*      1. NO_CLAUSE: clause not proved (yet)                                *)
    9.90 -(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
    9.91 -(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
    9.92 -(*         (a mapping from int's to its literals) for faster proof           *)
    9.93 -(*         reconstruction                                                    *)
    9.94 -(* ------------------------------------------------------------------------- *)
    9.95 -
    9.96 -datatype CLAUSE =
    9.97 -    NO_CLAUSE
    9.98 -  | ORIG_CLAUSE of thm
    9.99 -  | RAW_CLAUSE of thm * (int * cterm) list;
   9.100 -
   9.101 -(* ------------------------------------------------------------------------- *)
   9.102 -(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
   9.103 -(*      resolution over the list (starting with its head), i.e. with two raw *)
   9.104 -(*      clauses                                                              *)
   9.105 -(*        [P, x1, ..., a, ..., xn] |- False                                  *)
   9.106 -(*      and                                                                  *)
   9.107 -(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
   9.108 -(*      (where a and a' are dual to each other), we convert the first clause *)
   9.109 -(*      to                                                                   *)
   9.110 -(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
   9.111 -(*      the second clause to                                                 *)
   9.112 -(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
   9.113 -(*      and then perform resolution with                                     *)
   9.114 -(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
   9.115 -(*      to produce                                                           *)
   9.116 -(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
   9.117 -(*      Each clause is accompanied with an association list mapping integers *)
   9.118 -(*      (positive for positive literals, negative for negative literals, and *)
   9.119 -(*      the same absolute value for dual literals) to the actual literals as *)
   9.120 -(*      cterms.                                                              *)
   9.121 -(* ------------------------------------------------------------------------- *)
   9.122 -
   9.123 -fun resolve_raw_clauses _ [] =
   9.124 -      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   9.125 -  | resolve_raw_clauses ctxt (c::cs) =
   9.126 -      let
   9.127 -        (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
   9.128 -        fun merge xs [] = xs
   9.129 -          | merge [] ys = ys
   9.130 -          | merge (x :: xs) (y :: ys) =
   9.131 -              (case (lit_ord o pairself fst) (x, y) of
   9.132 -                LESS => x :: merge xs (y :: ys)
   9.133 -              | EQUAL => x :: merge xs ys
   9.134 -              | GREATER => y :: merge (x :: xs) ys)
   9.135 -
   9.136 -        (* find out which two hyps are used in the resolution *)
   9.137 -        fun find_res_hyps ([], _) _ =
   9.138 -              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   9.139 -          | find_res_hyps (_, []) _ =
   9.140 -              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   9.141 -          | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
   9.142 -              (case (lit_ord o pairself fst) (h1, h2) of
   9.143 -                LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
   9.144 -              | EQUAL =>
   9.145 -                  let
   9.146 -                    val (i1, chyp1) = h1
   9.147 -                    val (i2, chyp2) = h2
   9.148 -                  in
   9.149 -                    if i1 = ~ i2 then
   9.150 -                      (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
   9.151 -                    else (* i1 = i2 *)
   9.152 -                      find_res_hyps (hyps1, hyps2) (h1 :: acc)
   9.153 -                  end
   9.154 -          | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
   9.155 -
   9.156 -        fun resolution (c1, hyps1) (c2, hyps2) =
   9.157 -          let
   9.158 -            val _ =
   9.159 -              if ! trace_sat then  (* FIXME !? *)
   9.160 -                tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
   9.161 -                  " (hyps: " ^ ML_Syntax.print_list
   9.162 -                    (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
   9.163 -                  ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
   9.164 -                  " (hyps: " ^ ML_Syntax.print_list
   9.165 -                    (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
   9.166 -              else ()
   9.167 -
   9.168 -            (* the two literals used for resolution *)
   9.169 -            val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
   9.170 -
   9.171 -            val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
   9.172 -            val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
   9.173 -
   9.174 -            val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
   9.175 -              let
   9.176 -                val cLit =
   9.177 -                  snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
   9.178 -              in
   9.179 -                Thm.instantiate ([], [(cP, cLit)]) resolution_thm
   9.180 -              end
   9.181 -
   9.182 -            val _ =
   9.183 -              if !trace_sat then
   9.184 -                tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
   9.185 -              else ()
   9.186 -
   9.187 -            (* Gamma1, Gamma2 |- False *)
   9.188 -            val c_new =
   9.189 -              Thm.implies_elim
   9.190 -                (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
   9.191 -                (if hyp1_is_neg then c1' else c2')
   9.192 -
   9.193 -            val _ =
   9.194 -              if !trace_sat then
   9.195 -                tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
   9.196 -                  " (hyps: " ^ ML_Syntax.print_list
   9.197 -                      (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
   9.198 -              else ()
   9.199 -            val _ = Unsynchronized.inc counter
   9.200 -          in
   9.201 -            (c_new, new_hyps)
   9.202 -          end
   9.203 -        in
   9.204 -          fold resolution cs c
   9.205 -        end;
   9.206 -
   9.207 -(* ------------------------------------------------------------------------- *)
   9.208 -(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
   9.209 -(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
   9.210 -(*      'clauses' array with derived clauses, and returns the derived clause *)
   9.211 -(*      at index 'empty_id' (which should just be "False" if proof           *)
   9.212 -(*      reconstruction was successful, with the used clauses as hyps).       *)
   9.213 -(*      'atom_table' must contain an injective mapping from all atoms that   *)
   9.214 -(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
   9.215 -(* ------------------------------------------------------------------------- *)
   9.216 -
   9.217 -fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
   9.218 -  let
   9.219 -    fun index_of_literal chyp =
   9.220 -      (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
   9.221 -        (Const (@{const_name Not}, _) $ atom) =>
   9.222 -          SOME (~ (the (Termtab.lookup atom_table atom)))
   9.223 -      | atom => SOME (the (Termtab.lookup atom_table atom)))
   9.224 -      handle TERM _ => NONE;  (* 'chyp' is not a literal *)
   9.225 -
   9.226 -    fun prove_clause id =
   9.227 -      (case Array.sub (clauses, id) of
   9.228 -        RAW_CLAUSE clause => clause
   9.229 -      | ORIG_CLAUSE thm =>
   9.230 -          (* convert the original clause *)
   9.231 -          let
   9.232 -            val _ =
   9.233 -              if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
   9.234 -            val raw = cnf.clause2raw_thm thm
   9.235 -            val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
   9.236 -              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
   9.237 -            val clause = (raw, hyps)
   9.238 -            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   9.239 -          in
   9.240 -            clause
   9.241 -          end
   9.242 -      | NO_CLAUSE =>
   9.243 -          (* prove the clause, using information from 'clause_table' *)
   9.244 -          let
   9.245 -            val _ =
   9.246 -              if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
   9.247 -            val ids = the (Inttab.lookup clause_table id)
   9.248 -            val clause = resolve_raw_clauses ctxt (map prove_clause ids)
   9.249 -            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   9.250 -            val _ =
   9.251 -              if !trace_sat then
   9.252 -                tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
   9.253 -              else ()
   9.254 -          in
   9.255 -            clause
   9.256 -          end)
   9.257 -
   9.258 -    val _ = counter := 0
   9.259 -    val empty_clause = fst (prove_clause empty_id)
   9.260 -    val _ =
   9.261 -      if !trace_sat then
   9.262 -        tracing ("Proof reconstruction successful; " ^
   9.263 -          string_of_int (!counter) ^ " resolution step(s) total.")
   9.264 -      else ()
   9.265 -  in
   9.266 -    empty_clause
   9.267 -  end;
   9.268 -
   9.269 -(* ------------------------------------------------------------------------- *)
   9.270 -(* string_of_prop_formula: return a human-readable string representation of  *)
   9.271 -(*      a 'prop_formula' (just for tracing)                                  *)
   9.272 -(* ------------------------------------------------------------------------- *)
   9.273 -
   9.274 -fun string_of_prop_formula Prop_Logic.True = "True"
   9.275 -  | string_of_prop_formula Prop_Logic.False = "False"
   9.276 -  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
   9.277 -  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
   9.278 -  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
   9.279 -      "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   9.280 -  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
   9.281 -      "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
   9.282 -
   9.283 -(* ------------------------------------------------------------------------- *)
   9.284 -(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   9.285 -(*      a proof from the resulting proof trace of the SAT solver.  The       *)
   9.286 -(*      theorem returned is just "False" (with some of the given clauses as  *)
   9.287 -(*      hyps).                                                               *)
   9.288 -(* ------------------------------------------------------------------------- *)
   9.289 -
   9.290 -fun rawsat_thm ctxt clauses =
   9.291 -  let
   9.292 -    (* remove premises that equal "True" *)
   9.293 -    val clauses' = filter (fn clause =>
   9.294 -      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
   9.295 -        handle TERM ("dest_Trueprop", _) => true) clauses
   9.296 -    (* remove non-clausal premises -- of course this shouldn't actually   *)
   9.297 -    (* remove anything as long as 'rawsat_tac' is only called after the   *)
   9.298 -    (* premises have been converted to clauses                            *)
   9.299 -    val clauses'' = filter (fn clause =>
   9.300 -      ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
   9.301 -        handle TERM ("dest_Trueprop", _) => false)
   9.302 -      orelse (
   9.303 -        warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
   9.304 -        false)) clauses'
   9.305 -    (* remove trivial clauses -- this is necessary because zChaff removes *)
   9.306 -    (* trivial clauses during preprocessing, and otherwise our clause     *)
   9.307 -    (* numbering would be off                                             *)
   9.308 -    val nontrivial_clauses =
   9.309 -      filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
   9.310 -    (* sort clauses according to the term order -- an optimization,       *)
   9.311 -    (* useful because forming the union of hypotheses, as done by         *)
   9.312 -    (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
   9.313 -    (* terms sorted in descending order, while only linear for terms      *)
   9.314 -    (* sorted in ascending order                                          *)
   9.315 -    val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   9.316 -    val _ =
   9.317 -      if !trace_sat then
   9.318 -        tracing ("Sorted non-trivial clauses:\n" ^
   9.319 -          cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
   9.320 -      else ()
   9.321 -    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
   9.322 -    val (fms, atom_table) =
   9.323 -      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
   9.324 -        sorted_clauses Termtab.empty
   9.325 -    val _ =
   9.326 -      if !trace_sat then
   9.327 -        tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
   9.328 -      else ()
   9.329 -    val fm = Prop_Logic.all fms
   9.330 -    fun make_quick_and_dirty_thm () =
   9.331 -      let
   9.332 -        val _ =
   9.333 -          if !trace_sat then
   9.334 -            tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   9.335 -          else ()
   9.336 -        val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
   9.337 -      in
   9.338 -        (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   9.339 -        (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
   9.340 -        (* clauses in ascending order (which is linear for                  *)
   9.341 -        (* 'Conjunction.intr_balanced', used below)                         *)
   9.342 -        fold Thm.weaken (rev sorted_clauses) False_thm
   9.343 -      end
   9.344 -  in
   9.345 -    case
   9.346 -      let val the_solver = ! solver
   9.347 -      in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
   9.348 -    of
   9.349 -      SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
   9.350 -       (if !trace_sat then
   9.351 -          tracing ("Proof trace from SAT solver:\n" ^
   9.352 -            "clauses: " ^ ML_Syntax.print_list
   9.353 -              (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
   9.354 -              (Inttab.dest clause_table) ^ "\n" ^
   9.355 -            "empty clause: " ^ string_of_int empty_id)
   9.356 -        else ();
   9.357 -        if Config.get ctxt quick_and_dirty then
   9.358 -          make_quick_and_dirty_thm ()
   9.359 -        else
   9.360 -          let
   9.361 -            (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
   9.362 -            (*               this avoids accumulation of hypotheses during resolution    *)
   9.363 -            (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
   9.364 -            val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
   9.365 -            (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
   9.366 -            val cnf_cterm = cprop_of clauses_thm
   9.367 -            val cnf_thm = Thm.assume cnf_cterm
   9.368 -            (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
   9.369 -            val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
   9.370 -            (* initialize the clause array with the given clauses *)
   9.371 -            val max_idx = fst (the (Inttab.max clause_table))
   9.372 -            val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
   9.373 -            val _ =
   9.374 -              fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
   9.375 -                cnf_clauses 0
   9.376 -            (* replay the proof to derive the empty clause *)
   9.377 -            (* [c_1 && ... && c_n] |- False *)
   9.378 -            val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
   9.379 -          in
   9.380 -            (* [c_1, ..., c_n] |- False *)
   9.381 -            Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
   9.382 -          end)
   9.383 -    | SatSolver.UNSATISFIABLE NONE =>
   9.384 -        if Config.get ctxt quick_and_dirty then
   9.385 -         (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
   9.386 -          make_quick_and_dirty_thm ())
   9.387 -        else
   9.388 -          raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
   9.389 -    | SatSolver.SATISFIABLE assignment =>
   9.390 -        let
   9.391 -          val msg =
   9.392 -            "SAT solver found a countermodel:\n" ^
   9.393 -            (commas o map (fn (term, idx) =>
   9.394 -                Syntax.string_of_term_global @{theory} term ^ ": " ^
   9.395 -                  (case assignment idx of NONE => "arbitrary"
   9.396 -                  | SOME true => "true" | SOME false => "false")))
   9.397 -              (Termtab.dest atom_table)
   9.398 -        in
   9.399 -          raise THM (msg, 0, [])
   9.400 -        end
   9.401 -    | SatSolver.UNKNOWN =>
   9.402 -        raise THM ("SAT solver failed to decide the formula", 0, [])
   9.403 -  end;
   9.404 -
   9.405 -(* ------------------------------------------------------------------------- *)
   9.406 -(* Tactics                                                                   *)
   9.407 -(* ------------------------------------------------------------------------- *)
   9.408 -
   9.409 -(* ------------------------------------------------------------------------- *)
   9.410 -(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
   9.411 -(*      should be of the form                                                *)
   9.412 -(*        [| c1; c2; ...; ck |] ==> False                                    *)
   9.413 -(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
   9.414 -(*      or "True"                                                            *)
   9.415 -(* ------------------------------------------------------------------------- *)
   9.416 -
   9.417 -fun rawsat_tac ctxt i =
   9.418 -  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
   9.419 -    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
   9.420 -
   9.421 -(* ------------------------------------------------------------------------- *)
   9.422 -(* pre_cnf_tac: converts the i-th subgoal                                    *)
   9.423 -(*        [| A1 ; ... ; An |] ==> B                                          *)
   9.424 -(*      to                                                                   *)
   9.425 -(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
   9.426 -(*      (handling meta-logical connectives in B properly before negating),   *)
   9.427 -(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
   9.428 -(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
   9.429 -(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
   9.430 -(*      subgoal                                                              *)
   9.431 -(* ------------------------------------------------------------------------- *)
   9.432 -
   9.433 -fun pre_cnf_tac ctxt =
   9.434 -  rtac ccontr THEN'
   9.435 -  Object_Logic.atomize_prems_tac ctxt THEN'
   9.436 -  CONVERSION Drule.beta_eta_conversion;
   9.437 -
   9.438 -(* ------------------------------------------------------------------------- *)
   9.439 -(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
   9.440 -(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
   9.441 -(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
   9.442 -(*      subgoal                                                              *)
   9.443 -(* ------------------------------------------------------------------------- *)
   9.444 -
   9.445 -fun cnfsat_tac ctxt i =
   9.446 -  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
   9.447 -
   9.448 -(* ------------------------------------------------------------------------- *)
   9.449 -(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   9.450 -(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
   9.451 -(*      CNF formula becomes a separate premise) and existential quantifiers, *)
   9.452 -(*      then applies 'rawsat_tac' to solve the subgoal                       *)
   9.453 -(* ------------------------------------------------------------------------- *)
   9.454 -
   9.455 -fun cnfxsat_tac ctxt i =
   9.456 -  (etac FalseE i) ORELSE
   9.457 -    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
   9.458 -
   9.459 -(* ------------------------------------------------------------------------- *)
   9.460 -(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
   9.461 -(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
   9.462 -(*      an exponential blowup.                                               *)
   9.463 -(* ------------------------------------------------------------------------- *)
   9.464 -
   9.465 -fun sat_tac ctxt i =
   9.466 -  pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
   9.467 -
   9.468 -(* ------------------------------------------------------------------------- *)
   9.469 -(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   9.470 -(*      arbitrary formula.  The input is translated to CNF, possibly         *)
   9.471 -(*      introducing new literals.                                            *)
   9.472 -(* ------------------------------------------------------------------------- *)
   9.473 -
   9.474 -fun satx_tac ctxt i =
   9.475 -  pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
   9.476 -
   9.477 -end;
    10.1 --- a/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 20:38:29 2014 +0000
    10.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 22:02:20 2014 +0100
    10.3 @@ -3,14 +3,17 @@
    10.4      Copyright   2005-2009
    10.5  *)
    10.6  
    10.7 -header {* Examples for the 'sat' and 'satx' tactic *}
    10.8 +header {* Examples for proof methods "sat" and "satx" *}
    10.9  
   10.10  theory SAT_Examples imports Main
   10.11  begin
   10.12  
   10.13 -(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
   10.14 -(* ML {* sat.solver := "minisat_with_proofs"; *} *)
   10.15 -ML {* sat.trace_sat := true; *}
   10.16 +(*
   10.17 +declare [[sat_solver = zchaff_with_proofs]]
   10.18 +declare [[sat_solver = minisat_with_proofs]]
   10.19 +*)
   10.20 +
   10.21 +declare [[sat_trace]]
   10.22  declare [[quick_and_dirty]]
   10.23  
   10.24  lemma "True"
   10.25 @@ -24,13 +27,13 @@
   10.26  
   10.27  lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
   10.28  (*
   10.29 -apply (tactic {* cnf.cnf_rewrite_tac 1 *})
   10.30 +apply (tactic {* CNF.cnf_rewrite_tac @{context} 1 *})
   10.31  *)
   10.32  by sat
   10.33  
   10.34  lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
   10.35  (*
   10.36 -apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
   10.37 +apply (tactic {* CNF.cnfx_rewrite_tac @{context} 1 *})
   10.38  apply (erule exE | erule conjE)+
   10.39  *)
   10.40  by satx
   10.41 @@ -38,14 +41,14 @@
   10.42  lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
   10.43    \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
   10.44  (*
   10.45 -apply (tactic {* cnf.cnf_rewrite_tac 1 *})
   10.46 +apply (tactic {* CNF.cnf_rewrite_tac @{context} 1 *})
   10.47  *)
   10.48  by sat
   10.49  
   10.50  lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
   10.51    \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
   10.52  (*
   10.53 -apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
   10.54 +apply (tactic {* CNF.cnfx_rewrite_tac @{context} 1 *})
   10.55  apply (erule exE | erule conjE)+
   10.56  *)
   10.57  by satx
   10.58 @@ -77,11 +80,11 @@
   10.59  lemma "(ALL x. P x) | ~ All P"
   10.60  by sat
   10.61  
   10.62 -ML {* sat.trace_sat := false; *}
   10.63 +declare [[sat_trace = false]]
   10.64  declare [[quick_and_dirty = false]]
   10.65  
   10.66  method_setup rawsat = {*
   10.67 -  Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
   10.68 +  Scan.succeed (SIMPLE_METHOD' o SAT.rawsat_tac)
   10.69  *} "SAT solver (no preprocessing)"
   10.70  
   10.71  (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
   10.72 @@ -519,27 +522,25 @@
   10.73  the number of resolution steps in the proof.
   10.74  *}
   10.75  
   10.76 -(* ML {*
   10.77 -sat.solver := "zchaff_with_proofs";
   10.78 -sat.trace_sat := false;
   10.79 -*}
   10.80 +(*
   10.81 +declare [[sat_solver = zchaff_with_proofs]]
   10.82 +declare [[sat_trace = false]]
   10.83  declare [[quick_and_dirty = false]]
   10.84  *)
   10.85 -
   10.86  ML {*
   10.87 -fun benchmark dimacsfile =
   10.88 -let
   10.89 -  val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
   10.90 -  fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
   10.91 -    | and_to_list fm acc = rev (fm :: acc)
   10.92 -  val clauses = and_to_list prop_fm []
   10.93 -  val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
   10.94 -  val cterms = map (Thm.cterm_of @{theory}) terms
   10.95 -  val start = Timing.start ()
   10.96 -  val _ = sat.rawsat_thm @{context} cterms
   10.97 -in
   10.98 -  (Timing.result start, ! sat.counter)
   10.99 -end;
  10.100 +  fun benchmark dimacsfile =
  10.101 +    let
  10.102 +      val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
  10.103 +      fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
  10.104 +        | and_to_list fm acc = rev (fm :: acc)
  10.105 +      val clauses = and_to_list prop_fm []
  10.106 +      val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
  10.107 +      val cterms = map (Thm.cterm_of @{theory}) terms
  10.108 +      val start = Timing.start ()
  10.109 +      val _ = SAT.rawsat_thm @{context} cterms
  10.110 +    in
  10.111 +      (Timing.result start, ! SAT.counter)
  10.112 +    end;
  10.113  *}
  10.114  
  10.115  end