theory Perlen3_WS1617_Blatt13 imports "~~/src/HOL/Library/Multiset" begin section \Trees\ subsection \Tail-recursive inorder\ datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree" fun inorder :: "'a tree \ 'a list" where "inorder Leaf = []" | "inorder (Node l x r) = inorder l @ x # inorder r" text \ Unfortunately, @{const inorder} requires more than linear time. Why? Define a linear-time version instead and prove the time bound. \ section \Leftist heaps\ datatype 'a lheap = Leaf ("\\") | Node nat "'a lheap" 'a "'a lheap" ("(1\_,/ _,/ _,/ _\)") fun rank :: "'a lheap \ nat" where "rank Leaf = 0" | "rank (Node _ _ _ r) = rank r + 1" fun rk :: "'a lheap \ nat" where "rk Leaf = 0" | "rk (Node n _ _ _) = n" definition node :: "'a lheap \ 'a \ 'a lheap \ 'a lheap" where "node l a r = (let rl = rk l; rr = rk r in if rl \ rr then Node (rr+1) l a r else Node (rl+1) r a l)" function meld :: "'a::ord lheap \ 'a lheap \ 'a lheap" where "meld Leaf t2 = t2" | "meld t1 Leaf = t1" | "meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) = (if a1 \ a2 then node l1 a1 (meld r1 (Node n2 l2 a2 r2)) else node l2 a2 (meld r2 (Node n1 l1 a1 r1)))" by pat_completeness auto termination by (relation "measure (\(t1, t2). rank t1 + rank t2)") auto definition insert :: "'a::ord \ 'a lheap \ 'a lheap" where "insert x t = meld (Node 1 Leaf x Leaf) t" fun mset_tree :: "'a lheap \ 'a multiset" where "mset_tree Leaf = {#}" | "mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r" lemma mset_meld[simp]: "mset_tree (meld h1 h2) = mset_tree h1 + mset_tree h2" by (induction h1 h2 rule: meld.induct) (auto simp: node_def ac_simps Let_def) lemma mset_insert: "mset_tree (insert x t) = {#x#} + mset_tree t" by (auto simp add: insert_def mset_meld) fun mset_forest :: "'a lheap list \ 'a multiset" where "mset_forest [] = {#}" | "mset_forest (x # xs) = mset_tree x + mset_forest xs" fun inv :: "'a lheap \ bool" where "inv Leaf = True" | "inv (Node n l a r) = (n = rank r + 1 \ rank l \ rank r \ inv l \ inv r)" lemma rk_eq_rank[simp]: "inv t \ rk t = rank t" by(cases t) auto subsection \Construct a heap from a list\ text \ It is trivial to define a function @{typ "'a list \ 'a lheap"} that constructs a heap from an unordered list. But is the naive implementation efficient? Define such a function that only requires a logarithmic number of @{const meld} operations. Prove its correctness. What is the total running time? \ subsection \Direct insertion\ text \ Insertion is defined like this: @{term "insert x t = meld (Node 1 Leaf x Leaf) t"} This is quite elegant. However, there is also a direct version which does not require the @{const meld} function. Define it and prove its correctness. \ end