# HG changeset patch
# User blanchet
# Date 1283333762 -7200
# Node ID 504b9e1efd3302ad9f62b7fb6a9a7889d32a0e41
# Parent  542474156c661c2c3ed08dbc63e0aff049d64344
give priority to assumptions in structured proofs

diff -r 542474156c66 -r 504b9e1efd33 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 10:26:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 11:36:02 2010 +0200
@@ -5,7 +5,7 @@
 
 signature SLEDGEHAMMER_FILTER =
 sig
-  datatype locality = General | Intro | Elim | Simp | Local | Chained
+  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
   type relevance_override =
     {add: Facts.ref list,
@@ -24,6 +24,7 @@
   val elim_bonus : real Unsynchronized.ref
   val simp_bonus : real Unsynchronized.ref
   val local_bonus : real Unsynchronized.ref
+  val assum_bonus : real Unsynchronized.ref
   val chained_bonus : real Unsynchronized.ref
   val max_imperfect : real Unsynchronized.ref
   val max_imperfect_exp : real Unsynchronized.ref
@@ -50,7 +51,7 @@
 
 val respect_no_atp = true
 
-datatype locality = General | Intro | Elim | Simp | Local | Chained
+datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
 type relevance_override =
   {add: Facts.ref list,
@@ -331,6 +332,7 @@
 val elim_bonus = Unsynchronized.ref 0.15
 val simp_bonus = Unsynchronized.ref 0.15
 val local_bonus = Unsynchronized.ref 0.55
+val assum_bonus = Unsynchronized.ref 1.0
 val chained_bonus = Unsynchronized.ref 1.5
 
 fun locality_bonus General = 0.0
@@ -338,6 +340,7 @@
   | locality_bonus Elim = !elim_bonus
   | locality_bonus Simp = !simp_bonus
   | locality_bonus Local = !local_bonus
+  | locality_bonus Assum = !assum_bonus
   | locality_bonus Chained = !chained_bonus
 
 fun axiom_weight loc const_tab relevant_consts axiom_consts =
@@ -432,7 +435,8 @@
       fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
     val goal_const_tab =
       pconsts_in_terms thy false (SOME false) goal_ts
-      |> fold (if_empty_replace_with_locality thy axioms) [Chained, Local]
+      |> fold (if_empty_replace_with_locality thy axioms)
+              [Chained, Assum, Local]
     val add_thms = maps (ProofContext.get_fact ctxt) add
     val del_thms = maps (ProofContext.get_fact ctxt) del
     fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
@@ -690,6 +694,8 @@
     val global_facts = PureThy.facts_of thy
     val local_facts = ProofContext.facts_of ctxt
     val named_locals = local_facts |> Facts.dest_static []
+    val assms = Assumption.all_assms_of ctxt
+    fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
     val is_chained = member Thm.eq_thm chained_ths
     val (intros, elims, simps) =
       if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
@@ -750,11 +756,13 @@
                             end),
                       let val t = prop_of th in
                         if is_chained th then Chained
-                        else if not global then Local
-                        else if Termtab.defined intros t then Intro
-                        else if Termtab.defined elims t then Elim
-                        else if Termtab.defined simps t then Simp
-                        else General
+                        else if global then
+                          if Termtab.defined intros t then Intro
+                          else if Termtab.defined elims t then Elim
+                          else if Termtab.defined simps t then Simp
+                          else General
+                        else
+                          if is_assum th then Assum else Local
                       end),
                       (multi, th)) :: rest)) ths
             #> snd