Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Custom case distinction rules with consider (I...

Email Gateway (Aug 22 2022 at 12:49):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 22 2022 at 12:49):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,

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

Last updated: Apr 25 2024 at 16:19 UTC