# HG changeset patch
# User blanchet
# Date 1407223200 -7200
# Node ID 498b5b00f37feeac0c13ad06ffc305db0b2bdf29
# Parent  1f0efb4974fc0108f23d4a1ceb008da4894afc80
tuning

diff -r 1f0efb4974fc -r 498b5b00f37f src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Aug 04 16:55:03 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 05 09:20:00 2014 +0200
@@ -53,7 +53,7 @@
     int Symtab.table -> string atp_proof -> (term, string) atp_step list
   val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list
   val infer_formulas_types : Proof.context -> term list -> term list
-  val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
+  val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list
   val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
     (term, string) atp_step list
 end;
@@ -232,10 +232,6 @@
 
 fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT @{sort type}
 
-(* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
-fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
-  | loose_aconv (t, t') = t aconv t'
-
 val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
 val vampire_skolem_prefix = "sK"
 
@@ -251,7 +247,6 @@
       | norm_var_types t = t
   in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
 
-
 (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
    are typed. The code is similar to "term_of_atp_fo". *)
 fun term_of_atp_ho ctxt sym_tab =
@@ -685,58 +680,52 @@
     |> HOLogic.mk_Trueprop
   end
 
-fun introduce_spass_skolem [] = []
-  | introduce_spass_skolem (proof as (_, _, _, rule1, _) :: _) =
-    if rule1 = spass_input_rule then
-      let
-        fun add_sko (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
-          | add_sko _ = I
+fun introduce_spass_skolems proof =
+  let
+    fun add_sko (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
+      | add_sko _ = I
 
-        (* union-find would be faster *)
-        fun add_cycle [] = I
-          | add_cycle ss =
-            fold (fn s => Graph.default_node (s, ())) ss
-            #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss])
+    (* union-find would be faster *)
+    fun add_cycle [] = I
+      | add_cycle ss =
+        fold (fn s => Graph.default_node (s, ())) ss
+        #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss])
 
-        val (input_steps, other_steps) = List.partition (null o #5) proof
+    val (input_steps, other_steps) = List.partition (null o #5) proof
 
-        val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps
-        val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
-        val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty)
+    val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps
+    val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
+    val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty)
 
-        fun step_name_of_group skos = (implode skos, [])
-        fun in_group group = member (op =) group o hd
-        fun group_of sko = the (find_first (fn group => in_group group sko) groups)
+    fun step_name_of_group skos = (implode skos, [])
+    fun in_group group = member (op =) group o hd
+    fun group_of sko = the (find_first (fn group => in_group group sko) groups)
 
-        fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
-          let
-            val name = step_name_of_group group
-            val name0 = name |>> prefix "0"
-            val t =
-              skoss_steps
-              |> map (snd #> #3 #> HOLogic.dest_Trueprop)
-              |> Library.foldr1 s_conj
-              |> HOLogic.mk_Trueprop
-            val skos = fold (union (op =) o fst) skoss_steps []
-            val deps = map (snd #> #1) skoss_steps
-          in
-            [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
-             (name, Unknown, t, spass_skolemize_rule, [name0])]
-          end
+    fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
+      let
+        val name = step_name_of_group group
+        val name0 = name |>> prefix "0"
+        val t = skoss_steps
+          |> map (snd #> #3 #> HOLogic.dest_Trueprop)
+          |> Library.foldr1 s_conj
+          |> HOLogic.mk_Trueprop
+        val skos = fold (union (op =) o fst) skoss_steps []
+        val deps = map (snd #> #1) skoss_steps
+      in
+        [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
+         (name, Unknown, t, spass_skolemize_rule, [name0])]
+      end
 
-        val sko_steps =
-          maps (fn group => new_steps (filter (in_group group o fst) skoss_input_steps) group)
-            groups
+    val sko_steps =
+      maps (fn group => new_steps (filter (in_group group o fst) skoss_input_steps) group) groups
 
-        val old_news =
-          map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
-            skoss_input_steps
-        val repair_deps = fold replace_dependencies_in_line old_news
-      in
-        input_steps @ sko_steps @ map repair_deps other_steps
-      end
-  else
-    proof
+    val old_news =
+      map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
+        skoss_input_steps
+    val repair_deps = fold replace_dependencies_in_line old_news
+  in
+    input_steps @ sko_steps @ map repair_deps other_steps
+  end
 
 fun factify_atp_proof facts hyp_ts concl_t atp_proof =
   let
diff -r 1f0efb4974fc -r 498b5b00f37f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 04 16:55:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 05 09:20:00 2014 +0200
@@ -107,8 +107,7 @@
             Term.aconv_untyped (normalize prev_role prev_t, norm_t))
           res
 
-      fun looks_boring () =
-        t aconv @{prop True} orelse t aconv @{prop False} orelse length deps < 2
+      fun looks_boring () = t aconv @{prop False} orelse length deps < 2
 
       fun is_skolemizing_line (_, _, _, rule', deps') =
         is_skolemize_rule rule' andalso member (op =) deps' name
@@ -358,13 +357,6 @@
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
-          (* It's not clear whether this is worth the trouble (and if so, "compress" has an
-             unnatural semantics): *)
-(*
-          |> minimize
-               ? (compress_isar_proof ctxt compress preplay_timeout preplay_data
-                  #> tap (trace_isar_proof "Compressed again"))
-*)
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
diff -r 1f0efb4974fc -r 498b5b00f37f src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Aug 04 16:55:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Aug 05 09:20:00 2014 +0200
@@ -380,7 +380,7 @@
                     val atp_proof =
                       atp_proof
                       |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
-                      |> spass ? introduce_spass_skolem
+                      |> spass ? introduce_spass_skolems
                       |> factify_atp_proof (map fst used_from) hyp_ts concl_t
                   in
                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,