Time 
Nick 
Message 
02:48 

ilbot3 joined #isabelle 
02:48 

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/ 
04:33 

wagle joined #isabelle 
10:53 

silver joined #isabelle 
11:50 
JCaesar 
Uh, am I missing something? Does finite (dom S) ==> finite (ran S) hold? 
12:08 
pruvisto 
JCaesar: I guess so? 
12:09 
JCaesar 
I'm proving it in very weird ways right now, e.g. first proving finite (dom M) ==> ∃m. M = map_of m… 
12:12 
pruvisto 
JCaesar: http://downthetypehole.de/paste/015sbvqU 
12:14 
inte 
http://sprunge.us/XCVd ? 
12:14 
inte 
*compares* 
12:15 
JCaesar 
narf. 
12:16 
JCaesar 
auto3++ auto4++ 
12:19 
inte 
why didn't I know about ` 
12:34 
larsrh 
JCaesar: I have this proof somewhere 
12:34 
JCaesar 
larsrh: auto3 already applied… 
15:11 
JCaesar 
the irony of my theories: if there's apply, that is by me. if there's an isar proof… sledgehammer. 
15:13 
pruvisto 
olol 
15:13 
pruvisto 
I'm sure that Isar proof is very readable 
15:13 
JCaesar 
Uh, actually… this one is kinda good… 
15:13 
JCaesar 
for sledgehammer standards. 
15:13 
pruvisto 
I actually have almost no "apply"s anywhere 
15:14 
pruvisto 
the only exception is coinductionrelated stuff 
15:15 
pruvisto 
which accounts for like 5 or 6 applies in about 10 kLOC of proofs 
15:15 
pruvisto 
but to be fair, I sometimes put quite a bit of stuff into a "by" 
15:15 
pruvisto 
by (rule foo, rule bar, rule narf) (insert A, simp_all) 
15:15 
pruvisto 
by (rule A, simp, force)+ 
15:15 
pruvisto 
things like that 
15:16 
JCaesar 
that's actually worse than apply style… 
15:16 
JCaesar 
much more annoying to fix. 
15:16 
JCaesar 
(speaking from experience…) 
15:16 
pruvisto 
Well, depends on what the rules look like and where they come from. 
15:17 
pruvisto 
and those are some of the more extreme examples 
15:17 
JCaesar 
my favourite is: you used that one magic Multiset rule, which has now been removed, and you can, for the life of it, not remember what it did. 
18:08 

silver_ joined #isabelle 
18:12 

ertesx joined #isabelle 
19:37 

inte joined #isabelle 
19:39 

inte joined #isabelle 
19:42 

inte joined #isabelle 
19:42 

inte joined #isabelle 