src/HOL/Data_Structures/Tree234.thy
author nipkow
Sun Oct 25 17:31:14 2015 +0100 (2015-10-25)
changeset 61515 c64628dbac00
child 61640 44c9198f210c
permissions -rw-r--r--
added 234-trees (slow)
     1 (* Author: Tobias Nipkow *)
     2 
     3 section {* 2-3-4 Trees *}
     4 
     5 theory Tree234
     6 imports Main
     7 begin
     8 
     9 class height =
    10 fixes height :: "'a \<Rightarrow> nat"
    11 
    12 datatype 'a tree234 =
    13   Leaf |
    14   Node2 "'a tree234" 'a "'a tree234" |
    15   Node3 "'a tree234" 'a "'a tree234" 'a "'a tree234" |
    16   Node4 "'a tree234" 'a "'a tree234" 'a "'a tree234" 'a "'a tree234"
    17 
    18 fun inorder :: "'a tree234 \<Rightarrow> 'a list" where
    19 "inorder Leaf = []" |
    20 "inorder(Node2 l a r) = inorder l @ a # inorder r" |
    21 "inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |
    22 "inorder(Node4 l a m b n c r) = inorder l @ a # inorder m @ b # inorder n @ c # inorder r"
    23 
    24 
    25 instantiation tree234 :: (type)height
    26 begin
    27 
    28 fun height_tree234 :: "'a tree234 \<Rightarrow> nat" where
    29 "height Leaf = 0" |
    30 "height (Node2 l _ r) = Suc(max (height l) (height r))" |
    31 "height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
    32 "height (Node4 l _ m _ n _ r) = Suc(max (height l) (max (height m) (max (height n) (height r))))"
    33 
    34 instance ..
    35 
    36 end
    37 
    38 text{* Balanced: *}
    39 fun bal :: "'a tree234 \<Rightarrow> bool" where
    40 "bal Leaf = True" |
    41 "bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    42 "bal (Node3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" |
    43 "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)"
    44 
    45 end