--- 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
--- 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"