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:

context
begin

private inductive_cases my_cases: ...

lemma ... by (cases rule: my_cases)

end


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.


	Makarius




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