I see, thanks! The subst
proof method does the trick for me:
lemma "p ∨ q ⟹ p ∨ ¬ ¬ q"
proof -
assume "p ∨ q"
thus "p ∨ ¬ ¬ q" by(subst not_not)
qed
lemma "p ∨ ¬ ¬ q ⟹ p ∨ q"
proof -
assume "p ∨ ¬ ¬ q"
thus "p ∨ q" by(subst not_not[symmetric])
qed
Given a theorem , it substitutes terms matching its RHS by its LHS.
However, it doesn't work in calculational reasoning:
lemma "(P ⟶ Q) ⟷ ¬ (P ∧ ¬ Q)"
proof -
have "(P ⟶ Q) = (¬ P ∨ Q)" by(rule imp_conv_disj)
also have "... = (¬ P ∨ ¬ ¬ Q)" by(subst not_not) (* Error! *)
After searching around, the unfolding
proof method does the trick for me:
lemma "(P ⟶ Q) ⟷ ¬ (P ∧ ¬ Q)"
proof -
have "(P ⟶ Q) = (¬ P ∨ Q)" by(rule imp_conv_disj)
also have "... = (¬ P ∨ ¬ ¬ Q)" unfolding not_not by(rule refl) (* Ok! *)
Jiahong Lee has marked this topic as resolved.
Jiahong Lee said:
However, it doesn't work in calculational reasoning:
lemma "(P ⟶ Q) ⟷ ¬ (P ∧ ¬ Q)" proof - have "(P ⟶ Q) = (¬ P ∨ Q)" by(rule imp_conv_disj) also have "... = (¬ P ∨ ¬ ¬ Q)" by(subst not_not) (* Error! *)
as you noticed, subst only does the substitution, not proving that ?A = ?A
, so
also have "... = (¬ P ∨ ¬ ¬ Q)" by(subst not_not) (rule refl)
Note that rule refl
is something that the standard
proof method covers, so that you can replace rule refl
by ..
.
By the way, it took me years of intensely working with Isabelle to discover that; actually, my colleague @Javier Diaz discovered it, and I saw him using this trick. Before, I had resorted to simp
in such situations, which might often be considered overkill.
as you noticed, subst only does the substitution, not proving that ?A = ?A,
Ah, I see, the error message didn't make sense to me previously, thanks!
Note that
rule refl
is something that thestandard
proof method covers, so that you can replacerule refl
by..
.
Thanks for your info, but right now I prefer an explicit proof method for better understanding
Last updated: Oct 12 2024 at 20:18 UTC