# HG changeset patch
# User nipkow
# Date 1502828608 -7200
# Node ID 36a01c02d0ca4dab8ba409aef80d950174aac299
# Parent  ad1e8ad9a3aec75a4ba70bff1952ff58bb2f26e1# Parent  292680dde31447623a1b5a1fe27a5f938a4ea638
merged

diff -r ad1e8ad9a3ae -r 36a01c02d0ca NEWS
--- a/NEWS	Tue Aug 15 18:15:04 2017 +0200
+++ b/NEWS	Tue Aug 15 22:23:28 2017 +0200
@@ -131,8 +131,11 @@
 
 * Material on infinite products in HOL-Analysis
 
-* "sublist" from theory List renamed to "nths" in analogy with "nth".
-"sublisteq" renamed to "subseq".  Minor INCOMPATIBILITY.
+* Theory List:
+  "sublist" renamed to "nths" in analogy with "nth".
+  "sublisteq" renamed to "subseq".
+  Minor INCOMPATIBILITY.
+  New generic function "sorted_wrt"
 
 * Theories "GCD" and "Binomial" are already included in "Main" (instead
 of "Complex_Main").
diff -r ad1e8ad9a3ae -r 36a01c02d0ca src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue Aug 15 18:15:04 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Tue Aug 15 22:23:28 2017 +0200
@@ -563,6 +563,7 @@
 @{const List.shuffle} & @{typeof List.shuffle}\\
 @{const List.sort} & @{typeof List.sort}\\
 @{const List.sorted} & @{typeof List.sorted}\\
+@{const List.sorted_wrt} & @{typeof List.sorted_wrt}\\
 @{const List.splice} & @{typeof List.splice}\\
 @{const List.take} & @{typeof List.take}\\
 @{const List.takeWhile} & @{typeof List.takeWhile}\\
diff -r ad1e8ad9a3ae -r 36a01c02d0ca src/HOL/Data_Structures/Binomial_Heap.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Aug 15 22:23:28 2017 +0200
@@ -0,0 +1,836 @@
+(* Author: Peter Lammich *)
+
+section \<open>Binomial Heap\<close>
+
+theory Binomial_Heap
+imports
+  Complex_Main
+  Priority_Queue
+begin
+
+lemma sum_power2: "(\<Sum>i\<in>{0..<k}. (2::nat)^i) = 2^k-1"    
+by (induction k) auto
+
+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: 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)"
+  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 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_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
diff -r ad1e8ad9a3ae -r 36a01c02d0ca src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/Groups_List.thy	Tue Aug 15 22:23:28 2017 +0200
@@ -286,6 +286,31 @@
   with assms(1) show ?thesis by simp
 qed
 
+text \<open>Summation of a strictly ascending sequence with length \<open>n\<close> 
+  can be upper-bounded by summation over \<open>{0..<n}\<close>.\<close>
+
+lemma sorted_wrt_less_sum_mono_lowerbound:
+  fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)"
+  assumes mono: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y"
+  shows "sorted_wrt (op <) ns \<Longrightarrow>
+    (\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)"
+proof (induction ns rule: rev_induct)
+  case Nil
+  then show ?case by simp
+next
+  case (snoc n ns)
+  have "sum f {0..<length (ns @ [n])} 
+      = sum f {0..<length ns} + f (length ns)"    
+    by simp
+  also have "sum f {0..<length ns} \<le> sum_list (map f ns)"
+    using snoc by (auto simp: sorted_wrt_append)
+  also have "length ns \<le> n"
+    using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto 
+  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      
+
 
 subsection \<open>Further facts about @{const List.n_lists}\<close>
 
diff -r ad1e8ad9a3ae -r 36a01c02d0ca src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Aug 15 22:23:28 2017 +0200
@@ -2086,7 +2086,7 @@
 
 lemma set_sorted_list_of_multiset [simp]:
   "set (sorted_list_of_multiset M) = set_mset M"
-by (induct M) (simp_all add: set_insort)
+by (induct M) (simp_all add: set_insort_key)
 
 lemma sorted_list_of_mset_set [simp]:
   "sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
diff -r ad1e8ad9a3ae -r 36a01c02d0ca src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/List.thy	Tue Aug 15 22:23:28 2017 +0200
@@ -333,6 +333,17 @@
 text\<open>The following simple sort functions are intended for proofs,
 not for efficient implementations.\<close>
 
+text \<open>A sorted predicate w.r.t. a relation:\<close>
+
+fun sorted_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+"sorted_wrt P [] = True" |
+"sorted_wrt P [x] = True" |
+"sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
+
+(* FIXME: define sorted in terms of sorted_wrt *)
+
+text \<open>A class-based sorted predicate:\<close>
+
 context linorder
 begin
 
@@ -4844,73 +4855,69 @@
 
 subsection \<open>Sorting\<close>
 
-text\<open>Currently it is not shown that @{const sort} returns a
-permutation of its input because the nicest proof is via multisets,
-which are not yet available. Alternatively one could define a function
-that counts the number of occurrences of an element in a list and use
-that instead of multisets to state the correctness property.\<close>
+
+subsubsection \<open>@{const sorted_wrt}\<close>
+
+lemma sorted_wrt_induct:
+  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma sorted_wrt_Cons:
+assumes "transp P"
+shows   "sorted_wrt P (x # xs) = ((\<forall>y \<in> set xs. P x y) \<and> sorted_wrt P xs)"
+by(induction xs arbitrary: x)(auto intro: transpD[OF assms])
+
+lemma sorted_wrt_ConsI:
+  "\<lbrakk> transp P; \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow>
+  sorted_wrt P (x # xs)"
+by (simp add: sorted_wrt_Cons)
+
+lemma sorted_wrt_append:
+assumes "transp P"
+shows "sorted_wrt P (xs @ ys) \<longleftrightarrow>
+  sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"  
+by (induction xs) (auto simp: sorted_wrt_Cons[OF assms])
+
+lemma sorted_wrt_rev: assumes "transp P"
+shows "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
+proof(induction xs rule: sorted_wrt_induct)
+  case 3 thus ?case
+    by(simp add: sorted_wrt_append sorted_wrt_Cons assms)
+      (meson assms transpD)
+qed simp_all
+
+text \<open>Strictly Ascending Sequences of Natural Numbers\<close>    
+
+lemma sorted_wrt_upt[simp]: "sorted_wrt (op <) [0..<n]"
+by(induction n) (auto simp: sorted_wrt_append)
+
+text \<open>Each element is greater or equal to its index:\<close>
+
+lemma sorted_wrt_less_idx:
+  "sorted_wrt (op <) ns \<Longrightarrow> i < length ns \<Longrightarrow> i \<le> ns!i"
+proof (induction ns arbitrary: i rule: rev_induct)
+  case Nil thus ?case by simp
+next
+  case snoc
+  thus ?case
+    by (auto simp: nth_append sorted_wrt_append)
+       (metis less_antisym not_less nth_mem)  
+qed
+
+
+subsubsection \<open>@{const sorted}\<close>
 
 context linorder
 begin
 
-lemma set_insort_key:
-  "set (insort_key f x xs) = insert x (set xs)"
-  by (induct xs) auto
-
-lemma length_insort [simp]:
-  "length (insort_key f x xs) = Suc (length xs)"
-  by (induct xs) simp_all
-
-lemma insort_key_left_comm:
-  assumes "f x \<noteq> f y"
-  shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
-  by (induct xs) (auto simp add: assms dest: antisym)
-
-lemma insort_left_comm:
-  "insort x (insort y xs) = insort y (insort x xs)"
-  by (cases "x = y") (auto intro: insort_key_left_comm)
-
-lemma comp_fun_commute_insort:
-  "comp_fun_commute insort"
-proof
-qed (simp add: insort_left_comm fun_eq_iff)
-
-lemma sort_key_simps [simp]:
-  "sort_key f [] = []"
-  "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
-  by (simp_all add: sort_key_def)
-
-lemma (in linorder) sort_key_conv_fold:
-  assumes "inj_on f (set xs)"
-  shows "sort_key f xs = fold (insort_key f) xs []"
-proof -
-  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
-  proof (rule fold_rev, rule ext)
-    fix zs
-    fix x y
-    assume "x \<in> set xs" "y \<in> set xs"
-    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
-    have **: "x = y \<longleftrightarrow> y = x" by auto
-    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
-      by (induct zs) (auto intro: * simp add: **)
-  qed
-  then show ?thesis by (simp add: sort_key_def foldr_conv_fold)
-qed
-
-lemma (in linorder) sort_conv_fold:
-  "sort xs = fold insort xs []"
-  by (rule sort_key_conv_fold) simp
-
-lemma length_sort[simp]: "length (sort_key f xs) = length xs"
-by (induct xs, auto)
-
-lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
-apply(induct xs arbitrary: x) apply simp
+lemma sorted_Cons: "sorted (x#xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x \<le> y))"
+apply(induction xs arbitrary: x)
+ apply simp
 by simp (blast intro: order_trans)
 
 lemma sorted_tl:
   "sorted xs \<Longrightarrow> sorted (tl xs)"
-  by (cases xs) (simp_all add: sorted_Cons)
+by (cases xs) (simp_all add: sorted_Cons)
 
 lemma sorted_append:
   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
@@ -4954,86 +4961,22 @@
   "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
 by (auto intro: sorted_nth_monoI sorted_nth_mono)
 
-lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
-by (induct xs) auto
-
-lemma set_sort[simp]: "set(sort_key f xs) = set xs"
-by (induct xs) (simp_all add:set_insort)
-
-lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
-by(induct xs)(auto simp:set_insort)
-
-lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
-  by (induct xs) (simp_all add: distinct_insort)
-
-lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
-  by (induct xs) (auto simp:sorted_Cons set_insort)
-
-lemma sorted_insort: "sorted (insort x xs) = sorted xs"
-  using sorted_insort_key [where f="\<lambda>x. x"] by simp
-
-theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
-  by (induct xs) (auto simp:sorted_insort_key)
-
-theorem sorted_sort [simp]: "sorted (sort xs)"
-  using sorted_sort_key [where f="\<lambda>x. x"] by simp
+lemma sorted_map_remove1:
+  "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
+by (induct xs) (auto simp add: sorted_Cons)
+
+lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
+using sorted_map_remove1 [of "\<lambda>x. x"] by simp
 
 lemma sorted_butlast:
   assumes "xs \<noteq> []" and "sorted xs"
   shows "sorted (butlast xs)"
 proof -
-  from \<open>xs \<noteq> []\<close> obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
+  from \<open>xs \<noteq> []\<close> obtain ys y where "xs = ys @ [y]"
+    by (cases xs rule: rev_cases) auto
   with \<open>sorted xs\<close> show ?thesis by (simp add: sorted_append)
 qed
 
-lemma insort_not_Nil [simp]:
-  "insort_key f a xs \<noteq> []"
-  by (induct xs) simp_all
-
-lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
-by (cases xs) auto
-
-lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
-  by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
-
-lemma sorted_map_remove1:
-  "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
-  by (induct xs) (auto simp add: sorted_Cons)
-
-lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
-  using sorted_map_remove1 [of "\<lambda>x. x"] by simp
-
-lemma insort_key_remove1:
-  assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
-  shows "insort_key f a (remove1 a xs) = xs"
-using assms proof (induct xs)
-  case (Cons x xs)
-  then show ?case
-  proof (cases "x = a")
-    case False
-    then have "f x \<noteq> f a" using Cons.prems by auto
-    then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
-    with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
-  qed (auto simp: sorted_Cons insort_is_Cons)
-qed simp
-
-lemma insort_remove1:
-  assumes "a \<in> set xs" and "sorted xs"
-  shows "insort a (remove1 a xs) = xs"
-proof (rule insort_key_remove1)
-  define n where "n = length (filter (op = a) xs) - 1"
-  from \<open>a \<in> set xs\<close> show "a \<in> set xs" .
-  from \<open>sorted xs\<close> show "sorted (map (\<lambda>x. x) xs)" by simp
-  from \<open>a \<in> set xs\<close> have "a \<in> set (filter (op = a) xs)" by auto
-  then have "set (filter (op = a) xs) \<noteq> {}" by auto
-  then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
-  then have "length (filter (op = a) xs) > 0" by simp
-  then have n: "Suc n = length (filter (op = a) xs)" by (simp add: n_def)
-  moreover have "replicate (Suc n) a = a # replicate n a"
-    by simp
-  ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
-qed
-
 lemma sorted_remdups[simp]:
   "sorted l \<Longrightarrow> sorted (remdups l)"
 by (induct l) (auto simp: sorted_Cons)
@@ -5069,14 +5012,6 @@
     by (blast intro: map_inj_on)
 qed
 
-lemma finite_sorted_distinct_unique:
-shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
-apply(drule finite_distinct_list)
-apply clarify
-apply(rule_tac a="sort xs" in ex1I)
-apply (auto simp: sorted_distinct_set_unique)
-done
-
 lemma
   assumes "sorted xs"
   shows sorted_take: "sorted (take n xs)"
@@ -5133,6 +5068,155 @@
   finally show "\<not> t < f x" by simp
 qed
 
+lemma sorted_map_same:
+  "sorted (map f [x\<leftarrow>xs. f x = g xs])"
+proof (induct xs arbitrary: g)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs)
+  then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
+  moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
+  ultimately show ?case by (simp_all add: sorted_Cons)
+qed
+
+lemma sorted_same:
+  "sorted [x\<leftarrow>xs. x = g xs]"
+using sorted_map_same [of "\<lambda>x. x"] by simp
+
+end
+
+
+subsubsection \<open>Sorting functions\<close>
+
+text\<open>Currently it is not shown that @{const sort} returns a
+permutation of its input because the nicest proof is via multisets,
+which are not yet available. Alternatively one could define a function
+that counts the number of occurrences of an element in a list and use
+that instead of multisets to state the correctness property.\<close>
+
+context linorder
+begin
+
+lemma set_insort_key:
+  "set (insort_key f x xs) = insert x (set xs)"
+by (induct xs) auto
+
+lemma length_insort [simp]:
+  "length (insort_key f x xs) = Suc (length xs)"
+by (induct xs) simp_all
+
+lemma insort_key_left_comm:
+  assumes "f x \<noteq> f y"
+  shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
+by (induct xs) (auto simp add: assms dest: antisym)
+
+lemma insort_left_comm:
+  "insort x (insort y xs) = insort y (insort x xs)"
+by (cases "x = y") (auto intro: insort_key_left_comm)
+
+lemma comp_fun_commute_insort: "comp_fun_commute insort"
+proof
+qed (simp add: insort_left_comm fun_eq_iff)
+
+lemma sort_key_simps [simp]:
+  "sort_key f [] = []"
+  "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+by (simp_all add: sort_key_def)
+
+lemma sort_key_conv_fold:
+  assumes "inj_on f (set xs)"
+  shows "sort_key f xs = fold (insort_key f) xs []"
+proof -
+  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
+  proof (rule fold_rev, rule ext)
+    fix zs
+    fix x y
+    assume "x \<in> set xs" "y \<in> set xs"
+    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
+    have **: "x = y \<longleftrightarrow> y = x" by auto
+    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
+      by (induct zs) (auto intro: * simp add: **)
+  qed
+  then show ?thesis by (simp add: sort_key_def foldr_conv_fold)
+qed
+
+lemma sort_conv_fold:
+  "sort xs = fold insort xs []"
+by (rule sort_key_conv_fold) simp
+
+lemma length_sort[simp]: "length (sort_key f xs) = length xs"
+by (induct xs, auto)
+
+lemma set_sort[simp]: "set(sort_key f xs) = set xs"
+by (induct xs) (simp_all add: set_insort_key)
+
+lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
+by(induct xs)(auto simp: set_insort_key)
+
+lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
+by (induct xs) (simp_all add: distinct_insort)
+
+lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
+by (induct xs) (auto simp: sorted_Cons set_insort_key)
+
+lemma sorted_insort: "sorted (insort x xs) = sorted xs"
+using sorted_insort_key [where f="\<lambda>x. x"] by simp
+
+theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
+by (induct xs) (auto simp:sorted_insort_key)
+
+theorem sorted_sort [simp]: "sorted (sort xs)"
+using sorted_sort_key [where f="\<lambda>x. x"] by simp
+
+lemma insort_not_Nil [simp]:
+  "insort_key f a xs \<noteq> []"
+by (induction xs) simp_all
+
+lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
+by (cases xs) auto
+
+lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
+by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
+
+lemma insort_key_remove1:
+  assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
+  shows "insort_key f a (remove1 a xs) = xs"
+using assms proof (induct xs)
+  case (Cons x xs)
+  then show ?case
+  proof (cases "x = a")
+    case False
+    then have "f x \<noteq> f a" using Cons.prems by auto
+    then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
+    with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
+  qed (auto simp: sorted_Cons insort_is_Cons)
+qed simp
+
+lemma insort_remove1:
+  assumes "a \<in> set xs" and "sorted xs"
+  shows "insort a (remove1 a xs) = xs"
+proof (rule insort_key_remove1)
+  define n where "n = length (filter (op = a) xs) - 1"
+  from \<open>a \<in> set xs\<close> show "a \<in> set xs" .
+  from \<open>sorted xs\<close> show "sorted (map (\<lambda>x. x) xs)" by simp
+  from \<open>a \<in> set xs\<close> have "a \<in> set (filter (op = a) xs)" by auto
+  then have "set (filter (op = a) xs) \<noteq> {}" by auto
+  then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
+  then have "length (filter (op = a) xs) > 0" by simp
+  then have n: "Suc n = length (filter (op = a) xs)" by (simp add: n_def)
+  moreover have "replicate (Suc n) a = a # replicate n a"
+    by simp
+  ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
+qed
+
+lemma finite_sorted_distinct_unique:
+shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
+apply(drule finite_distinct_list)
+apply clarify
+apply(rule_tac a="sort xs" in ex1I)
+apply (auto simp: sorted_distinct_set_unique)
+done
+
 lemma insort_insert_key_triv:
   "f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
   by (simp add: insort_insert_key_def)
