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

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.

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