1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  ML {*
     1.6  val do_it = false (* switch to "true" to generate the files *);
     1.7 -val thy = @{theory Nat};
     1.8 +val thy = @{theory List};
     1.9  val params = Sledgehammer_Isar.default_params @{context} []
    1.10  *}
    1.11  

     2.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4          val _ = File.append path (query ^ update)
     2.5        in [name] end
     2.6      val thy_ths = old_facts |> thms_by_thy
     2.7 -    val parents = parent_thms thy_ths thy
     2.8 +    val parents = parent_facts thy_ths thy
     2.9    in fold do_fact new_facts parents; () end
    2.10  
    2.11  fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
     3.3 @@ -10,6 +10,8 @@
     3.4    type status = ATP_Problem_Generate.status
     3.5    type stature = ATP_Problem_Generate.stature
     3.6  
     3.7 +  type fact = ((unit -> string) * stature) * thm
     3.8 +
     3.9    type fact_override =
    3.10      {add : (Facts.ref * Attrib.src list) list,
    3.11       del : (Facts.ref * Attrib.src list) list,
    3.12 @@ -27,13 +29,12 @@
    3.13      -> (((unit -> string) * 'a) * thm) list
    3.14    val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    3.15    val all_facts :
    3.16 -    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
    3.17 -    -> thm list -> status Termtab.table
    3.18 -    -> (((unit -> string) * stature) * thm) list
    3.19 -  val all_facts_of : theory -> (((unit -> string) * stature) * thm) list
    3.20 +    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
    3.21 +    -> status Termtab.table -> fact list
    3.22 +  val all_facts_of : theory -> fact list
    3.23    val nearly_all_facts :
    3.24      Proof.context -> bool -> fact_override -> thm list -> term list -> term
    3.25 -    -> (((unit -> string) * stature) * thm) list
    3.26 +    -> fact list
    3.27  end;
    3.28  
    3.29  structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    3.30 @@ -43,6 +44,8 @@
    3.31  open Metis_Tactic
    3.32  open Sledgehammer_Util
    3.33  
    3.34 +type fact = ((unit -> string) * stature) * thm
    3.35 +
    3.36  type fact_override =
    3.37    {add : (Facts.ref * Attrib.src list) list,
    3.38     del : (Facts.ref * Attrib.src list) list,

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     4.3 @@ -8,6 +8,7 @@
     4.4  signature SLEDGEHAMMER_FILTER_ITER =
     4.5  sig
     4.6    type stature = ATP_Problem_Generate.stature
     4.7 +  type fact = Sledgehammer_Fact.fact
     4.8    type params = Sledgehammer_Provers.params
     4.9    type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    4.10  
    4.11 @@ -19,14 +20,14 @@
    4.12      -> string list
    4.13    val iterative_relevant_facts :
    4.14      Proof.context -> params -> string -> int -> relevance_fudge option
    4.15 -    -> term list -> term -> (((unit -> string) * stature) * thm) list
    4.16 -    -> (((unit -> string) * stature) * thm) list
    4.17 +    -> term list -> term -> fact list -> fact list
    4.18  end;
    4.19  
    4.20  structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    4.21  struct
    4.22  
    4.23  open ATP_Problem_Generate
    4.24 +open Sledgehammer_Fact
    4.25  open Sledgehammer_Provers
    4.26  
    4.27  val trace =
    4.28 @@ -333,12 +334,9 @@
    4.29          val res = rel_weight / (rel_weight + irrel_weight)
    4.30        in if Real.isFinite res then res else 0.0 end
    4.31  
    4.32 -type annotated_thm =
    4.33 -  (((unit -> string) * stature) * thm) * (string * ptype) list
    4.34 -
    4.35  fun take_most_relevant ctxt max_facts remaining_max
    4.36          ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
    4.37 -        (candidates : (annotated_thm * real) list) =
    4.38 +        (candidates : ((fact * (string * ptype) list) * real) list) =
    4.39    let
    4.40      val max_imperfect =
    4.41        Real.ceil (Math.pow (max_imperfect,

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     5.3 @@ -8,25 +8,23 @@
     5.4  sig
     5.5    type status = ATP_Problem_Generate.status
     5.6    type stature = ATP_Problem_Generate.stature
     5.7 +  type fact = Sledgehammer_Fact.fact
     5.8 +  type fact_override = Sledgehammer_Fact.fact_override
     5.9    type params = Sledgehammer_Provers.params
    5.10 -  type fact_override = Sledgehammer_Fact.fact_override
    5.11    type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    5.12    type prover_result = Sledgehammer_Provers.prover_result
    5.13  
    5.14    val fact_name_of : string -> string
    5.15 -  val all_non_tautological_facts_of :
    5.16 -    theory -> (((unit -> string) * stature) * thm) list
    5.17 +  val all_non_tautological_facts_of : theory -> fact list
    5.18    val theory_ord : theory * theory -> order
    5.19    val thm_ord : thm * thm -> order
    5.20    val thms_by_thy : ('a * thm) list -> (string * thm list) list
    5.21    val has_thy : theory -> thm -> bool
    5.22 -  val parent_thms : (string * thm list) list -> theory -> string list
    5.23 +  val parent_facts : (string * thm list) list -> theory -> string list
    5.24    val features_of : theory -> status * thm -> string list
    5.25    val isabelle_dependencies_of : string list -> thm -> string list
    5.26    val goal_of_thm : theory -> thm -> thm
    5.27 -  val run_prover :
    5.28 -    Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm
    5.29 -    -> prover_result
    5.30 +  val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
    5.31    val generate_accessibility : theory -> bool -> string -> unit
    5.32    val generate_features : theory -> bool -> string -> unit
    5.33    val generate_isa_dependencies : theory -> bool -> string -> unit
    5.34 @@ -42,8 +40,7 @@
    5.35  
    5.36    val relevant_facts :
    5.37      Proof.context -> params -> string -> int -> fact_override -> term list
    5.38 -    -> term -> (((unit -> string) * stature) * thm) list
    5.39 -    -> (((unit -> string) * stature) * thm) list
    5.40 +    -> term -> fact list -> fact list
    5.41  end;
    5.42  
    5.43  structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
    5.44 @@ -205,11 +202,15 @@
    5.45  
    5.46  fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
    5.47  
    5.48 -fun parent_thms thy_ths thy =
    5.49 -  Theory.parents_of thy
    5.50 -  |> map Context.theory_name
    5.51 -  |> map_filter (AList.lookup (op =) thy_ths)
    5.52 -  |> map List.last
    5.53 +fun add_last_thms thy_ths thy =
    5.54 +  case AList.lookup (op =) thy_ths (Context.theory_name thy) of
    5.55 +    SOME (ths as _ :: _) => insert Thm.eq_thm (List.last ths)
    5.56 +  | _ => add_parent_thms thy_ths thy
    5.57 +and add_parent_thms thy_ths thy =
    5.58 +  fold (add_last_thms thy_ths) (Theory.parents_of thy)
    5.59 +
    5.60 +fun parent_facts thy_ths thy =
    5.61 +  add_parent_thms thy_ths thy []
    5.62    |> map (fact_name_of o Thm.get_name_hint)
    5.63  
    5.64  fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
    5.65 @@ -276,7 +277,7 @@
    5.66      fun do_thy ths =
    5.67        let
    5.68          val thy = theory_of_thm (hd ths)
    5.69 -        val parents = parent_thms thy_ths thy
    5.70 +        val parents = parent_facts thy_ths thy
    5.71          val ths = ths |> map (fact_name_of o Thm.get_name_hint)
    5.72        in fold do_thm ths parents; () end
    5.73    in List.app (do_thy o snd) thy_ths end