Re: [isabelle] Pending sort hypotheses



On Sun, 1 Jul 2012, Henri.Debrat at loria.fr 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


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