diff --git a/src/HOL/Data_Structures/Array_Braun.thy b/src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy
+++ b/src/HOL/Data_Structures/Array_Braun.thy
@@ -1,670 +1,670 @@
 (* Author: Tobias Nipkow, with contributions by Thomas Sewell *)
 
 section "Arrays via Braun Trees"
 
 theory Array_Braun
 imports
   Array_Specs
   Braun_Tree
 begin
 
 subsection "Array"
 
 fun lookup1 :: "'a tree \<Rightarrow> nat \<Rightarrow> 'a" where
 "lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))"
 
 fun update1 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "update1 n x Leaf = Node Leaf x Leaf" |
 "update1 n x (Node l a r) =
   (if n=1 then Node l x r else
    if even n then Node (update1 (n div 2) x l) a r
             else Node l a (update1 (n div 2) x r))"
 
 fun adds :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "adds [] n t = t" |
 "adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)"
 
 fun list :: "'a tree \<Rightarrow> 'a list" where
 "list Leaf = []" |
 "list (Node l x r) = x # splice (list l) (list r)"
 
 
 subsubsection "Functional Correctness"
 
 lemma size_list: "size(list t) = size t"
 by(induction t)(auto)
 
 lemma minus1_div2: "(n - Suc 0) div 2 = (if odd n then n div 2 else n div 2 - 1)"
 by auto arith
 
 lemma nth_splice: "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk>
   \<Longrightarrow> splice xs ys ! n = (if even n then xs else ys) ! (n div 2)"
 apply(induction xs ys arbitrary: n rule: splice.induct)
 apply (auto simp: nth_Cons' minus1_div2)
 done
 
 lemma div2_in_bounds:
   "\<lbrakk> braun (Node l x r); n \<in> {1..size(Node l x r)}; n > 1 \<rbrakk> \<Longrightarrow>
    (odd n \<longrightarrow> n div 2 \<in> {1..size r}) \<and> (even n \<longrightarrow> n div 2 \<in> {1..size l})"
 by auto arith
 
 declare upt_Suc[simp del]
 
 
 paragraph \<open>\<^const>\<open>lookup1\<close>\<close>
 
 lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)"
 proof(induction t arbitrary: i)
   case Leaf thus ?case by simp
 next
   case Node
   thus ?case using div2_in_bounds[OF Node.prems(1), of "i+1"]
     by (auto simp: nth_splice minus1_div2 size_list)
 qed
 
 lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]"
 by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
 
 
 paragraph \<open>\<^const>\<open>update1\<close>\<close>
 
 lemma size_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t"
 proof(induction t arbitrary: n)
   case Leaf thus ?case by simp
 next
   case Node thus ?case using div2_in_bounds[OF Node.prems] by simp
 qed
 
 lemma braun_update1: "\<lbrakk>braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> braun(update1 n x t)"
 proof(induction t arbitrary: n)
   case Leaf thus ?case by simp
 next
   case Node thus ?case
     using div2_in_bounds[OF Node.prems] by (simp add: size_update1)
 qed
 
 lemma lookup1_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow>
   lookup1 (update1 n x t) m = (if n=m then x else lookup1 t m)"
 proof(induction t arbitrary: m n)
   case Leaf
   then show ?case by simp
 next
   have aux: "\<lbrakk> odd n; odd m \<rbrakk> \<Longrightarrow> n div 2 = (m::nat) div 2 \<longleftrightarrow> m=n" for m n
     using odd_two_times_div_two_succ by fastforce
   case Node
   thus ?case using div2_in_bounds[OF Node.prems] by (auto simp: aux)
 qed
 
 lemma list_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
 by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1)
 
 text \<open>A second proof of @{thm list_update1}:\<close>
 
 lemma diff1_eq_iff: "n > 0 \<Longrightarrow> n - Suc 0 = m \<longleftrightarrow> n = m+1"
 by arith
 
 lemma list_update_splice:
   "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk> \<Longrightarrow>
   (splice xs ys) [n := x] =
   (if even n then splice (xs[n div 2 := x]) ys else splice xs (ys[n div 2 := x]))"
 by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split)
 
 lemma list_update2: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
 proof(induction t arbitrary: n)
   case Leaf thus ?case by simp
 next
   case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems]
     by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split)
 qed
 
 
 paragraph \<open>\<^const>\<open>adds\<close>\<close>
 
 lemma splice_last: shows
   "size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"
 and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"
 by(induction xs ys arbitrary: x y rule: splice.induct) (auto)
 
 lemma list_add_hi: "braun t \<Longrightarrow> list(update1 (Suc(size t)) x t) = list t @ [x]"
 by(induction t)(auto simp: splice_last size_list)
 
 lemma size_add_hi: "braun t \<Longrightarrow> m = size t \<Longrightarrow> size(update1 (Suc m) x t) = size t + 1"
 by(induction t arbitrary: m)(auto)
 
 lemma braun_add_hi: "braun t \<Longrightarrow> braun(update1 (Suc(size t)) x t)"
 by(induction t)(auto simp: size_add_hi)
 
 lemma size_braun_adds:
   "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> size(adds xs n t) = size t + length xs \<and> braun (adds xs n t)"
 by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi)
 
 lemma list_adds: "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> list(adds xs n t) = list t @ xs"
 by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi)
 
 
 subsubsection "Array Implementation"
 
 interpretation A: Array
 where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
 and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
 and len = "\<lambda>(t,l). l"
 and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
 and invar = "\<lambda>(t,l). braun t \<and> l = size t"
 and list = "\<lambda>(t,l). list t"
 proof (standard, goal_cases)
   case 1 thus ?case by (simp add: nth_list_lookup1 split: prod.splits)
 next
   case 2 thus ?case by (simp add: list_update1 split: prod.splits)
 next
   case 3 thus ?case by (simp add: size_list split: prod.splits)
 next
   case 4 thus ?case by (simp add: list_adds)
 next
   case 5 thus ?case by (simp add: braun_update1 size_update1 split: prod.splits)
 next
   case 6 thus ?case by (simp add: size_braun_adds split: prod.splits)
 qed
 
 
 subsection "Flexible Array"
 
 fun add_lo where
 "add_lo x Leaf = Node Leaf x Leaf" |
 "add_lo x (Node l a r) = Node (add_lo a r) x l"
 
 fun merge where
 "merge Leaf r = r" |
 "merge (Node l a r) rr = Node rr a (merge l r)"
 
 fun del_lo where
 "del_lo Leaf = Leaf" |
 "del_lo (Node l a r) = merge l r"
 
 fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "del_hi n Leaf = Leaf" |
 "del_hi n (Node l x r) =
   (if n = 1 then Leaf
    else if even n
        then Node (del_hi (n div 2) l) x r
        else Node l x (del_hi (n div 2) r))"
 
 
 subsubsection "Functional Correctness"
 
 
 paragraph \<open>\<^const>\<open>add_lo\<close>\<close>
 
 lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"
 by(induction t arbitrary: a) auto
 
 lemma braun_add_lo: "braun t \<Longrightarrow> braun(add_lo x t)"
 by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
 
 
 paragraph \<open>\<^const>\<open>del_lo\<close>\<close>
 
 lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"
 by (induction l r rule: merge.induct) auto
 
 lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)"
 by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list)
 
 lemma list_del_lo: "braun t \<Longrightarrow> list(del_lo t) = tl (list t)"
 by (cases t) (simp_all add: list_merge)
 
 lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)"
 by (cases t) (simp_all add: braun_merge)
 
 
 paragraph \<open>\<^const>\<open>del_hi\<close>\<close>
 
 lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"
 by(cases t) simp_all
 
 lemma butlast_splice: "butlast (splice xs ys) =
   (if size xs > size ys then splice (butlast xs) ys else splice xs (butlast ys))"
 by(induction xs ys rule: splice.induct) (auto)
 
 lemma list_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> list(del_hi st t) = butlast(list t)"
 apply(induction t arbitrary: st)
 by(auto simp: list_Nil_iff size_list butlast_splice)
 
 lemma braun_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> braun(del_hi st t)"
 apply(induction t arbitrary: st)
 by(auto simp: list_del_hi simp flip: size_list)
 
 
 subsubsection "Flexible Array Implementation"
 
 interpretation AF: Array_Flex
 where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
 and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
 and len = "\<lambda>(t,l). l"
 and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
 and invar = "\<lambda>(t,l). braun t \<and> l = size t"
 and list = "\<lambda>(t,l). list t"
 and add_lo = "\<lambda>x (t,l). (add_lo x t, l+1)"
 and del_lo = "\<lambda>(t,l). (del_lo t, l-1)"
 and add_hi = "\<lambda>x (t,l). (update1 (Suc l) x t, l+1)"
 and del_hi = "\<lambda>(t,l). (del_hi l t, l-1)"
 proof (standard, goal_cases)
   case 1 thus ?case by (simp add: list_add_lo split: prod.splits)
 next
   case 2 thus ?case by (simp add: list_del_lo split: prod.splits)
 next
   case 3 thus ?case by (simp add: list_add_hi braun_add_hi split: prod.splits)
 next
   case 4 thus ?case by (simp add: list_del_hi split: prod.splits)
 next
   case 5 thus ?case by (simp add: braun_add_lo list_add_lo flip: size_list split: prod.splits)
 next
   case 6 thus ?case by (simp add: braun_del_lo list_del_lo flip: size_list split: prod.splits)
 next
   case 7 thus ?case by (simp add: size_add_hi braun_add_hi split: prod.splits)
 next
   case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits)
 qed
 
 
 subsection "Faster"
 
 
 subsubsection \<open>Size\<close>
 
 fun diff :: "'a tree \<Rightarrow> nat \<Rightarrow> nat" where
 "diff Leaf _ = 0" |
 "diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))"
 
 fun size_fast :: "'a tree \<Rightarrow> nat" where
 "size_fast Leaf = 0" |
 "size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
 
 declare Let_def[simp]
 
 lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n"
 by(induction t arbitrary: n) auto
 
 lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"
 by(induction t) (auto simp add: diff)
 
 
 subsubsection \<open>Initialization with 1 element\<close>
 
 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
 "braun_of_naive x n = (if n=0 then Leaf
   else let m = (n-1) div 2
        in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
        else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
 
 fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where
 "braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
   else let (s,t) = braun2_of x ((n-1) div 2)
        in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))"
 
 definition braun_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
 "braun_of x n = fst (braun2_of x n)"
 
 declare braun2_of.simps [simp del]
 
 lemma braun2_of_size_braun: "braun2_of x n = (s,t) \<Longrightarrow> size s = n \<and> size t = n+1 \<and> braun s \<and> braun t"
 proof(induction x n arbitrary: s t rule: braun2_of.induct)
   case (1 x n)
   then show ?case
     by (auto simp: braun2_of.simps[of x n] split: prod.splits if_splits) presburger+
 qed
 
 lemma braun2_of_replicate:
   "braun2_of x n = (s,t) \<Longrightarrow> list s = replicate n x \<and> list t = replicate (n+1) x"
 proof(induction x n arbitrary: s t rule: braun2_of.induct)
   case (1 x n)
   have "x # replicate m x = replicate (m+1) x" for m by simp
   with 1 show ?case
     apply (auto simp: braun2_of.simps[of x n] replicate.simps(2)[of 0 x]
         simp del: replicate.simps(2) split: prod.splits if_splits)
     by presburger+
 qed
 
 corollary braun_braun_of: "braun(braun_of x n)"
 unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)
 
 corollary list_braun_of: "list(braun_of x n) = replicate n x"
 unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)
 
 
 subsubsection "Proof Infrastructure"
 
 text \<open>Originally due to Thomas Sewell.\<close>
 
 paragraph \<open>\<open>take_nths\<close>\<close>
 
 fun take_nths :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "take_nths i k [] = []" |
 "take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
   else take_nths (i - 1) k xs)"
 
 text \<open>This is the more concise definition but seems to complicate the proofs:\<close>
 
 lemma take_nths_eq_nths: "take_nths i k xs = nths xs (\<Union>n. {n*2^k + i})"
 proof(induction xs arbitrary: i)
   case Nil
   then show ?case by simp
 next
   case (Cons x xs)
   show ?case
   proof cases
     assume [simp]: "i = 0"
     have "(\<Union>n. {(n+1) * 2 ^ k - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k}"
       apply (auto simp del: mult_Suc)
       by (metis diff_Suc_Suc diff_zero mult_eq_0_iff not0_implies_Suc)
     thus ?thesis by (simp add: Cons.IH ac_simps nths_Cons)
   next
     assume [arith]: "i \<noteq> 0"
     have "(\<Union>n. {n * 2 ^ k + i - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k + i}"
       apply auto
       by (metis diff_Suc_Suc diff_zero)
     thus ?thesis by (simp add: Cons.IH nths_Cons)
   qed
 qed
 
 lemma take_nths_drop:
   "take_nths i k (drop j xs) = take_nths (i + j) k xs"
 by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)
 
 lemma take_nths_00:
   "take_nths 0 0 xs = xs"
 by (induct xs; simp)
 
 lemma splice_take_nths:
   "splice (take_nths 0 (Suc 0) xs) (take_nths (Suc 0) (Suc 0) xs) = xs"
 by (induct xs; simp)
 
 lemma take_nths_take_nths:
   "take_nths i m (take_nths j n xs) = take_nths ((i * 2^n) + j) (m + n) xs"
 by (induct xs arbitrary: i j; simp add: algebra_simps power_add)
 
 lemma take_nths_empty:
   "(take_nths i k xs = []) = (length xs \<le> i)"
 by (induction xs arbitrary: i k) auto
 
 lemma hd_take_nths:
   "i < length xs \<Longrightarrow> hd(take_nths i k xs) = xs ! i"
 by (induction xs arbitrary: i k) auto
 
 lemma take_nths_01_splice:
   "\<lbrakk> length xs = length ys \<or> length xs = length ys + 1 \<rbrakk> \<Longrightarrow>
    take_nths 0 (Suc 0) (splice xs ys) = xs \<and>
    take_nths (Suc 0) (Suc 0) (splice xs ys) = ys"
 by (induct xs arbitrary: ys; case_tac ys; simp)
 
 lemma length_take_nths_00:
   "length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) \<or>
    length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) + 1"
 by (induct xs) auto
 
 
 paragraph \<open>\<open>braun_list\<close>\<close>
 
 fun braun_list :: "'a tree \<Rightarrow> 'a list \<Rightarrow> bool" where
 "braun_list Leaf xs = (xs = [])" |
 "braun_list (Node l x r) xs = (xs \<noteq> [] \<and> x = hd xs \<and>
     braun_list l (take_nths 1 1 xs) \<and>
     braun_list r (take_nths 2 1 xs))"
 
 lemma braun_list_eq:
   "braun_list t xs = (braun t \<and> xs = list t)"
 proof (induct t arbitrary: xs)
   case Leaf
   show ?case by simp
 next
   case Node
   show ?case
     using length_take_nths_00[of xs] splice_take_nths[of xs]
     by (auto simp: neq_Nil_conv Node.hyps size_list[symmetric] take_nths_01_splice)
 qed
 
 
 subsubsection \<open>Converting a list of elements into a Braun tree\<close>
 
 fun nodes :: "'a tree list \<Rightarrow> 'a list \<Rightarrow> 'a tree list \<Rightarrow> 'a tree list" where
 "nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" |
 "nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" |
 "nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" |
 "nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" |
 "nodes ls [] rs = []"
 
 fun brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree list" where
 "brauns k xs = (if xs = [] then [] else
    let ys = take (2^k) xs;
        zs = drop (2^k) xs;
        ts = brauns (k+1) zs
    in nodes ts ys (drop (2^k) ts))"
 
 declare brauns.simps[simp del]
 
 definition brauns1 :: "'a list \<Rightarrow> 'a tree" where
 "brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"
 
