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