# HG changeset patch
# User noschinl
# Date 1428929560 -7200
# Node ID 616a176402297bc30e7eaa8561e0bee095c90472
# Parent  2a1cab4c9c9d6b667753de0b1d57c28b8d700d07
rewrite: with asm pattern, try all premises for rewriting, not only the first

diff -r 2a1cab4c9c9d -r 616a17640229 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Mon Apr 13 14:45:44 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 14:52:40 2015 +0200
@@ -253,14 +253,16 @@
             | SOME ft => SOME ft
       in desc eta_expands ft end
 
-    fun seq_unfold f ft =
-      case f ft of
-        NONE => Seq.empty
-      | SOME ft' => Seq.cons ft' (seq_unfold f ft')
+    fun move_assms ctxt (ft: focusterm) =
+      let
+        fun f () = case try (ft_assm ctxt) ft of
+            NONE => NONE
+          | SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft))
+      in Seq.make f end
 
     fun apply_pat At = Seq.map (ft_judgment ctxt)
       | apply_pat In = Seq.maps (valid_match_points ctxt)
-      | apply_pat Asm = Seq.maps (seq_unfold (try (ft_assm ctxt)) o ft_params ctxt)
+      | apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt)
       | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt)
       | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents)))
       | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))
diff -r 2a1cab4c9c9d -r 616a17640229 src/HOL/ex/Rewrite_Examples.thy
--- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 14:45:44 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 14:52:40 2015 +0200
@@ -82,6 +82,13 @@
   shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
   by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
 
+(* This is not limited to the first assumption *)
+lemma
+  assumes "PROP P \<equiv> PROP Q"
+  shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
+    by (rewrite at asm assms)
+
+
 
 (* Rewriting with conditional rewriting rules works just as well. *)
 lemma test_theorem: