binom tree slides, moved bin tree thys to public draft
authorlammich <lammich@in.tum.de>
Thu, 06 Jul 2017 15:00:28 +0200
changeset 69829 6c684a17800e
parent 69828 e59d2c2ee8b2
child 69830 b73cacf0b109
binom tree slides, moved bin tree thys to public
Slides/Binomial_Tree_Slides.thy
Thys/BinHeap.thy
Thys/Heap_Prelim.thy
--- a/Slides/Binomial_Tree_Slides.thy	Thu Jul 06 14:57:19 2017 +0200
+++ b/Slides/Binomial_Tree_Slides.thy	Thu Jul 06 15:00:28 2017 +0200
@@ -2,10 +2,21 @@
 theory Binomial_Tree_Slides
 imports
   Tree_Notation
-  "../Thys/BinHeap"
+  "../../Public/Thys/BinHeap"
 begin
+  
+thm btree_invar.simps[unfolded compl_descending_def]
+  
+lemmas merge_simps = merge.simps(1) merge_simp2 merge.simps(3)
+  
+thm get_min.simps  
+  
+lemma find_min_alt: "ts\<noteq>[] \<Longrightarrow> find_min ts = Min (set (map root ts))"  
+  by (induction ts rule: find_min.induct) (auto simp: Let_def min_def)
 
-
+abbreviation (latex) sz_tree ("|_|") where "sz_tree t \<equiv> size (mset_tree t)"
+abbreviation (latex) sz_heap ("|_|") where "sz_heap t \<equiv> size (mset_heap t)"
+    
 (*>*)
 text_raw{*
 \end{isabellebody}%
@@ -15,12 +26,12 @@
 
 %-------------------------------------------------------------
 
-\begin{frame}{Numerical Method}
+\begin{frame}{Numerical Method}{See \emph{Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999}}
   Only use trees \<open>t\<^sub>i\<close> of size \<open>2\<^sup>i\<close>\\
-  \bigskip\pause
+  \smallskip\pause
 
-  E.g., to store \<open>0b1001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3]\<close>\\
-  \bigskip\pause
+  E.g., to store \<open>0b11001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close>\\
+  \smallskip\pause
 
   Meld: Addition with carry. \\
   \smallskip\pause
@@ -28,45 +39,119 @@
 \end{frame}
 
 \begin{frame}{Organization of Trees}
