# HG changeset patch
# User noschinl
# Date 1429260597 -7200
# Node ID d7fe3e0aca8525acf98ac9fe2c5eeca4ddc9408e
# Parent  0a064330a885b8681884b14460fa2e1a3749da1f
rewrite: add default pattern "in concl" for more cases

diff -r 0a064330a885 -r d7fe3e0aca85 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Fri Apr 17 10:49:57 2015 +0200
@@ -406,6 +406,8 @@
 
         fun append_default [] = [Concl, In]
           | append_default (ps as Term _ :: _) = Concl :: In :: ps
+          | append_default [For x, In] = [For x, Concl, In]
+          | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
           | append_default ps = ps
 
       in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
diff -r 0a064330a885 -r d7fe3e0aca85 src/HOL/ex/Rewrite_Examples.thy
--- a/src/HOL/ex/Rewrite_Examples.thy	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy	Fri Apr 17 10:49:57 2015 +0200
@@ -179,19 +179,29 @@
 lemma
   assumes "\<And>x y z. y + x + z = z + y + (x::int)"
   shows   "\<And>x y z. x + y + z = z + y + (x::int)"
-by (rewrite at "x + y" in "x + y + z" in concl at for (x y z) add.commute) fact
+by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact
 
 lemma
   assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
   shows   "\<And>x y z. x + y + z = z + y + (x::int)"
-by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact
+by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact
 
 lemma
   assumes "\<And>x y z. x + y + z = y + z + (x::int)"
   shows   "\<And>x y z. x + y + z = z + y + (x::int)"
-by (rewrite at "\<hole> + _" at "_ = \<hole>" in concl at for () add.commute) fact
+by (rewrite at "\<hole> + _" at "_ = \<hole>" in for () add.commute) fact
 
-(* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
+lemma
+  assumes eq: "\<And>x. P x \<Longrightarrow> g x = x"
+  assumes f1: "\<And>x. Q x \<Longrightarrow> P x"
+  assumes f2: "\<And>x. Q x \<Longrightarrow> x"
+  shows "\<And>x. Q x \<Longrightarrow> g x"
+  apply (rewrite at "g x" in for (x) eq)
+  apply (fact f1)
+  apply (fact f2)
+  done
+
+(* The for keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
 lemma
   assumes "(\<And>(x::int). x < 1 + x)"
   and     "(x::int) + 1 > x"