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/ 
09:57 
ammbauer 
is there a way to group lemmas/statements in an isar proof? 
09:57 
ammbauer 
http://downthetypehole.de/paste/bQfbTctD 
10:28 
pruvisto 
ammbauer: well there's "moreover" … "ultimately" 
10:29 
pruvisto 
and you can "group" facts together using "note" 
10:29 
pruvisto 
but you still have to do that explicitly 
10:29 
pruvisto 
i.e. "note foo = A B C" 
10:29 
pruvisto 
I don't think something like what you have in mind is possible 
12:56 
pruvisto 
chindy: Tobias Nipkow also asked when you'll submit your stuff to the AFP. ;) 
12:58 
chindy 
pruvisto: hopefully somewhen in september 
12:59 
pruvisto 
good 
13:00 
pruvisto 
the general observation is that when stuff does not get submitted to the AFP, it starts to rot 
13:00 
pruvisto 
until it reaches a point where it is painful or even virtually impossible to get back into a working state 
13:01 
pruvisto 
I was struggling to update my work on linear recurrences yesterday 
13:01 
pruvisto 
It was awful 
13:01 
pruvisto 
And Jeremy Avigad's proof of the Prime Number Theorem will almost certainly never be repaired. 
13:51 

pruvisto joined #isabelle 
14:02 

hazyPurple joined #isabelle 
14:37 
chindy 
pruvisto: why, is nobody maintaining the proof? 
14:45 
pruvisto 
chindy: No. 
14:48 

hazyPurple joined #isabelle 
15:00 

juanbono joined #isabelle 
15:30 
ammbauer 
"The formalization has not been adapated to Isabelle 2005." https://www.andrew.cmu.edu/user/avigad/isabelle/ 
15:31 
ammbauer 
pruvisto: can't be that hard :P 
15:41 
pruvisto 
Well it hardly matters 
15:41 
pruvisto 
We have another proof of this thing now 
15:41 
pruvisto 
one that's based on complex analysis 
15:42 
pruvisto 
Avigad's proof was an elementary one 
15:43 
pruvisto 
"elementary" sounds nice until you realise that this usually means a crapload of very specific, complicated, nonreusable material 
15:44 
pruvisto 
The analytic part alone is like 20 kLOC 
15:45 
pruvisto 
whereas the new proof is about 4 kLOC, and I intend to reduce that significantly by pulling out the Riemann Zeta function soon 
16:59 

hazyPurple joined #isabelle 
17:53 
chindy 
I wonder how i can define a set to be unbounded above, i thought one of these would do: http://downthetypehole.de/paste/72YtFlQP but it seems like i misunderstood something 
18:26 
pruvisto 
well you can write ¬bdd_above carrier 
18:27 
pruvisto 
that means something like "?C. ?x?carrier. x ? C" 
18:28 
pruvisto 
err, ?C. ?x?carrier. x > C 
18:28 
pruvisto 
that's usually equivalent though 
18:37 
chindy 
pruvisto: shouldn't this basically follow from the definition ? http://downthetypehole.de/paste/1yZCSHpz 
18:39 
chindy 
ah... i probably need a total order 
18:40 
chindy 
so that ~ <= <> > 
18:42 
chindy 
nvm... no idea why i dont get what i want :/ 
19:00 
chindy 
what about this: "?M ? carrier::'a::order set. (?x > M. x ? carrier)" 
19:00 
chindy 
seems like ~ bbd_above does not imply "?M ? carrier::'a::order set. (?x > M. x ? carrier)" 
19:01 
chindy 
bdd* 
19:04 

mal`` joined #isabelle 
19:13 
pruvisto 
no, of course not 
19:13 
pruvisto 
that's not what "unbounded" means 
19:14 
pruvisto 
what you wrote sounds more like a closure property 
19:14 
pruvisto 
the set {1,2,3,4,…} of real numbers is unbounded, but it certainly does not have the property that you just wrote 
19:15 
chindy 
hmm... wait what is the mathematical definition of unbounded above? 
19:18 
chindy 
seems like i have been looking for the wrong definition :/ 
19:45 
pruvisto 
well, "bounded" means that there is an upper bound 
19:45 
pruvisto 
i.e. some value such that nothing in the set is greater 
19:46 
pruvisto 
and unbounded is the negation of that 
19:46 
pruvisto 
for every value, there is something in the set that is greater 
20:07 

aindilis joined #isabelle 
21:51 

juanbono94 joined #isabelle 