correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs

--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 19:14:00 2014 +0200
@@ -8,8 +8,9 @@
 sig
   type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
 
-  val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> int list -> int ->
-    (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list
+  val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term ->
+    (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
+    (term, string) atp_step list
 end;
 
 structure Z3_New_Isar: Z3_NEW_ISAR =
@@ -83,15 +84,14 @@
   Term.map_abs_vars (perhaps (try Name.dest_skolem))
   #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
 
-fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof =
+fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_ts prem_ids conjecture_id fact_ids
+    proof =
   let
     val thy = Proof_Context.theory_of ctxt
 
     fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
       let
-        fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
-
-        val name as (sid, ss) = step_name_of id
+        val sid = string_of_int id
 
         val concl' =
           concl
@@ -102,22 +102,26 @@
           |> HOLogic.mk_Trueprop
 
         fun standard_step role =
-          (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
+          ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
+           map (fn id => (string_of_int id, [])) prems)
       in
         (case rule of
           Z3_New_Proof.Asserted =>
           let
+            val ss = the_list (AList.lookup (op =) fact_ids id)
             val name0 = (sid ^ "a", ss)
+
             val (role0, concl0) =
-              if not (null ss) then
-                (Axiom, concl(*FIXME*))
-              else if id = conjecture_id then
-                (Conjecture, concl_t)
-              else
-                (Hypothesis,
-                 (case find_index (curry (op =) id) prem_ids of
-                   ~1 => concl
-                 | i => nth hyp_ts i))
+              (case ss of
+                [s] => (Axiom, the (AList.lookup (op =) fact_ts s))
+              | _ =>
+                if id = conjecture_id then
+                  (Conjecture, concl_t)
+                else
+                  (Hypothesis,
+                   (case find_index (curry (op =) id) prem_ids of
+                     ~1 => concl
+                   | i => nth hyp_ts i)))
 
             val normalize_prems =
               SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
@@ -128,12 +132,9 @@
                 else
                   NONE)
           in
-            if null normalize_prems then
-              [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]
-            else
-              [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
-               (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
-                name0 :: normalize_prems)]
+            [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
+             ((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
+              name0 :: normalize_prems)]
           end
         | Z3_New_Proof.Rewrite => [standard_step Lemma]
         | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 16 19:14:00 2014 +0200
@@ -295,7 +295,7 @@
         fun str_of_preplay_outcome outcome =
           if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
         fun str_of_meth l meth =
-          string_of_proof_method [] meth ^ " " ^
+          string_of_proof_method ctxt [] meth ^ " " ^
           str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
         fun comment_of l = map (str_of_meth l) #> commas
 
@@ -355,7 +355,7 @@
           end)
       end
 
-    val one_line_proof = one_line_proof_text 0 one_line_params
+    val one_line_proof = one_line_proof_text ctxt 0 one_line_params
     val isar_proof =
       if debug then
         isar_proof_of ()
@@ -378,6 +378,6 @@
       (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
    else
-     one_line_proof_text num_chained) one_line_params
+     one_line_proof_text ctxt num_chained) one_line_params
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri May 16 19:14:00 2014 +0200
@@ -208,15 +208,15 @@
 
 val indent_size = 2
 
-fun string_of_isar_proof ctxt i n proof =
+fun string_of_isar_proof ctxt0 i n proof =
   let
     (* Make sure only type constraints inserted by the type annotation code are printed. *)
-    val ctxt =
-      ctxt |> Config.put show_markup false
-           |> Config.put Printer.show_type_emphasis false
-           |> Config.put show_types false
-           |> Config.put show_sorts false
-           |> Config.put show_consts false
+    val ctxt = ctxt0
+      |> Config.put show_markup false
+      |> Config.put Printer.show_type_emphasis false
+      |> Config.put show_types false
+      |> Config.put show_sorts false
+      |> Config.put show_consts false
 
     val register_fixes = map Free #> fold Variable.auto_fixes
 
@@ -264,7 +264,7 @@
     fun of_method ls ss meth =
       let val direct = is_direct_method meth in
         using_facts ls (if direct then [] else ss) ^
-        "by " ^ string_of_proof_method (if direct then ss else []) meth
+        "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
       end
 
     fun of_free (s, T) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri May 16 19:14:00 2014 +0200
@@ -33,12 +33,12 @@
   type one_line_params =
     (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
 
-  val string_of_proof_method : string list -> proof_method -> string
+  val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
     tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order
-  val one_line_proof_text : int -> one_line_params -> string
+  val one_line_proof_text : Proof.context -> int -> one_line_params -> string
 end;
 
 structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
@@ -74,7 +74,7 @@
 
 fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
 
-fun string_of_proof_method ss meth =
+fun string_of_proof_method ctxt ss meth =
   let
     val meth_s =
       (case meth of
@@ -86,7 +86,7 @@
       | SATx_Method => "satx"
       | Blast_Method => "blast"
       | Simp_Method => if null ss then "simp" else "simp add:"
-      | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
+      | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
       | Auto_Method => "auto"
       | Fastforce_Method => "fastforce"
       | Force_Method => "force"
@@ -141,8 +141,8 @@
     "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 (* FIXME *)
-fun proof_method_command meth i n _(*used_chaineds*) _(*num_chained*) ss =
-  apply_on_subgoal i n ^ string_of_proof_method ss meth
+fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
+  apply_on_subgoal i n ^ string_of_proof_method ctxt ss meth
 
 fun try_command_line banner play command =
   let val s = string_of_play_outcome play in
@@ -161,14 +161,14 @@
   |> List.partition (fn (_, (sc, _)) => sc = Chained)
   |> pairself (sort_distinct (string_ord o pairself fst))
 
-fun one_line_proof_text num_chained
+fun one_line_proof_text ctxt num_chained
     ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
   let
     val (chained, extra) = split_used_facts used_facts
 
     val try_line =
       map fst extra
-      |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
+      |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
       |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
           else try_command_line banner play)
   in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:14:00 2014 +0200
@@ -216,6 +216,8 @@
 
 fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
   let
+    val ctxt = Proof.context_of state
+
     fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   in
     if timeout = Time.zeroTime then
@@ -230,7 +232,7 @@
             let
               val _ =
                 if verbose then
-                  Output.urgent_message ("Trying \"" ^ string_of_proof_method [] meth ^
+                  Output.urgent_message ("Trying \"" ^ string_of_proof_method ctxt [] meth ^
                     "\" for " ^ string_of_time timeout ^ "...")
                 else
                   ()

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri May 16 19:14:00 2014 +0200
@@ -61,21 +61,22 @@
       else raise Fail ("unknown proof_method: " ^ quote name)
     val used_facts = facts |> map fst
   in
-    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
-        state subgoal meth [meth] of
+    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout
+        facts state subgoal meth [meth] of
       play as (_, Played time) =>
       {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
        preplay = Lazy.value play,
        message =
          fn play =>
             let
+              val ctxt = Proof.context_of state
               val (_, override_params) = extract_proof_method params meth
               val one_line_params =
                 (play, proof_banner mode name, used_facts, minimize_command override_params name,
                  subgoal, subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
             in
-              one_line_proof_text num_chained one_line_params
+              one_line_proof_text ctxt num_chained one_line_params
             end,
        message_tail = ""}
     | play =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 16 19:14:00 2014 +0200
@@ -243,7 +243,7 @@
                  subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
             in
-              one_line_proof_text num_chained one_line_params
+              one_line_proof_text ctxt num_chained one_line_params
             end,
          if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
       | SOME failure =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:14:00 2014 +0200
@@ -246,7 +246,8 @@
                 map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
                 map (fn (id, ((name, _), _)) => (id, name)) fact_ids
               val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
-                prem_ids conjecture_id fact_ids z3_proof
+                (map (fn ((s, _), th) => (s, prop_of th)) used_named_facts) prem_ids conjecture_id
+                fact_ids z3_proof
               val isar_params =
                 K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
                    minimize <> SOME false, atp_proof, goal)