## Stream: Beginner Questions

### Topic: OF: resolving premise that is an implication

#### Lukas Stevens (Jul 21 2020 at 08:13):

I have the following situation:

``````lemma
assumes "A ⟹ B ⟹ C"
assumes "(A ⟹ B ⟹ C) ⟹ D"
shows D
proof -
thm assms(2)[OF assms(1)]
oops
``````

The application of `OF` gives me the theorem `⟦⟦A; B⟧ ⟹ A; ⟦A; B⟧ ⟹ B⟧ ⟹ D`. What I want is just `D`. How can I do that?

#### Kevin Kappelmann (Jul 21 2020 at 08:50):

That's the best I can come up with: ` have "D" by (fact assms(2)[OF assms(1), simplified])`

#### Kevin Kappelmann (Jul 21 2020 at 08:51):

But assuming that `D` is not in some sort of simp normal form already, this will not be what you want.

#### Kevin Kappelmann (Jul 21 2020 at 08:53):

``````lemma
assumes "A ⟹ B ⟹ C"
assumes "(A ⟹ B ⟹ C) ⟹ D ∧ D"
shows D
proof -
have "D ∧ D" by (fact assms(2)[OF assms(1), simplified]) ― ‹fails›
have "D" by (fact assms(2)[OF assms(1), simplified]) ― ‹works›
oops
``````

#### Lukas Stevens (Jul 21 2020 at 08:53):

I'd like to avoid running a tactic.

#### Lukas Stevens (Jul 21 2020 at 08:54):

What I am showing here is part of a procedure which constructs a thm. So I would like to avoid tactics.

#### Kevin Kappelmann (Jul 21 2020 at 10:08):

``````lemma
assumes "A ⟹ B ⟹ C"
assumes "(A ⟹ B ⟹ C) ⟹ D"
shows D
proof -
from assms(2) assms(1) have "D" by (fact Pure.cut_rl)
oops
``````

#### Lukas Stevens (Jul 21 2020 at 10:23):

This still uses the fact tactic.

#### Josh Chen (Jul 21 2020 at 10:29):

I doubt there's any way of using `OF` to remove that premise, the really strict way resolution works precludes that. You'll have to resort to doing some ML, or else define some wrapper constant. [I'm not sure this is possible here.]

#### Simon Roßkopf (Jul 21 2020 at 10:32):

If you plan to work on the ML level, you might have some success with Drule.compose, depending on how your concrete theorems look

#### Josh Chen (Jul 21 2020 at 10:34):

Yes. Note that there might be issues with lifting for `Drule.compose` (e.g. https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2019-September/msg00090.html for a previous version of Isabelle, but I think the problem is still there).

For conclusions this is achievable by `Goal.protect`, and for terms `Logic.protect`, `Drule.protect`.

#### Lukas Stevens (Jul 21 2020 at 10:37):

I am working on the ML level, so using ML functions is my goal anyways.

#### Lukas Stevens (Jul 21 2020 at 10:38):

Judging from Makarius answer, it is probably better to discharge all the trivial goals coming from the final resolution step with `assume_tac`.

#### Josh Chen (Jul 21 2020 at 10:39):

I think that's the god-given way to do it, yes ;)

Last updated: Aug 15 2022 at 02:13 UTC