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?

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

But assuming that `D`

is not in some sort of simp normal form already, this will not be what you want.

```
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
```

I'd like to avoid running a tactic.

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

How about this?

```
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
```

This still uses the fact tactic.

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.]

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

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`

.

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

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

.

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

Last updated: Aug 15 2022 at 02:13 UTC