[isabelle-dev] Pending sort hypotheses

[Makarius]

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 
instances.


>> 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.

Do you mean you want to be able to prove False unconditionally?


 	Makarius