\xs -> composetree xs
===[unfold + simplification (step 1)
\xs ->
some
(\t ->
heapinv t && equals (elementsof xs) (abstraction t)
)
===[unfold + simplification (step 2)
\xs ->
some
(\t ->
heapinv t &&
equals
(case xs of
[] -> emptybag
x : b -> nonemptybag x (elementsof b)
)
(abstraction t)
)
===[tactic simplify (step 3)
\xs ->
case xs of
[] ->
some
(\t -> heapinv t && equals emptybag (abstraction t))
x : b ->
some
(\t ->
heapinv t &&
equals (nonemptybag x (elementsof b))
(abstraction t)
)
===[apply rule tree-derived.thy/some_heap_equals_empty_abstr (step 4)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
heapinv t &&
equals (nonemptybag x (elementsof b))
(abstraction t)
)
===[apply rule bag.thy/bag_equals (step 5)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
heapinv t &&
elembag x (abstraction t) &&
equals (elementsof b) (without (abstraction t) x)
)
===[apply rule general.thy/commutativity (step 6)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
heapinv t &&
elembag x (abstraction t) &&
equals (without (abstraction t) x) (elementsof b)
)
===[apply rule tree-derived.thy/introduce_composetree (step 7)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
heapinv t &&
elembag x (abstraction t) &&
equals (without (abstraction t) x)
(abstraction (composetree b))
)
===[apply rule general.thy/commutativity (step 8)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
heapinv t &&
elembag x (abstraction t) &&
equals (abstraction (composetree b))
(without (abstraction t) x)
)
===[apply rule bag.thy/bag_equals backwards (step 9)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
heapinv t &&
equals
(nonemptybag x (abstraction (composetree b)))
(abstraction t)
)
===[apply rule general.thy/left_neutral (step 10)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
True &&
heapinv t &&
equals
(nonemptybag x (abstraction (composetree b)))
(abstraction t)
)
===[apply rule tree-derived.thy/heap_composetree backwards (step 11)
\xs ->
case xs of
[] -> Leaf
x : b ->
some
(\t ->
heapinv (composetree b) &&
heapinv t &&
equals
(nonemptybag x (abstraction (composetree b)))
(abstraction t)
)
===[abstract (step 12)
\xs ->
case xs of
[] -> Leaf
x : b ->
(\a ->
some
(\t ->
heapinv a &&
heapinv t &&
equals (nonemptybag x (abstraction a))
(abstraction t)
)
)
(composetree b)
===[fold (step 13)
\xs ->
case xs of
[] -> Leaf
x : b -> insert x (composetree b)