[isabelle-dev] Pending sort hypotheses
makarius at sketis.net
Thu Jul 2 13:17:33 CEST 2009
On Thu, 2 Jul 2009, Amine Chaieb wrote:
> 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.
The proofs in Abstract_Rat implicitly depend on *some* actual instances of
the abstract structure being around. By including suitable concrete
versions, the implicit "strip_shyps" mechanism of Isabelle/Pure will
remove redundant constraints.
The SORT_CONSTRAINT notation explained in the NEWS/manuals of Isabelle2009
allows to state extraneous sort assumptions explicitly, so one can do this
kind of pseudo-abstract reasoning without relying on accidental concrete
>> 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.
Do you mean you want to be able to prove False unconditionally?
More information about the isabelle-dev