src/HOL/Data_Structures/Binomial_Heap.thy

reorg

(* Author: Peter Lammich *)

section \<open>Binomial Heap\<close>

theory Binomial_Heap
imports
  Base_FDS
  Complex_Main
  Priority_Queue
begin

text \<open>
  We formalize the binomial heap presentation from Okasaki's book.
  We show the functional correctness and complexity of all operations.

  The presentation is engineered for simplicity, and most 
  proofs are straightforward and automatic.
\<close>

subsection \<open>Binomial Tree and Heap Datatype\<close>

datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")

type_synonym 'a heap = "'a tree list"

subsubsection \<open>Multiset of elements\<close>

fun mset_tree :: "'a::linorder tree \<Rightarrow> 'a multiset" where
  "mset_tree (Node _ a c) = {#a#} + (\<Sum>t\<in>#mset c. mset_tree t)"
  
definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where  
  "mset_heap c = (\<Sum>t\<in>#mset c. mset_tree t)"
  
lemma mset_tree_simp_alt[simp]: 
  "mset_tree (Node r a c) = {#a#} + mset_heap c"
  unfolding mset_heap_def by auto
declare mset_tree.simps[simp del]    
  
lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}"  
  by (cases t) auto
  
lemma mset_heap_Nil[simp]: 
  "mset_heap [] = {#}"
  unfolding mset_heap_def 
  by auto 
  
lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts"
  unfolding mset_heap_def by auto 
  
lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]"
  unfolding mset_heap_def by auto 
    
lemma root_in_mset[simp]: "root t \<in># mset_tree t" by (cases t) auto    
    
lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts"    
  unfolding mset_heap_def by auto
    
subsubsection \<open>Invariants\<close>  
  
text \<open>Binomial invariant\<close>  
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" 
  where
    "invar_btree (Node r x ts) \<longleftrightarrow> 
      (\<forall>t\<in>set ts. invar_btree t) 
    \<and> (map rank ts = rev [0..<r])"

definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
  "invar_bheap ts
  \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (op <) (map rank ts))"

text \<open>Ordering (heap) invariant\<close>
fun otree_invar :: "'a::linorder tree \<Rightarrow> bool"
  where
    "otree_invar (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t \<and> x \<le> root t)"

definition oheap_invar :: "'a::linorder heap \<Rightarrow> bool" where
  "oheap_invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t)"
  
definition invar :: "'a::linorder heap \<Rightarrow> bool" where
  "invar ts \<longleftrightarrow> invar_bheap ts \<and> oheap_invar ts"
  
text \<open>The children of a node are a valid heap\<close>
lemma children_oheap_invar: 
  "otree_invar (Node r v ts) \<Longrightarrow> oheap_invar (rev ts)"  
  by (auto simp: oheap_invar_def)

lemma children_invar_bheap: 
  "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"  
  by (auto simp: invar_bheap_def rev_map[symmetric])
      
subsection \<open>Operations\<close>  
    
definition link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
  "link t\<^sub>1 t\<^sub>2 = (case (t\<^sub>1,t\<^sub>2) of (Node r x\<^sub>1 c\<^sub>1, Node _ x\<^sub>2 c\<^sub>2) \<Rightarrow>
    if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#c\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#c\<^sub>2)
  )"

lemma link_invar_btree:
  assumes "invar_btree t\<^sub>1"
  assumes "invar_btree t\<^sub>2"
  assumes "rank t\<^sub>1 = rank t\<^sub>2"  
  shows "invar_btree (link t\<^sub>1 t\<^sub>2)"  
  using assms  
  unfolding link_def
  by (force split: tree.split)
    
lemma link_otree_invar:      
  assumes "otree_invar t\<^sub>1"
  assumes "otree_invar t\<^sub>2"
  shows "otree_invar (link t\<^sub>1 t\<^sub>2)"  
  using assms  
  unfolding link_def
  by (auto split: tree.split)
    
