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



On 22.04.2015 10:50, Andreas Lochbihler wrote:
> Hi Lars,
>
> I don't know the design choices for cases, as I have not implemented
> them, but here are my comments: cases assumes that you give it a
> conventional case analysis rules. These rules do not change the
> conclusion, so cases has some point in not providing any term
> abbreviations for the conclusions. Anyway, you are trying to use
> sophisticated proof methods just to benefit from a certain side
> effect. I used to do that regularly, too (and sometimes still do, but
> much less).
>
> 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.
After looking at the code a bit I was wondering, how the cases method
manages to not declare the term bindings -- the term bindings are
present in the cases and I could not find an obvious flag or similar
which would hide the term bindings.

Does anybody know how this is achieved?

  -- Lars




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