Email Gateway (Aug 19 2022 at 17:23): Email Gateway (Aug 19 2022 at 17:23):From: Lars Hupel <hupel@in.tum.de>
It appears that the 'ind_cases' method, which is supposed to produce an
elimination rule on the fly and immediately apply it to the goal state,
does not take chained facts into account. Consider this small-ish example:
inductive app :: "'a list ⇒ 'a list ⇒ 'a list ⇒ bool" where
"app [] ys ys" |
"app xs ys zs ⟹ app (x # xs) ys (x # zs)"
notepad begin
fix xs ys zs :: "'a list" and x :: 'a
assume "app (x # xs) ys zs"
then obtain zs' where "zs = x # zs'"
apply - (* remove this and 'ind_cases' fails *)
apply (ind_cases "app (x # xs) ys zs")
apply auto
done
end
Same happens when I declare
inductive_cases foo: "app (x # xs) ys zs"
outside and use 'apply (erule foo)'. OTOH, both 'apply (rule foo)' and
'apply (elim foo)' do consume the chained facts. Looking closely at the
reference manual (§§6.2.3, 6.3.3) explains the behaviour of 'rule'
(namely, perform elimination under presence of chained facts). Still,
this does not explain why 'ind_cases' ignores chained facts. There's an
old thread [0] on this list about a related topic, but I couldn't find
an explanation there either.
Cheers
Lars
[0]
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-April/msg00002.html>
Email Gateway (Aug 19 2022 at 17:23):From: Lars Hupel <hupel@in.tum.de>
After some discussion with Lars, this question reduced to: Why does
'ind_cases' internally call 'Method.erule' instead of 'Method.rule' (or
even 'eresolve_tac')?
Email Gateway (Aug 19 2022 at 17:30):From: Makarius <makarius@sketis.net>
It is mainly historic: inductive_cases and ind_cases were never quite sure
if they belong to proper Isar or to old stuff. Things in this area have
slowly moved towards proper Isar-ness over the years.
I shall take another look for the coming release, if the move can be
continued, and old behaviours discontinued without too much effort.
Makarius
Email Gateway (Aug 22 2022 at 09:13):From: Lars Hupel <hupel@in.tum.de>
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.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:13):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 20 2024 at 12:26 UTC