-fun t_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
-"t_brauns k xs = (if xs = [] then 0 else
+fun T_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+"T_brauns k xs = (if xs = [] then 0 else
    let ys = take (2^k) xs;
        zs = drop (2^k) xs;
        ts = brauns (k+1) zs
-   in 4 * min (2^k) (length xs) + t_brauns (k+1) zs)"
+   in 4 * min (2^k) (length xs) + T_brauns (k+1) zs)"
 
 
 paragraph "Functional correctness"
 
 text \<open>The proof is originally due to Thomas Sewell.\<close>
 
 lemma length_nodes:
   "length (nodes ls xs rs) = length xs"
 by (induct ls xs rs rule: nodes.induct; simp)
 
 lemma nth_nodes:
   "i < length xs \<Longrightarrow> nodes ls xs rs ! i =
   Node (if i < length ls then ls ! i else Leaf) (xs ! i)
     (if i < length rs then rs ! i else Leaf)"
 by (induct ls xs rs arbitrary: i rule: nodes.induct;
     simp add: nth_Cons split: nat.split)
 
 theorem length_brauns:
   "length (brauns k xs) = min (length xs) (2 ^ k)"
 proof (induct xs arbitrary: k rule: measure_induct_rule[where f=length])
   case (less xs) thus ?case by (simp add: brauns.simps[of k xs] length_nodes)
 qed
 
 theorem brauns_correct:
   "i < min (length xs) (2 ^ k) \<Longrightarrow> braun_list (brauns k xs ! i) (take_nths i k xs)"
 proof (induct xs arbitrary: i k rule: measure_induct_rule[where f=length])
   case (less xs)
   have "xs \<noteq> []" using less.prems by auto
   let ?zs = "drop (2^k) xs"
   let ?ts = "brauns (Suc k) ?zs"
   from less.hyps[of ?zs _ "Suc k"]
   have IH: "\<lbrakk> j = i + 2 ^ k;  i < min (length ?zs) (2 ^ (k+1)) \<rbrakk> \<Longrightarrow>
     braun_list (?ts ! i) (take_nths j (Suc k) xs)" for i j
     using \<open>xs \<noteq> []\<close> by (simp add: take_nths_drop)
   show ?case
     using less.prems
     by (auto simp: brauns.simps[of k xs] nth_nodes take_nths_take_nths
                    IH take_nths_empty hd_take_nths length_brauns)
 qed
 
 corollary brauns1_correct:
   "braun (brauns1 xs) \<and> list (brauns1 xs) = xs"
 using brauns_correct[of 0 xs 0]
 by (simp add: brauns1_def braun_list_eq take_nths_00)
 
 
 paragraph "Running Time Analysis"
 
