Re: [isabelle] Dependent types and existence of n-dimensional space.
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]
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.
> Bogdan Grechuk.
This archive was generated by a fusion of
Pipermail (Mailman edition) and