@@ -5151,12 +5235,12 @@
 
 lemma set_insort_insert:
   "set (insort_insert x xs) = insert x (set xs)"
-  by (auto simp add: insort_insert_key_def set_insort)
+  by (auto simp add: insort_insert_key_def set_insort_key)
 
 lemma distinct_insort_insert:
   assumes "distinct xs"
   shows "distinct (insort_insert_key f x xs)"
-  using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort)
+using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort_key)
 
 lemma sorted_insort_insert_key:
   assumes "sorted (map f xs)"
@@ -5180,21 +5264,6 @@
   "filter P (sort_key f xs) = sort_key f (filter P xs)"
   by (induct xs) (simp_all add: filter_insort_triv filter_insort)
 
-lemma sorted_map_same:
-  "sorted (map f [x\<leftarrow>xs. f x = g xs])"
-proof (induct xs arbitrary: g)
-  case Nil then show ?case by simp
-next
-  case (Cons x xs)
-  then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
-  moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
-  ultimately show ?case by (simp_all add: sorted_Cons)
-qed
-
-lemma sorted_same:
-  "sorted [x\<leftarrow>xs. x = g xs]"
-  using sorted_map_same [of "\<lambda>x. x"] by simp
-
 lemma remove1_insort [simp]:
   "remove1 x (insort x xs) = xs"
   by (induct xs) simp_all
