(*  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

(*  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']
by (metis mset_subset_size multi_psub_of_add_self)

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']
        by (metis union_mset_add_mset_left union_mset_add_mset_right mset.simps(2))
    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

(*  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
    by (simp add: max_Max_commute)
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

(*  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

(*  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

(*  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"
      by (metis calculation monoid_add_class.add.left_neutral 
          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)
        by (simp add: ac_simps)
      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)
        by (simp add: ac_simps)
      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)
    by (simp add:is_heap.simps(5))+
  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›
      by (simp add: is_heap.simps(5))
    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)
    by (simp add:is_heap.simps(5))+
  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›
      by (simp add: is_heap.simps(5))
    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›
    by (simp add: ac_simps)
  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)))›
    by (simp add: ac_simps)
  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
    by (metis monoid_add_class.add.right_neutral 
        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"
    apply (simp add: hs_remove_max_def)
    apply (cases "?t1 = E")
    by (auto, metis prod.inject)    
  thus "m = val (id t)"
    by auto
qed




end