diff --git a/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis.thy b/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis.thy
--- a/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis.thy
+++ b/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis.thy
@@ -1,332 +1,332 @@
 (* Author: Tobias Nipkow (based on Hauke Brinkop's tree proofs) *)
 
 subsection \<open>Okasaki's Pairing Heap\<close>
 
 theory Pairing_Heap_List1_Analysis
 imports
   Pairing_Heap.Pairing_Heap_List1
   Amortized_Framework
   Priority_Queue_ops_merge
   Lemmas_log
 begin
 
 text
 \<open>Amortized analysis of pairing heaps as defined by Okasaki \cite{Okasaki}.\<close>
 
 fun hps where
 "hps (Hp _ hs) = hs"
 
 lemma merge_Empty[simp]: "merge heap.Empty h = h"
 by(cases h) auto
 
 lemma merge2: "merge (Hp x lx) h = (case h of heap.Empty \<Rightarrow> Hp x lx | (Hp y ly) \<Rightarrow> 
     (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly)))"
 by(auto split: heap.split)
 
 lemma pass1_Nil_iff: "pass\<^sub>1 hs = [] \<longleftrightarrow> hs = []"
 by(cases hs rule: pass\<^sub>1.cases) auto
 
 
 subsubsection \<open>Invariant\<close>
 
 fun no_Empty :: "'a :: linorder heap \<Rightarrow> bool" where
 "no_Empty heap.Empty = False" |
 "no_Empty (Hp x hs) = (\<forall>h \<in> set hs. no_Empty h)"
 
 abbreviation no_Emptys :: "'a :: linorder heap list \<Rightarrow> bool" where
 "no_Emptys hs \<equiv> \<forall>h \<in> set hs. no_Empty h"
 
 fun is_root :: "'a :: linorder heap \<Rightarrow> bool" where
 "is_root heap.Empty = True" |
 "is_root (Hp x hs) = no_Emptys hs"
 
 
 lemma is_root_if_no_Empty: "no_Empty h \<Longrightarrow> is_root h"
 by(cases h) auto
 
 lemma no_Emptys_hps: "no_Empty h \<Longrightarrow> no_Emptys(hps h)"
 by(induction h) auto
 
 lemma no_Empty_merge: "\<lbrakk> no_Empty h1; no_Empty h2\<rbrakk> \<Longrightarrow> no_Empty (merge h1 h2)"
 by (cases "(h1,h2)" rule: merge.cases) auto
 
 lemma is_root_merge: "\<lbrakk> is_root h1; is_root h2\<rbrakk> \<Longrightarrow> is_root (merge h1 h2)"
 by (cases "(h1,h2)" rule: merge.cases) auto
 
 lemma no_Emptys_pass1:
   "no_Emptys hs \<Longrightarrow> no_Emptys (pass\<^sub>1 hs)"
 by(induction hs rule: pass\<^sub>1.induct)(auto simp: no_Empty_merge)
 
 lemma is_root_pass2: "no_Emptys hs \<Longrightarrow> is_root(pass\<^sub>2 hs)"
 proof(induction hs)
   case (Cons _ hs)
   show ?case
   proof cases
     assume "hs = []" thus ?thesis using Cons by (auto simp: is_root_if_no_Empty)
   next
     assume "hs \<noteq> []" thus ?thesis using Cons by(auto simp: is_root_merge is_root_if_no_Empty)
   qed
 qed simp
 
 
 subsubsection \<open>Complexity\<close>
 
 fun size_hp :: "'a heap \<Rightarrow> nat" where
 "size_hp heap.Empty = 0" |
 "size_hp (Hp x hs) = sum_list(map size_hp hs) + 1"
 
 abbreviation size_hps where
 "size_hps hs \<equiv> sum_list(map size_hp hs)"
 
 fun \<Phi>_hps :: "'a heap list \<Rightarrow> real" where
 "\<Phi>_hps [] = 0" |
 "\<Phi>_hps (heap.Empty # hs) = \<Phi>_hps hs" |
 "\<Phi>_hps (Hp x hsl # hsr) =
  \<Phi>_hps hsl + \<Phi>_hps hsr + log 2 (size_hps hsl + size_hps hsr + 1)"
 
 fun \<Phi> :: "'a heap \<Rightarrow> real" where
 "\<Phi> heap.Empty = 0" |
 "\<Phi> (Hp _ hs) = \<Phi>_hps hs + log 2 (size_hps(hs)+1)"
 
 lemma \<Phi>_hps_ge0: "\<Phi>_hps hs \<ge> 0"
 by (induction hs rule: \<Phi>_hps.induct) auto
 
 lemma no_Empty_ge0: "no_Empty h \<Longrightarrow> size_hp h > 0"
 by(cases h) auto
 
 declare algebra_simps[simp]
 
 lemma \<Phi>_hps1: "\<Phi>_hps [h] = \<Phi> h"
 by(cases h) auto
 
 lemma size_hp_merge: "size_hp(merge h1 h2) = size_hp h1 + size_hp h2" 
 by (induction h1 h2 rule: merge.induct) simp_all
 
 lemma pass\<^sub>1_size[simp]: "size_hps (pass\<^sub>1 hs) = size_hps hs" 
 by (induct hs rule: pass\<^sub>1.induct) (simp_all add: size_hp_merge)
 
 lemma \<Delta>\<Phi>_insert:
   "\<Phi> (Pairing_Heap_List1.insert x h) - \<Phi> h \<le> log 2 (size_hp h + 1)"
 by(cases h)(auto simp: size_hp_merge)
 
 lemma \<Delta>\<Phi>_merge:
   "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2
   \<le> log 2 (size_hp h1 + size_hp h2 + 1) + 1"
 proof(induction h1 h2 rule: merge.induct)
   case (3 x lx y ly)
   thus ?case
     using ld_le_2ld[of "size_hps lx" "size_hps ly"]
       log_le_cancel_iff[of 2 "size_hps lx + size_hps ly + 2" "size_hps lx + size_hps ly + 3"]
     by (auto simp del: log_le_cancel_iff)
 qed auto
 
 fun sum_ub :: "'a heap list \<Rightarrow> real" where
   "sum_ub [] = 0"
 | "sum_ub [_] = 0"
 | "sum_ub [h1, h2] = 2*log 2 (size_hp h1 + size_hp h2)" 
 | "sum_ub (h1 # h2 # hs) = 2*log 2 (size_hp h1 + size_hp h2 + size_hps hs) 
     - 2*log 2 (size_hps hs) - 2 + sum_ub hs"
 
 lemma \<Delta>\<Phi>_pass1_sum_ub: "no_Emptys hs \<Longrightarrow>
   \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs  \<le> sum_ub hs" (is "_ \<Longrightarrow> ?P hs")
 proof (induction hs rule: sum_ub.induct)
   case (3 h1 h2)
   then obtain x hsx y hsy where [simp]: "h1 = Hp x hsx" "h2 = Hp y hsy"
     by simp (meson no_Empty.elims(2))
   have 0: "\<And>x y::real. 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x \<le> 2*y" by linarith
   show ?case using 3 by (auto simp add: add_increasing 0)
 next
   case (4 h1 h2 h3 hs)
   hence IH: "?P(h3#hs)" by auto
   from "4.prems" obtain x hsx y hsy where [simp]: "h1 = Hp x hsx" "h2 = Hp y hsy"
     by simp (meson no_Empty.elims(2))
   from "4.prems" have s3: "size_hp h3 > 0"
     apply auto using size_hp.elims by force
   let ?ry = "h3 # hs"
   let ?rx = "Hp y hsy # ?ry"
   let ?h = "Hp x hsx # ?rx"
   have "\<Phi>_hps(pass\<^sub>1 ?h) - \<Phi>_hps ?h  
     \<le> log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry) + sum_ub ?ry"
     using IH by simp
   also have "log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry) 
     \<le> 2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2"
   proof -
     have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) - 2*log 2 (size_hps ?h) 
       = log 2 ((1 + size_hps hsx + size_hps hsy)/(size_hps ?h) ) + log 2 (size_hps ?ry / size_hps ?h)"
       using s3 by (simp add: log_divide)
     also have "\<dots> \<le> -2" 
     proof -
       have "2 + \<dots>
         \<le> 2*log 2 ((1 + size_hps hsx + size_hps hsy) / size_hps ?h +  size_hps ?ry / size_hps ?h)"  
         using ld_sum_inequality [of "(1 + size_hps hsx + size_hps hsy) / size_hps ?h" "(size_hps ?ry / size_hps ?h)"] using s3 by simp
       also have "\<dots> \<le> 0" by (simp add: field_simps log_divide add_pos_nonneg)
       finally show ?thesis by linarith
     qed 
     finally have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) + 2
       \<le>  2*log 2 (size_hps ?h)" by simp
     moreover have "log 2 (size_hps ?ry) \<le> log 2 (size_hps ?rx)" using s3 by simp
     ultimately have "log 2 (1 + size_hps hsx + size_hps hsy) - \<dots> 
       \<le>  2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2" by linarith
     thus ?thesis by simp
   qed
   finally show ?case by (simp)
 qed simp_all
 
 lemma \<Delta>\<Phi>_pass1: assumes "hs \<noteq> []" "no_Emptys hs"
   shows "\<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (size_hps hs) - length hs + 2"
 proof - 
   have "sum_ub hs \<le> 2 * log 2 (size_hps hs) - length hs + 2" 
     using assms by (induct hs rule: sum_ub.induct) (auto dest: no_Empty_ge0)
   thus ?thesis using \<Delta>\<Phi>_pass1_sum_ub[OF assms(2)] by linarith
 qed
 
 lemma size_hps_pass2: "hs \<noteq> [] \<Longrightarrow> no_Emptys hs \<Longrightarrow>
   no_Empty(pass\<^sub>2 hs) & size_hps hs = size_hps(hps(pass\<^sub>2 hs))+1"
 apply(induction hs rule: \<Phi>_hps.induct)
   apply (fastforce simp: merge2 split: heap.split)+
 done
 
 lemma \<Delta>\<Phi>_pass2: "hs \<noteq> [] \<Longrightarrow> no_Emptys hs \<Longrightarrow>
   \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (size_hps hs)"
 proof (induction hs)
   case (Cons h hs)
   thus ?case
   proof cases
     assume "hs = []"
     thus ?thesis using Cons by (auto simp add: \<Phi>_hps1 dest: no_Empty_ge0)
   next
     assume *: "hs \<noteq> []"
     obtain x hs2 where [simp]: "h = Hp x hs2"
       using Cons.prems(2)by simp (meson no_Empty.elims(2))
     show ?thesis
     proof (cases "pass\<^sub>2 hs")
       case Empty thus ?thesis using \<Phi>_hps_ge0[of hs]
         by(simp add: add_increasing xt1(3)[OF mult_2, OF add_increasing])
     next
       case (Hp y hs3)
       with Cons * size_hps_pass2[of hs] show ?thesis by(auto simp: add_mono)
     qed
   qed
 qed simp
 
 lemma \<Delta>\<Phi>_del_min: assumes "hps h \<noteq> []" "no_Empty h"
   shows "\<Phi> (del_min h) - \<Phi> h 
   \<le> 3 * log 2 (size_hps(hps h)) - length(hps h) + 2"
 proof -
   obtain x hs where [simp]: "h = Hp x hs" using assms(2) by (cases h) auto
   let ?\<Delta>\<Phi>\<^sub>1 = "\<Phi>_hps(hps h) - \<Phi> h" 
   let ?\<Delta>\<Phi>\<^sub>2 = "\<Phi>(pass\<^sub>2(pass\<^sub>1 (hps h))) - \<Phi>_hps (hps h)"
   let ?\<Delta>\<Phi> = "\<Phi> (del_min h) - \<Phi> h"
   have "\<Phi>(pass\<^sub>2(pass\<^sub>1(hps h))) - \<Phi>_hps (pass\<^sub>1(hps h)) \<le> log 2 (size_hps(hps h))" 
     using \<Delta>\<Phi>_pass2[of "pass\<^sub>1(hps h)"] using assms
     by (auto simp: pass1_Nil_iff no_Emptys_pass1 dest: no_Emptys_hps)
   moreover have "\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le>  2*\<dots> - length (hps h) + 2"
     using \<Delta>\<Phi>_pass1[OF assms(1) no_Emptys_hps[OF assms(2)]] by blast
   moreover have "?\<Delta>\<Phi>\<^sub>1 \<le> 0" by simp
   moreover have "?\<Delta>\<Phi> = ?\<Delta>\<Phi>\<^sub>1 + ?\<Delta>\<Phi>\<^sub>2" by simp
   ultimately show ?thesis by linarith
 qed
 
 
 fun exec :: "'a :: linorder op \<Rightarrow> 'a heap list \<Rightarrow> 'a heap" where
 "exec Empty [] = heap.Empty" | 
 "exec Del_min [h] = del_min h" |
 "exec (Insert x) [h] = Pairing_Heap_List1.insert x h" |
 "exec Merge [h1,h2] = merge h1 h2"
 
