[isabelle-dev] Pending sort hypotheses
ac638 at cam.ac.uk
Thu Jul 2 01:39:10 CEST 2009
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
> 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
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