Section 2.7 of the Eisbach User Manual presents the reverse matching technique. I wanted to try it out and came up with the following example:
lemma "(⋀n m. Suc n = m) ⟹ False"
apply (
match premises in P for P ⇒ ‹
match ("Suc 1 = 1") in P ⇒ ‹
match premises in prems: _ ⇒ ‹
print_fact prems,
print_term P
›
›
›
)
I would have expected both printing methods to show Suc 1 = 1
, but instead I get the following output:
print_fact: prems: Suc ?n15 = ?m15
print_term: P: Suc ?n11 = ?m11
Is reverse matching not working (anymore), or am I missing something?
It seems that also the example in the user manual is at least not working as I understood it should: instantiation of schematic variables is not persistent. This is the example:
lemma
assumes asms: "⋀x :: 'a. A x"
shows "A y"
apply (match asms in H: "A y" ⇒ ‹rule H›)?
apply (
match asms in H: P for P ⇒ ‹
match ("A y") in P ⇒ ‹rule H›
›
)
done
Inserting diagnostic commands similar to the ones in my post above next to the rule H
invocation will result in output containing a schematic variable instead of y
. Now let’s restrict the type of the variable and replace y
by a constant:
lemma
assumes asms: "⋀x :: nat. A x"
shows "A y"
apply (match asms in H: "A y" ⇒ ‹rule H›)?
apply (
match asms in H: P for P ⇒ ‹
match ("A 0") in P ⇒ ‹rule H›
›
)
done
This code still works, which again illustrates that the x
from the assumption did not get bound beyond the actual matching activity, since otherwise rule H
would have been specialized to A 0
, making it impossible to prove A y
with it.
Last updated: Dec 07 2024 at 16:22 UTC