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