Theory PrioByAnnotatedList

header {*\isaheader{Implementing Priority Queues by Annotated Lists}*}
theory PrioByAnnotatedList
imports 
  "../spec/AnnotatedListSpec"
  "../spec/PrioSpec"
begin

text {*
  In this theory, we implement priority queues by annotated lists.

  The implementation is realized as a generic adapter from the
  AnnotatedList to the priority queue interface.

  Priority queues are realized as a sequence of pairs of
  elements and associated priority. The monoids operation
  takes the element with minimum priority.

  The element with minimum priority is extracted from the
  sum over all elements.
  Deleting the element with minimum priority is done by
  splitting the sequence at the point where the minimum priority
  of the elements read so far becomes equal to the minimum priority of 
  all elements.
*}

subsection "Definitions"
subsubsection "Monoid"
datatype ('e, 'a) Prio = Infty | Prio 'e 'a

fun p_unwrap :: "('e,'a) Prio => ('e × 'a)" where
"p_unwrap (Prio e a) = (e , a)"

fun p_min :: "('e, 'a::linorder) Prio => ('e, 'a) Prio => ('e, 'a) Prio"  where
  "p_min Infty Infty = Infty"|
  "p_min Infty (Prio e a) = Prio e a"|
  "p_min (Prio e a) Infty = Prio e a"|
  "p_min (Prio e1 a) (Prio e2 b) = (if a ≤ b then Prio e1 a else Prio e2 b)"


lemma p_min_re_neut[simp]: "p_min a Infty = a" by (induct a) auto
lemma p_min_le_neut[simp]: "p_min Infty a = a" by (induct a) auto
lemma p_min_asso: "p_min (p_min a b) c = p_min a (p_min b c)"
  apply(induct a b  rule: p_min.induct )
  apply auto 
  apply (induct c)
  apply auto
  apply (induct c)
  apply auto
  done
lemma lp_mono: "class.monoid_add p_min Infty" 
  by unfold_locales (auto simp add: p_min_asso)

instantiation Prio :: (type,linorder) monoid_add
begin
definition zero_def: "0 == Infty" 
definition plus_def: "a+b == p_min a b"
  
instance by 
  intro_classes 
(auto simp add: p_min_asso zero_def plus_def)
end

fun p_less_eq :: "('e, 'a::linorder) Prio => ('e, 'a) Prio => bool" where
  "p_less_eq (Prio e a) (Prio f b) = (a ≤ b)"|
  "p_less_eq  _ Infty = True"|
  "p_less_eq Infty (Prio e a) = False"

fun p_less :: "('e, 'a::linorder) Prio => ('e, 'a) Prio => bool" where
  "p_less (Prio e a) (Prio f b) = (a < b)"|
  "p_less (Prio e a) Infty = True"|
  "p_less Infty _ = False"

lemma p_less_le_not_le : "p_less x y <-> p_less_eq x y ∧ ¬ (p_less_eq y x)"
  by (induct x y rule: p_less.induct) auto

lemma p_order_refl : "p_less_eq x x"
  by (induct x) auto

lemma p_le_inf : "p_less_eq Infty x ==> x = Infty"
  by (induct x) auto

lemma p_order_trans : "[|p_less_eq x y; p_less_eq y z|] ==> p_less_eq x z"
  apply (induct y z rule: p_less.induct)
  apply auto
  apply (induct x)
  apply auto
  apply (cases x)
  apply auto
  apply(induct x)
  apply (auto simp add: p_le_inf)
  apply (metis p_le_inf p_less_eq.simps(2))
  apply (metis p_le_inf p_less_eq.simps(2))
  done

lemma p_linear2 : "p_less_eq x y ∨ p_less_eq y x"
  apply (induct x y rule: p_less_eq.induct)
  apply auto
  done

instantiation Prio :: (type, linorder) preorder
begin
definition plesseq_def: "less_eq = p_less_eq"
definition pless_def: "less = p_less"

instance 
  apply (intro_classes)
  apply (simp only: p_less_le_not_le pless_def plesseq_def)
  apply (simp only: p_order_refl plesseq_def pless_def)
  apply (simp only: plesseq_def)
  apply (metis p_order_trans)
  done

end


subsubsection "Operations"
definition alprio_α :: "('s => (unit × ('e,'a::linorder) Prio) list) 
  => 's => ('e × 'a::linorder) multiset"
  where 
  "alprio_α α al == (multiset_of (map p_unwrap (map snd (α al))))"

