\t -> decomposetree t
===[unfold + simplification (step 1)
\t ->
some
(\xs ->
heapinv t &&
issorted xs && equals (elementsof xs) (abstraction t)
)
===[case introduction (step 2)
\t ->
case t of
Leaf ->
some
(\xs ->
heapinv Leaf &&
issorted xs &&
equals (elementsof xs) (abstraction Leaf)
)
Node a b c ->
some
(\xs ->
heapinv (Node a b c) &&
issorted xs &&
equals (elementsof xs) (abstraction (Node a b c))
)
===[tactic solve (step 3)
\t ->
case t of
Leaf ->
some
(\xs -> issorted xs && equals (elementsof xs) emptybag
)
Node a b c ->
some
(\xs ->
heapinv (Node a b c) &&
issorted xs &&
equals (elementsof xs) (abstraction (Node a b c))
)
===[apply rule sort-derived.thy/some_sorted_equals_elements_empty (step 4)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\xs ->
heapinv (Node a b c) &&
issorted xs &&
equals (elementsof xs) (abstraction (Node a b c))
)
===[case introduction (step 5)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\xs ->
case xs of
[] ->
heapinv (Node a b c) &&
issorted [] &&
equals (elementsof [])
(abstraction (Node a b c))
x : d ->
heapinv (Node a b c) &&
issorted (x : d) &&
equals (elementsof (x : d))
(abstraction (Node a b c))
)
===[tactic solve (step 6)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\xs ->
case xs of
[] ->
heapinv (Node a b c) &&
equals emptybag
(unionbag
(unionbag (abstraction a) (singletonbag b))
(abstraction c)
)
x : d ->
heapinv (Node a b c) &&
issorted (x : d) &&
equals (elementsof (x : d))
(abstraction (Node a b c))
)
===[apply catalog bag-derived.thy + simplification (step 7)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\xs ->
case xs of
[] -> False
x : d ->
heapinv (Node a b c) &&
issorted (x : d) &&
equals (elementsof (x : d))
(abstraction (Node a b c))
)
===[apply rule sort-derived.thy/heap_sorted_equals_elements_abstr (step 8)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\xs ->
case xs of
[] -> False
x : d ->
x == b &&
heapinv (Node a b c) &&
issorted d &&
equals (elementsof d)
(abstraction (removemin (Node a b c)))
)
===[tactic Simplify with Flat (step 9)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\(x : d) ->
x == b &&
heapinv (Node a b c) &&
issorted d &&
equals (elementsof d)
(abstraction (removemin (Node a b c)))
)
===[abstract (step 10)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\(x : d) ->
(\e -> e == b) x &&
heapinv (Node a b c) &&
issorted d &&
equals (elementsof d)
(abstraction (removemin (Node a b c)))
)
===[abstract (step 11)
\t ->
case t of
Leaf -> []
Node a b c ->
some
(\(x : d) ->
(\e -> e == b) x &&
(\f ->
heapinv (Node a b c) &&
issorted f &&
equals (elementsof f)
(abstraction (removemin (Node a b c)))
)
d
)
===[apply rule general.thy/some_split + simplification (step 12)
\t ->
case t of
Leaf -> []
Node a b c ->
b :
some
(\f ->
heapinv (Node a b c) &&
issorted f &&
equals (elementsof f)
(abstraction (removemin (Node a b c)))
)
===[apply rule sort-derived.thy/heap_removemin backwards (step 13)
\t ->
case t of
Leaf -> []
Node a b c ->
b :
some
(\f ->
(heapinv (Node a b c) &&
heapinv (removemin (Node a b c))
) &&
issorted f &&
equals (elementsof f)
(abstraction (removemin (Node a b c)))
)
===[use assoc/comm (step 14)
\t ->
case t of
Leaf -> []
Node a b c ->
b :
some
(\f ->
heapinv (Node a b c) &&
heapinv (removemin (Node a b c)) &&
issorted f &&
equals (elementsof f)
(abstraction (removemin (Node a b c)))
)
===[abstract (step 15)
\t ->
case t of
Leaf -> []
Node a b c ->
b :
some
(\f ->
heapinv (Node a b c) &&
(\d ->
heapinv (removemin (Node a b c)) &&
issorted d &&
equals (elementsof d)
(abstraction (removemin (Node a b c)))
)
f
)
=>=[apply rule general.thy/some_eliminate_assertion + simplification (step 16)
\t ->
case t of
Leaf -> []
Node a b c ->
b :
some
(\d ->
heapinv (removemin (Node a b c)) &&
issorted d &&
equals (elementsof d)
(abstraction (removemin (Node a b c)))
)
===[fold (step 17)
\t ->
case t of
Leaf -> []
Node a b c -> b : decomposetree (removemin (Node a b c))