# IRC log for #isabelle, 2017-08-23

All times shown according to UTC.

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 int-e 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 int-e obtain y :: "'a::ordered_euclidean_space" where "y ? 0" using nonempty_Basis inner_Basis euclidean_all_zero_iff by blast
09:35 chindy int-e: euclidean_space already has an assumption that the Basis is non_empty
09:36 int-e yes, it already works in euclidean_space
09:36 int-e (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 int-e your final statement is stronger than just having a non-zero vector though; I guess you'll have to take the negative of the sum of all the basis vectors for that.
09:53 int-e 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 well-typed without that either
12:37 chindy pruvisto: thanks
12:38 pruvisto the main use is for Big-Oh 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.isa-afp.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.isa-afp.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