IRC log for #isabelle, 2017-08-16

All times shown according to UTC.

Time Nick Message
01:32 relrod joined #isabelle
01:32 relrod joined #isabelle
01:33 keep_learning joined #isabelle
01:51 ilbot3 joined #isabelle
01:51 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/
03:03 wagle joined #isabelle
05:02 dmiles joined #isabelle
10:00 dave24 joined #isabelle
11:20 JCaesar I wonder if I could abuse isabellectl to make decent isabelle ebuilds…
12:45 larsrh Why not?
12:48 chindy Is there a more canonical way of writing there exits a negative component, given an euclidean_space , than: ?e ? Basis. e ? y < 0 ?
12:52 int-e wouldn't that be  ¬(y ? 0)?
12:55 pruvisto int-e: I don't think any euclidean space has an order defined like that
12:55 pruvisto but in an ordered_euclidean_space, that should work
12:57 int-e fair enough
13:06 chindy pruvisto: in addition to the other 2 lemmas, one might consider adding this: http://downthetypehole.de/paste/ths1ANQR
13:08 pruvisto I don't know, that seems both very specific and very simple
13:09 pruvisto fyi you can prove that in one line with "by (subst eucl_le) (auto simp: not_le inner_commute)"
13:12 chindy pruvisto: thanks!
13:13 chindy pruvisto: yea maybe it is to specific and very simple. If that is a criterion for not adding something, then its probably better to not add it
13:13 pruvisto kind of
13:14 pruvisto if it's something that I cannot imagine being of great general use and also being provable in a single line if you do need it, I'm reluctant to add it to the library
13:48 int-e hmm,  foo[of t, unfolded bar[of t], for t]  would be nice (that is, separating the "of" and "for" of the foo[of xyzzy for x] syntax)
14:28 pruvisto argh Curry Club
14:29 pruvisto "Im Curry Club sind sie auch alle schwul. Alle stehen auf Typen."
14:30 * int-e grübelt
14:30 pruvisto oh
14:30 pruvisto crap
14:30 pruvisto wrong channel