-theorem t_brauns:
-  "t_brauns k xs = 4 * length xs"
+theorem T_brauns:
+  "T_brauns k xs = 4 * length xs"
 proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length])
   case (less xs)
   show ?case
   proof cases
     assume "xs = []"
     thus ?thesis by(simp)
   next
     assume "xs \<noteq> []"
     let ?zs = "drop (2^k) xs"
-    have "t_brauns k xs = t_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
+    have "T_brauns k xs = T_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
      using \<open>xs \<noteq> []\<close> by(simp)
     also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)"
       using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
       by (simp)
     also have "\<dots> = 4 * length xs"
       by(simp)
     finally show ?case .
   qed
 qed
 
 
 subsubsection \<open>Converting a Braun Tree into a List of Elements\<close>
 
 text \<open>The code and the proof are originally due to Thomas Sewell (except running time).\<close>
 
 function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
 "list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts in
   if us = [] then [] else
   map value us @ list_fast_rec (map left us @ map right us))"
 by (pat_completeness, auto)
 
 lemma list_fast_rec_term1: "ts \<noteq> [] \<Longrightarrow> Leaf \<notin> set ts \<Longrightarrow>
   sum_list (map (size o left) ts) + sum_list (map (size o right) ts) < sum_list (map size ts)"
   apply (clarsimp simp: sum_list_addf[symmetric] sum_list_map_filter')
   apply (rule sum_list_strict_mono; clarsimp?)
   apply (case_tac x; simp)
   done
 
 lemma list_fast_rec_term: "us \<noteq> [] \<Longrightarrow> us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<Longrightarrow>
   sum_list (map (size o left) us) + sum_list (map (size o right) us) < sum_list (map size ts)"
   apply (rule order_less_le_trans, rule list_fast_rec_term1, simp_all)
   apply (rule sum_list_filter_le_nat)
   done
 
 termination
   apply (relation "measure (sum_list o map size)")
    apply simp
   apply (simp add: list_fast_rec_term)
   done
 
 declare list_fast_rec.simps[simp del]
 
 definition list_fast :: "'a tree \<Rightarrow> 'a list" where
 "list_fast t = list_fast_rec [t]"
 
-function t_list_fast_rec :: "'a tree list \<Rightarrow> nat" where
-"t_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts
+function T_list_fast_rec :: "'a tree list \<Rightarrow> nat" where
+"T_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts
   in length ts + (if us = [] then 0 else
-  5 * length us + t_list_fast_rec (map left us @ map right us)))"
+  5 * length us + T_list_fast_rec (map left us @ map right us)))"
 by (pat_completeness, auto)
 
 termination
   apply (relation "measure (sum_list o map size)")
    apply simp
   apply (simp add: list_fast_rec_term)
   done
 
