Theory Heap

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

section ‹Verification of Heap Sort›

theory Heap
imports RemoveMax

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
  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)"
  fix x
  show "is_heap (as_tree (of_list x))"
    by (rule is_heap_of_list)
  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')
  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)
  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

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