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:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and