[isabelle] Building formulae dynamically from current subgoal


I am currently formalizing a Hoare logic in Isabelle/HOL, and e.g. one axiom looks like

{ f(Q) } stmt { Q }

where f yields some rather complex formula.

To be able to apply this axiom flexibly in a given proof without requiring the given precondition to have the exact syntactical shape, I formalized this as

P = f(Q)
==> { P } stmt { Q }

Now I think that it might look nicer if I stay closer to the original axiom with my formalization, i.e. if I formalize it in Isabelle as

{ f(Q) } stmt { Q }

as well. If I want to apply this axiom to a given Hoare triple

{ P1 } stmt { Q1 }

where P1 has a shape that is different from f(Q), e.g. because two conjuncts are given in a different order, I have two options (to my knowledge) to adapt the given triple: I can either add a lemma

lemma "P1 = f(Q)"

to my library and rewrite  the current goal with this lemma, or I can

apply (subgoal_tac "P1 = f(Q)")

and rewrite the current goal with the new assumption and prove the resulting subgoal later on.

But these two options imply that I explicitly give the actual shape of P1, either in the lemma or in the subgoal_tac application.

My question is: Can I apply subgoal_tac with a formula that is dynamically built from the current subgoal, i.e. can I state something like

apply (subgoal_tac "some_part_of_current_subgoal = f(Q)")

without explicitly giving P1 in my proof script?

Thanks a lot in advance


Books just wanna be FREE! See what I mean at:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.