# Theory Rewrite_Examples

```theory Rewrite_Examples
imports Main "HOL-Library.Rewrite"
begin

section ‹The rewrite Proof Method by Example›

(* This file is intended to give an overview over
the features of the pattern-based rewrite proof method.

*)
lemma
fixes a::int and b::int and c::int
assumes "P (b + a)"
shows "P (a + b)"
by (rewrite at "a + b" add.commute)
(rule assms)

(* Selecting a specific subterm in a large, ambiguous term. *)
lemma
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

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

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

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

lemma
fixes x y :: nat
shows"x + y > c ⟹ y + x > c"
by (rewrite at "⌑ > c" add.commute) assumption

(* We can also rewrite in the assumptions.  *)
lemma
fixes x y :: nat
assumes "y + x > c ⟹ y + x > c"
shows   "x + y > c ⟹ y + x > c"
by (rewrite in asm add.commute) fact

lemma
fixes x y :: nat
assumes "y + x > c ⟹ y + x > c"
shows   "x + y > c ⟹ y + x > c"
by (rewrite in "x + y > c" at asm add.commute) fact

lemma
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

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

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)
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

(* This is not limited to the first assumption *)
lemma
assumes "PROP P ≡ PROP Q"
shows "PROP R ⟹ PROP P ⟹ PROP Q"
by (rewrite at asm assms)

lemma
assumes "PROP P ≡ PROP Q"
shows "PROP R ⟹ PROP R ⟹ PROP P ⟹ PROP Q"
by (rewrite at asm assms)

(* Rewriting "at asm" selects each full assumption, not any parts *)
lemma
assumes "(PROP P ⟹ PROP Q) ≡ (PROP S ⟹ PROP R)"
shows "PROP S ⟹ (PROP P ⟹ PROP Q) ⟹ PROP R"
apply (rewrite at asm assms)
apply assumption
done

(* Rewriting with conditional rewriting rules works just as well. *)
lemma test_theorem:
fixes x :: nat
shows "x ≤ y ⟹ x ≥ y ⟹ x = y"
by (rule Orderings.order_antisym)

(* Premises of the conditional rule yield new subgoals. The
assumptions of the goal are propagated into these subgoals
*)
lemma
fixes f :: "nat ⇒ nat"
shows "f x ≤ 0 ⟹ f x ≥ 0 ⟹ f x = 0"
apply (rewrite at "f x" to "0" test_theorem)
apply assumption
apply assumption
apply (rule refl)
done

(* This holds also for rewriting in assumptions. The order of assumptions is preserved *)
lemma
assumes rewr: "PROP P ⟹ PROP Q ⟹ PROP R ≡ PROP R'"
assumes A1: "PROP S ⟹ PROP T ⟹ PROP U ⟹ PROP P"
assumes A2: "PROP S ⟹ PROP T ⟹ PROP U ⟹ PROP Q"
assumes C: "PROP S ⟹ PROP R' ⟹ PROP T ⟹ PROP U ⟹ PROP V"
shows "PROP S ⟹ PROP R ⟹ PROP T ⟹ PROP U ⟹ PROP V"
apply (rewrite at asm rewr)
apply (fact A1)
apply (fact A2)
apply (fact C)
done

(*
Instantiation.

Since all rewriting is now done via conversions,
instantiation becomes fairly easy to do.
*)

(* We first introduce a function f and an extended
version of f that is annotated with an invariant. *)
fun f :: "nat ⇒ nat" where "f n = n"
definition "f_inv (I :: nat ⇒ bool) n ≡ f n"

lemma annotate_f: "f = f_inv I"
by (simp add: f_inv_def fun_eq_iff)

(* We have a lemma with a bound variable n, and
want to add an invariant to f. *)
lemma
assumes "P (λn. f_inv (λ_. True) n + 1) = x"
shows "P (λn. f n + 1) = x"
by (rewrite to "f_inv (λ_. True)" annotate_f) fact

(* We can also add an invariant that contains the variable n bound in the outer context.
For this, we need to bind this variable to an identifier. *)
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

(* 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

(* The "for" keyword. *)
lemma
assumes "P (2 + 1)"
shows "⋀x y. P (1 + 2 :: nat)"
by (rewrite in "P (1 + 2)" at for (x) add.commute) fact

lemma
assumes "⋀x y. P (y + x)"
shows "⋀x y. P (x + y :: nat)"
by (rewrite in "P (x + _)" at for (x y) add.commute) fact

lemma
assumes "⋀x y z. y + x + z = z + y + (x::int)"
shows   "⋀x y z. x + y + z = z + y + (x::int)"
by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact

lemma
assumes "⋀x y z. z + (x + y) = z + y + (x::int)"
shows   "⋀x y z. x + y + z = z + y + (x::int)"
by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact

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 for () add.commute) fact

lemma
assumes eq: "⋀x. P x ⟹ g x = x"
assumes f1: "⋀x. Q x ⟹ P x"
assumes f2: "⋀x. Q x ⟹ x"
shows "⋀x. Q x ⟹ g x"
apply (rewrite at "g x" in for (x) eq)
apply (fact f1)
apply (fact f2)
done

(* The for keyword can be used anywhere in the pattern where there is an ⋀-Quantifier. *)
lemma
assumes "(⋀(x::int). x < 1 + x)"
and     "(x::int) + 1 > x"
shows   "(⋀(x::int). x + 1 > x) ⟹ (x::int) + 1 > x"
by (rewrite at "x + 1" in for (x) at asm add.commute)
(rule assms)

(* The rewrite method also has an ML interface *)
lemma
assumes "⋀a b. P ((a + 1) * (1 + b)) "
shows "⋀a b :: nat. P ((a + 1) * (b + 1))"
apply (tactic ‹
let
val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
(* Note that the pattern order is reversed *)
val pat = [
Rewrite.For [(x, SOME \<^Type>‹nat›)],
Rewrite.In,
Rewrite.Term (\<^Const>‹plus \<^Type>‹nat› for ‹Free (x, \<^Type>‹nat›)› \<^term>‹1 :: nat››, [])]
val to = NONE
in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
›)
apply (fact assms)
done

lemma
assumes "Q (λb :: int. P (λa. a + b) (λa. a + b))"
shows "Q (λb :: int. P (λa. a + b) (λa. b + a))"
apply (tactic ‹
let
val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
val pat = [
Rewrite.Concl,
Rewrite.In,
Rewrite.Term (Free ("Q", (\<^Type>‹int› --> TVar (("'b",0), [])) --> \<^Type>‹bool›)
\$ Abs ("x", \<^Type>‹int›, Rewrite.mk_hole 1 (\<^Type>‹int› --> TVar (("'b",0), [])) \$ Bound 0), [(x, \<^Type>‹int›)]),
Rewrite.In,
Rewrite.Term (\<^Const>‹plus \<^Type>‹int› for ‹Free (x, \<^Type>‹int›)› ‹Var (("c", 0), \<^Type>‹int›)››, [])
]
val to = NONE
in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
›)
apply (fact assms)
done

(* There is also conversion-like rewrite function: *)
ML ‹
val ct = \<^cprop>‹Q (λb :: int. P (λa. a + b) (λa. b + a))›
val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
val pat = [
Rewrite.Concl,
Rewrite.In,
Rewrite.Term (Free ("Q", (\<^typ>‹int› --> TVar (("'b",0), [])) --> \<^typ>‹bool›)
\$ Abs ("x", \<^typ>‹int›, Rewrite.mk_hole 1 (\<^typ>‹int› --> TVar (("'b",0), [])) \$ Bound 0), [(x, \<^typ>‹int›)]),
Rewrite.In,
Rewrite.Term (\<^Const>‹plus \<^Type>‹int› for ‹Free (x, \<^Type>‹int›)› ‹Var (("c", 0), \<^Type>‹int›)››, [])
]
val to = NONE
val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
›

section ‹Regression tests›

ML ‹
val ct = \<^cterm>‹(λb :: int. (λa. b + a))›
val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
val pat = [
Rewrite.In,
Rewrite.Term (\<^Const>‹plus \<^Type>‹int› for ‹Var (("c", 0), \<^Type>‹int›)› ‹Var (("c", 0), \<^Type>‹int›)››, [])
]
val to = NONE
val _ =
case try (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) ct of
NONE => ()
| _ => error "should not have matched anything"
›

ML ‹
Rewrite.params_pconv (Conv.all_conv |> K |> K) \<^context> (Vartab.empty, []) \<^cterm>‹⋀x. PROP A›
›

lemma
assumes eq: "PROP A ⟹ PROP B ≡ PROP C"
assumes f1: "PROP D ⟹ PROP A"
assumes f2: "PROP D ⟹ PROP C"
shows "⋀x. PROP D ⟹ PROP B"
apply (rewrite eq)
apply (fact f1)
apply (fact f2)
done

end
```