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