encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed

--- a/src/HOL/Sledgehammer.thy	Thu Aug 19 14:39:31 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Aug 19 18:16:47 2010 +0200
@@ -31,28 +31,31 @@
 [no_atp]: "skolem_id = (\<lambda>x. x)"
 
 definition COMBI :: "'a \<Rightarrow> 'a" where
-[no_atp]: "COMBI P \<equiv> P"
+[no_atp]: "COMBI P = P"
 
 definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
-[no_atp]: "COMBK P Q \<equiv> P"
+[no_atp]: "COMBK P Q = P"
 
 definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
-"COMBB P Q R \<equiv> P (Q R)"
+"COMBB P Q R = P (Q R)"
 
 definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBC P Q R \<equiv> P R Q"
+[no_atp]: "COMBC P Q R = P R Q"
 
 definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
+[no_atp]: "COMBS P Q R = P R (Q R)"
 
 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
-"fequal X Y \<equiv> (X = Y)"
+"fequal X Y \<longleftrightarrow> (X = Y)"
+
+lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
+by (simp add: fequal_def)
 
-lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
-  by (simp add: fequal_def)
+lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
+by (simp add: fequal_def)
 
-lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
-  by (simp add: fequal_def)
+lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
+by auto
 
 text{*Theorems for translation to combinators*}
 

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 14:39:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 18:16:47 2010 +0200
@@ -66,8 +66,10 @@
 (* HOL to FOL  (Isabelle to Metis)                                           *)
 (* ------------------------------------------------------------------------- *)
 
-fun fn_isa_to_met "equal" = "="
-  | fn_isa_to_met x       = x;
+fun fn_isa_to_met_sublevel "equal" = "c_fequal"
+  | fn_isa_to_met_sublevel x = x
+fun fn_isa_to_met_toplevel "equal" = "="
+  | fn_isa_to_met_toplevel x = x
 
 fun metis_lit b c args = (b, (c, args));
 
@@ -89,7 +91,7 @@
     | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
 
 fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
-      Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
+      Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
   | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
@@ -99,7 +101,7 @@
 
 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
   | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
-      wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
+      wrap_type (Metis.Term.Fn(fn_isa_to_met_sublevel a, []), ty)
   | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
                   combtyp_of tm)
@@ -108,7 +110,7 @@
       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
           val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
           val lits = map hol_term_to_fol_FO tms
