[isabelle] New AFP article: Generating Cases from Labeled Subgoals

Generating Cases from Labeled Subgoals
Lars Noschinski

Isabelle/Isar provides named cases to structure proofs. This article
contains an implementation of a proof method \texttt{casify}, which can
be used to easily extend proof tools with support for named cases. Such
a proof tool must produce labeled subgoals, which are then interpreted
by \texttt{casify}.

As examples, this work contains verification condition generators
producing named cases for three languages: The Hoare language from
\texttt{HOL/Library}, a monadic language for computations with failure
(inspired by the AutoCorres tool), and a language of conditional
expressions. These VCGs are demonstrated by a number of example programs.


Thank you, Lars!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature
