perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 16:11:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 16:41:32 2010 +0200
@@ -231,6 +231,13 @@
| aux _ t = t
in aux (maxidx_of_term t + 1) t end
+fun presimplify_term thy =
+ HOLogic.mk_Trueprop
+ #> Skip_Proof.make_thm thy
+ #> Meson.presimplify
+ #> prop_of
+ #> HOLogic.dest_Trueprop
+
(* FIXME: Guarantee freshness *)
fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
fun conceal_bounds Ts t =
@@ -278,14 +285,13 @@
| Conjecture => HOLogic.false_const
(* making axiom and conjecture formulas *)
-fun make_formula ctxt (formula_name, kind, t) =
+fun make_formula ctxt presimp (formula_name, kind, t) =
let
val thy = ProofContext.theory_of ctxt
- (* ### FIXME: perform other transformations previously done by
- "Clausifier.to_nnf", e.g. "HOL.If" *)
val t = t |> transform_elim_term
|> Object_Logic.atomize_term thy
|> extensionalize_term
+ |> presimp ? presimplify_term thy
|> introduce_combinators_in_term ctxt kind
val (combformula, ctypes_sorts) = combformula_for_prop thy t []
in
@@ -293,10 +299,10 @@
kind = kind, ctypes_sorts = ctypes_sorts}
end
-fun make_axiom ctxt (name, th) =
- (name, make_formula ctxt (name, Axiom, prop_of th))
+fun make_axiom ctxt presimp (name, th) =
+ (name, make_formula ctxt presimp (name, Axiom, prop_of th))
fun make_conjectures ctxt ts =
- map2 (fn j => fn t => make_formula ctxt (Int.toString j, Conjecture, t))
+ map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
(0 upto length ts - 1) ts
(** Helper facts **)
@@ -335,7 +341,7 @@
if exists is_needed ss then map (`Thm.get_name_hint) ths
else [])) @
(if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
- |> map (snd o make_axiom ctxt)
+ |> map (snd o make_axiom ctxt false)
end
fun meta_not t = @{const "==>"} $ t $ @{prop False}
@@ -351,7 +357,7 @@
val tycons = type_consts_of_terms thy (goal_t :: axtms)
(* TFrees in the conjecture; TVars in the axioms *)
val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
- val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls)
+ val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls)
val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
--- a/src/HOL/Tools/meson.ML Thu Jul 29 16:11:02 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jul 29 16:41:32 2010 +0200
@@ -14,6 +14,7 @@
val too_many_clauses: Proof.context option -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
val finish_cnf: thm list -> thm list
+ val presimplify: thm -> thm
val make_nnf: Proof.context -> thm -> thm
val skolemize: Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
@@ -529,9 +530,12 @@
HOL_basic_ss addsimps nnf_extra_simps
addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
+val presimplify =
+ rewrite_rule (map safe_mk_meta_eq nnf_simps)
+ #> simplify nnf_ss
+
fun make_nnf ctxt th = case prems_of th of
- [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
- |> simplify nnf_ss
+ [] => th |> presimplify
|> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]);