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