Re: [isabelle] Custom case distinction rules with consider (Isabelle2016-RC3)



Dear Makarius,

On 04/02/16 22:26, Makarius wrote:
On Thu, 4 Feb 2016, Andreas Lochbihler wrote:

I will only need them inside this particular lemma, so it makes sense to prove them there.

How about using "context begin ... end" around the lemma, and establish the rule as
"private lemma Î_cases: fixes x obtains ..." before it? (Minor disadvantage: the internal
full name still needs to be unique, because I did not manage to revisit that open question
from the last release.)
Indeed, this is a nice possibility for the given lemma and works in most of my cases. In a few, however, it fails, because some cases also include locally fixed parameters, as in

  fix a
  { fix x
    consider "x = Some a" | y where "x = Some y" "y ~= a" | "x = None" ... }

I also noticed the problem with unique full names when I tried to stretch private a bit too far in my theory. But that's another story.

Cheers,
Andreas




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