Time 
Nick 
Message 
01:48 

ilbot3 joined #isabelle 
01: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/ 
10:11 

silver joined #isabelle 
10:21 

aindilis2 joined #isabelle 
10:30 

ammbauer joined #isabelle 
16:03 
chindy 
Under what circumstatnces does sledgehammer tell me, that a proof was found, but never shows the proof, or takes forever 
16:07 
chindy 
Nevermind... i think it found one... but timed out :/ 
16:08 
larsrh 
if one of the automated provers found a proof but it can't be reconstructed in metis or smt 
16:10 
chindy 
:/ damn... i already had my hopes up :P 
16:11 
larsrh 
happens occasionally 
16:11 
larsrh 
you can try applying some rules manually, then trying again 
16:11 
larsrh 
of course that only works if you have a rough idea of what should happen 
16:13 
chindy 
well sledgehammer gave me a 78line isar proof :/ we'll see :P 
16:13 
larsrh 
... a proof that works? 
16:13 
larsrh 
if so you might've set a new record there 
16:16 
chindy 
no... as i said it said (* timed out in multiple parts *) 
16:16 
JCaesar 
larsrh: doubt it… 
16:16 
JCaesar 
chindy: If you're feeling lucky / lazy, you can try reapplying sledgehammer to the timedout parts. 
16:17 
larsrh 
chindy: ah, I get it now 
16:17 
larsrh 
I thought you retried with enabled Isar proofs 
16:26 
chindy 
sadly... would have been 120 lines :( 
18:08 

silver_ joined #isabelle 
18:12 

ertesx joined #isabelle 
18:37 
chindy 
is this the dot product or component wise product? (P::real^2) * X 
18:39 
JCaesar 
Hm, the controlclick doesn't take you to the instance definition, I guess? 
18:53 
chindy 
JCaesar: nah... only tells me that its part of a Group 
18:53 
chindy 
... 
18:53 
JCaesar 
thought so… 
18:54 
larsrh 
what's the type name of ^2? 
18:55 
pruvisto 
chindy: * always has type 'a => 'a => 'a 
18:55 
pruvisto 
so that can't be the dot product 
18:55 
pruvisto 
that's \<bullet> 
18:55 
pruvisto 
i.e. ∙ 
18:55 
pruvisto 
* is probably componentwise, just check the instantiation 
18:55 
pruvisto 
larsrh: real^2 = (real, 2) vec 
18:56 
larsrh 
in that case you can jump to the definition by clicking on the term "times_vec_inst.times_vec" 
18:56 
larsrh 
(that's the internal name of the instantiation) 
18:57 
larsrh 
vec is not in Complex_Main, is it? 
18:57 
chindy 
larsh... if understand correctly its not complex_Main 
18:58 
larsrh 
anyway, here's the definition: definition "op * ≡ (λ x y. (χ i. (x$i) * (y$i)))" 
18:58 
chindy 
its in Finite_Cartesian_Product whatever that entail 
18:58 
chindy 
s 
19:01 
larsrh 
yeah, as I expected 
19:02 
larsrh 
times_vec_inst.times_vec leads you to the instantiation 
19:02 
larsrh 
I wish this could be searched for in an easier way 
19:04 
larsrh 
Why is the instantiation (times, finite) times and not (times, type) times? 
19:04 
larsrh 
Funnily enough if you change finite to type it complains about a duplicate constant 
19:05 
larsrh 
fascinating 
19:14 
pruvisto 
larsrh: no 
19:15 
pruvisto 
it's part of HOLAnalysis 
19:15 
pruvisto 
chindy: are you that person on Stack Overflow? 
19:15 
pruvisto 
larsrh: because of reasons *shrug* 
19:16 
pruvisto 
probably because nobody really uses vec with infinite index types 
21:03 
chindy 
pruvisto: no... why ? 
21:08 
chindy 
Can somone explain how PBC and disjE work? I dont understand how here, http://downthetypehole.de/paste/SXC4NS9Q it says that it failed to finish the proof 
21:19 
JCaesar 
ah, you need to apply it as an erule, not a rule… 
21:19 
JCaesar 
and I think you can just do proof cases here… 
21:20 
JCaesar 
(or rather: elim, not erule. I'm not sure when either of those things work…) 
21:50 

silver_ joined #isabelle 