definition alprio_invar :: "('s => (unit × ('c, 'd::linorder) Prio) list) 
  => ('s => bool) => 's => bool" 
  where
  "alprio_invar α invar al == invar al ∧ (∀ x∈set (α al). snd x≠Infty)"

definition alprio_empty  where 
  "alprio_empty empt = empt"

definition alprio_isEmpty  where 
  "alprio_isEmpty isEmpty = isEmpty"

definition alprio_insert :: "(unit => ('e,'a) Prio => 's => 's) 
  => 'e => 'a::linorder => 's  => 's"  
  where
  "alprio_insert consl e a s = consl () (Prio e a) s"

definition alprio_find :: "('s => ('e,'a::linorder) Prio) => 's => ('e × 'a)" 
where
"alprio_find annot s = p_unwrap (annot s)"

definition alprio_delete :: "((('e,'a::linorder) Prio => bool) 
  => ('e,'a) Prio => 's => ('s × (unit × ('e,'a) Prio) × 's)) 
                      => ('s => ('e,'a) Prio) => ('s => 's => 's) => 's => 's" 
  where
  "alprio_delete splits annot app s = (let (l, _ , r) 
    = splits (λ x. x≤(annot s)) Infty s in app l r) "

definition alprio_meld where
  "alprio_meld app = app"

lemmas alprio_defs =
  alprio_invar_def
  alprio_α_def
  alprio_empty_def
  alprio_isEmpty_def
  alprio_insert_def
  alprio_find_def
  alprio_delete_def
  alprio_meld_def

subsection "Correctness"

subsubsection "Auxiliary Lemmas"
lemma listsum_split: "listsum (l @ (a::'a::monoid_add) # r) = (listsum l) + a + (listsum r)"
  by (induct l) (auto simp add: add_assoc)


lemma p_linear: "(x::('e, 'a::linorder) Prio) ≤ y ∨ y ≤ x"
  by (unfold plesseq_def) (simp only: p_linear2)


lemma p_min_mon: "(x::(('e,'a::linorder) Prio)) ≤ y ==> (z + x) ≤ y"
apply (unfold plus_def plesseq_def)
apply (induct x y rule: p_less_eq.induct)
apply (auto)
apply (induct z)
apply (auto)
done

lemma p_min_mon2: "p_less_eq x y ==> p_less_eq (p_min z x) y"
apply (induct x y rule: p_less_eq.induct)
apply (auto)
apply (induct z)
apply (auto)
done

lemma ls_min: " ∀x ∈ set (xs:: ('e,'a::linorder) Prio list) . listsum xs ≤ x"
proof (induct xs)
case Nil thus ?case by auto
next
case (Cons a ins) thus ?case
  apply (auto simp add: plus_def plesseq_def)
  apply (cases a)
  apply auto
  apply (cases "listsum ins")
  apply auto
  apply (case_tac x)
  apply auto
  apply (cases a)
  apply auto
  apply (cases "listsum ins")
  apply auto
  done
qed    

lemma infadd: "x ≠ Infty ==>x + y ≠ Infty"
apply (unfold plus_def)
apply (induct x y rule: p_min.induct)
apply auto
done


lemma prio_selects_one: "a+b = a ∨ a+b=(b::('e,'a::linorder) Prio)"
  apply (simp add: plus_def)
  apply (cases "(a,b)" rule: p_min.cases)
  apply simp_all
  done


lemma listsum_in_set: "(l::('x × ('e,'a::linorder) Prio) list)≠[] ==> 
  listsum (map snd l) ∈ set (map snd l)"
  apply (induct l)
  apply simp
  apply (case_tac l)
  apply simp
  using prio_selects_one
  apply auto
  apply force
  apply force
  done

lemma p_unwrap_less_sum: "snd (p_unwrap ((Prio e aa) + b)) ≤ aa"
  apply (cases b)
  apply (auto simp add: plus_def)
done

lemma prio_add_alb: "¬ b ≤ (a::('e,'a::linorder)Prio)  ==> b + a = a"
  by (auto simp add: plus_def, cases "(a,b)" rule: p_min.cases) (auto simp add: plesseq_def)

lemma prio_add_alb2: " (a::('e,'a::linorder)Prio)  ≤ a + b ==>  a + b = a"
  by (auto simp add: plus_def, cases "(a,b)" rule: p_min.cases) (auto simp add: plesseq_def)

lemma prio_add_abc:
  assumes "(l::('e,'a::linorder)Prio) + a ≤ c" 
  and "¬ l ≤ c"
  shows  "¬ l ≤ a"
