Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Building formulae dynamically from current sub...

Email Gateway (Aug 18 2022 at 10:18):

From: Nicole Rauch <rauch@informatik.uni-kl.de>
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

Email Gateway (Aug 18 2022 at 10:18):

From: Alexander Krauss <krauss@in.tum.de>
Nicole,

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
like

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...

Alex

Email Gateway (Aug 18 2022 at 10:18):

From: Norbert Schirmer <schirmer@informatik.tu-muenchen.de>
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

Last updated: May 03 2024 at 04:19 UTC