Equational proof that "treesort = radixsort" in Isabelle

Radix.thy

theory Radix
imports Main
begin

primrec fold_right :: "('a ⇒ 'b ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b" where
"fold_right f x [] = x" |
"fold_right f x (h#t) = f h (fold_right f x t)"

primrec ordered :: "('a ⇒ 'b::ord) list ⇒ 'a ⇒ 'a ⇒ bool" where
"ordered [] _ _ = True" |
"ordered (d#ds) x y = ((d x < d y) ∨ (d x = d y) ∧ ordered ds x y)"

datatype 'a tree = Leaf 'a | Node "'a tree list"

definition rng :: "nat list" where
"rng = [0..<255]"

fun ptn :: "('a ⇒ nat) ⇒ 'a list ⇒ 'a list list" where
"ptn d xs = map (λm. filter (λx. d x = m) xs) rng"

definition fm :: "('a ⇒ nat) ⇒ ('a list ⇒ 'a list tree) ⇒ 'a list ⇒ 'a list tree" where
"fm d g = Node ∘ map g ∘ ptn d"

primrec mktree0 :: "('a ⇒ nat) list ⇒ 'a list ⇒ 'a list tree" where
"mktree0 [] = Leaf" |
"mktree0 (d#ds) = Node ∘ map (mktree0 ds) ∘ ptn d"
(* "mktree = foldr fm Leaf" *)

definition mktree :: "('a ⇒ nat) list ⇒ 'a list ⇒ 'a list tree" where
"mktree = fold_right fm Leaf"

primrec foldt :: "('a ⇒ 'b) ⇒ ('b list ⇒ 'b) ⇒ 'a tree ⇒ 'b" where
"foldt f g (Leaf x) = f x" |
"foldt f g (Node ts) = g (map (foldt f g) ts)"

definition mapt :: "('a ⇒ 'b) ⇒ 'a tree ⇒ 'b tree" where
"mapt f = foldt (Leaf ∘ f) Node"

definition flatten :: "'a list tree ⇒ 'a list" where
"flatten = foldt id concat"

definition treesort :: "('a ⇒ nat) list ⇒ 'a list ⇒ 'a list" where
"treesort = (comp flatten) ∘ mktree"
(* treesort = (flatten ∘) ∘ mktree *)

(* treesort = fold_right ft et *)

definition et :: "'a list ⇒ 'a list" where
"et = flatten ∘ Leaf"

lemma [simp]: "flatten ∘ Leaf = id"
  (* by (metis comp_def eq_id_iff flatten_def foldt.simps(1)) *)
proof
  fix x :: "'a list"
  have "flatten (Leaf x) = foldt id concat (Leaf x)" by (simp add: flatten_def)
  also have "… = x" by (simp)
  finally have "flatten (Leaf x) = x" by this
  thus "(flatten ∘ Leaf) x = id x" by simp
qed

theorem "et = id"
  by (simp add: et_def)

theorem fold_map_tree_fusion [simp]: "foldt f g ∘ mapt h = foldt (f ∘ h) g"
proof
  fix x
  show "(foldt f g ∘ mapt h) x = foldt (f ∘ h) g x"
  proof (induction x)
    case (Leaf x)
    have "(foldt f g ∘ mapt h) (Leaf x) = foldt f g (mapt h (Leaf x))" by (simp)
    also have "… = foldt f g (foldt (Leaf ∘ h) Node (Leaf x))" by (simp add: mapt_def)
    also have "… = foldt f g ((Leaf ∘ h) x)" by (simp)
    also have "… = foldt f g (Leaf (h x))" by (simp)
    also have "… = f (h x)" by (simp)
    also have "… = (f ∘ h) x" by (simp)
    also have "… = foldt (f ∘ h) g (Leaf x)" by (simp)
    finally have "(foldt f g ∘ mapt h) (Leaf x) = foldt (f ∘ h) g (Leaf x)" by this
    then show ?case by (this)
  next
    case (Node x)
    have "(foldt f g ∘ mapt h) (Node x) = foldt f g (mapt h (Node x))" by (simp)
    also have "… = foldt f g (foldt (Leaf ∘ h) Node (Node x))" by (simp add: mapt_def)
    also have "… = foldt f g (Node (map (foldt (Leaf ∘ h) Node) x))" by (simp)
    also have "… = g (map (foldt f g) (map (foldt (Leaf ∘ h) Node) x))" by (simp)
    also have "… = g (map ((foldt f g) ∘ (foldt (Leaf ∘ h) Node)) x)" by (simp)
    also have "… = g (map ((foldt f g) ∘ (mapt h)) x)" by (simp add: mapt_def)
    also have "… = g (map (foldt (f ∘ h) g) x)" using Node.IH by (metis (mono_tags, hide_lams) map_eq_conv)
    finally have "(foldt f g ∘ mapt h) (Node x) = foldt (f ∘ h) g (Node x)" by (simp)
    then show ?case by this
  qed