lemma link_rank[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
  unfolding link_def
  by (auto split: tree.split)
    
lemma link_mset[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
  unfolding link_def
  by (auto split: tree.split)
    
fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
  "ins_tree t [] = [t]"
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) = (
    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts
  )"  
    
lemma invar_bheap_Cons[simp]: 
  "invar_bheap (t#ts) 
  \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
  unfolding invar_bheap_def
  by (auto simp: sorted_wrt_Cons)
  
lemma ins_tree_invar_btree:
  assumes "invar_btree t" 
  assumes "invar_bheap ts"
  assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"  
  shows "invar_bheap (ins_tree t ts)"  
  using assms
  apply (induction t ts rule: ins_tree.induct)  
  apply (auto simp: link_invar_btree less_eq_Suc_le[symmetric])
  done  
    
lemma oheap_invar_Cons[simp]: 
  "oheap_invar (t#ts) \<longleftrightarrow> otree_invar t \<and> oheap_invar ts"    
  unfolding oheap_invar_def by auto
    
lemma ins_tree_otree_invar:
  assumes "otree_invar t" 
  assumes "oheap_invar ts"
  shows "oheap_invar (ins_tree t ts)"  
  using assms  
  apply (induction t ts rule: ins_tree.induct)  
  apply (auto simp: link_otree_invar)
  done  
    
lemma ins_tree_mset[simp]: 
  "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"    
  by (induction t ts rule: ins_tree.induct) auto  

lemma ins_tree_rank_bound:
  assumes "t' \<in> set (ins_tree t ts)"  
  assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'"
  assumes "rank t\<^sub>0 < rank t"  
  shows "rank t\<^sub>0 < rank t'"
  using assms  
  by (induction t ts rule: ins_tree.induct) (auto split: if_splits)
  
    
definition ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
  "ins x ts = ins_tree (Node 0 x []) ts"
  
lemma ins_invar[simp]: "invar t \<Longrightarrow> invar (ins x t)"
  unfolding ins_def invar_def
  by (auto intro!: ins_tree_invar_btree simp: ins_tree_otree_invar)  
    
lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t"
  unfolding ins_def
  by auto

fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
  "merge ts\<^sub>1 [] = ts\<^sub>1"
| "merge [] ts\<^sub>2 = ts\<^sub>2"  
| "merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = (
    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2) else
    if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
    else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
  )"

lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" by (cases ts\<^sub>2) auto
  
