[isabelle-dev] Pending sort hypotheses

[Amine Chaieb]

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 :) :)

Amine.