properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
authorblanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 4234753e444ecb525
parent 42346 be52d9bed9f6
child 42348 187354e22c7d
properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
src/HOL/Tools/Meson/meson_clausify.ML
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -329,11 +329,17 @@
     1.4          fun skolemize choice_ths =
     1.5            skolemize_with_choice_theorems ctxt choice_ths
     1.6            #> simplify (ss_only @{thms all_simps[symmetric]})
     1.7 +        val no_choice = null choice_ths
     1.8          val pull_out =
     1.9 -          simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
    1.10 -        val no_choice = null choice_ths
    1.11 +          if no_choice then
    1.12 +            simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
    1.13 +          else
    1.14 +            skolemize choice_ths
    1.15 +        val discharger_th = th |> pull_out
    1.16          val discharger_th =
    1.17 -          th |> (if no_choice then pull_out else skolemize choice_ths)
    1.18 +          discharger_th |> has_too_many_clauses ctxt (concl_of discharger_th)
    1.19 +                           ? (to_definitional_cnf_with_quantifiers ctxt
    1.20 +                              #> pull_out)
    1.21          val zapped_th =
    1.22            discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
    1.23            |> (if no_choice then
    1.24 @@ -364,61 +370,10 @@
    1.25           (NONE, (th, ctxt))
    1.26        end
    1.27      else
    1.28 -      (NONE, (th, ctxt))
    1.29 +      (NONE, (th |> has_too_many_clauses ctxt (concl_of th)
    1.30 +                    ? to_definitional_cnf_with_quantifiers ctxt, ctxt))
    1.31    end
    1.32  
    1.33 -val all_out_ss =
    1.34 -  Simplifier.clear_ss HOL_basic_ss addsimps @{thms all_simps[symmetric]}
    1.35 -
    1.36 -val meta_allI = @{lemma "ALL x. P x ==> (!!x. P x)" by auto}
    1.37 -
    1.38 -fun repeat f x =
    1.39 -  case try f x of
    1.40 -    SOME y => repeat f y
    1.41 -  | NONE => x
    1.42 -
    1.43 -fun close_thm thy th =
    1.44 -  fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of th) []) th
    1.45 -
    1.46 -fun cnf_axiom_xxx ctxt0 new_skolemizer ax_no th =
    1.47 -  let
    1.48 -    val ctxt0 = Variable.global_thm_context th
    1.49 -    val thy = ProofContext.theory_of ctxt0
    1.50 -    val choice_ths = choice_theorems thy
    1.51 -    val (opt, (nnf_th, ctxt)) =
    1.52 -      nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    1.53 -    val skolem_ths = map (old_skolem_theorem_from_def thy) o old_skolem_defs
    1.54 -    fun make_cnf th = Meson.make_cnf (skolem_ths th) th
    1.55 -    val (cnf_ths, ctxt) =
    1.56 -       make_cnf nnf_th ctxt
    1.57 -       |> (fn (cnf, _) =>
    1.58 -              let
    1.59 -                val _ = tracing ("nondef CNF: " ^ string_of_int (length cnf) ^ " clause(s)")
    1.60 -                val sko_th =
    1.61 -                  nnf_th |> Simplifier.simplify all_out_ss
    1.62 -                         |> repeat (fn th => th RS meta_allI)
    1.63 -                         |> Meson.make_xxx_skolem ctxt (skolem_ths nnf_th)
    1.64 -                         |> close_thm thy
    1.65 -                         |> Conv.fconv_rule Object_Logic.atomize
    1.66 -                         |> to_definitional_cnf_with_quantifiers ctxt
    1.67 -              in make_cnf sko_th ctxt end
    1.68 -           | p => p)
    1.69 -    fun intr_imp ct th =
    1.70 -      Thm.instantiate ([], map (pairself (cterm_of thy))
    1.71 -                               [(Var (("i", 0), @{typ nat}),
    1.72 -                                 HOLogic.mk_nat ax_no)])
    1.73 -                      (zero_var_indexes @{thm skolem_COMBK_D})
    1.74 -      RS Thm.implies_intr ct th
    1.75 -  in
    1.76 -    (NONE (*###*),
    1.77 -     cnf_ths |> map (introduce_combinators_in_theorem
    1.78 -                     #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
    1.79 -             |> Variable.export ctxt ctxt0
    1.80 -             |> finish_cnf
    1.81 -             |> map Thm.close_derivation)
    1.82 -  end
    1.83 -
    1.84 -
    1.85  (* Convert a theorem to CNF, with additional premises due to skolemization. *)
    1.86  fun cnf_axiom ctxt0 new_skolemizer ax_no th =
    1.87    let
    1.88 @@ -427,32 +382,10 @@
    1.89      val (opt, (nnf_th, ctxt)) =
    1.90        nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    1.91      fun clausify th =
    1.92 -      make_cnf (if new_skolemizer orelse null choice_ths then
    1.93 -                  []
    1.94 -                else
    1.95 -                  map (old_skolem_theorem_from_def thy)
    1.96 -                      (old_skolem_defs th)) th ctxt
    1.97 -    val (cnf_ths, ctxt) =
    1.98 -      clausify nnf_th
    1.99 -      |> (fn ([], _) =>
   1.100 -             if new_skolemizer then
   1.101 -               let
   1.102 -val _ = tracing ("**** NEW CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th)) (*###*)
   1.103 -val _ = tracing (" *** th: " ^ Display.string_of_thm ctxt th) (*###*)
   1.104 -                 val (_, (th1, ctxt)) = nnf_axiom choice_ths true ax_no th ctxt0
   1.105 -val _ = tracing (" *** th1: " ^ Display.string_of_thm ctxt th1) (*###*)
   1.106 -                 val th2 = to_definitional_cnf_with_quantifiers ctxt th1
   1.107 -val _ = tracing (" *** th2: " ^ Display.string_of_thm ctxt th2) (*###*)
   1.108 -                 val (ths3, ctxt) = clausify th2
   1.109 -val _ = tracing (" *** hd ths3: " ^ Display.string_of_thm ctxt (hd ths3)) (*###*)
   1.110 -               in (ths3, ctxt) end
   1.111 -             else
   1.112 -let
   1.113 -val _ = tracing ("**** OLD CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th))
   1.114 -(*###*) in
   1.115 -               clausify (to_definitional_cnf_with_quantifiers ctxt nnf_th)
   1.116 -end
   1.117 -           | p => p)
   1.118 +      make_cnf (if new_skolemizer orelse null choice_ths then []
   1.119 +                else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
   1.120 +               th ctxt
   1.121 +    val (cnf_ths, ctxt) = clausify nnf_th
   1.122      fun intr_imp ct th =
   1.123        Thm.instantiate ([], map (pairself (cterm_of thy))
   1.124                                 [(Var (("i", 0), @{typ nat}),