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 2023 at 08:19 UTC