# HG changeset patch
# User blanchet
# Date 1343292483 -7200
# Node ID 7da5d3b8aef4e016bd3c18c9ff7f39c19fa383ba
# Parent  d443166f95202b12246a357e9d9550b1c117d9a8
don't export technical theorems for MaSh

diff -r d443166f9520 -r 7da5d3b8aef4 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 10:48:03 2012 +0200
@@ -23,9 +23,10 @@
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
 *}
+
 ML {*
 if do_it then
-  generate_accessibility thy false "/tmp/mash_accessibility"
+  generate_accessibility @{context} thy false "/tmp/mash_accessibility"
 else
   ()
 *}
@@ -39,7 +40,7 @@
 
 ML {*
 if do_it then
-  generate_isar_dependencies thy false "/tmp/mash_dependencies"
+  generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies"
 else
   ()
 *}
diff -r d443166f9520 -r 7da5d3b8aef4 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -37,6 +37,12 @@
 fun has_thy thy th =
   Context.theory_name thy = Context.theory_name (theory_of_thm th)
 
+fun all_non_technical_facts ctxt thy =
+  let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
+    all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+    |> filter_out (is_thm_technical o snd)
+  end
+
 fun parent_facts thy thy_map =
   let
     fun add_last thy =
@@ -65,9 +71,8 @@
         val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
         val _ = File.append path s
       in [fact] end
-    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val thy_map =
-      all_facts ctxt false Symtab.empty [] [] css
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> thy_map_from_facts
     fun do_thy facts =
@@ -81,9 +86,8 @@
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val css = clasimpset_rule_table_of ctxt
     val facts =
-      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
     fun do_fact ((_, stature), th) =
       let
@@ -98,9 +102,8 @@
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val ths =
-      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> map snd
     val all_names = all_names ths
@@ -118,9 +121,8 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val prover = hd provers
-    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val facts =
-      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
     val ths = facts |> map snd
     val all_names = all_names ths
@@ -137,9 +139,7 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val prover = hd provers
-    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts =
-      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+    val facts = all_non_technical_facts ctxt thy
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
@@ -168,9 +168,7 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val prover = hd provers
-    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts =
-      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+    val facts = all_non_technical_facts ctxt thy
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
diff -r d443166f9520 -r 7da5d3b8aef4 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -45,6 +45,7 @@
   val atp_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
     -> thm -> string list option
+  val is_thm_technical : thm -> bool
   val mash_CLEAR : Proof.context -> unit
   val mash_ADD :
     Proof.context -> bool
@@ -399,6 +400,14 @@
       | _ => NONE
     end
 
+val technical_theories =
+  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
+   "New_DSequence", "New_Random_Sequence", "Quickcheck",
+   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
+
+val is_thm_technical =
+  member (op =) technical_theories o Context.theory_name o theory_of_thm
+
 
 (*** Low-level communication with MaSh ***)
 
@@ -700,14 +709,6 @@
           (true, "")
         end)
 
-val evil_theories =
-  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
-   "New_DSequence", "New_Random_Sequence", "Quickcheck",
-   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
-
-fun fact_has_evil_theory (_, th) =
-  member (op =) evil_theories (Context.theory_name (theory_of_thm th))
-
 fun sendback sub =
   Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
 
@@ -722,7 +723,7 @@
       Time.+ (Timer.checkRealTimer timer, commit_timeout)
     val {fact_G} = mash_get ctxt
     val (old_facts, new_facts) =
-      facts |> filter_out fact_has_evil_theory
+      facts |> filter_out (is_thm_technical o snd)
             |> List.partition (is_fact_in_graph fact_G)
             ||> sort (thm_ord o pairself snd)
   in