Stream: Beginner Questions

Topic: OF: resolving premise that is an implication


view this post on Zulip 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?

view this post on Zulip 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])

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Lukas Stevens (Jul 21 2020 at 08:53):

I'd like to avoid running a tactic.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Lukas Stevens (Jul 21 2020 at 10:23):

This still uses the fact tactic.

view this post on Zulip 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.]

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Jul 21 2020 at 10:37):

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

view this post on Zulip 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.

view this post on Zulip 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