killed unfold_set_const option that makes no sense now that set is a type constructor again
authorblanchet
Mon Jan 02 14:12:20 2012 +0100 (2012-01-02)
changeset 460711613933e412c
parent 46070 8392c28d7868
child 46072 291c14a01b6d
killed unfold_set_const option that makes no sense now that set is a type constructor again
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jan 02 11:54:21 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jan 02 14:12:20 2012 +0100
     1.3 @@ -1205,7 +1205,6 @@
     1.4       val need_trueprop = (fastype_of t = @{typ bool})
     1.5     in
     1.6       t |> need_trueprop ? HOLogic.mk_Trueprop
     1.7 -       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
     1.8         |> extensionalize_term ctxt
     1.9         |> presimplify_term ctxt presimp_consts
    1.10         |> HOLogic.dest_Trueprop
     2.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Jan 02 11:54:21 2012 +0100
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Jan 02 14:12:20 2012 +0100
     2.3 @@ -9,7 +9,6 @@
     2.4  signature MESON =
     2.5  sig
     2.6    val trace : bool Config.T
     2.7 -  val unfold_set_consts : bool Config.T
     2.8    val max_clauses : int Config.T
     2.9    val term_pair_of: indexname * (typ * 'a) -> term * 'a
    2.10    val first_order_resolve : thm -> thm -> thm
    2.11 @@ -19,7 +18,6 @@
    2.12      thm list -> thm -> Proof.context
    2.13      -> Proof.context -> thm list * Proof.context
    2.14    val finish_cnf: thm list -> thm list
    2.15 -  val unfold_set_const_simps : Proof.context -> thm list
    2.16    val presimplified_consts : Proof.context -> string list
    2.17    val presimplify: Proof.context -> thm -> thm
    2.18    val make_nnf: Proof.context -> thm -> thm
    2.19 @@ -57,9 +55,6 @@
    2.20  
    2.21  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    2.22  
    2.23 -val unfold_set_consts =
    2.24 -  Attrib.setup_config_bool @{binding meson_unfold_set_consts} (K false)
    2.25 -
    2.26  val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K 60)
    2.27  
    2.28  (*No known example (on 1-5-2007) needs even thirty*)
    2.29 @@ -568,10 +563,6 @@
    2.30      handle THM ("tryres", _, _) => th
    2.31    else th
    2.32  
    2.33 -fun unfold_set_const_simps ctxt =
    2.34 -  if Config.get ctxt unfold_set_consts then []
    2.35 -  else []
    2.36 -
    2.37  (*The simplification removes defined quantifiers and occurrences of True and False.
    2.38    nnf_ss also includes the one-point simprocs,
    2.39    which are needed to avoid the various one-point theorems from generating junk clauses.*)
    2.40 @@ -591,16 +582,11 @@
    2.41    [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    2.42     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    2.43     @{const_name Let}]
    2.44 -  |> Config.get ctxt unfold_set_consts
    2.45 -     ? append ([@{const_name Collect}, @{const_name Set.member}])
    2.46  
    2.47  fun presimplify ctxt =
    2.48    rewrite_rule (map safe_mk_meta_eq nnf_simps)
    2.49    #> simplify nnf_ss
    2.50 -  (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
    2.51 -     when "metis_unfold_set_consts" becomes the only mode of operation. *)
    2.52 -  #> Raw_Simplifier.rewrite_rule
    2.53 -         (@{thm Let_def_raw} :: unfold_set_const_simps ctxt)
    2.54 +  #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
    2.55  
    2.56  fun make_nnf ctxt th = case prems_of th of
    2.57      [] => th |> presimplify ctxt |> make_nnf1 ctxt
    2.58 @@ -649,18 +635,17 @@
    2.59  val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
    2.60  
    2.61  (* "RS" can fail if "unify_search_bound" is too small. *)
    2.62 -fun try_skolemize_etc ctxt =
    2.63 -  Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
    2.64 +fun try_skolemize_etc ctxt th =
    2.65    (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    2.66       does, but also keep an unextensionalized version of "th" for backward
    2.67       compatibility. *)
    2.68 -  #> (fn th => insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) [th])
    2.69 -  #> map_filter (fn th => try (skolemize ctxt) th
    2.70 -                          |> tap (fn NONE =>
    2.71 -                                     trace_msg ctxt (fn () =>
    2.72 -                                         "Failed to skolemize " ^
    2.73 -                                          Display.string_of_thm ctxt th)
    2.74 -                                   | _ => ()))
    2.75 +  [th] |> insert Thm.eq_thm_prop (extensionalize_theorem ctxt th)
    2.76 +       |> map_filter (fn th => th |> try (skolemize ctxt)
    2.77 +                                  |> tap (fn NONE =>
    2.78 +                                             trace_msg ctxt (fn () =>
    2.79 +                                                 "Failed to skolemize " ^
    2.80 +                                                  Display.string_of_thm ctxt th)
    2.81 +                                           | _ => ()))
    2.82  
    2.83  fun add_clauses ctxt th cls =
    2.84    let val ctxt0 = Variable.global_thm_context th
     3.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jan 02 11:54:21 2012 +0100
     3.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jan 02 14:12:20 2012 +0100
     3.3 @@ -311,7 +311,6 @@
     3.4           |> new_skolemizer ? forall_intr_vars
     3.5      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     3.6      val th = th |> Conv.fconv_rule Object_Logic.atomize
     3.7 -                |> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
     3.8                  |> extensionalize_theorem ctxt
     3.9                  |> make_nnf ctxt
    3.10    in