-declare t_list_fast_rec.simps[simp del]
+declare T_list_fast_rec.simps[simp del]
 
 paragraph "Functional Correctness"
 
 lemma list_fast_rec_all_Leaf:
   "\<forall>t \<in> set ts. t = Leaf \<Longrightarrow> list_fast_rec ts = []"
 by (simp add: filter_empty_conv list_fast_rec.simps)
 
 lemma take_nths_eq_single:
   "length xs - i < 2^n \<Longrightarrow> take_nths i n xs = take 1 (drop i xs)"
 by (induction xs arbitrary: i n; simp add: drop_Cons')
 
 lemma braun_list_Nil:
   "braun_list t [] = (t = Leaf)"
 by (cases t; simp)
 
 lemma braun_list_not_Nil: "xs \<noteq> [] \<Longrightarrow>
   braun_list t xs =
  (\<exists>l x r. t = Node l x r \<and> x = hd xs \<and>
     braun_list l (take_nths 1 1 xs) \<and>
     braun_list r (take_nths 2 1 xs))"
 by(cases t; simp)
 
 theorem list_fast_rec_correct:
   "\<lbrakk> length ts = 2 ^ k; \<forall>i < 2 ^ k. braun_list (ts ! i) (take_nths i k xs) \<rbrakk>
     \<Longrightarrow> list_fast_rec ts = xs"
 proof (induct xs arbitrary: k ts rule: measure_induct_rule[where f=length])
   case (less xs)
   show ?case
   proof (cases "length xs < 2 ^ k")
     case True
     from less.prems True have filter:
       "\<exists>n. ts = map (\<lambda>x. Node Leaf x Leaf) xs @ replicate n Leaf"
       apply (rule_tac x="length ts - length xs" in exI)
       apply (clarsimp simp: list_eq_iff_nth_eq)
       apply(auto simp: nth_append braun_list_not_Nil take_nths_eq_single braun_list_Nil hd_drop_conv_nth)
       done
     thus ?thesis
       by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf)
   next
     case False
     with less.prems(2) have *:
       "\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf
          \<and> value (ts ! i) = xs ! i
          \<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
          \<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
                  \<longrightarrow> braun_list (right (ts ! i)) ys)"
       by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
                      algebra_simps)
     have 1: "map value ts = take (2 ^ k) xs"
       using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
     have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
       using less.prems(1) False
       by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"]
                simp: nth_append * take_nths_drop algebra_simps)
     from less.prems(1) False show ?thesis
       by (auto simp: list_fast_rec.simps[of ts] 1 2 * all_set_conv_all_nth)
   qed
 qed
 
 corollary list_fast_correct:
   "braun t \<Longrightarrow> list_fast t = list t"
 by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])
 
 paragraph "Running Time Analysis"
 
 lemma sum_tree_list_children: "\<forall>t \<in> set ts. t \<noteq> Leaf \<Longrightarrow>
   (\<Sum>t\<leftarrow>ts. k * size t) = (\<Sum>t \<leftarrow> map left ts @ map right ts. k * size t) + k * length ts"
 by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)
 
