# HG changeset patch
# User blanchet
# Date 1342035799 -7200
# Node ID fb11c09d7729a52ea1ca8265bf339770a1c232ce
# Parent  854a4767733544b7f8111ebd929c2a43c7f3492f
add Isabelle dependencies to tweak relevance filter

diff -r 854a47677335 -r fb11c09d7729 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
@@ -18,6 +18,11 @@
 *}
 
 ML {*
+val do_it = true (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
+*}
+
+ML {*
 if do_it then
   generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
 else
@@ -25,11 +30,6 @@
 *}
 
 ML {*
-val do_it = true (* switch to "true" to generate the files *);
-val thy = @{theory Nat}
-*}
-
-ML {*
 if do_it then
   generate_features thy false "/tmp/mash_features"
 else
diff -r 854a47677335 -r fb11c09d7729 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
@@ -201,8 +201,10 @@
         | Def => cons "def")
   end
 
-val dependencies_of =
-  map fact_name_of oo theorems_mentioned_in_proof_term o SOME
+fun dependencies_of all_facts =
+  theorems_mentioned_in_proof_term (SOME all_facts)
+  #> map fact_name_of
+  #> sort string_ord
 
 val freezeT = Type.legacy_freeze_type
 
@@ -306,20 +308,30 @@
       |> not include_thy ? filter_out (has_thy thy o snd)
     val ths = facts |> map snd
     val all_names = ths |> map Thm.get_name_hint
+    fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
+    fun add_isa_dep facts dep accum =
+      if exists (is_dep dep) accum then
+        accum
+      else case find_first (is_dep dep) facts of
+        SOME ((name, status), th) => accum @ [((name (), status), th)]
+      | NONE => accum (* shouldn't happen *)
+    fun fix_name ((_, stature), th) =
+      ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
     fun do_thm th =
       let
         val name = Thm.get_name_hint th
         val goal = goal_of_thm th
+        val isa_deps = dependencies_of all_names th
+        val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
         val facts =
-          facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
-                |> meng_paulson_facts ctxt (the max_relevant) goal
-                |> map (fn ((_, stature), th) =>
-                           ((th |> Thm.get_name_hint |> fact_name_of, stature),
-                            th))
+          facts |> meng_paulson_facts ctxt (the max_relevant) goal
+                |> fold (add_isa_dep facts) isa_deps
+                |> map fix_name
         val deps =
           case run_sledgehammer ctxt facts goal of
-            {outcome = NONE, used_facts, ...} => used_facts |> map fst
-          | _ => dependencies_of all_names th
+            {outcome = NONE, used_facts, ...} =>
+            used_facts |> map fst |> sort string_ord
+          | _ => isa_deps
         val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
@@ -370,6 +382,7 @@
               val suggs =
                 old_facts |> meng_paulson_facts ctxt max_relevant goal
                           |> map (fact_name_of o fst o fst)
+                          |> sort string_ord
               val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
             in File.append path s end
           else