Re: [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 }

This is probably the most practical solution. Note that the actual axiom
can still have the "original" form, so you know that you have the right Hoare
logic, but you can easily get the "useful" form as a derived rule.

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

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

without explicitly giving P1 in my proof script?

This is currently not possible. It could be achieved with a little ML
hacking, but I think it is better to derive rules in the right shape
(as above) and let unification do the work for you.

Hope this helps...


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