proof (rule ccontr)
  assume "¬ ¬ l ≤ a"
  with assms have "l + a = l"
    apply (auto simp add: plus_def plesseq_def)
    apply (cases "(l,a)" rule: p_less_eq.cases)
    apply auto
    done
  with assms show False by simp
qed

lemma prio_add_abc2:
  assumes "(a::('e,'a::linorder)Prio) ≤ a + b" 
  shows "a ≤ b"
proof (rule ccontr)
  assume ann: "¬ a ≤ b"
  hence "a + b = b" 
    apply (auto simp add: plus_def plesseq_def)
    apply (cases "(a,b)" rule: p_min.cases)
    apply auto
    done
  thus False using assms ann by simp
qed


subsubsection "Empty"
lemma alprio_empty_correct: 
  assumes "al_empty α invar empt"
  shows "prio_empty (alprio_α α) (alprio_invar α invar) (alprio_empty empt)"
proof -
  interpret al_empty α invar empt by fact
  show ?thesis
    apply (unfold_locales)
    apply (unfold alprio_invar_def)
    apply auto
    apply (unfold alprio_empty_def)
    apply (auto simp add: empty_correct)
    apply (unfold alprio_α_def)
    apply auto
    apply (simp only: empty_correct)
    done
qed


subsubsection "Is Empty"

lemma alprio_isEmpty_correct: 
  assumes "al_isEmpty α invar isEmpty"
  shows "prio_isEmpty (alprio_α α) (alprio_invar α invar) (alprio_isEmpty isEmpty)"
proof -
  interpret al_isEmpty α invar isEmpty by fact
  show ?thesis by (unfold_locales) (auto simp add: alprio_defs isEmpty_correct)
qed


subsubsection "Insert"
lemma alprio_insert_correct: 
  assumes "al_consl α invar consl"
  shows "prio_insert (alprio_α α) (alprio_invar α invar) (alprio_insert consl)"
proof -
  interpret al_consl α invar consl by fact
  show ?thesis by unfold_locales (auto simp add: alprio_defs consl_correct)
qed


subsubsection "Meld"

lemma alprio_meld_correct: 
  assumes "al_app α invar app"
  shows "prio_meld (alprio_α α) (alprio_invar α invar) (alprio_meld app)"
proof -
  interpret al_app α invar app by fact
  show ?thesis by unfold_locales (auto simp add: alprio_defs app_correct)
qed

subsubsection "Find"

lemma annot_not_inf :
  assumes "(alprio_invar α invar) s" 
  and "(alprio_α α) s ≠ {#}"
  and "al_annot α invar annot"
  shows "annot s ≠ Infty"
proof -
  interpret al_annot α invar annot by fact
  show ?thesis
  proof -
    from assms(1) have invs: "invar s" by (simp add: alprio_defs)
    from assms(2) have sne: "set (α s) ≠ {}"
    proof (cases "set (α s) = {}")
      case True 
      hence "α s = []" by simp
      hence "(alprio_α α) s = {#}" by (simp add: alprio_defs)
      from this assms(2) show ?thesis by simp
    next
      case False thus ?thesis by simp
    qed
    hence "(α s) ≠ []" by simp
    hence " ∃x xs. (α s) = x # xs" by (cases "α s") auto
    from this obtain x xs where [simp]: "(α s) = x # xs" by blast
    from this assms(1) have "snd x ≠ Infty" by (auto simp add: alprio_defs)
    hence "listsum (map snd (α s)) ≠ Infty" by (auto simp add: infadd)
    thus "annot s ≠ Infty" using annot_correct invs by simp
  qed
qed

lemma annot_in_set: 
  assumes "(alprio_invar α invar) s" 
  and "(alprio_α α) s ≠ {#}"
  and "al_annot α invar annot"
  shows "p_unwrap (annot s) ∈# ((alprio_α α) s)"         
proof - 
  interpret al_annot α invar annot by fact
  from assms(2) have snn: "α s ≠ []" by (auto simp add: alprio_defs)
  from assms(1) have invs: "invar s" by (simp add: alprio_defs)
  hence ans: "annot s = listsum (map snd (α s))" by (simp add: annot_correct)
  let ?P = "map snd (α s)"
  have "annot s ∈ set ?P"
    by (unfold ans) (rule listsum_in_set[OF snn])
  hence "p_unwrap (annot s) ∈ set (map p_unwrap ?P)"
    by (metis image_iff in_set_conv_decomp set_map split_list_last)
  thus ?thesis
    by (metis mem_set_multiset_eq alprio_α_def)
