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



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

This fact is absolutely obvious, and it is crucial for my formalization.
In Isabelle, for, say, n=100,  I can easily obtain 100-dimensional space by writing

have “CARD(100)=100” by auto
from this obtain A where “A = (UNIV :: (real^100) set)” and “dim A = 100”  by (simp add: dim_univ)

But I need this for general n. I can write

fix n :: nat
assume “CARD('m :: finite)=n”
from this obtain A where “A = (UNIV :: (real^'m) set)” and “dim A = n”  by (simp add: dim_univ)

But now I need to obtain a n-dimensional universe without additional assumptions. Can somebody help me?

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? 

Sincerely,
Bogdan Grechuk.





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