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):

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

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: Dec 21 2024 at 16:20 UTC