# HG changeset patch
# User Thomas Sewell <sewell@chalmers.se>
# Date 1553614049 -3600
# Node ID 8e916ed23d17fcdeb6f002eb5ee2b851e7b4e56f
# Parent  3afa3b25b5e75e726f1dc7d897ac4a3c75d1af43
follow up on Braun: get timing function right

diff -r 3afa3b25b5e7 -r 8e916ed23d17 src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Tue Mar 26 16:03:01 2019 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Tue Mar 26 16:27:29 2019 +0100
@@ -547,8 +547,8 @@
 
 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 if us = [] then 0 else
-  length ts + 5 * length us + t_list_fast_rec (map left us @ map right us))"
+  in length ts + (if us = [] then 0 else
+  5 * length us + t_list_fast_rec (map left us @ map right us)))"
 by (pat_completeness, auto)
 
 termination
@@ -635,8 +635,9 @@
   show ?case
   proof cases
     assume "?us = []"
-    thus ?thesis using t_list_fast_rec.simps[of ts] by(simp add: Let_def)
-  next
+    thus ?thesis using t_list_fast_rec.simps[of ts]
+      by(simp add: Let_def 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"