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.
> 
> 
> 	Makarius


Thanks a lot for your help, Makarius.

Unfolding the definition...Hum, I feel a little silly here...

Your solution works...partially. That is, it solves the sort_contraint goal. However, when closing the proof block, here is the error I get :


 exception TERM raised (line 137 of "more_thm.ML"):
dest_equals
SORT_CONSTRAINT(?'a∷{finite,perfect_space,real_normed_vector}) 

any idea ?

H.






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