theory Rewrite_Examples imports Main "HOL-Library.Rewrite" begin section ‹The rewrite Proof Method by Example› text‹ This theory gives an overview over the features of the pattern-based rewrite proof method. Documentation: 🌐‹https://arxiv.org/abs/2111.04082› › 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 › text ‹Some 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