qed

lemma  listsum_less_elems: "∀x∈set xs. snd x ≠ Infty ==>
   ∀y∈set_of (multiset_of (map p_unwrap (map snd xs))).
              snd (p_unwrap (listsum (map snd xs))) ≤ snd y"          
    proof (induct xs)
    case Nil thus ?case by simp
    next
    case (Cons a as) thus ?case
      apply auto
      apply (cases "(snd a)" rule: p_unwrap.cases)
      apply auto
      apply (cases "listsum (map snd as)")
      apply auto
      apply (metis linorder_linear p_min_re_neut 
        p_unwrap.simps plus_def [abs_def] snd_eqD)
      apply (auto simp add: p_unwrap_less_sum)
      apply (unfold plus_def)
      apply (cases "(snd a, listsum (map snd as))" rule: p_min.cases)
      apply auto
      apply (cases "map snd as")
      apply (auto simp add: infadd)
      done
qed  
  
lemma alprio_find_correct: 
  assumes  "al_annot α invar annot"
  shows "prio_find (alprio_α α) (alprio_invar α invar) (alprio_find annot)"
proof -
  interpret al_annot α invar annot by fact
  show ?thesis
    apply unfold_locales
    apply (rule conjI)
    apply (insert assms)
    apply (unfold alprio_find_def)
    apply (simp add:annot_in_set)
    apply (unfold alprio_defs)
    apply (simp add: annot_correct)
    apply (auto simp add: listsum_less_elems)
    done
qed


subsubsection "Delete"

lemma delpred_mon: 
  "∀(a:: ('e, 'a::linorder) Prio) b. ((λ x. x ≤ y) a 
    --> (λ x. x ≤ y) (a + b)) "
proof (intro impI allI) 
  fix a b 
  show "a ≤ y ==> a + b ≤ y"
    apply (induct a b rule: p_less.induct)
    apply (auto simp add: p_less_eq_def plus_def)
    apply (metis linorder_linear order_trans 
      p_linear p_min.simps(4) p_min_mon plus_def prio_selects_one)
    apply (metis order_trans p_linear p_min_mon p_min_re_neut plus_def)
    done 
qed

(* alprio_delete erhält die Invariante *)
lemma alpriodel_invar: 
  assumes "alprio_invar α invar s"
  and "al_annot α invar annot"
  and "alprio_α α s ≠ {#}"
  and "al_splits α invar splits"
  and "al_app α invar app"
  shows "alprio_invar α invar (alprio_delete splits annot app s)"
proof -
  interpret al_splits α invar splits by fact
  let ?P = "λx. x ≤ annot s"
  obtain l p r where 
    [simp]:"splits ?P Infty s = (l, p, r)" 
    by (cases "splits ?P Infty s")  auto
  obtain e a where 
    "p = (e, a)" 
    by (cases p, blast)
  hence 
    lear:"splits ?P Infty s = (l, (e,a), r)" 
    by simp
  from annot_not_inf[OF assms(1) assms(3) assms(2)] have 
    "annot s ≠ Infty" .
  hence 
    sv1: "¬ Infty ≤ annot s" 
    by (simp add: plesseq_def, cases "annot s", auto)
  from assms(1) have 
    invs: "invar s" 
    unfolding alprio_invar_def by simp
  interpret al_annot α invar annot by fact
  from invs have 
    sv2: "Infty + listsum (map snd (α s)) ≤ annot s" 
    by (auto simp add: annot_correct plus_def 
      plesseq_def p_min_le_neut p_order_refl)
  note sp = splits_correct[of s "?P" Infty l e a r]
  note dp = delpred_mon[of "annot s"]
  from sp[OF invs dp sv1 sv2 lear] have 
    invlr: "invar l ∧ invar r" and 
    alr: "α s = α l @ (e, a) # α r" 
    by auto
  interpret al_app α invar app by fact
  from invlr app_correct have 
    invapplr: "invar (app l r)" 
    by simp
  from invlr app_correct have 
    sr: "α (app l r) = (α l) @ (α r)" 
    by simp
  from alr have  
    "set (α s) ⊇ (set (α l) Un set (α r))" 
    by auto
  with app_correct[of l r] invlr have 
    "set (α s) ⊇ set (α (app l r))" by auto
  with invapplr assms(1) 
  show ?thesis 
    unfolding alprio_defs by auto
qed


