Re: [isabelle] Building formulae dynamically from current subgoal



Hello Nicole,

I would not propose to start building some complicated tactics, or instantiations. In my experience with Hoare logics the following approach worked out the best:
1) For the definition of the calculus take the variant
{ f(Q) } stmt { Q }. This reflects the core idea of the rule.
2) For application of the calculus in a backwards manner define a variant that is just a composition of the rule in 1) and a consequence rule that you surely also have
in your core calculus.

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

This rule can be applied to any P and Q and also deliberates you from explicitely
deriving P=f(Q).

    Norbert








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