# Theory Sort

(*  Title:      Sort.thy
Author:     Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *)

section ‹Locale Sort›

theory Sort
imports Main
"HOL-Library.Multiset"
begin

text ‹
First, we start from the definition of sorting algorithm. {\em What
are the basic properties that any sorting algorithm must satisfy? }
There are two
basic features any sorting algorithm must satisfy:
\begin{itemize}
\item The elements of sorted array must be in some order,
e.g. ascending or descending order. In this paper we are sorting in
ascending order.
$$sorted\ (sort\ \ l)$$

\item The algorithm does not change or delete elements of the given
array, e.g. the sorted array is the permutation of the input
array.
$$sort\ l\ <\sim \sim>\ l$$
\end{itemize}

›

locale Sort =
fixes sort :: "'a::linorder list ⇒ 'a list"
assumes sorted: "sorted (sort l)"
assumes permutation: "mset (sort l) = mset l"

end


# Theory RemoveMax

(*  Title:      Sort.thy
Author:     Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *)

section ‹Defining data structure and \\
key function remove\_max›

theory RemoveMax
imports Sort
begin

subsection ‹Describing data structure›

text‹
We have already said that we are going to formalize heap and selection
sort and to show connections between these two sorts.  However, one
can immediately notice that selection sort is using list and heap sort
is using heap during its work. It would be very difficult to show
equivalency between these two sorts if it is continued straightforward
and independently proved that they satisfy conditions of locale
\verb|Sort|. They work with different objects. Much better thing to do
is to stay on the abstract level and to add the new locale, one that
describes characteristics of both list and heap.
›

locale Collection =
fixes empty :: "'b"
― ‹-- Represents empty element of the object (for example, for list it is $[]$)›
fixes is_empty :: "'b ⇒ bool"
― ‹-- Function that checks weather the object is empty or not›
fixes of_list :: "'a list ⇒ 'b"
― ‹-- Function transforms given list to desired object (for example,
for heap sort, function {\em of\_list} transforms list to heap)›
fixes multiset :: "'b ⇒ 'a multiset"
― ‹-- Function makes a multiset from the given object. A multiset is a collection without order.›
assumes is_empty_inj: "is_empty e ⟹ e = empty"
― ‹-- It must be assured that the empty element is {\em empty}›
assumes is_empty_empty: "is_empty empty"
― ‹-- Must be satisfied that function {\em is\_empty} returns true for element {\em empty}›
assumes multiset_empty: "multiset empty = {#}"
― ‹-- Multiset of an empty object is empty multiset.›
assumes multiset_of_list: "multiset (of_list i) = mset i"
― ‹-- Multiset of an object gained by
applying function {\em of\_list} must be the same as the multiset of
the list. This, practically, means that function {\em of\_list} does
not delete or change elements of the starting list.›
begin
lemma is_empty_as_list: "is_empty e ⟹ multiset e = {#}"
using is_empty_inj multiset_empty
by auto

definition set :: "'b ⇒ 'a set" where
[simp]: "set l = set_mset (multiset l)"
end

subsection ‹Function remove\_max›

text‹
We wanted to emphasize that algorithms are same. Due to
the complexity of the implementation it usually happens that simple
properties are omitted, such as the connection between these two
sorting algorithms. This is a key feature that should be presented to
students in order to understand these algorithms. It is not unknown
that students usually prefer selection sort for its simplicity whereas
avoid heap sort for its complexity. However, if we can present them as
the algorithms that are same they may hesitate less in using the heap
sort. This is why the refinement is important. Using this technique we
were able to notice these characteristics. Separate verification would
not bring anything new. Being on the abstract level does not only
simplify the verifications, but also helps us to notice and to show
students important features. Even further, we can prove them formally
and completely justify our observation.
›

locale RemoveMax = Collection empty is_empty of_list  multiset for
empty :: "'b" and
is_empty :: "'b ⇒ bool" and
of_list :: "'a::linorder list ⇒ 'b" and
multiset :: "'b ⇒ 'a::linorder multiset" +
fixes remove_max :: "'b ⇒ 'a × 'b"
― ‹--- Function that removes maximum element from the object of type $'b$.
It returns maximum element and the object without that maximum element.›
fixes inv :: "'b ⇒ bool"
― ‹--- It checks weather the object is in required condition.
For example, if we expect to work with heap it checks weather the object
is heap. This is called {\em invariant condition}›
assumes of_list_inv: "inv (of_list x)"
― ‹--- This condition assures that function {\em of\_list}
made a object with desired property.›
assumes remove_max_max:
"⟦¬ is_empty l; inv l; (m, l') = remove_max l⟧ ⟹ m = Max (set l)"
― ‹--- First parameter of the return value of the
function {\em remove\_max} is the maximum element›
assumes remove_max_multiset:
"⟦¬ is_empty l; inv l; (m, l') = remove_max l⟧ ⟹
add_mset m (multiset l') = multiset l"
― ‹--- Condition for multiset, ensures that nothing new is added or nothing
is lost after applying {\em remove\_max} function.›
assumes remove_max_inv:
"⟦¬ is_empty l; inv l; (m, l') = remove_max l⟧ ⟹ inv l'"
― ‹--- Ensures that invariant condition is true after removing maximum element.
Invariant condition must be true in each step of sorting algorithm, for example
if we are sorting using heap than in each iteration we must have heap and function
{\em remove\_max} must not change that.›
begin

lemma remove_max_multiset_size:
"⟦¬ is_empty l; inv l; (m, l') = remove_max l⟧ ⟹
size (multiset l) > size (multiset l')"
using remove_max_multiset[of l m l']

lemma remove_max_set:
"⟦¬ is_empty l; inv l; (m, l') = remove_max l⟧ ⟹
set l' ∪ {m} = set l"
using remove_max_multiset[of l m l']
by (metis Un_insert_right local.set_def set_mset_add_mset_insert sup_bot_right)

text‹As it is said before
in each iteration invariant condition must be satisfied, so the {\em
inv l} is always true, e.g. before and after execution of any
function. This is also the reason why sort function must be defined as
partial. This function parameters stay the same in each step of
iteration -- list stays list, and heap stays heap. As we said before,
in Isabelle/HOL we can only define total function, but there is a
mechanism that enables total function to appear as partial one:›

partial_function (tailrec) ssort' where
"ssort' l sl =
(if is_empty l then
sl
else
let
(m, l') = remove_max l
in
ssort' l' (m # sl))"
declare ssort'.simps[code]
definition ssort :: "'a list ⇒ 'a list" where
"ssort l = ssort' (of_list l) []"

inductive ssort'_dom where
step: "⟦⋀m l'. ⟦¬ is_empty l; (m, l') = remove_max l⟧ ⟹
ssort'_dom (l', m # sl)⟧ ⟹ ssort'_dom (l, sl)"
lemma ssort'_termination:
assumes "inv (fst p)"
shows "ssort'_dom p"
using assms
proof (induct p rule: wf_induct[of "measure (λ(l, sl). size (multiset l))"])
let ?r = "measure (λ(l, sl). size (multiset l))"
fix p :: "'b × 'a list"
assume "inv (fst p)" and *:
"∀y. (y, p) ∈ ?r ⟶ inv (fst y) ⟶ ssort'_dom y"
obtain l sl where "p = (l, sl)"
by (cases p) auto
show "ssort'_dom p"
proof (subst ‹p = (l, sl)›, rule ssort'_dom.step)
fix m l'
assume "¬ is_empty l" "(m, l') = remove_max l"
show "ssort'_dom (l', m#sl)"
proof (rule *[rule_format])
show "((l', m#sl), p) ∈ ?r" "inv (fst (l', m#sl))"
using ‹p = (l, sl)› ‹inv (fst p)› ‹¬ is_empty l›
using ‹(m, l') = remove_max l›
using remove_max_inv[of l m l']
using remove_max_multiset_size[of l m l']
by auto
qed
qed
qed simp

lemma ssort'Induct:
assumes "inv l" "P l sl"
"⋀ l sl m l'.
⟦¬ is_empty l; inv l; (m, l') = remove_max l; P l sl⟧ ⟹ P l' (m # sl)"
shows "P empty (ssort' l sl)"
proof-
from ‹inv l› have "ssort'_dom (l, sl)"
using ssort'_termination
by auto
thus ?thesis
using assms
proof (induct "(l, sl)" arbitrary: l sl rule: ssort'_dom.induct)
case (step l sl)
show ?case
proof (cases "is_empty l")
case True
thus ?thesis
using step(4) step(5) ssort'.simps[of l sl] is_empty_inj[of l]
by simp
next
case False
let ?p = "remove_max l"
let ?m = "fst ?p" and ?l' = "snd ?p"
show ?thesis
using False step(2)[of ?m ?l'] step(3)
using step(4) step(5)[of l ?m ?l' sl] step(5)
using remove_max_inv[of l ?m ?l']
using ssort'.simps[of l sl]
by (cases ?p) auto
qed
qed
qed

lemma mset_ssort':
assumes "inv l"
shows "mset (ssort' l sl) = multiset l + mset sl"
using assms
proof-
have "multiset empty + mset (ssort' l sl) = multiset l + mset sl"
using assms
proof (rule ssort'Induct)
fix l1 sl1 m l'
assume "¬ is_empty l1"
"inv l1"
"(m, l') = remove_max l1"
"multiset l1 + mset sl1 = multiset l + mset sl"
thus "multiset l' + mset (m # sl1) = multiset l + mset sl"
using remove_max_multiset[of l1 m l']
qed simp
thus ?thesis
using multiset_empty
by simp
qed

lemma sorted_ssort':
assumes "inv l" "sorted sl ∧ (∀ x ∈ set l. (∀ y ∈ List.set sl. x ≤ y))"
shows "sorted (ssort' l sl)"
using assms
proof-
have "sorted (ssort' l sl) ∧
(∀ x ∈ set empty. (∀ y ∈ List.set (ssort' l sl). x ≤ y))"
using assms
proof (rule ssort'Induct)
fix l sl m l'
assume "¬ is_empty l"
"inv l"
"(m, l') = remove_max l"
"sorted sl ∧ (∀x∈set l. ∀y∈List.set sl. x ≤ y)"
thus "sorted (m # sl) ∧ (∀x∈set l'. ∀y∈List.set (m # sl). x ≤ y)"
using remove_max_set[of l m l'] remove_max_max[of l m l']
by (auto intro: Max_ge)
qed
thus ?thesis
by simp
qed

lemma sorted_ssort: "sorted (ssort i)"
unfolding ssort_def
using sorted_ssort'[of "of_list i" "[]"] of_list_inv
by auto

lemma permutation_ssort: "mset (ssort l) = mset l"
unfolding ssort_def
using mset_ssort'[of "of_list l" "[]"]
using multiset_of_list of_list_inv
by simp

end

text‹Using assumptions given in the definitions of the locales {\em
Collection} and {\em RemoveMax} for the functions {\em multiset},
{\em is\_empty}, {\em of\_list} and {\em remove\_max} it is no
difficulty to show:›

sublocale RemoveMax < Sort ssort
by (unfold_locales) (auto simp add: sorted_ssort permutation_ssort)

end


# Theory SelectionSort_Functional

(*  Title:      Sort.thy
Author:     Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *)

section ‹Verification of functional Selection Sort›

theory SelectionSort_Functional
imports RemoveMax
begin

subsection ‹Defining data structure›

text‹Selection sort works with list and that is the reason why {\em
Collection} should be interpreted as list.›

interpretation Collection "[]" "λ l. l = []" id mset
by (unfold_locales, auto)

subsection ‹Defining function remove\_max›

text‹The following is definition of {\em remove\_max} function.
The idea is very well known -- assume that the maximum element is the
first one and then compare with each element of the list. Function
{\em f} is one step in iteration, it compares current maximum {\em m}
with one element {\em x}, if it is bigger then {\em m} stays current
maximum and {\em x} is added in the resulting list, otherwise {\em x}
is current maximum and {\em m} is added in the resulting
list.
›

fun f where "f (m, l) x = (if x ≥ m then (x, m#l) else (m, x#l))"

definition remove_max where
"remove_max l = foldl f (hd l, []) (tl l)"

lemma max_Max_commute:
"finite A ⟹ max (Max (insert m A)) x = max m (Max (insert x A))"
apply (cases "A = {}", simp)
by (metis Max_insert max.commute max.left_commute)

text‹The function really returned the
maximum value.›

lemma remove_max_max_lemma:
shows "fst (foldl f (m, t) l) =  Max (set (m # l))"
proof (induct l arbitrary: m t rule: rev_induct)
case (snoc x xs)
let ?a = "foldl f (m, t) xs"
let ?m' = "fst ?a" and ?t' = "snd ?a"
have "fst (foldl f (m, t) (xs @ [x])) = max ?m' x"
by (cases ?a) (auto simp add: max_def)
thus ?case
using snoc
qed simp

lemma remove_max_max:
assumes "l ≠ []" "(m, l') = remove_max l"
shows "m = Max (set l)"
using assms
unfolding remove_max_def
using remove_max_max_lemma[of "hd l" "[]" "tl l"]
using fst_conv[of m l']
by simp

text‹Nothing new is added in the list and noting is deleted
from the list except the maximum element.›

lemma remove_max_mset_lemma:
assumes "(m, l') = foldl f (m', t') l"
shows "mset (m # l') = mset (m' # t' @ l)"
using assms
proof (induct l arbitrary: l' m m' t' rule: rev_induct)
case (snoc x xs)
let ?a = "foldl f (m', t') xs"
let ?m' = "fst ?a" and ?t' = "snd ?a"
have "mset (?m' # ?t') = mset (m' # t' @ xs)"
using snoc(1)[of ?m' ?t' m' t']
by simp
thus ?case
using snoc(2)
apply (cases "?a")
by (auto split: if_split_asm)
qed simp

lemma remove_max_mset:
assumes "l ≠ []" "(m, l') = remove_max l"
shows "add_mset m (mset l') = mset l"
using assms
unfolding remove_max_def
using remove_max_mset_lemma[of m l' "hd l" "[]" "tl l"]
by auto

definition ssf_ssort' where
[simp, code del]: "ssf_ssort' = RemoveMax.ssort' (λ l. l = []) remove_max"
definition ssf_ssort where
[simp, code del]: "ssf_ssort = RemoveMax.ssort (λ l. l = []) id remove_max"

interpretation SSRemoveMax:
RemoveMax "[]" "λ l. l = []" id mset remove_max "λ _. True"
rewrites
"RemoveMax.ssort' (λ l. l = []) remove_max = ssf_ssort'" and
"RemoveMax.ssort (λ l. l = []) id remove_max = ssf_ssort"
using remove_max_max
by (unfold_locales, auto simp add: remove_max_mset)

end


# Theory Heap

(*  Title:      Sort.thy
Author:     Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *)

section ‹Verification of Heap Sort›

theory Heap
imports RemoveMax
begin

subsection ‹Defining tree and properties of heap›

datatype 'a Tree = "E" | "T" 'a "'a Tree" "'a Tree"

text‹With {\em E} is represented empty tree and with {\em T\ \ \ 'a\ \ \ 'a
Tree\ \ \ 'a Tree} is represented a node whose root element is of
type {\em 'a} and its left and right branch is also a tree of
type {\em 'a}.›

primrec size :: "'a Tree ⇒ nat" where
"size E = 0"
| "size (T v l r) = 1 + size l + size r"

text‹Definition of the function that makes a multiset from the given tree:›

primrec multiset where
"multiset E = {#}"
| "multiset (T v l r) = multiset l + {#v#} + multiset r"

primrec val where
"val (T v _ _) = v"

text‹Definition of the function that has the value {\em True} if the tree is
heap, otherwise it is {\em False}:›

fun is_heap :: "'a::linorder Tree ⇒ bool" where
"is_heap E = True"
| "is_heap (T v E E) = True"
| "is_heap (T v E r) = (v ≥ val r ∧ is_heap r)"
| "is_heap (T v l E) = (v ≥ val l ∧ is_heap l)"
| "is_heap (T v l r) = (v ≥ val r ∧ is_heap r ∧ v ≥ val l ∧ is_heap l)"

lemma heap_top_geq:
assumes "a ∈# multiset t" "is_heap t"
shows "val t ≥ a"
using assms
by (induct t rule: is_heap.induct)  (auto split: if_split_asm)

lemma heap_top_max:
assumes "t ≠ E" "is_heap t"
shows "val t = Max_mset (multiset t)"
proof (rule Max_eqI[symmetric])
fix y
assume "y ∈ set_mset (multiset t)"
thus "y ≤ val t"
using heap_top_geq [of y t] ‹is_heap t›
by simp
next
show "val t ∈ set_mset (multiset t)"
using ‹t ≠ E›
by (cases t) auto
qed simp

text‹The next step is to define function {\em remove\_max}, but the
question is weather implementation of {\em remove\_max} depends on
implementation of the functions {\em is\_heap} and {\em multiset}. The
answer is negative. This suggests that another step of refinement
could be added before definition of function {\em
remove\_max}. Additionally, there are other reasons why this should
be done, for example, function {\em remove\_max} could be implemented
in functional or in imperative manner.
›

locale Heap =  Collection empty is_empty of_list  multiset for
empty :: "'b" and
is_empty :: "'b ⇒ bool" and
of_list :: "'a::linorder list ⇒ 'b" and
multiset :: "'b ⇒ 'a::linorder multiset" +
fixes as_tree :: "'b ⇒ 'a::linorder Tree"
― ‹This function is not very important, but it is needed in order to avoide problems with types and to detect that observed object is a tree.›
fixes remove_max :: "'b ⇒ 'a × 'b"
assumes multiset: "multiset l = Heap.multiset (as_tree l)"
assumes is_heap_of_list: "is_heap (as_tree (of_list i))"
assumes as_tree_empty: "as_tree t = E ⟷ is_empty t"
assumes remove_max_multiset':
"⟦¬ is_empty l; (m, l') = remove_max l⟧ ⟹ add_mset m (multiset l') = multiset l"
assumes remove_max_is_heap:
"⟦¬ is_empty l; is_heap (as_tree l); (m, l') = remove_max l⟧ ⟹
is_heap (as_tree l')"
assumes remove_max_val:
"⟦ ¬ is_empty t; (m, t') = remove_max t⟧ ⟹ m = val (as_tree t)"

text‹It is very easy to prove that locale {\em Heap} is sublocale of locale {\em RemoveMax}›

sublocale Heap <
RemoveMax empty is_empty of_list multiset remove_max "λ t. is_heap (as_tree t)"
proof
fix x
show "is_heap (as_tree (of_list x))"
by (rule is_heap_of_list)
next
fix l m l'
assume "¬ is_empty l" "(m, l') = remove_max l"
thus "add_mset m (multiset l') = multiset l"
by (rule remove_max_multiset')
next
fix l m l'
assume "¬ is_empty l" "is_heap (as_tree l)" "(m, l') = remove_max l"
thus "is_heap (as_tree l')"
by (rule remove_max_is_heap)
next
fix l m l'
assume "¬ is_empty l" "is_heap (as_tree l)" "(m, l') = remove_max l"
thus "m = Max (set l)"
unfolding set_def
using heap_top_max[of "as_tree l"] remove_max_val[of l m l']
using multiset is_empty_inj as_tree_empty
by auto
qed

primrec in_tree where
"in_tree v E = False"
| "in_tree v (T v' l r) ⟷ v = v' ∨ in_tree v l ∨ in_tree v r"

lemma is_heap_max:
assumes "in_tree v t" "is_heap t"
shows "val t ≥ v"
using assms
apply (induct t rule:is_heap.induct)
by auto

end


# Theory HeapFunctional

(*  Title:      Sort.thy
Author:     Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *)

section ‹Verification of Functional Heap Sort›

theory HeapFunctional
imports Heap
begin

text‹As we
said before, maximum element of the heap is its root. So, finding
maximum element is not difficulty. But, this element should also be
removed and remainder after deleting this element is two trees, left
and right branch of original heap. Those branches are also heaps by
the definition of the heap. To maintain consistency, branches should
be combined into one tree that satisfies heap condition:›

function merge :: "'a::linorder Tree ⇒ 'a Tree ⇒ 'a Tree" where
"merge t1 E = t1"
| "merge E t2 = t2"
| "merge (T v1 l1 r1) (T v2 l2 r2) =
(if v1 ≥ v2 then T v1 (merge l1 (T v2 l2 r2)) r1
else T v2 (merge l2 (T v1 l1 r1)) r2)"
by (pat_completeness) auto
termination
proof (relation "measure (λ (t1, t2). size t1 + size t2)")
fix v1 l1 r1 v2 l2 r2
assume "v2 ≤ v1"
thus "((l1, T v2 l2 r2), T v1 l1 r1, T v2 l2 r2) ∈
measure (λ(t1, t2). Heap.size t1 + Heap.size t2)"
by auto
next
fix v1 l1 r1 v2 l2 r2
assume "¬ v2 ≤ v1"
thus "((l2, T v1 l1 r1), T v1 l1 r1, T v2 l2 r2) ∈
measure (λ(t1, t2). Heap.size t1 + Heap.size t2)"
by auto
qed simp

lemma merge_val:
"val(merge l r) = val l ∨ val(merge l r) = val r"
proof(induct l r rule:merge.induct)
case (1 l)
thus ?case
by auto
next
case (2 r)
thus ?case
by auto
next
case (3 v1 l1 r1 v2 l2 r2)
thus ?case
proof(cases "v2 ≤ v1")
case True
hence "val (merge (T v1 l1 r1) (T v2 l2 r2)) = val (T v1 l1 r1)"
by auto
thus ?thesis
by auto
next
case False
hence "val (merge (T v1 l1 r1) (T v2 l2 r2)) = val (T v2 l2 r2)"
by auto
thus ?thesis
by auto
qed
qed

text‹Function {\em merge} merges two heaps into one:›

lemma merge_heap_is_heap:
assumes "is_heap l" "is_heap r"
shows "is_heap (merge l r)"
using assms
proof(induct l r rule:merge.induct)
case (1 l)
thus ?case
by auto
next
case (2 r)
thus ?case
by auto
next
case (3 v1 l1 r1 v2 l2 r2)
thus ?case
proof(cases "v2 ≤ v1")
case True
have "is_heap l1"
using ‹is_heap (T v1 l1 r1)›
by (metis Tree.exhaust is_heap.simps(1) is_heap.simps(4) is_heap.simps(5))
hence "is_heap (merge l1 (T v2 l2 r2))"
using True ‹is_heap (T v2 l2 r2)›  3
by auto
have "val (merge l1 (T v2 l2 r2)) = val l1 ∨ val(merge l1 (T v2 l2 r2)) = v2"
using merge_val[of l1 "T v2 l2 r2"]
by auto
show ?thesis
proof(cases "r1 = E")
case True
show ?thesis
proof(cases "l1 = E")
case True
hence "merge (T v1 l1 r1) (T v2 l2 r2) = T v1 (T v2 l2 r2) E"
using ‹r1 = E› ‹v2 ≤ v1›
by auto
thus ?thesis
using 3
using ‹v2 ≤ v1›
by auto
next
case False
hence "v1 ≥ val l1"
using 3(3)
by (metis Tree.exhaust in_tree.simps(2) is_heap_max val.simps)
thus ?thesis
using ‹r1 = E› ‹v1 ≥ v2›
using ‹val (merge l1 (T v2 l2 r2)) = val l1
∨ val(merge l1 (T v2 l2 r2)) = v2›
using ‹is_heap (merge l1 (T v2 l2 r2))›
by (metis False Tree.exhaust is_heap.simps(2)
is_heap.simps(4) merge.simps(3) val.simps)
qed
next
case False
hence "v1 ≥ val r1"
using 3(3)
by (metis Tree.exhaust in_tree.simps(2) is_heap_max val.simps)
show ?thesis
proof(cases "l1 = E")
case True
hence "merge (T v1 l1 r1) (T v2 l2 r2) = T v1 (T v2 l2 r2) r1"
using ‹v2 ≤ v1›
by auto
thus ?thesis
using 3 ‹v1 ≥ val r1›
using ‹v2 ≤ v1›
by (metis False Tree.exhaust Tree.inject Tree.simps(3)
True is_heap.simps(3) is_heap.simps(6) merge.simps(2)
merge.simps(3) order_eq_iff val.simps)
next
case False
hence "v1 ≥ val l1"
using 3(3)
by (metis Tree.exhaust in_tree.simps(2) is_heap_max val.simps)
have "merge l1 (T v2 l2 r2) ≠ E"
using False
by (metis Tree.exhaust Tree.simps(2) merge.simps(3))
have "is_heap r1"
using 3(3)
by (metis False Tree.exhaust ‹r1 ≠ E› is_heap.simps(5))
obtain ll1 lr1 lv1 where "r1 = T lv1 ll1 lr1"
using ‹r1 ≠ E›
by (metis Tree.exhaust)
obtain rl1 rr1 rv1 where "merge l1 (T v2 l2 r2) = T rv1 rl1 rr1"
using ‹merge l1 (T v2 l2 r2) ≠ E›
by (metis Tree.exhaust)
have "val (merge l1 (T v2 l2 r2)) ≤ v1"
using ‹val (merge l1 (T v2 l2 r2)) = val l1 ∨
val(merge l1 (T v2 l2 r2)) = v2›
using ‹v1 ≥ v2› ‹v1 ≥ val l1›
by auto
hence "is_heap (T v1 (merge l1 (T v2 l2 r2)) r1)"
using is_heap.simps(5)[of v1 lv1 ll1 lr1 rv1 rl1  rr1]
using ‹r1 = T lv1 ll1 lr1› ‹merge l1 (T v2 l2 r2) = T rv1 rl1 rr1›
using ‹is_heap r1› ‹is_heap (merge l1 (T v2 l2 r2))› ‹v1 ≥ val r1›
by auto
thus ?thesis
using ‹v2 ≤ v1›
by auto
qed
qed
next
case False
have "is_heap l2"
using 3(4)
by (metis Tree.exhaust is_heap.simps(1)
is_heap.simps(4) is_heap.simps(5))
hence "is_heap (merge l2 (T v1 l1 r1))"
using False ‹is_heap (T v1 l1 r1)›  3
by auto
have "val (merge l2 (T v1 l1 r1)) = val l2 ∨
val(merge l2 (T v1 l1 r1)) = v1"
using merge_val[of l2 "T v1 l1 r1"]
by auto
show ?thesis
proof(cases "r2 = E")
case True
show ?thesis
proof(cases "l2 = E")
case True
hence "merge (T v1 l1 r1) (T v2 l2 r2) = T v2 (T v1 l1 r1) E"
using ‹r2 = E› ‹¬ v2 ≤ v1›
by auto
thus ?thesis
using 3
using ‹¬ v2 ≤ v1›
by auto
next
case False
hence "v2 ≥ val l2"
using 3(4)
by (metis Tree.exhaust in_tree.simps(2) is_heap_max val.simps)
thus ?thesis
using ‹r2 = E› ‹¬ v1 ≥ v2›
using ‹is_heap (merge l2 (T v1 l1 r1))›
using ‹val (merge l2 (T v1 l1 r1)) = val l2 ∨
val(merge l2 (T v1 l1 r1)) = v1›
by (metis False Tree.exhaust is_heap.simps(2)
is_heap.simps(4) linorder_linear merge.simps(3) val.simps)
qed
next
case False
hence "v2 ≥ val r2"
using 3(4)
by (metis Tree.exhaust in_tree.simps(2) is_heap_max val.simps)
show ?thesis
proof(cases "l2 = E")
case True
hence "merge (T v1 l1 r1) (T v2 l2 r2) = T v2 (T v1 l1 r1) r2"
using ‹¬ v2 ≤ v1›
by auto
thus ?thesis
using 3 ‹v2 ≥ val r2›
using ‹¬ v2 ≤ v1›
by (metis False Tree.exhaust Tree.simps(3) is_heap.simps(3)
is_heap.simps(5) linorder_linear val.simps)
next
case False
hence "v2 ≥ val l2"
using 3(4)
by (metis Tree.exhaust in_tree.simps(2) is_heap_max val.simps)
have "merge l2 (T v1 l1 r1) ≠ E"
using False
by (metis Tree.exhaust Tree.simps(2) merge.simps(3))
have "is_heap r2"
using 3(4)
by (metis False Tree.exhaust ‹r2 ≠ E› is_heap.simps(5))
obtain ll1 lr1 lv1 where "r2 = T lv1 ll1 lr1"
using ‹r2 ≠ E›
by (metis Tree.exhaust)
obtain rl1 rr1 rv1 where "merge l2 (T v1 l1 r1) = T rv1 rl1 rr1"
using ‹merge l2 (T v1 l1 r1) ≠ E›
by (metis Tree.exhaust)
have "val (merge l2 (T v1 l1 r1)) ≤ v2"
using ‹val (merge l2 (T v1 l1 r1)) = val l2 ∨
val(merge l2 (T v1 l1 r1)) = v1›
using ‹¬ v1 ≥ v2› ‹v2 ≥ val l2›
by auto
hence "is_heap (T v2 (merge l2 (T v1 l1 r1)) r2)"
using is_heap.simps(5)[of v1 lv1 ll1 lr1 rv1 rl1 rr1]
using ‹r2 = T lv1 ll1 lr1› ‹merge l2 (T v1 l1 r1) = T rv1 rl1 rr1›
using ‹is_heap r2› ‹is_heap (merge l2 (T v1 l1 r1))› ‹v2 ≥ val r2›
by auto
thus ?thesis
using ‹¬ v2 ≤ v1›
by auto
qed
qed
qed
qed

definition insert :: "'a::linorder ⇒ 'a Tree ⇒ 'a Tree" where
"insert v t =  merge t (T v E E)"

primrec hs_of_list where
"hs_of_list [] = E"
| "hs_of_list (v # l) = insert v (hs_of_list l)"

definition hs_is_empty where
[simp]: "hs_is_empty t ⟷  t = E"

text‹Definition of function {\em remove\_max}:›

fun hs_remove_max:: "'a::linorder Tree ⇒ 'a × 'a Tree"  where
"hs_remove_max (T v l r) = (v, merge l r)"

lemma merge_multiset:
"multiset l + multiset g = multiset (merge l g)"
proof(induct l g rule:merge.induct)
case (1 l)
thus ?case
by auto
next
case (2 g)
thus ?case
by auto
next
case (3 v1 l1 r1 v2 l2 r2)
thus ?case
proof(cases "v2 ≤ v1")
case  True
hence "multiset (merge (T v1 l1 r1) (T v2 l2 r2)) =
{#v1#} + multiset (merge l1 (T v2 l2 r2)) +  multiset r1"
by auto
hence "multiset (merge (T v1 l1 r1) (T v2 l2 r2)) =
{#v1#} + multiset l1 + multiset (T v2 l2 r2) + multiset r1"
using 3 True
by (metis union_assoc)
hence "multiset (merge (T v1 l1 r1) (T v2 l2 r2)) =
{#v1#} + multiset l1 + multiset r1 + multiset (T v2 l2 r2)"
by (metis union_commute union_lcomm)
thus ?thesis
by auto
next
case False
hence "multiset (merge (T v1 l1 r1) (T v2 l2 r2)) =
{#v2#} + multiset (merge l2 (T v1 l1 r1)) + multiset r2"
by auto
hence "multiset (merge (T v1 l1 r1) (T v2 l2 r2)) =
{#v2#} + multiset l2 + multiset r2 +  multiset (T v1 l1 r1)"
using 3 False
by (metis union_commute union_lcomm)
thus ?thesis
by (metis multiset.simps(2) union_commute)
qed
qed

text‹Proof that defined functions are interpretation of abstract functions from locale {\em Collection}:›

interpretation HS: Collection "E" hs_is_empty hs_of_list multiset
proof
fix t
assume "hs_is_empty t"
thus "t = E"
by auto
next
show "hs_is_empty E"
by auto
next
show "multiset E = {#}"
by auto
next
fix l
show "multiset (hs_of_list l) = mset l"
proof(induct l)
case Nil
thus ?case
by auto
next
case (Cons a l)
have "multiset (hs_of_list (a # l)) = multiset (hs_of_list l) + {#a#}"
using merge_multiset[of "hs_of_list l" "T a E E"]
apply auto
unfolding insert_def
by auto
thus ?case
using Cons
by auto
qed
qed

text‹Proof that defined functions are interpretation of abstract functions from locale {\em Heap}:›

interpretation Heap "E" hs_is_empty hs_of_list multiset id hs_remove_max
proof
fix l
show "multiset l = Heap.multiset (id l)"
by auto
next
fix l
show "is_heap (id (hs_of_list l))"
proof(induct l)
case Nil
thus ?case
by auto
next
case (Cons a l)
have "hs_of_list (a # l) = merge (hs_of_list l) (T a E E)"
apply auto
unfolding insert_def
by auto
have "is_heap (T a E E)"
by auto
hence "is_heap (merge (hs_of_list l) (T a E E))"
using Cons merge_heap_is_heap[of "hs_of_list l" "T a E E"]
by auto
thus ?case
using ‹hs_of_list (a # l) = merge (hs_of_list l) (T a E E)›
by auto
qed
next
fix t
show " (id t = E) = hs_is_empty t"
by auto
next
fix t m t'
assume "¬ hs_is_empty t" "(m, t') = hs_remove_max t"
then obtain l r where "t = T m l r"
by (metis Pair_inject Tree.exhaust hs_is_empty_def hs_remove_max.simps)
thus "add_mset m (multiset t') = multiset t"
using merge_multiset[of l r]
using ‹(m, t') = hs_remove_max t›
by auto
next
fix t m t'
assume "¬ hs_is_empty t" "is_heap (id t)" "(m, t') = hs_remove_max t"
then obtain v l r where "t = T v l r"
by (metis Tree.exhaust hs_is_empty_def)
hence "t' = merge l r"
using ‹(m, t') = hs_remove_max t›
by auto
have "is_heap l ∧ is_heap r"
using ‹is_heap (id t)›
using ‹t = T v l r›
by (metis Tree.exhaust id_apply is_heap.simps(1)
is_heap.simps(3) is_heap.simps(4) is_heap.simps(5))
thus "is_heap (id t')"
using ‹t' = merge l r›
using merge_heap_is_heap
by auto
next
fix t m t'
assume "¬ hs_is_empty t" "(m, t') = hs_remove_max t"
thus "m = val (id t)"
by (metis Pair_inject Tree.exhaust hs_is_empty_def
hs_remove_max.simps id_apply val.simps)
qed

end


# Theory HeapImperative

(*  Title:      Sort.thy
Author:     Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *)

section ‹Verification of Imperative Heap Sort›

theory HeapImperative
imports Heap
begin

primrec left :: "'a Tree ⇒ 'a Tree" where
"left (T v l r) = l"

abbreviation left_val :: "'a Tree ⇒ 'a" where
"left_val t ≡ val (left t)"

primrec right :: "'a Tree ⇒ 'a Tree" where
"right (T v l r) = r"

abbreviation right_val :: "'a Tree ⇒ 'a" where
"right_val t ≡ val (right t)"

abbreviation set_val :: "'a Tree ⇒ 'a ⇒ 'a Tree" where
"set_val t x ≡ T x (left t) (right t)"

text‹The first step is to implement function {\em siftDown}. If some node
does not satisfy heap property, this function moves it down the heap
until it does. For a node is checked weather it satisfies heap property or not. If it
does nothing is changed. If it does not, value of the root node
becomes a value of the larger child and the value of that child
becomes the value of the root node. This is the reason this function
is called {\tt siftDown} -- value of the node is places down in the
heap. Now, the problem is that the child node may not satisfy the heap
property and that is the reason why function {\tt siftDown} is
recursively applied.›

fun siftDown :: "'a::linorder Tree ⇒ 'a Tree" where
"siftDown E = E"
|  "siftDown (T v E E) = T v E E"
|  "siftDown (T v l E) =
(if v ≥ val l then T v l E else T (val l) (siftDown (set_val l v)) E)"
|  "siftDown (T v E r) =
(if v ≥ val r then T v E r else T (val r) E (siftDown (set_val r v)))"
|  "siftDown (T v l r) =
(if val l ≥ val r then
if v ≥ val l then T v l r else T (val l) (siftDown (set_val l v)) r
else
if v ≥ val r then T v l r else T (val r) l (siftDown (set_val r v)))"

lemma siftDown_Node:
assumes "t = T v l r"
shows "∃ l' v' r'. siftDown t = T v' l' r' ∧ v' ≥ v"
using assms
apply(induct t rule:siftDown.induct)
by auto

lemma siftDown_in_tree:
assumes "t ≠ E"
shows "in_tree (val (siftDown t)) t"
using assms
apply(induct t rule:siftDown.induct)
by auto

lemma siftDown_in_tree_set:
shows "in_tree v t ⟷ in_tree v (siftDown t)"
proof
assume "in_tree v t"
thus "in_tree v (siftDown t)"
apply (induct t rule:siftDown.induct)
by auto
next
assume " in_tree v (siftDown t)"
thus "in_tree v t"
proof (induct t rule:siftDown.induct)
case 1
thus ?case
by auto
next
case (2 v1)
thus ?case
by auto
next
case (3 v2 v1 l1 r1)
show ?case
proof(cases "v2 ≥ v1")
case True
thus ?thesis
using 3
by auto
next
case False
show ?thesis
proof(cases "v1 = v")
case True
thus ?thesis
using 3 False
by auto
next
case False
hence "in_tree v (siftDown (set_val (T v1 l1 r1) v2))"
using ‹¬ v2 ≥ v1› 3(2)
by auto
hence "in_tree v (T v2 l1 r1)"
using 3(1) ‹¬ v2 ≥ v1›
by auto
thus ?thesis
proof(cases "v2 = v")
case True
thus ?thesis
by auto
next
case False
hence "in_tree v (T v1 l1 r1)"
using ‹in_tree v (T v2 l1 r1)›
by auto
thus ?thesis
by auto
qed
qed
qed
next
case (4 v2 v1 l1 r1)
show ?case
proof(cases "v2 ≥ v1")
case True
thus ?thesis
using 4
by auto
next
case False
show ?thesis
proof(cases "v1 = v")
case True
thus ?thesis
using 4 False
by auto
next
case False
hence "in_tree v (siftDown (set_val (T v1 l1 r1) v2))"
using ‹¬ v2 ≥ v1› 4(2)
by auto
hence "in_tree v (T v2 l1 r1)"
using 4(1) ‹¬ v2 ≥ v1›
by auto
thus ?thesis
proof(cases "v2 = v")
case True
thus ?thesis
by auto
next
case False
hence "in_tree v (T v1 l1 r1)"
using ‹in_tree v (T v2 l1 r1)›
by auto
thus ?thesis
by auto
qed
qed
qed
next
case ("5_1" v' v1 l1 r1 v2 l2 r2)
show ?case
proof(cases "v = v' ∨ v= v1 ∨ v = v2")
case True
thus ?thesis
by auto
next
case False
show ?thesis
proof(cases "v1 ≥ v2")
case True
show ?thesis
proof(cases "v' ≥ v1")
case True
thus ?thesis
using ‹v1 ≥ v2› "5_1"
by auto
next
case False
thus ?thesis
proof(cases "in_tree v (T v2 l2 r2)")
case True
thus ?thesis
by auto
next
case False
hence "in_tree v (siftDown (set_val (T v1 l1 r1) v'))"
using "5_1"(3) ‹¬ in_tree v (T v2 l2 r2)› ‹v1 ≥ v2› ‹¬ v' ≥ v1›
using ‹ ¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
hence "in_tree v (T v' l1 r1)"
using "5_1"(1) ‹v1 ≥ v2› ‹¬ v' ≥ v1›
by auto
hence "in_tree v (T v1 l1 r1)"
using  ‹¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
thus ?thesis
by auto
qed
qed
next
case False
show ?thesis
proof(cases "v' ≥ v2")
case True
thus ?thesis
using ‹¬ v1 ≥ v2› "5_1"
by auto
next
case False
thus ?thesis
proof(cases "in_tree v (T v1 l1 r1)")
case True
thus ?thesis
by auto
next
case False
hence "in_tree v (siftDown (set_val (T v2 l2 r2) v'))"
using "5_1"(3) ‹¬ in_tree v (T v1 l1 r1)› ‹¬ v1 ≥ v2› ‹¬ v' ≥ v2›
using ‹ ¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
hence "in_tree v (T v' l2 r2)"
using "5_1"(2) ‹¬ v1 ≥ v2› ‹¬ v' ≥ v2›
by auto
hence "in_tree v (T v2 l2 r2)"
using  ‹¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
thus ?thesis
by auto
qed
qed
qed
qed
next
case ("5_2" v' v1 l1 r1 v2 l2 r2)
show ?case
proof(cases "v = v' ∨ v= v1 ∨ v = v2")
case True
thus ?thesis
by auto
next
case False
show ?thesis
proof(cases "v1 ≥ v2")
case True
show ?thesis
proof(cases "v' ≥ v1")
case True
thus ?thesis
using ‹v1 ≥ v2› "5_2"
by auto
next
case False
thus ?thesis
proof(cases "in_tree v (T v2 l2 r2)")
case True
thus ?thesis
by auto
next
case False
hence "in_tree v (siftDown (set_val (T v1 l1 r1) v'))"
using "5_2"(3) ‹¬ in_tree v (T v2 l2 r2)› ‹v1 ≥ v2› ‹¬ v' ≥ v1›
using ‹ ¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
hence "in_tree v (T v' l1 r1)"
using "5_2"(1) ‹v1 ≥ v2› ‹¬ v' ≥ v1›
by auto
hence "in_tree v (T v1 l1 r1)"
using  ‹¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
thus ?thesis
by auto
qed
qed
next
case False
show ?thesis
proof(cases "v' ≥ v2")
case True
thus ?thesis
using ‹¬ v1 ≥ v2› "5_2"
by auto
next
case False
thus ?thesis
proof(cases "in_tree v (T v1 l1 r1)")
case True
thus ?thesis
by auto
next
case False
hence "in_tree v (siftDown (set_val (T v2 l2 r2) v'))"
using "5_2"(3) ‹¬ in_tree v (T v1 l1 r1)› ‹¬ v1 ≥ v2› ‹¬ v' ≥ v2›
using ‹ ¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
hence "in_tree v (T v' l2 r2)"
using "5_2"(2) ‹¬ v1 ≥ v2› ‹¬ v' ≥ v2›
by auto
hence "in_tree v (T v2 l2 r2)"
using  ‹¬ (v = v' ∨ v = v1 ∨ v = v2)›
by auto
thus ?thesis
by auto
qed
qed
qed
qed
qed
qed

lemma siftDown_heap_is_heap:
assumes "is_heap l" "is_heap r" "t = T v l r"
shows "is_heap (siftDown t)"
using assms
proof (induct t arbitrary: v l r  rule:siftDown.induct)
case 1
thus ?case
by simp
next
case (2 v')
show ?case
by simp
next
case (3 v2 v1 l1 r1)
show ?case
proof (cases "v2 ≥ v1")
case True
thus ?thesis
using 3(2) 3(4)
by auto
next
case False
show ?thesis
proof-
let ?t = "siftDown (T v2 l1 r1)"
obtain l' v' r' where *: "?t = T v' l' r'" "v' ≥ v2"
using siftDown_Node[of "T v2 l1 r1" v2 l1 r1]
by auto
have "l = T v1 l1 r1"
using 3(4)
by auto
hence "is_heap l1" "is_heap r1"
using 3(2)
apply (induct l rule:is_heap.induct)
by auto
hence "is_heap ?t"
using 3(1)[of l1 r1 v2] False 3
by auto
show ?thesis
proof (cases "v' = v2")
case True
thus ?thesis
using False ‹is_heap ?t› *
by auto
next
case False
have "in_tree v' ?t"
using *
using siftDown_in_tree[of ?t]
by simp
hence "in_tree v' (T v2 l1 r1)"
using siftDown_in_tree_set[symmetric, of v' "T v2 l1 r1"]
by auto
hence "in_tree v' (T v1 l1 r1)"
using False
by simp
hence "v1 ≥ v'"
using 3
using is_heap_max[of v' "T v1 l1 r1"]
by auto
thus ?thesis
using ‹is_heap ?t› * ‹¬ v2 ≥ v1›
by auto
qed
qed
qed
next
case (4 v2 v1 l1 r1)
show ?case
proof(cases "v2 ≥ v1")
case True
thus ?thesis
using 4(2-4)
by auto
next
case False
let ?t = "siftDown (T v2 l1 r1)"
obtain v' l' r' where *: "?t = T v' l' r'" "v' ≥ v2"
using siftDown_Node[of "T v2 l1 r1" v2 l1 r1]
by auto
have "r = T v1 l1 r1"
using 4(4)
by auto
hence "is_heap l1" "is_heap r1"
using 4(3)
apply (induct r rule:is_heap.induct)
by auto
hence "is_heap ?t"
using False  4(1)[of l1 r1 v2]
by auto
show ?thesis
proof(cases "v' = v2")
case True
thus ?thesis
using * ‹is_heap ?t› False
by auto
next
case False
have "in_tree v' ?t"
using *
using siftDown_in_tree[of ?t]
by auto
hence "in_tree v' (T v2 l1 r1)"
using * siftDown_in_tree_set[of v' "T v2 l1 r1"]
by auto
hence "in_tree v' (T v1 l1 r1)"
using False
by auto
hence "v1 ≥ v'"
using is_heap_max[of v' "T v1 l1 r1"] 4
by auto
thus ?thesis
using ‹is_heap ?t› False *
by auto
qed
qed
next
case ("5_1" v1 v2 l2 r2 v3 l3 r3)
show ?case
proof(cases "v2 ≥ v3")
case True
show ?thesis
proof(cases "v1 ≥ v2")
case True
thus ?thesis
using ‹v2 ≥ v3› "5_1"
by auto
next
case False
let ?t = "siftDown (T v1 l2 r2)"
obtain l' v' r' where *: "?t = T v' l' r'" "v' ≥ v1"
using siftDown_Node
by blast
have "is_heap l2" "is_heap r2"
using "5_1"(3, 5)
apply(induct l rule:is_heap.induct)
by auto
hence "is_heap ?t"
using "5_1"(1)[of l2 r2 v1] ‹v2 ≥ v3› False
by auto
have "v2 ≥ v'"
proof(cases "v' = v1")
case True
thus ?thesis
using False
by auto
next
case False
have "in_tree v' ?t"
using * siftDown_in_tree
by auto
hence "in_tree v' (T v1 l2 r2)"
using siftDown_in_tree_set[of v' "T v1 l2 r2"]
by auto
hence "in_tree v' (T v2 l2 r2)"
using False
by auto
thus ?thesis
using is_heap_max[of v' "T v2 l2 r2"] "5_1"
by auto
qed
thus ?thesis
using ‹is_heap ?t› ‹v2 ≥ v3› * False "5_1"
by auto
qed
next
case False
show ?thesis
proof(cases "v1 ≥ v3")
case True
thus ?thesis
using ‹¬ v2 ≥ v3› "5_1"
by auto
next
case False
let ?t = "siftDown (T v1 l3 r3)"
obtain l' v' r' where *: "?t = T v' l' r'" "v' ≥ v1"
using siftDown_Node
by blast
have "is_heap l3" "is_heap r3"
using "5_1"(4, 5)
apply(induct r rule:is_heap.induct)
by auto
hence "is_heap ?t"
using "5_1"(2)[of l3 r3 v1] ‹¬ v2 ≥ v3› False
by auto
have "v3 ≥ v'"
proof(cases "v' = v1")
case True
thus ?thesis
using False
by auto
next
case False
have "in_tree v' ?t"
using * siftDown_in_tree
by auto
hence "in_tree v' (T v1 l3 r3)"
using siftDown_in_tree_set[of v' "T v1 l3 r3"]
by auto
hence "in_tree v' (T v3 l3 r3)"
using False
by auto
thus ?thesis
using is_heap_max[of v' "T v3 l3 r3"] "5_1"
by auto
qed
thus ?thesis
using ‹is_heap ?t› ‹¬ v2 ≥ v3› * False "5_1"
by auto
qed
qed
next
case ("5_2" v1 v2 l2 r2 v3 l3 r3)
show ?case
proof(cases "v2 ≥ v3")
case True
show ?thesis
proof(cases "v1 ≥ v2")
case True
thus ?thesis
using ‹v2 ≥ v3› "5_2"
by auto
next
case False
let ?t = "siftDown (T v1 l2 r2)"
obtain l' v' r' where *: "?t = T v' l' r'" "v1 ≤ v'"
using siftDown_Node
by blast
have "is_heap l2" "is_heap r2"
using "5_2"(3, 5)
apply(induct l rule:is_heap.induct)
by auto
hence "is_heap ?t"
using "5_2"(1)[of l2 r2 v1] ‹v2 ≥ v3› False
by auto
have "v2 ≥ v'"
proof(cases "v' = v1")
case True
thus ?thesis
using False
by auto
next
case False
have "in_tree v' ?t"
using * siftDown_in_tree
by auto
hence "in_tree v' (T v1 l2 r2)"
using siftDown_in_tree_set[of v' "T v1 l2 r2"]
by auto
hence "in_tree v' (T v2 l2 r2)"
using False
by auto
thus ?thesis
using is_heap_max[of v' "T v2 l2 r2"] "5_2"
by auto
qed
thus ?thesis
using ‹is_heap ?t› ‹v2 ≥ v3› * False "5_2"
by auto
qed
next
case False
show ?thesis
proof(cases "v1 ≥ v3")
case True
thus ?thesis
using ‹¬ v2 ≥ v3› "5_2"
by auto
next
case False
let ?t = "siftDown (T v1 l3 r3)"
obtain l' v' r' where *: "?t = T v' l' r'" "v' ≥ v1"
using siftDown_Node
by blast
have "is_heap l3" "is_heap r3"
using "5_2"(4, 5)
apply(induct r rule:is_heap.induct)
by auto
hence "is_heap ?t"
using "5_2"(2)[of l3 r3 v1] ‹¬ v2 ≥ v3› False
by auto
have "v3 ≥ v'"
proof(cases "v' = v1")
case True
thus ?thesis
using False
by auto
next
case False
have "in_tree v' ?t"
using * siftDown_in_tree
by auto
hence "in_tree v' (T v1 l3 r3)"
using siftDown_in_tree_set[of v' "T v1 l3 r3"]
by auto
hence "in_tree v' (T v3 l3 r3)"
using False
by auto
thus ?thesis
using is_heap_max[of v' "T v3 l3 r3"] "5_2"
by auto
qed
thus ?thesis
using ‹is_heap ?t› ‹¬ v2 ≥ v3› * False "5_2"
by auto
qed
qed
qed

text‹Definition of the function {\em heapify} which
makes a heap from any given binary tree.›

primrec heapify where
"heapify E = E"
|  "heapify (T v l r) = siftDown (T v (heapify l) (heapify r))"

lemma heapify_heap_is_heap:
"is_heap (heapify t)"
proof(induct t)
case E
thus ?case
by auto
next
case (T v l r)
thus ?case
using siftDown_heap_is_heap[of "heapify l" "heapify r" "T v (heapify l) (heapify r)" v]
by auto
qed

text‹Definition of {\em removeLeaf} function.  Function returns two values. The first one
is the value of romoved leaf element. The second returned value is tree without that leaf.›

fun removeLeaf:: "'a::linorder Tree ⇒ 'a × 'a Tree" where
"removeLeaf (T v E E) = (v, E)"
| "removeLeaf (T v l E) = (fst (removeLeaf l), T v (snd (removeLeaf l)) E)"
| "removeLeaf (T v E r) = (fst (removeLeaf r), T v E (snd (removeLeaf r)))"
| "removeLeaf (T v l r) = (fst (removeLeaf l), T v (snd (removeLeaf l)) r)"

text‹Function {\em of\_list\_tree} makes a binary tree from any given
list.›

primrec of_list_tree:: "'a::linorder list ⇒ 'a Tree" where
"of_list_tree [] = E"
| "of_list_tree (v # tail) = T v (of_list_tree tail) E"

text‹By applying {\em heapify} binary tree is transformed into
heap.›

definition hs_of_list where
"hs_of_list l = heapify (of_list_tree l)"

text‹Definition of function {\em hs\_remove\_max}. As it is already well
established, finding maximum is not a problem, since it is in the root
element of the heap. The root element is replaced with leaf of the
heap and that leaf is erased from its previous position. However, now
the new root element may not satisfy heap property and that is the
reason to apply function {\em siftDown}.›

definition hs_remove_max :: "'a::linorder Tree ⇒ 'a × 'a Tree" where
"hs_remove_max t ≡
(let v' = fst (removeLeaf t);
t' = snd (removeLeaf t) in
(if t' = E then (val t, E)
else (val t, siftDown (set_val t' v'))))"

definition hs_is_empty where
[simp]: "hs_is_empty t ⟷  t = E"

lemma siftDown_multiset:
"multiset (siftDown t) = multiset t"
proof(induct t rule:siftDown.induct)
case 1
thus ?case
by simp
next
case (2 v)
thus ?case
by simp
next
case (3 v1 v l r)
thus ?case
proof(cases "v ≤ v1")
case True
thus ?thesis
by auto
next
case False
hence "multiset (siftDown (T v1 (T v l r) E)) =
multiset l + {#v1#} + multiset r + {#v#}"
using 3
by auto
moreover
have "multiset (T v1 (T v l r) E) =
multiset l + {#v#} + multiset r + {#v1#}"
by auto
moreover
have "multiset l + {#v1#} + multiset r + {#v#} =
multiset l + {#v#} + multiset r + {#v1#}"
by (metis union_commute union_lcomm)
ultimately
show ?thesis
by auto
qed
next
case (4 v1 v l r)
thus ?case
proof(cases "v ≤ v1")
case True
thus ?thesis
by auto
next
case False
have "multiset (set_val (T v l r) v1) =
multiset l + {#v1#} + multiset r"
by auto
hence "multiset (siftDown (T v1 E (T v l r))) =
{#v#} +  multiset (set_val (T v l r) v1)"
using 4 False
by auto
hence "multiset (siftDown (T v1 E (T v l r))) =
{#v#} + multiset l + {#v1#} + multiset r"
using ‹multiset (set_val (T v l r) v1) =
multiset l + {#v1#} + multiset r›
by (metis union_commute union_lcomm)
moreover
have "multiset (T v1 E (T v l r)) =
{#v1#} + multiset l + {#v#} + multiset r"
multiset.simps(1) multiset.simps(2) union_commute union_lcomm)
moreover
have "{#v#} + multiset l + {#v1#} + multiset r =
{#v1#} + multiset l + {#v#} + multiset r"
by (metis union_commute union_lcomm)
ultimately
show ?thesis
by auto
qed
next
case ("5_1" v v1 l1 r1 v2 l2 r2)
thus ?case
proof(cases "v1 ≥ v2")
case True
thus ?thesis
proof(cases "v ≥ v1")
case True
thus ?thesis
using ‹v1 ≥ v2›
by auto
next
case False
hence "multiset (siftDown (T v (T v1 l1 r1) (T v2 l2 r2))) =
multiset l1 + {#v#} + multiset r1 + {#v1#} +
multiset (T v2 l2 r2)"
using ‹v1 ≥ v2› "5_1"(1)
by auto
moreover
have "multiset (T v (T v1 l1 r1) (T v2 l2 r2)) =
multiset l1 + {#v1#} + multiset r1 + {#v#} +
multiset(T v2 l2 r2)"
by auto
moreover
have "multiset l1 + {#v1#} + multiset r1 + {#v#} +
multiset(T v2 l2 r2) =
multiset l1 + {#v#} + multiset r1 + {#v1#} +
multiset (T v2 l2 r2)"
by (metis union_commute union_lcomm)
ultimately
show ?thesis
by auto
qed
next
case False
show ?thesis
proof(cases "v ≥ v2")
case True
thus ?thesis
using False
by auto
next
case False
hence "multiset (siftDown (T v (T v1 l1 r1) (T v2 l2 r2))) =
multiset (T v1 l1 r1) + {#v2#} +
multiset l2 + {#v#} + multiset r2"
using ‹¬ v1 ≥ v2› "5_1"(2)
moreover
have
"multiset (T v (T v1 l1 r1) (T v2 l2 r2)) =
multiset (T v1 l1 r1) + {#v#} + multiset l2 +
{#v2#} + multiset r2"
by simp
moreover
have
"multiset (T v1 l1 r1) + {#v#} + multiset l2 + {#v2#} +
multiset r2 =
multiset (T v1 l1 r1) + {#v2#} + multiset l2 +
{#v#} + multiset r2"
by (metis union_commute union_lcomm)
ultimately
show ?thesis
by auto
qed
qed
next
case ("5_2" v v1 l1 r1 v2 l2 r2)
thus ?case
proof(cases "v1 ≥ v2")
case True
thus ?thesis
proof(cases "v ≥ v1")
case True
thus ?thesis
using ‹v1 ≥ v2›
by auto
next
case False
hence "multiset (siftDown (T v (T v1 l1 r1) (T v2 l2 r2))) =
multiset l1 + {#v#} + multiset r1 + {#v1#} +
multiset (T v2 l2 r2)"
using ‹v1 ≥ v2› "5_2"(1)
by auto
moreover
have "multiset (T v (T v1 l1 r1) (T v2 l2 r2)) =
multiset l1 + {#v1#} + multiset r1 +
{#v#} + multiset(T v2 l2 r2)"
by auto
moreover
have "multiset l1 + {#v1#} + multiset r1 + {#v#} +
multiset(T v2 l2 r2) =
multiset l1 + {#v#} + multiset r1 + {#v1#} +
multiset (T v2 l2 r2)"
by (metis union_commute union_lcomm)
ultimately
show ?thesis
by auto
qed
next
case False
show ?thesis
proof(cases "v ≥ v2")
case True
thus ?thesis
using False
by auto
next
case False
hence "multiset (siftDown (T v (T v1 l1 r1) (T v2 l2 r2))) =
multiset (T v1 l1 r1) + {#v2#} + multiset l2 + {#v#} +
multiset r2"
using ‹¬ v1 ≥ v2› "5_2"(2)
moreover
have "multiset (T v (T v1 l1 r1) (T v2 l2 r2)) =
multiset (T v1 l1 r1) + {#v#} + multiset l2 + {#v2#} +
multiset r2"
by simp
moreover
have "multiset (T v1 l1 r1) + {#v#} + multiset l2 + {#v2#} +
multiset r2 =
multiset (T v1 l1 r1) + {#v2#} + multiset l2 + {#v#} +
multiset r2"
by (metis union_commute union_lcomm)
ultimately
show ?thesis
by auto
qed
qed
qed

lemma mset_list_tree:
"multiset (of_list_tree l) = mset l"
proof(induct l)
case Nil
thus ?case
by auto
next
case (Cons v tail)
hence "multiset (of_list_tree (v # tail)) = mset tail + {#v#}"
by auto
also have "... = mset (v # tail)"
by auto
finally show "multiset (of_list_tree (v # tail)) = mset (v # tail)"
by auto
qed

lemma multiset_heapify:
"multiset (heapify t) = multiset t"
proof(induct t)
case E
thus ?case
by auto
next
case (T v l r)
hence "multiset (heapify (T v l r)) = multiset l + {#v#} + multiset r"
using siftDown_multiset[of "T v (heapify l) (heapify r)"]
by auto
thus ?case
by auto
qed

lemma multiset_heapify_of_list_tree:
"multiset (heapify (of_list_tree l)) = mset l"
using multiset_heapify[of "of_list_tree l"]
using mset_list_tree[of l]
by auto

lemma removeLeaf_val_val:
assumes "snd (removeLeaf t) ≠ E" "t ≠ E"
shows "val t = val (snd (removeLeaf t))"
using assms
apply (induct t rule:removeLeaf.induct)
by auto

lemma removeLeaf_heap_is_heap:
assumes "is_heap t" "t ≠ E"
shows "is_heap (snd (removeLeaf t))"
using assms
proof(induct t rule:removeLeaf.induct)
case (1 v)
thus ?case
by auto
next
case (2 v v1 l1 r1)
have "is_heap (T v1 l1 r1)"
using 2(3)
by auto
hence "is_heap (snd (removeLeaf (T v1 l1 r1)))"
using 2(1)
by auto
let ?t = "(snd (removeLeaf (T v1 l1 r1)))"
show ?case
proof(cases "?t = E")
case True
thus ?thesis
by auto
next
case False
have "v ≥ v1"
using 2(3)
by auto
hence "v ≥ val ?t"
using False removeLeaf_val_val[of "T v1 l1 r1"]
by auto
hence "is_heap (T v (snd (removeLeaf (T v1 l1 r1))) E)"
using ‹is_heap (snd (removeLeaf (T v1 l1 r1)))›
by (metis Tree.exhaust is_heap.simps(2) is_heap.simps(4))
thus ?thesis
using 2
by auto
qed
next
case (3 v v1 l1 r1)
have "is_heap (T v1 l1 r1)"
using 3(3)
by auto
hence "is_heap (snd (removeLeaf (T v1 l1 r1)))"
using 3(1)
by auto
let ?t = "(snd (removeLeaf (T v1 l1 r1)))"
show ?case
proof(cases "?t = E")
case True
thus ?thesis
by auto
next
case False
have "v ≥ v1"
using 3(3)
by auto
hence "v ≥ val ?t"
using False removeLeaf_val_val[of "T v1 l1 r1"]
by auto
hence "is_heap (T v E (snd (removeLeaf (T v1 l1 r1))))"
using ‹is_heap (snd (removeLeaf (T v1 l1 r1)))›
by (metis False Tree.exhaust is_heap.simps(3))
thus ?thesis
using 3
by auto
qed
next
case ("4_1" v v1 l1 r1 v2 l2 r2)
have "is_heap (T v1 l1 r1)" "is_heap (T v2 l2 r2)" "v ≥ v1" "v ≥ v2"
using "4_1"(3)
hence "is_heap (snd (removeLeaf (T v1 l1 r1)))"
using "4_1"(1)
by auto
let ?t = "(snd (removeLeaf (T v1 l1 r1)))"
show ?case
proof(cases "?t = E")
case True
thus ?thesis
using ‹is_heap (T v2 l2 r2)› ‹v ≥ v2›
by auto
next
case False
then obtain v1' l1' r1' where "?t = T v1' l1' r1'"
by (metis Tree.exhaust)
hence "is_heap (T v1' l1' r1')"
using ‹is_heap (snd (removeLeaf (T v1 l1 r1)))›
by auto
have "v ≥ v1"
using "4_1"(3)
by auto
hence "v ≥ val ?t"
using False removeLeaf_val_val[of "T v1 l1 r1"]
by auto
hence "v ≥ v1'"
using ‹?t = T v1' l1' r1'›
by auto
hence "is_heap (T v (T v1' l1' r1') (T v2 l2 r2))"
using ‹is_heap (T v1' l1' r1')›
using ‹is_heap (T v2 l2 r2)› ‹v ≥ v2›
thus ?thesis
using "4_1" ‹?t = T v1' l1' r1'›
by auto
qed
next
case ("4_2" v v1 l1 r1 v2 l2 r2)
have "is_heap (T v1 l1 r1)" "is_heap (T v2 l2 r2)" "v ≥ v1" "v ≥ v2"
using "4_2"(3)
hence "is_heap (snd (removeLeaf (T v1 l1 r1)))"
using "4_2"(1)
by auto
let ?t = "(snd (removeLeaf (T v1 l1 r1)))"
show ?case
proof(cases "?t = E")
case True
thus ?thesis
using ‹is_heap (T v2 l2 r2)› ‹v ≥ v2›
by auto
next
case False
then obtain v1' l1' r1' where "?t = T v1' l1' r1'"
by (metis Tree.exhaust)
hence "is_heap (T v1' l1' r1')"
using ‹is_heap (snd (removeLeaf (T v1 l1 r1)))›
by auto
have "v ≥ v1"
using "4_2"(3)
by auto
hence "v ≥ val ?t"
using False removeLeaf_val_val[of "T v1 l1 r1"]
by auto
hence "v ≥ v1'"
using ‹?t = T v1' l1' r1'›
by auto
hence "is_heap (T v (T v1' l1' r1') (T v2 l2 r2))"
using ‹is_heap (T v1' l1' r1')›
using ‹is_heap (T v2 l2 r2)› ‹v ≥ v2›
thus ?thesis
using "4_2" ‹?t = T v1' l1' r1'›
by auto
qed
next
case 5
thus ?case
by auto
qed

text‹Difined functions satisfy conditions of locale {\em Collection} and thus represent
interpretation of this locale.›

interpretation HS: Collection "E" hs_is_empty hs_of_list multiset
proof
fix t
assume "hs_is_empty t"
thus "t = E"
by auto
next
show "hs_is_empty E"
by auto
next
show "multiset E = {#}"
by auto
next
fix l
show "multiset (hs_of_list l) = mset l"
unfolding hs_of_list_def
using multiset_heapify_of_list_tree[of l]
by auto
qed

lemma removeLeaf_multiset:
assumes "(v', t') = removeLeaf t" "t ≠ E"
shows "{#v'#} + multiset t' = multiset t"
using assms
proof(induct t arbitrary: v' t' rule:removeLeaf.induct)
case 1
thus ?case
by auto
next
case (2 v v1 l1 r1)
have "t' = T v (snd (removeLeaf (T v1 l1 r1))) E"
using 2(3)
by auto
have "v' = fst (removeLeaf (T v1 l1 r1))"
using 2(3)
by auto
hence "{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) +
{#v#}"
using ‹t' = T v (snd (removeLeaf (T v1 l1 r1))) E›
have "{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) =
multiset (T v1 l1 r1)"
using 2(1)
by auto
hence "{#v'#} + multiset t' = multiset (T v1 l1 r1) + {#v#}"
using ‹{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) + {#v#}›
by auto
thus ?case
by auto
next
case (3 v v1 l1 r1)
have "t' = T v E (snd (removeLeaf (T v1 l1 r1)))"
using 3(3)
by auto
have "v' = fst (removeLeaf (T v1 l1 r1))"
using 3(3)
by auto
hence "{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) +
{#v#}"
using ‹t' = T v E (snd (removeLeaf (T v1 l1 r1)))›
have "{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) =
multiset (T v1 l1 r1)"
using 3(1)
by auto
hence "{#v'#} + multiset t' = multiset (T v1 l1 r1) + {#v#}"
using ‹{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) + {#v#}›
by auto
thus ?case
multiset.simps(1) multiset.simps(2) union_commute)
next
case ("4_1" v v1 l1 r1 v2 l2 r2)
have "t' = T v (snd (removeLeaf (T v1 l1 r1))) (T v2 l2 r2)"
using "4_1"(3)
by auto
have "v' = fst (removeLeaf (T v1 l1 r1))"
using "4_1"(3)
by auto
hence "{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) +
{#v#} + multiset (T v2 l2 r2)"
using ‹t' = T v (snd (removeLeaf (T v1 l1 r1))) (T v2 l2 r2)›
by (metis multiset.simps(2) union_assoc)
have "{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) =
multiset (T v1 l1 r1)"
using "4_1"(1)
by auto
hence "{#v'#} + multiset t' =
multiset (T v1 l1 r1) + {#v#} + multiset (T v2 l2 r2)"
using ‹{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) +
{#v#} + multiset (T v2 l2 r2)›
by auto
thus ?case
by auto
next
case ("4_2" v v1 l1 r1 v2 l2 r2)
have "t' = T v (snd (removeLeaf (T v1 l1 r1))) (T v2 l2 r2)"
using "4_2"(3)
by auto
have "v' = fst (removeLeaf (T v1 l1 r1))"
using "4_2"(3)
by auto
hence "{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) +
{#v#} + multiset (T v2 l2 r2)"
using ‹t' = T v (snd (removeLeaf (T v1 l1 r1))) (T v2 l2 r2)›
by (metis multiset.simps(2) union_assoc)
have "{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) =
multiset (T v1 l1 r1)"
using "4_2"(1)
by auto
hence "{#v'#} + multiset t' =
multiset (T v1 l1 r1) + {#v#} + multiset (T v2 l2 r2)"
using ‹{#v'#} + multiset t' =
{#fst (removeLeaf (T v1 l1 r1))#} +
multiset (snd (removeLeaf (T v1 l1 r1))) +
{#v#} + multiset (T v2 l2 r2)›
by auto
thus ?case
by auto
next
case 5
thus ?case
by auto
qed

lemma set_val_multiset:
assumes "t ≠ E"
shows "multiset (set_val t v') +  {#val t#} = {#v'#} + multiset t"
proof-
obtain v l r where "t = T v l r"
using assms
by (metis Tree.exhaust)
hence "multiset (set_val t v') + {#val t#} =
multiset l + {#v'#} + multiset r + {#v#}"
by auto
have "{#v'#} + multiset t =
{#v'#} + multiset l + {#v#} + multiset r"
using ‹t = T v l r›
by (metis multiset.simps(2) union_assoc)
have "{#v'#} + multiset l + {#v#} + multiset r =
multiset l + {#v'#} + multiset r + {#v#}"
by (metis union_commute union_lcomm)
thus ?thesis
using ‹multiset (set_val t v') + {#val t#} =
multiset l + {#v'#} + multiset r + {#v#}›
using ‹{#v'#} + multiset t =
{#v'#} + multiset l + {#v#} + multiset r›
by auto
qed

lemma hs_remove_max_multiset:
assumes "(m, t') = hs_remove_max t" "t ≠ E"
shows "{#m#} + multiset t' = multiset t"
proof-
let ?v1 = "fst (removeLeaf t)"
let ?t1 = "snd (removeLeaf t)"
show ?thesis
proof(cases "?t1 = E")
case True
hence "{#m#} + multiset t' = {#m#}"
using assms
unfolding hs_remove_max_def
by auto
have "?v1 = val t"
using True assms(2)
apply (induct t rule:removeLeaf.induct)
by auto
hence "?v1 = m"
using assms(1) True
unfolding hs_remove_max_def
by auto
hence "multiset t = {#m#}"
using removeLeaf_multiset[of ?v1 ?t1 t] True assms(2)
by (metis empty_neutral(2) multiset.simps(1) prod.collapse)
thus ?thesis
using ‹{#m#} + multiset t' = {#m#}›
by auto
next
case False
hence "t' = siftDown (set_val ?t1 ?v1)"
using assms(1)
by (auto simp add: hs_remove_max_def) (metis prod.inject)
hence "multiset t' + {#val ?t1#} = multiset t"
using siftDown_multiset[of "set_val ?t1 ?v1"]
using removeLeaf_multiset[of ?v1 ?t1 t] assms(2)
using set_val_multiset[of ?t1 ?v1] False
by auto
have "val ?t1 = val t"
using False assms(2)
apply (induct t rule:removeLeaf.induct)
by auto
have "val t = m"
using assms(1) False
using ‹t' = siftDown (set_val ?t1 ?v1)›
unfolding hs_remove_max_def
by (metis (full_types) fst_conv removeLeaf.simps(1))
hence "val ?t1 = m"
using ‹val ?t1 = val t›
by auto
hence "multiset t' + {#m#} = multiset t"
using ‹multiset t' + {#val ?t1#} = multiset t›
by metis
thus ?thesis
by (metis union_commute)
qed
qed

text‹Difined functions satisfy conditions of locale {\em Heap} and thus represent
interpretation of this locale.›

interpretation Heap "E" hs_is_empty hs_of_list multiset id hs_remove_max
proof
fix t
show "multiset t = multiset (id t)"
by auto
next
fix t
show " is_heap (id (hs_of_list t))"
unfolding hs_of_list_def
using heapify_heap_is_heap[of "of_list_tree t"]
by auto
next
fix t
show "(id t = E) = hs_is_empty t"
by auto
next
fix t m t'
assume "¬ hs_is_empty t" "(m, t') = hs_remove_max t"
thus "add_mset m (multiset t') = multiset t"
using hs_remove_max_multiset[of m t' t]
by auto
next
fix t v' t'
assume "¬ hs_is_empty t" "is_heap (id t)" "(v', t') = hs_remove_max t"
let ?v1 = "fst (removeLeaf t)"
let ?t1 = "snd (removeLeaf t)"
have "is_heap ?t1"
using ‹¬ hs_is_empty t› ‹is_heap (id t)›
using removeLeaf_heap_is_heap[of t]
by auto
show "is_heap (id t')"
proof(cases "?t1 = E")
case True
hence "t' = E"
using ‹(v', t') = hs_remove_max t›
unfolding hs_remove_max_def
by auto
thus ?thesis
by auto
next
case False
then obtain v_t1 l_t1 r_t1 where "?t1 = T v_t1 l_t1 r_t1"
by (metis Tree.exhaust)
hence "is_heap l_t1" "is_heap r_t1"
using ‹is_heap ?t1›
by (auto, metis (full_types) Tree.exhaust
is_heap.simps(1) is_heap.simps(4) is_heap.simps(5))
(metis (full_types) Tree.exhaust
is_heap.simps(1) is_heap.simps(3) is_heap.simps(5))
have "set_val ?t1 ?v1 = T ?v1 l_t1 r_t1"
using ‹?t1 = T v_t1 l_t1 r_t1›
by auto
hence "is_heap (siftDown (set_val ?t1 ?v1))"
using ‹is_heap l_t1› ‹is_heap r_t1›
using siftDown_heap_is_heap[of l_t1 r_t1 "set_val ?t1 ?v1" ?v1]
by auto
have "t' = siftDown (set_val ?t1 ?v1)"
using ‹(v', t') = hs_remove_max t› False
by (auto simp add: hs_remove_max_def) (metis prod.inject)
thus ?thesis
using ‹is_heap (siftDown (set_val ?t1 ?v1))›
by auto
qed
next
fix t m t'
let ?t1 = "snd (removeLeaf t)"
assume "¬ hs_is_empty t" "(m, t') = hs_remove_max t"
hence "m = val t"