Re: [isabelle] Pending sort hypotheses

> On Sun, 1 Jul 2012, Henri.Debrat at wrote:
>> Ok, I solved my problem all by myself :-)
>> Just in case it might be useful to someone, here is the solution:
>> interpretation rs:product_prob_space "(λi. bernoulli bp)" "UNIV::(nat × Proc) set"
>> where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
>> proof [...]
> I am impressed.  How did you figure that out?
> The pro-forma proposition "SORT_CONSTRAINT('a::sort)" is indeed the way to help out in situations where certain sort occurrences in a proof need to be specified statically in the result, to avoid the "Pending sort hypotheses" problem.
> This vacous proposition is later stripped away in the HHF normalization of Isabelle rule statements.  So it does its job of introducing sorts formally, without changing the result.  It occurs in are situations as 'assumes' in the standard collection of Isabelle applications shipped with the release.
> 	Makarius


Well, I used the grep command to discover the word "sort" in the Isabelle directory : doing this, I discovered some lemmas had "assumes SORT_CONSTRAINT" in their header.
Then I have seen in the old isar-ref.pdf file that interpretation could take an optional "where" clause...and I tried to mix up the whole thing ! Kind of a dirty method, I admit.

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.

By the way, I do not know what  "HHF normalization" stands for so I do not really understand what's happening here.

Thanks a lot for your help !

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