theory HeapHW imports Heap begin lemma is_lheap_weaken: "\ is_lheap h x; y \ x \ \ is_lheap h y" by (induct h) auto lemma make_heap_makes_heap: "\ is_lheap a x; is_lheap b y; z \ x; z \ y \ \ is_lheap (make_heap a z b) z" apply (auto simp: make_heap_def) using is_lheap_weaken apply blast+ done theorem merge_makes_heap: "\ is_lheap a z; is_lheap b z \ \ is_lheap (merge a b) z" proof (induct a b arbitrary: z rule: merge.induct) fix h z assume "is_lheap h z" thus "is_lheap (merge Leaf h) z" by simp next fix r1 a1 x b1 h2 z let ?h1 = "(Node r1 a1 x b1)" assume IH1: "\nat1 lheap1 nat2 lheap2 z. \h2 = Node nat1 lheap1 nat2 lheap2; x \ nat2; is_lheap b1 z; is_lheap h2 z\ \ is_lheap (merge b1 h2) z" and IH2: "\nat1 lheap1 nat2 lheap2 z. \h2 = Node nat1 lheap1 nat2 lheap2; \ x \ nat2; is_lheap ?h1 z; is_lheap lheap2 z\ \ is_lheap (merge ?h1 lheap2) z" and h1: "is_lheap ?h1 z" and h2: "is_lheap h2 z" show "is_lheap (merge ?h1 h2) z" proof (cases h2) case Leaf with Leaf h1 show "is_lheap (merge ?h1 h2) z" by simp next case (Node r2 a2 y b2) from h1 have a1: "is_lheap a1 x" by simp from h1 have b1: "is_lheap b1 x" by simp from h2 Node have a2: "is_lheap a2 y" by simp from h2 Node have b2: "is_lheap b2 y" by simp from h1 have zx: "z \ x" by simp from h2 Node have zy: "z \ y" by simp show ?thesis proof (cases "x \ y") assume xy: "x \ y" from IH1 h2 Node xy b1 have b1h2: "is_lheap (merge b1 h2) x" by simp let ?M = "(make_heap a1 x (merge b1 h2))" from b1h2 a1 xy have hxx: "is_lheap ?M x" using make_heap_makes_heap by simp from hxx zx Node xy show ?thesis using is_lheap_weaken by simp next assume xy: "\ x \ y" from Node h1 b2 IH2[of r2 a2 y b2 y] xy have hm: "is_lheap (merge ?h1 b2) y" by simp from a2 hm have "is_lheap (make_heap a2 y (merge ?h1 b2)) y" using make_heap_makes_heap by simp with zy have "is_lheap (make_heap a2 y (merge ?h1 b2)) z" using is_lheap_weaken by simp with xy Node show ?thesis by simp qed qed qed end