I understand how ccontr works, however I am unsure how (or even if it is possible) to use it on a lemma declared with assumption(s).
Take this simple example, all is good:
lemma l1: "A⊆B ⟶ A ∩ B = A"
proof(rule ccontr)
assume "¬(A⊆B ⟶ A ∩ B = A)"
then show False
by auto
qed
Technically, the lemma is equivalent (**Note) to:
lemma l2:
assumes P: "A⊆B"
shows Q: "A ∩ B = A"
proof(rule ccontr)
assume "¬(P ⟶ Q)"
then show False ...
qed
gives an error on the "then show..." line
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(¬ (P ⟶ Q)) ⟹ False
It seems that I cannot use ccontr in the assumes... shows... version (l2). I have tried to use assume Q ∧ ¬P, with the same error.
Is there a way to go on with some sort of proof of the form "assume (Q and ~P) show False therefore lemma is correct"?
(**Note): Side question: is my assumption that lemmas l1 and l2 are logically equivalent? Is there something that makes them dramatically different from each other (in Isabelle)?
Thank you in advance!
You should negate what you claim (in shows) and then prove that given the assumptions this leads to False:
lemma l2:
assumes P: "A⊆B"
shows "A ∩ B = A"
proof (rule ccontr)
assume "¬(A ∩ B = A)"
with P show False by auto
qed
I checked this in Isabelle/ZF but it should be the same in Isabelle/HOL.
As for the side question strictly speaking these two forms are not logically the same as the first one uses the object logic implication ⟶ while the second one uses ==> from meta-logic. Both forms express the same idea however and I personally prefer the second one as it is more readable and works better with automation in Isabelle.