# HG changeset patch
# User blanchet
# Date 1280414492 -7200
# Node ID ed65a0777e10b18ad61a8f26ebb24abcea3f799b
# Parent  a9847fb539dd430d68bad4881b9aa932b8f5ecfc
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs

diff -r a9847fb539dd -r ed65a0777e10 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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'
diff -r a9847fb539dd -r ed65a0777e10 src/HOL/Tools/meson.ML
--- 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]);