Email Gateway (Jul 07 2025 at 12:54): Email Gateway (Jul 07 2025 at 12:54):From: "\"Putti, Edoardo (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
I am writing a verification condition generation tactic and I have two questions.
The problem with 1 is that irrespective of the matchin pattern (for fixes, schematics, _) match
always instantiates the schematics by focusing on the subgoal. This happens even when the names introduced
are not used/bound in the match body. A matching goal like "hoare ?P C ?Q" gets instantiated to "hoare P C Q"
and this cannot match any specification I have. Is there a way to control this focusing behavior, e.g. an option?
The second issue becomes clearer with an example. The following is a pattern for guiding the tactic to use a specific lemma for verification condition generation. The precondition P is tagged with a marker, i.e. STATE P, the vcg_lemma can be used as
an elimination rule to remove it from the premises.
definition STATE :: "('s ⇒ bool) ⇒ 's ⇒ bool"
― ‹tagging of state predicates for use in preconditions›
where
"STATE P ≡ P"
lemma STATE_vcg:
assumes pre: "STATE P s" and spec: "hoare P' M Q'"
and pre_framing: "⋀ s. P s ⟹ (P' ** F) s"
and post_framing: "⋀ x s. STATE (Q' x ** F) s ⟹ Q x s"
shows "wp_cnres M Q s"
If I want to extend this pattern with more markers, .e.g. LOCK lid, I add a LOCK_vcg lemma. I can make the
vcg tactic more generic by adding all my vcg lemmas into one fact abstraction but this is not enough.
I don't have a way to abstract over the marker terms and I need to repeat the same pattern as long as I introduce more markers.
My tactic is not really extensible.
(match premises in marker [thin]: "STATE P s" for P ⇒ ‹(rule vcg_lemmas[OF marker])›)
| (match premises in marker [thin]: "LOCK lid" for lid ⇒ ‹(rule vcg_lemmas[OF marker])›)
Is there a simple solution that I am missing? I know I can abstract over terms but the type-checking does not allow me to mix
them as I would like.
The obvious solution to me is to have an overloadable constant but using that as the marker in the tactic does not work as
I expected. The tactic never matches over the overloadable marker. Is there a way to obtain this behavior from Eisbach?
Wishful thinking example below.
consts marker :: "('s ⇒ bool) ⇒ ('s ⇒ bool)"
overloading
marker_state ≡ marker
marker_lock ≡ marker
...
lemma STATE_vcg [vcg_lemmas]:
assumes pre: "marker_state P s" and spec: "hoare P' M Q'"
...
lemma LOCK_vcg [vcg_lemmas]:
assumes pre: "marker_lock lid" and spec: "hoare P' M Q'"
...
method vcg = ... (match premises in marker [thin]: "marker P" for P ⇒ ‹(rule vcg_lemmas[OF marker])›)
Thanks for the help
Edoardo
Last updated: Jul 26 2025 at 12:43 UTC