Time 
Nick 
Message 
00:17 
Jafet 
isabelle ie. "I can't get no documentation" 
01:12 
Jafet 
http://hpaste.org/82658 
01:12 
Jafet 
That wasn't so bad, only 18 ambiguous parses 
02:03 
kaki 
I was trying to use built theories as much as i can 
02:05 
kaki 
but if there is no theory included into Isabelle2013 about vector spaces than I'll happily stay with your 18 ambiguous parses 
02:08 
kaki 
If they would work 
02:14 
kaki 
actually the problem still persist because isabelle doesnt accept this definition as it is 
02:15 
kaki 
to get away from those technical problems I'm trying to use built theories 
02:18 
Jafet 
% find Isabelle2012/src iname '*vector*' 
02:18 
Jafet 
Isabelle2012/src/HOL/Library/Product_Vector.thy 
02:18 
Jafet 
Isabelle2012/src/HOL/Library/ListVector.thy 
02:18 
Jafet 
Isabelle2012/src/HOL/RealVector.thy 
02:18 
Jafet 
Isabelle2012/src/HOL/Hahn_Banach/Vector_Space.thy 
02:28 
kaki 
Library/Product_vector looks promising 
02:28 
kaki 
im using isabelle2013 btw, i hope that makes no essential difference 
02:31 
kaki 
one thing that is strange to me, that you used the type "real*real" and in Product_Vector they use "'a x 'b" 
02:31 
Jafet 
I hope your font distinguishes × and x 
02:33 
kaki 
oh, thats tricky 
02:33 
kaki 
it does, but i didnt saw it 
02:33 
kaki 
so real*real is some kind of builtin logic of isabelle to declare a tuple 
02:34 
kaki 
and real \<times> real is the logic from Product_Vector 
02:36 
Jafet 
Both notations are defined in Product_Type 
02:36 
kaki 
but even though i use real \<times> real it doesn't know what to do with a multiplication of a vector from "real \<times> real" and a real 
02:38 
kaki 
I'm reading Product_Type.thy 
02:41 
Jafet 
You should define that notation, then. 
02:56 
kaki 
http://hpaste.org/82660 
02:56 
kaki 
so i did as i think you advised me, i just defined those notations 
02:57 
kaki 
beside that isabelle is complaining that input is ambiguous 
02:58 
kaki 
its just not not solving easy things by simp but also giving me an error when i try so 
02:58 
kaki 
i guess thats my mistake but i don't know how to solve it 
02:59 
kaki 
its not just not* 
02:59 
kaki 
a bit too late over here to stay concentrated 
03:02 
Jafet 
simp doesn't unfold Scale 
03:03 
kaki 
but apply (simp add:Scale) doesn't work either 
03:05 
Jafet 
It's called Scale_def 
03:07 
kaki 
okay, by (simp add:Scale_def RScale_def) proofes that lemma 
03:14 

kaki joined #isabelle 
03:31 
kaki 
thanks for your help so far 
03:33 
kaki 
there is one question left: is there a way to quantify over sets directly? 
03:33 
kaki 
I mean i could always write "\forall a. P a \and a \in M" 
03:34 
kaki 
but i think its more readable to write "\forall a \in M. P a" 
03:41 
Jafet 
Ok, so write that 
05:23 

inte joined #isabelle 
05:40 

lazard joined #isabelle 
11:39 

felipealmeida joined #isabelle 
13:00 

Jafet joined #isabelle 
13:22 

Jafet joined #isabelle 
16:09 

felipealmeida joined #isabelle 
16:49 

tsinnema joined #isabelle 
17:29 

felipealmeida joined #isabelle 
23:02 

kaki joined #isabelle 
23:34 

felipealmeida joined #isabelle 