qed

lemma filter_flatten [simp]: "filter p ∘ flatten = flatten ∘ mapt (filter p)"
proof -
  fix p :: "'a ⇒ bool"
  have "filter p ∘ flatten = filter p ∘ foldt id concat" by (simp add: flatten_def)
  also have "… = foldt (filter p) concat"
  proof
    fix x
    show "(filter p ∘ foldt id concat) x = foldt (filter p) concat x"
    proof (induction x)
      case (Leaf x)
      have "(filter p ∘ foldt id concat) (Leaf x) = filter p (foldt id concat (Leaf x))" by (simp)
      also have "… = filter p (id x)" by (simp)
      also have "… = filter p x" by (simp)
      finally have "(filter p ∘ foldt id concat) (Leaf x) = foldt (filter p) concat (Leaf x)" by (simp)
      then show ?case by this
    next
      case (Node x)
      have "(filter p ∘ foldt id concat) (Node x) = filter p (foldt id concat (Node x))" by (simp)
      also have "… = filter p (concat (map (foldt id concat) x))" by (simp)
      also have "… = concat (map (filter p) (map (foldt id concat) x))" by (simp add: filter_concat)
      also have "… = concat (map (filter p ∘ foldt id concat) x)" by (simp)
      also have "… = concat (map (foldt (filter p) concat) x)" by (metis (mono_tags, hide_lams) Node.IH map_eq_conv)
      finally have "(filter p ∘ foldt id concat) (Node x) = foldt (filter p) concat (Node x)" by (simp)
      then show ?case by this
    qed
  qed
  also have "… = foldt id concat ∘ mapt (filter p)" by (simp)
  finally have "filter p ∘ flatten = flatten ∘ mapt (filter p)" by (simp add: flatten_def)
  then show  "filter p ∘ flatten = flatten ∘ mapt (filter p)" by this
qed

lemma [simp]: "comp (mapt (filter p)) ∘ mktree = fold_right fm (Leaf ∘ filter p)"
proof -
  have "comp (mapt (filter p)) ∘ mktree = (λl. comp (mapt (filter p)) (mktree l))" by (simp add: comp_def)
  also have "… = (λl. comp (mapt (filter p)) (fold_right fm Leaf l))" by (simp add: mktree_def)
  finally have 1: "comp (mapt (filter p)) ∘ mktree = (λl. comp (foldt (Leaf ∘ filter p) Node) (fold_right fm Leaf l))" by (simp add: mapt_def)
  {
    fix l
    have "comp (foldt (Leaf ∘ filter p) Node) (fold_right fm Leaf l) = fold_right fm (Leaf ∘ filter p) l"
    proof (induction l)
      case Nil
      have "foldt (Leaf ∘ filter p) Node ∘ fold_right fm Leaf [] = (λl. (foldt (Leaf ∘ filter p) Node) ((fold_right fm Leaf []) l))" by (simp add: comp_def)
      also have "… = (λl. (foldt (Leaf ∘ filter p) Node) (Leaf l))" by (simp)
      also have "… = (λl. (Leaf ∘ filter p) l)" by (simp)
      finally have "foldt (Leaf ∘ filter p) Node ∘ fold_right fm Leaf [] = fold_right fm (Leaf ∘ filter p) []" by (simp add: comp_def)
      then show ?case by this
    next
      case (Cons a l)
      have "foldt (Leaf ∘ filter p) Node ∘ fold_right fm Leaf (a#l) = foldt (Leaf ∘ filter p) Node ∘ (fm a (fold_right fm Leaf l))" by (simp)
      also have "… = foldt (Leaf ∘ filter p) Node ∘ Node ∘ map (fold_right fm Leaf l) ∘ ptn a" by (simp add: fm_def comp_assoc)
      also have "… = (λxs. foldt (Leaf ∘ filter p) Node (Node (map (fold_right fm Leaf l) (ptn a xs))))" by (simp add: comp_def)
      also have "… = (λxs. Node (map (foldt (Leaf ∘ filter p) Node) (map (fold_right fm Leaf l) (ptn a xs))))" by (simp)
      also have "… = (λxs. Node (map ( foldt (Leaf ∘ filter p) Node ∘ fold_right fm Leaf l ) (ptn a xs)))" by (simp add: comp_def)
      also have "… = (λxs. Node (map ( fold_right fm (Leaf ∘ filter p) l ) (ptn a xs)))" using Cons.IH by (simp add: comp_def)
      also have "… = Node ∘ map (fold_right fm (Leaf ∘ filter p) l) ∘ ptn a" by (simp add: comp_def)
      also have "… = fm a (fold_right fm (Leaf ∘ filter p) l)" by (simp add: fm_def)
      finally have "foldt (Leaf ∘ filter p) Node ∘ fold_right fm Leaf (a#l) = fold_right fm (Leaf ∘ filter p) (a # l)" by (simp)
      then show ?case by this
    qed
  }
  thus ?thesis using 1 by (simp add: comp_def)
