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 