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