
diff -r 4d78ad5abeca -r 40f979c845b7 src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Sun Jan 12 23:07:50 2025 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Mon Jan 13 21:17:40 2025 +0100
@@ -500,13 +500,6 @@
 
 time_fun brauns
 
-lemma T_brauns_pretty: "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 T_take (2 ^ k) xs + T_drop (2 ^ k) xs + T_brauns (k + 1) zs + T_drop (2 ^ k) ts + T_nodes ts ys (drop (2 ^ k) ts)) + 1"
-by(simp)
-
 lemma T_brauns_simple: "T_brauns k xs = (if xs = [] then 0 else
    3 * (min (2^k) (length xs) + 1) + (min (2^k) (length xs - 2^k) + 1) + T_brauns (k+1) (drop (2^k) xs)) + 1"
 by(simp add: T_nodes T_take T_drop length_brauns min_def)
@@ -615,13 +608,6 @@
 termination
   by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term defs)
 
-lemma T_list_fast_rec_pretty:
-  "T_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts
-  in length ts + 1 + (if us = [] then 0 else
-  5 * (length us + 1) + T_list_fast_rec (map left us @ map right us))) + 1"
-unfolding defs T_list_fast_rec.simps[of ts]
-by(simp add: T_append)
-
 declare T_list_fast_rec.simps[simp del]
 
 




