-- ********
--! FUNS
-- ********

-- The function composetree is defined in step 6 of the derivation of
-- the rule introduce_composetree.

composetree :: [a] -> Tree a
composetree xs = some (\t -> heapinv t && elementsof xs `equals` abstraction t)

-- The function insert is defined in step 13 of the derivation of
-- the rule composetree_recursive.

insert :: a -> Tree a -> Tree a
insert x t = some (\s -> heapinv t && heapinv s &&
  nonemptybag x (abstraction t) `equals` abstraction s)

-- ********
--! RULES
-- ********

equals_abstr_some_heap_equals_abstr b =
  []
  |=
  b `equals` (abstraction (some (\t -> heapinv t && b `equals` abstraction t)))
  <=>
  True

introduce_composetree b xs =
  []
  |=
  b `equals` elementsof xs
  <=>
  b `equals` abstraction (composetree xs)

heap_composetree xs =
  []
  |=
  heapinv (composetree xs)
  <=>
  True

some_heap_equals_empty_abstr =
  []
  |=
  some (\t -> heapinv t && emptybag `equals` abstraction t)
  <=>
  Leaf

composetree_recursive xs =
  []
  |=
  composetree xs
  <=>
  case xs of
    [] -> Leaf
    y : ys -> insert y (composetree ys)

equals_empty_union_abstr_abstr l r =
  []
  |=
  emptybag `equals` (abstraction l `unionbag` abstraction r)
  <=>
  case l of
    Leaf -> case r of
              Leaf -> True
              Node d e f -> False
    Node b e c -> False

some_heap_equals_nonempty_abstr e =
  []
  |=
  some (\t -> heapinv t && nonemptybag e emptybag `equals` abstraction t)
  <=>
  Node Leaf e Leaf

heap_equals_nonempty_abstr_abstr_insert e t =
  []
  |=
  heapinv t && nonemptybag e (abstraction t) `equals` abstraction (insert e t)
  <=>
  heapinv t

heap_equals_union_union_single_abstr b1 b2 e t =
  []
  |=
  heapinv t && b1 `equals` (b2 `unionbag` (singletonbag e `unionbag` abstraction t))
  <=>
  heapinv t && b1 `equals` (b2 `unionbag` abstraction (insert e t))

some_heap_insert_1 e l r x =
  []
  |=
  some (\s -> (heapinv (Node l e r) && heapinv (Node (insert x r) e l)) &&
               heapinv s && abstraction s `equals` (abstraction l `unionbag`
               singletonbag e `unionbag` singletonbag x `unionbag` abstraction r))
  ==>
  Node (insert x r) e l

some_heap_insert_2 e l r x =
  []
  |=
  some (\s -> (heapinv (Node l e r) && heapinv (Node (insert e r) x l)) &&
               heapinv s && abstraction s `equals` (abstraction l `unionbag`
               singletonbag e `unionbag` singletonbag x `unionbag` abstraction r))
  ==>
  Node (insert e r) x l

insert_recursive x t =
  []
  |=
  insert x t
  ==>
  case t of
    Leaf -> Node Leaf x Leaf
    Node l e r -> if e <= x then Node (insert x r) e l
                            else Node (insert e r) x l

some_heap_equals_union_empty_abstr e r =
  []
  |=
  some (\t -> heapinv (Node Leaf e r) && heapinv t &&
    (abstraction Leaf `unionbag` abstraction r) `equals` abstraction t)
  ==>
  r

some_heap_equals_union_abstr_empty e1 e2 l r =
  []
  |=
  some (\t -> heapinv (Node (Node l e1 r) e2 Leaf) && heapinv t &&
    (abstraction (Node l e1 r) `unionbag` abstraction Leaf) `equals` abstraction t)
  ==>
  Node l e1 r

-- ********
--! CLAUSES
-- ********