Inproceedings,
Iterative Circular Coinduction for CoCASL in Isabelle/HOL
Fundamental Approaches to Software Engineering 2005, volume 3442 of Lecture Notes in Computer Science, page 341-356. Springer; Berlin; http://www.springer.de, (2005)
Abstract
Coalgebra has in recent years been recognized as the framework of choice
for the treatment of reactive systems at an appropriate level of
generality. Proofs about the reactive behavior of a coalgebraic system
typically rely on the method of coinduction. In comparison to
`traditional' coinduction, which has the disadvantage of requiring the
invention of a bisimulation relation, the method of emphcircular
coinduction allows a higher degree of automation. As part of an effort
to provide proof support for the algebraic-coalgebraic specification
language textmdtextscCoCasl, we develop a new coinductive proof
strategy which iteratively constructs a bisimulation relation, thus
arriving at a new variant of circular coinduction. Based on this result,
we design and implement tactics for the theorem prover Isabelle which
allow for both automatic and semiautomatic coinductive proofs. The
flexibility of this approach is demonstrated by means of examples of
(semi-)automatic proofs of consequences of textmdtextscCoCasl
specifications, automatically translated into Isabelle theories by means
of the Bremen heterogeneous CASL tool set Hets.
