[isabelle] Unexpected assumptions in nested contexts

[Lars Hupel]

(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?

[Christian Sternagel]

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

[Andreas Lochbihler]

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

--
Karlsruher Institut fï¿œr Technologie
IPD Snelting

Dr. Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.l...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universitï¿œt des Landes Baden-Wï¿œrttemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft