added function
authornipkow
Thu Mar 21 15:51:04 2019 +0100 (3 months ago)
changeset 69941423c0b571f1e
parent 69940 d043ccb998ee
child 69942 2c48be88f847
child 69943 deb05b4c48ba
added function
src/HOL/Data_Structures/Array_Braun.thy
     1.1 --- a/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 14:18:37 2019 +0000
     1.2 +++ b/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 15:51:04 2019 +0100
     1.3 @@ -269,6 +269,23 @@
     1.4  subsection "Faster"
     1.5  
     1.6  
     1.7 +subsubsection \<open>Size\<close>
     1.8 +
     1.9 +fun diff :: "'a tree \<Rightarrow> nat \<Rightarrow> nat" where
    1.10 +"diff Leaf 0 = 0" |
    1.11 +"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))"
    1.12 +
    1.13 +fun size_fast :: "'a tree \<Rightarrow> nat" where
    1.14 +"size_fast Leaf = 0" |
    1.15 +"size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
    1.16 +
    1.17 +lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = (if size t = n then 0 else 1)"
    1.18 +by(induction t arbitrary: n) auto
    1.19 +
    1.20 +lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"
    1.21 +by(induction t) (auto simp add: Let_def diff)
    1.22 +
    1.23 +
    1.24  subsubsection \<open>Initialization with 1 element\<close>
    1.25  
    1.26  fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where