# HG changeset patch # User nipkow # Date 1736799460 -3600 # Node ID 40f979c845b7d68f06b201ef7cb7428792a5e7ea # Parent 4d78ad5abeca0c78e37e2742f084a052c45132b9 moved lemmas to book 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 (\t. t \ 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]