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