# HG changeset patch # User blanchet # Date 1285577048 -7200 # Node ID 0b93a954da4f9b8473e9652ebf1e312964c1e3f5 # Parent b876d7525e7228ec11440858ff701812838ed880 rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic" diff -r b876d7525e72 -r 0b93a954da4f src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Sep 27 09:17:24 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Sep 27 10:44:08 2010 +0200 @@ -316,8 +316,7 @@ Tools/recdef.ML \ Tools/record.ML \ Tools/semiring_normalizer.ML \ - Tools/Sledgehammer/clausifier.ML \ - Tools/Sledgehammer/meson_tactic.ML \ + Tools/Sledgehammer/meson_clausifier.ML \ Tools/Sledgehammer/metis_reconstruct.ML \ Tools/Sledgehammer/metis_translate.ML \ Tools/Sledgehammer/metis_tactics.ML \ diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Sep 27 09:17:24 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Sep 27 10:44:08 2010 +0200 @@ -14,8 +14,7 @@ ("Tools/ATP/atp_proof.ML") ("Tools/ATP/atp_systems.ML") ("~~/src/Tools/Metis/metis.ML") - ("Tools/Sledgehammer/clausifier.ML") - ("Tools/Sledgehammer/meson_tactic.ML") + ("Tools/Sledgehammer/meson_clausifier.ML") ("Tools/Sledgehammer/metis_translate.ML") ("Tools/Sledgehammer/metis_reconstruct.ML") ("Tools/Sledgehammer/metis_tactics.ML") @@ -99,9 +98,8 @@ setup ATP_Systems.setup use "~~/src/Tools/Metis/metis.ML" -use "Tools/Sledgehammer/clausifier.ML" -use "Tools/Sledgehammer/meson_tactic.ML" -setup Meson_Tactic.setup +use "Tools/Sledgehammer/meson_clausifier.ML" +setup Meson_Clausifier.setup use "Tools/Sledgehammer/metis_translate.ML" use "Tools/Sledgehammer/metis_reconstruct.ML" diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 27 09:17:24 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,254 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/clausifier.ML - Author: Jia Meng, Cambridge University Computer Laboratory and NICTA - Author: Jasmin Blanchette, TU Muenchen - -Transformation of axiom rules (elim/intro/etc) into CNF forms. -*) - -signature CLAUSIFIER = -sig - val extensionalize_theorem : thm -> thm - val introduce_combinators_in_cterm : cterm -> thm - val introduce_combinators_in_theorem : thm -> thm - val to_definitional_cnf_with_quantifiers : theory -> thm -> thm - val cnf_axiom : theory -> thm -> thm list -end; - -structure Clausifier : CLAUSIFIER = -struct - -(**** Transformation of Elimination Rules into First-Order Formulas****) - -val cfalse = cterm_of @{theory HOL} HOLogic.false_const; -val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); - -(* Converts an elim-rule into an equivalent theorem that does not have the - predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_term" in - "Sledgehammer_Util".) *) -fun transform_elim_theorem th = - case concl_of th of (*conclusion variable*) - @{const Trueprop} $ (v as Var (_, @{typ bool})) => - Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th - | v as Var(_, @{typ prop}) => - Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th - | _ => th - - -(**** SKOLEMIZATION BY INFERENCE (lcp) ****) - -fun mk_skolem t = - let val T = fastype_of t in - Const (@{const_name skolem}, T --> T) $ t - end - -fun beta_eta_under_lambdas (Abs (s, T, t')) = - Abs (s, T, beta_eta_under_lambdas t') - | beta_eta_under_lambdas t = Envir.beta_eta_contract t - -(*Traverse a theorem, accumulating Skolem function definitions.*) -fun assume_skolem_funs th = - let - fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss = - (*Existential: declare a Skolem function, then insert into body and continue*) - let - val args = OldTerm.term_frees body - (* Forms a lambda-abstraction over the formal parameters *) - val rhs = - list_abs_free (map dest_Free args, - HOLogic.choice_const T $ beta_eta_under_lambdas body) - |> mk_skolem - val comb = list_comb (rhs, args) - in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end - | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = - (*Universal quant: insert a free variable into body and continue*) - let val fname = Name.variant (OldTerm.add_term_names (p,[])) a - in dec_sko (subst_bound (Free(fname,T), p)) rhss end - | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q - | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q - | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss - | dec_sko _ rhss = rhss - in dec_sko (prop_of th) [] end; - - -(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) - -val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} - -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) -fun extensionalize_theorem th = - case prop_of th of - _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _])) - $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all) - | _ => th - -fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true - | is_quasi_lambda_free (t1 $ t2) = - is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 - | is_quasi_lambda_free (Abs _) = false - | is_quasi_lambda_free _ = true - -val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); -val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); -val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); - -(* FIXME: Requires more use of cterm constructors. *) -fun abstract ct = - let - val thy = theory_of_cterm ct - val Abs(x,_,body) = term_of ct - val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) - val cxT = ctyp_of thy xT - val cbodyT = ctyp_of thy bodyT - fun makeK () = - instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] - @{thm abs_K} - in - case body of - Const _ => makeK() - | Free _ => makeK() - | Var _ => makeK() (*though Var isn't expected*) - | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) - | rator$rand => - if loose_bvar1 (rator,0) then (*C or S*) - if loose_bvar1 (rand,0) then (*S*) - let val crator = cterm_of thy (Abs(x,xT,rator)) - val crand = cterm_of thy (Abs(x,xT,rand)) - val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} - val (_,rhs) = Thm.dest_equals (cprop_of abs_S') - in - Thm.transitive abs_S' (Conv.binop_conv abstract rhs) - end - else (*C*) - let val crator = cterm_of thy (Abs(x,xT,rator)) - val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} - val (_,rhs) = Thm.dest_equals (cprop_of abs_C') - in - Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) - end - else if loose_bvar1 (rand,0) then (*B or eta*) - if rand = Bound 0 then Thm.eta_conversion ct - else (*B*) - let val crand = cterm_of thy (Abs(x,xT,rand)) - val crator = cterm_of thy rator - val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} - val (_,rhs) = Thm.dest_equals (cprop_of abs_B') - in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end - else makeK() - | _ => raise Fail "abstract: Bad term" - end; - -(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) -fun introduce_combinators_in_cterm ct = - if is_quasi_lambda_free (term_of ct) then - Thm.reflexive ct - else case term_of ct of - Abs _ => - let - val (cv, cta) = Thm.dest_abs NONE ct - val (v, _) = dest_Free (term_of cv) - val u_th = introduce_combinators_in_cterm cta - val cu = Thm.rhs_of u_th - val comb_eq = abstract (Thm.cabs cv cu) - in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end - | _ $ _ => - let val (ct1, ct2) = Thm.dest_comb ct in - Thm.combination (introduce_combinators_in_cterm ct1) - (introduce_combinators_in_cterm ct2) - end - -fun introduce_combinators_in_theorem th = - if is_quasi_lambda_free (prop_of th) then - th - else - let - val th = Drule.eta_contraction_rule th - val eqth = introduce_combinators_in_cterm (cprop_of th) - in Thm.equal_elim eqth th end - handle THM (msg, _, _) => - (warning ("Error in the combinator translation of " ^ - Display.string_of_thm_without_context th ^ - "\nException message: " ^ msg ^ "."); - (* A type variable of sort "{}" will make abstraction fail. *) - TrueI) - -(*cterms are used throughout for efficiency*) -val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop; - -(*Given an abstraction over n variables, replace the bound variables by free - ones. Return the body, along with the list of free variables.*) -fun c_variant_abs_multi (ct0, vars) = - let val (cv,ct) = Thm.dest_abs NONE ct0 - in c_variant_abs_multi (ct, cv::vars) end - handle CTERM _ => (ct0, rev vars); - -val skolem_def_raw = @{thms skolem_def_raw} - -(* Given the definition of a Skolem function, return a theorem to replace - an existential formula by a use of that function. - Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) -fun skolem_theorem_of_def thy rhs0 = - let - val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy - val rhs' = rhs |> Thm.dest_comb |> snd - val (ch, frees) = c_variant_abs_multi (rhs', []) - val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of - val T = - case hilbert of - Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T - | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert]) - val cex = cterm_of thy (HOLogic.exists_const T) - val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) - val conc = - Drule.list_comb (rhs, frees) - |> Drule.beta_conv cabs |> Thm.capply cTrueprop - fun tacf [prem] = - rewrite_goals_tac skolem_def_raw - THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1 - in - Goal.prove_internal [ex_tm] conc tacf - |> forall_intr_list frees - |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) - |> Thm.varifyT_global - end - -(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order) - into NNF. *) -fun to_nnf th ctxt0 = - let - val th1 = th |> transform_elim_theorem |> zero_var_indexes - val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 - val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize - |> extensionalize_theorem - |> Meson.make_nnf ctxt - in (th3, ctxt) end - -fun to_definitional_cnf_with_quantifiers thy th = - let - val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) - val eqth = eqth RS @{thm eq_reflection} - val eqth = eqth RS @{thm TruepropI} - in Thm.equal_elim eqth th end - -(* Convert a theorem to CNF, with Skolem functions as additional premises. *) -fun cnf_axiom thy th = - let - val ctxt0 = Variable.global_thm_context th - val (nnf_th, ctxt) = to_nnf th ctxt0 - fun aux th = - Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th)) - th ctxt - val (cnf_ths, ctxt) = - aux nnf_th - |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th) - | p => p) - in - cnf_ths |> map introduce_combinators_in_theorem - |> Variable.export ctxt ctxt0 - |> Meson.finish_cnf - |> map Thm.close_derivation - end - handle THM _ => [] - -end; diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Tools/Sledgehammer/meson_clausifier.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Mon Sep 27 10:44:08 2010 +0200 @@ -0,0 +1,267 @@ +(* Title: HOL/Tools/Sledgehammer/clausifier.ML + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen + +Transformation of axiom rules (elim/intro/etc) into CNF forms. +*) + +signature MESON_CLAUSIFIER = +sig + val extensionalize_theorem : thm -> thm + val introduce_combinators_in_cterm : cterm -> thm + val introduce_combinators_in_theorem : thm -> thm + val to_definitional_cnf_with_quantifiers : theory -> thm -> thm + val cnf_axiom : theory -> thm -> thm list + val meson_general_tac : Proof.context -> thm list -> int -> tactic + val setup: theory -> theory +end; + +structure Meson_Clausifier : MESON_CLAUSIFIER = +struct + +(**** Transformation of Elimination Rules into First-Order Formulas****) + +val cfalse = cterm_of @{theory HOL} HOLogic.false_const; +val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); + +(* Converts an elim-rule into an equivalent theorem that does not have the + predicate variable. Leaves other theorems unchanged. We simply instantiate + the conclusion variable to False. (Cf. "transform_elim_term" in + "Sledgehammer_Util".) *) +fun transform_elim_theorem th = + case concl_of th of (*conclusion variable*) + @{const Trueprop} $ (v as Var (_, @{typ bool})) => + Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th + | v as Var(_, @{typ prop}) => + Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th + | _ => th + + +(**** SKOLEMIZATION BY INFERENCE (lcp) ****) + +fun mk_skolem t = + let val T = fastype_of t in + Const (@{const_name skolem}, T --> T) $ t + end + +fun beta_eta_under_lambdas (Abs (s, T, t')) = + Abs (s, T, beta_eta_under_lambdas t') + | beta_eta_under_lambdas t = Envir.beta_eta_contract t + +(*Traverse a theorem, accumulating Skolem function definitions.*) +fun assume_skolem_funs th = + let + fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss = + (*Existential: declare a Skolem function, then insert into body and continue*) + let + val args = OldTerm.term_frees body + (* Forms a lambda-abstraction over the formal parameters *) + val rhs = + list_abs_free (map dest_Free args, + HOLogic.choice_const T $ beta_eta_under_lambdas body) + |> mk_skolem + val comb = list_comb (rhs, args) + in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end + | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = + (*Universal quant: insert a free variable into body and continue*) + let val fname = Name.variant (OldTerm.add_term_names (p,[])) a + in dec_sko (subst_bound (Free(fname,T), p)) rhss end + | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q + | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q + | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss + | dec_sko _ rhss = rhss + in dec_sko (prop_of th) [] end; + + +(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) + +val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} + +(* Removes the lambdas from an equation of the form "t = (%x. u)". + (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) +fun extensionalize_theorem th = + case prop_of th of + _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _])) + $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all) + | _ => th + +fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true + | is_quasi_lambda_free (t1 $ t2) = + is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 + | is_quasi_lambda_free (Abs _) = false + | is_quasi_lambda_free _ = true + +val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); +val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); +val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); + +(* FIXME: Requires more use of cterm constructors. *) +fun abstract ct = + let + val thy = theory_of_cterm ct + val Abs(x,_,body) = term_of ct + val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) + val cxT = ctyp_of thy xT + val cbodyT = ctyp_of thy bodyT + fun makeK () = + instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] + @{thm abs_K} + in + case body of + Const _ => makeK() + | Free _ => makeK() + | Var _ => makeK() (*though Var isn't expected*) + | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) + | rator$rand => + if loose_bvar1 (rator,0) then (*C or S*) + if loose_bvar1 (rand,0) then (*S*) + let val crator = cterm_of thy (Abs(x,xT,rator)) + val crand = cterm_of thy (Abs(x,xT,rand)) + val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} + val (_,rhs) = Thm.dest_equals (cprop_of abs_S') + in + Thm.transitive abs_S' (Conv.binop_conv abstract rhs) + end + else (*C*) + let val crator = cterm_of thy (Abs(x,xT,rator)) + val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} + val (_,rhs) = Thm.dest_equals (cprop_of abs_C') + in + Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) + end + else if loose_bvar1 (rand,0) then (*B or eta*) + if rand = Bound 0 then Thm.eta_conversion ct + else (*B*) + let val crand = cterm_of thy (Abs(x,xT,rand)) + val crator = cterm_of thy rator + val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} + val (_,rhs) = Thm.dest_equals (cprop_of abs_B') + in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end + else makeK() + | _ => raise Fail "abstract: Bad term" + end; + +(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) +fun introduce_combinators_in_cterm ct = + if is_quasi_lambda_free (term_of ct) then + Thm.reflexive ct + else case term_of ct of + Abs _ => + let + val (cv, cta) = Thm.dest_abs NONE ct + val (v, _) = dest_Free (term_of cv) + val u_th = introduce_combinators_in_cterm cta + val cu = Thm.rhs_of u_th + val comb_eq = abstract (Thm.cabs cv cu) + in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end + | _ $ _ => + let val (ct1, ct2) = Thm.dest_comb ct in + Thm.combination (introduce_combinators_in_cterm ct1) + (introduce_combinators_in_cterm ct2) + end + +fun introduce_combinators_in_theorem th = + if is_quasi_lambda_free (prop_of th) then + th + else + let + val th = Drule.eta_contraction_rule th + val eqth = introduce_combinators_in_cterm (cprop_of th) + in Thm.equal_elim eqth th end + handle THM (msg, _, _) => + (warning ("Error in the combinator translation of " ^ + Display.string_of_thm_without_context th ^ + "\nException message: " ^ msg ^ "."); + (* A type variable of sort "{}" will make abstraction fail. *) + TrueI) + +(*cterms are used throughout for efficiency*) +val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop; + +(*Given an abstraction over n variables, replace the bound variables by free + ones. Return the body, along with the list of free variables.*) +fun c_variant_abs_multi (ct0, vars) = + let val (cv,ct) = Thm.dest_abs NONE ct0 + in c_variant_abs_multi (ct, cv::vars) end + handle CTERM _ => (ct0, rev vars); + +val skolem_def_raw = @{thms skolem_def_raw} + +(* Given the definition of a Skolem function, return a theorem to replace + an existential formula by a use of that function. + Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) +fun skolem_theorem_of_def thy rhs0 = + let + val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy + val rhs' = rhs |> Thm.dest_comb |> snd + val (ch, frees) = c_variant_abs_multi (rhs', []) + val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of + val T = + case hilbert of + Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T + | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert]) + val cex = cterm_of thy (HOLogic.exists_const T) + val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) + val conc = + Drule.list_comb (rhs, frees) + |> Drule.beta_conv cabs |> Thm.capply cTrueprop + fun tacf [prem] = + rewrite_goals_tac skolem_def_raw + THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1 + in + Goal.prove_internal [ex_tm] conc tacf + |> forall_intr_list frees + |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) + |> Thm.varifyT_global + end + +(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order) + into NNF. *) +fun to_nnf th ctxt0 = + let + val th1 = th |> transform_elim_theorem |> zero_var_indexes + val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 + val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize + |> extensionalize_theorem + |> Meson.make_nnf ctxt + in (th3, ctxt) end + +fun to_definitional_cnf_with_quantifiers thy th = + let + val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) + val eqth = eqth RS @{thm eq_reflection} + val eqth = eqth RS @{thm TruepropI} + in Thm.equal_elim eqth th end + +(* Convert a theorem to CNF, with Skolem functions as additional premises. *) +fun cnf_axiom thy th = + let + val ctxt0 = Variable.global_thm_context th + val (nnf_th, ctxt) = to_nnf th ctxt0 + fun aux th = + Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th)) + th ctxt + val (cnf_ths, ctxt) = + aux nnf_th + |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th) + | p => p) + in + cnf_ths |> map introduce_combinators_in_theorem + |> Variable.export ctxt ctxt0 + |> Meson.finish_cnf + |> map Thm.close_derivation + end + handle THM _ => [] + +fun meson_general_tac ctxt ths = + let + val thy = ProofContext.theory_of ctxt + val ctxt0 = Classical.put_claset HOL_cs ctxt + in Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) end + +val setup = + Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) + "MESON resolution proof procedure"; + +end; diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Tools/Sledgehammer/meson_tactic.ML --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Sep 27 09:17:24 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML - Author: Jia Meng, Cambridge University Computer Laboratory and NICTA - Author: Jasmin Blanchette, TU Muenchen - -MESON general tactic and proof method. -*) - -signature MESON_TACTIC = -sig - val meson_general_tac : Proof.context -> thm list -> int -> tactic - val setup: theory -> theory -end; - -structure Meson_Tactic : MESON_TACTIC = -struct - -fun meson_general_tac ctxt ths = - let - val thy = ProofContext.theory_of ctxt - val ctxt0 = Classical.put_claset HOL_cs ctxt - in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end - -val setup = - Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) - "MESON resolution proof procedure"; - -end; diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 27 09:17:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 27 10:44:08 2010 +0200 @@ -56,7 +56,8 @@ let val thy = ProofContext.theory_of ctxt val type_lits = Config.get ctxt type_lits val th_cls_pairs = - map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0 + map (fn th => (Thm.get_name_hint th, + Meson_Clausifier.cnf_axiom thy th)) ths0 val ths = maps #2 th_cls_pairs val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls @@ -116,7 +117,7 @@ does, but also keep an unextensionalized version of "th" for backward compatibility. *) fun also_extensionalize_theorem th = - let val th' = Clausifier.extensionalize_theorem th in + let val th' = Meson_Clausifier.extensionalize_theorem th in if Thm.eq_thm (th, th') then [th] else th :: Meson.make_clauses_unsorted [th'] end @@ -125,7 +126,7 @@ single #> Meson.make_clauses_unsorted #> maps also_extensionalize_theorem - #> map Clausifier.introduce_combinators_in_theorem + #> map Meson_Clausifier.introduce_combinators_in_theorem #> Meson.finish_cnf fun preskolem_tac ctxt st0 = diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Tools/Sledgehammer/metis_translate.ML --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Mon Sep 27 09:17:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Mon Sep 27 10:44:08 2010 +0200 @@ -554,7 +554,8 @@ Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); (*The fully-typed translation, to avoid type errors*) -fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]); +fun wrap_type (tm, ty) = + Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty]) fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty) | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Sep 27 09:17:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Sep 27 10:44:08 2010 +0200 @@ -94,7 +94,7 @@ (0 upto length Ts - 1 ~~ Ts)) (* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_theorem" in "Clausifier".) *) + (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *) fun extensionalize_term t = let fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t' @@ -141,7 +141,7 @@ t |> conceal_bounds Ts |> Envir.eta_contract |> cterm_of thy - |> Clausifier.introduce_combinators_in_cterm + |> Meson_Clausifier.introduce_combinators_in_cterm |> prop_of |> Logic.dest_equals |> snd |> reveal_bounds Ts val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single diff -r b876d7525e72 -r 0b93a954da4f src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 27 09:17:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 27 10:44:08 2010 +0200 @@ -98,7 +98,7 @@ (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate the conclusion variable to False. (Cf. "transform_elim_theorem" in - "Clausifier".) *) + "Meson_Clausifier".) *) fun transform_elim_term t = case Logic.strip_imp_concl t of @{const Trueprop} $ Var (z, @{typ bool}) =>