-theorem t_list_fast_rec_ub:
-  "t_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)"
+theorem T_list_fast_rec_ub:
+  "T_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)"
 proof (induction ts rule: measure_induct_rule[where f="sum_list o map size"])
   case (less ts)
   let ?us = "filter (\<lambda>t. t \<noteq> Leaf) ts"
   show ?case
   proof cases
     assume "?us = []"
-    thus ?thesis using t_list_fast_rec.simps[of ts]
+    thus ?thesis using T_list_fast_rec.simps[of ts]
       by(simp add: sum_list_Suc)
     next
     assume "?us \<noteq> []"
     let ?children = "map left ?us @ map right ?us"
-    have "t_list_fast_rec ts = t_list_fast_rec ?children + 5 * length ?us + length ts"
-     using \<open>?us \<noteq> []\<close> t_list_fast_rec.simps[of ts] by(simp)
+    have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts"
+     using \<open>?us \<noteq> []\<close> T_list_fast_rec.simps[of ts] by(simp)
     also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts"
       using less[of "?children"] list_fast_rec_term[of "?us"] \<open>?us \<noteq> []\<close>
       by (simp)
     also have "\<dots> = (\<Sum>t\<leftarrow>?children. 7*size t) + 7 * length ?us + length ts"
       by(simp add: sum_list_Suc o_def)
     also have "\<dots> = (\<Sum>t\<leftarrow>?us. 7*size t) + length ts"
       by(simp add: sum_tree_list_children)
     also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 7*size t) + length ts"
       by(simp add: sum_list_filter_le_nat)
     also have "\<dots> = (\<Sum>t\<leftarrow>ts. 7 * size t + 1)"
       by(simp add: sum_list_Suc)
     finally show ?case .
   qed
 qed
 
