renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
authorblanchet
Fri Jun 25 16:15:03 2010 +0200 (2010-06-25)
changeset 37574b8c1f4c46983
parent 37573 7f987e8582a7
child 37575 cfc5e281740f
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/meson_tactic.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 25 16:03:34 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 25 16:15:03 2010 +0200
     1.3 @@ -313,11 +313,11 @@
     1.4    Tools/Quotient/quotient_typ.ML \
     1.5    Tools/recdef.ML \
     1.6    Tools/semiring_normalizer.ML \
     1.7 +  Tools/Sledgehammer/clausifier.ML \
     1.8    Tools/Sledgehammer/meson_tactic.ML \
     1.9    Tools/Sledgehammer/metis_tactics.ML \
    1.10    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
    1.11    Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
    1.12 -  Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
    1.13    Tools/Sledgehammer/sledgehammer_fol_clause.ML \
    1.14    Tools/Sledgehammer/sledgehammer_hol_clause.ML \
    1.15    Tools/Sledgehammer/sledgehammer_isar.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 25 16:03:34 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 16:15:03 2010 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  imports Plain Hilbert_Choice
     2.5  uses
     2.6    "~~/src/Tools/Metis/metis.ML"
     2.7 -  ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
     2.8 +  ("Tools/Sledgehammer/clausifier.ML")
     2.9    ("Tools/Sledgehammer/meson_tactic.ML")
    2.10    ("Tools/Sledgehammer/sledgehammer_util.ML")
    2.11    ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
    2.12 @@ -85,8 +85,8 @@
    2.13  apply (simp add: COMBC_def) 
    2.14  done
    2.15  
    2.16 -use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
    2.17 -setup Sledgehammer_Fact_Preprocessor.setup
    2.18 +use "Tools/Sledgehammer/clausifier.ML"
    2.19 +setup Clausifier.setup
    2.20  use "Tools/Sledgehammer/meson_tactic.ML"
    2.21  setup Meson_Tactic.setup
    2.22  
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 16:03:34 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 16:15:03 2010 +0200
     3.3 @@ -8,8 +8,8 @@
     3.4  
     3.5  signature ATP_MANAGER =
     3.6  sig
     3.7 +  type cnf_thm = Clausifier.cnf_thm
     3.8    type name_pool = Sledgehammer_FOL_Clause.name_pool
     3.9 -  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
    3.10    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
    3.11    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    3.12    type params =
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 16:03:34 2010 +0200
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 16:15:03 2010 +0200
     4.3 @@ -22,8 +22,8 @@
     4.4  structure ATP_Systems : ATP_SYSTEMS =
     4.5  struct
     4.6  
     4.7 +open Clausifier
     4.8  open Sledgehammer_Util
     4.9 -open Sledgehammer_Fact_Preprocessor
    4.10  open Sledgehammer_HOL_Clause
    4.11  open Sledgehammer_Fact_Filter
    4.12  open Sledgehammer_Proof_Reconstruct
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Jun 25 16:15:03 2010 +0200
     5.3 @@ -0,0 +1,571 @@
     5.4 +(*  Title:      HOL/Tools/Sledgehammer/clausifier.ML
     5.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory
     5.6 +    Author:     Jasmin Blanchette, TU Muenchen
     5.7 +
     5.8 +Transformation of axiom rules (elim/intro/etc) into CNF forms.
     5.9 +*)
    5.10 +
    5.11 +signature CLAUSIFIER =
    5.12 +sig
    5.13 +  type cnf_thm = thm * ((string * int) * thm)
    5.14 +
    5.15 +  val sledgehammer_prefix: string
    5.16 +  val chained_prefix: string
    5.17 +  val trace: bool Unsynchronized.ref
    5.18 +  val trace_msg: (unit -> string) -> unit
    5.19 +  val name_thms_pair_from_ref :
    5.20 +    Proof.context -> thm list -> Facts.ref -> string * thm list
    5.21 +  val skolem_theory_name: string
    5.22 +  val skolem_prefix: string
    5.23 +  val skolem_infix: string
    5.24 +  val is_skolem_const_name: string -> bool
    5.25 +  val num_type_args: theory -> string -> int
    5.26 +  val cnf_axiom: theory -> thm -> thm list
    5.27 +  val multi_base_blacklist: string list
    5.28 +  val is_theorem_bad_for_atps: thm -> bool
    5.29 +  val type_has_topsort: typ -> bool
    5.30 +  val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
    5.31 +  val saturate_skolem_cache: theory -> theory option
    5.32 +  val auto_saturate_skolem_cache: bool Unsynchronized.ref
    5.33 +  val neg_clausify: thm -> thm list
    5.34 +  val neg_conjecture_clauses:
    5.35 +    Proof.context -> thm -> int -> thm list list * (string * typ) list
    5.36 +  val setup: theory -> theory
    5.37 +end;
    5.38 +
    5.39 +structure Clausifier : CLAUSIFIER =
    5.40 +struct
    5.41 +
    5.42 +type cnf_thm = thm * ((string * int) * thm)
    5.43 +
    5.44 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    5.45 +
    5.46 +(* Used to label theorems chained into the goal. *)
    5.47 +val chained_prefix = sledgehammer_prefix ^ "chained_"
    5.48 +
    5.49 +val trace = Unsynchronized.ref false;
    5.50 +fun trace_msg msg = if !trace then tracing (msg ()) else ();
    5.51 +
    5.52 +fun name_thms_pair_from_ref ctxt chained_ths xref =
    5.53 +  let
    5.54 +    val ths = ProofContext.get_fact ctxt xref
    5.55 +    val name = Facts.string_of_ref xref
    5.56 +               |> forall (member Thm.eq_thm chained_ths) ths
    5.57 +                  ? prefix chained_prefix
    5.58 +  in (name, ths) end
    5.59 +
    5.60 +val skolem_theory_name = sledgehammer_prefix ^ "Sko"
    5.61 +val skolem_prefix = "sko_"
    5.62 +val skolem_infix = "$"
    5.63 +
    5.64 +val type_has_topsort = Term.exists_subtype
    5.65 +  (fn TFree (_, []) => true
    5.66 +    | TVar (_, []) => true
    5.67 +    | _ => false);
    5.68 +
    5.69 +
    5.70 +(**** Transformation of Elimination Rules into First-Order Formulas****)
    5.71 +
    5.72 +val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    5.73 +val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
    5.74 +
    5.75 +(*Converts an elim-rule into an equivalent theorem that does not have the
    5.76 +  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
    5.77 +  conclusion variable to False.*)
    5.78 +fun transform_elim th =
    5.79 +  case concl_of th of    (*conclusion variable*)
    5.80 +       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    5.81 +           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    5.82 +    | v as Var(_, @{typ prop}) =>
    5.83 +           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    5.84 +    | _ => th;
    5.85 +
    5.86 +(*To enforce single-threading*)
    5.87 +exception Clausify_failure of theory;
    5.88 +
    5.89 +
    5.90 +(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    5.91 +
    5.92 +(*Keep the full complexity of the original name*)
    5.93 +fun flatten_name s = space_implode "_X" (Long_Name.explode s);
    5.94 +
    5.95 +fun skolem_name thm_name j var_name =
    5.96 +  skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
    5.97 +  skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
    5.98 +
    5.99 +(* Hack: Could return false positives (e.g., a user happens to declare a
   5.100 +   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
   5.101 +val is_skolem_const_name =
   5.102 +  Long_Name.base_name
   5.103 +  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
   5.104 +
   5.105 +(* The number of type arguments of a constant, zero if it's monomorphic. For
   5.106 +   (instances of) Skolem pseudoconstants, this information is encoded in the
   5.107 +   constant name. *)
   5.108 +fun num_type_args thy s =
   5.109 +  if String.isPrefix skolem_theory_name s then
   5.110 +    s |> unprefix skolem_theory_name
   5.111 +      |> space_explode skolem_infix |> hd
   5.112 +      |> space_explode "_" |> List.last |> Int.fromString |> the
   5.113 +  else
   5.114 +    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
   5.115 +
   5.116 +fun rhs_extra_types lhsT rhs =
   5.117 +  let val lhs_vars = Term.add_tfreesT lhsT []
   5.118 +      fun add_new_TFrees (TFree v) =
   5.119 +            if member (op =) lhs_vars v then I else insert (op =) (TFree v)
   5.120 +        | add_new_TFrees _ = I
   5.121 +      val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
   5.122 +  in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
   5.123 +
   5.124 +fun skolem_type_and_args bound_T body =
   5.125 +  let
   5.126 +    val args1 = OldTerm.term_frees body
   5.127 +    val Ts1 = map type_of args1
   5.128 +    val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
   5.129 +    val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
   5.130 +  in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
   5.131 +
   5.132 +(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
   5.133 +   suggested prefix for the Skolem constants. *)
   5.134 +fun declare_skolem_funs s th thy =
   5.135 +  let
   5.136 +    val skolem_count = Unsynchronized.ref 0    (* FIXME ??? *)
   5.137 +    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
   5.138 +                (axs, thy) =
   5.139 +        (*Existential: declare a Skolem function, then insert into body and continue*)
   5.140 +        let
   5.141 +          val id = skolem_name s (Unsynchronized.inc skolem_count) s'
   5.142 +          val (cT, args) = skolem_type_and_args T body
   5.143 +          val rhs = list_abs_free (map dest_Free args,
   5.144 +                                   HOLogic.choice_const T $ body)
   5.145 +                  (*Forms a lambda-abstraction over the formal parameters*)
   5.146 +          val (c, thy) =
   5.147 +            Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
   5.148 +          val cdef = id ^ "_def"
   5.149 +          val ((_, ax), thy) =
   5.150 +            Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
   5.151 +          val ax' = Drule.export_without_context ax
   5.152 +        in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
   5.153 +      | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
   5.154 +        (*Universal quant: insert a free variable into body and continue*)
   5.155 +        let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
   5.156 +        in dec_sko (subst_bound (Free (fname, T), p)) thx end
   5.157 +      | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
   5.158 +      | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
   5.159 +      | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
   5.160 +      | dec_sko _ thx = thx
   5.161 +  in dec_sko (prop_of th) ([], thy) end
   5.162 +
   5.163 +fun mk_skolem_id t =
   5.164 +  let val T = fastype_of t in
   5.165 +    Const (@{const_name skolem_id}, T --> T) $ t
   5.166 +  end
   5.167 +
   5.168 +fun quasi_beta_eta_contract (Abs (s, T, t')) =
   5.169 +    Abs (s, T, quasi_beta_eta_contract t')
   5.170 +  | quasi_beta_eta_contract t = Envir.beta_eta_contract t
   5.171 +
   5.172 +(*Traverse a theorem, accumulating Skolem function definitions.*)
   5.173 +fun assume_skolem_funs s th =
   5.174 +  let
   5.175 +    val skolem_count = Unsynchronized.ref 0   (* FIXME ??? *)
   5.176 +    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
   5.177 +        (*Existential: declare a Skolem function, then insert into body and continue*)
   5.178 +        let
   5.179 +          val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   5.180 +          val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
   5.181 +          val Ts = map type_of args
   5.182 +          val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
   5.183 +          val id = skolem_name s (Unsynchronized.inc skolem_count) s'
   5.184 +          val c = Free (id, cT) (* FIXME: needed? ### *)
   5.185 +          (* Forms a lambda-abstraction over the formal parameters *)
   5.186 +          val rhs =
   5.187 +            list_abs_free (map dest_Free args,
   5.188 +                           HOLogic.choice_const T
   5.189 +                           $ quasi_beta_eta_contract body)
   5.190 +            |> mk_skolem_id
   5.191 +          val def = Logic.mk_equals (c, rhs)
   5.192 +          val comb = list_comb (rhs, args)
   5.193 +        in dec_sko (subst_bound (comb, p)) (def :: defs) end
   5.194 +      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
   5.195 +        (*Universal quant: insert a free variable into body and continue*)
   5.196 +        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
   5.197 +        in dec_sko (subst_bound (Free(fname,T), p)) defs end
   5.198 +      | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
   5.199 +      | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
   5.200 +      | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
   5.201 +      | dec_sko _ defs = defs
   5.202 +  in  dec_sko (prop_of th) []  end;
   5.203 +
   5.204 +
   5.205 +(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
   5.206 +
   5.207 +(*Returns the vars of a theorem*)
   5.208 +fun vars_of_thm th =
   5.209 +  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
   5.210 +
   5.211 +val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
   5.212 +
   5.213 +(* Removes the lambdas from an equation of the form t = (%x. u). *)
   5.214 +fun extensionalize th =
   5.215 +  case prop_of th of
   5.216 +    _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
   5.217 +         $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
   5.218 +  | _ => th
   5.219 +
   5.220 +fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
   5.221 +  | is_quasi_lambda_free (t1 $ t2) =
   5.222 +    is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   5.223 +  | is_quasi_lambda_free (Abs _) = false
   5.224 +  | is_quasi_lambda_free _ = true
   5.225 +
   5.226 +val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
   5.227 +val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
   5.228 +val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
   5.229 +
   5.230 +(*FIXME: requires more use of cterm constructors*)
   5.231 +fun abstract ct =
   5.232 +  let
   5.233 +      val thy = theory_of_cterm ct
   5.234 +      val Abs(x,_,body) = term_of ct
   5.235 +      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
   5.236 +      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
   5.237 +      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
   5.238 +  in
   5.239 +      case body of
   5.240 +          Const _ => makeK()
   5.241 +        | Free _ => makeK()
   5.242 +        | Var _ => makeK()  (*though Var isn't expected*)
   5.243 +        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   5.244 +        | rator$rand =>
   5.245 +            if loose_bvar1 (rator,0) then (*C or S*)
   5.246 +               if loose_bvar1 (rand,0) then (*S*)
   5.247 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
   5.248 +                     val crand = cterm_of thy (Abs(x,xT,rand))
   5.249 +                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
   5.250 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
   5.251 +                 in
   5.252 +                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
   5.253 +                 end
   5.254 +               else (*C*)
   5.255 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
   5.256 +                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
   5.257 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
   5.258 +                 in
   5.259 +                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
   5.260 +                 end
   5.261 +            else if loose_bvar1 (rand,0) then (*B or eta*)
   5.262 +               if rand = Bound 0 then Thm.eta_conversion ct
   5.263 +               else (*B*)
   5.264 +                 let val crand = cterm_of thy (Abs(x,xT,rand))
   5.265 +                     val crator = cterm_of thy rator
   5.266 +                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
   5.267 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
   5.268 +                 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
   5.269 +            else makeK()
   5.270 +        | _ => raise Fail "abstract: Bad term"
   5.271 +  end;
   5.272 +
   5.273 +(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
   5.274 +fun do_introduce_combinators ct =
   5.275 +  if is_quasi_lambda_free (term_of ct) then
   5.276 +    Thm.reflexive ct
   5.277 +  else case term_of ct of
   5.278 +    Abs _ =>
   5.279 +    let
   5.280 +      val (cv, cta) = Thm.dest_abs NONE ct
   5.281 +      val (v, _) = dest_Free (term_of cv)
   5.282 +      val u_th = do_introduce_combinators cta
   5.283 +      val cu = Thm.rhs_of u_th
   5.284 +      val comb_eq = abstract (Thm.cabs cv cu)
   5.285 +    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   5.286 +  | _ $ _ =>
   5.287 +    let val (ct1, ct2) = Thm.dest_comb ct in
   5.288 +        Thm.combination (do_introduce_combinators ct1)
   5.289 +                        (do_introduce_combinators ct2)
   5.290 +    end
   5.291 +
   5.292 +fun introduce_combinators th =
   5.293 +  if is_quasi_lambda_free (prop_of th) then
   5.294 +    th
   5.295 +  else
   5.296 +    let
   5.297 +      val th = Drule.eta_contraction_rule th
   5.298 +      val eqth = do_introduce_combinators (cprop_of th)
   5.299 +    in Thm.equal_elim eqth th end
   5.300 +    handle THM (msg, _, _) =>
   5.301 +           (warning ("Error in the combinator translation of " ^
   5.302 +                     Display.string_of_thm_without_context th ^
   5.303 +                     "\nException message: " ^ msg ^ ".");
   5.304 +            (* A type variable of sort "{}" will make abstraction fail. *)
   5.305 +            TrueI)
   5.306 +
   5.307 +(*cterms are used throughout for efficiency*)
   5.308 +val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
   5.309 +
   5.310 +(*cterm version of mk_cTrueprop*)
   5.311 +fun c_mkTrueprop A = Thm.capply cTrueprop A;
   5.312 +
   5.313 +(*Given an abstraction over n variables, replace the bound variables by free
   5.314 +  ones. Return the body, along with the list of free variables.*)
   5.315 +fun c_variant_abs_multi (ct0, vars) =
   5.316 +      let val (cv,ct) = Thm.dest_abs NONE ct0
   5.317 +      in  c_variant_abs_multi (ct, cv::vars)  end
   5.318 +      handle CTERM _ => (ct0, rev vars);
   5.319 +
   5.320 +(*Given the definition of a Skolem function, return a theorem to replace
   5.321 +  an existential formula by a use of that function.
   5.322 +   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   5.323 +fun skolem_theorem_of_def inline def =
   5.324 +  let
   5.325 +      val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of
   5.326 +                         |> Thm.dest_equals
   5.327 +      val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
   5.328 +      val (ch, frees) = c_variant_abs_multi (rhs', [])
   5.329 +      val (chilbert, cabs) = ch |> Thm.dest_comb
   5.330 +      val thy = Thm.theory_of_cterm chilbert
   5.331 +      val t = Thm.term_of chilbert
   5.332 +      val T =
   5.333 +        case t of
   5.334 +          Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
   5.335 +        | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
   5.336 +      val cex = Thm.cterm_of thy (HOLogic.exists_const T)
   5.337 +      val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
   5.338 +      and conc =
   5.339 +        Drule.list_comb (if inline then rhs else c, frees)
   5.340 +        |> Drule.beta_conv cabs |> c_mkTrueprop
   5.341 +      fun tacf [prem] =
   5.342 +        (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
   5.343 +         else rewrite_goals_tac [def])
   5.344 +        THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
   5.345 +                   RS @{thm someI_ex}) 1
   5.346 +  in  Goal.prove_internal [ex_tm] conc tacf
   5.347 +       |> forall_intr_list frees
   5.348 +       |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   5.349 +       |> Thm.varifyT_global
   5.350 +  end;
   5.351 +
   5.352 +
   5.353 +(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
   5.354 +fun to_nnf th ctxt0 =
   5.355 +  let val th1 = th |> transform_elim |> zero_var_indexes
   5.356 +      val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
   5.357 +      val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
   5.358 +                    |> extensionalize
   5.359 +                    |> Meson.make_nnf ctxt
   5.360 +  in  (th3, ctxt)  end;
   5.361 +
   5.362 +(*Generate Skolem functions for a theorem supplied in nnf*)
   5.363 +fun skolem_theorems_of_assume s th =
   5.364 +  map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th))
   5.365 +      (assume_skolem_funs s th)
   5.366 +
   5.367 +
   5.368 +(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
   5.369 +
   5.370 +val max_lambda_nesting = 3
   5.371 +
   5.372 +fun term_has_too_many_lambdas max (t1 $ t2) =
   5.373 +    exists (term_has_too_many_lambdas max) [t1, t2]
   5.374 +  | term_has_too_many_lambdas max (Abs (_, _, t)) =
   5.375 +    max = 0 orelse term_has_too_many_lambdas (max - 1) t
   5.376 +  | term_has_too_many_lambdas _ _ = false
   5.377 +
   5.378 +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
   5.379 +
   5.380 +(* Don't count nested lambdas at the level of formulas, since they are
   5.381 +   quantifiers. *)
   5.382 +fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
   5.383 +    formula_has_too_many_lambdas (T :: Ts) t
   5.384 +  | formula_has_too_many_lambdas Ts t =
   5.385 +    if is_formula_type (fastype_of1 (Ts, t)) then
   5.386 +      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
   5.387 +    else
   5.388 +      term_has_too_many_lambdas max_lambda_nesting t
   5.389 +
   5.390 +(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
   5.391 +   was 11. *)
   5.392 +val max_apply_depth = 15
   5.393 +
   5.394 +fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   5.395 +  | apply_depth (Abs (_, _, t)) = apply_depth t
   5.396 +  | apply_depth _ = 0
   5.397 +
   5.398 +fun is_formula_too_complex t =
   5.399 +  apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
   5.400 +  formula_has_too_many_lambdas [] t
   5.401 +
   5.402 +fun is_strange_thm th =
   5.403 +  case head_of (concl_of th) of
   5.404 +      Const (a, _) => (a <> @{const_name Trueprop} andalso
   5.405 +                       a <> @{const_name "=="})
   5.406 +    | _ => false;
   5.407 +
   5.408 +fun is_theorem_bad_for_atps thm =
   5.409 +  let val t = prop_of thm in
   5.410 +    is_formula_too_complex t orelse exists_type type_has_topsort t orelse
   5.411 +    is_strange_thm thm
   5.412 +  end
   5.413 +
   5.414 +(* FIXME: put other record thms here, or declare as "no_atp" *)
   5.415 +val multi_base_blacklist =
   5.416 +  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
   5.417 +   "split_asm", "cases", "ext_cases"];
   5.418 +
   5.419 +fun fake_name th =
   5.420 +  if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
   5.421 +  else gensym "unknown_thm_";
   5.422 +
   5.423 +(*Skolemize a named theorem, with Skolem functions as additional premises.*)
   5.424 +fun skolemize_theorem s th =
   5.425 +  if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
   5.426 +     is_theorem_bad_for_atps th then
   5.427 +    []
   5.428 +  else
   5.429 +    let
   5.430 +      val ctxt0 = Variable.global_thm_context th
   5.431 +      val (nnfth, ctxt) = to_nnf th ctxt0
   5.432 +      val defs = skolem_theorems_of_assume s nnfth
   5.433 +      val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
   5.434 +    in
   5.435 +      cnfs |> map introduce_combinators
   5.436 +           |> Variable.export ctxt ctxt0
   5.437 +           |> Meson.finish_cnf
   5.438 +    end
   5.439 +    handle THM _ => []
   5.440 +
   5.441 +(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   5.442 +  Skolem functions.*)
   5.443 +structure ThmCache = Theory_Data
   5.444 +(
   5.445 +  type T = thm list Thmtab.table * unit Symtab.table;
   5.446 +  val empty = (Thmtab.empty, Symtab.empty);
   5.447 +  val extend = I;
   5.448 +  fun merge ((cache1, seen1), (cache2, seen2)) : T =
   5.449 +    (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
   5.450 +);
   5.451 +
   5.452 +val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
   5.453 +val already_seen = Symtab.defined o #2 o ThmCache.get;
   5.454 +
   5.455 +val update_cache = ThmCache.map o apfst o Thmtab.update;
   5.456 +fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
   5.457 +
   5.458 +(* Convert Isabelle theorems into axiom clauses. *)
   5.459 +fun cnf_axiom thy th0 =
   5.460 +  let val th = Thm.transfer thy th0 in
   5.461 +    case lookup_cache thy th of
   5.462 +      SOME cls => cls
   5.463 +    | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
   5.464 +  end;
   5.465 +
   5.466 +
   5.467 +(**** Translate a set of theorems into CNF ****)
   5.468 +
   5.469 +(*The combination of rev and tail recursion preserves the original order*)
   5.470 +fun cnf_rules_pairs thy =
   5.471 +  let
   5.472 +    fun do_one _ [] = []
   5.473 +      | do_one ((name, k), th) (cls :: clss) =
   5.474 +        (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
   5.475 +    fun do_all pairs [] = pairs
   5.476 +      | do_all pairs ((name, th) :: ths) =
   5.477 +        let
   5.478 +          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
   5.479 +                          handle THM _ => []
   5.480 +        in do_all (new_pairs @ pairs) ths end
   5.481 +  in do_all [] o rev end
   5.482 +
   5.483 +
   5.484 +(**** Convert all facts of the theory into FOL or HOL clauses ****)
   5.485 +
   5.486 +local
   5.487 +
   5.488 +fun skolem_def (name, th) thy =
   5.489 +  let val ctxt0 = Variable.global_thm_context th in
   5.490 +    case try (to_nnf th) ctxt0 of
   5.491 +      NONE => (NONE, thy)
   5.492 +    | SOME (nnfth, ctxt) =>
   5.493 +      let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
   5.494 +      in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
   5.495 +  end;
   5.496 +
   5.497 +fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
   5.498 +  let
   5.499 +    val (cnfs, ctxt) =
   5.500 +      Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
   5.501 +    val cnfs' = cnfs
   5.502 +      |> map introduce_combinators
   5.503 +      |> Variable.export ctxt ctxt0
   5.504 +      |> Meson.finish_cnf
   5.505 +      |> map Thm.close_derivation;
   5.506 +    in (th, cnfs') end;
   5.507 +
   5.508 +in
   5.509 +
   5.510 +fun saturate_skolem_cache thy =
   5.511 +  let
   5.512 +    val facts = PureThy.facts_of thy;
   5.513 +    val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
   5.514 +      if Facts.is_concealed facts name orelse already_seen thy name then I
   5.515 +      else cons (name, ths));
   5.516 +    val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
   5.517 +      if member (op =) multi_base_blacklist (Long_Name.base_name name) then
   5.518 +        I
   5.519 +      else
   5.520 +        fold_index (fn (i, th) =>
   5.521 +          if is_theorem_bad_for_atps th orelse
   5.522 +             is_some (lookup_cache thy th) then
   5.523 +            I
   5.524 +          else
   5.525 +            cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
   5.526 +  in
   5.527 +    if null new_facts then
   5.528 +      NONE
   5.529 +    else
   5.530 +      let
   5.531 +        val (defs, thy') = thy
   5.532 +          |> fold (mark_seen o #1) new_facts
   5.533 +          |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
   5.534 +          |>> map_filter I;
   5.535 +        val cache_entries = Par_List.map skolem_cnfs defs;
   5.536 +      in SOME (fold update_cache cache_entries thy') end
   5.537 +  end;
   5.538 +
   5.539 +end;
   5.540 +
   5.541 +(* For emergency use where the Skolem cache causes problems. *)
   5.542 +val auto_saturate_skolem_cache = Unsynchronized.ref true
   5.543 +
   5.544 +fun conditionally_saturate_skolem_cache thy =
   5.545 +  if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
   5.546 +
   5.547 +
   5.548 +(*** Converting a subgoal into negated conjecture clauses. ***)
   5.549 +
   5.550 +fun neg_skolemize_tac ctxt =
   5.551 +  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
   5.552 +
   5.553 +val neg_clausify =
   5.554 +  single
   5.555 +  #> Meson.make_clauses_unsorted
   5.556 +  #> map introduce_combinators
   5.557 +  #> Meson.finish_cnf
   5.558 +
   5.559 +fun neg_conjecture_clauses ctxt st0 n =
   5.560 +  let
   5.561 +    (* "Option" is thrown if the assumptions contain schematic variables. *)
   5.562 +    val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
   5.563 +    val ({params, prems, ...}, _) =
   5.564 +      Subgoal.focus (Variable.set_body false ctxt) n st
   5.565 +  in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
   5.566 +
   5.567 +
   5.568 +(** setup **)
   5.569 +
   5.570 +val setup =
   5.571 +  perhaps conditionally_saturate_skolem_cache
   5.572 +  #> Theory.at_end conditionally_saturate_skolem_cache
   5.573 +
   5.574 +end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Fri Jun 25 16:03:34 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Fri Jun 25 16:15:03 2010 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4  structure Meson_Tactic : MESON_TACTIC =
     6.5  struct
     6.6  
     6.7 -open Sledgehammer_Fact_Preprocessor
     6.8 +open Clausifier
     6.9  
    6.10  (*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
    6.11  fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
     7.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 16:03:34 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 16:15:03 2010 +0200
     7.3 @@ -18,8 +18,8 @@
     7.4  structure Metis_Tactics : METIS_TACTICS =
     7.5  struct
     7.6  
     7.7 +open Clausifier
     7.8  open Sledgehammer_Util
     7.9 -open Sledgehammer_Fact_Preprocessor
    7.10  open Sledgehammer_FOL_Clause
    7.11  open Sledgehammer_HOL_Clause
    7.12  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 16:03:34 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 16:15:03 2010 +0200
     8.3 @@ -5,7 +5,7 @@
     8.4  
     8.5  signature SLEDGEHAMMER_FACT_FILTER =
     8.6  sig
     8.7 -  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
     8.8 +  type cnf_thm = Clausifier.cnf_thm
     8.9  
    8.10    type relevance_override =
    8.11      {add: Facts.ref list,
    8.12 @@ -21,8 +21,8 @@
    8.13  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    8.14  struct
    8.15  
    8.16 +open Clausifier
    8.17  open Sledgehammer_FOL_Clause
    8.18 -open Sledgehammer_Fact_Preprocessor
    8.19  open Sledgehammer_HOL_Clause
    8.20  
    8.21  (* Experimental feature: Filter theorems in natural form or in CNF? *)
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 16:03:34 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 16:15:03 2010 +0200
     9.3 @@ -18,8 +18,8 @@
     9.4  structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
     9.5  struct
     9.6  
     9.7 +open Clausifier
     9.8  open Sledgehammer_Util
     9.9 -open Sledgehammer_Fact_Preprocessor
    9.10  open Sledgehammer_HOL_Clause
    9.11  open Sledgehammer_Proof_Reconstruct
    9.12  open ATP_Manager
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 16:03:34 2010 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,571 +0,0 @@
    10.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
    10.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory
    10.6 -    Author:     Jasmin Blanchette, TU Muenchen
    10.7 -
    10.8 -Transformation of axiom rules (elim/intro/etc) into CNF forms.
    10.9 -*)
   10.10 -
   10.11 -signature SLEDGEHAMMER_FACT_PREPROCESSOR =
   10.12 -sig
   10.13 -  type cnf_thm = thm * ((string * int) * thm)
   10.14 -
   10.15 -  val sledgehammer_prefix: string
   10.16 -  val chained_prefix: string
   10.17 -  val trace: bool Unsynchronized.ref
   10.18 -  val trace_msg: (unit -> string) -> unit
   10.19 -  val name_thms_pair_from_ref :
   10.20 -    Proof.context -> thm list -> Facts.ref -> string * thm list
   10.21 -  val skolem_theory_name: string
   10.22 -  val skolem_prefix: string
   10.23 -  val skolem_infix: string
   10.24 -  val is_skolem_const_name: string -> bool
   10.25 -  val num_type_args: theory -> string -> int
   10.26 -  val cnf_axiom: theory -> thm -> thm list
   10.27 -  val multi_base_blacklist: string list
   10.28 -  val is_theorem_bad_for_atps: thm -> bool
   10.29 -  val type_has_topsort: typ -> bool
   10.30 -  val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
   10.31 -  val saturate_skolem_cache: theory -> theory option
   10.32 -  val auto_saturate_skolem_cache: bool Unsynchronized.ref
   10.33 -  val neg_clausify: thm -> thm list
   10.34 -  val neg_conjecture_clauses:
   10.35 -    Proof.context -> thm -> int -> thm list list * (string * typ) list
   10.36 -  val setup: theory -> theory
   10.37 -end;
   10.38 -
   10.39 -structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
   10.40 -struct
   10.41 -
   10.42 -type cnf_thm = thm * ((string * int) * thm)
   10.43 -
   10.44 -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
   10.45 -
   10.46 -(* Used to label theorems chained into the goal. *)
   10.47 -val chained_prefix = sledgehammer_prefix ^ "chained_"
   10.48 -
   10.49 -val trace = Unsynchronized.ref false;
   10.50 -fun trace_msg msg = if !trace then tracing (msg ()) else ();
   10.51 -
   10.52 -fun name_thms_pair_from_ref ctxt chained_ths xref =
   10.53 -  let
   10.54 -    val ths = ProofContext.get_fact ctxt xref
   10.55 -    val name = Facts.string_of_ref xref
   10.56 -               |> forall (member Thm.eq_thm chained_ths) ths
   10.57 -                  ? prefix chained_prefix
   10.58 -  in (name, ths) end
   10.59 -
   10.60 -val skolem_theory_name = sledgehammer_prefix ^ "Sko"
   10.61 -val skolem_prefix = "sko_"
   10.62 -val skolem_infix = "$"
   10.63 -
   10.64 -val type_has_topsort = Term.exists_subtype
   10.65 -  (fn TFree (_, []) => true
   10.66 -    | TVar (_, []) => true
   10.67 -    | _ => false);
   10.68 -
   10.69 -
   10.70 -(**** Transformation of Elimination Rules into First-Order Formulas****)
   10.71 -
   10.72 -val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
   10.73 -val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
   10.74 -
   10.75 -(*Converts an elim-rule into an equivalent theorem that does not have the
   10.76 -  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
   10.77 -  conclusion variable to False.*)
   10.78 -fun transform_elim th =
   10.79 -  case concl_of th of    (*conclusion variable*)
   10.80 -       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
   10.81 -           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
   10.82 -    | v as Var(_, @{typ prop}) =>
   10.83 -           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
   10.84 -    | _ => th;
   10.85 -
   10.86 -(*To enforce single-threading*)
   10.87 -exception Clausify_failure of theory;
   10.88 -
   10.89 -
   10.90 -(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
   10.91 -
   10.92 -(*Keep the full complexity of the original name*)
   10.93 -fun flatten_name s = space_implode "_X" (Long_Name.explode s);
   10.94 -
   10.95 -fun skolem_name thm_name j var_name =
   10.96 -  skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
   10.97 -  skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
   10.98 -
   10.99 -(* Hack: Could return false positives (e.g., a user happens to declare a
  10.100 -   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
  10.101 -val is_skolem_const_name =
  10.102 -  Long_Name.base_name
  10.103 -  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
  10.104 -
  10.105 -(* The number of type arguments of a constant, zero if it's monomorphic. For
  10.106 -   (instances of) Skolem pseudoconstants, this information is encoded in the
  10.107 -   constant name. *)
  10.108 -fun num_type_args thy s =
  10.109 -  if String.isPrefix skolem_theory_name s then
  10.110 -    s |> unprefix skolem_theory_name
  10.111 -      |> space_explode skolem_infix |> hd
  10.112 -      |> space_explode "_" |> List.last |> Int.fromString |> the
  10.113 -  else
  10.114 -    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
  10.115 -
  10.116 -fun rhs_extra_types lhsT rhs =
  10.117 -  let val lhs_vars = Term.add_tfreesT lhsT []
  10.118 -      fun add_new_TFrees (TFree v) =
  10.119 -            if member (op =) lhs_vars v then I else insert (op =) (TFree v)
  10.120 -        | add_new_TFrees _ = I
  10.121 -      val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
  10.122 -  in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
  10.123 -
  10.124 -fun skolem_type_and_args bound_T body =
  10.125 -  let
  10.126 -    val args1 = OldTerm.term_frees body
  10.127 -    val Ts1 = map type_of args1
  10.128 -    val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
  10.129 -    val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
  10.130 -  in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
  10.131 -
  10.132 -(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
  10.133 -   suggested prefix for the Skolem constants. *)
  10.134 -fun declare_skolem_funs s th thy =
  10.135 -  let
  10.136 -    val skolem_count = Unsynchronized.ref 0    (* FIXME ??? *)
  10.137 -    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
  10.138 -                (axs, thy) =
  10.139 -        (*Existential: declare a Skolem function, then insert into body and continue*)
  10.140 -        let
  10.141 -          val id = skolem_name s (Unsynchronized.inc skolem_count) s'
  10.142 -          val (cT, args) = skolem_type_and_args T body
  10.143 -          val rhs = list_abs_free (map dest_Free args,
  10.144 -                                   HOLogic.choice_const T $ body)
  10.145 -                  (*Forms a lambda-abstraction over the formal parameters*)
  10.146 -          val (c, thy) =
  10.147 -            Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
  10.148 -          val cdef = id ^ "_def"
  10.149 -          val ((_, ax), thy) =
  10.150 -            Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
  10.151 -          val ax' = Drule.export_without_context ax
  10.152 -        in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
  10.153 -      | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
  10.154 -        (*Universal quant: insert a free variable into body and continue*)
  10.155 -        let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
  10.156 -        in dec_sko (subst_bound (Free (fname, T), p)) thx end
  10.157 -      | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
  10.158 -      | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
  10.159 -      | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
  10.160 -      | dec_sko _ thx = thx
  10.161 -  in dec_sko (prop_of th) ([], thy) end
  10.162 -
  10.163 -fun mk_skolem_id t =
  10.164 -  let val T = fastype_of t in
  10.165 -    Const (@{const_name skolem_id}, T --> T) $ t
  10.166 -  end
  10.167 -
  10.168 -fun quasi_beta_eta_contract (Abs (s, T, t')) =
  10.169 -    Abs (s, T, quasi_beta_eta_contract t')
  10.170 -  | quasi_beta_eta_contract t = Envir.beta_eta_contract t
  10.171 -
  10.172 -(*Traverse a theorem, accumulating Skolem function definitions.*)
  10.173 -fun assume_skolem_funs s th =
  10.174 -  let
  10.175 -    val skolem_count = Unsynchronized.ref 0   (* FIXME ??? *)
  10.176 -    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
  10.177 -        (*Existential: declare a Skolem function, then insert into body and continue*)
  10.178 -        let
  10.179 -          val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
  10.180 -          val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
  10.181 -          val Ts = map type_of args
  10.182 -          val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
  10.183 -          val id = skolem_name s (Unsynchronized.inc skolem_count) s'
  10.184 -          val c = Free (id, cT) (* FIXME: needed? ### *)
  10.185 -          (* Forms a lambda-abstraction over the formal parameters *)
  10.186 -          val rhs =
  10.187 -            list_abs_free (map dest_Free args,
  10.188 -                           HOLogic.choice_const T
  10.189 -                           $ quasi_beta_eta_contract body)
  10.190 -            |> mk_skolem_id
  10.191 -          val def = Logic.mk_equals (c, rhs)
  10.192 -          val comb = list_comb (rhs, args)
  10.193 -        in dec_sko (subst_bound (comb, p)) (def :: defs) end
  10.194 -      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
  10.195 -        (*Universal quant: insert a free variable into body and continue*)
  10.196 -        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
  10.197 -        in dec_sko (subst_bound (Free(fname,T), p)) defs end
  10.198 -      | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
  10.199 -      | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
  10.200 -      | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
  10.201 -      | dec_sko _ defs = defs
  10.202 -  in  dec_sko (prop_of th) []  end;
  10.203 -
  10.204 -
  10.205 -(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
  10.206 -
  10.207 -(*Returns the vars of a theorem*)
  10.208 -fun vars_of_thm th =
  10.209 -  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
  10.210 -
  10.211 -val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
  10.212 -
  10.213 -(* Removes the lambdas from an equation of the form t = (%x. u). *)
  10.214 -fun extensionalize th =
  10.215 -  case prop_of th of
  10.216 -    _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
  10.217 -         $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
  10.218 -  | _ => th
  10.219 -
  10.220 -fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
  10.221 -  | is_quasi_lambda_free (t1 $ t2) =
  10.222 -    is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
  10.223 -  | is_quasi_lambda_free (Abs _) = false
  10.224 -  | is_quasi_lambda_free _ = true
  10.225 -
  10.226 -val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
  10.227 -val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
  10.228 -val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
  10.229 -
  10.230 -(*FIXME: requires more use of cterm constructors*)
  10.231 -fun abstract ct =
  10.232 -  let
  10.233 -      val thy = theory_of_cterm ct
  10.234 -      val Abs(x,_,body) = term_of ct
  10.235 -      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
  10.236 -      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
  10.237 -      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
  10.238 -  in
  10.239 -      case body of
  10.240 -          Const _ => makeK()
  10.241 -        | Free _ => makeK()
  10.242 -        | Var _ => makeK()  (*though Var isn't expected*)
  10.243 -        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
  10.244 -        | rator$rand =>
  10.245 -            if loose_bvar1 (rator,0) then (*C or S*)
  10.246 -               if loose_bvar1 (rand,0) then (*S*)
  10.247 -                 let val crator = cterm_of thy (Abs(x,xT,rator))
  10.248 -                     val crand = cterm_of thy (Abs(x,xT,rand))
  10.249 -                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
  10.250 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
  10.251 -                 in
  10.252 -                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
  10.253 -                 end
  10.254 -               else (*C*)
  10.255 -                 let val crator = cterm_of thy (Abs(x,xT,rator))
  10.256 -                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
  10.257 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
  10.258 -                 in
  10.259 -                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
  10.260 -                 end
  10.261 -            else if loose_bvar1 (rand,0) then (*B or eta*)
  10.262 -               if rand = Bound 0 then Thm.eta_conversion ct
  10.263 -               else (*B*)
  10.264 -                 let val crand = cterm_of thy (Abs(x,xT,rand))
  10.265 -                     val crator = cterm_of thy rator
  10.266 -                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
  10.267 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
  10.268 -                 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
  10.269 -            else makeK()
  10.270 -        | _ => raise Fail "abstract: Bad term"
  10.271 -  end;
  10.272 -
  10.273 -(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
  10.274 -fun do_introduce_combinators ct =
  10.275 -  if is_quasi_lambda_free (term_of ct) then
  10.276 -    Thm.reflexive ct
  10.277 -  else case term_of ct of
  10.278 -    Abs _ =>
  10.279 -    let
  10.280 -      val (cv, cta) = Thm.dest_abs NONE ct
  10.281 -      val (v, _) = dest_Free (term_of cv)
  10.282 -      val u_th = do_introduce_combinators cta
  10.283 -      val cu = Thm.rhs_of u_th
  10.284 -      val comb_eq = abstract (Thm.cabs cv cu)
  10.285 -    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
  10.286 -  | _ $ _ =>
  10.287 -    let val (ct1, ct2) = Thm.dest_comb ct in
  10.288 -        Thm.combination (do_introduce_combinators ct1)
  10.289 -                        (do_introduce_combinators ct2)
  10.290 -    end
  10.291 -
  10.292 -fun introduce_combinators th =
  10.293 -  if is_quasi_lambda_free (prop_of th) then
  10.294 -    th
  10.295 -  else
  10.296 -    let
  10.297 -      val th = Drule.eta_contraction_rule th
  10.298 -      val eqth = do_introduce_combinators (cprop_of th)
  10.299 -    in Thm.equal_elim eqth th end
  10.300 -    handle THM (msg, _, _) =>
  10.301 -           (warning ("Error in the combinator translation of " ^
  10.302 -                     Display.string_of_thm_without_context th ^
  10.303 -                     "\nException message: " ^ msg ^ ".");
  10.304 -            (* A type variable of sort "{}" will make abstraction fail. *)
  10.305 -            TrueI)
  10.306 -
  10.307 -(*cterms are used throughout for efficiency*)
  10.308 -val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
  10.309 -
  10.310 -(*cterm version of mk_cTrueprop*)
  10.311 -fun c_mkTrueprop A = Thm.capply cTrueprop A;
  10.312 -
  10.313 -(*Given an abstraction over n variables, replace the bound variables by free
  10.314 -  ones. Return the body, along with the list of free variables.*)
  10.315 -fun c_variant_abs_multi (ct0, vars) =
  10.316 -      let val (cv,ct) = Thm.dest_abs NONE ct0
  10.317 -      in  c_variant_abs_multi (ct, cv::vars)  end
  10.318 -      handle CTERM _ => (ct0, rev vars);
  10.319 -
  10.320 -(*Given the definition of a Skolem function, return a theorem to replace
  10.321 -  an existential formula by a use of that function.
  10.322 -   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
  10.323 -fun skolem_theorem_of_def inline def =
  10.324 -  let
  10.325 -      val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of
  10.326 -                         |> Thm.dest_equals
  10.327 -      val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
  10.328 -      val (ch, frees) = c_variant_abs_multi (rhs', [])
  10.329 -      val (chilbert, cabs) = ch |> Thm.dest_comb
  10.330 -      val thy = Thm.theory_of_cterm chilbert
  10.331 -      val t = Thm.term_of chilbert
  10.332 -      val T =
  10.333 -        case t of
  10.334 -          Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
  10.335 -        | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
  10.336 -      val cex = Thm.cterm_of thy (HOLogic.exists_const T)
  10.337 -      val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
  10.338 -      and conc =
  10.339 -        Drule.list_comb (if inline then rhs else c, frees)
  10.340 -        |> Drule.beta_conv cabs |> c_mkTrueprop
  10.341 -      fun tacf [prem] =
  10.342 -        (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
  10.343 -         else rewrite_goals_tac [def])
  10.344 -        THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
  10.345 -                   RS @{thm someI_ex}) 1
  10.346 -  in  Goal.prove_internal [ex_tm] conc tacf
  10.347 -       |> forall_intr_list frees
  10.348 -       |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
  10.349 -       |> Thm.varifyT_global
  10.350 -  end;
  10.351 -
  10.352 -
  10.353 -(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
  10.354 -fun to_nnf th ctxt0 =
  10.355 -  let val th1 = th |> transform_elim |> zero_var_indexes
  10.356 -      val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
  10.357 -      val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
  10.358 -                    |> extensionalize
  10.359 -                    |> Meson.make_nnf ctxt
  10.360 -  in  (th3, ctxt)  end;
  10.361 -
  10.362 -(*Generate Skolem functions for a theorem supplied in nnf*)
  10.363 -fun skolem_theorems_of_assume s th =
  10.364 -  map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th))
  10.365 -      (assume_skolem_funs s th)
  10.366 -
  10.367 -
  10.368 -(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
  10.369 -
  10.370 -val max_lambda_nesting = 3
  10.371 -
  10.372 -fun term_has_too_many_lambdas max (t1 $ t2) =
  10.373 -    exists (term_has_too_many_lambdas max) [t1, t2]
  10.374 -  | term_has_too_many_lambdas max (Abs (_, _, t)) =
  10.375 -    max = 0 orelse term_has_too_many_lambdas (max - 1) t
  10.376 -  | term_has_too_many_lambdas _ _ = false
  10.377 -
  10.378 -fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
  10.379 -
  10.380 -(* Don't count nested lambdas at the level of formulas, since they are
  10.381 -   quantifiers. *)
  10.382 -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
  10.383 -    formula_has_too_many_lambdas (T :: Ts) t
  10.384 -  | formula_has_too_many_lambdas Ts t =
  10.385 -    if is_formula_type (fastype_of1 (Ts, t)) then
  10.386 -      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
  10.387 -    else
  10.388 -      term_has_too_many_lambdas max_lambda_nesting t
  10.389 -
  10.390 -(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
  10.391 -   was 11. *)
  10.392 -val max_apply_depth = 15
  10.393 -
  10.394 -fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
  10.395 -  | apply_depth (Abs (_, _, t)) = apply_depth t
  10.396 -  | apply_depth _ = 0
  10.397 -
  10.398 -fun is_formula_too_complex t =
  10.399 -  apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
  10.400 -  formula_has_too_many_lambdas [] t
  10.401 -
  10.402 -fun is_strange_thm th =
  10.403 -  case head_of (concl_of th) of
  10.404 -      Const (a, _) => (a <> @{const_name Trueprop} andalso
  10.405 -                       a <> @{const_name "=="})
  10.406 -    | _ => false;
  10.407 -
  10.408 -fun is_theorem_bad_for_atps thm =
  10.409 -  let val t = prop_of thm in
  10.410 -    is_formula_too_complex t orelse exists_type type_has_topsort t orelse
  10.411 -    is_strange_thm thm
  10.412 -  end
  10.413 -
  10.414 -(* FIXME: put other record thms here, or declare as "no_atp" *)
  10.415 -val multi_base_blacklist =
  10.416 -  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
  10.417 -   "split_asm", "cases", "ext_cases"];
  10.418 -
  10.419 -fun fake_name th =
  10.420 -  if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
  10.421 -  else gensym "unknown_thm_";
  10.422 -
  10.423 -(*Skolemize a named theorem, with Skolem functions as additional premises.*)
  10.424 -fun skolemize_theorem s th =
  10.425 -  if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
  10.426 -     is_theorem_bad_for_atps th then
  10.427 -    []
  10.428 -  else
  10.429 -    let
  10.430 -      val ctxt0 = Variable.global_thm_context th
  10.431 -      val (nnfth, ctxt) = to_nnf th ctxt0
  10.432 -      val defs = skolem_theorems_of_assume s nnfth
  10.433 -      val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
  10.434 -    in
  10.435 -      cnfs |> map introduce_combinators
  10.436 -           |> Variable.export ctxt ctxt0
  10.437 -           |> Meson.finish_cnf
  10.438 -    end
  10.439 -    handle THM _ => []
  10.440 -
  10.441 -(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
  10.442 -  Skolem functions.*)
  10.443 -structure ThmCache = Theory_Data
  10.444 -(
  10.445 -  type T = thm list Thmtab.table * unit Symtab.table;
  10.446 -  val empty = (Thmtab.empty, Symtab.empty);
  10.447 -  val extend = I;
  10.448 -  fun merge ((cache1, seen1), (cache2, seen2)) : T =
  10.449 -    (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
  10.450 -);
  10.451 -
  10.452 -val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
  10.453 -val already_seen = Symtab.defined o #2 o ThmCache.get;
  10.454 -
  10.455 -val update_cache = ThmCache.map o apfst o Thmtab.update;
  10.456 -fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
  10.457 -
  10.458 -(* Convert Isabelle theorems into axiom clauses. *)
  10.459 -fun cnf_axiom thy th0 =
  10.460 -  let val th = Thm.transfer thy th0 in
  10.461 -    case lookup_cache thy th of
  10.462 -      SOME cls => cls
  10.463 -    | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
  10.464 -  end;
  10.465 -
  10.466 -
  10.467 -(**** Translate a set of theorems into CNF ****)
  10.468 -
  10.469 -(*The combination of rev and tail recursion preserves the original order*)
  10.470 -fun cnf_rules_pairs thy =
  10.471 -  let
  10.472 -    fun do_one _ [] = []
  10.473 -      | do_one ((name, k), th) (cls :: clss) =
  10.474 -        (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
  10.475 -    fun do_all pairs [] = pairs
  10.476 -      | do_all pairs ((name, th) :: ths) =
  10.477 -        let
  10.478 -          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
  10.479 -                          handle THM _ => []
  10.480 -        in do_all (new_pairs @ pairs) ths end
  10.481 -  in do_all [] o rev end
  10.482 -
  10.483 -
  10.484 -(**** Convert all facts of the theory into FOL or HOL clauses ****)
  10.485 -
  10.486 -local
  10.487 -
  10.488 -fun skolem_def (name, th) thy =
  10.489 -  let val ctxt0 = Variable.global_thm_context th in
  10.490 -    case try (to_nnf th) ctxt0 of
  10.491 -      NONE => (NONE, thy)
  10.492 -    | SOME (nnfth, ctxt) =>
  10.493 -      let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
  10.494 -      in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
  10.495 -  end;
  10.496 -
  10.497 -fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
  10.498 -  let
  10.499 -    val (cnfs, ctxt) =
  10.500 -      Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
  10.501 -    val cnfs' = cnfs
  10.502 -      |> map introduce_combinators
  10.503 -      |> Variable.export ctxt ctxt0
  10.504 -      |> Meson.finish_cnf
  10.505 -      |> map Thm.close_derivation;
  10.506 -    in (th, cnfs') end;
  10.507 -
  10.508 -in
  10.509 -
  10.510 -fun saturate_skolem_cache thy =
  10.511 -  let
  10.512 -    val facts = PureThy.facts_of thy;
  10.513 -    val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
  10.514 -      if Facts.is_concealed facts name orelse already_seen thy name then I
  10.515 -      else cons (name, ths));
  10.516 -    val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
  10.517 -      if member (op =) multi_base_blacklist (Long_Name.base_name name) then
  10.518 -        I
  10.519 -      else
  10.520 -        fold_index (fn (i, th) =>
  10.521 -          if is_theorem_bad_for_atps th orelse
  10.522 -             is_some (lookup_cache thy th) then
  10.523 -            I
  10.524 -          else
  10.525 -            cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
  10.526 -  in
  10.527 -    if null new_facts then
  10.528 -      NONE
  10.529 -    else
  10.530 -      let
  10.531 -        val (defs, thy') = thy
  10.532 -          |> fold (mark_seen o #1) new_facts
  10.533 -          |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
  10.534 -          |>> map_filter I;
  10.535 -        val cache_entries = Par_List.map skolem_cnfs defs;
  10.536 -      in SOME (fold update_cache cache_entries thy') end
  10.537 -  end;
  10.538 -
  10.539 -end;
  10.540 -
  10.541 -(* For emergency use where the Skolem cache causes problems. *)
  10.542 -val auto_saturate_skolem_cache = Unsynchronized.ref true
  10.543 -
  10.544 -fun conditionally_saturate_skolem_cache thy =
  10.545 -  if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
  10.546 -
  10.547 -
  10.548 -(*** Converting a subgoal into negated conjecture clauses. ***)
  10.549 -
  10.550 -fun neg_skolemize_tac ctxt =
  10.551 -  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
  10.552 -
  10.553 -val neg_clausify =
  10.554 -  single
  10.555 -  #> Meson.make_clauses_unsorted
  10.556 -  #> map introduce_combinators
  10.557 -  #> Meson.finish_cnf
  10.558 -
  10.559 -fun neg_conjecture_clauses ctxt st0 n =
  10.560 -  let
  10.561 -    (* "Option" is thrown if the assumptions contain schematic variables. *)
  10.562 -    val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
  10.563 -    val ({params, prems, ...}, _) =
  10.564 -      Subgoal.focus (Variable.set_body false ctxt) n st
  10.565 -  in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
  10.566 -
  10.567 -
  10.568 -(** setup **)
  10.569 -
  10.570 -val setup =
  10.571 -  perhaps conditionally_saturate_skolem_cache
  10.572 -  #> Theory.at_end conditionally_saturate_skolem_cache
  10.573 -
  10.574 -end;
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 16:03:34 2010 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 16:15:03 2010 +0200
    11.3 @@ -7,7 +7,7 @@
    11.4  
    11.5  signature SLEDGEHAMMER_HOL_CLAUSE =
    11.6  sig
    11.7 -  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
    11.8 +  type cnf_thm = Clausifier.cnf_thm
    11.9    type name = Sledgehammer_FOL_Clause.name
   11.10    type name_pool = Sledgehammer_FOL_Clause.name_pool
   11.11    type kind = Sledgehammer_FOL_Clause.kind
   11.12 @@ -49,9 +49,9 @@
   11.13  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
   11.14  struct
   11.15  
   11.16 +open Clausifier
   11.17  open Sledgehammer_Util
   11.18  open Sledgehammer_FOL_Clause
   11.19 -open Sledgehammer_Fact_Preprocessor
   11.20  
   11.21  (******************************************************)
   11.22  (* data types for typed combinator expressions        *)
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 16:03:34 2010 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 16:15:03 2010 +0200
    12.3 @@ -17,8 +17,8 @@
    12.4  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    12.5  struct
    12.6  
    12.7 +open Clausifier
    12.8  open Sledgehammer_Util
    12.9 -open Sledgehammer_Fact_Preprocessor
   12.10  open ATP_Manager
   12.11  open ATP_Systems
   12.12  open Sledgehammer_Fact_Minimizer
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 25 16:03:34 2010 +0200
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 25 16:15:03 2010 +0200
    13.3 @@ -27,10 +27,10 @@
    13.4  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    13.5  struct
    13.6  
    13.7 +open Clausifier
    13.8  open Sledgehammer_Util
    13.9  open Sledgehammer_FOL_Clause
   13.10  open Sledgehammer_HOL_Clause
   13.11 -open Sledgehammer_Fact_Preprocessor
   13.12  
   13.13  type minimize_command = string list -> string
   13.14