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