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 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: Oct 12 2024 at 20:18 UTC