don't needlessly presimplify -- makes ATP problem preparation much faster
authorblanchet
Wed Jun 08 08:47:43 2011 +0200 (2011-06-08)
changeset 43264a1a48c69d623
parent 43263 ab9addf5165a
child 43265 096237fe70f1
don't needlessly presimplify -- makes ATP problem preparation much faster
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -870,10 +870,12 @@
     1.4        | _ => do_term bs t
     1.5    in do_formula [] end
     1.6  
     1.7 -fun presimplify_term ctxt =
     1.8 -  Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
     1.9 -  #> Meson.presimplify ctxt
    1.10 -  #> prop_of
    1.11 +fun presimplify_term _ [] t = t
    1.12 +  | presimplify_term ctxt presimp_consts t =
    1.13 +    t |> exists_Const (member (op =) presimp_consts o fst) t
    1.14 +         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    1.15 +            #> Meson.presimplify ctxt
    1.16 +            #> prop_of)
    1.17  
    1.18  fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
    1.19  fun conceal_bounds Ts t =
    1.20 @@ -940,7 +942,7 @@
    1.21        | aux t = t
    1.22    in t |> exists_subterm is_Var t ? aux end
    1.23  
    1.24 -fun preprocess_prop ctxt presimp kind t =
    1.25 +fun preprocess_prop ctxt presimp_consts kind t =
    1.26    let
    1.27      val thy = Proof_Context.theory_of ctxt
    1.28      val t = t |> Envir.beta_eta_contract
    1.29 @@ -951,7 +953,7 @@
    1.30      t |> need_trueprop ? HOLogic.mk_Trueprop
    1.31        |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
    1.32        |> extensionalize_term ctxt
    1.33 -      |> presimp ? presimplify_term ctxt
    1.34 +      |> presimplify_term ctxt presimp_consts
    1.35        |> perhaps (try (HOLogic.dest_Trueprop))
    1.36        |> introduce_combinators_in_term ctxt kind
    1.37    end
    1.38 @@ -966,11 +968,11 @@
    1.39       atomic_types = atomic_types}
    1.40    end
    1.41  
    1.42 -fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp
    1.43 +fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts
    1.44                ((name, loc), t) =
    1.45    let val thy = Proof_Context.theory_of ctxt in
    1.46      case (keep_trivial,
    1.47 -          t |> preproc ? preprocess_prop ctxt presimp Axiom
    1.48 +          t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
    1.49              |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
    1.50        (false,
    1.51         formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
    1.52 @@ -978,7 +980,7 @@
    1.53      | (_, formula) => SOME formula
    1.54    end
    1.55  
    1.56 -fun make_conjecture ctxt format prem_kind type_sys preproc ts =
    1.57 +fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
    1.58    let
    1.59      val thy = Proof_Context.theory_of ctxt
    1.60      val last = length ts - 1
    1.61 @@ -993,7 +995,8 @@
    1.62                      if prem_kind = Conjecture then update_combformula mk_anot
    1.63                      else I)
    1.64                in
    1.65 -                t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
    1.66 +                t |> preproc ?
    1.67 +                     (preprocess_prop ctxt presimp_consts kind #> freeze_term)
    1.68                    |> make_formula thy format type_sys (format <> CNF)
    1.69                                    (string_of_int j) General kind
    1.70                    |> maybe_negate
    1.71 @@ -1344,7 +1347,7 @@
    1.72                     | _ => I)
    1.73           end)
    1.74        val make_facts =
    1.75 -        map_filter (make_fact ctxt format type_sys false false false false)
    1.76 +        map_filter (make_fact ctxt format type_sys false false false [])
    1.77        val fairly_sound = is_type_sys_fairly_sound type_sys
    1.78      in
    1.79        helper_table
    1.80 @@ -1406,11 +1409,11 @@
    1.81    let
    1.82      val thy = Proof_Context.theory_of ctxt
    1.83      val fact_ts = facts |> map snd
    1.84 +    val presimp_consts = Meson.presimplified_consts ctxt
    1.85 +    val make_fact =
    1.86 +      make_fact ctxt format type_sys false true true presimp_consts
    1.87      val (facts, fact_names) =
    1.88 -      facts |> map (fn (name, t) =>
    1.89 -                        (name, t)
    1.90 -                        |> make_fact ctxt format type_sys false true true true
    1.91 -                        |> rpair name)
    1.92 +      facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
    1.93              |> map_filter (try (apfst the))
    1.94              |> ListPair.unzip
    1.95      (* Remove existing facts from the conjecture, as this can dramatically
    1.96 @@ -1425,7 +1428,7 @@
    1.97      val tycons = type_constrs_of_terms thy all_ts
    1.98      val conjs =
    1.99        hyp_ts @ [concl_t]
   1.100 -      |> make_conjecture ctxt format prem_kind type_sys preproc
   1.101 +      |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
   1.102      val (supers', arity_clauses) =
   1.103        if level_of_type_sys type_sys = No_Types then ([], [])
   1.104        else make_arity_clauses thy tycons supers
     2.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Jun 08 08:47:43 2011 +0200
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Jun 08 08:47:43 2011 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     2.5    val finish_cnf: thm list -> thm list
     2.6    val unfold_set_const_simps : Proof.context -> thm list
     2.7 +  val presimplified_consts : Proof.context -> string list
     2.8    val presimplify: Proof.context -> thm -> thm
     2.9    val make_nnf: Proof.context -> thm -> thm
    2.10    val choice_theorems : theory -> thm list
    2.11 @@ -576,7 +577,15 @@
    2.12  
    2.13  val nnf_ss =
    2.14    HOL_basic_ss addsimps nnf_extra_simps
    2.15 -    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
    2.16 +    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
    2.17 +                 @{simproc let_simp}]
    2.18 +
    2.19 +fun presimplified_consts ctxt =
    2.20 +  [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    2.21 +   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    2.22 +   @{const_name Let}]
    2.23 +  |> Config.get ctxt unfold_set_consts
    2.24 +     ? append ([@{const_name Collect}, @{const_name Set.member}])
    2.25  
    2.26  fun presimplify ctxt =
    2.27    rewrite_rule (map safe_mk_meta_eq nnf_simps)