Theory GHC_Rewrite_Rules

section ‹GHC's "fold/build" Rule›

theory GHC_Rewrite_Rules
  imports "../HOLCF_Prelude"
begin

subsection ‹Approximating the Rewrite Rule›

text ‹
  The original rule looks as follows (see also \<^cite>‹"ghc-rewriting"›):
  \begin{verbatim}
  "fold/build"
    forall k z (g :: forall b. (a -> b -> b) -> b -> b).
    foldr k z (build g) = g k z
  \end{verbatim}
  Since we do not have rank-2 polymorphic types in Isabelle/HOL, we try to imitate a similar
  statement by introducing a new type that combines possible folds with their argument lists, i.e.,
  @{term f} below is a function that, in a way, represents the list @{term xs}, but where list
  constructors are functionally abstracted.
›

abbreviation (input) abstract_list where
  "abstract_list xs ≡ (Λ c n. foldr⋅c⋅n⋅xs)"

cpodef ('a, 'b) listfun =
  "{(f :: ('a → 'b → 'b) → 'b → 'b, xs). f = abstract_list xs}"
  by auto

definition listfun :: "('a, 'b) listfun → ('a → 'b → 'b) → 'b → 'b" where
  "listfun = (Λ g. Product_Type.fst (Rep_listfun g))"

definition build :: "('a, 'b) listfun → ['a]" where
  "build = (Λ g. Product_Type.snd (Rep_listfun g))"

definition augment :: "('a, 'b) listfun → ['a] → ['a]" where
  "augment = (Λ g xs. build⋅g ++ xs)"

definition listfun_comp :: "('a, 'b) listfun → ('a, 'b) listfun → ('a, 'b) listfun" where
  "listfun_comp = (Λ g h.
    Abs_listfun (Λ c n. listfun⋅g⋅c⋅(listfun⋅h⋅c⋅n), build⋅g ++ build⋅h))"

abbreviation
  listfun_comp_infix :: "('a, 'b) listfun ⇒ ('a, 'b) listfun ⇒ ('a, 'b) listfun" (infixl ‹∘lf› 55)
  where
    "g ∘lf h ≡ listfun_comp⋅g⋅h"

fixrec mapFB :: "('b → 'c → 'c) → ('a → 'b) → 'a → 'c → 'c" where
  "mapFB⋅c⋅f = (Λ x ys. c⋅(f⋅x)⋅ys)"


subsection ‹Lemmas›

lemma cont_listfun_body [simp]:
  "cont (λg. Product_Type.fst (Rep_listfun g))"
  by (simp add: cont_Rep_listfun)

lemma cont_build_body [simp]:
  "cont (λg. Product_Type.snd (Rep_listfun g))"
  by (simp add: cont_Rep_listfun)

lemma build_Abs_listfun:
  assumes "abstract_list xs = f"
  shows "build⋅(Abs_listfun (f, xs)) = xs"
  using assms and Abs_listfun_inverse [of "(f, xs)"]
  by (simp add: build_def)

lemma listfun_Abs_listfun [simp]:
  assumes "abstract_list xs = f"
  shows "listfun⋅(Abs_listfun (f, xs)) = f"
  using assms and Abs_listfun_inverse [of "(f, xs)"]
  by (simp add: listfun_def)

lemma augment_Abs_listfun [simp]:
  assumes "abstract_list xs = f"
  shows "augment⋅(Abs_listfun (f, xs))⋅ys = xs ++ ys"
  using assms and Abs_listfun_inverse [of "(f, xs)"]
  by (simp add: augment_def build_Abs_listfun)

lemma cont_augment_body [simp]:
  "cont (λg. Abs_cfun ((++) (Product_Type.snd (Rep_listfun g))))"
  by (simp add: cont_Rep_listfun)

lemma "fold/build":
  fixes g :: "('a, 'b) listfun"
  shows "foldr⋅k⋅z⋅(build⋅g) = listfun⋅g⋅k⋅z"
proof -
  from Rep_listfun obtain f xs where
    "Rep_listfun g = (f, xs)" and "f = abstract_list xs" by blast
  then show ?thesis by (simp add: build_def listfun_def)
qed

lemma "foldr/augment":
  fixes g :: "('a, 'b) listfun"
  shows "foldr⋅k⋅z⋅(augment⋅g⋅xs) = listfun⋅g⋅k⋅(foldr⋅k⋅z⋅xs)"
proof -
  from Rep_listfun obtain f ys where
    "Rep_listfun g = (f, ys)" and "f = abstract_list ys" by blast
  then show ?thesis
    by (simp add: augment_def build_def listfun_def)
qed

lemma "foldr/id":
  "foldr⋅(:)⋅[] = (Λ x. x)"
proof (rule cfun_eqI)
  fix xs :: "['a]"
  show "foldr⋅(:)⋅[]⋅xs = (Λ x. x)⋅xs"
    by (induction xs) simp+
qed

lemma "foldr/app":
  "foldr⋅(:)⋅ys = (Λ xs. xs ++ ys)"
proof (rule cfun_eqI)
  fix xs :: "['a]"
  show "foldr⋅(:)⋅ys⋅xs = (Λ xs. xs ++ ys)⋅xs" by (induct xs) simp+
qed

lemma "foldr/cons": "foldr⋅k⋅z⋅(x:xs) = k⋅x⋅(foldr⋅k⋅z⋅xs)" by simp
lemma "foldr/single": "foldr⋅k⋅z⋅[x] = k⋅x⋅z" by simp
lemma "foldr/nil": "foldr⋅k⋅z⋅[] = z" by simp

