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:25 
pruvisto 
hm, well I don't know anything about this. 
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 ordertheoretic 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/IsabelleHelloWorld 
17:38 
pruvisto 
hey, not much more boilerplate than Java 
18:32 

mal`` joined #isabelle 
21:41 

aindilis joined #isabelle 