-end
\ No newline at end of file
+end
diff --git a/src/HOL/Data_Structures/Binomial_Heap.thy b/src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy
@@ -1,728 +1,728 @@
 (* Author: Peter Lammich
            Tobias Nipkow (tuning)
 *)
 
 section \<open>Binomial Heap\<close>
 
 theory Binomial_Heap
 imports
   "HOL-Library.Pattern_Aliases"
   Complex_Main
   Priority_Queue_Specs
 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 ts) = {#a#} + (\<Sum>t\<in>#mset ts. mset_tree t)"
 
 definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where
   "mset_heap ts = (\<Sum>t\<in>#mset ts. mset_tree t)"
 
 lemma mset_tree_simp_alt[simp]:
   "mset_tree (Node r a ts) = {#a#} + mset_heap ts"
   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 [] = {#}"
 by (auto simp: mset_heap_def)
 
 lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts"
 by (auto simp: mset_heap_def)
 
 lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]"
 by (auto simp: mset_heap_def)
 
 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"
 by (auto simp: mset_heap_def)
 
 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 (<) (map rank ts))"
 
 text \<open>Ordering (heap) invariant\<close>
 fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
 "invar_otree (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)"
 
 definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where
 "invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)"
 
 definition invar :: "'a::linorder heap \<Rightarrow> bool" where
 "invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts"
 
 text \<open>The children of a node are a valid heap\<close>
 lemma invar_oheap_children:
   "invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)"
 by (auto simp: invar_oheap_def)
 
 lemma invar_bheap_children:
   "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"
 by (auto simp: invar_bheap_def rev_map[symmetric])
 
 
 subsection \<open>Operations and Their Functional Correctness\<close>
 
 subsubsection \<open>\<open>link\<close>\<close>
 
 context
 includes pattern_aliases
 begin
 
 fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   "link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) =
     (if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#ts\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#ts\<^sub>2))"
 
 end
 
 lemma invar_btree_link:
   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
 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
 
 lemma invar_link_otree:
   assumes "invar_otree t\<^sub>1"
   assumes "invar_otree t\<^sub>2"
   shows "invar_otree (link t\<^sub>1 t\<^sub>2)"
 using assms
 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto
 
 lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
 
 lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
 
 subsubsection \<open>\<open>ins_tree\<close>\<close>
 
 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')"
 by (auto simp: invar_bheap_def)
 
 lemma invar_btree_ins_tree:
   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
 by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric])
 
 lemma invar_oheap_Cons[simp]:
   "invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts"
 by (auto simp: invar_oheap_def)
 
 lemma invar_oheap_ins_tree:
   assumes "invar_otree t"
   assumes "invar_oheap ts"
   shows "invar_oheap (ins_tree t ts)"
 using assms
 by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree)
 
 lemma mset_heap_ins_tree[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)
 
 subsubsection \<open>\<open>insert\<close>\<close>
 
 hide_const (open) insert
 
 definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
 "insert x ts = ins_tree (Node 0 x []) ts"
 
 lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
 by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def)
 
 lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
 by(auto simp: insert_def)
 
 subsubsection \<open>\<open>merge\<close>\<close>
 
 context
 includes pattern_aliases
 begin
 
 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 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = (
     if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 h\<^sub>2 else
     if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge h\<^sub>1 ts\<^sub>2
     else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
   )"
 
 end
 
 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\<^sub>1\<in>set ts\<^sub>1. rank t < rank t\<^sub>1"
   assumes "\<forall>t\<^sub>2\<in>set ts\<^sub>2. rank t < rank t\<^sub>2"
   shows "rank t < rank t'"
 using assms
 by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
    (auto split: if_splits simp: ins_tree_rank_bound)
 
 lemma invar_bheap_merge:
   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 invar_btree_ins_tree invar_btree_link)
   qed
 qed simp_all
 
 lemma invar_oheap_merge:
   assumes "invar_oheap ts\<^sub>1"
   assumes "invar_oheap ts\<^sub>2"
   shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)"
 using assms
 by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
    (auto simp: invar_oheap_ins_tree invar_link_otree)
 
 lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
 by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)
 
 lemma mset_heap_merge[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
 
 subsubsection \<open>\<open>get_min\<close>\<close>
 
 fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where
   "get_min [t] = root t"
 | "get_min (t#ts) = min (root t) (get_min ts)"
 
 lemma invar_otree_root_min:
   assumes "invar_otree t"
   assumes "x \<in># mset_tree t"
   shows "root t \<le> x"
 using assms
 by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def)
 
 lemma get_min_mset_aux:
   assumes "ts\<noteq>[]"
   assumes "invar_oheap ts"
   assumes "x \<in># mset_heap ts"
   shows "get_min ts \<le> x"
   using assms
 apply (induction ts arbitrary: x rule: get_min.induct)
 apply (auto
       simp: invar_otree_root_min min_def intro: order_trans;
       meson linear order_trans invar_otree_root_min
       )+
 done
 
 lemma get_min_mset:
   assumes "ts\<noteq>[]"
   assumes "invar ts"
   assumes "x \<in># mset_heap ts"
   shows "get_min ts \<le> x"
 using assms by (auto simp: invar_def get_min_mset_aux)
 
 lemma get_min_member:
   "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"
 by (induction ts rule: get_min.induct) (auto simp: min_def)
 
 lemma get_min:
   assumes "mset_heap ts \<noteq> {#}"
   assumes "invar ts"
   shows "get_min ts = Min_mset (mset_heap ts)"
 using assms get_min_member get_min_mset
 by (auto simp: eq_Min_iff)
 
 subsubsection \<open>\<open>get_min_rest\<close>\<close>
 
 fun get_min_rest :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
   "get_min_rest [t] = (t,[])"
 | "get_min_rest (t#ts) = (let (t',ts') = get_min_rest ts
                      in if root t \<le> root t' then (t,ts) else (t',t#ts'))"
 
 lemma get_min_rest_get_min_same_root:
   assumes "ts\<noteq>[]"
   assumes "get_min_rest ts = (t',ts')"
   shows "root t' = get_min ts"
 using assms
 by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits)
 
 lemma mset_get_min_rest:
   assumes "get_min_rest ts = (t',ts')"
   assumes "ts\<noteq>[]"
   shows "mset ts = {#t'#} + mset ts'"
 using assms
 by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
 