lemma cont_listfun_comp_body1 [simp]:
  "cont (λh. Abs_listfun (Λ c n. listfun⋅g⋅c⋅(listfun⋅h⋅c⋅n), build⋅g ++ build⋅h))"
proof -
  have "⋀h.
    (Λ c n. listfun⋅g⋅c⋅(listfun⋅h⋅c⋅n), build⋅g ++ build⋅h) ∈ {(f, xs). f = abstract_list xs}"
    by (simp add: "fold/build")
  from cont_Abs_listfun [OF this, of "λx. x"]
  show ?thesis by simp
qed

lemma cont_listfun_comp_body2 [simp]:
  "cont (λg. Abs_listfun (Λ c n. listfun⋅g⋅c⋅(listfun⋅h⋅c⋅n), build⋅g ++ build⋅h))"
proof -
  have "⋀g.
    (Λ c n. listfun⋅g⋅c⋅(listfun⋅h⋅c⋅n), build⋅g ++ build⋅h) ∈ {(f, xs). f = abstract_list xs}"
    by (simp add: "fold/build")
  from cont_Abs_listfun [OF this, of "λx. x"]
  show ?thesis by simp
qed

lemma cont_listfun_comp_body [simp]:
  "cont (λg. Λ h. Abs_listfun (Λ c n. listfun⋅g⋅c⋅(listfun⋅h⋅c⋅n), build⋅g ++ build⋅h))"
  by (rule cont2cont_LAM) simp+

lemma abstract_list_build_append:
  "abstract_list (build⋅g ++ build⋅h) = (Λ c n. listfun⋅g⋅c⋅(listfun⋅h⋅c⋅n))"
  by (intro cfun_eqI) (simp add: "fold/build")

lemma "augment/build":
  "augment⋅g⋅(build⋅h) = build⋅(g ∘lf h)"
  by (simp add: listfun_comp_def augment_def build_Abs_listfun [OF abstract_list_build_append])

lemma "augment/nil":
  "augment⋅g⋅[] = build⋅g"
  by (simp add: augment_def)

lemma build_listfun_comp [simp]:
  "build⋅(g ∘lf h) = build⋅g ++ build⋅h"
  unfolding "augment/build" [symmetric]
  by (simp add: augment_def)

lemma augment_augment:
  "augment⋅g⋅(augment⋅h⋅xs) = augment⋅(g ∘lf h)⋅xs"
  by (simp add: augment_def)

lemma abstract_list_map [simp]:
  "abstract_list (map⋅f⋅xs) = (Λ c n. foldr⋅(mapFB⋅c⋅f)⋅n⋅xs)"
  by (intro cfun_eqI, induct xs) simp+

lemma "map":
  "map⋅f⋅xs = build⋅(Abs_listfun (Λ c n. foldr⋅(mapFB⋅c⋅f)⋅n⋅xs, map⋅f⋅xs))"
  by (simp add: build_Abs_listfun)

lemma "mapList":
  "foldr⋅(mapFB⋅(:)⋅f)⋅[] = map⋅f"
  by (rule cfun_eqI, rename_tac x, induct_tac x) simp+

lemma "mapFB":
  "mapFB⋅(mapFB⋅c⋅f)⋅g = mapFB⋅c⋅(f oo g)"
  by simp

lemma "++":
  "xs ++ ys = augment⋅(Abs_listfun (abstract_list xs, xs))⋅ys"
  by simp

subsection ‹Examples›

fixrec sum :: "[Integer] → Integer" where
  "sum⋅xs = foldr⋅(+)⋅0⋅xs"

fixrec down' :: "Integer → (Integer → 'a → 'a) → 'a → 'a" where
  "down'⋅v⋅c⋅n = If le⋅1⋅v then c⋅v⋅(down'⋅(v - 1)⋅c⋅n) else n"
declare down'.simps [simp del]

lemma down'_strict [simp]: "down'⋅⊥ = ⊥" by (fixrec_simp)

definition down :: "'b itself ⇒ Integer → [Integer]" where
  "down C_type = (Λ v. build⋅(Abs_listfun (
    (down' :: Integer → (Integer → 'b → 'b) → 'b → 'b)⋅v,
    down'⋅v⋅(:)⋅[])))"

lemma abstract_list_down' [simp]:
  "abstract_list (down'⋅v⋅(:)⋅[]) = down'⋅v"
proof (intro cfun_eqI)
  fix c :: "Integer → 'b → 'b" and n :: "'b"
  show "(abstract_list (down'⋅v⋅(:)⋅[]))⋅c⋅n = down'⋅v⋅c⋅n"
  proof (cases "le⋅1⋅v")
    assume "le⋅1⋅v = ⊥" then show ?thesis by simp
  next
    assume "le⋅1⋅v = FF" then show ?thesis
      by (subst (1 2) down'.simps) simp
  next
    have "le⋅(0::Integer)⋅1 = TT" by simp
    moreover assume "le⋅1⋅v = TT"
    ultimately have "le⋅0⋅v = TT" by (rule le_trans)
    then show ?thesis
      by (induct v rule: nonneg_Integer_induct)
         (subst (1 2) down'.simps, simp)+
  qed
qed

lemma cont_Abs_listfun_down' [simp]:
  "cont (λv. Abs_listfun (down'⋅v, down'⋅v⋅(:)⋅[]))"
proof -
  have "⋀v. (down'⋅v, down'⋅v⋅(:)⋅[]) ∈ {(f, xs). f = abstract_list xs}" by simp
  from cont_Abs_listfun [OF this, of id] show ?thesis by simp
qed

lemma sum_down:
  "sum⋅((down TYPE(Integer))⋅v) = down'⋅v⋅(+)⋅0"
  by (simp add: down_def "fold/build")

end