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



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.)

  { fix x :: "('v + 'v) option"
    consider "x = None" | y where "x = Some (Inl y)" | y where "x = Some
    (Inr y)"
      by pat_completeness }
  note Î_cases = this[case_names None Inl Inr]

Is there any way write this more nicely? I'd like to (in increasing importance)
(i) using note to give a name to the rule andblock
(ii) avoid the boilerplate with opening a proof
(iii) declaring the case names with the cases in consider.

Compact eigen-context notation is nice for small things, but it still needs to be seen how far it can be stretched, before it all becomes a bit odd. Note that the quasi-disjunction form binds weakly, so a 'for' behind it would refer to each case individually.

The case names can be declared with round parentheses as usual (like in 'obtains' or 'obtain'), but they get lost in the export of the proof block { ... }. In full generality, export operations can disrupt the meaning of such "tags", so they are usually not preserved.


	Makarius


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