Why3 Standard Library index



Polymorphic binary trees with elements at nodes

theory Tree

  type tree 'a = Empty | Node (tree 'a) 'a (tree 'a)

end

theory Size "number of nodes"

  use import Tree
  use import int.Int

  function size (t: tree 'a) : int = match t with
    | Empty -> 0
    | Node l _ r -> 1 + size l + size r
  end

  lemma size_nonneg: forall t: tree 'a. 0 <= size t

  lemma size_empty: forall t: tree 'a. 0 = size t <-> t = Empty

end

theory Occ "occurrences in a binary tree"

  use import Tree
  use import int.Int

  function occ (x: 'a) (t: tree 'a) : int = match t with
    | Empty      -> 0
    | Node l y r -> (if y = x then 1 else 0) + occ x l + occ x r
  end

  lemma occ_nonneg:
    forall x: 'a, t: tree 'a. 0 <= occ x t

  predicate mem (x: 'a) (t: tree 'a) =
    0 < occ x t

end

theory Height "height of a tree"

  use import Tree
  use import int.Int
  use import int.MinMax

  function height (t: tree 'a) : int = match t with
    | Empty ->
        0
    | Node l _ r ->
        1 + max (height l) (height r)
  end

  lemma height_nonneg:
    forall t: tree 'a. 0 <= height t

end

theory Inorder "inorder traversal"

  use import Tree
  use import list.List
  use import list.Append

  function inorder (t: tree 'a) : list 'a = match t with
    | Empty -> Nil
    | Node l x r -> inorder l ++ Cons x (inorder r)
  end

end

theory Preorder "preorder traversal"

  use import Tree
  use import list.List
  use import list.Append

  function preorder (t: tree 'a) : list 'a = match t with
    | Empty -> Nil
    | Node l x r -> Cons x (preorder l ++ preorder r)
  end

end

theory InorderLength

  use import Tree
  use import Size
  use import Inorder
  use import list.List
  use import list.Length

  lemma inorder_length: forall t: tree 'a. length (inorder t) = size t

end

theory Zipper "Huet's zipper"

  use import Tree

  type zipper 'a =
    | Top
    | Left  (zipper 'a) 'a (tree 'a)
    | Right (tree 'a)   'a (zipper 'a)

  function zip (t: tree 'a) (z: zipper 'a) : tree 'a = match z with
    | Top -> t
    | Left z x r -> zip (Node t x r) z
    | Right l x z -> zip (Node l x t) z
  end

  (* navigating in a tree using a zipper *)

  type pointed 'a = (tree 'a, zipper 'a)

  function start (t: tree 'a) : pointed 'a = (t, Top)

  function up (p: pointed 'a) : pointed 'a = match p with
    | _, Top -> p (* do nothing *)
    | l, Left z x r | r, Right l x z -> (Node l x r, z)
  end

  function top (p: pointed 'a) : tree 'a = let t, z = p in zip t z

  function down_left (p: pointed 'a) : pointed 'a = match p with
    | Empty, _ -> p (* do nothing *)
    | Node l x r, z -> (l, Left z x r)
  end

  function down_right (p: pointed 'a) : pointed 'a = match p with
    | Empty, _ -> p (* do nothing *)
    | Node l x r, z -> (r, Right l x z)
  end

end

Generated by why3doc 0.87.3