Re: [isabelle] Unexpected assumptions in nested contexts



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

Am 28.10.2012 22:13, schrieb 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?



--
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.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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