rewrite: add default pattern "in concl" for more cases
authornoschinl
Fri Apr 17 10:49:57 2015 +0200 (2015-04-17)
changeset 60108d7fe3e0aca85
parent 60088 0a064330a885
child 60109 22389d4cdd6b
rewrite: add default pattern "in concl" for more cases
src/HOL/Library/rewrite.ML
src/HOL/ex/Rewrite_Examples.thy
     1.1 --- a/src/HOL/Library/rewrite.ML	Thu Apr 16 15:55:55 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Fri Apr 17 10:49:57 2015 +0200
     1.3 @@ -406,6 +406,8 @@
     1.4  
     1.5          fun append_default [] = [Concl, In]
     1.6            | append_default (ps as Term _ :: _) = Concl :: In :: ps
     1.7 +          | append_default [For x, In] = [For x, Concl, In]
     1.8 +          | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
     1.9            | append_default ps = ps
    1.10  
    1.11        in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
     2.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Thu Apr 16 15:55:55 2015 +0200
     2.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Fri Apr 17 10:49:57 2015 +0200
     2.3 @@ -179,19 +179,29 @@
     2.4  lemma
     2.5    assumes "\<And>x y z. y + x + z = z + y + (x::int)"
     2.6    shows   "\<And>x y z. x + y + z = z + y + (x::int)"
     2.7 -by (rewrite at "x + y" in "x + y + z" in concl at for (x y z) add.commute) fact
     2.8 +by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact
     2.9  
    2.10  lemma
    2.11    assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
    2.12    shows   "\<And>x y z. x + y + z = z + y + (x::int)"
    2.13 -by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact
    2.14 +by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact
    2.15  
    2.16  lemma
    2.17    assumes "\<And>x y z. x + y + z = y + z + (x::int)"
    2.18    shows   "\<And>x y z. x + y + z = z + y + (x::int)"
    2.19 -by (rewrite at "\<hole> + _" at "_ = \<hole>" in concl at for () add.commute) fact
    2.20 +by (rewrite at "\<hole> + _" at "_ = \<hole>" in for () add.commute) fact
    2.21  
    2.22 -(* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
    2.23 +lemma
    2.24 +  assumes eq: "\<And>x. P x \<Longrightarrow> g x = x"
    2.25 +  assumes f1: "\<And>x. Q x \<Longrightarrow> P x"
    2.26 +  assumes f2: "\<And>x. Q x \<Longrightarrow> x"
    2.27 +  shows "\<And>x. Q x \<Longrightarrow> g x"
    2.28 +  apply (rewrite at "g x" in for (x) eq)
    2.29 +  apply (fact f1)
    2.30 +  apply (fact f2)
    2.31 +  done
    2.32 +
    2.33 +(* The for keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
    2.34  lemma
    2.35    assumes "(\<And>(x::int). x < 1 + x)"
    2.36    and     "(x::int) + 1 > x"