Time 
Nick 
Message 
14:54 

kaki joined #isabelle 
15:01 
kaki 
Hello! I'm trying to formalize the following definition in Isabelle: We call S a line segment iff there is a P \subset \mathbb{R}^2 such that P = 2 and S = {p*t+(1t)*q  t\in[0,1] and p,q \in P} 
15:05 
kaki 
I tried it with definition LineSegment :: "'a \<Rightarrow> bool" where "LineSegment S = (\<exists>P::(real*real) set. card P = 2 \<and> S = {x::(real*real). x = p*(t::real)+(1t)*q \<and> 0\<le>t \<and> t\<le>1 \<and> p\<in>P \<and> q\<in>P})" 
15:05 
kaki 
And Isabelle isn't accepting this Definition because of failing to meet type constraint 
15:06 
kaki 
I imported Complex_Main and did nothing else than this definition in this theory 
15:09 
kaki 
another question is, what package to import to have isabelle understand things like value "(3::real,2::real)*3::real" 
15:09 
kaki 
that means, vector calculations, scalar multiplications 
16:46 

mekeor joined #isabelle 