@@ -5391,13 +5460,6 @@
 sets to lists but one should convert in the other direction (via
 @{const set}).\<close>
 
-subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
-
-text\<open>This function maps (finite) linearly ordered sets to sorted
-lists. Warning: in most cases it is not a good idea to convert from
-sets to lists but one should convert in the other direction (via
-@{const set}).\<close>
-
 context linorder
 begin
 
@@ -5428,7 +5490,8 @@
 lemma sorted_list_of_set [simp]:
   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
     \<and> distinct (sorted_list_of_set A)"
-  by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
+by(induct A rule: finite_induct)
+  (simp_all add: set_insort_key sorted_insort distinct_insort)
 
 lemma distinct_sorted_list_of_set:
   "distinct (sorted_list_of_set A)"
diff -r ad1e8ad9a3ae -r 36a01c02d0ca src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/ROOT	Tue Aug 15 22:23:28 2017 +0200
@@ -213,6 +213,7 @@
     AA_Map
     Splay_Map
     Leftist_Heap
+    Binomial_Heap
   document_files "root.tex" "root.bib"
 
 session "HOL-Import" in Import = HOL +
diff -r ad1e8ad9a3ae -r 36a01c02d0ca src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/Relation.thy	Tue Aug 15 22:23:28 2017 +0200
@@ -438,6 +438,18 @@
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
   by (simp add: transp_def)
 
+lemma transp_le[simp]: "transp (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
+lemma transp_less[simp]: "transp (op < :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
+lemma transp_ge[simp]: "transp (op \<ge> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
+lemma transp_gr[simp]: "transp (op > :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
 
 subsubsection \<open>Totality\<close>