distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh

--- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -113,10 +113,6 @@
     handle TYPE _ => @{prop True}
   end
 
-fun all_non_tautological_facts_of thy css_table =
-  Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
-  |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
-
 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -126,7 +122,8 @@
     val mono = not (is_type_enc_polymorphic type_enc)
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts = all_non_tautological_facts_of thy css_table
+    val facts =
+      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     val atp_problem =
       facts
       |> map (fn ((_, loc), th) =>

--- a/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -26,9 +26,7 @@
 
 val max_facts_slack = 2
 
-val all_names =
-  filter_out is_likely_tautology_or_too_meta
-  #> map (rpair () o nickname_of) #> Symtab.make
+val all_names = map (rpair () o nickname_of) #> Symtab.make
 
 fun evaluate_mash_suggestions ctxt params thy file_name =
   let

--- a/src/HOL/TPTP/mash_export.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -49,9 +49,7 @@
 val thy_name_of_fact = hd o Long_Name.explode
 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
 
-val all_names =
-  filter_out is_likely_tautology_or_too_meta
-  #> map (rpair () o nickname_of) #> Symtab.make
+val all_names = map (rpair () o nickname_of) #> Symtab.make
 
 fun generate_accessibility thy include_thy file_name =
   let

--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -88,11 +88,13 @@
   val isabelle_info : string -> int -> (string, 'a) ho_term list
   val extract_isabelle_status : (string, 'a) ho_term list -> string option
   val extract_isabelle_rank : (string, 'a) ho_term list -> int
+  val inductionN : string
   val introN : string
   val inductiveN : string
   val elimN : string
   val simpN : string
-  val defN : string
+  val non_rec_defN : string
+  val rec_defN : string
   val rankN : string
   val minimum_rank : int
   val default_rank : int
@@ -222,11 +224,14 @@
 
 val isabelle_info_prefix = "isabelle_"
 
+val inductionN = "induction"
 val introN = "intro"
 val inductiveN = "inductive"
 val elimN = "elim"
 val simpN = "simp"
-val defN = "def"
+val non_rec_defN = "non_rec_def"
+val rec_defN = "rec_def"
+
 val rankN = "rank"
 
 val minimum_rank = 0
@@ -503,9 +508,13 @@
     fun suffix_tag top_level s =
       if top_level then
         case extract_isabelle_status info of
-          SOME s' => if s' = defN then s ^ ":lt"
-                     else if s' = simpN andalso gen_simp then s ^ ":lr"
-                     else s
+          SOME s' =>
+          if s' = non_rec_defN then
+            s ^ ":lt"
+          else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then
+            s ^ ":lr"
+          else
+            s
         | NONE => s
       else
         s

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -18,7 +18,9 @@
   datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
 
   datatype scope = Global | Local | Assum | Chained
-  datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
+  datatype status =
+    General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
+    Rec_Def
   type stature = scope * status
 
   datatype strictness = Strict | Non_Strict
@@ -103,6 +105,7 @@
   val helper_table : ((string * bool) * (status * thm) list) list
   val trans_lams_from_string :
     Proof.context -> type_enc -> string -> term list -> term list * term list
+  val string_of_status : status -> string
   val factsN : string
   val prepare_atp_problem :
     Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
@@ -123,7 +126,8 @@
 datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
 
 datatype scope = Global | Local | Assum | Chained
-datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
+datatype status =
+  General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
 type stature = scope * status
 
 datatype order =
@@ -1236,7 +1240,8 @@
             |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
     val lam_facts =
       map2 (fn t => fn j =>
-               ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
+               ((lam_fact_prefix ^ Int.toString j,
+                 (Global, Non_Rec_Def)), (Axiom, t)))
            lambda_ts (1 upto length lambda_ts)
   in (facts, lam_facts) end
 
@@ -1293,7 +1298,7 @@
               ((name, stature as (_, status)), t) =
   let
     val role =
-      if is_format_with_defs format andalso status = Def andalso
+      if is_format_with_defs format andalso status = Non_Rec_Def andalso
          is_legitimate_tptp_def t then
         Definition
       else
@@ -1664,18 +1669,18 @@
 
 (* The Boolean indicates that a fairly sound type encoding is needed. *)
 val base_helper_table =
-  [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
-   (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
-   (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
-   (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
-   (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
+  [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
+   (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
+   (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
+   (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
+   (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
    ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
    (("fFalse", false), [(General, not_ffalse)]),
    (("fFalse", true), [(General, @{thm True_or_False})]),
    (("fTrue", false), [(General, ftrue)]),
    (("fTrue", true), [(General, @{thm True_or_False})]),
    (("If", true),
-    [(Def, @{thm if_True}), (Def, @{thm if_False}),
+    [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
      (General, @{thm True_or_False})])]
 
 val helper_table =
@@ -1683,7 +1688,7 @@
   [(("fNot", false),
     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
            fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
-    |> map (pair Def)),
+    |> map (pair Non_Rec_Def)),
    (("fconj", false),
     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
         by (unfold fconj_def) fast+}
@@ -1718,19 +1723,19 @@
    ((app_op_name, true),
     [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
    (("fconj", false),
-    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
+    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    (("fdisj", false),
-    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
+    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    (("fimplies", false),
     @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
-    |> map (pair Def)),
+    |> map (pair Non_Rec_Def)),
    (("fequal", false),
-    (@{thms fequal_table} |> map (pair Def)) @
+    (@{thms fequal_table} |> map (pair Non_Rec_Def)) @
     (@{thms fequal_laws} |> map (pair General))),
    (("fAll", false),
-    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
+    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)),
    (("fEx", false),
-    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
+    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))]
   |> map (apsnd (map (apsnd zero_var_indexes)))
 
 fun bound_tvars type_enc sorts Ts =
@@ -2104,28 +2109,29 @@
       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
   in do_formula end
 
+fun string_of_status General = ""
+  | string_of_status Induction = inductionN
+  | string_of_status Intro = introN
+  | string_of_status Inductive = inductiveN
+  | string_of_status Elim = elimN
+  | string_of_status Simp = simpN
+  | string_of_status Non_Rec_Def = non_rec_defN
+  | string_of_status Rec_Def = rec_defN
+
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
 fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
-                  (j, {name, stature, role, iformula, atomic_types}) =
-  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
-   iformula
-   |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula
-                            (if pos then SOME true else NONE)
-   |> close_formula_universally
-   |> bound_tvars type_enc true atomic_types,
-   NONE,
-   let val rank = rank j in
-     case snd stature of
-       Intro => isabelle_info introN rank
-     | Inductive => isabelle_info inductiveN rank
-     | Elim => isabelle_info elimN rank
-     | Simp => isabelle_info simpN rank
-     | Def => isabelle_info defN rank
-     | _ => isabelle_info "" rank
-   end)
-  |> Formula
+        (j, {name, stature = (_, status), role, iformula, atomic_types}) =
+  Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
+           encode name,
+           role,
+           iformula
+           |> formula_from_iformula ctxt mono type_enc
+                  should_guard_var_in_formula (if pos then SOME true else NONE)
+           |> close_formula_universally
+           |> bound_tvars type_enc true atomic_types,
+           NONE, isabelle_info (string_of_status status) (rank j))
 
 fun lines_for_subclass type_enc sub super =
   Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
@@ -2355,7 +2361,7 @@
              Axiom,
              eq_formula type_enc (atomic_types_of T) [] false
                   (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
-             NONE, isabelle_info defN helper_rank)
+             NONE, isabelle_info non_rec_defN helper_rank)
   end
 
 fun lines_for_mono_types ctxt mono type_enc Ts =
@@ -2438,7 +2444,7 @@
     val tag_with = tag_with_type ctxt mono type_enc NONE
     fun formula c =
       [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
-                defN helper_rank)]
+                non_rec_defN helper_rank)]
   in
     if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
       []
@@ -2538,7 +2544,7 @@
       in
         ([tm1, tm2],
          [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
-                   NONE, isabelle_info defN helper_rank)])
+                   NONE, isabelle_info non_rec_defN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
@@ -2878,8 +2884,9 @@
     fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
     val graph =
       Graph.empty
-      |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
-      |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
+      |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem
+      |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN
+                                  orf is_conj)) o snd) problem
       |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
       |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
     fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -200,10 +200,11 @@
   else
     isa_ext
 
-fun add_all_defs fact_names accum =
+fun add_non_rec_defs fact_names accum =
   Vector.foldl
       (fn (facts, facts') =>
-          union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
+          union (op =)
+                (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
                 facts')
       accum fact_names
 
@@ -214,12 +215,12 @@
        (* LEO 1.3.3 does not record definitions properly, leading to missing
          dependencies in the TSTP proof. Remove the next line once this is
          fixed. *)
-       add_all_defs fact_names
+       add_non_rec_defs fact_names
      else if rule = satallax_unsat_coreN then
        (fn [] =>
            (* Satallax doesn't include definitions in its unsatisfiable cores,
               so we assume the worst and include them all here. *)
-           [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
+           [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
          | facts => facts)
      else
        I)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -23,7 +23,6 @@
   val fact_from_ref :
     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
-  val is_likely_tautology_or_too_meta : thm -> bool
   val backquote_thm : thm -> string
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   val maybe_instantiate_inducts :
@@ -50,7 +49,8 @@
    del : (Facts.ref * Attrib.src list) list,
    only : bool}
 
-val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+val sledgehammer_prefixes =
+  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
 
 (* experimental features *)
 val ignore_no_atp =
@@ -182,9 +182,9 @@
   apply_depth t > max_apply_depth orelse
   (not ho_atp andalso formula_has_too_many_lambdas [] t)
 
-(* FIXME: Extend to "Meson" and "Metis" *)
 val exists_sledgehammer_const =
-  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
+  exists_Const (fn (s, _) =>
+      exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
 
 (* FIXME: make more reliable *)
 val exists_low_level_class_const =
@@ -192,25 +192,11 @@
      s = @{const_name equal_class.equal} orelse
      String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
 
-fun is_metastrange_theorem th =
-  case head_of (concl_of th) of
-    Const (s, _) => (s <> @{const_name Trueprop} andalso
-                     s <> @{const_name "=="})
-  | _ => false
-
 fun is_that_fact th =
   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
                            | _ => false) (prop_of th)
 
-fun is_theorem_bad_for_atps ho_atp thm =
-  is_metastrange_theorem thm orelse
-  let val t = prop_of thm in
-    is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
-    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
-    is_that_fact thm
-  end
-
 fun is_likely_tautology_or_too_meta th =
   let
     val is_boring_const = member (op =) atp_widely_irrelevant_consts
@@ -229,6 +215,15 @@
     is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
   end
 
+fun is_theorem_bad_for_atps ho_atp th =
+  is_likely_tautology_or_too_meta th orelse
+  let val t = prop_of th in
+    is_formula_too_complex ho_atp t orelse
+    exists_type type_has_top_sort t orelse
+    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
+    is_that_fact th
+  end
+
 fun hackish_string_for_term thy t =
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                    (print_mode_value ())) (Syntax.string_of_term_global thy) t
@@ -299,8 +294,8 @@
             |> maps (snd o snd)
   in
     Termtab.empty |> add Simp [atomize] snd simps
-                  |> add Simp [] I rec_defs
-                  |> add Def [] I nonrec_defs
+                  |> add Rec_Def [] I rec_defs
+                  |> add Non_Rec_Def [] I nonrec_defs
 (* Add once it is used:
                   |> add Elim [] I elims
 *)
@@ -458,7 +453,6 @@
        else
          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
            all_facts ctxt ho_atp reserved add chained css
-           |> filter_out (is_likely_tautology_or_too_meta o snd)
            |> filter_out (member Thm.eq_thm_prop del o snd)
            |> maybe_filter_no_atps ctxt
            |> uniquify

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -312,22 +312,32 @@
   |> forall is_lambda_free ts ? cons "no_lams"
   |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
   |> scope <> Global ? cons "local"
-  |> (case status of
-        General => I
-      | Induction => cons "induction"
-      | Intro => cons "intro"
-      | Inductive => cons "inductive"
-      | Elim => cons "elim"
-      | Simp => cons "simp"
-      | Def => cons "def")
+  |> (case string_of_status status of "" => I | s => cons s)
 
 (* Too many dependencies is a sign that a decision procedure is at work. There
    isn't much too learn from such proofs. *)
-val max_dependencies = 10
+val max_dependencies = 15
 val atp_dependency_default_max_fact = 50
 
+(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
+val typedef_sig = [@{thm CollectI} |> nickname_of]
+
+(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
+val typedef_ths =
+  @{thms type_definition.Abs_inverse type_definition.Rep_inverse
+         type_definition.Rep type_definition.Rep_inject
+         type_definition.Abs_inject type_definition.Rep_cases
+         type_definition.Abs_cases type_definition.Rep_induct
+         type_definition.Abs_induct type_definition.Rep_range
+         type_definition.Abs_image}
+  |> map nickname_of
+
 fun trim_dependencies deps =
-  if length deps <= max_dependencies then SOME deps else NONE
+  if length deps > max_dependencies orelse deps = typedef_sig orelse
+     exists (member (op =) typedef_ths) deps then
+    NONE
+  else
+    SOME deps
 
 fun isar_dependencies_of all_names =
   thms_in_proof (SOME all_names) #> trim_dependencies
@@ -708,10 +718,7 @@
     else
       let
         val all_names =
-          facts |> map snd
-                |> filter_out is_likely_tautology_or_too_meta
-                |> map (rpair () o nickname_of)
-                |> Symtab.make
+          facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
         val deps_of =
           if atp then
             atp_dependencies_of ctxt params prover auto_level facts all_names