1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -113,10 +113,6 @@
     1.4      handle TYPE _ => @{prop True}
     1.5    end
     1.6  
     1.7 -fun all_non_tautological_facts_of thy css_table =
     1.8 -  Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     1.9 -  |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
    1.10 -
    1.11  fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
    1.12    let
    1.13      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.14 @@ -126,7 +122,8 @@
    1.15      val mono = not (is_type_enc_polymorphic type_enc)
    1.16      val path = file_name |> Path.explode
    1.17      val _ = File.write path ""
    1.18 -    val facts = all_non_tautological_facts_of thy css_table
    1.19 +    val facts =
    1.20 +      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
    1.21      val atp_problem =
    1.22        facts
    1.23        |> map (fn ((_, loc), th) =>

     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 15:32:30 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 15:32:30 2012 +0200
     2.3 @@ -26,9 +26,7 @@
     2.4  
     2.5  val max_facts_slack = 2
     2.6  
     2.7 -val all_names =
     2.8 -  filter_out is_likely_tautology_or_too_meta
     2.9 -  #> map (rpair () o nickname_of) #> Symtab.make
    2.10 +val all_names = map (rpair () o nickname_of) #> Symtab.make
    2.11  
    2.12  fun evaluate_mash_suggestions ctxt params thy file_name =
    2.13    let

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

     4.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 15:32:30 2012 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 15:32:30 2012 +0200
     4.3 @@ -88,11 +88,13 @@
     4.4    val isabelle_info : string -> int -> (string, 'a) ho_term list
     4.5    val extract_isabelle_status : (string, 'a) ho_term list -> string option
     4.6    val extract_isabelle_rank : (string, 'a) ho_term list -> int
     4.7 +  val inductionN : string
     4.8    val introN : string
     4.9    val inductiveN : string
    4.10    val elimN : string
    4.11    val simpN : string
    4.12 -  val defN : string
    4.13 +  val non_rec_defN : string
    4.14 +  val rec_defN : string
    4.15    val rankN : string
    4.16    val minimum_rank : int
    4.17    val default_rank : int
    4.18 @@ -222,11 +224,14 @@
    4.19  
    4.20  val isabelle_info_prefix = "isabelle_"
    4.21  
    4.22 +val inductionN = "induction"
    4.23  val introN = "intro"
    4.24  val inductiveN = "inductive"
    4.25  val elimN = "elim"
    4.26  val simpN = "simp"
    4.27 -val defN = "def"
    4.28 +val non_rec_defN = "non_rec_def"
    4.29 +val rec_defN = "rec_def"
    4.30 +
    4.31  val rankN = "rank"
    4.32  
    4.33  val minimum_rank = 0
    4.34 @@ -503,9 +508,13 @@
    4.35      fun suffix_tag top_level s =
    4.36        if top_level then
    4.37          case extract_isabelle_status info of
    4.38 -          SOME s' => if s' = defN then s ^ ":lt"
    4.39 -                     else if s' = simpN andalso gen_simp then s ^ ":lr"
    4.40 -                     else s
    4.41 +          SOME s' =>
    4.42 +          if s' = non_rec_defN then
    4.43 +            s ^ ":lt"
    4.44 +          else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then
    4.45 +            s ^ ":lr"
    4.46 +          else
    4.47 +            s
    4.48          | NONE => s
    4.49        else
    4.50          s

     5.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jul 23 15:32:30 2012 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jul 23 15:32:30 2012 +0200
     5.3 @@ -18,7 +18,9 @@
     5.4    datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
     5.5  
     5.6    datatype scope = Global | Local | Assum | Chained
     5.7 -  datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
     5.8 +  datatype status =
     5.9 +    General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
    5.10 +    Rec_Def
    5.11    type stature = scope * status
    5.12  
    5.13    datatype strictness = Strict | Non_Strict
    5.14 @@ -103,6 +105,7 @@
    5.15    val helper_table : ((string * bool) * (status * thm) list) list
    5.16    val trans_lams_from_string :
    5.17      Proof.context -> type_enc -> string -> term list -> term list * term list
    5.18 +  val string_of_status : status -> string
    5.19    val factsN : string
    5.20    val prepare_atp_problem :
    5.21      Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
    5.22 @@ -123,7 +126,8 @@
    5.23  datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
    5.24  
    5.25  datatype scope = Global | Local | Assum | Chained
    5.26 -datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
    5.27 +datatype status =
    5.28 +  General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
    5.29  type stature = scope * status
    5.30  
    5.31  datatype order =
    5.32 @@ -1236,7 +1240,8 @@
    5.33              |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
    5.34      val lam_facts =
    5.35        map2 (fn t => fn j =>
    5.36 -               ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
    5.37 +               ((lam_fact_prefix ^ Int.toString j,
    5.38 +                 (Global, Non_Rec_Def)), (Axiom, t)))
    5.39             lambda_ts (1 upto length lambda_ts)
    5.40    in (facts, lam_facts) end
    5.41  
    5.42 @@ -1293,7 +1298,7 @@
    5.43                ((name, stature as (_, status)), t) =
    5.44    let
    5.45      val role =
    5.46 -      if is_format_with_defs format andalso status = Def andalso
    5.47 +      if is_format_with_defs format andalso status = Non_Rec_Def andalso
    5.48           is_legitimate_tptp_def t then
    5.49          Definition
    5.50        else
    5.51 @@ -1664,18 +1669,18 @@
    5.52  
    5.53  (* The Boolean indicates that a fairly sound type encoding is needed. *)
    5.54  val base_helper_table =
    5.55 -  [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
    5.56 -   (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
    5.57 -   (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
    5.58 -   (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
    5.59 -   (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
    5.60 +  [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
    5.61 +   (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
    5.62 +   (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
    5.63 +   (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
    5.64 +   (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
    5.65     ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
    5.66     (("fFalse", false), [(General, not_ffalse)]),
    5.67     (("fFalse", true), [(General, @{thm True_or_False})]),
    5.68     (("fTrue", false), [(General, ftrue)]),
    5.69     (("fTrue", true), [(General, @{thm True_or_False})]),
    5.70     (("If", true),
    5.71 -    [(Def, @{thm if_True}), (Def, @{thm if_False}),
    5.72 +    [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
    5.73       (General, @{thm True_or_False})])]
    5.74  
    5.75  val helper_table =
    5.76 @@ -1683,7 +1688,7 @@
    5.77    [(("fNot", false),
    5.78      @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    5.79             fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
    5.80 -    |> map (pair Def)),
    5.81 +    |> map (pair Non_Rec_Def)),
    5.82     (("fconj", false),
    5.83      @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
    5.84          by (unfold fconj_def) fast+}
    5.85 @@ -1718,19 +1723,19 @@
    5.86     ((app_op_name, true),
    5.87      [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
    5.88     (("fconj", false),
    5.89 -    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
    5.90 +    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    5.91     (("fdisj", false),
    5.92 -    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
    5.93 +    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    5.94     (("fimplies", false),
    5.95      @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
    5.96 -    |> map (pair Def)),
    5.97 +    |> map (pair Non_Rec_Def)),
    5.98     (("fequal", false),
    5.99 -    (@{thms fequal_table} |> map (pair Def)) @
   5.100 +    (@{thms fequal_table} |> map (pair Non_Rec_Def)) @
   5.101      (@{thms fequal_laws} |> map (pair General))),
   5.102     (("fAll", false),
   5.103 -    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
   5.104 +    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)),
   5.105     (("fEx", false),
   5.106 -    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
   5.107 +    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))]
   5.108    |> map (apsnd (map (apsnd zero_var_indexes)))
   5.109  
   5.110  fun bound_tvars type_enc sorts Ts =
   5.111 @@ -2104,28 +2109,29 @@
   5.112        | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
   5.113    in do_formula end
   5.114  
   5.115 +fun string_of_status General = ""
   5.116 +  | string_of_status Induction = inductionN
   5.117 +  | string_of_status Intro = introN
   5.118 +  | string_of_status Inductive = inductiveN
   5.119 +  | string_of_status Elim = elimN
   5.120 +  | string_of_status Simp = simpN
   5.121 +  | string_of_status Non_Rec_Def = non_rec_defN
   5.122 +  | string_of_status Rec_Def = rec_defN
   5.123 +
   5.124  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   5.125     of monomorphization). The TPTP explicitly forbids name clashes, and some of
   5.126     the remote provers might care. *)
   5.127  fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
   5.128 -                  (j, {name, stature, role, iformula, atomic_types}) =
   5.129 -  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
   5.130 -   iformula
   5.131 -   |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula
   5.132 -                            (if pos then SOME true else NONE)
   5.133 -   |> close_formula_universally
   5.134 -   |> bound_tvars type_enc true atomic_types,
   5.135 -   NONE,
   5.136 -   let val rank = rank j in
   5.137 -     case snd stature of
   5.138 -       Intro => isabelle_info introN rank
   5.139 -     | Inductive => isabelle_info inductiveN rank
   5.140 -     | Elim => isabelle_info elimN rank
   5.141 -     | Simp => isabelle_info simpN rank
   5.142 -     | Def => isabelle_info defN rank
   5.143 -     | _ => isabelle_info "" rank
   5.144 -   end)
   5.145 -  |> Formula
   5.146 +        (j, {name, stature = (_, status), role, iformula, atomic_types}) =
   5.147 +  Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
   5.148 +           encode name,
   5.149 +           role,
   5.150 +           iformula
   5.151 +           |> formula_from_iformula ctxt mono type_enc
   5.152 +                  should_guard_var_in_formula (if pos then SOME true else NONE)
   5.153 +           |> close_formula_universally
   5.154 +           |> bound_tvars type_enc true atomic_types,
   5.155 +           NONE, isabelle_info (string_of_status status) (rank j))
   5.156  
   5.157  fun lines_for_subclass type_enc sub super =
   5.158    Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
   5.159 @@ -2355,7 +2361,7 @@
   5.160               Axiom,
   5.161               eq_formula type_enc (atomic_types_of T) [] false
   5.162                    (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
   5.163 -             NONE, isabelle_info defN helper_rank)
   5.164 +             NONE, isabelle_info non_rec_defN helper_rank)
   5.165    end
   5.166  
   5.167  fun lines_for_mono_types ctxt mono type_enc Ts =
   5.168 @@ -2438,7 +2444,7 @@
   5.169      val tag_with = tag_with_type ctxt mono type_enc NONE
   5.170      fun formula c =
   5.171        [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
   5.172 -                defN helper_rank)]
   5.173 +                non_rec_defN helper_rank)]
   5.174    in
   5.175      if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
   5.176        []
   5.177 @@ -2538,7 +2544,7 @@
   5.178        in
   5.179          ([tm1, tm2],
   5.180           [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
   5.181 -                   NONE, isabelle_info defN helper_rank)])
   5.182 +                   NONE, isabelle_info non_rec_defN helper_rank)])
   5.183          |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
   5.184              else pair_append (do_alias (ary - 1)))
   5.185        end
   5.186 @@ -2878,8 +2884,9 @@
   5.187      fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
   5.188      val graph =
   5.189        Graph.empty
   5.190 -      |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
   5.191 -      |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
   5.192 +      |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem
   5.193 +      |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN
   5.194 +                                  orf is_conj)) o snd) problem
   5.195        |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
   5.196        |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
   5.197      fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1

     6.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 23 15:32:30 2012 +0200
     6.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 23 15:32:30 2012 +0200
     6.3 @@ -200,10 +200,11 @@
     6.4    else
     6.5      isa_ext
     6.6  
     6.7 -fun add_all_defs fact_names accum =
     6.8 +fun add_non_rec_defs fact_names accum =
     6.9    Vector.foldl
    6.10        (fn (facts, facts') =>
    6.11 -          union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
    6.12 +          union (op =)
    6.13 +                (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
    6.14                  facts')
    6.15        accum fact_names
    6.16  
    6.17 @@ -214,12 +215,12 @@
    6.18         (* LEO 1.3.3 does not record definitions properly, leading to missing
    6.19           dependencies in the TSTP proof. Remove the next line once this is
    6.20           fixed. *)
    6.21 -       add_all_defs fact_names
    6.22 +       add_non_rec_defs fact_names
    6.23       else if rule = satallax_unsat_coreN then
    6.24         (fn [] =>
    6.25             (* Satallax doesn't include definitions in its unsatisfiable cores,
    6.26                so we assume the worst and include them all here. *)
    6.27 -           [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
    6.28 +           [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
    6.29           | facts => facts)
    6.30       else
    6.31         I)

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
     7.3 @@ -23,7 +23,6 @@
     7.4    val fact_from_ref :
     7.5      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     7.6      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     7.7 -  val is_likely_tautology_or_too_meta : thm -> bool
     7.8    val backquote_thm : thm -> string
     7.9    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    7.10    val maybe_instantiate_inducts :
    7.11 @@ -50,7 +49,8 @@
    7.12     del : (Facts.ref * Attrib.src list) list,
    7.13     only : bool}
    7.14  
    7.15 -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    7.16 +val sledgehammer_prefixes =
    7.17 +  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
    7.18  
    7.19  (* experimental features *)
    7.20  val ignore_no_atp =
    7.21 @@ -182,9 +182,9 @@
    7.22    apply_depth t > max_apply_depth orelse
    7.23    (not ho_atp andalso formula_has_too_many_lambdas [] t)
    7.24  
    7.25 -(* FIXME: Extend to "Meson" and "Metis" *)
    7.26  val exists_sledgehammer_const =
    7.27 -  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
    7.28 +  exists_Const (fn (s, _) =>
    7.29 +      exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
    7.30  
    7.31  (* FIXME: make more reliable *)
    7.32  val exists_low_level_class_const =
    7.33 @@ -192,25 +192,11 @@
    7.34       s = @{const_name equal_class.equal} orelse
    7.35       String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
    7.36  
    7.37 -fun is_metastrange_theorem th =
    7.38 -  case head_of (concl_of th) of
    7.39 -    Const (s, _) => (s <> @{const_name Trueprop} andalso
    7.40 -                     s <> @{const_name "=="})
    7.41 -  | _ => false
    7.42 -
    7.43  fun is_that_fact th =
    7.44    String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
    7.45    andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
    7.46                             | _ => false) (prop_of th)
    7.47  
    7.48 -fun is_theorem_bad_for_atps ho_atp thm =
    7.49 -  is_metastrange_theorem thm orelse
    7.50 -  let val t = prop_of thm in
    7.51 -    is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
    7.52 -    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    7.53 -    is_that_fact thm
    7.54 -  end
    7.55 -
    7.56  fun is_likely_tautology_or_too_meta th =
    7.57    let
    7.58      val is_boring_const = member (op =) atp_widely_irrelevant_consts
    7.59 @@ -229,6 +215,15 @@
    7.60      is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
    7.61    end
    7.62  
    7.63 +fun is_theorem_bad_for_atps ho_atp th =
    7.64 +  is_likely_tautology_or_too_meta th orelse
    7.65 +  let val t = prop_of th in
    7.66 +    is_formula_too_complex ho_atp t orelse
    7.67 +    exists_type type_has_top_sort t orelse
    7.68 +    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    7.69 +    is_that_fact th
    7.70 +  end
    7.71 +
    7.72  fun hackish_string_for_term thy t =
    7.73    Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    7.74                     (print_mode_value ())) (Syntax.string_of_term_global thy) t
    7.75 @@ -299,8 +294,8 @@
    7.76              |> maps (snd o snd)
    7.77    in
    7.78      Termtab.empty |> add Simp [atomize] snd simps
    7.79 -                  |> add Simp [] I rec_defs
    7.80 -                  |> add Def [] I nonrec_defs
    7.81 +                  |> add Rec_Def [] I rec_defs
    7.82 +                  |> add Non_Rec_Def [] I nonrec_defs
    7.83  (* Add once it is used:
    7.84                    |> add Elim [] I elims
    7.85  *)
    7.86 @@ -458,7 +453,6 @@
    7.87         else
    7.88           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    7.89             all_facts ctxt ho_atp reserved add chained css
    7.90 -           |> filter_out (is_likely_tautology_or_too_meta o snd)
    7.91             |> filter_out (member Thm.eq_thm_prop del o snd)
    7.92             |> maybe_filter_no_atps ctxt
    7.93             |> uniquify

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     8.3 @@ -312,22 +312,32 @@
     8.4    |> forall is_lambda_free ts ? cons "no_lams"
     8.5    |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
     8.6    |> scope <> Global ? cons "local"
     8.7 -  |> (case status of
     8.8 -        General => I
     8.9 -      | Induction => cons "induction"
    8.10 -      | Intro => cons "intro"
    8.11 -      | Inductive => cons "inductive"
    8.12 -      | Elim => cons "elim"
    8.13 -      | Simp => cons "simp"
    8.14 -      | Def => cons "def")
    8.15 +  |> (case string_of_status status of "" => I | s => cons s)
    8.16  
    8.17  (* Too many dependencies is a sign that a decision procedure is at work. There
    8.18     isn't much too learn from such proofs. *)
    8.19 -val max_dependencies = 10
    8.20 +val max_dependencies = 15
    8.21  val atp_dependency_default_max_fact = 50
    8.22  
    8.23 +(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
    8.24 +val typedef_sig = [@{thm CollectI} |> nickname_of]
    8.25 +
    8.26 +(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
    8.27 +val typedef_ths =
    8.28 +  @{thms type_definition.Abs_inverse type_definition.Rep_inverse
    8.29 +         type_definition.Rep type_definition.Rep_inject
    8.30 +         type_definition.Abs_inject type_definition.Rep_cases
    8.31 +         type_definition.Abs_cases type_definition.Rep_induct
    8.32 +         type_definition.Abs_induct type_definition.Rep_range
    8.33 +         type_definition.Abs_image}
    8.34 +  |> map nickname_of
    8.35 +
    8.36  fun trim_dependencies deps =
    8.37 -  if length deps <= max_dependencies then SOME deps else NONE
    8.38 +  if length deps > max_dependencies orelse deps = typedef_sig orelse
    8.39 +     exists (member (op =) typedef_ths) deps then
    8.40 +    NONE
    8.41 +  else
    8.42 +    SOME deps
    8.43  
    8.44  fun isar_dependencies_of all_names =
    8.45    thms_in_proof (SOME all_names) #> trim_dependencies
    8.46 @@ -708,10 +718,7 @@
    8.47      else
    8.48        let
    8.49          val all_names =
    8.50 -          facts |> map snd
    8.51 -                |> filter_out is_likely_tautology_or_too_meta
    8.52 -                |> map (rpair () o nickname_of)
    8.53 -                |> Symtab.make
    8.54 +          facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
    8.55          val deps_of =
    8.56            if atp then
    8.57              atp_dependencies_of ctxt params prover auto_level facts all_names