79 lines
2 KiB
Text
79 lines
2 KiB
Text
theory Tree
|
||
imports Main
|
||
begin
|
||
|
||
datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree"
|
||
|
||
definition example :: "int tree" where
|
||
"example =
|
||
Node
|
||
(Node
|
||
(Node
|
||
(Node Leaf 7 Leaf)
|
||
4
|
||
Leaf
|
||
)
|
||
2
|
||
(Node Leaf 5 Leaf)
|
||
)
|
||
1
|
||
(Node
|
||
(Node
|
||
(Node Leaf 8 Leaf)
|
||
6
|
||
(Node Leaf 9 Leaf)
|
||
)
|
||
3
|
||
Leaf
|
||
)"
|
||
|
||
fun preorder :: "'a tree ? 'a list" where
|
||
"preorder Leaf = []"
|
||
| "preorder (Node l a r) = a # preorder l @ preorder r"
|
||
|
||
lemma "preorder example = [1, 2, 4, 7, 5, 3, 6, 8, 9]" by code_simp
|
||
|
||
fun inorder :: "'a tree ? 'a list" where
|
||
"inorder Leaf = []"
|
||
| "inorder (Node l a r) = inorder l @ [a] @ inorder r"
|
||
|
||
lemma "inorder example = [7, 4, 2, 5, 1, 8, 6, 9, 3]" by code_simp
|
||
|
||
fun postorder :: "'a tree ? 'a list" where
|
||
"postorder Leaf = []"
|
||
| "postorder (Node l a r) = postorder l @ postorder r @ [a]"
|
||
|
||
lemma "postorder example = [7, 4, 5, 2, 8, 9, 6, 3, 1]" by code_simp
|
||
|
||
lemma
|
||
"set (inorder t) = set (preorder t)"
|
||
"set (preorder t) = set (postorder t)"
|
||
"set (inorder t) = set (postorder t)"
|
||
by(induction t, simp, simp)+
|
||
|
||
text‹
|
||
For a breadth first search, we will have a queue of the nodes we still
|
||
want to visit. The type of the queue is \<^typ>‹'a tree list›.
|
||
With each step, summing the sizes of the subtrees in the queue,
|
||
the queue gets smaller. Thus, the breadth first search terminates.
|
||
Isabelle cannot figure out this termination argument automatically,
|
||
so we provide some help by defining what the size of a tree is.
|
||
›
|
||
fun tree_size :: "'a tree ? nat" where
|
||
"tree_size Leaf = 1"
|
||
| "tree_size (Node l _ r) = 1 + tree_size l + tree_size r"
|
||
|
||
function (sequential) bfs :: "'a tree list ? 'a list" where
|
||
"bfs [] = []"
|
||
| "bfs (Leaf#q) = bfs q"
|
||
| "bfs ((Node l a r)#q) = a # bfs (q @ [l,r])"
|
||
by pat_completeness auto
|
||
termination bfs
|
||
by(relation "measure (?qs. sum_list (map tree_size qs))") simp+
|
||
|
||
fun levelorder :: "'a tree ? 'a list" where
|
||
"levelorder t = bfs [t]"
|
||
|
||
lemma "levelorder example = [1, 2, 3, 4, 5, 6, 7, 8, 9]" by code_simp
|
||
|
||
end
|