merged
authornipkow
Thu Mar 21 19:46:26 2019 +0100 (4 weeks ago)
changeset 69944ab8aad4aa76e
parent 69942 2c48be88f847
parent 69943 deb05b4c48ba
child 69945 35ba13ac6e5c
child 69948 a591de179931
merged
     1.1 --- a/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 16:16:43 2019 +0100
     1.2 +++ b/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 19:46:26 2019 +0100
     1.3 @@ -279,7 +279,7 @@
     1.4  "size_fast Leaf = 0" |
     1.5  "size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
     1.6  
     1.7 -lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = (if size t = n then 0 else 1)"
     1.8 +lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n"
     1.9  by(induction t arbitrary: n) auto
    1.10  
    1.11  lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"