# 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{https://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.