-  Tree of size \<open>2\<^sup>i\<close> has \emph{rank} \<open>i\<close>\\
-  \bigskip\pause
+  \high{@{theory_text \<open>(*<*)datatype (*>*)'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")\<close>}}\\
+  \smallskip\pause
+  
+  Node with rank \<open>i\<close> has successors \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>
+  with ranks \<open>[i-1,\<dots>,0]\<close>
+  \high{@{thm [display] btree_invar.simps[unfolded compl_descending_def]}}
+  \smallskip\pause
 
-  Node with rank \<open>i\<close> has successors \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>
-  with ranks \<open>[i-1,\<dots>,0]\<close>\\
+  Tree has exactly @{term \<open>(2::nat)^rank t\<close>} nodes
+  \high{@{thm [display] size_btree}}
 \end{frame}
 
-\begin{frame}{Sparse Binary Numbers}
-  Using sparse binary numbers: \\
-  \<open>[t\<^sub>0,0,0,t\<^sub>3]\<close> represented as \<open>[ (0,t\<^sub>0), (3,t\<^sub>3) ]\<close>
+\begin{frame}{Linking two Trees}
+  Given two trees of rank \<open>i\<close>, join them to tree of rank \<open>i+1\<close>.\\
+  \smallskip\pause
+
+  Idea: Insert one tree under root of other tree
+  \smallskip\pause
+
+  \high{@{thm[display] link_def}}
 \end{frame}
 
 \begin{frame}{Heap Datatype}
-  \high{\<open>'a tree\<close>\\~~~\<open>= Node (rank: nat) (root: 'a) (children: "'a tree list")\<close>}\\
-  \high{\<open>'a heap = 'a tree list\<close>}\\
+  Using sparse representation for binary numbers: \\
+  \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close> represented as \<open>[ (0,t\<^sub>0), (3,t\<^sub>3),(4,t\<^sub>4) ]\<close>
   \bigskip\pause
 
-  \high{@{thm btree_invar.simps}}\\
+  \high{@{theory_text \<open>(*<*)type_synonym (*>*)'a heap = "'a tree list"\<close>}}
   \smallskip\pause
-  Ranks of successors in \high{descending} order\\
-  \smallskip\pause
-  Sparse implementation has no advantage here, but code gets more readable [Okasaki]\\
-  \bigskip\pause
 
   \high{@{thm bheap_invar_def}}\\
   Ranks in \high{ascending} order\\
 \end{frame}
 
 \begin{frame}{Inserting a Tree}
-  \high{@{thm ins_tree.simps}}\\
+  \high{@{thm [display, margin=60] ins_tree.simps}}
+  \smallskip\pause
+
+  Intuition: Handle a carry
+  \smallskip\pause
+
+  Precondition:\\
+  Rank of inserted tree \<open>\<le>\<close> ranks of trees in heap \\
+\end{frame}
+
+\begin{frame}{Merge}
+  \high{@{thm [display] merge_simps}}
+  \smallskip\pause
+
+  Intuition: Addition of binary numbers
   \smallskip\pause
-  Precondition: Rank of inserted tree \<open>\<le>\<close> ranks of trees in heap \\
+
+  Note: Handling of carry after recursive call
+\end{frame}
+
+\begin{frame}{Find/Delete Minimum Element}
+  All trees are min-heaps
+  \smallskip\pause
+
+  Smallest element may be any root node
+  \high{@{thm [display] find_min_alt}}
+  \smallskip\pause
+
+  Similar: \high{@{term_type get_min}} \\
+  Returns tree with minimal root, and other trees
+
   \smallskip\pause
-  Intuition: Increment, handle carry \\
-  \bigskip\pause
-  Link: One tree inserted under root of other\\
-  \high{@{thm link_def}}\\
+  Delete via merge
+  \high{@{thm [display, margin=60] delete_min_def}}
+  Note the \<open>rev\<close>!
+
+\end{frame}
+
+\begin{frame}{Complexity}
+  Recall: @{term \<open>size (mset_tree t) = 2^rank t\<close>}
+  \smallskip\pause
+
+  Similarly for heap: @{term \<open>size (mset_heap h) \<ge> 2^length h\<close>}
+  \smallskip\pause
+
+  Complexity of operations: linear in length of heap\\ \pause
+  i.e., logarithmic in number of elements
+  \smallskip\pause
+
+  Proofs: \pause straightforward\pause ?
 \end{frame}
 
+\begin{frame}{Complexity of Merge}
+  \high{@{thm [display] merge_simps(3)}}
+  \smallskip\pause
+
+  Complexity of @{const ins_tree} call depends on length of result of recursive call.
+  \smallskip\pause
+
+  Naive: @{term \<open>length (merge ts\<^sub>1 ts\<^sub>2) \<le> length ts\<^sub>1 + length ts\<^sub>2\<close>}
+  \smallskip\pause
+
+  Yields (roughly) \<open>m n = m (n-2) + n\<close> \pause quadratic!
+\end{frame}
+
+\begin{frame}{Complexity of Merge}
+  \high{@{thm [display] merge_simps(3)}}
+  \smallskip\pause
+
+  Idea: Estimate cost and length of result:
+  \high{@{thm [display, margin=60] l_ins_tree_estimate l_merge_estimate}}
+
+  \smallskip\pause
+  Yields desired linear bound!
+\end{frame}
+
+
+
 \begin{isabellebody}%
 *}
 (*<*)
--- a/Thys/BinHeap.thy	Thu Jul 06 14:57:19 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,836 +0,0 @@
-(* Author: Peter Lammich *)
-section \<open>Binomial Heaps\<close>
-theory BinHeap
-imports Complex_Main
-  "../../Public/Thys/Priority_Queue"
-  "Heap_Prelim"
-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 btree_invar :: "'a::linorder tree \<Rightarrow> bool" 
-  where
-    "btree_invar (Node r _ c) \<longleftrightarrow> 
-      (\<forall>t\<in>set c. btree_invar t) 
-    \<and> (compl_descending r (map rank c))
-"
-
-definition bheap_invar :: "'a::linorder heap \<Rightarrow> bool" where
-  "bheap_invar c 
-  \<longleftrightarrow> (\<forall>t\<in>set c. btree_invar t) \<and> (strictly_ascending (map rank c))"
-  
-text \<open>Ordering (heap) invariant\<close>
-fun otree_invar :: "'a::linorder tree \<Rightarrow> bool"
-  where
-    "otree_invar (Node _ x c) \<longleftrightarrow> (\<forall>t\<in>set c. otree_invar t \<and> x \<le> root t)"
-
-definition oheap_invar :: "'a::linorder heap \<Rightarrow> bool" where
-  "oheap_invar c \<longleftrightarrow> (\<forall>t\<in>set c. otree_invar t)"
-  
-definition invar :: "'a::linorder heap \<Rightarrow> bool" where
-  "invar ts \<longleftrightarrow> bheap_invar 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_bheap_invar: 
-  "btree_invar (Node r v ts) \<Longrightarrow> bheap_invar (rev ts)"  
-  by (auto 
-      simp: bheap_invar_def 
-      simp: rev_map[symmetric]
-      dest: compl_is_strictly_descending
-      )
-      
-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_btree_invar:
-  assumes "btree_invar t\<^sub>1"
-  assumes "btree_invar t\<^sub>2"
-  assumes "rank t\<^sub>1 = rank t\<^sub>2"  
-  shows "btree_invar (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#rest) = (
-    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#rest else ins_tree (link t\<^sub>1 t\<^sub>2) rest
-  )"  
-    
-lemma bheap_invar_Cons[simp]: 
-  "bheap_invar (t#ts) 
-  \<longleftrightarrow> btree_invar t \<and> bheap_invar ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
-  unfolding bheap_invar_def
-  by auto  
-  
-lemma ins_tree_btree_invar:
-  assumes "btree_invar t" 
-  assumes "bheap_invar ts"
-  assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"  
-  shows "bheap_invar (ins_tree t ts)"  
-  using assms
-  apply (induction t ts rule: ins_tree.induct)  
-  apply (auto simp: link_btree_invar 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_btree_invar 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_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_bheap_invar:
-  assumes "bheap_invar ts\<^sub>1"
-  assumes "bheap_invar ts\<^sub>2"
-  shows "bheap_invar (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]: "btree_invar t\<^sub>1" "btree_invar 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]: "bheap_invar (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_btree_invar link_btree_invar)
-  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_bheap_invar 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: Let_def 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 simp: Let_def)
-  done  
-
-lemma find_min:    
-  assumes "mset_heap ts \<noteq> {#}"
-  assumes "invar ts"
-  shows "find_min ts = Min_mset (mset_heap ts)"
-  apply rule
-  using assms find_min_member find_min_mset  
-  by auto
-    
-
-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 simp: Let_def 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_bheap_invar:    
-  assumes "get_min ts = (t',ts')"  
-  assumes "ts\<noteq>[]"
-  assumes "bheap_invar ts"  
-  shows "btree_invar t'" and "bheap_invar ts'"
-proof -
-  have "btree_invar t' \<and> bheap_invar 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 "btree_invar t'" and "bheap_invar 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 delete_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" 
-  where
-  "delete_min ts = (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) 
-                    \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2
-  )"
-  
-lemma delete_min_invar[simp]:
-  assumes "ts \<noteq> []"
-  assumes "invar ts"
-  shows "invar (delete_min ts)"
-  using assms  
-  unfolding invar_def delete_min_def  
-  by (auto 
-      split: prod.split tree.split 
-      intro!: merge_bheap_invar merge_oheap_invar
-      dest: get_min_bheap_invar get_min_oheap_invar
-      intro!: children_oheap_invar children_bheap_invar
-      )
-    
-lemma delete_min_mset: 
-  assumes "ts \<noteq> []"
-  shows "mset_heap ts = mset_heap (delete_min ts) + {# find_min ts #}"
-  using assms
-  unfolding delete_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 "btree_invar 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_descending r (map rank ts)" by auto
-  hence COMPL: "map rank ts = rev [0..<r]" unfolding compl_descending_def .
-      
-  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 "bheap_invar ts"
-  shows "2^length ts \<le> size (mset_heap ts) + 1"
-proof -
-  from \<open>bheap_invar ts\<close> have 
-    ASC: "strictly_ascending (map rank ts)" and
-    TINV: "\<forall>t\<in>set ts. btree_invar t"
-    unfolding bheap_invar_def by auto
-      
-  have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1" 
-    by (simp add: power2sum)
-  also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
-    using strictly_ascending_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_bound: 
-  assumes "invar ts"
-  shows "t_ins x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
-proof -
-  have 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
-
-  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: "bheap_invar ts\<^sub>1" "bheap_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"
-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 "bheap_invar 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_delete_min :: "'a::linorder heap \<Rightarrow> nat" 
-  where
-  "t_delete_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: "bheap_invar (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_delete_min_bound_aux:
-  fixes ts
-  defines "n \<equiv> size (mset_heap ts)"
-  assumes BINVAR: "bheap_invar ts"
-  assumes "ts\<noteq>[]"
-  shows "t_delete_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_bheap_invar[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
-  hence BINVAR1: "bheap_invar (rev ts\<^sub>1)" by (blast intro: children_bheap_invar)
-
-  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_delete_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
-    unfolding t_delete_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>bheap_invar (rev ts\<^sub>1)\<close> \<open>bheap_invar 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_delete_min ts \<le> 6 * log 2 (n+1) + 3" 
-    by auto
-  thus ?thesis by (simp add: algebra_simps)
-qed      
-  
-lemma t_delete_min_bound:
-  fixes ts
-  defines "n \<equiv> size (mset_heap ts)"
-  assumes "invar ts"
-  assumes "ts\<noteq>[]"
-  shows "t_delete_min ts \<le> 6 * log 2 (n+1) + 3"  
-  using assms t_delete_min_bound_aux unfolding invar_def by blast
-
-subsection \<open>Instantiating the Priority Queue Locale\<close>
-
-interpretation binheap: 
-  Priority_Queue "[]" "op = []" ins find_min delete_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 delete_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 bheap_invar_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, delete_min ts)"
-  unfolding pop_min_def delete_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 delete_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 delete_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] delete_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: "bheap_invar 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_bheap_invar[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
-  hence BINVAR1: "bheap_invar (rev ts\<^sub>1)" by (blast intro: children_bheap_invar)
-
-  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>bheap_invar (rev ts\<^sub>1)\<close> \<open>bheap_invar 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
--- a/Thys/Heap_Prelim.thy	Thu Jul 06 14:57:19 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-section \<open>Preliminaries for Heap Formalization\<close>
-theory Heap_Prelim
-imports Complex_Main
-begin
-lemma power2sum: "(\<Sum>i\<in>{0..<k}. (2::nat)^i) = 2^k-1"    
-  by (induction k) auto
-  
-subsection \<open>Strictly Ascending and Descending Sequences\<close>
-definition strictly_ascending :: "'a::linorder list \<Rightarrow> bool" 
-  where
-  "strictly_ascending xs \<equiv> sorted xs \<and> distinct xs"
-  
-definition strictly_descending :: "'a::linorder list \<Rightarrow> bool" 
-  where
-  "strictly_descending xs \<equiv> sorted (rev xs) \<and> distinct xs"
-  
-text \<open>The sequence \<open>[r-1,\<dots>,0]\<close>: \<close>
-definition compl_descending :: "nat \<Rightarrow> nat list \<Rightarrow> bool" where   
-  "compl_descending r ns \<longleftrightarrow> (ns = rev [0..<r])"
-  
-lemma strictly_descending_alt: 
-  "strictly_descending = strictly_ascending o rev"  
-  unfolding strictly_descending_def strictly_ascending_def by auto
-  
-lemma strictly_ascending_Nil[simp, intro!]: "strictly_ascending []"
-  unfolding strictly_ascending_def by auto
-    
-lemma strictly_ascending_Cons[simp]:
-  "strictly_ascending (x#xs) \<longleftrightarrow> strictly_ascending xs \<and> (\<forall>y\<in>set xs. x<y)"  
-  unfolding strictly_ascending_def using le_neq_trans 
-  by (auto simp: sorted_Cons)
-
-lemma strictly_ascending_append[simp]:
-  "strictly_ascending (xs@ys) 
-  \<longleftrightarrow> strictly_ascending xs \<and> strictly_ascending ys 
-    \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. x<y)"  
-  by (induction xs) auto
-
-lemma strictly_descending_Nil[simp, intro!]: "strictly_descending []"
-  unfolding strictly_descending_def by auto
-    
-lemma strictly_descending_Cons[simp]:
-  "strictly_descending (x#xs) \<longleftrightarrow> strictly_descending xs \<and> (\<forall>y\<in>set xs. x>y)"  
-  unfolding strictly_descending_alt 
-  by (auto)
-
-lemma strictly_descending_append[simp]:
-  "strictly_descending (xs@ys) 
-  \<longleftrightarrow> strictly_descending xs \<and> strictly_descending ys 
-    \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. x>y)"  
-  unfolding strictly_descending_alt by auto
-    
-lemma strictly_ascending_rev[simp]: 
-  "strictly_ascending (rev xs) \<longleftrightarrow> strictly_descending xs"
-  unfolding strictly_descending_alt by auto
-
-lemma strictly_descending_rev[simp]: 
-  "strictly_descending (rev xs) \<longleftrightarrow> strictly_ascending xs"
-  unfolding strictly_descending_alt by auto
-    
-lemma compl_descending_Nil[simp]: 
-  "compl_descending 0 []"
-  "compl_descending r [] \<longleftrightarrow> r = 0"
-  "compl_descending 0 ns \<longleftrightarrow> ns=[]"
-  unfolding compl_descending_def by auto
-  
-lemma compl_descending_Cons[simp]: 
-  "compl_descending r (n#ns) \<longleftrightarrow> (r = Suc n \<and> compl_descending n ns)"
-  unfolding compl_descending_def
-  by (cases r) (auto)
-
-lemma compl_is_strictly_descending: 
-  "compl_descending r ns \<Longrightarrow> strictly_descending ns"    
-  unfolding compl_descending_def strictly_descending_def
-  by auto  
-
-subsubsection \<open>Strictly Ascending Sequences of Natural Numbers\<close>    
-  
-text \<open>Each element is greater or equal to its index\<close>
-lemma strictly_ascending_idx:
-  assumes "strictly_ascending ns"
-  shows "\<forall>i<length ns. i\<le>ns!i"
-  using assms
-  apply (induction ns rule: rev_induct)
-  subgoal by simp  
-  subgoal 
-    apply (clarsimp simp: nth_append)
-    by (metis less_antisym not_less nth_mem)  
-  done
-
-text \<open>Summation of a strictly ascending sequence with length \<open>n\<close> 
-  can be estimated by summation over \<open>{0..<n}\<close>.
-\<close>
-lemma strictly_ascending_sum_mono_lowerbound:
-  fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)"
-  assumes "strictly_ascending ns"
-  assumes MONO: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y"  
-  shows "(\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)"
-  using assms
-proof (induction ns rule: rev_induct)
-  case Nil
-  then show ?case by simp
-next
-  case (snoc n ns)
-  hence IH: "sum f {0..<length ns} \<le> sum_list (map f ns)"
-    by auto
-      
-  from strictly_ascending_idx[OF snoc.prems(1), THEN spec[of _ "length ns"]]
-  have NGE: "length ns \<le> n" by auto 
-
-  have "sum f {0..<length (ns @ [n])} 
-      = sum f {0..<length ns} + f (length ns)"    
-    by simp
-  also note IH
-  also note NGE
-  finally have "sum f {0..<length (ns @ [n])} \<le> sum_list (map f ns) + f n"
-    using MONO add_mono by blast
-  thus ?case by simp
-qed      
-
-end