tuned
authornipkow
Thu Nov 09 09:08:14 2017 +0100 (10 months ago)
changeset 67038db3e2240f830
parent 67037 a76fb0f4b9ca
child 67039 690b4b334889
tuned
src/HOL/Data_Structures/Tree23_Set.thy
     1.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Wed Nov 08 21:02:05 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 09 09:08:14 2017 +0100
     1.3 @@ -108,6 +108,9 @@
     1.4  "del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
     1.5  "del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
     1.6  
     1.7 +text \<open>In the base cases of \<open>del_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
     1.8 +in which case balancedness implies that so are the others. Exercise.\<close>
     1.9 +
    1.10  fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    1.11  "del x Leaf = T\<^sub>d Leaf" |
    1.12  "del x (Node2 Leaf a Leaf) =