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
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
I think that's the god-given way to do it, yes ;)
Last updated: Aug 15 2022 at 02:13 UTC