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

section ‹The rewrite Proof Method by Example›

text‹
  theory gives an overview over the features of the pattern-based rewrite proof method.

 : 🌐‹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 \<And>-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 🚫‹nat›)],
        Rewrite.In,
        Rewrite.Term (Const‹plus 🚫‹nat› for ‹Free (x, 🚫‹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>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^Type>\<open>bool\<close>)
          $ Abs ("x", \<^Type>\<open>int\<close>, Rewrite.mk_hole 1 (\<^Type>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^Type>\<open>int\<close>)]),
        Rewrite.In,
        Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Free (x, \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
        ]
      val to = NONE
    in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
  \<close>)
  apply (fact assms)
  done

(* There is also conversion-like rewrite function: *)
ML ‹
 val ct = 🚫‹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 🚫‹int› for ‹Free (x, 🚫‹int›)› ‹Var (("c", 0), 🚫‹int›)››, [])
 ]
 val to = NONE
 val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
 ›

text ‹Some regression tests›

ML ‹
 val ct = 🚫‹(λb :: int. (λa. b + a))›
 val (x, ctxt) = yield_singleton Variable.add_fixes "x" context
 val pat = [
 Rewrite.In,
 Rewrite.Term (Const‹plus 🚫‹int› for ‹Var (("c", 0), 🚫‹int›)› ‹Var (("c", 0), ??‹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, []) 🚫‹∧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