src/HOL/Data_Structures/Tree234.thy
changeset 61515 c64628dbac00
child 61640 44c9198f210c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/Tree234.thy	Sun Oct 25 17:31:14 2015 +0100
     1.3 @@ -0,0 +1,45 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section {* 2-3-4 Trees *}
     1.7 +
     1.8 +theory Tree234
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +class height =
    1.13 +fixes height :: "'a \<Rightarrow> nat"
    1.14 +
    1.15 +datatype 'a tree234 =
    1.16 +  Leaf |
    1.17 +  Node2 "'a tree234" 'a "'a tree234" |
    1.18 +  Node3 "'a tree234" 'a "'a tree234" 'a "'a tree234" |
    1.19 +  Node4 "'a tree234" 'a "'a tree234" 'a "'a tree234" 'a "'a tree234"
    1.20 +
    1.21 +fun inorder :: "'a tree234 \<Rightarrow> 'a list" where
    1.22 +"inorder Leaf = []" |
    1.23 +"inorder(Node2 l a r) = inorder l @ a # inorder r" |
    1.24 +"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |
    1.25 +"inorder(Node4 l a m b n c r) = inorder l @ a # inorder m @ b # inorder n @ c # inorder r"
    1.26 +
    1.27 +
    1.28 +instantiation tree234 :: (type)height
    1.29 +begin
    1.30 +
    1.31 +fun height_tree234 :: "'a tree234 \<Rightarrow> nat" where
    1.32 +"height Leaf = 0" |
    1.33 +"height (Node2 l _ r) = Suc(max (height l) (height r))" |
    1.34 +"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
    1.35 +"height (Node4 l _ m _ n _ r) = Suc(max (height l) (max (height m) (max (height n) (height r))))"
    1.36 +
    1.37 +instance ..
    1.38 +
    1.39 +end
    1.40 +
    1.41 +text{* Balanced: *}
    1.42 +fun bal :: "'a tree234 \<Rightarrow> bool" where
    1.43 +"bal Leaf = True" |
    1.44 +"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    1.45 +"bal (Node3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" |
    1.46 +"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)"
    1.47 +
    1.48 +end