Re: [isabelle] Unexpected assumptions in nested contexts



On 13.06.2012 17:02, Lars Hupel wrote:
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.

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





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