qed

lemma ptn_filt: "ptn d ∘ filter p = map (filter p) ∘ ptn d"
  by (simp add: comp_def conj_commute)

lemma fm_filter: "fm d (g ∘ filter p) = fm d g ∘ filter p"
  using ptn_filt
  by (simp add: fm_def comp_def conj_commute)

corollary mktree_filter [simp]: "mapt (filter p) ∘ mktree ds = mktree ds ∘ filter p"
proof -
  have "mapt (filter p) ∘ mktree ds = (comp (mapt (filter p)) ∘ mktree) ds" by (simp add: comp_def)
  also have "… = (fold_right fm (Leaf ∘ filter p)) ds" by (simp)
  finally have 1: "mapt (filter p) ∘ mktree ds = (fold_right fm (Leaf ∘ filter p)) ds" by (this)

  have "(fold_right fm (Leaf ∘ filter p)) ds = ((λf. f ∘ filter p) ∘ mktree) ds"
  proof (induction ds)
    case Nil
    then show ?case  by (simp add: comp_def mktree_def)
  next
    case (Cons a ds)
    have "fold_right fm (Leaf ∘ filter p) (a # ds) = fm a (fold_right fm (Leaf ∘ filter p) ds)" by (simp)
    also have "… = fm a (((λf. f ∘ filter p) ∘ mktree) ds)" using Cons.IH by (simp add: comp_def)
    also have "… = fm a ((mktree ds) ∘ filter p)" by (simp add: comp_def)
    also have "… = fm a (mktree ds) ∘ filter p" using fm_filter [where d=a] by (simp)
    finally have "fold_right fm (Leaf ∘ filter p) (a # ds) = ((λf. f ∘ filter p) ∘ mktree) (a # ds)" by (simp add: comp_def mktree_def)
    then show ?case by (this)
  qed

  thus ?thesis using 1 by (simp)
qed

lemma aux: "filter p ∘ treesort ds = treesort ds ∘ filter p"
proof -
  have "filter p ∘ treesort ds = filter p ∘ flatten ∘ mktree ds" by (simp add: treesort_def comp_def)
  also have "… = flatten ∘ mapt (filter p) ∘ mktree ds" by (simp)
  also have "… = flatten ∘ mktree ds ∘ filter p" using mktree_filter[where ds=ds and p=p] comp_eq_dest[where a="mapt (filter p)" and b="mktree ds" and c="mktree ds"] by (simp add: comp_def)
  finally have "filter p ∘ treesort ds = treesort ds ∘ filter p" by (simp add: treesort_def)
  thus ?thesis by (this)
qed

lemma stability [simp]: "ptn d (treesort ds xs) = map (treesort ds) (ptn d xs)"
proof -
  have lhs: "ptn d (treesort ds xs) = map (λm. filter (λx. d x = m) (treesort ds xs)) rng" by (simp)

  have "map (treesort ds) (ptn d xs) = map (treesort ds) (map (λm. filter (λx. d x = m) xs) rng)" by (simp)
  also have "… = map (treesort ds ∘ (λm. filter (λx. d x = m) xs)) rng"  by (simp)
  finally have rhs: "map (treesort ds) (ptn d xs) = map (λm. treesort ds (filter (λx. d x = m) xs)) rng"  by (simp)

  then show ?thesis using lhs rhs
  proof -
    have "map (λm. filter (λx. d x = m) (treesort ds xs)) rng = map (λm. treesort ds (filter (λx. d x = m) xs)) rng" using aux by (metis comp_apply)
    hence "ptn d (treesort ds xs) = map (treesort ds) (ptn d xs)" by (simp)
    thus ?thesis by (this)
  qed
