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)