Re: [isabelle] print_cases shows non-existing schematic variable

On Wed, 22 Apr 2015, Andreas Lochbihler wrote:

I guess that it should be fairly easy to implement your own method that does nothing but applying a rule and setting up the cases. The infrastructure should be all there.

Indeed. Proof methods can always produce cases as they see fit, cf. existing uses of METHOD_CASES and type cases_tactic. These things have been slightly tuned and cleaned up for Isabelle2015, as part of the integration of Eisbach.

Nonetheless, proof method definitions with cases are rare in practice. It requires some care and sometimes technical tricks to get material from the internal goal state into the proof text, without breaking down normal Isar principles of proof composition.

One example that is not from the "cases" and "induct" family is "eventually_elim" in ~~/src/HOL/Filter.thy (in Isabelle2015-RC1). It uses some basic tools to compose cases from module Rule_Cases, which is also the basis for the other cases methods.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.