# [isabelle] Building formulae dynamically from current subgoal

Hello,

`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
Nicole
--
Books just wanna be FREE! See what I mean at:
http://bookcrossing.com/friend/HoneyBunny42

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