Insertion in sorted tree

  • fully automatic

    module Bintree_insert
    
      use import bintree.Tree
      use import bintree.Size
      use import bintree.Inorder
      use import bintree.InorderLength
      use import int.Int
    (*-------------------------------*)
    
      function num_occ (x: 'a) (l: tree 'a) : int =
        match l with
        | Empty -> 0
        | Node t1 y t2 -> (if x = y then 1 else 0) + num_occ x t1 + num_occ x t2
       end
    
    (*-------------------------------*)
    
      let rec add (t : tree int) (v : int) : tree int =
        ensures {forall x : int. num_occ x result =
                 if x = v then 1 + num_occ x t else num_occ x t }
        match t with
         | Empty -> Node (Empty) v (Empty)
         | Node t1 x t2 ->
           if v <= x then Node (add t1 v) x t2 else Node t1 x (add t2 v)
        end
    
    end
    

  • Generated by why3doc 0.85