1(* Author: Tobias Nipkow *) 2 3section \<open>2-3 Trees\<close> 4 5theory Tree23 6imports Main 7begin 8 9class height = 10fixes height :: "'a \<Rightarrow> nat" 11 12datatype 'a tree23 = 13 Leaf ("\<langle>\<rangle>") | 14 Node2 "'a tree23" 'a "'a tree23" ("\<langle>_, _, _\<rangle>") | 15 Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" ("\<langle>_, _, _, _, _\<rangle>") 16 17fun inorder :: "'a tree23 \<Rightarrow> 'a list" where 18"inorder Leaf = []" | 19"inorder(Node2 l a r) = inorder l @ a # inorder r" | 20"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" 21 22 23instantiation tree23 :: (type)height 24begin 25 26fun height_tree23 :: "'a tree23 \<Rightarrow> nat" where 27"height Leaf = 0" | 28"height (Node2 l _ r) = Suc(max (height l) (height r))" | 29"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" 30 31instance .. 32 33end 34 35text \<open>Balanced:\<close> 36 37fun bal :: "'a tree23 \<Rightarrow> bool" where 38"bal Leaf = True" | 39"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" | 40"bal (Node3 l _ m _ r) = 41 (bal l & bal m & bal r & height l = height m & height m = height r)" 42 43lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1" 44by (induction t) auto 45 46end 47