*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Pending sort hypotheses*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 04 Jul 2012 14:27:28 +0200*In-reply-to*: <1341395647.1962.18.camel@macbroy12.informatik.tu-muenchen.de>*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> <1341395647.1962.18.camel@macbroy12.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:8.0) Gecko/20120104 Icedove/8.0

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.

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)"

lemma Y:

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

-- Lars

**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

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

- Previous by Date: [isabelle] ADG 2012: Call for Papers (Extended Deadline: 8 July 2012)
- Next by Date: Re: [isabelle] Pending sort hypotheses
- 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