Stream: Beginner Questions

Topic: ✔ Rewrite term using a proven "p ==> q" theorem?

Jiahong Lee (Dec 19 2022 at 06:46):

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.

Jiahong Lee (Dec 19 2022 at 06:48):

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! *)

Jiahong Lee (Dec 19 2022 at 06:49):

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! *)

Notification Bot (Dec 19 2022 at 06:49):

Jiahong Lee has marked this topic as resolved.

Mathias Fleury (Dec 19 2022 at 09:06):

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)

Wolfgang Jeltsch (Dec 19 2022 at 15:31):

Note that rule refl is something that the standard proof method covers, so that you can replace rule refl by ...

Wolfgang Jeltsch (Dec 19 2022 at 15:32):

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.

Jiahong Lee (Dec 20 2022 at 02:12):

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!

Jiahong Lee (Dec 20 2022 at 02:19):

Note that rule refl is something that the standard proof method covers, so that you can replace rule refl by ...

Thanks for your info, but right now I prefer an explicit proof method for better understanding

Last updated: Apr 28 2024 at 08:19 UTC