## 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: Sep 11 2024 at 16:22 UTC