Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Applying drule to specific premise

Email Gateway (Aug 22 2022 at 18:52):

From: Peter Lammich <lammich@in.tum.de>
Hi,

I have a subgoal of the form 

!!x1...xn. [| P1; ...; Pn |] ==> Q

and a function 
  convert :: ctxt -> thm -> thm

I need a tactic that applies convert to each of the premises Pi.
However, I'm somehow lost in what is the right approach to this tactic:
  I know of Subgoal.FOCUS_PREMS to make available the premises as
theorems, but I cannot change them thereafter, e.g., the old premises
will remain in the goal.

The best solution I'm aware of is using FOCUS_PREMS, inserting the new
premises, and then thinning the old ones. However, this feels a bit
odd?

Best,
  Peter

Last updated: Apr 25 2024 at 20:15 UTC