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