Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-29

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

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/
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, non-reusable 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

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary