# HG changeset patch
# User blanchet
# Date 1604663311 -3600
# Node ID 1d0ae7e578a0c6859881943509b77d163f91e5c2
# Parent  726d17b280ea0e37ac43f9e7af063d7cc5cda3ab
renamed t_ functions to T_ (im Auftrag von T. Nipkow)

diff -r 726d17b280ea -r 1d0ae7e578a0 src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Thu Nov 05 19:09:11 2020 +0000
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Fri Nov 06 12:48:31 2020 +0100
@@ -444,12 +444,12 @@
 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"
@@ -498,8 +498,8 @@
 
 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
@@ -509,7 +509,7 @@
   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>
@@ -555,10 +555,10 @@
 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
@@ -567,7 +567,7 @@
   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"
 
@@ -637,21 +637,21 @@
   (\<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)
@@ -667,4 +667,4 @@
   qed
 qed
 
-end
\ No newline at end of file
+end
diff -r 726d17b280ea -r 1d0ae7e578a0 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Nov 05 19:09:11 2020 +0000
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Fri Nov 06 12:48:31 2020 +0100
@@ -326,7 +326,7 @@
 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')"
@@ -345,7 +345,7 @@
       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
@@ -482,31 +482,31 @@
   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
@@ -519,19 +519,19 @@
     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
@@ -539,73 +539,73 @@
 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
+  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>
+subsubsection \<open>\<open>T_get_min\<close>\<close>
 
-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"
+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_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts"
+by (induction ts rule: T_get_min.induct) auto
 
-lemma t_get_min_bound:
+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"
@@ -615,21 +615,21 @@
   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"
@@ -639,46 +639,46 @@
   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)
@@ -689,9 +689,9 @@
   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>]
@@ -699,30 +699,30 @@
     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