lemma merge_rank_bound:
  assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)"
  assumes "\<forall>t'\<in>set ts\<^sub>1. rank t < rank t'"
  assumes "\<forall>t'\<in>set ts\<^sub>2. rank t < rank t'"
  shows "rank t < rank t'"
  using assms
  apply (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
  apply (auto split: if_splits simp: ins_tree_rank_bound)
  done
    
lemma merge_invar_bheap:
  assumes "invar_bheap ts\<^sub>1"
  assumes "invar_bheap ts\<^sub>2"
  shows "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"  
  using assms
proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
  case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
    
  from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2"  
    by auto
    
  consider (LT) "rank t\<^sub>1 < rank t\<^sub>2" 
         | (GT) "rank t\<^sub>1 > rank t\<^sub>2" 
         | (EQ) "rank t\<^sub>1 = rank t\<^sub>2"
    using antisym_conv3 by blast
  then show ?case proof cases
    case LT
    then show ?thesis using 3
      by (force elim!: merge_rank_bound)
  next
    case GT
    then show ?thesis using 3
      by (force elim!: merge_rank_bound)
  next
    case [simp]: EQ

    from "3.IH"(3) "3.prems" have [simp]: "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
      by auto
      
    have "rank t\<^sub>2 < rank t'" if "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" for t'
      using that
      apply (rule merge_rank_bound)
      using "3.prems" by auto
    with EQ show ?thesis
      by (auto simp: Suc_le_eq ins_tree_invar_btree link_invar_btree)
  qed
qed simp_all
  
lemma merge_oheap_invar:
  assumes "oheap_invar ts\<^sub>1"
  assumes "oheap_invar ts\<^sub>2"
  shows "oheap_invar (merge ts\<^sub>1 ts\<^sub>2)"  
  using assms
  apply (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
  apply (auto simp: ins_tree_otree_invar link_otree_invar)  
  done
    
lemma merge_invar[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
  unfolding invar_def by (auto simp: merge_invar_bheap merge_oheap_invar)
    
lemma merge_mset[simp]: 
  "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
  by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto  
    

fun find_min :: "'a::linorder heap \<Rightarrow> 'a" where
  "find_min [t] = root t"
| "find_min (t#ts) = (let x=root t; 
                          y=find_min ts
                      in if x\<le>y then x else y)"
  
lemma otree_invar_root_min:
  assumes "otree_invar t"
  assumes "x \<in># mset_tree t" 
  shows "root t \<le> x"  
  using assms
  apply (induction t arbitrary: x rule: mset_tree.induct)  
  apply (force simp: mset_heap_def)
  done  
    
  
lemma find_min_mset_aux: 
  assumes "ts\<noteq>[]"    
  assumes "oheap_invar ts"
  assumes "x \<in># mset_heap ts"  
  shows "find_min ts \<le> x"
  using assms  
  apply (induction ts arbitrary: x rule: find_min.induct)  
  apply (auto 
      simp: otree_invar_root_min intro: order_trans;
      meson linear order_trans otree_invar_root_min
      )+
  done  

lemma find_min_mset: 
  assumes "ts\<noteq>[]"    
  assumes "invar ts"
  assumes "x \<in># mset_heap ts"  
  shows "find_min ts \<le> x"
  using assms unfolding invar_def 
  by (auto simp: find_min_mset_aux)
    
    
lemma find_min_member:    
  assumes "ts\<noteq>[]"    
  shows "find_min ts \<in># mset_heap ts"  
  using assms  
  apply (induction ts rule: find_min.induct)  
  apply (auto)
  done  

lemma find_min:    
  assumes "mset_heap ts \<noteq> {#}"
  assumes "invar ts"
  shows "find_min ts = Min_mset (mset_heap ts)"
  using assms find_min_member find_min_mset  
  by (auto simp: eq_Min_iff)
    

fun get_min :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
  "get_min [t] = (t,[])"
| "get_min (t#ts) = (let (t',ts') = get_min ts
                     in if root t \<le> root t' then (t,ts) else (t',t#ts'))"

  
lemma get_min_find_min_same_root: 
  assumes "ts\<noteq>[]"
  assumes "get_min ts = (t',ts')"  
  shows "root t' = find_min ts"  
  using assms  
  apply (induction ts arbitrary: t' ts' rule: find_min.induct)
  apply (auto split: prod.splits)
  done
  
lemma get_min_mset:    
  assumes "get_min ts = (t',ts')"  
  assumes "ts\<noteq>[]"
  shows "mset ts = {#t'#} + mset ts'"  
  using assms  
  apply (induction ts arbitrary: t' ts' rule: find_min.induct)
  apply (auto split: prod.splits if_splits)
  done  
    
lemma get_min_set:
  assumes "get_min ts = (t', ts')" 
  assumes "ts\<noteq>[]"
  shows "set ts = insert t' (set ts')" 
  using get_min_mset[OF assms, THEN arg_cong[where f=set_mset]]
  by auto  

    
lemma get_min_invar_bheap:    
  assumes "get_min ts = (t',ts')"  
  assumes "ts\<noteq>[]"
  assumes "invar_bheap ts"  
  shows "invar_btree t'" and "invar_bheap ts'"
proof -
  have "invar_btree t' \<and> invar_bheap ts'"
    using assms  
    proof (induction ts arbitrary: t' ts' rule: find_min.induct)
      case (2 t v va)
      then show ?case
        apply (clarsimp split: prod.splits if_splits)
        apply (drule get_min_set; fastforce)
        done  
    qed auto
  thus "invar_btree t'" and "invar_bheap ts'" by auto
qed
  
lemma get_min_oheap_invar:    
  assumes "get_min ts = (t',ts')"  
  assumes "ts\<noteq>[]"
  assumes "oheap_invar ts"  
  shows "otree_invar t'" and "oheap_invar ts'"
  using assms  
  apply (induction ts arbitrary: t' ts' rule: find_min.induct)
  apply (auto split: prod.splits if_splits)
  done  
    
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
"del_min ts = (case get_min ts of
   (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
  
lemma del_min_invar[simp]:
  assumes "ts \<noteq> []"
  assumes "invar ts"
  shows "invar (del_min ts)"
  using assms  
  unfolding invar_def del_min_def  
  by (auto 
      split: prod.split tree.split 
      intro!: merge_invar_bheap merge_oheap_invar
      dest: get_min_invar_bheap get_min_oheap_invar
      intro!: children_oheap_invar children_invar_bheap
      )
    
lemma del_min_mset: 
  assumes "ts \<noteq> []"
  shows "mset_heap ts = mset_heap (del_min ts) + {# find_min ts #}"
  using assms
  unfolding del_min_def
  apply (clarsimp split: tree.split prod.split)
  apply (frule (1) get_min_find_min_same_root)  
  apply (frule (1) get_min_mset)  
  apply (auto simp: mset_heap_def)
  done  

subsection \<open>Complexity\<close>
  
text \<open>The size of a binomial tree is determined by its rank\<close>  
lemma size_btree:
  assumes "invar_btree t"
  shows "size (mset_tree t) = 2^rank t"  
  using assms
proof (induction t)
  case (Node r v ts)
  hence IH: "size (mset_tree t) = 2^rank t" if "t \<in> set ts" for t
    using that by auto
    
  from Node have COMPL: "map rank ts = rev [0..<r]" by auto
      
  have "size (mset_heap ts) = (\<Sum>t\<leftarrow>ts. size (mset_tree t))"
    by (induction ts) auto
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH
    by (auto cong: sum_list_cong)
  also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)" 
    by (induction ts) auto
  also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)" 
    unfolding COMPL 
    by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat)
  also have "\<dots> = 2^r - 1" 
    by (induction r) auto
  finally show ?case 
    by (simp)
qed
   
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>  
lemma size_bheap:      
  assumes "invar_bheap ts"
  shows "2^length ts \<le> size (mset_heap ts) + 1"
proof -
  from \<open>invar_bheap ts\<close> have 
    ASC: "sorted_wrt (op <) (map rank ts)" and
    TINV: "\<forall>t\<in>set ts. invar_btree t"
    unfolding invar_bheap_def by auto
      
  have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1" 
    by (simp add: sum_power2)
  also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
    using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "op ^ (2::nat)"]
    using power_increasing[where a="2::nat"]  
    by (auto simp: o_def)
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV   
    by (auto cong: sum_list_cong simp: size_btree)
  also have "\<dots> = size (mset_heap ts) + 1"
    unfolding mset_heap_def by (induction ts) auto
  finally show ?thesis .
qed      
  
subsubsection \<open>Timing Functions\<close>  
text \<open>
  We define timing functions for each operation, and provide
  estimations of their complexity.
\<close>
definition t_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
[simp]: "t_link _ _ = 1"  

fun t_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
  "t_ins_tree t [] = 1"
| "t_ins_tree t\<^sub>1 (t\<^sub>2#rest) = (
    (if rank t\<^sub>1 < rank t\<^sub>2 then 1 
     else t_link t\<^sub>1 t\<^sub>2 + t_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
  )"  
    
  
definition t_ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
  "t_ins x ts = t_ins_tree (Node 0 x []) ts"

lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1" for t 
  by (induction t ts rule: t_ins_tree.induct) auto
  
