# HG changeset patch # User blanchet # Date 1285795599 -7200 # Node ID 21d556f109443ad9b0e74e1a8afeecaf13c3813b # Parent 40ef95149770e9dd91de05d0c5faa61842bf98a3 rename file diff -r 40ef95149770 -r 21d556f10944 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Sep 29 23:24:31 2010 +0200 +++ b/src/HOL/IsaMakefile Wed Sep 29 23:26:39 2010 +0200 @@ -315,7 +315,7 @@ Tools/recdef.ML \ Tools/record.ML \ Tools/semiring_normalizer.ML \ - Tools/Sledgehammer/meson_clausifier.ML \ + Tools/Sledgehammer/meson_clausify.ML \ Tools/Sledgehammer/metis_reconstruct.ML \ Tools/Sledgehammer/metis_translate.ML \ Tools/Sledgehammer/metis_tactics.ML \ diff -r 40ef95149770 -r 21d556f10944 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Sep 29 23:24:31 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Sep 29 23:26:39 2010 +0200 @@ -14,7 +14,7 @@ ("Tools/ATP/atp_proof.ML") ("Tools/ATP/atp_systems.ML") ("~~/src/Tools/Metis/metis.ML") - ("Tools/Sledgehammer/meson_clausifier.ML") + ("Tools/Sledgehammer/meson_clausify.ML") ("Tools/Sledgehammer/metis_translate.ML") ("Tools/Sledgehammer/metis_reconstruct.ML") ("Tools/Sledgehammer/metis_tactics.ML") @@ -98,7 +98,7 @@ setup ATP_Systems.setup use "~~/src/Tools/Metis/metis.ML" -use "Tools/Sledgehammer/meson_clausifier.ML" +use "Tools/Sledgehammer/meson_clausify.ML" setup Meson_Clausifier.setup use "Tools/Sledgehammer/metis_translate.ML" diff -r 40ef95149770 -r 21d556f10944 src/HOL/Tools/Sledgehammer/meson_clausifier.ML --- a/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Wed Sep 29 23:24:31 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,349 +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 MESON_CLAUSIFIER = -sig - val new_skolemizer : bool Config.T - val new_skolem_var_prefix : string - 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 option * thm list - val meson_general_tac : Proof.context -> thm list -> int -> tactic - val setup: theory -> theory -end; - -structure Meson_Clausifier : MESON_CLAUSIFIER = -struct - -val (new_skolemizer, new_skolemizer_setup) = - Attrib.config_bool "meson_new_skolemizer" (K false) - -val new_skolem_var_prefix = "SK?" (* purposedly won't parse *) - -(**** 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_old_skolem_term_wrapper 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 old_skolem_defs 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_old_skolem_term_wrapper - 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 old_skolem_theorem_from_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 ("old_skolem_theorem_from_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 - -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 - -val kill_quantifiers = - let - fun conv pos ct = - ct |> (case term_of ct of - Const (s, _) $ Abs (s', _, _) => - if s = @{const_name all} orelse s = @{const_name All} orelse - s = @{const_name Ex} then - Thm.dest_comb #> snd - #> Thm.dest_abs (SOME (s' |> pos = (s = @{const_name Ex}) - ? prefix new_skolem_var_prefix)) - #> snd #> conv pos - else - Conv.all_conv - | Const (s, _) $ _ $ _ => - if s = @{const_name "==>"} orelse - s = @{const_name HOL.implies} then - Conv.combination_conv (Conv.arg_conv (conv (not pos))) - (conv pos) - else if s = @{const_name HOL.conj} orelse - s = @{const_name HOL.disj} then - Conv.combination_conv (Conv.arg_conv (conv pos)) (conv pos) - else - Conv.all_conv - | Const (s, _) $ _ => - if s = @{const_name Trueprop} then - Conv.arg_conv (conv pos) - else if s = @{const_name Not} then - Conv.arg_conv (conv (not pos)) - else - Conv.all_conv - | _ => Conv.all_conv) - in - conv true #> Drule.export_without_context - #> cprop_of #> Thm.dest_equals #> snd - end - -val pull_out_quant_ss = - MetaSimplifier.clear_ss HOL_basic_ss - addsimps @{thms all_simps[symmetric]} - -(* Converts an Isabelle theorem into NNF. *) -fun nnf_axiom new_skolemizer th ctxt = - let - val thy = ProofContext.theory_of ctxt - val th = - th |> transform_elim_theorem - |> zero_var_indexes - |> new_skolemizer ? forall_intr_vars - val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single - val th = th |> Conv.fconv_rule Object_Logic.atomize - |> extensionalize_theorem - |> Meson.make_nnf ctxt - in - if new_skolemizer then - let - val th' = th |> Meson.skolemize ctxt - |> simplify pull_out_quant_ss - |> Drule.eta_contraction_rule - val t = th' |> cprop_of |> kill_quantifiers |> term_of - in - if exists_subterm (fn Var ((s, _), _) => - String.isPrefix new_skolem_var_prefix s - | _ => false) t then - let - val (ct, ctxt) = - Variable.import_terms true [t] ctxt - |>> the_single |>> cterm_of thy - in (SOME (th', ct), ct |> Thm.assume, ctxt) end - else - (NONE, th, ctxt) - end - else - (NONE, th, ctxt) - end - -(* Convert a theorem to CNF, with additional premises due to skolemization. *) -fun cnf_axiom thy th = - let - val ctxt0 = Variable.global_thm_context th - val new_skolemizer = Config.get ctxt0 new_skolemizer - val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0 - fun aux th = - Meson.make_cnf (if new_skolemizer then - [] - else - map (old_skolem_theorem_from_def thy) - (old_skolem_defs th)) th ctxt - val (cnf_ths, ctxt) = - aux nnf_th - |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th) - | p => p) - val export = Variable.export ctxt ctxt0 - in - (opt |> Option.map (singleton export o fst), - cnf_ths |> map (introduce_combinators_in_theorem - #> (case opt of - SOME (_, ct) => Thm.implies_intr ct - | NONE => I)) - |> export - |> Meson.finish_cnf - |> map Thm.close_derivation) - end - handle THM _ => (NONE, []) - -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 (snd o cnf_axiom thy) ths) end - -val setup = - new_skolemizer_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 40ef95149770 -r 21d556f10944 src/HOL/Tools/Sledgehammer/meson_clausify.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Wed Sep 29 23:26:39 2010 +0200 @@ -0,0 +1,349 @@ +(* 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 new_skolemizer : bool Config.T + val new_skolem_var_prefix : string + 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 option * thm list + val meson_general_tac : Proof.context -> thm list -> int -> tactic + val setup: theory -> theory +end; + +structure Meson_Clausifier : MESON_CLAUSIFIER = +struct + +val (new_skolemizer, new_skolemizer_setup) = + Attrib.config_bool "meson_new_skolemizer" (K false) + +val new_skolem_var_prefix = "SK?" (* purposedly won't parse *) + +(**** 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_old_skolem_term_wrapper 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 old_skolem_defs 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_old_skolem_term_wrapper + 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 old_skolem_theorem_from_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 ("old_skolem_theorem_from_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 + +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 + +val kill_quantifiers = + let + fun conv pos ct = + ct |> (case term_of ct of + Const (s, _) $ Abs (s', _, _) => + if s = @{const_name all} orelse s = @{const_name All} orelse + s = @{const_name Ex} then + Thm.dest_comb #> snd + #> Thm.dest_abs (SOME (s' |> pos = (s = @{const_name Ex}) + ? prefix new_skolem_var_prefix)) + #> snd #> conv pos + else + Conv.all_conv + | Const (s, _) $ _ $ _ => + if s = @{const_name "==>"} orelse + s = @{const_name HOL.implies} then + Conv.combination_conv (Conv.arg_conv (conv (not pos))) + (conv pos) + else if s = @{const_name HOL.conj} orelse + s = @{const_name HOL.disj} then + Conv.combination_conv (Conv.arg_conv (conv pos)) (conv pos) + else + Conv.all_conv + | Const (s, _) $ _ => + if s = @{const_name Trueprop} then + Conv.arg_conv (conv pos) + else if s = @{const_name Not} then + Conv.arg_conv (conv (not pos)) + else + Conv.all_conv + | _ => Conv.all_conv) + in + conv true #> Drule.export_without_context + #> cprop_of #> Thm.dest_equals #> snd + end + +val pull_out_quant_ss = + MetaSimplifier.clear_ss HOL_basic_ss + addsimps @{thms all_simps[symmetric]} + +(* Converts an Isabelle theorem into NNF. *) +fun nnf_axiom new_skolemizer th ctxt = + let + val thy = ProofContext.theory_of ctxt + val th = + th |> transform_elim_theorem + |> zero_var_indexes + |> new_skolemizer ? forall_intr_vars + val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single + val th = th |> Conv.fconv_rule Object_Logic.atomize + |> extensionalize_theorem + |> Meson.make_nnf ctxt + in + if new_skolemizer then + let + val th' = th |> Meson.skolemize ctxt + |> simplify pull_out_quant_ss + |> Drule.eta_contraction_rule + val t = th' |> cprop_of |> kill_quantifiers |> term_of + in + if exists_subterm (fn Var ((s, _), _) => + String.isPrefix new_skolem_var_prefix s + | _ => false) t then + let + val (ct, ctxt) = + Variable.import_terms true [t] ctxt + |>> the_single |>> cterm_of thy + in (SOME (th', ct), ct |> Thm.assume, ctxt) end + else + (NONE, th, ctxt) + end + else + (NONE, th, ctxt) + end + +(* Convert a theorem to CNF, with additional premises due to skolemization. *) +fun cnf_axiom thy th = + let + val ctxt0 = Variable.global_thm_context th + val new_skolemizer = Config.get ctxt0 new_skolemizer + val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0 + fun aux th = + Meson.make_cnf (if new_skolemizer then + [] + else + map (old_skolem_theorem_from_def thy) + (old_skolem_defs th)) th ctxt + val (cnf_ths, ctxt) = + aux nnf_th + |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th) + | p => p) + val export = Variable.export ctxt ctxt0 + in + (opt |> Option.map (singleton export o fst), + cnf_ths |> map (introduce_combinators_in_theorem + #> (case opt of + SOME (_, ct) => Thm.implies_intr ct + | NONE => I)) + |> export + |> Meson.finish_cnf + |> map Thm.close_derivation) + end + handle THM _ => (NONE, []) + +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 (snd o cnf_axiom thy) ths) end + +val setup = + new_skolemizer_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;