*To*: grechukbogdan <grechukbogdan at yandex.ru>*Subject*: Re: [isabelle] Dependent types and existence of n-dimensional space.*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Wed, 12 May 2010 10:10:45 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <580921273596674@web127.yandex.ru>*Organization*: Technische Universität München*References*: <580921273596674@web127.yandex.ru>

Hi Bogdan, Am Dienstag, den 11.05.2010, 20:51 +0400 schrieb grechukbogdan: > Dear Isabelle Users > > I know that dependent types do not exist in Isabelle. But there > should be some alternative way to express any (simple) mathematical > fact, should not it? I really need the following lemma. > > Lemma. Fix natural number n. Then there exist a n-dimensional real > vector space R^n [..] It works as long as _the type 'n_ is fixed: fix n :: nat assume "CARD('n :: finite) = n" moreover def "A == UNIV :: (real^'n) set" ultimately have "dim A = n" using dim_univ[where 'n='n] by simp What you can't do is to _obtain a type_, i.e. you can not say to obtain a 'm with CARD('m) = n. You need always to formulate it the other way round: i.e. n = CARD('m) when 'm is fixed. > But now I need to obtain a n-dimensional universe without additional assumptions. Can somebody help me? 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. > P. S. I hope this is possible. Otherwise how we can hope to formalize significant part of mathematics if we > cannot prove such a simple fact? This is an unfortunate side effect of the formalization of finite cartesian products in HOL-Multivariate_Analysis. However this is probably the only sensible formalization possible in HOL. Otherwise all the advantages of having types is lost and we could also work in ZF. - Johannes > Sincerely, > Bogdan Grechuk.

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

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

- Previous by Date: [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: [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