# HG changeset patch # User blanchet # Date 1286269152 -7200 # Node ID f3c4849868b82b42d9c25597b9fc756dba7ef6ce # Parent 186a3b447e0bf0d6253a098406a3d07576321339 got rid of overkill "meson_choice" attribute; tuning diff -r 186a3b447e0b -r f3c4849868b8 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Tue Oct 05 10:30:50 2010 +0200 +++ b/src/HOL/Hilbert_Choice.thy Tue Oct 05 10:59:12 2010 +0200 @@ -80,7 +80,7 @@ subsection{*Axiom of Choice, Proved Using the Description Operator*} -lemma choice [meson_choice]: "\x. \y. Q x y ==> \f. \x. Q x (f x)" +lemma choice: "\x. \y. Q x y ==> \f. \x. Q x (f x)" by (fast elim: someI) lemma bchoice: "\x\S. \y. Q x y ==> \f. \x\S. Q x (f x)" diff -r 186a3b447e0b -r f3c4849868b8 src/HOL/Meson.thy --- a/src/HOL/Meson.thy Tue Oct 05 10:30:50 2010 +0200 +++ b/src/HOL/Meson.thy Tue Oct 05 10:59:12 2010 +0200 @@ -188,21 +188,12 @@ section {* Meson package *} -ML {* -structure Meson_Choices = Named_Thms -( - val name = "meson_choice" - val description = "choice axioms for MESON's (and Metis's) skolemizer" -) -*} - use "Tools/Meson/meson.ML" use "Tools/Meson/meson_clausify.ML" use "Tools/Meson/meson_tactic.ML" setup {* - Meson_Choices.setup - #> Meson.setup + Meson.setup #> Meson_Tactic.setup *} diff -r 186a3b447e0b -r f3c4849868b8 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Tue Oct 05 10:30:50 2010 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Tue Oct 05 10:59:12 2010 +0200 @@ -16,7 +16,8 @@ val finish_cnf: thm list -> thm list val presimplify: thm -> thm val make_nnf: Proof.context -> thm -> thm - val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm + val choice_theorems : theory -> thm list + val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm val skolemize : Proof.context -> thm -> thm val is_fol_term: theory -> term -> bool val make_clauses_unsorted: thm list -> thm list @@ -554,9 +555,12 @@ [] => th |> presimplify |> make_nnf1 ctxt | _ => raise THM ("make_nnf: premises in argument", 0, [th]); +fun choice_theorems thy = + try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list + (* Pull existential quantifiers to front. This accomplishes Skolemization for clauses that arise from a subgoal. *) -fun skolemize_with_choice_thms ctxt choice_ths = +fun skolemize_with_choice_theorems ctxt choice_ths = let fun aux th = if not (has_conns [@{const_name Ex}] (prop_of th)) then @@ -574,7 +578,10 @@ |> forward_res ctxt aux in aux o make_nnf ctxt end -fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt) +fun skolemize ctxt = + let val thy = ProofContext.theory_of ctxt in + skolemize_with_choice_theorems ctxt (choice_theorems thy) + end (* "RS" can fail if "unify_search_bound" is too small. *) fun try_skolemize ctxt th = diff -r 186a3b447e0b -r f3c4849868b8 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Oct 05 10:30:50 2010 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Oct 05 10:59:12 2010 +0200 @@ -20,6 +20,8 @@ structure Meson_Clausify : MESON_CLAUSIFY = struct +open Meson + (* the extra "?" helps prevent clashes *) val new_skolem_var_prefix = "?SK" val new_nonskolem_var_prefix = "?V" @@ -293,12 +295,12 @@ 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 + |> make_nnf ctxt in if new_skolemizer then let fun skolemize choice_ths = - Meson.skolemize_with_choice_thms ctxt choice_ths + skolemize_with_choice_theorems ctxt choice_ths #> simplify (ss_only @{thms all_simps[symmetric]}) val pull_out = simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) @@ -331,21 +333,21 @@ fun cnf_axiom ctxt0 new_skolemizer ax_no th = let val thy = ProofContext.theory_of ctxt0 - val choice_ths = Meson_Choices.get ctxt0 + val choice_ths = choice_theorems thy val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 fun clausify th = - Meson.make_cnf (if new_skolemizer then - [] - else - map (old_skolem_theorem_from_def thy) - (old_skolem_defs th)) th ctxt + make_cnf (if new_skolemizer orelse null choice_ths then + [] + else + map (old_skolem_theorem_from_def thy) + (old_skolem_defs th)) th ctxt val (cnf_ths, ctxt) = clausify nnf_th |> (fn ([], _) => clausify (to_definitional_cnf_with_quantifiers thy nnf_th) | p => p) fun intr_imp ct th = - Thm.instantiate ([], map (pairself (cterm_of @{theory})) + Thm.instantiate ([], map (pairself (cterm_of thy)) [(Var (("i", 1), @{typ nat}), HOLogic.mk_nat ax_no)]) @{thm skolem_COMBK_D} @@ -357,7 +359,7 @@ cnf_ths |> map (introduce_combinators_in_theorem #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) |> Variable.export ctxt ctxt0 - |> Meson.finish_cnf + |> finish_cnf |> map Thm.close_derivation) end handle THM _ => (NONE, []) diff -r 186a3b447e0b -r f3c4849868b8 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 05 10:30:50 2010 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 05 10:59:12 2010 +0200 @@ -313,7 +313,7 @@ let val thy = ProofContext.theory_of ctxt val type_lits = Config.get ctxt type_lits val new_skolemizer = - Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt) + Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) val th_cls_pairs = map2 (fn j => fn th => (Thm.get_name_hint th,