# 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 "\x y z. y + x + z = z + y + (x::int)" shows "\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 "\x y z. z + (x + y) = z + y + (x::int)" shows "\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 "\x y z. x + y + z = y + z + (x::int)" shows "\x y z. x + y + z = z + y + (x::int)" -by (rewrite at "\ + _" at "_ = \" in concl at for () add.commute) fact +by (rewrite at "\ + _" at "_ = \" in for () add.commute) fact -(* The all-keyword can be used anywhere in the pattern where there is an \-Quantifier. *) +lemma + assumes eq: "\x. P x \ g x = x" + assumes f1: "\x. Q x \ P x" + assumes f2: "\x. Q x \ x" + shows "\x. Q x \ 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 \-Quantifier. *) lemma assumes "(\(x::int). x < 1 + x)" and "(x::int) + 1 > x"