Email Gateway (Aug 18 2022 at 20:23): Email Gateway (Aug 18 2022 at 20:23):From: Lars Hupel <hupel@in.tum.de>
Nesting two contexts, where the inner context makes assumptions about
fixed variables from the outer context, results in unexpected
all-quantified assumptions. Consider this minimal example:
context
fixes I :: "'a set"
begin
context
assumes I: "finite I"
begin
lemma test: "something_about I"
sorry
end
end
Looking at the fact test from outside both contexts with thm test, I
get:
(!!I. finite I) ==> ?something_about ?I [!]
Obviously, this fact says something completely different. Am I doing
something wrong here?
(Also, what does the [!] mean after the fact?)
Email Gateway (Aug 18 2022 at 20:23):From: Lars Noschinski <noschinl@in.tum.de>
This means that this theorem is not really proven (in most cases this
means, that you used "sorry", as you did above).
Email Gateway (Aug 18 2022 at 20:24):From: Lars Noschinski <noschinl@in.tum.de>
This issue arises already after leaving the inner context:
context
fixes I :: "'a set" assumes nonempty: "I ≠ {}"
begin
context
assumes I: "finite I"
begin
lemma card_neq_0: "card I ≠ 0" using I nonempty by auto
end
thm card_neq_0
This gives us "(⋀I. finite I) ⟹ card I ≠ 0 ", i.e. the I in the
assumption is generalized (but not the one in the conclusion). I first
assumed, the I in the inner context might be different from the one in
the outer context, but this is not the case as the "I ~= {}" can be used
in the inner context.
But I don't have any idea how these contexts work or are supposed to work.
-- Lars
Email Gateway (Aug 19 2022 at 08:53):From: Lars Hupel <hupel@in.tum.de>
(I already posted this several months ago, got no replies, and forgot
about it. I'm sending it again in case there's a solution/workaround
which I've missed. The original thread is at
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00052.html>.)
Nesting two contexts, where the inner context makes assumptions about
fixed variables from the outer context, results in unexpected
all-quantified assumptions. Consider this minimal example:
context
fixes I :: "'a set"
begin
context
assumes I: "finite I"
begin
lemma test: "something_about I"
sorry
end
end
Looking at the fact test from outside both contexts with thm test, I
get:
(!!I. finite I) ==> ?something_about ?I
Obviously, this fact says something completely different. Am I doing
something wrong here?
Email Gateway (Aug 19 2022 at 08:53):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Lars,
it seems that your message was at least considered, see
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-October/003308.html
Unfortunately that was not visible on the isabelle-users mailing list.
As far as I can tell (from looking at the development version of
Isabelle), the next Isabelle release will behave as expected on your
example, i.e., the result will be:
finite ?I ⟹ ?something_about ?I
cheers
chris
Email Gateway (Aug 19 2022 at 08:53):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Lars,
Makarius has already fixed this in the development branch, your example works
there. This will also work in the next Isabelle release as expected. For the
moment, you cannot do much about this in Isabelle2012. If you absolutely depend
on this working correct, you could try and switch to the development version,
but this incurs a lot of extra trouble.
Best,
Andreas
Last updated: Apr 18 2024 at 20:16 UTC