theory Heap imports Main begin -- "Leftist Heap" datatype lheap = Leaf | Node nat lheap nat lheap primrec rank :: "lheap \ nat" where "rank Leaf = 0" | "rank (Node r a x b) = r" primrec is_lheap :: "lheap \ nat \ bool" where "is_lheap Leaf n = True" | "is_lheap (Node r a x b) n = (n \ x \ r = Suc (rank b) \ is_lheap a x \ is_lheap b x)" definition make_heap :: "lheap \ nat \ lheap \ lheap" where "make_heap a x b \ (if rank b \ rank a then Node (rank b + 1) a x b else Node (rank a + 1) b x a)" fun merge :: "lheap \ lheap \ lheap" where "merge Leaf h = h" | "merge (Node r1 a1 x b1) h2 = (case h2 of Leaf \ (Node r1 a1 x b1) | Node r2 a2 y b2 \ (if x \ y then (make_heap a1 x (merge b1 h2)) else make_heap a2 y (merge (Node r1 a1 x b1) b2)))" definition insert :: "nat \ lheap \ lheap" where "insert x h \ merge (Node 1 Leaf x Leaf) h" declare insert_def[simp] primrec find_min :: "lheap \ nat option" where "find_min Leaf = None" | "find_min (Node r a x b) = Some x" primrec delete_min :: "lheap \ lheap" where "delete_min Leaf = Leaf" | "delete_min (Node r a x b) = merge a b" theorem merge_makes_heap: "\ is_lheap a z; is_lheap b z \ \ is_lheap (merge a b) z" oops end