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