# IRC log for #isabelle, 2016-09-27

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01:47 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/
08:35 pootler joined #isabelle
09:09 JCaesar IIRC, there was some way to give the resulting goals of proof(rule foo) a name to use as case (Bar x). Do I remember correctly? Is there an example somewhere
09:10 JCaesar case_names?
09:12 ThreeOfEight yes.
09:12 ThreeOfEight proof (rule foo [case_names Bar])
09:12 ThreeOfEight but the "proper" way in that situation is "proof (rule foo, goal_cases)"
09:12 ThreeOfEight goal_cases can also take parameters for the case names, I think
09:13 ThreeOfEight i.e. "goal_cases Bar"
09:13 JCaesar ah, that's neat.
09:13 larsrh JCaesar: is foo a case rule?
09:13 JCaesar I thought I could provide the case names with the lemma, though, but that doesn't seem to work.
09:13 JCaesar mmmh, I wonder. Probably not.
09:13 ThreeOfEight JCaesar: it does, but only when you use the "cases" command
09:13 larsrh you can, but they will only get interpreted by induct and cases
09:13 ThreeOfEight oh
09:14 ThreeOfEight actually, yeah, "rule foo [case_names â€¦]" probably won't work
09:15 ThreeOfEight It should be possible to extend rule to use case names
09:15 JCaesar would be neat, especially for things you use a lot, like ccontrâ€¦
09:44 ThreeOfEight Good ol' ccontr, yeah, that's a classic.
09:44 larsrh ThreeOfEight: you're out
09:44 ThreeOfEight larsrh: Aber warum das denn?
09:45 ThreeOfEight JCaesar: if you use ccontr /that/ often, you ought to perhaps reconsider your proof style :P
09:46 JCaesar actually, I use notI more often. Anyway.
09:46 ThreeOfEight notI is fine
09:46 larsrh JCaesar: notI is the intuitive choice
09:46 ThreeOfEight larsrh: now you're out
09:47 JCaesar ThreeOfEight: close but no, I think he's still in.
09:47 JCaesar larsrh: That's still a proof by contradiction, at least in my head.
09:47 larsrh JCaesar: nope
09:48 larsrh If your proposition is "Not P", proving "P ==> False" is perfectly constructive.
09:48 larsrh In fact, "Not P" is defined as "P ==> False"
09:48 ThreeOfEight glad to see you're sticking to constructive criticism in here.
09:49 JCaesar -_-
15:11 kini joined #isabelle
15:26 pootler joined #isabelle
16:38 wagle joined #isabelle
16:38 logicmoo joined #isabelle
16:44 relrod_ joined #isabelle
16:44 relrod_ joined #isabelle
16:45 dmiles joined #isabelle
16:48 pootler joined #isabelle
16:49 wagle joined #isabelle
16:56 ski joined #isabelle
16:58 kini joined #isabelle
17:01 ThreeOfEight joined #isabelle
17:08 Merv_ joined #isabelle
17:59 aindilis2 joined #isabelle
18:10 aindilis` joined #isabelle
18:23 pootler joined #isabelle
19:20 pootler joined #isabelle
19:45 int-e joined #isabelle
20:23 pootler joined #isabelle
20:23 int-e joined #isabelle
20:25 dmiles joined #isabelle
20:32 logicmoo joined #isabelle
20:33 int-e joined #isabelle
20:45 int-e_ joined #isabelle
21:24 pootler joined #isabelle
22:25 pootler joined #isabelle
23:26 pootler joined #isabelle