# Re: [isabelle] Pending sort hypotheses

On 03.07.2012 18:53, Henri DEBRAT wrote:

Yet, some great mystery lies here concerning sort_constraint and the exception it raises.
In case it might be an interesting issue to solve, I copy here two piece of code.

`The first proof does not go through for me (Isabelle 2012) -- the proof
``of obtains in the 3rd block fails and there is some remaining goal.
`

definition
"bernoulli ≡ point_measure (UNIV :: bool set) (% True => ereal bp | False => 1 - ereal bp)"

[...]

interpretation rs:product_prob_space "(λi::nat × Proc. bernoulli)" "UNIV::(nat × Proc) set"
where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
proof(unfold_locales, auto)
have "UNIV = { True, False }" by auto
thus "emeasure bernoulli (space bernoulli) = 1"
using space_point_measure finite_UNIV
by (blast dest:emeasure_point_measure_finite)

`This looks already a bit suspicious -- you proof something about
``bernoulli without ever using its definition (definitions are not
``unfolded automatically). Indeed it turns out, that you can prove False here:
`

`interpretation rs:product_prob_space "(λi::nat × Proc. bernoulli)"
``"UNIV::(nat × Proc) set"
`where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
proof(unfold_locales, auto)
have A: "UNIV = { True, False }" by auto
then have False using finite_UNIV
by (blast dest:emeasure_point_measure_finite)

`This means, you assumptions are inconsistent. The SORT_CONSTRAINT you
``gave adds the assumption, that there exists a type, which is finite, a
``perfect_space, and a real_normed_vector. I guess such a type does not
``exist -- maybe somebody more familiar with this field can confirm this?
`

`These sort constraints are necessary to keep the system consistent, when
``type variables vanish from a term: If you have a type class c with
``inconsistent assumptions, then you can easily derive False from it. But
``the term False does not contain references to c anymore. Hence, Isabelle
``attaches the additional sort constraint "c" to this theorem. This
``basically encodes "If the type class c is not empty, then this theorem
``holds". If there is already an instance of this class, the additional
``sort constraint is automatically discharged.
`

`So, in your case, somehow blast is able to find a proof which basically
``runs into above situation -- i.e., it is not really a proof.
`
-- Lars

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