# HG changeset patch
# User blanchet
# Date 1435614293 -7200
# Node ID 79d71bfea3105ce0925fbebf299a4f25f6dabd30
# Parent  27255d1fbe1a377e10d682c73731e8e5081bb244
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs

diff -r 27255d1fbe1a -r 79d71bfea310 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jun 29 21:56:20 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jun 29 23:44:53 2015 +0200
@@ -8,6 +8,7 @@
 
 signature SLEDGEHAMMER =
 sig
+  type stature = ATP_Problem_Generate.stature
   type fact = Sledgehammer_Fact.fact
   type fact_override = Sledgehammer_Fact.fact_override
   type proof_method = Sledgehammer_Proof_Methods.proof_method
@@ -20,8 +21,8 @@
   val timeoutN : string
   val unknownN : string
 
-  val play_one_line_proof : bool -> Time.time -> (string * 'a) list -> Proof.state -> int ->
-    proof_method * proof_method list list -> (string * 'a) list * (proof_method * play_outcome)
+  val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int ->
+    proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome)
   val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
     Proof.state -> bool * (string * string list)
@@ -71,48 +72,50 @@
     t $ Abs (s, T, add_chained chained u)
   | add_chained chained t = Logic.list_implies (chained, t)
 
-fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) =
-  if timeout = Time.zeroTime then
-    (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
-  else
-    let
-      val ctxt = Proof.context_of state
+fun play_one_line_proof minimize timeout used_facts0 state i (preferred_meth, methss) =
+  let val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts0 in
+    if timeout = Time.zeroTime then
+      (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
+    else
+      let
+        val ctxt = Proof.context_of state
 
-      val fact_names = map fst used_facts
-      val {facts = chained, goal, ...} = Proof.goal state
-      val goal_t = Logic.get_goal (Thm.prop_of goal) i
-        |> add_chained (map Thm.prop_of chained)
+        val fact_names = map fst used_facts
+        val {facts = chained, goal, ...} = Proof.goal state
+        val goal_t = Logic.get_goal (Thm.prop_of goal) i
+          |> add_chained (map Thm.prop_of chained)
 
-      fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
-        | try_methss ress [] =
-          (used_facts,
-           (case AList.lookup (op =) ress preferred_meth of
-             SOME play => (preferred_meth, play)
-           | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
-        | try_methss ress (meths :: methss) =
-          let
-            fun mk_step fact_names meths =
-              Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
-          in
-            (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of
-              (res as (meth, Played time)) :: _ =>
-              (* if a fact is needed by an ATP, it will be needed by "metis" *)
-              if not minimize orelse is_metis_method meth then
-                (used_facts, res)
-              else
-                let
-                  val (time', used_names') =
-                    minimized_isar_step ctxt time (mk_step fact_names [meth])
-                    ||> (facts_of_isar_step #> snd)
-                  val used_facts' = filter (member (op =) used_names' o fst) used_facts
-                in
-                  (used_facts', (meth, Played time'))
-                end
-            | ress' => try_methss (ress' @ ress) methss)
-          end
-    in
-      try_methss [] methss
-    end
+        fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
+          | try_methss ress [] =
+            (used_facts,
+             (case AList.lookup (op =) ress preferred_meth of
+               SOME play => (preferred_meth, play)
+             | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
+          | try_methss ress (meths :: methss) =
+            let
+              fun mk_step fact_names meths =
+                Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
+            in
+              (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of
+                (res as (meth, Played time)) :: _ =>
+                (* if a fact is needed by an ATP, it will be needed by "metis" *)
+                if not minimize orelse is_metis_method meth then
+                  (used_facts, res)
+                else
+                  let
+                    val (time', used_names') =
+                      minimized_isar_step ctxt time (mk_step fact_names [meth])
+                      ||> (facts_of_isar_step #> snd)
+                    val used_facts' = filter (member (op =) used_names' o fst) used_facts
+                  in
+                    (used_facts', (meth, Played time'))
+                  end
+              | ress' => try_methss (ress' @ ress) methss)
+            end
+      in
+        try_methss [] methss
+      end
+  end
 
 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout,
       preplay_timeout, expect, ...}) mode output_result only learn
diff -r 27255d1fbe1a -r 79d71bfea310 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 29 21:56:20 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 29 23:44:53 2015 +0200
@@ -147,7 +147,7 @@
 val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
 val skolem_methods = Moura_Method :: systematic_methods
 
-fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
+fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
     (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
   let
     val _ = if debug then writeln "Constructing Isar proof..." else ()
@@ -407,20 +407,23 @@
                #> relabel_isar_proof_nicely
                #> rationalize_obtains_in_isar_proofs ctxt)
       in
-        (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
-          1 =>
+        (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
+          (0, 1) =>
           one_line_proof_text ctxt 0
             (if play_outcome_ord (play_outcome, one_line_play) = LESS then
                (case isar_proof of
                  Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
-                 let val used_facts' = filter (member (op =) gfs o fst) used_facts in
+                 let
+                   val used_facts' = filter (fn (s, (sc, _)) =>
+                     member (op =) gfs s andalso sc <> Chained) used_facts
+                 in
                    ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
                  end)
              else
                one_line_params) ^
           (if isar_proofs = SOME true then "\n(No Isar proof available.)"
            else "")
-        | num_steps =>
+        | (_, num_steps) =>
           let
             val msg =
               (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @
@@ -453,7 +456,7 @@
     (one_line_params as ((_, preplay), _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
-     isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
+     isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
    else
      one_line_proof_text ctxt num_chained) one_line_params