# IRC log for #isabelle, 2013-02-19

All times shown according to UTC.

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 built-in 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: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 int-e 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