lemma t_ins_bound: 
  assumes "invar ts"
  shows "t_ins x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
proof -

  have 1: "t_ins x ts \<le> length ts + 1" 
    unfolding t_ins_def by (rule t_ins_tree_simple_bound)
  also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))" 
  proof -
    from size_bheap[of ts] assms 
    have "2 ^ length ts \<le> size (mset_heap ts) + 1"
      unfolding invar_def by auto
    hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto
    thus ?thesis using le_log2_of_power by blast
  qed
  finally show ?thesis 
    by (simp only: log_mult of_nat_mult) auto
qed      
  
fun t_merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> nat" where
  "t_merge ts\<^sub>1 [] = 1"
| "t_merge [] ts\<^sub>2 = 1"  
| "t_merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = 1 + (
    if rank t\<^sub>1 < rank t\<^sub>2 then t_merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2)
    else if rank t\<^sub>2 < rank t\<^sub>1 then t_merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
    else t_ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) + t_merge ts\<^sub>1 ts\<^sub>2
  )"  
  
text \<open>A crucial idea is to estimate the time in correlation with the 
  result length, as each carry reduces the length of the result.\<close>  
lemma l_ins_tree_estimate: 
  "t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
by (induction t ts rule: ins_tree.induct) auto

lemma l_merge_estimate: 
  "length (merge ts\<^sub>1 ts\<^sub>2) + t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1"
  apply (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct)  
  apply (auto simp: l_ins_tree_estimate algebra_simps)
  done
    
text \<open>Finally, we get the desired logarithmic bound\<close>
lemma t_merge_bound_aux:
  fixes ts\<^sub>1 ts\<^sub>2
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"    
  defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
  assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2"
  shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
proof -
  define n where "n = n\<^sub>1 + n\<^sub>2"  
      
  from l_merge_estimate[of ts\<^sub>1 ts\<^sub>2] 
  have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto
  hence "(2::nat)^t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)" 
    by (rule power_increasing) auto
  also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"    
    by (auto simp: algebra_simps power_add power_mult)
  also note BINVARS(1)[THEN size_bheap]
  also note BINVARS(2)[THEN size_bheap]
  finally have "2 ^ t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2" 
    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
  from le_log2_of_power[OF this] have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"    
    by simp
  also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
    by (simp add: log_mult log_nat_power)
  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
  finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)"    
    by auto
  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
  finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
    by auto
  also have "log 2 2 \<le> 2" by auto
  finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
qed      
    
lemma t_merge_bound:
  fixes ts\<^sub>1 ts\<^sub>2
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"    
  defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
  assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
  shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
using assms t_merge_bound_aux unfolding invar_def by blast  
  
  
fun t_find_min :: "'a::linorder heap \<Rightarrow> nat" where
  "t_find_min [t] = 1"
| "t_find_min (t#ts) = 1 + t_find_min ts"

lemma t_find_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_find_min ts = length ts"  
by (induction ts rule: t_find_min.induct) auto
  
lemma t_find_min_bound: 
  assumes "invar ts"
  assumes "ts\<noteq>[]"
  shows "t_find_min ts \<le> log 2 (size (mset_heap ts) + 1)"
proof -
  have 1: "t_find_min ts = length ts" using assms t_find_min_estimate by auto
  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
  proof -
    from size_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
      unfolding invar_def by auto
    thus ?thesis using le_log2_of_power by blast
  qed
  finally show ?thesis by auto 
qed  
    
fun t_get_min :: "'a::linorder heap \<Rightarrow> nat" where
  "t_get_min [t] = 1"
| "t_get_min (t#ts) = 1 + t_get_min ts"

lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts"  
  by (induction ts rule: t_get_min.induct) auto
  
lemma t_get_min_bound_aux: 
  assumes "invar_bheap ts"
  assumes "ts\<noteq>[]"
  shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
proof -
  have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto
  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
  proof -
    from size_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
      by auto
    thus ?thesis using le_log2_of_power by blast
  qed
  finally show ?thesis by auto 
