[isabelle-dev] Pending sort hypotheses

Amine Chaieb ac638 at cam.ac.uk
Thu Jul 2 01:39:10 CEST 2009

Hi Brian,

Many thanks for the explanation. Indeed, if I make Abstract_Rat import
say Complex_Main, the proofs work without the sort assumption. This must
be due to the fact that concrete instances of field (I think) come only
after Main.

> That's exactly right. Theorems need to have sort hypotheses to prevent
> proofs like this:
> class impossible =
>   assumes impossible: "EX x. x ~= x"
> lemma False: "False"
> proof -
>   obtain x :: "'a::impossible" where "x ~= x"
>     using impossible ..
>   then show "False" by simp
> qed

I have nothing against proofs like this one, but I agree that it is a
matter of taste. I would not like to dive into a discussion if this good
or bad :) :)


More information about the isabelle-dev mailing list