Email Gateway (Jul 11 2026 at 12:00): Email Gateway (Jul 11 2026 at 12:00):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] Strange effect when matching (intro) + lambda + binders + schematic variable
Dear list,
I recently discovered a quite unexpected effect when matching (using
intro, or the underlying match_tac):
A rule of the form: "FOO (P x) ⟹ FOO (λs. ∃x. P x s)" does not match a
goal of the form "FOO (λs. ∃x. P ∧ ?F)" but it does match "FOO (λs.
∃x. P ∧ F)"
Intuitively, schematicity of goal variables shouldn't influence
matching, isn't it?
Find below a few examples where I explored this effect.
Question: Is this the expected behavior? If yes, why?
I'm currently still exploring workarounds for my situation, but I can
imagine the following might work:
* focus on the goal to fix schematic variable
* more low-level: substitute all schematics by fresh frees, apply
rule, substitute back.
Question: Do the above sound reasonable, or can you think of other
workarounds.
--
Peter
(* Some predicate P that implicitly depends on a state (such as
assertions in Hoare-triples) *)
definition "FOO P ≡ ∀s. P s"
(*
Setup similar to AFP/Separation_Algebra,
abbreviating EXS x. P ≡ λs. ∃x. P x s
*)
lemma FExI: "FOO (P x) ⟹ FOO (λs. ∃x. P x s)"
unfolding FOO_def by blast
schematic_goal "FOO (λs. ∃x. P ∧ ?F)"
apply (intro FExI)
apply (rule FExI) (* Works, but instantiates ?F ↝ ?F5 *)
oops
schematic_goal "FOO (λs. ∃x. P ∧ ?F x s)"
apply (intro FExI)
apply (rule FExI) (* Works, but instantiates ?F ↝ ?F5 *)
oops
(* Testing the prerequisites for the effect *)
(* The schematic variable is required *)
lemma "FOO (λs. ∃x. P ∧ F x)"
apply (intro FExI) (* Works as Expected *)
oops
(* It must not be top-level below the binder *)
schematic_goal
"FOO (λs. ∃x. ?F x)"
"FOO (λs. ∃x. ?G x s)"
(* All work as expected *)
apply (intro FExI) defer
apply (intro FExI) defer
oops
(* There must be a binder *)
lemma FConjI: "FOO P ⟹ FOO Q ⟹ FOO (λs. P s ∧ Q s)"
unfolding FOO_def by blast
schematic_goal "FOO (λs. P ∧ ?F s)"
apply (intro FConjI) (* Works as expected *)
oops
(* There must be a λs. … *)
definition "BAR P ≡ P"
lemma BExI: "P x ⟹ BAR (∃x. P x)" unfolding BAR_def by auto
schematic_goal "BAR (∃x. P ∧ ?F x s)"
apply (intro BExI) (* Works as expected *)
oops
Last updated: Jul 22 2026 at 14:00 UTC