1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 16:11:02 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 16:41:32 2010 +0200
1.3 @@ -231,6 +231,13 @@
1.4 | aux _ t = t
1.5 in aux (maxidx_of_term t + 1) t end
1.6
1.7 +fun presimplify_term thy =
1.8 + HOLogic.mk_Trueprop
1.9 + #> Skip_Proof.make_thm thy
1.10 + #> Meson.presimplify
1.11 + #> prop_of
1.12 + #> HOLogic.dest_Trueprop
1.13 +
1.14 (* FIXME: Guarantee freshness *)
1.15 fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
1.16 fun conceal_bounds Ts t =
1.17 @@ -278,14 +285,13 @@
1.18 | Conjecture => HOLogic.false_const
1.19
1.20 (* making axiom and conjecture formulas *)
1.21 -fun make_formula ctxt (formula_name, kind, t) =
1.22 +fun make_formula ctxt presimp (formula_name, kind, t) =
1.23 let
1.24 val thy = ProofContext.theory_of ctxt
1.25 - (* ### FIXME: perform other transformations previously done by
1.26 - "Clausifier.to_nnf", e.g. "HOL.If" *)
1.27 val t = t |> transform_elim_term
1.28 |> Object_Logic.atomize_term thy
1.29 |> extensionalize_term
1.30 + |> presimp ? presimplify_term thy
1.31 |> introduce_combinators_in_term ctxt kind
1.32 val (combformula, ctypes_sorts) = combformula_for_prop thy t []
1.33 in
1.34 @@ -293,10 +299,10 @@
1.35 kind = kind, ctypes_sorts = ctypes_sorts}
1.36 end
1.37
1.38 -fun make_axiom ctxt (name, th) =
1.39 - (name, make_formula ctxt (name, Axiom, prop_of th))
1.40 +fun make_axiom ctxt presimp (name, th) =
1.41 + (name, make_formula ctxt presimp (name, Axiom, prop_of th))
1.42 fun make_conjectures ctxt ts =
1.43 - map2 (fn j => fn t => make_formula ctxt (Int.toString j, Conjecture, t))
1.44 + map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
1.45 (0 upto length ts - 1) ts
1.46
1.47 (** Helper facts **)
1.48 @@ -335,7 +341,7 @@
1.49 if exists is_needed ss then map (`Thm.get_name_hint) ths
1.50 else [])) @
1.51 (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
1.52 - |> map (snd o make_axiom ctxt)
1.53 + |> map (snd o make_axiom ctxt false)
1.54 end
1.55
1.56 fun meta_not t = @{const "==>"} $ t $ @{prop False}
1.57 @@ -351,7 +357,7 @@
1.58 val tycons = type_consts_of_terms thy (goal_t :: axtms)
1.59 (* TFrees in the conjecture; TVars in the axioms *)
1.60 val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
1.61 - val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls)
1.62 + val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls)
1.63 val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
1.64 val (supers', arity_clauses) = make_arity_clauses thy tycons supers
1.65 val class_rel_clauses = make_class_rel_clauses thy subs supers'