# HG changeset patch
# User blanchet
# Date 1307515663 -7200
# Node ID a1a48c69d623227b484c82ca6d168819b5cff49f
# Parent  ab9addf5165ad3fd037ec76cdfcf3602f7cbdf85
don't needlessly presimplify -- makes ATP problem preparation much faster

diff -r ab9addf5165a -r a1a48c69d623 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -870,10 +870,12 @@
       | _ => do_term bs t
   in do_formula [] end
 
-fun presimplify_term ctxt =
-  Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-  #> Meson.presimplify ctxt
-  #> prop_of
+fun presimplify_term _ [] t = t
+  | presimplify_term ctxt presimp_consts t =
+    t |> exists_Const (member (op =) presimp_consts o fst) t
+         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+            #> Meson.presimplify ctxt
+            #> prop_of)
 
 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
 fun conceal_bounds Ts t =
@@ -940,7 +942,7 @@
       | aux t = t
   in t |> exists_subterm is_Var t ? aux end
 
-fun preprocess_prop ctxt presimp kind t =
+fun preprocess_prop ctxt presimp_consts kind t =
   let
     val thy = Proof_Context.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
@@ -951,7 +953,7 @@
     t |> need_trueprop ? HOLogic.mk_Trueprop
       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
       |> extensionalize_term ctxt
-      |> presimp ? presimplify_term ctxt
+      |> presimplify_term ctxt presimp_consts
       |> perhaps (try (HOLogic.dest_Trueprop))
       |> introduce_combinators_in_term ctxt kind
   end
@@ -966,11 +968,11 @@
      atomic_types = atomic_types}
   end
 
-fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp
+fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts
               ((name, loc), t) =
   let val thy = Proof_Context.theory_of ctxt in
     case (keep_trivial,
-          t |> preproc ? preprocess_prop ctxt presimp Axiom
+          t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
             |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
       (false,
        formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
@@ -978,7 +980,7 @@
     | (_, formula) => SOME formula
   end
 
-fun make_conjecture ctxt format prem_kind type_sys preproc ts =
+fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
   let
     val thy = Proof_Context.theory_of ctxt
     val last = length ts - 1
@@ -993,7 +995,8 @@
                     if prem_kind = Conjecture then update_combformula mk_anot
                     else I)
               in
-                t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
+                t |> preproc ?
+                     (preprocess_prop ctxt presimp_consts kind #> freeze_term)
                   |> make_formula thy format type_sys (format <> CNF)
                                   (string_of_int j) General kind
                   |> maybe_negate
@@ -1344,7 +1347,7 @@
                    | _ => I)
          end)
       val make_facts =
-        map_filter (make_fact ctxt format type_sys false false false false)
+        map_filter (make_fact ctxt format type_sys false false false [])
       val fairly_sound = is_type_sys_fairly_sound type_sys
     in
       helper_table
@@ -1406,11 +1409,11 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val fact_ts = facts |> map snd
+    val presimp_consts = Meson.presimplified_consts ctxt
+    val make_fact =
+      make_fact ctxt format type_sys false true true presimp_consts
     val (facts, fact_names) =
-      facts |> map (fn (name, t) =>
-                        (name, t)
-                        |> make_fact ctxt format type_sys false true true true
-                        |> rpair name)
+      facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
             |> map_filter (try (apfst the))
             |> ListPair.unzip
     (* Remove existing facts from the conjecture, as this can dramatically
@@ -1425,7 +1428,7 @@
     val tycons = type_constrs_of_terms thy all_ts
     val conjs =
       hyp_ts @ [concl_t]
-      |> make_conjecture ctxt format prem_kind type_sys preproc
+      |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
     val (supers', arity_clauses) =
       if level_of_type_sys type_sys = No_Types then ([], [])
       else make_arity_clauses thy tycons supers
diff -r ab9addf5165a -r a1a48c69d623 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -17,6 +17,7 @@
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
   val unfold_set_const_simps : Proof.context -> thm list
+  val presimplified_consts : Proof.context -> string list
   val presimplify: Proof.context -> thm -> thm
   val make_nnf: Proof.context -> thm -> thm
   val choice_theorems : theory -> thm list
@@ -576,7 +577,15 @@
 
 val nnf_ss =
   HOL_basic_ss addsimps nnf_extra_simps
-    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
+    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
+                 @{simproc let_simp}]
+
+fun presimplified_consts ctxt =
+  [@{const_name simp_implies}, @{const_name False}, @{const_name True},
+   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
+   @{const_name Let}]
+  |> Config.get ctxt unfold_set_consts
+     ? append ([@{const_name Collect}, @{const_name Set.member}])
 
 fun presimplify ctxt =
   rewrite_rule (map safe_mk_meta_eq nnf_simps)