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