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--
```     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
```