tuning
authorblanchet
Tue Jan 03 18:33:18 2012 +0100 (2012-01-03)
changeset 460934bf24b90703c
parent 46092 287a3cefc21b
child 46094 4d9a5f1514b4
tuning
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -1093,12 +1093,11 @@
     1.4        | _ => do_term bs t
     1.5    in do_formula [] end
     1.6  
     1.7 -fun presimplify_term _ [] t = t
     1.8 -  | presimplify_term ctxt presimp_consts t =
     1.9 -    t |> exists_Const (member (op =) presimp_consts o fst) t
    1.10 -         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    1.11 -            #> Meson.presimplify ctxt
    1.12 -            #> prop_of)
    1.13 +fun presimplify_term ctxt t =
    1.14 +  t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
    1.15 +       ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    1.16 +          #> Meson.presimplify
    1.17 +          #> prop_of)
    1.18  
    1.19  fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
    1.20  fun conceal_bounds Ts t =
    1.21 @@ -1196,7 +1195,7 @@
    1.22        | freeze t = t
    1.23    in t |> exists_subterm is_Var t ? freeze end
    1.24  
    1.25 -fun presimp_prop ctxt presimp_consts role t =
    1.26 +fun presimp_prop ctxt role t =
    1.27    (let
    1.28       val thy = Proof_Context.theory_of ctxt
    1.29       val t = t |> Envir.beta_eta_contract
    1.30 @@ -1206,7 +1205,7 @@
    1.31     in
    1.32       t |> need_trueprop ? HOLogic.mk_Trueprop
    1.33         |> extensionalize_term ctxt
    1.34 -       |> presimplify_term ctxt presimp_consts
    1.35 +       |> presimplify_term ctxt
    1.36         |> HOLogic.dest_Trueprop
    1.37     end
    1.38     handle TERM _ => if role = Conjecture then @{term False} else @{term True})
    1.39 @@ -1708,7 +1707,6 @@
    1.40    let
    1.41      val thy = Proof_Context.theory_of ctxt
    1.42      val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
    1.43 -    val presimp_consts = Meson.presimplified_consts ctxt
    1.44      val fact_ts = facts |> map snd
    1.45      (* Remove existing facts from the conjecture, as this can dramatically
    1.46         boost an ATP's performance (for some reason). *)
    1.47 @@ -1722,8 +1720,7 @@
    1.48        |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
    1.49      val ((conjs, facts), lam_facts) =
    1.50        (conjs, facts)
    1.51 -      |> presimp
    1.52 -         ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
    1.53 +      |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
    1.54        |> (if lam_trans = no_lamsN then
    1.55              rpair []
    1.56            else
     2.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
     2.3 @@ -18,8 +18,8 @@
     2.4      thm list -> thm -> Proof.context
     2.5      -> Proof.context -> thm list * Proof.context
     2.6    val finish_cnf: thm list -> thm list
     2.7 -  val presimplified_consts : Proof.context -> string list
     2.8 -  val presimplify: Proof.context -> thm -> thm
     2.9 +  val presimplified_consts : string list
    2.10 +  val presimplify: thm -> thm
    2.11    val make_nnf: Proof.context -> thm -> thm
    2.12    val choice_theorems : theory -> thm list
    2.13    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
    2.14 @@ -578,18 +578,18 @@
    2.15      addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
    2.16                   @{simproc let_simp}]
    2.17  
    2.18 -fun presimplified_consts ctxt =
    2.19 +val presimplified_consts =
    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  
    2.24 -fun presimplify ctxt =
    2.25 +val presimplify =
    2.26    rewrite_rule (map safe_mk_meta_eq nnf_simps)
    2.27    #> simplify nnf_ss
    2.28    #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
    2.29  
    2.30  fun make_nnf ctxt th = case prems_of th of
    2.31 -    [] => th |> presimplify ctxt |> make_nnf1 ctxt
    2.32 +    [] => th |> presimplify |> make_nnf1 ctxt
    2.33    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    2.34  
    2.35  fun choice_theorems thy =