[isabelle-dev] Pending sort hypotheses

[Brian Huffman]

On Wed, Jul 1, 2009 at 4:46 AM, Amine Chaieb<ac638 at cam.ac.uk> wrote:
> I wonder why this restriction has been introduced in the first place. Is
> it because sorts can be empty (i.e. there are no possible type
> 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

The above script fails at "qed" with a pending sort hypothesis error.

> For sorts with instances it should even be logically correct
> to eliminate such sorts constraints, when they are introduced
> exclusively during the proof.

When possible, they *are* removed during the proof as far as I can tell.

Here's an example of a proof that fails due to a pending sort hypothesis:

class nontrivial = assumes nontrivial: "EX x y. x ~= y"

lemma "True"
proof -
  obtain x y :: "'a::nontrivial" where "x ~= y"
    using nontrivial by auto
  then show "True" by simp
qed

Isabelle can't remove the [nontrivial] sort hypothesis because it
doesn't know whether or not class nontrivial has any instances.

But if we declare the following subclass relationship...

instance zero_neq_one < nontrivial
proof
  from zero_neq_one [where 'a='a]
  show "EX x y::'a. x ~= y" by blast
qed

...and run the above proof script again, then it will work. Since
Isabelle already knows there are instances of class zero_neq_one, now
it knows that class nontrivial is inhabited, and it can discharge the
sort hypothesis.

- Brian