# IRC log for #isabelle, 2017-08-08

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:15 ammbauer joined #isabelle
10:11 silver joined #isabelle
17:14 dave24 joined #isabelle
17:23 chindy remote_vampire sometimes tells me that it derived false, without showing the proof of that, eventhough i am in a proof by contradiction
18:02 pruvisto chindy: well sledgehammer can't really know that
18:03 pruvisto "show False sledgehammer" should work though
18:04 chindy I have two identical proofs when where i construct an element e by subtracting v from w and one vice versa. the proofs are identical (on paper it says without loss of generalisation assume v < w)... is there a way to tell isabelle, i proved it in one direction, show it in the other, without having to write a separate lemma with all the previously used assumptions
18:04 pruvisto there is the "linorder_wlog" rule
18:04 chindy i dont have a linorder
18:05 chindy its only order
18:05 pruvisto but you know that either v < w or w < v holds?
18:05 chindy yes... they are special constructions... the proof is also done without sorries... its just i want to make it nicer t oread
18:05 chindy to read*
18:06 chindy pruvisto: funny thing is when i do have "P x" sledgehammer it says vampire derived false when i do show False, it does not say such a thing :/
18:06 pruvisto yeah no idea what goes on there
18:06 pruvisto anyway, you can prove your own rule like linorder_wlog, I suppose
18:07 pruvisto or, what I often do is to prove the statement for arbitrary v w and then just instantiate that with [of u v] and with [of v u]
18:07 chindy yea... but how can i do that with arbitrary v w within an isar block
18:13 larsrh chindy: have "bla v w" for v w
18:20 chindy hmm.. problem is i already have obtained v and w i just dont know if w > v or v > w, but its only 20 lines of "duplicate"code so i might just leave it
18:21 larsrh you can either make the obtained facts local assumptions (have "bla v w" if "P v" "Q w" for v w)
18:21 larsrh or as pruvisto said prove your own rule
19:14 stoopkid_ joined #isabelle