noschinl@59739: theory Rewrite_Examples
noschinl@59739: imports Main "~~/src/HOL/Library/Rewrite"
noschinl@59739: begin
noschinl@59739:
noschinl@59739: section \The rewrite Proof Method by Example\
noschinl@59739:
noschinl@59739: (* This file is intended to give an overview over
noschinl@59739: the features of the pattern-based rewrite proof method.
noschinl@59739:
noschinl@59739: See also https://www21.in.tum.de/~noschinl/Pattern-2014/
noschinl@59739: *)
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: fixes a::int and b::int and c::int
noschinl@59739: assumes "P (b + a)"
noschinl@59739: shows "P (a + b)"
noschinl@59739: by (rewrite at "a + b" add.commute)
noschinl@59739: (rule assms)
noschinl@59739:
noschinl@59739: (* Selecting a specific subterm in a large, ambiguous term. *)
noschinl@59739: lemma
noschinl@59739: fixes a b c :: int
noschinl@59739: assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c"
noschinl@59739: shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047: by (rewrite in "f _ + f \ = _" diff_self) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: fixes a b c :: int
noschinl@59739: assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
noschinl@59739: shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047: by (rewrite at "f (_ + \) + f _ = _" diff_self) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: fixes a b c :: int
noschinl@59739: assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@59739: shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047: by (rewrite in "f (\ + _) + _ = _" diff_self) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: fixes a b c :: int
noschinl@59739: assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
noschinl@59739: shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047: by (rewrite in "f (_ + \) + _ = _" diff_self) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: fixes x y :: nat
noschinl@59739: shows"x + y > c \ y + x > c"
noschinl@60047: by (rewrite at "\ > c" add.commute) assumption
noschinl@59739:
noschinl@59739: (* We can also rewrite in the assumptions. *)
noschinl@59739: lemma
noschinl@59739: fixes x y :: nat
noschinl@59739: assumes "y + x > c \ y + x > c"
noschinl@59739: shows "x + y > c \ y + x > c"
noschinl@59739: by (rewrite in asm add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: fixes x y :: nat
noschinl@59739: assumes "y + x > c \ y + x > c"
noschinl@59739: shows "x + y > c \ y + x > c"
noschinl@59739: by (rewrite in "x + y > c" at asm add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: fixes x y :: nat
noschinl@59739: assumes "y + x > c \ y + x > c"
noschinl@59739: shows "x + y > c \ y + x > c"
noschinl@60047: by (rewrite at "\ > c" at asm add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: assumes "P {x::int. y + 1 = 1 + x}"
noschinl@59739: shows "P {x::int. y + 1 = x + 1}"
noschinl@60047: by (rewrite at "x+1" in "{x::int. \ }" add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: assumes "P {x::int. y + 1 = 1 + x}"
noschinl@59739: shows "P {x::int. y + 1 = x + 1}"
noschinl@60047: by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \ }" add.commute)
noschinl@59739: fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. s * t + y - 3)}"
noschinl@59739: shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. y + s * t - 3)}"
noschinl@60047: by (rewrite at "b + d * e" in "\(a, b, c). _ = Q (\d e. \)" add.commute) fact
noschinl@59739:
noschinl@59739:
noschinl@59739: (* Rewriting with conditional rewriting rules works just as well. *)
noschinl@59739: lemma test_theorem:
noschinl@59739: fixes x :: nat
noschinl@59739: shows "x \ y \ x \ y \ x = y"
noschinl@59739: by (rule Orderings.order_antisym)
noschinl@59739:
noschinl@60050: (* Premises of the conditional rule yield new subgoals. The
noschinl@60050: assumptions of the goal are propagated into these subgoals
noschinl@60050: *)
noschinl@59739: lemma
noschinl@60050: fixes f :: "nat \ nat"
noschinl@60050: shows "f x \ 0 \ f x \ 0 \ f x = 0"
noschinl@59739: apply (rewrite at "f x" to "0" test_theorem)
noschinl@60050: apply assumption
noschinl@60050: apply assumption
noschinl@59739: apply (rule refl)
noschinl@60050: done
noschinl@59739:
noschinl@59739: (*
noschinl@59739: Instantiation.
noschinl@59739:
noschinl@59739: Since all rewriting is now done via conversions,
noschinl@59739: instantiation becomes fairly easy to do.
noschinl@59739: *)
noschinl@59739:
noschinl@59739: (* We first introduce a function f and an extended
noschinl@59739: version of f that is annotated with an invariant. *)
noschinl@59739: fun f :: "nat \ nat" where "f n = n"
noschinl@59739: definition "f_inv (I :: nat \ bool) n \ f n"
noschinl@59739:
noschinl@59739: lemma annotate_f: "f = f_inv I"
noschinl@59739: by (simp add: f_inv_def fun_eq_iff)
noschinl@59739:
noschinl@59739: (* We have a lemma with a bound variable n, and
noschinl@59739: want to add an invariant to f. *)
noschinl@59739: lemma
noschinl@59739: assumes "P (\n. f_inv (\_. True) n + 1) = x"
noschinl@59739: shows "P (\n. f n + 1) = x"
noschinl@59739: by (rewrite to "f_inv (\_. True)" annotate_f) fact
noschinl@59739:
noschinl@59739: (* We can also add an invariant that contains the variable n bound in the outer context.
noschinl@59739: For this, we need to bind this variable to an identifier. *)
noschinl@59739: lemma
noschinl@59739: assumes "P (\n. f_inv (\x. n < x + 1) n + 1) = x"
noschinl@59739: shows "P (\n. f n + 1) = x"
noschinl@60047: by (rewrite in "\n. \" to "f_inv (\x. n < x + 1)" annotate_f) fact
noschinl@59739:
noschinl@59739: (* Any identifier will work *)
noschinl@59739: lemma
noschinl@59739: assumes "P (\n. f_inv (\x. n < x + 1) n + 1) = x"
noschinl@59739: shows "P (\n. f n + 1) = x"
noschinl@60047: by (rewrite in "\abc. \" to "f_inv (\x. abc < x + 1)" annotate_f) fact
noschinl@59739:
noschinl@59739: (* The "for" keyword. *)
noschinl@59739: lemma
noschinl@59739: assumes "P (2 + 1)"
noschinl@59739: shows "\x y. P (1 + 2 :: nat)"
noschinl@59739: by (rewrite in "P (1 + 2)" at for (x) add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: assumes "\x y. P (y + x)"
noschinl@59739: shows "\x y. P (x + y :: nat)"
noschinl@59739: by (rewrite in "P (x + _)" at for (x y) add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: assumes "\x y z. y + x + z = z + y + (x::int)"
noschinl@59739: shows "\x y z. x + y + z = z + y + (x::int)"
noschinl@59739: by (rewrite at "x + y" in "x + y + z" in concl at for (x y z) add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: assumes "\x y z. z + (x + y) = z + y + (x::int)"
noschinl@59739: shows "\x y z. x + y + z = z + y + (x::int)"
noschinl@59739: by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact
noschinl@59739:
noschinl@59739: lemma
noschinl@59739: assumes "\x y z. x + y + z = y + z + (x::int)"
noschinl@59739: shows "\x y z. x + y + z = z + y + (x::int)"
noschinl@60047: by (rewrite at "\ + _" at "_ = \" in concl at for () add.commute) fact
noschinl@59739:
noschinl@59739: (* The all-keyword can be used anywhere in the pattern where there is an \-Quantifier. *)
noschinl@59739: lemma
noschinl@59739: assumes "(\(x::int). x < 1 + x)"
noschinl@59739: and "(x::int) + 1 > x"
noschinl@59739: shows "(\(x::int). x + 1 > x) \ (x::int) + 1 > x"
noschinl@59739: by (rewrite at "x + 1" in for (x) at asm add.commute)
noschinl@59739: (rule assms)
noschinl@59739:
noschinl@59739: end
noschinl@59739: