# Re: [isabelle] Pending sort hypotheses

```On 04.07.2012 11:54, Johannes Hölzl wrote:
```
```Am Mittwoch, den 04.07.2012, 11:34 +0200 schrieb Lars Noschinski:
```
```
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?

```
```real_normed_vector includes open_dist, which together with finite
forces it to be a discrete topology, i.e. "!!x. open {x}".
The opposite of a perfect space "!!x. ~ open {x}".

However, I have now idea how blast can deduce False by itself. I don't
think there is any theorem in the library which relates finite with
topology.
```
```
```
I had now a look in the proof terms. One can see, that this proof uses in particular the following three theorems:
```
not_bounded_univ:
"¬bounded (UNIV :: ('a :: {perfect_space,real_normed_vector})  set)"

finite_imp_bounded:
"finite (S :: ('a :: metric_space) set) ⟹ bounded S"

finite_UNIV:
"finite (UNIV :: ('a :: finite) set)"

```
If there existed a type 'a satisfying these four sorts, we could prove false (a real_normed_vector is in particular a metric space, so we only need to mention three sorts explicitly):
```
lemma Y:
```
assumes S: "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector})"
```  shows False
proof -
from finite_UNIV have "bounded (UNIV :: 'a set)"
by (rule finite_imp_bounded)
moreover have "¬bounded (UNIV :: 'a set)"
by (rule not_bounded_UNIV)
ultimately show False by metis
qed

```
So, blast did not really find a proof for you, it just gave you an error message which might lead you into thinking it found a proof.
```
-- Lars

```

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