*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] Pending sort hypotheses*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Wed, 04 Jul 2012 11:54:07 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FF40E43.6070304@in.tum.de>*Organization*: Technische Universität München*References*: <C889C598-FE01-49FD-8D17-50FEA8F7B266@loria.fr> <1341258546.2104.13.camel@vogelfrei> <B3EA1E91-10B2-4B0C-B254-DECEA5478DC5@loria.fr> <4FF40E43.6070304@in.tum.de>

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

**Follow-Ups**:**Re: [isabelle] Pending sort hypotheses***From:*Lars Noschinski

**References**:**Re: [isabelle] Pending sort hypotheses***From:*Johannes Hölzl

**Re: [isabelle] Pending sort hypotheses***From:*Henri DEBRAT

**Re: [isabelle] Pending sort hypotheses***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Pending sort hypotheses
- Next by Date: Re: [isabelle] Overriding reason not to use single quote or camelcase in identifiers?
- Previous by Thread: Re: [isabelle] Pending sort hypotheses
- Next by Thread: Re: [isabelle] Pending sort hypotheses
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list