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

All times shown according to UTC.

Time Nick Message
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/
08:17 dmiles joined #isabelle
08:54 chuchucorny joined #isabelle
08:55 chuchucorny moin
08:55 chuchucorny are there any simple examples for IO programming in Isabelle/HOL?
09:19 pruvisto There is IO programming in Isabelle/HOL?
09:23 chuchucorny Well, there is code export and code printing, ....
09:31 chuchucorny Lochbihler, Züst, and and Hölzl wrote TLS in Isabelle/HOL. Are the sources lying around somewhere?
09:37 larsrh I haven't seen them
09:37 larsrh you should mail Andreas and bug him
12:20 Merv joined #isabelle
13:00 chindy can someone explain why sledgehammer does not seem to be able to prove this? http://downthetypehole.de/paste/69PsdUDs
13:01 chindy or maybe i am missing something crucial
13:05 pruvisto chindy: what if S is infinite?
13:06 pruvisto the way Min is defined, it is simply undefined if the set that it is given is empty or infinite
13:06 chindy even if it is well ordered?
13:06 chindy i though every well ordered subset has a least eleemnt or something
13:06 chindy i mean every subset of a well ordered set has a least element
13:06 pruvisto yeah I think you want to use "Inf"
13:06 pruvisto that works on any conditionally complete lattice
13:07 chindy I see... but inf requires analysis right?
13:07 pruvisto I doubt it
13:08 pruvisto for nat, there also exists the "Least" combinator
13:08 pruvisto e.g. "LEAST n. P n"
13:09 pruvisto ok I just checked and "Inf" definitely doesn't require Analysis
13:09 pruvisto not even Complex_Main
13:09 pruvisto and, well, there's no reason why it's should; it's an order-theoretic concept, not an analytic one
13:12 chindy pruvisto: ah thanks!
13:12 pruvisto I can see why "Min"/"Max" are confusing in this regard
13:13 pruvisto they're probably for things that aren't a conditionally complete lattice
13:13 pruvisto but that still support at least a binary minimum/maximum operation, and therefore one for finite sets
13:14 pruvisto also, I guess it is a slightly different thing
13:14 pruvisto one would expect a "minimum" of a set to be in that set
13:14 pruvisto whereas the infimum isn't always in the set
13:15 pruvisto (of course, whenever there /is/ a minimum, it will be equal to the infimum, but in general, the infimum is a stronger concept)
13:29 chindy just to be clear the infimum of 1/x x-> inf is 0, right
13:30 chindy so inf {1/x |x. x : 1..infinity} = 0
14:16 pruvisto yes
15:38 chuchucorny I wrote HelloWorld in Isabelle :D https://github.com/diekmann/Isabelle-Hello-World
17:38 pruvisto hey, not much more boilerplate than Java
18:32 mal`` joined #isabelle
21:41 aindilis joined #isabelle