src/HOL/Tools/Meson/meson.ML
changeset 46071 1613933e412c
parent 45981 4c629115e3ab
child 46093 4bf24b90703c
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Jan 02 11:54:21 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Jan 02 14:12:20 2012 +0100
     1.3 @@ -9,7 +9,6 @@
     1.4  signature MESON =
     1.5  sig
     1.6    val trace : bool Config.T
     1.7 -  val unfold_set_consts : bool Config.T
     1.8    val max_clauses : int Config.T
     1.9    val term_pair_of: indexname * (typ * 'a) -> term * 'a
    1.10    val first_order_resolve : thm -> thm -> thm
    1.11 @@ -19,7 +18,6 @@
    1.12      thm list -> thm -> Proof.context
    1.13      -> Proof.context -> thm list * Proof.context
    1.14    val finish_cnf: thm list -> thm list
    1.15 -  val unfold_set_const_simps : Proof.context -> thm list
    1.16    val presimplified_consts : Proof.context -> string list
    1.17    val presimplify: Proof.context -> thm -> thm
    1.18    val make_nnf: Proof.context -> thm -> thm
    1.19 @@ -57,9 +55,6 @@
    1.20  
    1.21  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.22  
    1.23 -val unfold_set_consts =
    1.24 -  Attrib.setup_config_bool @{binding meson_unfold_set_consts} (K false)
    1.25 -
    1.26  val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K 60)
    1.27  
    1.28  (*No known example (on 1-5-2007) needs even thirty*)
    1.29 @@ -568,10 +563,6 @@
    1.30      handle THM ("tryres", _, _) => th
    1.31    else th
    1.32  
    1.33 -fun unfold_set_const_simps ctxt =
    1.34 -  if Config.get ctxt unfold_set_consts then []
    1.35 -  else []
    1.36 -
    1.37  (*The simplification removes defined quantifiers and occurrences of True and False.
    1.38    nnf_ss also includes the one-point simprocs,
    1.39    which are needed to avoid the various one-point theorems from generating junk clauses.*)
    1.40 @@ -591,16 +582,11 @@
    1.41    [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    1.42     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    1.43     @{const_name Let}]
    1.44 -  |> Config.get ctxt unfold_set_consts
    1.45 -     ? append ([@{const_name Collect}, @{const_name Set.member}])
    1.46  
    1.47  fun presimplify ctxt =
    1.48    rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.49    #> simplify nnf_ss
    1.50 -  (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
    1.51 -     when "metis_unfold_set_consts" becomes the only mode of operation. *)
    1.52 -  #> Raw_Simplifier.rewrite_rule
    1.53 -         (@{thm Let_def_raw} :: unfold_set_const_simps ctxt)
    1.54 +  #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
    1.55  
    1.56  fun make_nnf ctxt th = case prems_of th of
    1.57      [] => th |> presimplify ctxt |> make_nnf1 ctxt
    1.58 @@ -649,18 +635,17 @@
    1.59  val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
    1.60  
    1.61  (* "RS" can fail if "unify_search_bound" is too small. *)
    1.62 -fun try_skolemize_etc ctxt =
    1.63 -  Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
    1.64 +fun try_skolemize_etc ctxt th =
    1.65    (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    1.66       does, but also keep an unextensionalized version of "th" for backward
    1.67       compatibility. *)
    1.68 -  #> (fn th => insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) [th])
    1.69 -  #> map_filter (fn th => try (skolemize ctxt) th
    1.70 -                          |> tap (fn NONE =>
    1.71 -                                     trace_msg ctxt (fn () =>
    1.72 -                                         "Failed to skolemize " ^
    1.73 -                                          Display.string_of_thm ctxt th)
    1.74 -                                   | _ => ()))
    1.75 +  [th] |> insert Thm.eq_thm_prop (extensionalize_theorem ctxt th)
    1.76 +       |> map_filter (fn th => th |> try (skolemize ctxt)
    1.77 +                                  |> tap (fn NONE =>
    1.78 +                                             trace_msg ctxt (fn () =>
    1.79 +                                                 "Failed to skolemize " ^
    1.80 +                                                  Display.string_of_thm ctxt th)
    1.81 +                                           | _ => ()))
    1.82  
    1.83  fun add_clauses ctxt th cls =
    1.84    let val ctxt0 = Variable.global_thm_context th