-fun t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 :: "'a heap list \<Rightarrow> nat" where
-  "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [] = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [_] = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (_ # _ # hs) = 1 + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs"
+fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 :: "'a heap list \<Rightarrow> nat" where
+  "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [] = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [_] = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (_ # _ # hs) = 1 + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs"
 
-fun t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 :: "'a heap list \<Rightarrow> nat" where
- "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 [] = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (_ # hs) = 1 + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 hs"
+fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 :: "'a heap list \<Rightarrow> nat" where
+ "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 [] = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (_ # hs) = 1 + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 hs"
 
 fun cost :: "'a :: linorder op \<Rightarrow> 'a heap list \<Rightarrow> nat" where
 "cost Empty _ = 1" |
 "cost Del_min [heap.Empty] = 1" |
-"cost Del_min [Hp x hs] = t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs" |
+"cost Del_min [Hp x hs] = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs" |
 "cost (Insert a) _ = 1" |
 "cost Merge _ = 1"
 
 fun U :: "'a :: linorder op \<Rightarrow> 'a heap list \<Rightarrow> real" where
 "U Empty _ = 1" |
 "U (Insert a) [h] = log 2 (size_hp h + 1) + 1" |
 "U Del_min [h] = 3*log 2 (size_hp h + 1) + 4" |
 "U Merge [h1,h2] = log 2 (size_hp h1 + size_hp h2 + 1) + 2"
 
 interpretation pairing: Amortized
 where arity = arity and exec = exec and cost = cost and inv = "is_root"
 and \<Phi> = \<Phi> and U = U
 proof (standard, goal_cases)
   case (1 ss f) show ?case
   proof (cases f)
     case Empty with 1 show ?thesis by simp
   next
     case Insert thus ?thesis using 1 by(auto simp: is_root_merge)
   next
     case Merge
     thus ?thesis using 1 by(auto simp: is_root_merge numeral_eq_Suc)
   next
     case [simp]: Del_min
     then obtain h where [simp]: "ss = [h]" using 1 by auto
     show ?thesis
     proof (cases h)
       case [simp]: (Hp _ hs)
       show ?thesis
       proof cases
         assume "hs = []" thus ?thesis by simp
       next
         assume "hs \<noteq> []" thus ?thesis
           using 1(1) no_Emptys_pass1 by (auto intro: is_root_pass2)
       qed
     qed simp
   qed
 next
   case (2 s) show ?case by (cases s) (auto simp: \<Phi>_hps_ge0)
 next
   case (3 ss f) show ?case
   proof (cases f)
     case Empty with 3 show ?thesis by(auto)
   next
     case Insert thus ?thesis using \<Delta>\<Phi>_insert 3 by auto
   next
     case [simp]: Del_min
     then obtain h where [simp]: "ss = [h]" using 3 by auto
     show ?thesis
     proof (cases h)
       case [simp]: (Hp x hs)
