got rid of overkill "meson_choice" attribute;
authorblanchet
Tue Oct 05 10:59:12 2010 +0200 (2010-10-05)
changeset 39950f3c4849868b8
parent 39949 186a3b447e0b
child 39951 ff60a6e4edfe
got rid of overkill "meson_choice" attribute;
tuning
src/HOL/Hilbert_Choice.thy
src/HOL/Meson.thy
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactics.ML
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Oct 05 10:30:50 2010 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 05 10:59:12 2010 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  
     1.5  subsection{*Axiom of Choice, Proved Using the Description Operator*}
     1.6  
     1.7 -lemma choice [meson_choice]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
     1.8 +lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
     1.9  by (fast elim: someI)
    1.10  
    1.11  lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
     2.1 --- a/src/HOL/Meson.thy	Tue Oct 05 10:30:50 2010 +0200
     2.2 +++ b/src/HOL/Meson.thy	Tue Oct 05 10:59:12 2010 +0200
     2.3 @@ -188,21 +188,12 @@
     2.4  
     2.5  section {* Meson package *}
     2.6  
     2.7 -ML {*
     2.8 -structure Meson_Choices = Named_Thms
     2.9 -(
    2.10 -  val name = "meson_choice"
    2.11 -  val description = "choice axioms for MESON's (and Metis's) skolemizer"
    2.12 -)
    2.13 -*}
    2.14 -
    2.15  use "Tools/Meson/meson.ML"
    2.16  use "Tools/Meson/meson_clausify.ML"
    2.17  use "Tools/Meson/meson_tactic.ML"
    2.18  
    2.19  setup {*
    2.20 -  Meson_Choices.setup
    2.21 -  #> Meson.setup
    2.22 +  Meson.setup
    2.23    #> Meson_Tactic.setup
    2.24  *}
    2.25  
     3.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 10:30:50 2010 +0200
     3.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 10:59:12 2010 +0200
     3.3 @@ -16,7 +16,8 @@
     3.4    val finish_cnf: thm list -> thm list
     3.5    val presimplify: thm -> thm
     3.6    val make_nnf: Proof.context -> thm -> thm
     3.7 -  val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm
     3.8 +  val choice_theorems : theory -> thm list
     3.9 +  val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
    3.10    val skolemize : Proof.context -> thm -> thm
    3.11    val is_fol_term: theory -> term -> bool
    3.12    val make_clauses_unsorted: thm list -> thm list
    3.13 @@ -554,9 +555,12 @@
    3.14      [] => th |> presimplify |> make_nnf1 ctxt
    3.15    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    3.16  
    3.17 +fun choice_theorems thy =
    3.18 +  try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list
    3.19 +
    3.20  (* Pull existential quantifiers to front. This accomplishes Skolemization for
    3.21     clauses that arise from a subgoal. *)
    3.22 -fun skolemize_with_choice_thms ctxt choice_ths =
    3.23 +fun skolemize_with_choice_theorems ctxt choice_ths =
    3.24    let
    3.25      fun aux th =
    3.26        if not (has_conns [@{const_name Ex}] (prop_of th)) then
    3.27 @@ -574,7 +578,10 @@
    3.28                        |> forward_res ctxt aux
    3.29    in aux o make_nnf ctxt end
    3.30  
    3.31 -fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt)
    3.32 +fun skolemize ctxt =
    3.33 +  let val thy = ProofContext.theory_of ctxt in
    3.34 +    skolemize_with_choice_theorems ctxt (choice_theorems thy)
    3.35 +  end
    3.36  
    3.37  (* "RS" can fail if "unify_search_bound" is too small. *)
    3.38  fun try_skolemize ctxt th =
     4.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:30:50 2010 +0200
     4.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:59:12 2010 +0200
     4.3 @@ -20,6 +20,8 @@
     4.4  structure Meson_Clausify : MESON_CLAUSIFY =
     4.5  struct
     4.6  
     4.7 +open Meson
     4.8 +
     4.9  (* the extra "?" helps prevent clashes *)
    4.10  val new_skolem_var_prefix = "?SK"
    4.11  val new_nonskolem_var_prefix = "?V"
    4.12 @@ -293,12 +295,12 @@
    4.13      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
    4.14      val th = th |> Conv.fconv_rule Object_Logic.atomize
    4.15                  |> extensionalize_theorem
    4.16 -                |> Meson.make_nnf ctxt
    4.17 +                |> make_nnf ctxt
    4.18    in
    4.19      if new_skolemizer then
    4.20        let
    4.21          fun skolemize choice_ths =
    4.22 -          Meson.skolemize_with_choice_thms ctxt choice_ths
    4.23 +          skolemize_with_choice_theorems ctxt choice_ths
    4.24            #> simplify (ss_only @{thms all_simps[symmetric]})
    4.25          val pull_out =
    4.26            simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
    4.27 @@ -331,21 +333,21 @@
    4.28  fun cnf_axiom ctxt0 new_skolemizer ax_no th =
    4.29    let
    4.30      val thy = ProofContext.theory_of ctxt0
    4.31 -    val choice_ths = Meson_Choices.get ctxt0
    4.32 +    val choice_ths = choice_theorems thy
    4.33      val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    4.34      fun clausify th =
    4.35 -      Meson.make_cnf (if new_skolemizer then
    4.36 -                        []
    4.37 -                      else
    4.38 -                        map (old_skolem_theorem_from_def thy)
    4.39 -                            (old_skolem_defs th)) th ctxt
    4.40 +      make_cnf (if new_skolemizer orelse null choice_ths then
    4.41 +                  []
    4.42 +                else
    4.43 +                  map (old_skolem_theorem_from_def thy)
    4.44 +                      (old_skolem_defs th)) th ctxt
    4.45      val (cnf_ths, ctxt) =
    4.46        clausify nnf_th
    4.47        |> (fn ([], _) =>
    4.48               clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
    4.49             | p => p)
    4.50      fun intr_imp ct th =
    4.51 -      Thm.instantiate ([], map (pairself (cterm_of @{theory}))
    4.52 +      Thm.instantiate ([], map (pairself (cterm_of thy))
    4.53                                 [(Var (("i", 1), @{typ nat}),
    4.54                                   HOLogic.mk_nat ax_no)])
    4.55                        @{thm skolem_COMBK_D}
    4.56 @@ -357,7 +359,7 @@
    4.57       cnf_ths |> map (introduce_combinators_in_theorem
    4.58                       #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
    4.59               |> Variable.export ctxt ctxt0
    4.60 -             |> Meson.finish_cnf
    4.61 +             |> finish_cnf
    4.62               |> map Thm.close_derivation)
    4.63    end
    4.64    handle THM _ => (NONE, [])
     5.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 10:30:50 2010 +0200
     5.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 10:59:12 2010 +0200
     5.3 @@ -313,7 +313,7 @@
     5.4    let val thy = ProofContext.theory_of ctxt
     5.5        val type_lits = Config.get ctxt type_lits
     5.6        val new_skolemizer =
     5.7 -        Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt)
     5.8 +        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
     5.9        val th_cls_pairs =
    5.10          map2 (fn j => fn th =>
    5.11                  (Thm.get_name_hint th,