src/HOL/ex/Rewrite_Examples.thy
 changeset 60047 58e5b16cbd94 parent 59739 4ed50ebf5d36 child 60050 dc6ac152d864
```     1.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 00:59:17 2015 +0200
1.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 10:21:35 2015 +0200
1.3 @@ -22,30 +22,30 @@
1.4    fixes a b c :: int
1.5    assumes "f (a - a + (a - a)) + f (   0    + c) = f 0 + f c"
1.6    shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
1.7 -  by (rewrite in "f _ + f \<box> = _" diff_self) fact
1.8 +  by (rewrite in "f _ + f \<hole> = _" diff_self) fact
1.9
1.10  lemma
1.11    fixes a b c :: int
1.12    assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
1.13    shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
1.14 -  by (rewrite at "f (_ + \<box>) + f _ = _" diff_self) fact
1.15 +  by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact
1.16
1.17  lemma
1.18    fixes a b c :: int
1.19    assumes "f (  0   + (a - a)) + f ((a - a) + c) = f 0 + f c"
1.20    shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
1.21 -  by (rewrite in "f (\<box> + _) + _ = _" diff_self) fact
1.22 +  by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact
1.23
1.24  lemma
1.25    fixes a b c :: int
1.26    assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
1.27    shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
1.28 -  by (rewrite in "f (_ + \<box>) + _ = _" diff_self) fact
1.29 +  by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact
1.30
1.31  lemma
1.32    fixes x y :: nat
1.33    shows"x + y > c \<Longrightarrow> y + x > c"
1.34 -  by (rewrite at "\<box> > c" add.commute) assumption
1.35 +  by (rewrite at "\<hole> > c" add.commute) assumption
1.36
1.37  (* We can also rewrite in the assumptions.  *)
1.38  lemma
1.39 @@ -64,23 +64,23 @@
1.40    fixes x y :: nat
1.41    assumes "y + x > c \<Longrightarrow> y + x > c"
1.42    shows   "x + y > c \<Longrightarrow> y + x > c"
1.43 -  by (rewrite at "\<box> > c" at asm  add.commute) fact
1.44 +  by (rewrite at "\<hole> > c" at asm  add.commute) fact
1.45
1.46  lemma
1.47    assumes "P {x::int. y + 1 = 1 + x}"
1.48    shows   "P {x::int. y + 1 = x + 1}"
1.49 -  by (rewrite at "x+1" in "{x::int. \<box> }" add.commute) fact
1.50 +  by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact
1.51
1.52  lemma
1.53    assumes "P {x::int. y + 1 = 1 + x}"
1.54    shows   "P {x::int. y + 1 = x + 1}"
1.55 -  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<box> }" add.commute)
1.56 +  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute)
1.57     fact
1.58
1.59  lemma
1.60    assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
1.61    shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
1.62 -  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<box>)" add.commute) fact
1.63 +  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
1.64
1.65
1.66  (* Rewriting with conditional rewriting rules works just as well. *)
1.67 @@ -126,13 +126,13 @@
1.68  lemma
1.69    assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
1.70    shows "P (\<lambda>n. f n + 1) = x"
1.71 -  by (rewrite in "\<lambda>n. \<box>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
1.72 +  by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
1.73
1.74  (* Any identifier will work *)
1.75  lemma
1.76    assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
1.77    shows "P (\<lambda>n. f n + 1) = x"
1.78 -  by (rewrite in "\<lambda>abc. \<box>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
1.79 +  by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
1.80
1.81  (* The "for" keyword. *)
1.82  lemma
1.83 @@ -158,7 +158,7 @@
1.84  lemma
1.85    assumes "\<And>x y z. x + y + z = y + z + (x::int)"
1.86    shows   "\<And>x y z. x + y + z = z + y + (x::int)"
1.87 -by (rewrite at "\<box> + _" at "_ = \<box>" in concl at for () add.commute) fact
1.88 +by (rewrite at "\<hole> + _" at "_ = \<hole>" in concl at for () add.commute) fact
1.89
1.90  (* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
1.91  lemma
```