# HG changeset patch # User noschinl # Date 1428913295 -7200 # Node ID 58e5b16cbd9450aeb26bcaa48924805c4b8fbce4 # Parent 7ff7fdfbb9a079134c21fbdff96d3b7824b554d4 enable \ syntax for rewrite diff -r 7ff7fdfbb9a0 -r 58e5b16cbd94 src/HOL/Library/Rewrite.thy --- a/src/HOL/Library/Rewrite.thy Mon Apr 13 00:59:17 2015 +0200 +++ b/src/HOL/Library/Rewrite.thy Mon Apr 13 10:21:35 2015 +0200 @@ -10,7 +10,7 @@ consts rewrite_HOLE :: "'a::{}" notation rewrite_HOLE ("HOLE") -notation rewrite_HOLE ("\") +notation rewrite_HOLE ("\") lemma eta_expand: fixes f :: "'a::{} \ 'b::{}" diff -r 7ff7fdfbb9a0 -r 58e5b16cbd94 src/HOL/ex/Rewrite_Examples.thy --- a/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 00:59:17 2015 +0200 +++ b/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 10:21:35 2015 +0200 @@ -22,30 +22,30 @@ fixes a b c :: int assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c" shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" - by (rewrite in "f _ + f \ = _" diff_self) fact + by (rewrite in "f _ + f \ = _" diff_self) fact lemma fixes a b c :: int assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" - by (rewrite at "f (_ + \) + f _ = _" diff_self) fact + by (rewrite at "f (_ + \) + f _ = _" diff_self) fact lemma fixes a b c :: int assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c" shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" - by (rewrite in "f (\ + _) + _ = _" diff_self) fact + by (rewrite in "f (\ + _) + _ = _" diff_self) fact lemma fixes a b c :: int assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" - by (rewrite in "f (_ + \) + _ = _" diff_self) fact + by (rewrite in "f (_ + \) + _ = _" diff_self) fact lemma fixes x y :: nat shows"x + y > c \ y + x > c" - by (rewrite at "\ > c" add.commute) assumption + by (rewrite at "\ > c" add.commute) assumption (* We can also rewrite in the assumptions. *) lemma @@ -64,23 +64,23 @@ fixes x y :: nat assumes "y + x > c \ y + x > c" shows "x + y > c \ y + x > c" - by (rewrite at "\ > c" at asm add.commute) fact + by (rewrite at "\ > c" at asm add.commute) fact lemma assumes "P {x::int. y + 1 = 1 + x}" shows "P {x::int. y + 1 = x + 1}" - by (rewrite at "x+1" in "{x::int. \ }" add.commute) fact + by (rewrite at "x+1" in "{x::int. \ }" add.commute) fact lemma assumes "P {x::int. y + 1 = 1 + x}" shows "P {x::int. y + 1 = x + 1}" - by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \ }" add.commute) + by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \ }" add.commute) fact lemma assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. s * t + y - 3)}" shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. y + s * t - 3)}" - by (rewrite at "b + d * e" in "\(a, b, c). _ = Q (\d e. \)" add.commute) fact + by (rewrite at "b + d * e" in "\(a, b, c). _ = Q (\d e. \)" add.commute) fact (* Rewriting with conditional rewriting rules works just as well. *) @@ -126,13 +126,13 @@ lemma assumes "P (\n. f_inv (\x. n < x + 1) n + 1) = x" shows "P (\n. f n + 1) = x" - by (rewrite in "\n. \" to "f_inv (\x. n < x + 1)" annotate_f) fact + by (rewrite in "\n. \" to "f_inv (\x. n < x + 1)" annotate_f) fact (* Any identifier will work *) lemma assumes "P (\n. f_inv (\x. n < x + 1) n + 1) = x" shows "P (\n. f n + 1) = x" - by (rewrite in "\abc. \" to "f_inv (\x. abc < x + 1)" annotate_f) fact + by (rewrite in "\abc. \" to "f_inv (\x. abc < x + 1)" annotate_f) fact (* The "for" keyword. *) lemma @@ -158,7 +158,7 @@ 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 concl at for () add.commute) fact (* The all-keyword can be used anywhere in the pattern where there is an \-Quantifier. *) lemma