qed  

lemma t_get_min_bound: 
  assumes "invar ts"
  assumes "ts\<noteq>[]"
  shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
  using assms t_get_min_bound_aux unfolding invar_def by blast  
  
thm fold_simps -- \<open>Theorems used by code generator\<close>
fun t_fold :: "('a \<Rightarrow> 'b \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> nat" 
  where
  "t_fold t_f f [] s = 1"
| "t_fold t_f f (x # xs) s = t_f x s + t_fold t_f f xs (f x s)"
    
text \<open>Estimation for constant function is enough for our purpose\<close>
lemma t_fold_const_bound:  
  shows "t_fold (\<lambda>_ _. K) f l s = K*length l + 1"  
  by (induction l arbitrary: s) auto

lemma t_fold_bounded_bound:  
  assumes "\<forall>x s. x\<in>set l \<longrightarrow> t_f x s \<le> K"
  shows "t_fold t_f f l s \<le> K*length l + 1"  
  using assms 
  apply (induction l arbitrary: s)
  apply (simp; fail)
  using add_mono
  by (fastforce simp: algebra_simps) 
  
thm rev_conv_fold -- \<open>Theorem used by code generator\<close>
definition "t_rev xs = t_fold (\<lambda>_ _. 1) op # xs []"
lemma t_rev_bound: "t_rev xs = length xs + 1"
  unfolding t_rev_def t_fold_const_bound by auto
    
definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" 
  where
  "t_del_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
                    \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
  )"
  
lemma t_rev_ts1_bound_aux: 
  fixes ts
  defines "n \<equiv> size (mset_heap ts)"
  assumes BINVAR: "invar_bheap (rev ts)"
  shows "t_rev ts \<le> 1 + log 2 (n+1)"
proof -
  have "t_rev ts = length ts + 1"
    by (auto simp: t_rev_bound)
  hence "2^t_rev ts = 2*2^length ts" by auto
  also have "\<dots> \<le> 2*n+2" using size_bheap[OF BINVAR] by (auto simp: n_def)
  finally have "2 ^ t_rev ts \<le> 2 * n + 2" .
  from le_log2_of_power[OF this] have "t_rev ts \<le> log 2 (2 * (n + 1))"
    by auto
  also have "\<dots> = 1 + log 2 (n+1)"
    by (simp only: of_nat_mult log_mult) auto  
  finally show ?thesis by (auto simp: algebra_simps)
qed    
  
  
lemma t_del_min_bound_aux:
  fixes ts
  defines "n \<equiv> size (mset_heap ts)"
  assumes BINVAR: "invar_bheap ts"
  assumes "ts\<noteq>[]"
  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"  
proof -
  obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
    by (metis surj_pair tree.exhaust_sel)

  note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap)

  define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
  define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
      
  have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
  proof -
    note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
    also have "n\<^sub>1 \<le> n" 
      unfolding n\<^sub>1_def n_def
      using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
      by (auto simp: mset_heap_def)
    finally show ?thesis by (auto simp: algebra_simps)
  qed    
    
  have "t_del_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
    unfolding t_del_min_def by (simp add: GM)
  also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
    using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def)
  also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
    using t_rev_ts1_bound by auto
  also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
    using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
    by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
  also have "n\<^sub>1 + n\<^sub>2 \<le> n"
    unfolding n\<^sub>1_def n\<^sub>2_def n_def
    using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
    by (auto simp: mset_heap_def)
  finally have "t_del_min ts \<le> 6 * log 2 (n+1) + 3" 
    by auto
  thus ?thesis by (simp add: algebra_simps)
qed      
  
lemma t_del_min_bound:
  fixes ts
  defines "n \<equiv> size (mset_heap ts)"
  assumes "invar ts"
  assumes "ts\<noteq>[]"
  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"  
  using assms t_del_min_bound_aux unfolding invar_def by blast

