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'

     2.1 --- a/src/HOL/Tools/meson.ML	Thu Jul 29 16:11:02 2010 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Thu Jul 29 16:41:32 2010 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4    val too_many_clauses: Proof.context option -> term -> bool
     2.5    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     2.6    val finish_cnf: thm list -> thm list
     2.7 +  val presimplify: thm -> thm
     2.8    val make_nnf: Proof.context -> thm -> thm
     2.9    val skolemize: Proof.context -> thm -> thm
    2.10    val is_fol_term: theory -> term -> bool
    2.11 @@ -529,9 +530,12 @@
    2.12    HOL_basic_ss addsimps nnf_extra_simps
    2.13      addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
    2.14  
    2.15 +val presimplify =
    2.16 +  rewrite_rule (map safe_mk_meta_eq nnf_simps)
    2.17 +  #> simplify nnf_ss
    2.18 +
    2.19  fun make_nnf ctxt th = case prems_of th of
    2.20 -    [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
    2.21 -             |> simplify nnf_ss
    2.22 +    [] => th |> presimplify
    2.23               |> make_nnf1 ctxt
    2.24    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    2.25