# IRC log for #isabelle, 2017-03-27

All times shown according to UTC.

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 re-applying sledgehammer to the timed-out 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 control-click 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 component-wise, 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 HOL-Analysis
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