*To*: grechukbogdan <grechukbogdan at yandex.ru>*Subject*: Re: [isabelle] Dependent types and existence of n-dimensional space.*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 12 May 2010 12:19:56 -0700*Cc*: isabelle-users at cl.cam.ac.uk, Johannes Hölzl <hoelzl at in.tum.de>*In-reply-to*: <171691273656081@web144.yandex.ru>*References*: <580921273596674@web127.yandex.ru> <1273651845.2263.50.camel@macbroy12.informatik.tu-muenchen.de> <171691273656081@web144.yandex.ru>*Sender*: huffman.brian.c at gmail.com

On Wed, May 12, 2010 at 2:21 AM, grechukbogdan <grechukbogdan at yandex.ru> wrote: > Dear Johannes > > Thank you for the responce. > >> Where do you get n from? If it is a fixed variable at the toplevel of >> your prove replace it by some finite type variable. If you get it via >> induction or similar it is probably not possible. > > Actually, I am proving lemma "Every convex nonempty set S has a nonempty relative interior", and n is the dimension of set S. > So, I would say that n is a fixed variable at the toplevel, no induction here or similar, I just have fixed set S and it has a fixed dimension. Can I use "some finite type variable"? But I cannot "assume "CARD('n :: finite) = n" inside the proof, in this case I have error when try to write "qed". Hi Bogdan, In this particular case, since "S" has a specific (finite) dimension that is fixed in advance, you should not need to resort to using the inf_vector type that I recommended in my previous email. You should be able to prove your lemma using only types like "real^'n". In order to help you more, I will need to know more details about the lemma you are trying to prove. I guess that "Every convex nonempty set S has a nonempty relative interior" would be formalized like lemma fixes S :: ??? obtains T :: ??? where <some formula of S and T> or "ALL S::???. EX T::???. <some formula of S and T>" In particular, I need to know the types of S and T, which would be in place of "???" above. > Also, my critical lemma > > fixes n :: nat obtains A where “A = (UNIV :: (real^'m) set)” and “dim A = n” My earlier advice applies here: Instead of trying to quantify over types, you need to rephrase this by quantifying over subspaces of a single fixed type. It seems like you are trying to say: "ALL n::nat. EX 'm. (dim (UNIV :: (real^'m) set)) = n" which is true, but nonsense in HOL because you can't quantify over types. Instead, you should be trying to prove something like this, where type 'm is fixed, and you quantify over subsets of real^'m: "ALL n::nat. n <= CARD('m) --> EX A::(real^'m) set. dim A = n" Again, it's hard to give more specific advice without knowing more details about what exactly you are trying to prove. - Brian

**Follow-Ups**:**Re: [isabelle] Dependent types and existence of n-dimensional space.***From:*grechukbogdan

**Re: [isabelle] Dependent types and existence of n-dimensional space.***From:*Timothy McKenzie

**References**:**[isabelle] Dependent types and existence of n-dimensional space.***From:*grechukbogdan

**Re: [isabelle] Dependent types and existence of n-dimensional space.***From:*Johannes Hölzl

**Re: [isabelle] Dependent types and existence of n-dimensional space.***From:*grechukbogdan

- Previous by Date: Re: [isabelle] how is one supposed to get !!x. p(x) from p(?x)
- Next by Date: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Previous by Thread: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Next by Thread: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Cl-isabelle-users May 2010 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