--- 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]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
+lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
by (fast elim: someI)
lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
--- 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
*}
--- 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 =
--- 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, [])
--- 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,