Generating Cases from Labeled Subgoals

Title:	Generating Cases from Labeled Subgoals
Author:	Lars Noschinski
Submission date:	2015-07-21
Abstract:	Isabelle/Isar provides named cases to structure proofs. This article contains an implementation of a proof method `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 `casify`. As examples, this work contains verification condition generators producing named cases for three languages: The Hoare language from `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.
BibTeX:	@article{Case_Labeling-AFP, author = {Lars Noschinski}, title = {Generating Cases from Labeled Subgoals}, journal = {Archive of Formal Proofs}, month = jul, year = 2015, note = {\url{http://isa-afp.org/entries/Case_Labeling.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Planarity_Certificates
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.