-      in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
+      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
   | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
      (case strip_combterm_comb tm of
           (CombConst(("equal", _), _, _), tms) =>
@@ -224,13 +226,16 @@
 
 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
 
+fun smart_invert_const "fequal" = @{const_name "op ="}
+  | smart_invert_const s = invert_const s
+
 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
      (case strip_prefix_and_undo_ascii tvar_prefix v of
           SOME w => make_tvar w
         | NONE   => make_tvar v)
   | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
      (case strip_prefix_and_undo_ascii type_const_prefix x of
-          SOME tc => Term.Type (invert_const tc,
+          SOME tc => Term.Type (smart_invert_const tc,
                                 map (hol_type_from_metis_term ctxt) tys)
         | NONE    =>
       case strip_prefix_and_undo_ascii tfree_prefix x of
@@ -265,7 +270,7 @@
         | applic_to_tt (a,ts) =
             case strip_prefix_and_undo_ascii const_prefix a of
                 SOME b =>
-                  let val c = invert_const b
+                  let val c = smart_invert_const b
                       val ntypes = num_type_args thy c
                       val nterms = length ts - ntypes
                       val tts = map tm_to_tt ts
@@ -283,7 +288,7 @@
               | NONE => (*Not a constant. Is it a type constructor?*)
             case strip_prefix_and_undo_ascii type_const_prefix a of
                 SOME b =>
-                  Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
+                  Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
             case strip_prefix_and_undo_ascii tfree_prefix a of
                 SOME b => Type (mk_tfree ctxt b)
@@ -311,7 +316,7 @@
             Const ("op =", HOLogic.typeT)
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
            (case strip_prefix_and_undo_ascii const_prefix x of
-                SOME c => Const (invert_const c, dummyT)
+                SOME c => Const (smart_invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_undo_ascii fixed_var_prefix x of
                 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
@@ -325,7 +330,7 @@
             list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
         | cvt (t as Metis.Term.Fn (x, [])) =
            (case strip_prefix_and_undo_ascii const_prefix x of
-                SOME c => Const (invert_const c, dummyT)
+                SOME c => Const (smart_invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_undo_ascii fixed_var_prefix x of
                 SOME v => Free (v, dummyT)
@@ -598,9 +603,6 @@
 (* Translation of HO Clauses                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-fun cnf_helper_theorem thy raw th =
-  if raw then th else the_single (Clausifier.cnf_axiom thy th)
-
 fun type_ext thy tms =
   let val subs = tfree_classes_of_terms tms
       val supers = tvar_classes_of_terms tms
@@ -650,15 +652,16 @@
   | string_of_mode FT = "FT"
 
 val helpers =
-  [("c_COMBI", (false, @{thms COMBI_def})),
-   ("c_COMBK", (false, @{thms COMBK_def})),
-   ("c_COMBB", (false, @{thms COMBB_def})),
-   ("c_COMBC", (false, @{thms COMBC_def})),
-   ("c_COMBS", (false, @{thms COMBS_def})),
-   ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
-   ("c_True", (true, @{thms True_or_False})),
-   ("c_False", (true, @{thms True_or_False})),
-   ("c_If", (true, @{thms if_True if_False True_or_False}))]
+  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
+   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
+   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
+   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
+   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
+   ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
+                            @{thms fequal_imp_equal equal_imp_fequal})),
+   ("c_True", (true, map (`I) @{thms True_or_False})),
+   ("c_False", (true, map (`I) @{thms True_or_False})),
+   ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
 
 fun is_quasi_fol_clause thy =
   Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
@@ -673,18 +676,20 @@
         | set_mode FT = FT
       val mode = set_mode mode0
       (*transform isabelle clause to metis clause *)
-      fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map =
+      fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
+                  : logic_map =
         let
           val (mth, tfree_lits, skolems) =
-            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith
+            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems
+                           metis_ith
         in
-           {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
+           {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
             tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
         end;
       val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
-                 |> fold (add_thm true) cls
+                 |> fold (add_thm true o `I) cls
                  |> add_tfrees
-                 |> fold (add_thm false) ths
+                 |> fold (add_thm false o `I) ths
       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
       fun is_used c =
         exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -695,11 +700,12 @@
           let
             val helper_ths =
               helpers |> filter (is_used o fst)
-                      |> maps (fn (_, (raw, thms)) =>
-                                  if mode = FT orelse not raw then
-                                    map (cnf_helper_theorem @{theory} raw) thms
+                      |> maps (fn (c, (needs_full_types, thms)) =>
+                                  if not (is_used c) orelse
+                                     needs_full_types andalso mode <> FT then
+                                    []
                                   else
-                                    [])
+                                    thms)
           in lmap |> fold (add_thm false) helper_ths end
   in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 19 14:39:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 19 18:16:47 2010 +0200
@@ -82,9 +82,9 @@
 
 (*Pairs a constant with the list of its type instantiations (using const_typ)*)
 fun const_with_typ thy (c,typ) =
-    let val tvars = Sign.const_typargs thy (c,typ)
-    in (c, map const_typ_of tvars) end
-    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)
+  let val tvars = Sign.const_typargs thy (c,typ) in
+    (c, map const_typ_of tvars) end
+  handle TYPE _ => (c, [])   (*Variable (locale constant): monomorphic*)
 
 (*Add a const/type pair to the table, but a [] entry means a standard connective,
   which we ignore.*)
@@ -95,7 +95,8 @@
 val fresh_prefix = "Sledgehammer.Fresh."
 val flip = Option.map not
 (* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts = [@{const_name If}, @{const_name Let}]
+val boring_consts =
+  [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)]
 
 fun get_consts_typs thy pos ts =
   let
@@ -104,9 +105,8 @@
        introduce a fresh constant to simulate the effect of Skolemization. *)
     fun do_term t =
       case t of
-        Const (@{const_name Let}, _) => I
-      | Const x => add_const_type_to_table (const_with_typ thy x)
-      | Free x => add_const_type_to_table (const_with_typ thy x)
+        Const x => add_const_type_to_table (const_with_typ thy x)
+      | Free (s, _) => add_const_type_to_table (s, [])
       | t1 $ t2 => do_term t1 #> do_term t2
       | Abs (_, _, t) =>
         (* Abstractions lead to combinators, so we add a penalty for them. *)
@@ -198,7 +198,7 @@
 fun count_axiom_consts theory_relevant thy (_, th) =
   let
     fun do_const (a, T) =
-      let val (c, cts) = const_with_typ thy (a,T) in
+      let val (c, cts) = const_with_typ thy (a, T) in
         (* Two-dimensional table update. Constant maps to types maps to
            count. *)
         CTtab.map_default (cts, 0) (Integer.add 1)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 19 14:39:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 19 18:16:47 2010 +0200
@@ -209,7 +209,7 @@
 val optional_typed_helpers =
   [(["c_True", "c_False"], @{thms True_or_False}),
    (["c_If"], @{thms if_True if_False True_or_False})]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+val mandatory_helpers = @{thms fequal_def}
 
 val init_counters =
   Symtab.make (maps (maps (map (rpair 0) o fst))

--- a/src/HOL/Tools/meson.ML	Thu Aug 19 14:39:31 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Aug 19 18:16:47 2010 +0200
@@ -527,7 +527,8 @@
   which are needed to avoid the various one-point theorems from generating junk clauses.*)
 val nnf_simps =
   @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
-         if_eq_cancel cases_simp}
+         if_eq_cancel cases_simp (* TODO: mem_def_raw Collect_def_raw *)}
+(* TODO:  @ [@{lemma "{} = (%x. False)" by (rule ext) auto}] *)
 val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
 
 val nnf_ss =
@@ -539,8 +540,7 @@
   #> simplify nnf_ss
 
 fun make_nnf ctxt th = case prems_of th of
-    [] => th |> presimplify
-             |> make_nnf1 ctxt
+    [] => th |> presimplify |> make_nnf1 ctxt
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
 
 (*Pull existential quantifiers to front. This accomplishes Skolemization for