-      have "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs \<le> 2 + length hs"
+      have "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs \<le> 2 + length hs"
         by (induct hs rule: pass\<^sub>1.induct) simp_all
       hence  "cost f ss \<le> \<dots>" by simp
       moreover have  "\<Phi> (del_min h) - \<Phi> h \<le> 3*log 2 (size_hp h + 1) - length hs + 2"
       proof (cases "hs = []")
         case False
         hence "\<Phi> (del_min h) - \<Phi> h \<le> 3*log 2 (size_hps hs) - length hs + 2"
           using  \<Delta>\<Phi>_del_min[of h] 3(1) by simp
         also have "\<dots> \<le> 3*log 2 (size_hp h + 1) - length hs + 2"
           using False 3(1) size_hps_pass2 by fastforce
         finally show ?thesis .
       qed simp
       ultimately show ?thesis by simp
     qed simp
   next
     case [simp]: Merge
     then obtain h1 h2 where [simp]: "ss = [h1, h2]"
       using 3 by(auto simp: numeral_eq_Suc)
     show ?thesis
     proof (cases "h1 = heap.Empty \<or> h2 = heap.Empty")
       case True thus ?thesis by auto
     next                  
       case False
       then obtain x1 x2 hs1 hs2 where [simp]: "h1 = Hp x1 hs1" "h2 = Hp x2 hs2"
         by (meson hps.cases) 
       have "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (size_hp h1 + size_hp h2 + 1) + 1"
         using \<Delta>\<Phi>_merge[of h1 h2] by simp
       thus ?thesis by(simp)
     qed
   qed
 qed
 
 end
diff --git a/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis2.thy b/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis2.thy
--- a/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis2.thy
+++ b/thys/Amortized_Complexity/Pairing_Heap_List1_Analysis2.thy
@@ -1,130 +1,130 @@
 (* Author: Tobias Nipkow *)
 
 subsection \<open>Transfer of Tree Analysis to List Representation\<close>
 
 theory Pairing_Heap_List1_Analysis2
 imports
   Pairing_Heap_List1_Analysis
   Pairing_Heap_Tree_Analysis
 begin
 
 text\<open>This theory transfers the amortized analysis of the tree-based
 pairing heaps to Okasaki's pairing heaps.\<close>
 
 abbreviation "is_root' == Pairing_Heap_List1_Analysis.is_root"
 abbreviation "del_min' == Pairing_Heap_List1.del_min"
 abbreviation "insert' == Pairing_Heap_List1.insert"
 abbreviation "merge' == Pairing_Heap_List1.merge"
 abbreviation "pass\<^sub>1' == Pairing_Heap_List1.pass\<^sub>1"
 abbreviation "pass\<^sub>2' == Pairing_Heap_List1.pass\<^sub>2"
-abbreviation "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' == Pairing_Heap_List1_Analysis.t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1"
-abbreviation "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2' == Pairing_Heap_List1_Analysis.t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2"
+abbreviation "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' == Pairing_Heap_List1_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1"
+abbreviation "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2' == Pairing_Heap_List1_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2"
 
 fun homs :: "'a heap list \<Rightarrow> 'a tree" where
 "homs [] = Leaf" |
 "homs (Hp x lhs # rhs) = Node (homs lhs) x (homs rhs)"
 
 fun hom :: "'a heap \<Rightarrow> 'a tree" where
 "hom heap.Empty = Leaf" |
 "hom (Hp x hs) = (Node (homs hs) x Leaf)"
 
 lemma homs_pass1': "no_Emptys hs \<Longrightarrow> homs(pass\<^sub>1' hs) = pass\<^sub>1 (homs hs)"
 apply(induction hs rule: Pairing_Heap_List1.pass\<^sub>1.induct)
   apply simp
  subgoal for h
  apply(case_tac h)
   apply (auto)
  done
 subgoal for h1 h2
 apply(case_tac h1)
  apply simp
 apply(case_tac h2)
  apply (auto)
 done
 done
 
 lemma hom_merge': "\<lbrakk> no_Emptys lhs; Pairing_Heap_List1_Analysis.is_root h\<rbrakk>
        \<Longrightarrow> hom (merge' (Hp x lhs) h) = link \<langle>homs lhs, x, hom h\<rangle>"
 by(cases h) auto
 
 lemma hom_pass2': "no_Emptys hs \<Longrightarrow> hom(pass\<^sub>2' hs) = pass\<^sub>2 (homs hs)"
 by(induction hs rule: homs.induct) (auto simp: hom_merge' is_root_pass2)
 
 lemma del_min': "is_root' h \<Longrightarrow> hom(del_min' h) = del_min (hom h)"
 by(cases h)
   (auto simp: homs_pass1' hom_pass2' no_Emptys_pass1 is_root_pass2)
 
 lemma insert': "is_root' h \<Longrightarrow> hom(insert' x h) = insert x (hom h)"
 by(cases h)(auto)
 
 lemma merge':
   "\<lbrakk> is_root' h1; is_root' h2 \<rbrakk> \<Longrightarrow> hom(merge' h1 h2) = merge (hom h1) (hom h2)"
 apply(cases h1)
  apply(simp)
 apply(cases h2)
  apply(auto)
 done
 
-lemma t_pass1': "no_Emptys hs \<Longrightarrow> t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs = t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1(homs hs)"
+lemma T_pass1': "no_Emptys hs \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1(homs hs)"
 apply(induction hs rule: Pairing_Heap_List1.pass\<^sub>1.induct)
   apply simp
  subgoal for h
  apply(case_tac h)
   apply (auto)
  done
 subgoal for h1 h2
 apply(case_tac h1)
  apply simp
 apply(case_tac h2)
  apply (auto)
 done
 done
 
-lemma t_pass2': "no_Emptys hs \<Longrightarrow> t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2' hs = t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2(homs hs)"
+lemma T_pass2': "no_Emptys hs \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2' hs = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2(homs hs)"
 by(induction hs rule: homs.induct) (auto simp: hom_merge' is_root_pass2)
 
 lemma size_hp: "is_root' h \<Longrightarrow> size_hp h = size (hom h)"
 proof(induction h)
   case (Hp _ hs) thus ?case
     apply(induction hs rule: homs.induct)
       apply simp
      apply force
     apply simp
     done
 qed simp
 
 interpretation Amortized2
 where arity = arity and exec = exec and inv = is_root
 and cost = cost and \<Phi> = \<Phi> and U = U
 and hom = hom
 and exec' = Pairing_Heap_List1_Analysis.exec
 and cost' = Pairing_Heap_List1_Analysis.cost and inv' = "is_root'"
 and U' = Pairing_Heap_List1_Analysis.U
 proof (standard, goal_cases)
   case (1 _ f) thus ?case
     by (cases f)(auto simp: merge' del_min' numeral_eq_Suc)
 next
   case (2 ts f)
   show ?case
   proof(cases f)
     case [simp]: Del_min
     then obtain h where [simp]: "ts = [h]" using 2 by auto
     show ?thesis using 2
       by(cases h) (auto simp: is_root_pass2 no_Emptys_pass1)
   qed (insert 2,
       auto simp: Pairing_Heap_List1_Analysis.is_root_merge numeral_eq_Suc)
 next
   case (3 t) thus ?case by (cases t) (auto)
 next
   case (4 ts f) show ?case
   proof (cases f)
     case [simp]: Del_min
     then obtain h where [simp]: "ts = [h]" using 4 by auto
     show ?thesis using 4
-      by (cases h)(auto simp: t_pass1' t_pass2' no_Emptys_pass1 homs_pass1')
+      by (cases h)(auto simp: T_pass1' T_pass2' no_Emptys_pass1 homs_pass1')
   qed (insert 4, auto)
 next
   case (5 _ f) thus ?case by(cases f) (auto simp: size_hp numeral_eq_Suc)
 qed
 
 end
diff --git a/thys/Amortized_Complexity/Pairing_Heap_List2_Analysis.thy b/thys/Amortized_Complexity/Pairing_Heap_List2_Analysis.thy
--- a/thys/Amortized_Complexity/Pairing_Heap_List2_Analysis.thy
+++ b/thys/Amortized_Complexity/Pairing_Heap_List2_Analysis.thy
@@ -1,243 +1,243 @@
 (* Author: Tobias Nipkow (based on Hauke Brinkop's tree proofs) *)
 
 subsection \<open>Okasaki's Pairing Heap (Modified)\<close>
 
 theory Pairing_Heap_List2_Analysis
 imports
   Pairing_Heap.Pairing_Heap_List2
   Amortized_Framework
   Priority_Queue_ops_merge
   Lemmas_log
 begin
 
 text
 \<open>Amortized analysis of a modified version of the pairing heaps
 defined by Okasaki \cite{Okasaki}.\<close>
 
 fun lift_hp :: "'b \<Rightarrow> ('a hp \<Rightarrow> 'b) \<Rightarrow> 'a heap \<Rightarrow> 'b" where
 "lift_hp c f None = c" |
 "lift_hp c f (Some h) = f h"
 
 fun size_hps :: "'a hp list \<Rightarrow> nat" where
 "size_hps(Hp x hsl # hsr) = size_hps hsl + size_hps hsr + 1" |
 "size_hps [] = 0"
 
 definition size_hp :: "'a hp \<Rightarrow> nat" where
 [simp]: "size_hp h = size_hps(hps h) + 1"
 
 fun \<Phi>_hps :: "'a hp list \<Rightarrow> real" where
 "\<Phi>_hps [] = 0" |
 "\<Phi>_hps (Hp x hsl # hsr) = \<Phi>_hps hsl + \<Phi>_hps hsr + log 2 (size_hps hsl + size_hps hsr + 1)"
 
 definition \<Phi>_hp :: "'a hp \<Rightarrow> real" where
 [simp]: "\<Phi>_hp h = \<Phi>_hps (hps h) + log 2 (size_hps(hps(h))+1)"
 
 abbreviation \<Phi> :: "'a heap \<Rightarrow> real" where
 "\<Phi> \<equiv> lift_hp 0 \<Phi>_hp"
 
 abbreviation size_heap :: "'a heap \<Rightarrow> nat" where
 "size_heap \<equiv> lift_hp 0 size_hp"
 
 lemma \<Phi>_hps_ge0: "\<Phi>_hps hs \<ge> 0"
 by (induction hs rule: size_hps.induct) auto
 
 declare algebra_simps[simp]
 
 lemma size_hps_Cons[simp]: "size_hps(h # hs) = size_hp h + size_hps hs"
 by(cases h) simp
 
 lemma link2: "link (Hp x lx) h = (case h of (Hp y ly) \<Rightarrow> 
     (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly)))"
 by(simp split: hp.split)
 
 lemma size_hps_link: "size_hps(hps (link h1 h2)) = size_hp h1 + size_hp h2 - 1" 
 by (induction rule: link.induct) simp_all
 
 lemma pass\<^sub>1_size[simp]: "size_hps (pass\<^sub>1 hs) = size_hps hs" 
 by (induct hs rule: pass\<^sub>1.induct) (simp_all add: size_hps_link)
 
 lemma pass\<^sub>2_None[simp]: "pass\<^sub>2 hs = None \<longleftrightarrow> hs = []"
 by(cases hs) auto
 
 lemma \<Delta>\<Phi>_insert:
   "\<Phi> (Pairing_Heap_List2.insert x h) - \<Phi> h \<le> log 2 (size_heap h + 1)"
 by(induct h)(auto simp: link2 split: hp.split)
 
 lemma \<Delta>\<Phi>_link: "\<Phi>_hp (link h1 h2) - \<Phi>_hp h1 - \<Phi>_hp h2 \<le> 2 * log 2 (size_hp h1 + size_hp h2)"
 by (induction h1 h2 rule: link.induct) (simp  add: add_increasing)
 
 fun sum_ub :: "'a hp list \<Rightarrow> real" where
   "sum_ub [] = 0"
 | "sum_ub [Hp _ _] = 0"
 | "sum_ub [Hp _ lx, Hp _ ly] = 2*log 2 (2 + size_hps lx + size_hps ly)" 
 | "sum_ub (Hp _ lx # Hp _ ly # ry) = 2*log 2 (2 + size_hps lx + size_hps ly + size_hps ry) 
     - 2*log 2 (size_hps ry) - 2 + sum_ub ry"
 
 
 lemma \<Delta>\<Phi>_pass1_sum_ub: "\<Phi>_hps (pass\<^sub>1 h) - \<Phi>_hps h  \<le> sum_ub h"
 proof (induction h rule: sum_ub.induct)
   case (3 lx x ly y)
   have 0: "\<And>x y::real. 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x \<le> 2*y" by linarith
   show ?case by (simp add: add_increasing 0)
 next
   case (4 x hsx y hsy z hsize_hp)
   let ?ry = "z # hsize_hp"
   let ?rx = "Hp y hsy # ?ry"
   let ?h = "Hp x hsx # ?rx"
   have "\<Phi>_hps(pass\<^sub>1 ?h) - \<Phi>_hps ?h  
     \<le> log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry) + sum_ub ?ry"
     using "4.IH" by simp
   also have "log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry) 
     \<le> 2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2"
   proof -
     have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) - 2*log 2 (size_hps ?h) 
       = log 2 ((1 + size_hps hsx + size_hps hsy)/(size_hps ?h) ) + log 2 (size_hps ?ry / size_hps ?h)"
       by (simp add: log_divide)
     also have "\<dots> \<le> -2" 
     proof -
       have "2 + \<dots>
         \<le> 2*log 2 ((1 + size_hps hsx + size_hps hsy) / size_hps ?h +  size_hps ?ry / size_hps ?h)"  
         using ld_sum_inequality [of "(1 + size_hps hsx + size_hps hsy) / size_hps ?h" "(size_hps ?ry / size_hps ?h)"] by simp
       also have "\<dots> \<le> 0" by (simp add: field_simps log_divide add_pos_nonneg)
       finally show ?thesis by linarith
     qed 
     finally have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) + 2
       \<le>  2*log 2 (size_hps ?h)" by simp
     moreover have "log 2 (size_hps ?ry) \<le> log 2 (size_hps ?rx)" by simp
     ultimately have "log 2 (1 + size_hps hsx + size_hps hsy) - \<dots> 
       \<le>  2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2" by linarith
     thus ?thesis by simp
   qed
   finally show ?case by (simp)
 qed simp_all
 
 
 lemma \<Delta>\<Phi>_pass1: assumes "hs \<noteq> []"
   shows "\<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (size_hps hs) - length hs + 2"
 proof - 
   have "sum_ub hs \<le> 2 * log 2 (size_hps hs) - length hs + 2" 
     using assms by (induct hs rule: sum_ub.induct) (simp_all)
   thus ?thesis using \<Delta>\<Phi>_pass1_sum_ub[of hs] by linarith
 qed
 
 lemma size_hps_pass2: "pass\<^sub>2 hs = Some h \<Longrightarrow> size_hps hs = size_hps(hps h)+1"
 apply(induction hs arbitrary: h rule: \<Phi>_hps.induct)
 apply (auto simp: link2 split: option.split hp.split)
 done
 
 lemma \<Delta>\<Phi>_pass2: "hs \<noteq> [] \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (size_hps hs)"
 proof (induction hs)
   case (Cons h hs)
   thus ?case
   proof -
     obtain x hs2 where [simp]: "h = Hp x hs2" by (metis hp.exhaust)
     show ?thesis
     proof (cases "pass\<^sub>2 hs")
       case [simp]: (Some h2)
       obtain y hs3 where [simp]: "h2 = Hp y hs3" by (metis hp.exhaust)
       from size_hps_pass2[OF Some] Cons show ?thesis
         by(cases "hs=[]")(auto simp: add_mono)
     qed simp
   qed
 qed simp
 
 lemma \<Delta>\<Phi>_del_min: assumes "hps h \<noteq> []"
   shows "\<Phi> (del_min (Some h)) - \<Phi> (Some h) 
   \<le> 3 * log 2 (size_hps(hps h)) - length(hps h) + 2"
 proof -
   let ?\<Delta>\<Phi>\<^sub>1 = "\<Phi>_hps(hps h) - \<Phi>_hp h" 
   let ?\<Delta>\<Phi>\<^sub>2 = "\<Phi>(pass\<^sub>2(pass\<^sub>1 (hps h))) - \<Phi>_hps (hps h)"
   let ?\<Delta>\<Phi> = "\<Phi> (del_min (Some h)) - \<Phi> (Some h)"
   have "\<Phi>(pass\<^sub>2(pass\<^sub>1(hps h))) - \<Phi>_hps (pass\<^sub>1(hps h)) \<le> log 2 (size_hps(hps h))" 
     using \<Delta>\<Phi>_pass2[of "pass\<^sub>1(hps h)"] using size_hps.elims assms by force
   moreover have "\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le>  2*\<dots> - length (hps h) + 2"
     using \<Delta>\<Phi>_pass1[OF assms] by blast
   moreover have "?\<Delta>\<Phi>\<^sub>1 \<le> 0" by (cases h) simp
   moreover have "?\<Delta>\<Phi> = ?\<Delta>\<Phi>\<^sub>1 + ?\<Delta>\<Phi>\<^sub>2" by (cases h) simp
   ultimately show ?thesis by linarith
 qed
 
 
 fun exec :: "'a :: linorder op \<Rightarrow> 'a heap list \<Rightarrow> 'a heap" where
 "exec Empty [] = None" | 
 "exec Del_min [h] = del_min h" |
 "exec (Insert x) [h] = Pairing_Heap_List2.insert x h" |
 "exec Merge [h1,h2] = merge h1 h2"
 
-fun t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 :: "'a hp list \<Rightarrow> nat" where
-  "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [] = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [_] = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (_ # _ # hs) = 1 + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs"
+fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 :: "'a hp list \<Rightarrow> nat" where
+  "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [] = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 [_] = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (_ # _ # hs) = 1 + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs"
 
-fun t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 :: "'a hp list \<Rightarrow> nat" where
- "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 [] = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (_ # hs) = 1 + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 hs"
+fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 :: "'a hp list \<Rightarrow> nat" where
+"T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 [] = 1" |
+"T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (_ # hs) = 1 + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 hs"
 
 fun cost :: "'a :: linorder op \<Rightarrow> 'a heap list \<Rightarrow> nat" where
 "cost Empty _ = 1" |
 "cost Del_min [None] = 1" |
-"cost Del_min [Some(Hp x hs)] = 1 + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs" |
+"cost Del_min [Some(Hp x hs)] = 1 + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs" |
 "cost (Insert a) _ = 1" |
 "cost Merge _ = 1"
 
 fun U :: "'a :: linorder op \<Rightarrow> 'a heap list \<Rightarrow> real" where
 "U Empty _ = 1" |
 "U (Insert a) [h] = log 2 (size_heap h + 1) + 1" |
 "U Del_min [h] = 3*log 2 (size_heap h + 1) + 5" |
 "U Merge [h1,h2] = 2*log 2 (size_heap h1 + size_heap h2 + 1) + 1"
 
 interpretation pairing: Amortized
 where arity = arity and exec = exec and cost = cost and inv = "\<lambda>_. True"
 and \<Phi> = \<Phi> and U = U
 proof (standard, goal_cases)
   case (2 s) show ?case by (cases s) (auto simp: \<Phi>_hps_ge0)
 next
   case (3 ss f) show ?case
   proof (cases f)
     case Empty with 3 show ?thesis by(auto)
   next
     case Insert
     thus ?thesis using Insert \<Delta>\<Phi>_insert 3 by auto
   next
     case [simp]: Del_min
     then obtain ho where [simp]: "ss = [ho]" using 3 by auto
     show ?thesis
     proof (cases ho)
       case [simp]: (Some h)
         show ?thesis
         proof (cases h)
         case [simp]: (Hp x hs)
-        have "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs \<le> 2 + length hs"
+        have "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 hs) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 hs \<le> 2 + length hs"
           by (induct hs rule: pass\<^sub>1.induct) simp_all
         hence  "cost f ss \<le> 1 + \<dots>" by simp
         moreover have  "\<Phi> (del_min ho) - \<Phi> ho \<le> 3*log 2 (size_heap ho + 1) - length hs + 2"
         proof (cases "hs = []")
           case False
           hence "\<Phi> (del_min ho) - \<Phi> ho \<le> 3*log 2 (size_hps hs) - length hs + 2"
             using  \<Delta>\<Phi>_del_min[of h] by simp
           also have "\<dots> \<le> 3*log 2 (size_heap ho + 1) - length hs + 2"
             using False size_hps.elims by force
           finally show ?thesis .
         qed simp
         ultimately show ?thesis by simp
       qed
     qed simp
   next
     case [simp]: Merge
     then obtain ho1 ho2 where [simp]: "ss = [ho1, ho2]"
       using 3 by(auto simp: numeral_eq_Suc)
     show ?thesis
     proof (cases "ho1 = None \<or> ho2 = None")
       case True thus ?thesis by auto
     next
       case False
       then obtain h1 h2 where [simp]: "ho1 = Some h1" "ho2 = Some h2" by auto
       have "\<Phi> (merge ho1 ho2) - \<Phi> ho1 - \<Phi> ho2 \<le> 2 * log 2 (size_heap ho1 + size_heap ho2)"
         using \<Delta>\<Phi>_link[of h1 h2] by simp
       also have "\<dots> \<le> 2 * log 2 (size_hp h1 + size_hp h2 + 1)" by (simp)
       finally show ?thesis by(simp)
     qed
   qed
 qed simp
 
 end
diff --git a/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy b/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy
--- a/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy
+++ b/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy
@@ -1,268 +1,268 @@
 (* Author: Hauke Brinkop and Tobias Nipkow *)
 
 section \<open>Pairing Heaps\<close>
 
 subsection \<open>Binary Tree Representation\<close>
 
 theory Pairing_Heap_Tree_Analysis
 imports  
   Pairing_Heap.Pairing_Heap_Tree
   Amortized_Framework
   Priority_Queue_ops_merge
   Lemmas_log
 begin
 
 text
 \<open>Verification of logarithmic bounds on the amortized complexity of
 pairing heaps \cite{FredmanSST86,Brinkop}.\<close>
 
 fun len :: "'a tree \<Rightarrow> nat" where 
   "len Leaf = 0"
 | "len (Node _ _ r) = 1 + len r"
 
 fun \<Phi> :: "'a tree \<Rightarrow> real" where
   "\<Phi> Leaf = 0"
 | "\<Phi> (Node l _ r) = \<Phi> l + \<Phi> r + log 2 (1 + size l + size r)"
 
 lemma link_size[simp]: "size (link h) = size h" 
   by (cases h rule: link.cases) simp_all
 
 lemma size_pass\<^sub>1: "size (pass\<^sub>1 h) = size h" 
   by (induct h rule: pass\<^sub>1.induct) simp_all
 
 lemma size_pass\<^sub>2: "size (pass\<^sub>2 h) = size h" 
   by (induct h rule: pass\<^sub>2.induct) simp_all
 
 lemma size_merge: 
   "is_root h1 \<Longrightarrow> is_root h2 \<Longrightarrow> size (merge h1 h2) = size h1 + size h2"
   by (simp split: tree.splits)
 
 lemma \<Delta>\<Phi>_insert: "is_root h \<Longrightarrow> \<Phi> (insert x h) - \<Phi> h \<le> log 2  (size h + 1)"
   by (simp split: tree.splits)
 
 lemma \<Delta>\<Phi>_merge:
   assumes "h1 = Node lx x Leaf" "h2 = Node ly y Leaf" 
   shows "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (size h1 + size h2) + 1" 
 proof -
   let ?hs = "Node lx x (Node ly y Leaf)"
   have "\<Phi> (merge h1 h2) = \<Phi> (link ?hs)" using assms by simp
   also have "\<dots> = \<Phi> lx + \<Phi> ly + log 2 (size lx + size ly + 1) + log 2 (size lx + size ly + 2)"
     by (simp add: algebra_simps)
   also have "\<dots> = \<Phi> lx + \<Phi> ly + log 2 (size lx + size ly + 1) + log 2 (size h1 + size h2)"
      using assms by simp
   finally have "\<Phi> (merge h1 h2) = \<dots>" .
   have "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 =
    log 2 (size lx + size ly + 1) + log 2 (size h1 + size h2)
    - log 2 (size lx + 1) - log 2 (size ly + 1)"
      using assms by (simp add: algebra_simps)
   also have "\<dots> \<le> log 2 (size h1 + size h2) + 1"
     using ld_le_2ld[of "size lx" "size ly"] assms by (simp add: algebra_simps)
   finally show ?thesis .
 qed
 
 fun upperbound :: "'a tree \<Rightarrow> real" where
   "upperbound Leaf = 0"
 | "upperbound (Node _ _ Leaf) = 0"
 | "upperbound (Node lx _ (Node ly _ Leaf)) = 2*log 2 (size lx + size ly + 2)" 
 | "upperbound (Node lx _ (Node ly _ ry)) = 2*log 2 (size lx + size ly + size ry + 2) 
     - 2*log 2 (size ry) - 2 + upperbound ry"
 
 lemma \<Delta>\<Phi>_pass1_upperbound: "\<Phi> (pass\<^sub>1 hs) - \<Phi> hs  \<le> upperbound hs"
 proof (induction hs rule: upperbound.induct)
   case (3 lx x ly y)
   have "log 2  (size lx + size ly + 1) - log 2  (size ly + 1) 
     \<le> log 2 (size lx + size ly + 1)" by simp
   also have "\<dots> \<le> log 2 (size lx + size ly + 2)" by simp
   also have "\<dots> \<le> 2*\<dots>" by simp
   finally show ?case by (simp add: algebra_simps)
 next
   case (4 lx x ly y lz z rz)
   let ?ry = "Node lz z rz"
   let ?rx = "Node ly y ?ry"
   let ?h = "Node lx x ?rx"
   let ?t ="log 2 (size lx + size ly + 1) - log 2 (size ly + size ?ry + 1)"
   have "\<Phi> (pass\<^sub>1 ?h) - \<Phi> ?h \<le> ?t + upperbound ?ry" 
     using "4.IH" by (simp add: size_pass\<^sub>1 algebra_simps)
   moreover have "log 2 (size lx + size ly + 1) + 2 * log 2 (size ?ry) + 2
     \<le> 2 * log 2 (size ?h) + log 2 (size ly + size ?ry + 1)" (is "?l \<le> ?r")
   proof -
     have "?l \<le> 2 * log 2 (size lx + size ly + size ?ry + 1) + log 2 (size ?ry)"
       using ld_sum_inequality [of "size lx + size ly + 1" "size ?ry"] by simp
     also have "\<dots> \<le> 2 * log 2 (size lx + size ly + size ?ry + 2) + log 2 (size ?ry)"
       by simp
     also have "\<dots> \<le> ?r" by simp
     finally show ?thesis .
   qed
   ultimately show ?case by simp
 qed simp_all
 
 lemma \<Delta>\<Phi>_pass1: assumes "hs \<noteq> Leaf"
   shows "\<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2*log 2 (size hs) - len hs + 2"
 proof -
   from assms have "upperbound hs \<le> 2*log 2 (size hs) - len hs + 2" 
     by (induct hs rule: upperbound.induct) (simp_all add: algebra_simps)
   thus ?thesis using \<Delta>\<Phi>_pass1_upperbound [of "hs"] order_trans by blast
 qed
 
 lemma \<Delta>\<Phi>_pass2: "hs \<noteq> Leaf \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (size hs)"
 proof (induction hs)
   case (Node lx x rx)
   thus ?case 
   proof (cases rx)
     case 1: (Node ly y ry)
     let ?h = "Node lx x rx"
     obtain la a where 2: "pass\<^sub>2 rx = Node la a Leaf" 
       using pass\<^sub>2_struct 1 by force
     hence 3: "size rx = size \<dots>" using size_pass\<^sub>2 by metis
     have link: "\<Phi>(link(Node lx x (pass\<^sub>2 rx))) - \<Phi> lx - \<Phi> (pass\<^sub>2 rx) =
           log 2 (size lx + size rx + 1) + log 2 (size lx + size rx) - log 2 (size rx)"
       using 2 3 by (simp add: algebra_simps) 
     have "\<Phi> (pass\<^sub>2 ?h) - \<Phi> ?h =
         \<Phi> (link (Node lx x (pass\<^sub>2 rx))) - \<Phi> lx - \<Phi> rx - log 2 (size lx + size rx + 1)"
       by (simp)
     also have "\<dots> = \<Phi> (pass\<^sub>2 rx) - \<Phi> rx + log 2 (size lx + size rx) - log 2 (size rx)"
       using link by linarith
     also have "\<dots> \<le> log 2 (size lx + size rx)"
       using Node.IH 1 by simp
     also have "\<dots> \<le> log 2 (size ?h)" using 1 by simp
     finally show ?thesis .
   qed simp
 qed simp
 
 lemma \<Delta>\<Phi>_mergepairs: assumes "hs \<noteq> Leaf"
   shows "\<Phi> (merge_pairs hs) - \<Phi> hs \<le> 3 * log 2 (size hs) - len hs + 2"
 proof -
   have "pass\<^sub>1 hs \<noteq> Leaf" by (metis assms eq_size_0 size_pass\<^sub>1)
   with assms \<Delta>\<Phi>_pass1[of hs] \<Delta>\<Phi>_pass2[of "pass\<^sub>1 hs"]
   show ?thesis by (auto simp add: size_pass\<^sub>1 pass12_merge_pairs)
 qed
 
 lemma \<Delta>\<Phi>_del_min: assumes "lx \<noteq> Leaf"
 shows "\<Phi> (del_min (Node lx x Leaf)) - \<Phi> (Node lx x Leaf) 
   \<le> 3*log 2 (size lx) - len lx + 2"
 proof -
   let ?h = "Node lx x Leaf"
   let ?\<Delta>\<Phi>\<^sub>1 = "\<Phi> lx - \<Phi> ?h" 
   let ?\<Delta>\<Phi>\<^sub>2 = "\<Phi>(pass\<^sub>2(pass\<^sub>1 lx)) - \<Phi> lx"
   let ?\<Delta>\<Phi> = "\<Phi> (del_min ?h) - \<Phi> ?h"
   have "lx \<noteq> Leaf \<Longrightarrow> \<Phi>(pass\<^sub>2(pass\<^sub>1 lx)) - \<Phi> (pass\<^sub>1 lx) \<le> log 2  (size lx)" 
     using \<Delta>\<Phi>_pass2 [of "pass\<^sub>1 lx"] by(metis eq_size_0 size_pass\<^sub>1)
   moreover have "lx \<noteq> Leaf \<Longrightarrow> \<Phi> (pass\<^sub>1 lx) - \<Phi> lx \<le>  2*\<dots> - len lx + 2" 
     using \<Delta>\<Phi>_pass1 by metis
   moreover have "?\<Delta>\<Phi> \<le> ?\<Delta>\<Phi>\<^sub>2" by simp
   ultimately show ?thesis using assms by linarith
 qed
 
 lemma is_root_merge:
   "is_root h1 \<Longrightarrow> is_root h2 \<Longrightarrow> is_root (merge h1 h2)"
 by (simp split: tree.splits)
 
 lemma is_root_insert: "is_root h \<Longrightarrow> is_root (insert x h)"
 by (simp split: tree.splits)
 
 lemma is_root_del_min:
   assumes "is_root h" shows "is_root (del_min h)"
 proof (cases h)
   case [simp]: (Node lx x rx)
   have "rx = Leaf" using assms by simp
   thus ?thesis 
   proof (cases lx)
     case (Node ly y ry)
     then obtain la a ra where "pass\<^sub>1 lx = Node a la ra" 
       using pass\<^sub>1_struct by blast
     moreover obtain lb b where "pass\<^sub>2 \<dots> = Node b lb Leaf"
       using pass\<^sub>2_struct by blast
     ultimately show ?thesis using assms by simp
   qed simp
 qed simp
 
 lemma pass\<^sub>1_len: "len (pass\<^sub>1 h) \<le> len h"
 by (induct h rule: pass\<^sub>1.induct) simp_all
 
 fun exec :: "'a :: linorder op \<Rightarrow> 'a tree list \<Rightarrow> 'a tree" where
 "exec Empty [] = Leaf" | 
 "exec Del_min [h] = del_min h" |
 "exec (Insert x) [h] = insert x h" |
 "exec Merge [h1,h2] = merge h1 h2"
 
-fun t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 :: "'a tree \<Rightarrow> nat" where
-  "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 Leaf = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (Node _ _ Leaf) = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (Node _ _ (Node _ _ ry)) = t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 ry + 1"
+fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 :: "'a tree \<Rightarrow> nat" where
+  "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 Leaf = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (Node _ _ Leaf) = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (Node _ _ (Node _ _ ry)) = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 ry + 1"
 
-fun t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 :: "'a tree \<Rightarrow> nat" where
-  "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 Leaf = 1"
-| "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (Node _ _ rx) = t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 rx + 1"
+fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 :: "'a tree \<Rightarrow> nat" where
+  "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 Leaf = 1"
+| "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (Node _ _ rx) = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 rx + 1"
 
 fun cost :: "'a :: linorder op \<Rightarrow> 'a tree list \<Rightarrow> nat" where
   "cost Empty [] = 1"
 | "cost Del_min [Leaf] = 1"
-| "cost Del_min [Node lx _  _] = t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 lx) + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 lx"
+| "cost Del_min [Node lx _  _] = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 lx) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 lx"
 | "cost (Insert a) _ = 1"
 | "cost Merge _ = 1"
 
 fun U :: "'a :: linorder op \<Rightarrow> 'a tree list \<Rightarrow> real" where
   "U Empty [] = 1"
 | "U (Insert a) [h] = log 2 (size h + 1) + 1"
 | "U Del_min [h] = 3*log 2 (size h + 1) + 4"
 | "U Merge [h1,h2] = log 2 (size h1 + size h2 + 1) + 2"
 
 interpretation Amortized
 where arity = arity and exec = exec and cost = cost and inv = is_root 
 and \<Phi> = \<Phi> and U = U
 proof (standard, goal_cases)
   case (1 _ f) thus ?case using is_root_insert is_root_del_min is_root_merge
     by (cases f) (auto simp: numeral_eq_Suc)
 next
   case (2 s) show ?case by (induct s) simp_all
 next
   case (3 ss f) show ?case 
   proof (cases f)
     case Empty with 3 show ?thesis by(auto)
   next
     case (Insert x)
     then obtain h where "ss = [h]" "is_root h" using 3 by auto
     thus ?thesis using Insert \<Delta>\<Phi>_insert 3 by auto
   next
     case [simp]: (Del_min)
     then obtain h where [simp]: "ss = [h]" using 3 by auto
     show ?thesis
     proof (cases h)
       case [simp]: (Node lx x rx)
-      have "t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 lx) + t\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 lx \<le> len lx + 2"
+      have "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 lx) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 lx \<le> len lx + 2"
         by (induct lx rule: pass\<^sub>1.induct) simp_all
       hence "cost f ss \<le> \<dots>" by simp 
       moreover have "\<Phi> (del_min h) - \<Phi> h \<le> 3*log 2 (size h + 1) - len lx + 2"
       proof (cases lx)
         case [simp]: (Node ly y ry) 
         have "\<Phi> (del_min h) - \<Phi> h \<le> 3*log 2 (size lx) - len lx + 2"
           using  \<Delta>\<Phi>_del_min[of "lx" "x"] 3 by simp
         also have "\<dots> \<le> 3*log 2 (size h + 1) - len lx + 2" by fastforce
         finally show ?thesis by blast
       qed (insert 3, simp)
       ultimately show ?thesis by auto
     qed simp
   next
     case [simp]: Merge
     then obtain h1 h2 where [simp]: "ss = [h1,h2]" and 1: "is_root h1" "is_root h2"
       using 3 by (auto simp: numeral_eq_Suc)
     show ?thesis
     proof (cases h1)
       case Leaf thus ?thesis by (cases h2) auto
     next
       case h1: Node
       show ?thesis
       proof (cases h2)
         case Leaf thus ?thesis using h1 by simp
       next
         case h2: Node
         have "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1"
           apply(rule \<Delta>\<Phi>_merge) using h1 h2 1 by auto
         also have "\<dots> \<le> log 2 (size h1 + size h2 + 1) + 1" by (simp add: h1)
         finally show ?thesis by(simp add: algebra_simps)
       qed
     qed
   qed
 qed
 
 end