src/HOL/Tools/Meson/meson_clausify.ML
changeset 39950 f3c4849868b8
parent 39949 186a3b447e0b
child 39962 d42ddd7407ca
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:30:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:59:12 2010 +0200
     1.3 @@ -20,6 +20,8 @@
     1.4  structure Meson_Clausify : MESON_CLAUSIFY =
     1.5  struct
     1.6  
     1.7 +open Meson
     1.8 +
     1.9  (* the extra "?" helps prevent clashes *)
    1.10  val new_skolem_var_prefix = "?SK"
    1.11  val new_nonskolem_var_prefix = "?V"
    1.12 @@ -293,12 +295,12 @@
    1.13      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
    1.14      val th = th |> Conv.fconv_rule Object_Logic.atomize
    1.15                  |> extensionalize_theorem
    1.16 -                |> Meson.make_nnf ctxt
    1.17 +                |> make_nnf ctxt
    1.18    in
    1.19      if new_skolemizer then
    1.20        let
    1.21          fun skolemize choice_ths =
    1.22 -          Meson.skolemize_with_choice_thms ctxt choice_ths
    1.23 +          skolemize_with_choice_theorems ctxt choice_ths
    1.24            #> simplify (ss_only @{thms all_simps[symmetric]})
    1.25          val pull_out =
    1.26            simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
    1.27 @@ -331,21 +333,21 @@
    1.28  fun cnf_axiom ctxt0 new_skolemizer ax_no th =
    1.29    let
    1.30      val thy = ProofContext.theory_of ctxt0
    1.31 -    val choice_ths = Meson_Choices.get ctxt0
    1.32 +    val choice_ths = choice_theorems thy
    1.33      val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    1.34      fun clausify th =
    1.35 -      Meson.make_cnf (if new_skolemizer then
    1.36 -                        []
    1.37 -                      else
    1.38 -                        map (old_skolem_theorem_from_def thy)
    1.39 -                            (old_skolem_defs th)) th ctxt
    1.40 +      make_cnf (if new_skolemizer orelse null choice_ths then
    1.41 +                  []
    1.42 +                else
    1.43 +                  map (old_skolem_theorem_from_def thy)
    1.44 +                      (old_skolem_defs th)) th ctxt
    1.45      val (cnf_ths, ctxt) =
    1.46        clausify nnf_th
    1.47        |> (fn ([], _) =>
    1.48               clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
    1.49             | p => p)
    1.50      fun intr_imp ct th =
    1.51 -      Thm.instantiate ([], map (pairself (cterm_of @{theory}))
    1.52 +      Thm.instantiate ([], map (pairself (cterm_of thy))
    1.53                                 [(Var (("i", 1), @{typ nat}),
    1.54                                   HOLogic.mk_nat ax_no)])
    1.55                        @{thm skolem_COMBK_D}
    1.56 @@ -357,7 +359,7 @@
    1.57       cnf_ths |> map (introduce_combinators_in_theorem
    1.58                       #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
    1.59               |> Variable.export ctxt ctxt0
    1.60 -             |> Meson.finish_cnf
    1.61 +             |> finish_cnf
    1.62               |> map Thm.close_derivation)
    1.63    end
    1.64    handle THM _ => (NONE, [])