Re: [isabelle] Possible unsoundness in axclass mechanism



Tom,

On Wednesday 14 September 2005 18:36, Tom Ridge wrote:
> axclass blurg < type
>    blurg: "! x. x ~= x"

> lemma "False"
>    apply(rule l[of "x"])
>    apply(simp only: blurg)
>    apply(simp)
>    done

> Is this supposed to happen? I thought declaring an axclass was supposed to
> be a conservative extension.

You should see a warning "### Pending sort hypotheses: blurg" when proving 
"False" in the above way, meaning that the lemma only holds under the 
assumption that the type class blurg is non-empty.  There is a short 
discussion of this issue at the end of Section 8.3 of the Isabelle/HOL 
tutorial (http://isabelle.in.tum.de/dist/packages/Isabelle/doc/tutorial.pdf).

Best regards,
Tjark





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