Re: [isabelle] ind_cases appears to ignore chained facts
On Thu, 16 Apr 2015, Lars Hupel wrote:
I shall take another look for the coming release, if the move can be
continued, and old behaviours discontinued without too much effort.
I have just attempted to perform this change. Turns out, a lot of proofs
actually break (I did not investigate the failures). So, I guess this
would not qualify as a "minor" change wrt to the approaching release.
It is normal that any attempt to change anything does not work out by
default. This is why I make all these jokes about "bugs" and "fixes"
here. Without special precautions, a change usually makes the situation
worse than before.
I had one round of looking at ind_cases some weeks ago, made some tiny
reforms, and then got stuck with more fundamental questions what the whole
purpose of ind_cases actually is. (I did not try to answer this question,
and merely put it on my TODO list.)
Since Isabelle2015-RC0 has already 'private' (or 'qualified')
declarations, one could try the canonical pattern for proof-local
specifications like that and thus avoid ind_cases:
private inductive_cases my_cases: ...
lemma ... by (cases rule: my_cases)
Note that 'private' only affects the name space. So if rules are declared
(e.g. as [elim]) in the local context, they will be outside as well.
The new 'experiment' target prevents this by wrapping a locale around the
whole block. But here the very point is to export nothing from it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and