Re: [isabelle] Pending sort hypotheses



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.

 - Johannes






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