(* Author: Tobias Nipkow *)
(* Todo: minimal ipl of almost complete trees *)
section ‹Binary Tree
›
theory Tree
imports Main
begin
datatype 'a tree =
Leaf (
‹⟨⟩›) |
Node
"'a tree" (
"value":
'a) "'a tree
" (\(\indent=1 notation=\mixfix Node\\\_,/ _,/ _\)\)
datatype_compat tree
primrec left ::
"'a tree \ 'a tree" where
"left (Node l v r) = l" |
"left Leaf = Leaf"
primrec right ::
"'a tree \ 'a tree" where
"right (Node l v r) = r" |
"right Leaf = Leaf"
text‹Counting the number of leaves rather than nodes:
›
fun size1 ::
"'a tree \ nat" where
"size1 \\ = 1" |
"size1 \l, x, r\ = size1 l + size1 r"
fun subtrees ::
"'a tree \ 'a tree set" where
"subtrees \\ = {\\}" |
"subtrees (\l, a, r\) = {\l, a, r\} \ subtrees l \ subtrees r"
fun mirror ::
"'a tree \ 'a tree" where
"mirror \\ = Leaf" |
"mirror \l,x,r\ = \mirror r, x, mirror l\"
class height =
fixes height ::
"'a \ nat"
instantiation tree :: (type)height
begin
fun height_tree ::
"'a tree => nat" where
"height Leaf = 0" |
"height (Node l a r) = max (height l) (height r) + 1"
instance ..
end
fun min_height ::
"'a tree \ nat" where
"min_height Leaf = 0" |
"min_height (Node l _ r) = min (min_height l) (min_height r) + 1"
fun complete ::
"'a tree \ bool" where
"complete Leaf = True" |
"complete (Node l x r) = (height l = height r \ complete l \ complete r)"
text ‹Almost complete:
›
definition acomplete ::
"'a tree \ bool" where
"acomplete t = (height t - min_height t \ 1)"
text ‹Weight balanced:
›
fun wbalanced ::
"'a tree \ bool" where
"wbalanced Leaf = True" |
"wbalanced (Node l x r) = (abs(int(size l) - int(size r)) \ 1 \ wbalanced l \ wbalanced r)"
text ‹Internal path length:
›
fun ipl ::
"'a tree \ nat" where
"ipl Leaf = 0 " |
"ipl (Node l _ r) = ipl l + size l + ipl r + size r"
fun preorder ::
"'a tree \ 'a list" where
"preorder \\ = []" |
"preorder \l, x, r\ = x # preorder l @ preorder r"
fun inorder ::
"'a tree \ 'a list" where
"inorder \\ = []" |
"inorder \l, x, r\ = inorder l @ [x] @ inorder r"
text‹A linear version avoiding append:
›
fun inorder2 ::
"'a tree \ 'a list \ 'a list" where
"inorder2 \\ xs = xs" |
"inorder2 \l, x, r\ xs = inorder2 l (x # inorder2 r xs)"
fun postorder ::
"'a tree \ 'a list" where
"postorder \\ = []" |
"postorder \l, x, r\ = postorder l @ postorder r @ [x]"
text‹Binary Search Tree:
›
fun bst_wrt ::
"('a \ 'a \ bool) \ 'a tree \ bool" where
"bst_wrt P \\ \ True" |
"bst_wrt P \l, a, r\ \
(
∀x
∈set_tree l. P x a)
∧ (
∀x
∈set_tree r. P a x)
∧ bst_wrt P l
∧ bst_wrt P r
"
abbreviation bst ::
"('a::linorder) tree \ bool" where
"bst \ bst_wrt (<)"
fun (
in linorder) heap ::
"'a tree \ bool" where
"heap Leaf = True" |
"heap (Node l m r) =
((
∀x
∈ set_tree l
∪ set_tree r. m
≤ x)
∧ heap l
∧ heap r)
"
subsection ‹🍋‹map_tree
››
lemma eq_map_tree_Leaf[simp]:
"map_tree f t = Leaf \ t = Leaf"
by (rule tree.map_disc_iff)
lemma eq_Leaf_map_tree[simp]:
"Leaf = map_tree f t \ t = Leaf"
by (cases t) auto
subsection ‹🍋‹size
››
lemma size1_size:
"size1 t = size t + 1"
by (
induction t) simp_all
lemma size1_ge0[simp]:
"0 < size1 t"
by (simp add: size1_size)
lemma eq_size_0[simp]:
"size t = 0 \ t = Leaf"
by(cases t) auto
lemma eq_0_size[simp]:
"0 = size t \ t = Leaf"
by(cases t) auto
lemma neq_Leaf_iff:
"(t \ \\) = (\l a r. t = \l, a, r\)"
by (cases t) auto
lemma size_map_tree[simp]:
"size (map_tree f t) = size t"
by (
induction t) auto
lemma size1_map_tree[simp]:
"size1 (map_tree f t) = size1 t"
by (simp add: size1_size)
subsection ‹🍋‹set_tree
››
lemma eq_set_tree_empty[simp]:
"set_tree t = {} \ t = Leaf"
by (cases t) auto
lemma eq_empty_set_tree[simp]:
"{} = set_tree t \ t = Leaf"
by (cases t) auto
lemma finite_set_tree[simp]:
"finite(set_tree t)"
by(
induction t) auto
subsection ‹🍋‹subtrees
››
lemma neq_subtrees_empty[simp]:
"subtrees t \ {}"
by (cases t)(auto)
lemma neq_empty_subtrees[simp]:
"{} \ subtrees t"
by (cases t)(auto)
lemma size_subtrees:
"s \ subtrees t \ size s \ size t"
by(
induction t)(auto)
lemma set_treeE:
"a \ set_tree t \ \l r. \l, a, r\ \ subtrees t"
by (
induction t)(auto)
lemma Node_notin_subtrees_if[simp]:
"a \ set_tree t \ Node l a r \ subtrees t"
by (
induction t) auto
lemma in_set_tree_if:
"\l, a, r\ \ subtrees t \ a \ set_tree t"
by (metis Node_notin_subtrees_if)
subsection ‹🍋‹height
› and 🍋‹min_height
››
lemma eq_height_0[simp]:
"height t = 0 \ t = Leaf"
by(cases t) auto
lemma eq_0_height[simp]:
"0 = height t \ t = Leaf"
by(cases t) auto
lemma height_map_tree[simp]:
"height (map_tree f t) = height t"
by (
induction t) auto
lemma height_le_size_tree:
"height t \ size (t::'a tree)"
by (
induction t) auto
lemma size1_height:
"size1 t \ 2 ^ height (t::'a tree)"
proof(
induction t)
case (Node l a r)
show ?
case
proof (cases
"height l \ height r")
case True
have "size1(Node l a r) = size1 l + size1 r" by simp
also have "\ \ 2 ^ height l + 2 ^ height r" using Node.IH
by arith
also have "\ \ 2 ^ height r + 2 ^ height r" using True
by simp
also have "\ = 2 ^ height (Node l a r)"
using True
by (auto simp: max_def mult_2)
finally show ?thesis .
next
case False
have "size1(Node l a r) = size1 l + size1 r" by simp
also have "\ \ 2 ^ height l + 2 ^ height r" using Node.IH
by arith
also have "\ \ 2 ^ height l + 2 ^ height l" using False
by simp
finally show ?thesis
using False
by (auto simp: max_def mult_2)
qed
qed simp
corollary size_height:
"size t \ 2 ^ height (t::'a tree) - 1"
using size1_height[of t, unfolded size1_size]
by(arith)
lemma height_subtrees:
"s \ subtrees t \ height s \ height t"
by (
induction t) auto
lemma min_height_le_height:
"min_height t \ height t"
by(
induction t) auto
lemma min_height_map_tree[simp]:
"min_height (map_tree f t) = min_height t"
by (
induction t) auto
lemma min_height_size1:
"2 ^ min_height t \ size1 t"
proof(
induction t)
case (Node l a r)
have "(2::nat) ^ min_height (Node l a r) \ 2 ^ min_height l + 2 ^ min_height r"
by (simp add: min_def)
also have "\ \ size1(Node l a r)" using Node.IH
by simp
finally show ?
case .
qed simp
subsection ‹🍋‹complete
››
lemma complete_iff_height:
"complete t \ (min_height t = height t)"
apply(
induction t)
apply simp
apply (simp add: min_def max_def)
by (metis le_antisym le_trans min_height_le_height)
lemma size1_if_complete:
"complete t \ size1 t = 2 ^ height t"
by (
induction t) auto
lemma size_if_complete:
"complete t \ size t = 2 ^ height t - 1"
using size1_if_complete[simplified size1_size]
by fastforce
lemma size1_height_if_incomplete:
"\ complete t \ size1 t < 2 ^ height t"
proof(
induction t)
case Leaf
thus ?
case by simp
next
case (Node l x r)
have 1: ?
case if h:
"height l < height r"
using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of
"2::nat"]
by(auto simp: max_def simp del: power_strict_increasing_iff)
have 2: ?
case if h:
"height l > height r"
using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of
"2::nat"]
by(auto simp: max_def simp del: power_strict_increasing_iff)
have 3: ?
case if h:
"height l = height r" and c:
"\ complete l"
using h size1_height[of r] Node.IH(1)[OF c]
by(simp)
have 4: ?
case if h:
"height l = height r" and c:
"\ complete r"
using h size1_height[of l] Node.IH(2)[OF c]
by(simp)
from 1 2 3 4 Node.prems
show ?
case apply (simp add: max_def)
by linarith
qed
lemma complete_iff_min_height:
"complete t \ (height t = min_height t)"
by(auto simp add: complete_iff_height)
lemma min_height_size1_if_incomplete:
"\ complete t \ 2 ^ min_height t < size1 t"
proof(
induction t)
case Leaf
thus ?
case by simp
next
case (Node l x r)
have 1: ?
case if h:
"min_height l < min_height r"
using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of
"2::nat"]
by(auto simp: max_def simp del: power_strict_increasing_iff)
have 2: ?
case if h:
"min_height l > min_height r"
using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of
"2::nat"]
by(auto simp: max_def simp del: power_strict_increasing_iff)
have 3: ?
case if h:
"min_height l = min_height r" and c:
"\ complete l"
using h min_height_size1[of r] Node.IH(1)[OF c]
by(simp add: complete_iff_min_height)
have 4: ?
case if h:
"min_height l = min_height r" and c:
"\ complete r"
using h min_height_size1[of l] Node.IH(2)[OF c]
by(simp add: complete_iff_min_height)
from 1 2 3 4 Node.prems
show ?
case
by (fastforce simp: complete_iff_min_height[
THEN iffD1])
qed
lemma complete_if_size1_height:
"size1 t = 2 ^ height t \ complete t"
using size1_height_if_incomplete
by fastforce
lemma complete_if_size1_min_height:
"size1 t = 2 ^ min_height t \ complete t"
using min_height_size1_if_incomplete
by fastforce
lemma complete_iff_size1:
"complete t \ size1 t = 2 ^ height t"
using complete_if_size1_height size1_if_complete
by blast
subsection ‹🍋‹acomplete
››
lemma acomplete_subtreeL:
"acomplete (Node l x r) \ acomplete l"
by(simp add: acomplete_def)
lemma acomplete_subtreeR:
"acomplete (Node l x r) \ acomplete r"
by(simp add: acomplete_def)
lemma acomplete_subtrees:
"\ acomplete t; s \ subtrees t \ \ acomplete s"
using [[simp_depth_limit=1]]
by(
induction t arbitrary: s)
(auto simp add: acomplete_subtreeL acomplete_subtreeR)
text‹Balanced trees
have optimal height:
›
lemma acomplete_optimal:
fixes t ::
"'a tree" and t
' :: "'b tree
"
assumes "acomplete t" "size t \ size t'" shows "height t \ height t'"
proof (cases
"complete t")
case True
have "(2::nat) ^ height t \ 2 ^ height t'"
proof -
have "2 ^ height t = size1 t"
using True
by (simp add: size1_if_complete)
also have "\ \ size1 t'" using assms(2)
by(simp add: size1_size)
also have "\ \ 2 ^ height t'" by (rule size1_height)
finally show ?thesis .
qed
thus ?thesis
by (simp)
next
case False
have "(2::nat) ^ min_height t < 2 ^ height t'"
proof -
have "(2::nat) ^ min_height t < size1 t"
by(rule min_height_size1_if_incomplete[OF False])
also have "\ \ size1 t'" using assms(2)
by (simp add: size1_size)
also have "\ \ 2 ^ height t'" by(rule size1_height)
finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" .
thus ?thesis .
qed
hence *:
"min_height t < height t'" by simp
have "min_height t + 1 = height t"
using min_height_le_height[of t] assms(1) False
by (simp add: complete_iff_height acomplete_def)
with *
show ?thesis
by arith
qed
subsection ‹🍋‹wbalanced
››
lemma wbalanced_subtrees:
"\ wbalanced t; s \ subtrees t \ \ wbalanced s"
using [[simp_depth_limit=1]]
by(
induction t arbitrary: s) auto
subsection ‹🍋‹ipl
››
text ‹The internal path length of a tree:
›
lemma ipl_if_complete_int:
"complete t \ int(ipl t) = (int(height t) - 2) * 2^(height t) + 2"
apply(
induction t)
apply simp
apply simp
apply (simp add: algebra_simps size_if_complete of_nat_diff)
done
subsection "List of entries"
lemma eq_inorder_Nil[simp]:
"inorder t = [] \ t = Leaf"
by (cases t) auto
lemmas eq_Nil_inorder[simp] = eq_inorder_Nil[
THEN eq_iff_swap]
lemma set_inorder[simp]:
"set (inorder t) = set_tree t"
by (
induction t) auto
lemma preorder_eq_Nil_iff[simp]:
"(preorder t = []) = (t = \\)"
by (cases t) auto
lemmas Nil_eq_preorder_iff [simp] = preorder_eq_Nil_iff[
THEN eq_iff_swap]
lemma preorder_eq_Cons_iff:
"preorder t = x # xs \ (\ l r. t = \l, x, r\ \ xs = preorder l @ preorder r)"
by (cases t) auto
lemmas Cons_eq_preorder_iff = preorder_eq_Cons_iff[
THEN eq_iff_swap]
lemma set_preorder[simp]:
"set (preorder t) = set_tree t"
by (
induction t) auto
lemma set_postorder[simp]:
"set (postorder t) = set_tree t"
by (
induction t) auto
lemma length_preorder[simp]:
"length (preorder t) = size t"
by (
induction t) auto
lemma length_inorder[simp]:
"length (inorder t) = size t"
by (
induction t) auto
lemma length_postorder[simp]:
"length (postorder t) = size t"
by (
induction t) auto
lemma preorder_map:
"preorder (map_tree f t) = map f (preorder t)"
by (
induction t) auto
lemma inorder_map:
"inorder (map_tree f t) = map f (inorder t)"
by (
induction t) auto
lemma postorder_map:
"postorder (map_tree f t) = map f (postorder t)"
by (
induction t) auto
lemma inorder2_inorder:
"inorder2 t xs = inorder t @ xs"
by (
induction t arbitrary: xs) auto
subsection ‹Binary Search Tree
›
lemma bst_wrt_mono:
"(\x y. P x y \ Q x y) \ bst_wrt P t \ bst_wrt Q t"
by (
induction t) (auto)
lemma bst_wrt_le_if_bst:
"bst t \ bst_wrt (\) t"
using bst_wrt_mono less_imp_le
by blast
lemma bst_wrt_le_iff_sorted:
"bst_wrt (\) t \ sorted (inorder t)"
apply (
induction t)
apply(simp)
by (fastforce simp: sorted_append intro: less_imp_le less_trans)
lemma bst_iff_sorted_wrt_less:
"bst t \ sorted_wrt (<) (inorder t)"
apply (
induction t)
apply simp
apply (fastforce simp: sorted_wrt_append)
done
subsection ‹🍋‹heap
››
subsection ‹🍋‹mirror
››
lemma mirror_Leaf[simp]:
"mirror t = \\ \ t = \\"
by (
induction t) simp_all
lemma Leaf_mirror[simp]:
"\\ = mirror t \ t = \\"
using mirror_Leaf
by fastforce
lemma size_mirror[simp]:
"size(mirror t) = size t"
by (
induction t) simp_all
lemma size1_mirror[simp]:
"size1(mirror t) = size1 t"
by (simp add: size1_size)
lemma height_mirror[simp]:
"height(mirror t) = height t"
by (
induction t) simp_all
lemma min_height_mirror [simp]:
"min_height (mirror t) = min_height t"
by (
induction t) simp_all
lemma ipl_mirror [simp]:
"ipl (mirror t) = ipl t"
by (
induction t) simp_all
lemma inorder_mirror:
"inorder(mirror t) = rev(inorder t)"
by (
induction t) simp_all
lemma map_mirror:
"map_tree f (mirror t) = mirror (map_tree f t)"
by (
induction t) simp_all
lemma mirror_mirror[simp]:
"mirror(mirror t) = t"
by (
induction t) simp_all
end
