Time 
Nick 
Message 
00:02 
rollary 
could someone point me to an example of how to do proofs by contradiction in isar using "proof contradiction"? 
00:02 
rollary 
my proof state has the following two subgoals: 1. ¬ ?P 2. ?P 
00:03 
rollary 
how can i specify them? this might be more of an isar question 
00:09 
JCaesar 
proof(rule ccontr) 
00:10 
JCaesar 
show "¬ something" show "something" (possibly with a next in between.) 
00:10 
JCaesar 
(I'd be worried about the thing you're showing, though.) 
00:12 
JCaesar 
You can do the same thing with assumptions, btw. if you have goals 1. "?P ==> asdf" 2. "¬ ?P ==> asdf", you can do an assume foo show asdf next assume "¬ foo" show asdf. 
00:12 
rollary 
ah, thanks 
00:13 
rollary 
why are you worried about what i'm showing? the types notP and P appear in my assumptions 
00:13 
JCaesar 
That's okay. But if you have to show ?P and ¬ ?P, I'd be worried. 
00:13 
rollary 
i see 
00:18 
rollary 
sorry, another question 
00:18 
JCaesar 
Oh, btw, there's a nice section in the isar manual that explains how to do all the usual derivations in natural deduction in isar. If you have a bit of a logic background, that might help. 
00:19 
rollary 
my theorem looks like this: P > notP > Q 
00:19 
rollary 
i can't see how to use proof (rule ccontr) to show Q 
00:19 
JCaesar 
that might be due to how the facts are… available… 
00:20 
JCaesar 
I can't explain this very well. 
00:20 
JCaesar 
The rule method doesn't like it if you have facts lying around the way you get then when you use "using". 
00:21 
JCaesar 
You can try an apply  before the proof(rule ccontr). If that helps, that was the case. 
00:21 
rollary 
ah so would you recommend not using isar for this then? 
00:21 
JCaesar 
I wouldn't say that. 
00:21 
JCaesar 
I have to ask, though… what's notP? 
00:21 
JCaesar 
You said, it was a type, earlier? 
00:22 
rollary 
just an assertion? 
00:22 
rollary 
i'm sorry, i'm quite new to isabelle 
00:22 
rollary 
it's just a statement 
00:22 
JCaesar 
did you say anything like lemma "P ==> ¬ P ==> Q"? 
00:23 
rollary 
yup 
00:23 
JCaesar 
then, a simple by blast should solve the goal. 
00:23 
JCaesar 
The assumptions are contradictory, after all. 
00:24 
JCaesar 
(if you write "try" instead of apply or proof, it should directly tell you that.) 
00:24 
JCaesar 
("try", and nothing after it.) 
00:25 
rollary 
sure, trying (hah) 
00:26 
rollary 
ah so it suggests notE 
00:26 
rollary 
how do i use it? 
00:26 
JCaesar 
Much of the stuff has funny names. There's proof methods called force (so you'll write "apply force"), and a command called sledgehammer. 
00:26 
JCaesar 
Oh, it comes back with autosolve direct? 
00:26 
rollary 
yup 
00:27 
JCaesar 
Meh, right, that's actually a bit annoying. It's telling you that what you want to prove has already been proved (maybe in a more general way). 
00:28 
JCaesar 
In theory, it should be possible to use by(rule notE) as a proof, but I'm not sure that always works. 
00:28 
JCaesar 
Try writing try0 instead of try, that will give you concrete instructions. 
00:29 
JCaesar 
(I'm not a big fan of try. sometimes it will take ages and you have no idea what it's doing. I usually use try0 and sledgehammer instead.) 
00:29 
rollary 
hm, it shows no proof found :/ 
00:29 
rollary 
why is this so (seemingly) difficult? 
00:30 
JCaesar 
issues with unification. 
00:30 
JCaesar 
(I'm assuming. No idea.) 
00:30 
rollary 
aha, so sledgehammer has done the trick 
00:32 
rollary 
i'd like to bother you about another thing now. suppose i have lemma "A ==> B ==> P ==> Q" and I know that A & B ==> not(P) 
00:32 
rollary 
how can I prove this new lemma? 
00:49 
JCaesar 
proof  assume "A" "B" hence "¬ P" by … moreover assume "P" ultimately show "Q" by … qed 
00:53 
rollary 
ah, brilliant, trying it out now  thanks 
00:56 
rollary 
what should the last ... be? 
00:57 
rollary 
oh, "by contradiction" 
00:57 
rollary 
got it 
06:18 

wagle joined #isabelle 
10:01 
JCaesar 
I've never used the contradiction method… 
10:20 

larsrh joined #isabelle 
10:31 
pruvisto 
JCaesar: I use it all the time 
10:31 
pruvisto 
it's not strictly speaking necessary 
10:31 
pruvisto 
but it sounds nice and idiomatic 
10:31 
JCaesar 
Agreed. 
10:54 

silver joined #isabelle 
17:33 
chindy 
how do i define some predicate that is true for all pairs of elements in 1 set ... say: \forall x y \in S . x = y this syntax is wrong, but what would be tghe right syntax? 
17:40 
chindy 
okay got it just with two quantifiers 
22:12 

silver_ joined #isabelle 