author blanchet Wed Dec 12 02:47:45 2012 +0100 (2012-12-12 ago) changeset 50485 3c6ac2da2f45 parent 50484 8ec31bdb9d36 child 50486 d5dc28fafd9d
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
```     1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed Dec 12 00:24:06 2012 +0100
1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Dec 12 02:47:45 2012 +0100
1.3 @@ -136,13 +136,13 @@
1.4      val atp_problem =
1.5        atp_problem
1.6        |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
1.7 -    val ths = facts |> map snd
1.8 -    val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make
1.9 +    val all_names = Sledgehammer_Fact.build_all_names Thm.get_name_hint facts
1.10      val infers =
1.11 -      facts |> map (fn (_, th) =>
1.12 -                       (fact_name_of (Thm.get_name_hint th),
1.13 -                        th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
1.14 -                           |> map fact_name_of))
1.15 +      facts
1.16 +      |> map (fn (_, th) =>
1.17 +                 (fact_name_of (Thm.get_name_hint th),
1.18 +                  th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
1.19 +                     |> map fact_name_of))
1.20      val all_atp_problem_names =
1.21        atp_problem |> maps (map ident_of_problem_line o snd)
1.22      val infers =
```
```     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Dec 12 00:24:06 2012 +0100
2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Dec 12 02:47:45 2012 +0100
2.3 @@ -24,8 +24,6 @@
2.4  val MeShN = "MeSh"
2.5  val IsarN = "Isar"
2.6
2.7 -val all_names = map (rpair () o nickname_of) #> Symtab.make
2.8 -
2.9  fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name
2.10                                report_file_name =
2.11    let
2.12 @@ -40,7 +38,7 @@
2.13      val lines = sugg_path |> File.read_lines
2.14      val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.15      val facts = all_facts ctxt true false Symtab.empty [] [] css
2.16 -    val all_names = all_names (facts |> map snd)
2.17 +    val all_names = build_all_names nickname_of facts
2.18      val mepo_ok = Unsynchronized.ref 0
2.19      val mash_ok = Unsynchronized.ref 0
2.20      val mesh_ok = Unsynchronized.ref 0
```
```     3.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Dec 12 00:24:06 2012 +0100
3.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Dec 12 02:47:45 2012 +0100
3.3 @@ -28,11 +28,12 @@
3.4  structure MaSh_Export : MASH_EXPORT =
3.5  struct
3.6
3.7 +open Sledgehammer_Fact
3.8  open Sledgehammer_MePo
3.9  open Sledgehammer_MaSh
3.10
3.11  fun thy_map_from_facts ths =
3.12 -  ths |> sort (thm_ord o swap o pairself snd)
3.13 +  ths |> rev
3.14        |> map (snd #> `(theory_of_thm #> Context.theory_name))
3.15        |> AList.coalesce (op =)
3.16        |> map (apsnd (map nickname_of))
3.17 @@ -45,6 +46,7 @@
3.18  fun all_facts ctxt =
3.19    let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
3.20      Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css
3.21 +    |> sort (thm_ord o pairself snd)
3.22    end
3.23
3.24  fun add_thy_parent_facts thy_map thy =
3.25 @@ -59,8 +61,6 @@
3.26  val thy_name_of_fact = hd o Long_Name.explode
3.27  fun thy_of_fact thy = Context.get_theory thy o thy_name_of_fact
3.28
3.29 -val all_names = map (rpair () o nickname_of) #> Symtab.make
3.30 -
3.31  fun generate_accessibility ctxt thys include_thys file_name =
3.32    let
3.33      val path = file_name |> Path.explode
3.34 @@ -110,18 +110,16 @@
3.35      val path = file_name |> Path.explode
3.36      val _ = File.write path ""
3.37      val facts =
3.38 -      all_facts ctxt
3.39 -      |> not include_thys ? filter_out (has_thys thys o snd)
3.40 -    val ths = facts |> map snd
3.41 -    val all_names = all_names ths
3.42 -    fun do_thm th =
3.43 +      all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
3.44 +    val all_names = build_all_names nickname_of facts
3.45 +    fun do_fact (_, th) =
3.46        let
3.47          val name = nickname_of th
3.48          val deps =
3.49            isar_or_prover_dependencies_of ctxt params_opt facts all_names th
3.50          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
3.51        in File.append path s end
3.52 -  in List.app do_thm ths end
3.53 +  in List.app do_fact facts end
3.54
3.55  fun generate_isar_dependencies ctxt =
3.56    generate_isar_or_prover_dependencies ctxt NONE
3.57 @@ -134,10 +132,8 @@
3.58      val path = file_name |> Path.explode
3.59      val _ = File.write path ""
3.60      val facts = all_facts ctxt
3.61 -    val (new_facts, old_facts) =
3.62 -      facts |> List.partition (has_thys thys o snd)
3.63 -            |>> sort (thm_ord o pairself snd)
3.64 -    val all_names = all_names (map snd facts)
3.65 +    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
3.66 +    val all_names = build_all_names nickname_of facts
3.67      fun do_fact ((_, stature), th) prevs =
3.68        let
3.69          val name = nickname_of th
3.70 @@ -171,9 +167,7 @@
3.71      val _ = File.write path ""
3.72      val prover = hd provers
3.73      val facts = all_facts ctxt
3.74 -    val (new_facts, old_facts) =
3.75 -      facts |> List.partition (has_thys thys o snd)
3.76 -            |>> sort (thm_ord o pairself snd)
3.77 +    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
3.78      fun do_fact (fact as (_, th)) old_facts =
3.79        let
3.80          val name = nickname_of th
```
```     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 00:24:06 2012 +0100
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 02:47:45 2012 +0100
4.3 @@ -25,7 +25,8 @@
4.4      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
4.5    val backquote_thm : Proof.context -> thm -> string
4.6    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
4.7 -  val normalize_eq : term -> term
4.8 +  val build_all_names :
4.9 +    (thm -> string) -> ('a * thm) list -> string Symtab.table
4.10    val maybe_instantiate_inducts :
4.11      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
4.12      -> (((unit -> string) * 'a) * thm) list
4.13 @@ -320,9 +321,25 @@
4.14      else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 \$ t2 \$ t1))
4.15    | normalize_eq t = t
4.16
4.17 -fun uniquify xs =
4.18 +val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
4.19 +
4.20 +fun if_thm_before th th' =
4.21 +  if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
4.22 +
4.23 +fun build_all_names name_of facts =
4.24 +  Termtab.fold
4.25 +      (fn (_, aliases as main :: _) =>
4.26 +          fold (fn alias =>
4.27 +                   Symtab.update (name_of alias,
4.28 +                                  name_of (if_thm_before main alias))) aliases)
4.29 +      (fold_rev (fn (_, thm) =>
4.30 +                    Termtab.cons_list (normalize_eq_etc (prop_of thm), thm))
4.31 +            facts Termtab.empty)
4.32 +      Symtab.empty
4.33 +
4.34 +fun uniquify facts =
4.35    Termtab.fold (cons o snd)
4.36 -      (fold (Termtab.default o `(normalize_eq o prop_of o snd)) xs
4.37 +      (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
4.38              Termtab.empty) []
4.39
4.40  fun struct_induct_rule_on th =
4.41 @@ -411,36 +428,37 @@
4.42            I
4.43          else
4.44            let
4.45 -            val multi = length ths > 1
4.46 +            val n = length ths
4.47 +            val multi = n > 1
4.48              fun check_thms a =
4.49                case try (Proof_Context.get_thms ctxt) a of
4.50                  NONE => false
4.51                | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
4.52            in
4.53 -            pair 1
4.54 -            #> fold (fn th => fn (j, (multis, unis)) =>
4.55 -                        (j + 1,
4.56 -                         if not (member Thm.eq_thm_prop add_ths th) andalso
4.57 -                            is_theorem_bad_for_atps ho_atp th then
4.58 -                           (multis, unis)
4.59 -                         else
4.60 -                           let
4.61 -                             val new =
4.62 -                               (((fn () =>
4.63 -                                     if name0 = "" then
4.64 -                                       backquote_thm ctxt th
4.65 -                                     else
4.66 -                                       [Facts.extern ctxt facts name0,
4.67 -                                        Name_Space.extern ctxt full_space name0]
4.68 -                                       |> find_first check_thms
4.69 -                                       |> the_default name0
4.70 -                                       |> make_name reserved multi j),
4.71 -                                  stature_of_thm global assms chained css name0
4.72 -                                                 th), th)
4.73 -                           in
4.74 -                             if multi then (new :: multis, unis)
4.75 -                             else (multis, new :: unis)
4.76 -                           end)) ths
4.77 +            pair n
4.78 +            #> fold_rev (fn th => fn (j, (multis, unis)) =>
4.79 +                   (j - 1,
4.80 +                    if not (member Thm.eq_thm_prop add_ths th) andalso
4.81 +                       is_theorem_bad_for_atps ho_atp th then
4.82 +                      (multis, unis)
4.83 +                    else
4.84 +                      let
4.85 +                        val new =
4.86 +                          (((fn () =>
4.87 +                                if name0 = "" then
4.88 +                                  backquote_thm ctxt th
4.89 +                                else
4.90 +                                  [Facts.extern ctxt facts name0,
4.91 +                                   Name_Space.extern ctxt full_space name0]
4.92 +                                  |> find_first check_thms
4.93 +                                  |> the_default name0
4.94 +                                  |> make_name reserved multi j),
4.95 +                             stature_of_thm global assms chained css name0 th),
4.96 +                           th)
4.97 +                      in
4.98 +                        if multi then (new :: multis, unis)
4.99 +                        else (multis, new :: unis)
4.100 +                      end)) ths
4.101              #> snd
4.102            end)
4.103    in
```
```     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 12 00:24:06 2012 +0100
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 12 02:47:45 2012 +0100
5.3 @@ -54,9 +54,9 @@
5.4    val features_of :
5.5      Proof.context -> string -> theory -> stature -> term list
5.6      -> (string * real) list
5.7 -  val isar_dependencies_of : unit Symtab.table -> thm -> string list option
5.8 +  val isar_dependencies_of : string Symtab.table -> thm -> string list option
5.9    val prover_dependencies_of :
5.10 -    Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
5.11 +    Proof.context -> params -> string -> int -> fact list -> string Symtab.table
5.12      -> thm -> bool * string list option
5.13    val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
5.14    val find_mash_suggestions :
5.15 @@ -296,7 +296,7 @@
5.16
5.17  local
5.18
5.19 -val version = "*** MaSh version 20121205c ***"
5.20 +val version = "*** MaSh version 20121212a ***"
5.21
5.22  exception Too_New of unit
5.23
5.24 @@ -836,7 +836,7 @@
5.25
5.26  val commit_timeout = seconds 30.0
5.27
5.28 -(* The timeout is understood in a very slack fashion. *)
5.29 +(* The timeout is understood in a very relaxed fashion. *)
5.30  fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
5.31                       auto_level run_prover learn_timeout facts =
5.32    let
5.33 @@ -844,9 +844,9 @@
5.34      fun next_commit_time () =
5.35        Time.+ (Timer.checkRealTimer timer, commit_timeout)
5.36      val {fact_G, ...} = mash_get ctxt
5.37 +    val facts = facts |> sort (thm_ord o pairself snd)
5.38      val (old_facts, new_facts) =
5.39        facts |> List.partition (is_fact_in_graph fact_G)
5.40 -            ||> sort (thm_ord o pairself snd)
5.41    in
5.42      if null new_facts andalso (not run_prover orelse null old_facts) then
5.43        if auto_level < 2 then
5.44 @@ -861,9 +861,7 @@
5.45          ""
5.46      else
5.47        let
5.48 -        val all_names =
5.49 -          Symtab.empty
5.50 -          |> fold Symtab.update (facts |> map (rpair () o nickname_of o snd))
5.51 +        val all_names = build_all_names nickname_of facts
5.52          fun deps_of status th =
5.53            if status = Non_Rec_Def orelse status = Rec_Def then
5.54              SOME []
```
```     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Dec 12 00:24:06 2012 +0100
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Dec 12 02:47:45 2012 +0100
6.3 @@ -17,7 +17,7 @@
6.4    val parse_time_option : string -> string -> Time.time option
6.5    val subgoal_count : Proof.state -> int
6.6    val reserved_isar_keyword_table : unit -> unit Symtab.table
6.7 -  val thms_in_proof : unit Symtab.table option -> thm -> string list
6.8 +  val thms_in_proof : string Symtab.table option -> thm -> string list
6.9    val thms_of_name : Proof.context -> string -> thm list
6.10    val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
6.11  end;
6.12 @@ -97,7 +97,10 @@
6.13    let
6.14      val collect =
6.15        case all_names of
6.16 -        SOME names => (fn s => Symtab.defined names s ? insert (op =) s)
6.17 +        SOME names =>
6.18 +        (fn s => case Symtab.lookup names s of
6.19 +                   SOME s' => insert (op =) s'
6.20 +                 | NONE => I)
6.21        | NONE => insert (op =)
6.22      val names =
6.23        [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
```