rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
authorblanchet
Mon Sep 27 10:44:08 2010 +0200 (2010-09-27)
changeset 397200b93a954da4f
parent 39719 b876d7525e72
child 39721 76a61ca09d5d
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/meson_clausifier.ML
src/HOL/Tools/Sledgehammer/meson_tactic.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 27 09:17:24 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 27 10:44:08 2010 +0200
     1.3 @@ -316,8 +316,7 @@
     1.4    Tools/recdef.ML \
     1.5    Tools/record.ML \
     1.6    Tools/semiring_normalizer.ML \
     1.7 -  Tools/Sledgehammer/clausifier.ML \
     1.8 -  Tools/Sledgehammer/meson_tactic.ML \
     1.9 +  Tools/Sledgehammer/meson_clausifier.ML \
    1.10    Tools/Sledgehammer/metis_reconstruct.ML \
    1.11    Tools/Sledgehammer/metis_translate.ML \
    1.12    Tools/Sledgehammer/metis_tactics.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Mon Sep 27 09:17:24 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Mon Sep 27 10:44:08 2010 +0200
     2.3 @@ -14,8 +14,7 @@
     2.4    ("Tools/ATP/atp_proof.ML")
     2.5    ("Tools/ATP/atp_systems.ML")
     2.6    ("~~/src/Tools/Metis/metis.ML")
     2.7 -  ("Tools/Sledgehammer/clausifier.ML")
     2.8 -  ("Tools/Sledgehammer/meson_tactic.ML")
     2.9 +  ("Tools/Sledgehammer/meson_clausifier.ML")
    2.10    ("Tools/Sledgehammer/metis_translate.ML")
    2.11    ("Tools/Sledgehammer/metis_reconstruct.ML")
    2.12    ("Tools/Sledgehammer/metis_tactics.ML")
    2.13 @@ -99,9 +98,8 @@
    2.14  setup ATP_Systems.setup
    2.15  
    2.16  use "~~/src/Tools/Metis/metis.ML"
    2.17 -use "Tools/Sledgehammer/clausifier.ML"
    2.18 -use "Tools/Sledgehammer/meson_tactic.ML"
    2.19 -setup Meson_Tactic.setup
    2.20 +use "Tools/Sledgehammer/meson_clausifier.ML"
    2.21 +setup Meson_Clausifier.setup
    2.22  
    2.23  use "Tools/Sledgehammer/metis_translate.ML"
    2.24  use "Tools/Sledgehammer/metis_reconstruct.ML"
     3.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Sep 27 09:17:24 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,254 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Sledgehammer/clausifier.ML
     3.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3.6 -    Author:     Jasmin Blanchette, TU Muenchen
     3.7 -
     3.8 -Transformation of axiom rules (elim/intro/etc) into CNF forms.
     3.9 -*)
    3.10 -
    3.11 -signature CLAUSIFIER =
    3.12 -sig
    3.13 -  val extensionalize_theorem : thm -> thm
    3.14 -  val introduce_combinators_in_cterm : cterm -> thm
    3.15 -  val introduce_combinators_in_theorem : thm -> thm
    3.16 -  val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
    3.17 -  val cnf_axiom : theory -> thm -> thm list
    3.18 -end;
    3.19 -
    3.20 -structure Clausifier : CLAUSIFIER =
    3.21 -struct
    3.22 -
    3.23 -(**** Transformation of Elimination Rules into First-Order Formulas****)
    3.24 -
    3.25 -val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    3.26 -val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
    3.27 -
    3.28 -(* Converts an elim-rule into an equivalent theorem that does not have the
    3.29 -   predicate variable. Leaves other theorems unchanged. We simply instantiate
    3.30 -   the conclusion variable to False. (Cf. "transform_elim_term" in
    3.31 -   "Sledgehammer_Util".) *)
    3.32 -fun transform_elim_theorem th =
    3.33 -  case concl_of th of    (*conclusion variable*)
    3.34 -       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    3.35 -           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    3.36 -    | v as Var(_, @{typ prop}) =>
    3.37 -           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    3.38 -    | _ => th
    3.39 -
    3.40 -
    3.41 -(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    3.42 -
    3.43 -fun mk_skolem t =
    3.44 -  let val T = fastype_of t in
    3.45 -    Const (@{const_name skolem}, T --> T) $ t
    3.46 -  end
    3.47 -
    3.48 -fun beta_eta_under_lambdas (Abs (s, T, t')) =
    3.49 -    Abs (s, T, beta_eta_under_lambdas t')
    3.50 -  | beta_eta_under_lambdas t = Envir.beta_eta_contract t
    3.51 -
    3.52 -(*Traverse a theorem, accumulating Skolem function definitions.*)
    3.53 -fun assume_skolem_funs th =
    3.54 -  let
    3.55 -    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
    3.56 -        (*Existential: declare a Skolem function, then insert into body and continue*)
    3.57 -        let
    3.58 -          val args = OldTerm.term_frees body
    3.59 -          (* Forms a lambda-abstraction over the formal parameters *)
    3.60 -          val rhs =
    3.61 -            list_abs_free (map dest_Free args,
    3.62 -                           HOLogic.choice_const T $ beta_eta_under_lambdas body)
    3.63 -            |> mk_skolem
    3.64 -          val comb = list_comb (rhs, args)
    3.65 -        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    3.66 -      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    3.67 -        (*Universal quant: insert a free variable into body and continue*)
    3.68 -        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    3.69 -        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
    3.70 -      | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    3.71 -      | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    3.72 -      | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
    3.73 -      | dec_sko _ rhss = rhss
    3.74 -  in  dec_sko (prop_of th) []  end;
    3.75 -
    3.76 -
    3.77 -(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    3.78 -
    3.79 -val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
    3.80 -
    3.81 -(* Removes the lambdas from an equation of the form "t = (%x. u)".
    3.82 -   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
    3.83 -fun extensionalize_theorem th =
    3.84 -  case prop_of th of
    3.85 -    _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
    3.86 -         $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
    3.87 -  | _ => th
    3.88 -
    3.89 -fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
    3.90 -  | is_quasi_lambda_free (t1 $ t2) =
    3.91 -    is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
    3.92 -  | is_quasi_lambda_free (Abs _) = false
    3.93 -  | is_quasi_lambda_free _ = true
    3.94 -
    3.95 -val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
    3.96 -val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
    3.97 -val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
    3.98 -
    3.99 -(* FIXME: Requires more use of cterm constructors. *)
   3.100 -fun abstract ct =
   3.101 -  let
   3.102 -      val thy = theory_of_cterm ct
   3.103 -      val Abs(x,_,body) = term_of ct
   3.104 -      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
   3.105 -      val cxT = ctyp_of thy xT
   3.106 -      val cbodyT = ctyp_of thy bodyT
   3.107 -      fun makeK () =
   3.108 -        instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
   3.109 -                     @{thm abs_K}
   3.110 -  in
   3.111 -      case body of
   3.112 -          Const _ => makeK()
   3.113 -        | Free _ => makeK()
   3.114 -        | Var _ => makeK()  (*though Var isn't expected*)
   3.115 -        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   3.116 -        | rator$rand =>
   3.117 -            if loose_bvar1 (rator,0) then (*C or S*)
   3.118 -               if loose_bvar1 (rand,0) then (*S*)
   3.119 -                 let val crator = cterm_of thy (Abs(x,xT,rator))
   3.120 -                     val crand = cterm_of thy (Abs(x,xT,rand))
   3.121 -                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
   3.122 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
   3.123 -                 in
   3.124 -                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
   3.125 -                 end
   3.126 -               else (*C*)
   3.127 -                 let val crator = cterm_of thy (Abs(x,xT,rator))
   3.128 -                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
   3.129 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
   3.130 -                 in
   3.131 -                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
   3.132 -                 end
   3.133 -            else if loose_bvar1 (rand,0) then (*B or eta*)
   3.134 -               if rand = Bound 0 then Thm.eta_conversion ct
   3.135 -               else (*B*)
   3.136 -                 let val crand = cterm_of thy (Abs(x,xT,rand))
   3.137 -                     val crator = cterm_of thy rator
   3.138 -                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
   3.139 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
   3.140 -                 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
   3.141 -            else makeK()
   3.142 -        | _ => raise Fail "abstract: Bad term"
   3.143 -  end;
   3.144 -
   3.145 -(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
   3.146 -fun introduce_combinators_in_cterm ct =
   3.147 -  if is_quasi_lambda_free (term_of ct) then
   3.148 -    Thm.reflexive ct
   3.149 -  else case term_of ct of
   3.150 -    Abs _ =>
   3.151 -    let
   3.152 -      val (cv, cta) = Thm.dest_abs NONE ct
   3.153 -      val (v, _) = dest_Free (term_of cv)
   3.154 -      val u_th = introduce_combinators_in_cterm cta
   3.155 -      val cu = Thm.rhs_of u_th
   3.156 -      val comb_eq = abstract (Thm.cabs cv cu)
   3.157 -    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   3.158 -  | _ $ _ =>
   3.159 -    let val (ct1, ct2) = Thm.dest_comb ct in
   3.160 -        Thm.combination (introduce_combinators_in_cterm ct1)
   3.161 -                        (introduce_combinators_in_cterm ct2)
   3.162 -    end
   3.163 -
   3.164 -fun introduce_combinators_in_theorem th =
   3.165 -  if is_quasi_lambda_free (prop_of th) then
   3.166 -    th
   3.167 -  else
   3.168 -    let
   3.169 -      val th = Drule.eta_contraction_rule th
   3.170 -      val eqth = introduce_combinators_in_cterm (cprop_of th)
   3.171 -    in Thm.equal_elim eqth th end
   3.172 -    handle THM (msg, _, _) =>
   3.173 -           (warning ("Error in the combinator translation of " ^
   3.174 -                     Display.string_of_thm_without_context th ^
   3.175 -                     "\nException message: " ^ msg ^ ".");
   3.176 -            (* A type variable of sort "{}" will make abstraction fail. *)
   3.177 -            TrueI)
   3.178 -
   3.179 -(*cterms are used throughout for efficiency*)
   3.180 -val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
   3.181 -
   3.182 -(*Given an abstraction over n variables, replace the bound variables by free
   3.183 -  ones. Return the body, along with the list of free variables.*)
   3.184 -fun c_variant_abs_multi (ct0, vars) =
   3.185 -      let val (cv,ct) = Thm.dest_abs NONE ct0
   3.186 -      in  c_variant_abs_multi (ct, cv::vars)  end
   3.187 -      handle CTERM _ => (ct0, rev vars);
   3.188 -
   3.189 -val skolem_def_raw = @{thms skolem_def_raw}
   3.190 -
   3.191 -(* Given the definition of a Skolem function, return a theorem to replace
   3.192 -   an existential formula by a use of that function.
   3.193 -   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   3.194 -fun skolem_theorem_of_def thy rhs0 =
   3.195 -  let
   3.196 -    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
   3.197 -    val rhs' = rhs |> Thm.dest_comb |> snd
   3.198 -    val (ch, frees) = c_variant_abs_multi (rhs', [])
   3.199 -    val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
   3.200 -    val T =
   3.201 -      case hilbert of
   3.202 -        Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
   3.203 -      | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
   3.204 -    val cex = cterm_of thy (HOLogic.exists_const T)
   3.205 -    val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
   3.206 -    val conc =
   3.207 -      Drule.list_comb (rhs, frees)
   3.208 -      |> Drule.beta_conv cabs |> Thm.capply cTrueprop
   3.209 -    fun tacf [prem] =
   3.210 -      rewrite_goals_tac skolem_def_raw
   3.211 -      THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
   3.212 -  in
   3.213 -    Goal.prove_internal [ex_tm] conc tacf
   3.214 -    |> forall_intr_list frees
   3.215 -    |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   3.216 -    |> Thm.varifyT_global
   3.217 -  end
   3.218 -
   3.219 -(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
   3.220 -   into NNF. *)
   3.221 -fun to_nnf th ctxt0 =
   3.222 -  let
   3.223 -    val th1 = th |> transform_elim_theorem |> zero_var_indexes
   3.224 -    val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
   3.225 -    val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
   3.226 -                  |> extensionalize_theorem
   3.227 -                  |> Meson.make_nnf ctxt
   3.228 -  in (th3, ctxt) end
   3.229 -
   3.230 -fun to_definitional_cnf_with_quantifiers thy th =
   3.231 -  let
   3.232 -    val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
   3.233 -    val eqth = eqth RS @{thm eq_reflection}
   3.234 -    val eqth = eqth RS @{thm TruepropI}
   3.235 -  in Thm.equal_elim eqth th end
   3.236 -
   3.237 -(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
   3.238 -fun cnf_axiom thy th =
   3.239 -  let
   3.240 -    val ctxt0 = Variable.global_thm_context th
   3.241 -    val (nnf_th, ctxt) = to_nnf th ctxt0
   3.242 -    fun aux th =
   3.243 -      Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
   3.244 -                     th ctxt
   3.245 -    val (cnf_ths, ctxt) =
   3.246 -      aux nnf_th
   3.247 -      |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
   3.248 -           | p => p)
   3.249 -  in
   3.250 -    cnf_ths |> map introduce_combinators_in_theorem
   3.251 -            |> Variable.export ctxt ctxt0
   3.252 -            |> Meson.finish_cnf
   3.253 -            |> map Thm.close_derivation
   3.254 -  end
   3.255 -  handle THM _ => []
   3.256 -
   3.257 -end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Sledgehammer/meson_clausifier.ML	Mon Sep 27 10:44:08 2010 +0200
     4.3 @@ -0,0 +1,267 @@
     4.4 +(*  Title:      HOL/Tools/Sledgehammer/clausifier.ML
     4.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4.6 +    Author:     Jasmin Blanchette, TU Muenchen
     4.7 +
     4.8 +Transformation of axiom rules (elim/intro/etc) into CNF forms.
     4.9 +*)
    4.10 +
    4.11 +signature MESON_CLAUSIFIER =
    4.12 +sig
    4.13 +  val extensionalize_theorem : thm -> thm
    4.14 +  val introduce_combinators_in_cterm : cterm -> thm
    4.15 +  val introduce_combinators_in_theorem : thm -> thm
    4.16 +  val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
    4.17 +  val cnf_axiom : theory -> thm -> thm list
    4.18 +  val meson_general_tac : Proof.context -> thm list -> int -> tactic
    4.19 +  val setup: theory -> theory
    4.20 +end;
    4.21 +
    4.22 +structure Meson_Clausifier : MESON_CLAUSIFIER =
    4.23 +struct
    4.24 +
    4.25 +(**** Transformation of Elimination Rules into First-Order Formulas****)
    4.26 +
    4.27 +val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    4.28 +val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
    4.29 +
    4.30 +(* Converts an elim-rule into an equivalent theorem that does not have the
    4.31 +   predicate variable. Leaves other theorems unchanged. We simply instantiate
    4.32 +   the conclusion variable to False. (Cf. "transform_elim_term" in
    4.33 +   "Sledgehammer_Util".) *)
    4.34 +fun transform_elim_theorem th =
    4.35 +  case concl_of th of    (*conclusion variable*)
    4.36 +       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    4.37 +           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    4.38 +    | v as Var(_, @{typ prop}) =>
    4.39 +           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    4.40 +    | _ => th
    4.41 +
    4.42 +
    4.43 +(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    4.44 +
    4.45 +fun mk_skolem t =
    4.46 +  let val T = fastype_of t in
    4.47 +    Const (@{const_name skolem}, T --> T) $ t
    4.48 +  end
    4.49 +
    4.50 +fun beta_eta_under_lambdas (Abs (s, T, t')) =
    4.51 +    Abs (s, T, beta_eta_under_lambdas t')
    4.52 +  | beta_eta_under_lambdas t = Envir.beta_eta_contract t
    4.53 +
    4.54 +(*Traverse a theorem, accumulating Skolem function definitions.*)
    4.55 +fun assume_skolem_funs th =
    4.56 +  let
    4.57 +    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
    4.58 +        (*Existential: declare a Skolem function, then insert into body and continue*)
    4.59 +        let
    4.60 +          val args = OldTerm.term_frees body
    4.61 +          (* Forms a lambda-abstraction over the formal parameters *)
    4.62 +          val rhs =
    4.63 +            list_abs_free (map dest_Free args,
    4.64 +                           HOLogic.choice_const T $ beta_eta_under_lambdas body)
    4.65 +            |> mk_skolem
    4.66 +          val comb = list_comb (rhs, args)
    4.67 +        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    4.68 +      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    4.69 +        (*Universal quant: insert a free variable into body and continue*)
    4.70 +        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    4.71 +        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
    4.72 +      | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    4.73 +      | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    4.74 +      | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
    4.75 +      | dec_sko _ rhss = rhss
    4.76 +  in  dec_sko (prop_of th) []  end;
    4.77 +
    4.78 +
    4.79 +(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    4.80 +
    4.81 +val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
    4.82 +
    4.83 +(* Removes the lambdas from an equation of the form "t = (%x. u)".
    4.84 +   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
    4.85 +fun extensionalize_theorem th =
    4.86 +  case prop_of th of
    4.87 +    _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
    4.88 +         $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
    4.89 +  | _ => th
    4.90 +
    4.91 +fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
    4.92 +  | is_quasi_lambda_free (t1 $ t2) =
    4.93 +    is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
    4.94 +  | is_quasi_lambda_free (Abs _) = false
    4.95 +  | is_quasi_lambda_free _ = true
    4.96 +
    4.97 +val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
    4.98 +val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
    4.99 +val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
   4.100 +
   4.101 +(* FIXME: Requires more use of cterm constructors. *)
   4.102 +fun abstract ct =
   4.103 +  let
   4.104 +      val thy = theory_of_cterm ct
   4.105 +      val Abs(x,_,body) = term_of ct
   4.106 +      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
   4.107 +      val cxT = ctyp_of thy xT
   4.108 +      val cbodyT = ctyp_of thy bodyT
   4.109 +      fun makeK () =
   4.110 +        instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
   4.111 +                     @{thm abs_K}
   4.112 +  in
   4.113 +      case body of
   4.114 +          Const _ => makeK()
   4.115 +        | Free _ => makeK()
   4.116 +        | Var _ => makeK()  (*though Var isn't expected*)
   4.117 +        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   4.118 +        | rator$rand =>
   4.119 +            if loose_bvar1 (rator,0) then (*C or S*)
   4.120 +               if loose_bvar1 (rand,0) then (*S*)
   4.121 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
   4.122 +                     val crand = cterm_of thy (Abs(x,xT,rand))
   4.123 +                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
   4.124 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
   4.125 +                 in
   4.126 +                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
   4.127 +                 end
   4.128 +               else (*C*)
   4.129 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
   4.130 +                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
   4.131 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
   4.132 +                 in
   4.133 +                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
   4.134 +                 end
   4.135 +            else if loose_bvar1 (rand,0) then (*B or eta*)
   4.136 +               if rand = Bound 0 then Thm.eta_conversion ct
   4.137 +               else (*B*)
   4.138 +                 let val crand = cterm_of thy (Abs(x,xT,rand))
   4.139 +                     val crator = cterm_of thy rator
   4.140 +                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
   4.141 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
   4.142 +                 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
   4.143 +            else makeK()
   4.144 +        | _ => raise Fail "abstract: Bad term"
   4.145 +  end;
   4.146 +
   4.147 +(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
   4.148 +fun introduce_combinators_in_cterm ct =
   4.149 +  if is_quasi_lambda_free (term_of ct) then
   4.150 +    Thm.reflexive ct
   4.151 +  else case term_of ct of
   4.152 +    Abs _ =>
   4.153 +    let
   4.154 +      val (cv, cta) = Thm.dest_abs NONE ct
   4.155 +      val (v, _) = dest_Free (term_of cv)
   4.156 +      val u_th = introduce_combinators_in_cterm cta
   4.157 +      val cu = Thm.rhs_of u_th
   4.158 +      val comb_eq = abstract (Thm.cabs cv cu)
   4.159 +    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   4.160 +  | _ $ _ =>
   4.161 +    let val (ct1, ct2) = Thm.dest_comb ct in
   4.162 +        Thm.combination (introduce_combinators_in_cterm ct1)
   4.163 +                        (introduce_combinators_in_cterm ct2)
   4.164 +    end
   4.165 +
   4.166 +fun introduce_combinators_in_theorem th =
   4.167 +  if is_quasi_lambda_free (prop_of th) then
   4.168 +    th
   4.169 +  else
   4.170 +    let
   4.171 +      val th = Drule.eta_contraction_rule th
   4.172 +      val eqth = introduce_combinators_in_cterm (cprop_of th)
   4.173 +    in Thm.equal_elim eqth th end
   4.174 +    handle THM (msg, _, _) =>
   4.175 +           (warning ("Error in the combinator translation of " ^
   4.176 +                     Display.string_of_thm_without_context th ^
   4.177 +                     "\nException message: " ^ msg ^ ".");
   4.178 +            (* A type variable of sort "{}" will make abstraction fail. *)
   4.179 +            TrueI)
   4.180 +
   4.181 +(*cterms are used throughout for efficiency*)
   4.182 +val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
   4.183 +
   4.184 +(*Given an abstraction over n variables, replace the bound variables by free
   4.185 +  ones. Return the body, along with the list of free variables.*)
   4.186 +fun c_variant_abs_multi (ct0, vars) =
   4.187 +      let val (cv,ct) = Thm.dest_abs NONE ct0
   4.188 +      in  c_variant_abs_multi (ct, cv::vars)  end
   4.189 +      handle CTERM _ => (ct0, rev vars);
   4.190 +
   4.191 +val skolem_def_raw = @{thms skolem_def_raw}
   4.192 +
   4.193 +(* Given the definition of a Skolem function, return a theorem to replace
   4.194 +   an existential formula by a use of that function.
   4.195 +   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   4.196 +fun skolem_theorem_of_def thy rhs0 =
   4.197 +  let
   4.198 +    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
   4.199 +    val rhs' = rhs |> Thm.dest_comb |> snd
   4.200 +    val (ch, frees) = c_variant_abs_multi (rhs', [])
   4.201 +    val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
   4.202 +    val T =
   4.203 +      case hilbert of
   4.204 +        Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
   4.205 +      | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
   4.206 +    val cex = cterm_of thy (HOLogic.exists_const T)
   4.207 +    val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
   4.208 +    val conc =
   4.209 +      Drule.list_comb (rhs, frees)
   4.210 +      |> Drule.beta_conv cabs |> Thm.capply cTrueprop
   4.211 +    fun tacf [prem] =
   4.212 +      rewrite_goals_tac skolem_def_raw
   4.213 +      THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
   4.214 +  in
   4.215 +    Goal.prove_internal [ex_tm] conc tacf
   4.216 +    |> forall_intr_list frees
   4.217 +    |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   4.218 +    |> Thm.varifyT_global
   4.219 +  end
   4.220 +
   4.221 +(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
   4.222 +   into NNF. *)
   4.223 +fun to_nnf th ctxt0 =
   4.224 +  let
   4.225 +    val th1 = th |> transform_elim_theorem |> zero_var_indexes
   4.226 +    val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
   4.227 +    val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
   4.228 +                  |> extensionalize_theorem
   4.229 +                  |> Meson.make_nnf ctxt
   4.230 +  in (th3, ctxt) end
   4.231 +
   4.232 +fun to_definitional_cnf_with_quantifiers thy th =
   4.233 +  let
   4.234 +    val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
   4.235 +    val eqth = eqth RS @{thm eq_reflection}
   4.236 +    val eqth = eqth RS @{thm TruepropI}
   4.237 +  in Thm.equal_elim eqth th end
   4.238 +
   4.239 +(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
   4.240 +fun cnf_axiom thy th =
   4.241 +  let
   4.242 +    val ctxt0 = Variable.global_thm_context th
   4.243 +    val (nnf_th, ctxt) = to_nnf th ctxt0
   4.244 +    fun aux th =
   4.245 +      Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
   4.246 +                     th ctxt
   4.247 +    val (cnf_ths, ctxt) =
   4.248 +      aux nnf_th
   4.249 +      |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
   4.250 +           | p => p)
   4.251 +  in
   4.252 +    cnf_ths |> map introduce_combinators_in_theorem
   4.253 +            |> Variable.export ctxt ctxt0
   4.254 +            |> Meson.finish_cnf
   4.255 +            |> map Thm.close_derivation
   4.256 +  end
   4.257 +  handle THM _ => []
   4.258 +
   4.259 +fun meson_general_tac ctxt ths =
   4.260 +  let
   4.261 +    val thy = ProofContext.theory_of ctxt
   4.262 +    val ctxt0 = Classical.put_claset HOL_cs ctxt
   4.263 +  in Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) end
   4.264 +
   4.265 +val setup =
   4.266 +  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
   4.267 +    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
   4.268 +    "MESON resolution proof procedure";
   4.269 +
   4.270 +end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Mon Sep 27 09:17:24 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,28 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
     5.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     5.6 -    Author:     Jasmin Blanchette, TU Muenchen
     5.7 -
     5.8 -MESON general tactic and proof method.
     5.9 -*)
    5.10 -
    5.11 -signature MESON_TACTIC =
    5.12 -sig
    5.13 -  val meson_general_tac : Proof.context -> thm list -> int -> tactic
    5.14 -  val setup: theory -> theory
    5.15 -end;
    5.16 -
    5.17 -structure Meson_Tactic : MESON_TACTIC =
    5.18 -struct
    5.19 -
    5.20 -fun meson_general_tac ctxt ths =
    5.21 -  let
    5.22 -    val thy = ProofContext.theory_of ctxt
    5.23 -    val ctxt0 = Classical.put_claset HOL_cs ctxt
    5.24 -  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
    5.25 -
    5.26 -val setup =
    5.27 -  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    5.28 -    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    5.29 -    "MESON resolution proof procedure";
    5.30 -
    5.31 -end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 27 09:17:24 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 27 10:44:08 2010 +0200
     6.3 @@ -56,7 +56,8 @@
     6.4    let val thy = ProofContext.theory_of ctxt
     6.5        val type_lits = Config.get ctxt type_lits
     6.6        val th_cls_pairs =
     6.7 -        map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0
     6.8 +        map (fn th => (Thm.get_name_hint th,
     6.9 +                       Meson_Clausifier.cnf_axiom thy th)) ths0
    6.10        val ths = maps #2 th_cls_pairs
    6.11        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    6.12        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
    6.13 @@ -116,7 +117,7 @@
    6.14     does, but also keep an unextensionalized version of "th" for backward
    6.15     compatibility. *)
    6.16  fun also_extensionalize_theorem th =
    6.17 -  let val th' = Clausifier.extensionalize_theorem th in
    6.18 +  let val th' = Meson_Clausifier.extensionalize_theorem th in
    6.19      if Thm.eq_thm (th, th') then [th]
    6.20      else th :: Meson.make_clauses_unsorted [th']
    6.21    end
    6.22 @@ -125,7 +126,7 @@
    6.23    single
    6.24    #> Meson.make_clauses_unsorted
    6.25    #> maps also_extensionalize_theorem
    6.26 -  #> map Clausifier.introduce_combinators_in_theorem
    6.27 +  #> map Meson_Clausifier.introduce_combinators_in_theorem
    6.28    #> Meson.finish_cnf
    6.29  
    6.30  fun preskolem_tac ctxt st0 =
     7.1 --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML	Mon Sep 27 09:17:24 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML	Mon Sep 27 10:44:08 2010 +0200
     7.3 @@ -554,7 +554,8 @@
     7.4         Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
     7.5  
     7.6  (*The fully-typed translation, to avoid type errors*)
     7.7 -fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
     7.8 +fun wrap_type (tm, ty) =
     7.9 +  Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
    7.10  
    7.11  fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
    7.12    | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Sep 27 09:17:24 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Sep 27 10:44:08 2010 +0200
     8.3 @@ -94,7 +94,7 @@
     8.4                      (0 upto length Ts - 1 ~~ Ts))
     8.5  
     8.6  (* Removes the lambdas from an equation of the form "t = (%x. u)".
     8.7 -   (Cf. "extensionalize_theorem" in "Clausifier".) *)
     8.8 +   (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *)
     8.9  fun extensionalize_term t =
    8.10    let
    8.11      fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
    8.12 @@ -141,7 +141,7 @@
    8.13                     t |> conceal_bounds Ts
    8.14                       |> Envir.eta_contract
    8.15                       |> cterm_of thy
    8.16 -                     |> Clausifier.introduce_combinators_in_cterm
    8.17 +                     |> Meson_Clausifier.introduce_combinators_in_cterm
    8.18                       |> prop_of |> Logic.dest_equals |> snd
    8.19                       |> reveal_bounds Ts
    8.20          val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 27 09:17:24 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 27 10:44:08 2010 +0200
     9.3 @@ -98,7 +98,7 @@
     9.4  (* Converts an elim-rule into an equivalent theorem that does not have the
     9.5     predicate variable. Leaves other theorems unchanged. We simply instantiate
     9.6     the conclusion variable to False. (Cf. "transform_elim_theorem" in
     9.7 -   "Clausifier".) *)
     9.8 +   "Meson_Clausifier".) *)
     9.9  fun transform_elim_term t =
    9.10    case Logic.strip_imp_concl t of
    9.11      @{const Trueprop} $ Var (z, @{typ bool}) =>