Re: [isabelle] Unexpected assumptions in nested contexts



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

On 10/29/2012 06:13 AM, Lars Hupel wrote:
(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?








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