--- a/src/HOL/Data_Structures/Array_Braun.thy Mon Jan 14 14:46:12 2019 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy Mon Jan 14 16:10:56 2019 +0100
@@ -501,7 +501,7 @@
function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
"list_fast_rec ts = (if ts = [] then [] else
let us = filter (\<lambda>t. t \<noteq> Leaf) ts
- in map root_val us @ list_fast_rec (map left us @ map right us))"
+ in map value us @ list_fast_rec (map left us @ map right us))"
by (pat_completeness, auto)
lemma list_fast_rec_term: "\<lbrakk> ts \<noteq> []; us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<rbrakk> \<Longrightarrow>
@@ -576,13 +576,13 @@
case False
with less.prems(2) have *:
"\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf
- \<and> root_val (ts ! i) = xs ! i
+ \<and> value (ts ! i) = xs ! i
\<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
\<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
\<longrightarrow> braun_list (right (ts ! i)) ys)"
by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
algebra_simps)
- have 1: "map root_val ts = take (2 ^ k) xs"
+ have 1: "map value ts = take (2 ^ k) xs"
using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
using less.prems(1) False