lemma listsum_elem:
  assumes " ins = l @ (a::('e,'a::linorder)Prio) # r"  
  and "¬ listsum l ≤ listsum ins"  
  and "listsum l + a ≤ listsum ins "
  shows " a = listsum ins"
proof -
  have "¬ listsum l ≤ a" using assms prio_add_abc by simp
  hence lpa: "listsum l + a = a" using prio_add_alb by auto
  hence als: "a ≤ listsum ins" using assms(3) by simp
  have "listsum ins = a + listsum r" 
    using lpa listsum_split[of l a r] assms(1) by auto
  thus ?thesis using prio_add_alb2[of a "listsum r"] prio_add_abc2 als  
    by auto
qed

lemma alpriodel_right:
  assumes "alprio_invar α invar s"
  and "al_annot α invar annot"
  and "alprio_α α s ≠ {#}"
  and "al_splits α invar splits"
  and "al_app α invar app"
  shows "alprio_α α (alprio_delete splits annot app s) = 
          alprio_α α s - {#p_unwrap (annot s)#}"
proof -
  interpret al_splits α invar splits by fact
  let ?P = "λx. x ≤ annot s"
  obtain l p r where 
    [simp]:"splits ?P Infty s = (l, p, r)" 
    by (cases "splits ?P Infty s")  auto
  obtain e a where 
    "p = (e, a)" 
    by (cases p, blast)
  hence 
    lear:"splits ?P Infty s = (l, (e,a), r)" 
    by simp
  from annot_not_inf[OF assms(1) assms(3) assms(2)] have 
    "annot s ≠ Infty" .
  hence 
    sv1: "¬ Infty ≤ annot s" 
    by (simp add: plesseq_def, cases "annot s", auto)
  from assms(1) have 
    invs: "invar s" 
    unfolding alprio_invar_def by simp
  interpret al_annot α invar annot by fact
  from invs have 
    sv2: "Infty + listsum (map snd (α s)) ≤ annot s" 
    by (auto simp add: annot_correct plus_def 
      plesseq_def p_min_le_neut p_order_refl)
  note sp = splits_correct[of s "?P" Infty l e a r]
  note dp = delpred_mon[of "annot s"]
  
  from sp[OF invs dp sv1 sv2 lear] have 
    invlr: "invar l ∧ invar r" and 
    alr: "α s = α l @ (e, a) # α r" and
    anlel: "¬ listsum (map snd (α l)) ≤ annot s" and 
    aneqa: "(listsum (map snd (α l)) + a) ≤ annot s"
    by (auto simp add: plus_def zero_def)
  have mapalr: "map snd (α s) = (map snd (α l)) @ a # (map snd (α r))" 
    using alr by simp
  note lsa = listsum_elem[of "map snd (α s)" "map snd (α l)" a "map snd (α r)"]
  note lsa2 = lsa[OF mapalr]
  hence a_is_annot: "a = annot s" 
    using annot_correct[OF invs] anlel aneqa by auto
  have "map p_unwrap (map snd (α s)) = 
    (map p_unwrap (map snd (α l))) @ (p_unwrap a) 
      # (map p_unwrap (map snd (α r)))" 
    using alr by simp
  hence alpriolst: "(alprio_α α s) = (alprio_α α l) +{# p_unwrap a #}+ (alprio_α α r)" 
    unfolding alprio_defs
    by (simp add: algebra_simps)
  interpret al_app α invar app by fact
  from alpriolst show ?thesis using app_correct[of l r] invlr a_is_annot 
    by (auto simp add: alprio_defs algebra_simps)
qed  

lemma alprio_delete_correct: 
  assumes "al_annot α invar annot"
  and "al_splits α invar splits"
  and "al_app α invar app"
  shows "prio_delete (alprio_α α) (alprio_invar α invar) 
           (alprio_find annot) (alprio_delete splits annot app)"
proof-
  interpret al_annot α invar annot by fact
  interpret al_splits α invar splits by fact
  interpret al_app α invar app by fact
  show ?thesis
    apply intro_locales
    apply (rule alprio_find_correct,simp add: assms) 
    apply unfold_locales
    apply (insert assms)
    apply (simp add: alpriodel_invar)
    apply (simp add: alpriodel_right alprio_find_def)   
    done
qed  

lemmas alprio_correct =
  alprio_empty_correct
  alprio_isEmpty_correct
  alprio_insert_correct
  alprio_delete_correct
  alprio_find_correct
  alprio_meld_correct
    
end