# [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?

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.