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