OrderedTree.fst

module OrderedTree

type elem = int

type tree =
  | Leaf
  | Node of (tree * elem * tree)

let rec all_tree pred t =
  match t with
  | Leaf -> True
  | Node (left, x, right) ->
  pred x /\
  all_tree pred left /\
  all_tree pred right

let all_le x t = all_tree (fun e -> e <= x) t
let all_ge x t = all_tree (fun e -> x <= e) t

let rec ordered t =
  match t with
  | Leaf -> True
  | Node (left, x, right) ->
  ordered left /\
  ordered right /\
  all_le x left /\
  all_ge x right

let rec insert x t =
  match t with
  | Leaf -> Node (Leaf, x, Leaf)
  | Node (left, y, right) ->
    begin match x <= y with
    | true  -> Node (insert x left, y, right)
    | false -> Node (left, y, insert x right)
    end

let rec all_insert pred x t :
  Lemma (requires (all_tree pred t /\ pred x)) (ensures (all_tree pred (insert x t))) =
  match t with
  | Leaf -> ()
  | Node (left, y, right) ->
    begin match x <= y with
    | true  -> all_insert pred x left
    | false -> all_insert pred x right
    end

let all_insert_le y x t :
  Lemma (requires (all_le y t /\ x <= y))
        (ensures (all_le y (insert x t)))
  = (all_insert (fun e -> e <= y) x t)

let all_insert_ge y x t :
  Lemma (requires (all_ge y t /\ y <= x))
        (ensures (all_ge y (insert x t)))
  = (all_insert (fun e -> y <= e) x t)

let rec insert_ordered x t :
  Lemma (requires (ordered t))
        (ensures (ordered (insert x t))) (decreases t) =
  match t with
  | Leaf -> ()
  | Node (left, y, right) ->
    begin match x <= y with
    | true  ->
       insert_ordered x left;
       all_insert_le y x left
    | false ->
       insert_ordered x right;
       all_insert_ge y x right
    end