Time 
Nick 
Message 
01:52 

ilbot3 joined #isabelle 
01:52 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
05:01 

logicmoo joined #isabelle 
05:52 

ski joined #isabelle 
06:32 
chindy 
doing that results in Type unification failed: No type arity set :: plus since plus is 'a => 'a => 'a and not set, I believe 
09:07 
chindy 
I think i dont understand the concept of euclidean spaces... can someone explain why there is negation on euclidean spaces but not negative components? http://downthetypehole.de/paste/cZUnmIT1 
09:22 
chindy 
I hade a mistake... but i still dont understand why its so difficult to obtain an element that is not 0: http://downthetypehole.de/paste/fTW0Hu5x 
09:28 
inte 
Well, there isn't one if the dimension of the space is 0. So it's tied to the basis being nonempty etc. 
09:34 
inte 
obtain y :: "'a::ordered_euclidean_space" where "y ? 0" using nonempty_Basis inner_Basis euclidean_all_zero_iff by blast 
09:35 
chindy 
inte: euclidean_space already has an assumption that the Basis is non_empty 
09:36 
inte 
yes, it already works in euclidean_space 
09:36 
inte 
(I manually typed obtain y :: "'a::ordered_euclidean_space" where "y ? 0" using nonempty_Basis inner_Basis euclidean_all_zero_iff and then I used the sledgehammer panel because I didn't expect blast to do the job :P) 
09:39 
inte 
your final statement is stronger than just having a nonzero vector though; I guess you'll have to take the negative of the sum of all the basis vectors for that. 
09:53 
inte 
oh actually since < is just <= and ~= (which is perhaps not what you want), it's enough to pick any basis vector and negate ti. obtain i :: "'b :: ordered_euclidean_space" where "i ? Basis" using nonempty_Basis by blast then have "i ? 0" "i ? 0" by auto then have "i < 0" by simp 
12:25 
pruvisto 
chindy: well you have to import ~~/src/HOL/Library/Set_Algebras 
12:25 
pruvisto 
but "op + ({1}::nat set) {2,1}" won't be welltyped without that either 
12:37 
chindy 
pruvisto: thanks 
12:38 
pruvisto 
the main use is for BigOh notation, I think 
12:38 
pruvisto 
so you can write something like O(f) + O(g) 
12:41 
JCaesar 
Hm, btw, are there any nice examples of Landau notation in Isabelle? 
12:42 
chindy 
pruvisto: but it's well typed... 
12:42 
chindy 
what is used in big o ? 
12:46 
JCaesar 
Set_Algebras, I presume? 
12:50 
pruvisto 
JCaesar: depends on what you mean by "nice" 
12:50 
pruvisto 
there's some stuff in Akra_Bazzi 
12:51 
pruvisto 
https://www.isaafp.org/browser_info/current/AFP/Akra_Bazzi/Master_Theorem_Examples.html 
12:53 
pruvisto 
but I don't really use the Set_Algebras stuff very much 
12:53 
pruvisto 
Jeremy Avigad used notation like "f =o g +o O(%n. n)" back in the day 
12:54 
pruvisto 
you can also do that with my Landau symbols, but I never really liked it very much 
12:54 
pruvisto 
also there's https://www.isaafp.org/browser_info/current/AFP/Euler_MacLaurin/Euler_MacLaurin_Landau.html 
12:57 
JCaesar 
Akra_Bazzi does at least show one or the other thing. :) (Aber warum ist der Akra so ein Bazi?) 
13:01 
pruvisto 
JCaesar: Sie sind raus. 
13:06 
* JCaesar 
ist raus. 
13:06 

JCaesar left #isabelle 
13:07 

JCaesar joined #isabelle 
16:29 

juanbono joined #isabelle 
21:32 

numee joined #isabelle 