-lemma set_get_min_rest:
+lemma seT_get_min_rest:
   assumes "get_min_rest ts = (t', ts')"
   assumes "ts\<noteq>[]"
   shows "set ts = Set.insert t' (set ts')"
 using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
 by auto
 
 lemma invar_bheap_get_min_rest:
   assumes "get_min_rest 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: get_min.induct)
       case (2 t v va)
       then show ?case
         apply (clarsimp split: prod.splits if_splits)
-        apply (drule set_get_min_rest; fastforce)
+        apply (drule seT_get_min_rest; fastforce)
         done
     qed auto
   thus "invar_btree t'" and "invar_bheap ts'" by auto
 qed
 
 lemma invar_oheap_get_min_rest:
   assumes "get_min_rest ts = (t',ts')"
   assumes "ts\<noteq>[]"
   assumes "invar_oheap ts"
   shows "invar_otree t'" and "invar_oheap ts'"
 using assms
 by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
 
 subsubsection \<open>\<open>del_min\<close>\<close>
 
 definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
 "del_min ts = (case get_min_rest ts of
    (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
 
 lemma invar_del_min[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!: invar_bheap_merge invar_oheap_merge
       dest: invar_bheap_get_min_rest invar_oheap_get_min_rest
       intro!: invar_oheap_children invar_bheap_children
     )
 
 lemma mset_heap_del_min:
   assumes "ts \<noteq> []"
   shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
 using assms
 unfolding del_min_def
 apply (clarsimp split: tree.split prod.split)
 apply (frule (1) get_min_rest_get_min_same_root)
 apply (frule (1) mset_get_min_rest)
 apply (auto simp: mset_heap_def)
 done
 
 
 subsubsection \<open>Instantiating the Priority Queue Locale\<close>
 
 text \<open>Last step of functional correctness proof: combine all the above lemmas
 to show that binomial heaps satisfy the specification of priority queues with merge.\<close>
 
 interpretation binheap: Priority_Queue_Merge
   where empty = "[]" and is_empty = "(=) []" and insert = insert
   and get_min = get_min and del_min = del_min and merge = merge
   and invar = invar and mset = mset_heap
 proof (unfold_locales, goal_cases)
   case 1 thus ?case by simp
 next
   case 2 thus ?case by auto
 next
   case 3 thus ?case by auto
 next
   case (4 q)
   thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>]
     by (auto simp: union_single_eq_diff)
 next
   case (5 q) thus ?case using get_min[of q] by auto
 next
   case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
 next
   case 7 thus ?case by simp
 next
   case 8 thus ?case by simp
 next
   case 9 thus ?case by simp
 next
   case 10 thus ?case by simp
 qed
 
 
 subsection \<open>Complexity\<close>
 
 text \<open>The size of a binomial tree is determined by its rank\<close>
 lemma size_mset_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: map_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_mset_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 (<) (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 "(^) (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: map_cong simp: size_mset_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"
+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) = (
+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)
+     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
   )"
 
-definition t_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
-"t_insert x ts = t_ins_tree (Node 0 x []) ts"
+definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
+"T_insert x ts = T_ins_tree (Node 0 x []) ts"
 
-lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1"
-by (induction t ts rule: t_ins_tree.induct) auto
+lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
+by (induction t ts rule: T_ins_tree.induct) auto
 
-subsubsection \<open>\<open>t_insert\<close>\<close>
+subsubsection \<open>\<open>T_insert\<close>\<close>
 
-lemma t_insert_bound:
+lemma T_insert_bound:
   assumes "invar ts"
-  shows "t_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
+  shows "T_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
 proof -
 
-  have 1: "t_insert x ts \<le> length ts + 1"
-    unfolding t_insert_def by (rule t_ins_tree_simple_bound)
+  have 1: "T_insert x ts \<le> length ts + 1"
+    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_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
 
-subsubsection \<open>\<open>t_merge\<close>\<close>
+subsubsection \<open>\<open>T_merge\<close>\<close>
 
 context
 includes pattern_aliases
 begin
 
-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 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = 1 + (
-    if rank t\<^sub>1 < rank t\<^sub>2 then t_merge ts\<^sub>1 h\<^sub>2
-    else if rank t\<^sub>2 < rank t\<^sub>1 then t_merge h\<^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
+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 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = 1 + (
+    if rank t\<^sub>1 < rank t\<^sub>2 then T_merge ts\<^sub>1 h\<^sub>2
+    else if rank t\<^sub>2 < rank t\<^sub>1 then T_merge h\<^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
   )"
 
 end
 
 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 t_ins_tree_length:
-  "t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
+lemma T_ins_tree_length:
+  "T_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
 by (induction t ts rule: ins_tree.induct) auto
 
-lemma t_merge_length:
-  "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"
-by (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct)
-   (auto simp: t_ins_tree_length algebra_simps)
+lemma T_merge_length:
+  "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"
+by (induction ts\<^sub>1 ts\<^sub>2 rule: T_merge.induct)
+   (auto simp: T_ins_tree_length algebra_simps)
 
 text \<open>Finally, we get the desired logarithmic bound\<close>
-lemma t_merge_bound_aux:
+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"
+  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 t_merge_length[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)"
+  from T_merge_length[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_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"
+  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>"
+  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)"
+  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)"
+  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
+  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:
+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
-
-subsubsection \<open>\<open>t_get_min\<close>\<close>
+  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_get_min :: "'a::linorder heap \<Rightarrow> nat" where
-  "t_get_min [t] = 1"
-| "t_get_min (t#ts) = 1 + t_get_min ts"
+subsubsection \<open>\<open>T_get_min\<close>\<close>
 
-lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts"
-by (induction ts rule: t_get_min.induct) auto
+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_bound:
+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:
   assumes "invar ts"
   assumes "ts\<noteq>[]"
-  shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
+  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
+  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_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
 
-subsubsection \<open>\<open>t_del_min\<close>\<close>
+subsubsection \<open>\<open>T_del_min\<close>\<close>
 
-fun t_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
-  "t_get_min_rest [t] = 1"
-| "t_get_min_rest (t#ts) = 1 + t_get_min_rest ts"
+fun T_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
+  "T_get_min_rest [t] = 1"
+| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"
 
-lemma t_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min_rest ts = length ts"
-  by (induction ts rule: t_get_min_rest.induct) auto
+lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts"
+  by (induction ts rule: T_get_min_rest.induct) auto
 
-lemma t_get_min_rest_bound_aux:
+lemma T_get_min_rest_bound_aux:
   assumes "invar_bheap ts"
   assumes "ts\<noteq>[]"
-  shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
+  shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
 proof -
-  have 1: "t_get_min_rest ts = length ts" using assms t_get_min_rest_estimate by auto
+  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_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_rest_bound:
+lemma T_get_min_rest_bound:
   assumes "invar ts"
   assumes "ts\<noteq>[]"
-  shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
-using assms t_get_min_rest_bound_aux unfolding invar_def by blast
+  shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
+using assms T_get_min_rest_bound_aux unfolding invar_def by blast
 
 text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity,
 it can and is implemented (via suitable code lemmas) as a linear time function.
 Thus the following definition is justified:\<close>
 
-definition "t_rev xs = length xs + 1"
+definition "T_rev xs = length xs + 1"
 
-definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" where
-  "t_del_min ts = t_get_min_rest ts + (case get_min_rest 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
+definition T_del_min :: "'a::linorder heap \<Rightarrow> nat" where
+  "T_del_min ts = T_get_min_rest ts + (case get_min_rest 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:
+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)"
+  shows "T_rev ts \<le> 1 + log 2 (n+1)"
 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
+  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_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))"
+  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:
+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"
+  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_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
     by (metis surj_pair tree.exhaust_sel)
 
   note BINVAR' = invar_bheap_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
   hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: invar_bheap_children)
 
   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)"
+  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]
+    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 mset_get_min_rest[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_rest 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_rest_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
+  have "T_del_min ts = T_get_min_rest 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_rest_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>]
+    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 mset_get_min_rest[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"
+  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:
+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
+  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
+using assms T_del_min_bound_aux unfolding invar_def by blast
 
-end
\ No newline at end of file
+end