# HG changeset patch
# User nipkow
# Date 1504013822 -7200
# Node ID 188c7853f84abb829ef71f1bc0ca8edcc113a8bb
# Parent  14a7d2a3933682dc4cc1bd91fd3538d7f23cec66
typo

diff -r 14a7d2a39336 -r 188c7853f84a src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Aug 29 15:07:15 2017 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Aug 29 15:37:02 2017 +0200
@@ -443,7 +443,7 @@
 qed
    
 text \<open>The length of a binomial heap is bounded by the number of its elements\<close>  
-lemma size_mset_heap:      
+lemma size_mset_bheap:      
   assumes "invar_bheap ts"
   shows "2^length ts \<le> size (mset_heap ts) + 1"
 proof -
@@ -498,7 +498,7 @@
     unfolding t_insert_def by (rule t_ins_tree_simple_bound)
   also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))" 
   proof -
-    from size_mset_heap[of ts] assms 
+    from size_mset_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
@@ -547,8 +547,8 @@
     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_mset_heap]
-  also note BINVARS(2)[THEN size_mset_heap]
+  also note BINVARS(1)[THEN size_mset_bheap]
+  also note BINVARS(2)[THEN size_mset_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>"    
@@ -591,7 +591,7 @@
   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_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+    from size_mset_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
@@ -615,7 +615,7 @@
   have 1: "t_get_min_rest ts = length ts" using assms t_get_min_rest_estimate by auto
   also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
   proof -
-    from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+    from size_mset_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
@@ -647,7 +647,7 @@
 proof -
   have "t_rev ts = length ts + 1" by (auto simp: t_rev_def)
   hence "2^t_rev ts = 2*2^length ts" by auto
-  also have "\<dots> \<le> 2*n+2" using size_mset_heap[OF BINVAR] by (auto simp: n_def)
+  also have "\<dots> \<le> 2*n+2" using size_mset_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