Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Equational proof that "treesort = radixsort" in Isabelle
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.