Re: [isabelle] Pending sort hypotheses

On Mon, 2 Jul 2012, Henri DEBRAT wrote:

Anyway, that is not so magic. It does not fully solve my issue: in the end, I discovered that a new goal had appeared in the "proof" block of the interpretation command. And guess what, this new goal is:

"SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"

So I am blocked again, even thought I could put an end to all other goals, which is already a little step forward.

OK, I was half suspecting that, but did not try your example. This is how you can establish these vacuous propositions as conclusions:

lemma "SORT_CONSTRAINT('a::ord)" unfolding sort_constraint_def .
lemma "SORT_CONSTRAINT('a::ord)" by (rule sort_constraintI)

The first form works, because it reveals the definition of this trick in terms of TERM/TYPE wrappers in Isabelle/Pure: a TERM proposition is always implicitly provable via ".", ie. "by this".

The second is the more explicit direct introduction. I am considering to make this a default intro in Pure, so that one could write ".." instead next time.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.