# HG changeset patch
# User blanchet
# Date 1409249139 -7200
# Node ID 20e76da3a0efc722e7913416333b9c7ed9f91827
# Parent  f9e4a9621c759d5d8ca14b2c5c3b9f7a73931b93
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)

diff -r f9e4a9621c75 -r 20e76da3a0ef src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Aug 28 19:07:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Aug 28 20:05:39 2014 +0200
@@ -318,8 +318,24 @@
 
 fun hammer_away override_params subcommand opt_i fact_override state0 =
   let
+    (* We generally want chained facts to be picked up by the relevance filter, because it can then
+       give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
+       verbose output, machine learning). However, if the fact is available by no other means (not
+       even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice
+       but to insert it into the state as an additional hypothesis.
+    *)
+    val {facts = chained0, ...} = Proof.goal state0
+    val (inserts, keep_chained) =
+      if null chained0 orelse #only fact_override then
+        (chained0, [])
+      else
+        let val ctxt0 = Proof.context_of state0 in
+          List.partition (is_useful_unnamed_local_fact ctxt0) chained0
+        end
     val state = state0
+      |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained)
       |> Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
+
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
diff -r f9e4a9621c75 -r 20e76da3a0ef src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Aug 28 19:07:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Aug 28 20:05:39 2014 +0200
@@ -31,6 +31,7 @@
   val maybe_instantiate_inducts : Proof.context -> term list -> term ->
     (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
   val fact_of_raw_fact : raw_fact -> fact
+  val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
 
   val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list ->
     status Termtab.table -> raw_fact list
@@ -442,6 +443,18 @@
 
 fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
 
+fun is_useful_unnamed_local_fact ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val global_facts = Global_Theory.facts_of thy
+    val local_facts = Proof_Context.facts_of ctxt
+    val named_locals = Facts.dest_static true [global_facts] local_facts
+  in
+    fn th =>
+      not (Thm.has_name_hint th) andalso
+      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
+  end
+
 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -450,16 +463,13 @@
       if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false
       else is_too_complex
     val local_facts = Proof_Context.facts_of ctxt
-    val named_locals = local_facts |> Facts.dest_static true [global_facts]
     val assms = Assumption.all_assms_of ctxt
+    val named_locals = Facts.dest_static true [global_facts] local_facts
+    val unnamed_locals =
+      Facts.props local_facts
+      |> filter (is_useful_unnamed_local_fact ctxt)
+      |> map (pair "" o single)
 
-    fun is_good_unnamed_local th =
-      not (Thm.has_name_hint th) andalso
-      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
-
-    val unnamed_locals =
-      union Thm.eq_thm_prop (Facts.props local_facts) chained
-      |> filter is_good_unnamed_local |> map (pair "" o single)
     val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
     val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp