# HG changeset patch
# User nipkow
# Date 1553179864 -3600
# Node ID 423c0b571f1e85caa6f374acae00c52b53976b14
# Parent  d043ccb998eea23fdc46d258696e5e1ca20699b6
added function

diff -r d043ccb998ee -r 423c0b571f1e src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 14:18:37 2019 +0000
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 15:51:04 2019 +0100
@@ -269,6 +269,23 @@
 subsection "Faster"
 
 
+subsubsection \<open>Size\<close>
+
+fun diff :: "'a tree \<Rightarrow> nat \<Rightarrow> nat" where
+"diff Leaf 0 = 0" |
+"diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))"
+
+fun size_fast :: "'a tree \<Rightarrow> nat" where
+"size_fast Leaf = 0" |
+"size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
+
+lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = (if size t = n then 0 else 1)"
+by(induction t arbitrary: n) auto
+
+lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"
+by(induction t) (auto simp add: Let_def diff)
+
+
 subsubsection \<open>Initialization with 1 element\<close>
 
 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where