[isabelle-dev] Pending sort hypotheses
Brian Huffman
brianh at cs.pdx.edu
Thu Jul 2 00:19:58 CEST 2009
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
More information about the isabelle-dev
mailing list