subsection \<open>Instantiating the Priority Queue Locale\<close>

interpretation binheap: 
  Priority_Queue "[]" "op = []" ins find_min del_min invar mset_heap
proof (unfold_locales, goal_cases)
  case 1
  then show ?case by simp
next
  case (2 q)
  then show ?case by auto
next
  case (3 q x)
  then show ?case by auto
next
  case (4 q)
  then show ?case using del_min_mset[of q] find_min[OF _ \<open>invar q\<close>] 
    by (auto simp: union_single_eq_diff)
next
  case (5 q)
  then show ?case using find_min[of q] by auto
next 
  case 6 
  then show ?case by (auto simp add: invar_def invar_bheap_def oheap_invar_def)
next
  case (7 q x)
  then show ?case by simp
next
  case (8 q)
  then show ?case by simp
qed
    
    
(* Exercise? *)    
subsection \<open>Combined Find and Delete Operation\<close>
  
text \<open>We define an operation that returns the minimum element and 
  a heap with this element removed. \<close>
definition pop_min :: "'a::linorder heap \<Rightarrow> 'a \<times> 'a::linorder heap" 
  where
  "pop_min ts = (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) 
                    \<Rightarrow> (x,merge (rev ts\<^sub>1) ts\<^sub>2)
  )"
    
lemma pop_min_refine:  
  assumes "ts \<noteq> []"
  shows "pop_min ts = (find_min ts, del_min ts)"
  unfolding pop_min_def del_min_def
  by (auto 
      split: prod.split tree.split 
      dest: get_min_find_min_same_root[OF assms])
  
lemma pop_min_invar:
  assumes "ts \<noteq> []"
  assumes "invar ts"
  assumes "pop_min ts = (x,ts')"  
  shows "invar ts'"  
  using del_min_invar[of ts] pop_min_refine[of ts] assms by simp

lemma pop_min_mset:    
  assumes "ts \<noteq> []"
  assumes "invar ts"
  assumes "pop_min ts = (x,ts')"  
  shows "mset_heap ts = add_mset x (mset_heap ts')"
  using del_min_mset[of ts] pop_min_refine[of ts] assms by simp 
  
lemma pop_min_min:
  assumes "ts \<noteq> []"
  assumes "invar ts"
  assumes "pop_min ts = (x,ts')"  
  shows "\<forall>y\<in>#mset_heap ts'. x\<le>y"
  using pop_min_refine[of ts] del_min_mset[of ts] find_min_mset[of ts] assms
  by (auto simp del: binheap.mset_simps)
    

definition t_pop_min :: "'a::linorder heap \<Rightarrow> nat" 
  where
  "t_pop_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) 
                    \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
  )"
    
lemma t_pop_min_bound_aux:
  fixes ts
  defines "n \<equiv> size (mset_heap ts)"
  assumes BINVAR: "invar_bheap ts"
  assumes "ts\<noteq>[]"
  shows "t_pop_min ts \<le> 6 * log 2 (n+1) + 3"  
proof -
  obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
    by (metis surj_pair tree.exhaust_sel)

  note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap)

  define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
  define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
      
  have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
  proof -
    note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
    also have "n\<^sub>1 \<le> n" 
      unfolding n\<^sub>1_def n_def
      using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
      by (auto simp: mset_heap_def)
    finally show ?thesis by (auto simp: algebra_simps)
  qed

  have "t_pop_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
    unfolding t_pop_min_def by (simp add: GM)
  also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
    using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def)
  also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
    using t_rev_ts1_bound by auto
  also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
    using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
    by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
  also have "n\<^sub>1 + n\<^sub>2 \<le> n"
    unfolding n\<^sub>1_def n\<^sub>2_def n_def
    using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
    by (auto simp: mset_heap_def)
  finally have "t_pop_min ts \<le> 6 * log 2 (n+1) + 3" 
    by auto
  thus ?thesis by (simp add: algebra_simps)
qed      

end