qed

corollary [simp]: "ptn d ∘ treesort ds = map (treesort ds) ∘ ptn d"
  using stability[where d=d and ds=ds]
  apply (simp add: comp_def)
proof -
  assume "⋀xs. ∀x∈set rng. [xa←treesort ds xs . d xa = x] = treesort ds [xa←xs . d xa = x]"
  then show "(λas. map (λn. [a←treesort ds as . d a = n]) rng) = (λas. map (λn. treesort ds [a←as . d a = n]) rng)"
    by (meson map_eq_conv)
qed

lemma "flatten ∘ fm d (mktree ds) = concat ∘ ptn d ∘ flatten ∘ mktree ds"
proof -
  have "flatten ∘ fm d (mktree ds) = flatten ∘ Node ∘ map (mktree ds) ∘ ptn d" by (simp add: fm_def comp_assoc)
  also have "… = concat ∘ map flatten ∘ map (mktree ds) ∘ ptn d" by (simp add: flatten_def comp_def)
  also have "… = concat ∘ map (treesort ds) ∘ ptn d" by (simp add: treesort_def comp_def)
  also have "… = concat ∘ ptn d ∘ treesort ds" by (simp add: comp_assoc)
  finally have "flatten ∘ fm d (mktree ds) = concat ∘ ptn d ∘ flatten ∘ mktree ds" by (simp add: treesort_def comp_assoc)
  thus ?thesis by (this)
qed

definition ft :: "('a ⇒ nat) ⇒ ('a list ⇒ 'a list) ⇒ 'a list ⇒ 'a list" where
"ft d g =  concat ∘ ptn d ∘ g"

lemma [simp]: "treesort = fold_right ft id"
proof -
  {
    fix l :: "('a ⇒ nat) list"
    have "treesort l = fold_right ft id l"
    proof (induction l)
      case Nil
      have "treesort [] = flatten ∘ fold_right fm Leaf []" by (simp add: treesort_def mktree_def)
      also have "… = flatten ∘ Leaf" by (simp)
      also have "… = id" by (simp)
      finally have "treesort [] = fold_right ft id []" by (simp)
      then show ?case by this
    next
      case (Cons a l)
      have "treesort (a#l) = flatten ∘ fold_right fm Leaf (a#l)" by (simp add: treesort_def mktree_def)
      also have "… = flatten ∘ fm a (fold_right fm Leaf l)" by (simp)
      also have "… = flatten ∘ Node ∘ map (fold_right fm Leaf l) ∘ ptn a" by (simp add: fm_def comp_assoc)
      also have "… = foldt id concat ∘ Node ∘ map (fold_right fm Leaf l) ∘ ptn a" by (simp add: flatten_def)
      also have "… = (λxs. foldt id concat (Node (map (fold_right fm Leaf l) (ptn a xs))))" by (simp add: comp_def)
      also have "… = (λxs. concat (map (foldt id concat) (map (fold_right fm Leaf l) (ptn a xs))))" by (simp)
      also have "… = concat ∘ map ( foldt id concat ∘ fold_right fm Leaf l ) ∘ ptn a" by (simp add: comp_def)
      also have "… = concat ∘ map (flatten ∘ fold_right fm Leaf l) ∘ ptn a" by (simp add: flatten_def)
      also have "… = concat ∘ map (treesort l) ∘ ptn a" by (simp add: treesort_def mktree_def)
      also have "… = concat ∘ ptn a ∘ treesort l" by (simp add: comp_assoc)
      also have "… = concat ∘ ptn a ∘ fold_right ft id l" using Cons.IH by (simp add: id_def)
      finally have "treesort (a#l) = fold_right ft id (a#l)" by (simp add: ft_def)
      then show ?case by this
    qed
  }
  thus ?thesis by (simp add: HOL.ext)
qed

definition radixsort :: "('a ⇒ nat) list ⇒ 'a list ⇒ 'a list" where
"radixsort = fold_right ft id"

theorem treesort_radixsort: "treesort = radixsort" by (simp add: radixsort_def et_def)

declare treesort_radixsort[code]

export_code treesort in Haskell

end