80 lines
2 KiB
Text
80 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
|