author | nipkow |
Sun, 18 Oct 2015 17:25:13 +0200 | |
changeset 61469 | cd82b1023932 |
child 61640 | 44c9198f210c |
permissions | -rw-r--r-- |
61469
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow *) |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
2 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
3 |
section \<open>2-3 Trees\<close> |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
4 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
5 |
theory Tree23 |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
6 |
imports Main |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
7 |
begin |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
8 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
9 |
class height = |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
10 |
fixes height :: "'a \<Rightarrow> nat" |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
11 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
12 |
datatype 'a tree23 = |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
13 |
Leaf | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
14 |
Node2 "'a tree23" 'a "'a tree23" | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
15 |
Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
16 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
17 |
fun inorder :: "'a tree23 \<Rightarrow> 'a list" where |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
18 |
"inorder Leaf = []" | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
19 |
"inorder(Node2 l a r) = inorder l @ a # inorder r" | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
20 |
"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
21 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
22 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
23 |
instantiation tree23 :: (type)height |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
24 |
begin |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
25 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
26 |
fun height_tree23 :: "'a tree23 \<Rightarrow> nat" where |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
27 |
"height Leaf = 0" | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
28 |
"height (Node2 l _ r) = Suc(max (height l) (height r))" | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
29 |
"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
30 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
31 |
instance .. |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
32 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
33 |
end |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
34 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
35 |
text \<open>Balanced:\<close> |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
36 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
37 |
fun bal :: "'a tree23 \<Rightarrow> bool" where |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
38 |
"bal Leaf = True" | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
39 |
"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" | |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
40 |
"bal (Node3 l _ m _ r) = |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
41 |
(bal l & bal m & bal r & height l = height m & height m = height r)" |
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
42 |
|
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
diff
changeset
|
43 |
end |