I'm having trouble matching meta-universally quantified variables in my conclusion in Eisabach with the match command. Let's say I want to match an HOL \<forall> . I can do that as follows:

```
method mymethod =
(match conclusion in "∀x. A x" for A ⇒ blah)
```

And that works fine:

```
lemma "∀x::nat. x + x = 2*x"
apply(mymethod) (* matches, does blah *)
```

However, a similar looking method with an \<And> instead doesn't match:

```
method mymethod2 =
(match conclusion in "⋀x. A x" for A ⇒ blah)
lemma "⋀x::nat. x + x = 2*x"
apply(mymethod) (* fails *)
```

I can kind of see why, since:

```
method debugabit =
(match conclusion in A for A ⇒ ‹print_term A›)
lemma "⋀x::nat. x + x = 2*x"
apply(debugabit)
```

gives:

```
print_term: A: x + x = 2 * x
```

Which obviously doesn't have an explicit \<And>. What ways are there for dealing with this? One solution is that I can match very broadly:

```
method mymethod2 =
(match conclusion in "A x" for A x ⇒ blah)
```

But this is annoying, since it picks up x = a billion things other than the variable I'm interested in, and that was breaking some of my other methods. Are there any suggestions for matching this correctly, or getting a reference to the quantified variable?

(An email thread that may be relevant: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-October/msg00091.html)

Yes, interestingly, the application of `match`

seems to fix the universally quantified variable.

When matching a pattern like `A x`

, you need to make sure that `x`

refers to the `x`

in your conclusion. For this, I think, you need to manually fix the variable and then reference it inside your method application as follows (I’m using `n`

instead of `x`

):

```
lemma
fixes n :: nat
shows "n + n = 2 * n"
apply (match conclusion in "A n" for A ⇒ ‹print_term A›)
```

This correctly prints `λa. a + a = 2 * a`

. Note that fixing the variable only affects the proof; from the outside, `n`

appears as a schematic variable, like if you had explicitly universally quantified it.

Now the above example uses `match`

directly inside `apply`

. What if you wanted to have it in a separate, custom proof method? Then you would have to explicitly communicate the variable to be considered the argument of `A`

to the method (it’s good you have to do that, because it ensures that your proof method is independent of the naming of the argument in the respective conclusion). Here’s how you could achieved that:

```
method print_predicate for n = (match conclusion in "A n" for A ⇒ ‹print_term A›)
lemma
fixes n :: nat
shows "n + n = 2 * n"
apply (print_predicate n)
```

I hope that helps. :smile:

This is helpful information, thanks. Unfortunately, there's still a slight problem with it, which is that I can't refer to the variable `x`

when it's universally quantified in my goal. For instance, your example works well when we have

```
lemma
fixes n :: nat
shows "n + n = 2 * n"
```

but if we have

```
lemma
shows "!!n. n + n = 2 * n"
```

we're kind of out of luck, since we have no name to refer to n with. In this simple example, the solution is very obvious (just use `fix n`

). However, I encounter this situation often where I'm in the middle of an apply-style proof, and my subgoals have all these "un-referable" variables, and I need to break out Isar to get anything done. I encountered the main problem here when trying to create methods to help deal with this

For instance, I encounter this type of situation when I `apply(insert atheorem[of stuff])`

where I haven't filled in all the unknowns in `atheorem`

, or when I `apply(induction)`

(in the inductive hypothesis)

It looks like `apply(atomize)`

might be of some help: https://stackoverflow.com/questions/21430238/how-to-replace-%E2%8B%80-and-%E2%9F%B9-with-%E2%88%80-and-%E2%9F%B6-in-assumption, but I can't quite get it to work on the example I gave...

aha! What I was looking for was `apply(atomize (full))`

(https://stackoverflow.com/questions/53487024/pull-all-occurrences-of-the-induction-variable-into-the-conclusion-in-isabelle). To summarize, this takes meta quantifiers to HOL quantifiers, which (as we started with) might be easier to match over. I'll have to play around, because this feels fairly hack-y, but I'm glad to at least have a solution

Why are you using `apply`

-style?

Personally, I find `apply`

style great for experimenting in order to find concise proof method expressions to be used with `by`

(for example, to come up with something like `by transfer (auto simp del: shift_append simp add: shift_append [symmetric])`

. For the final code, I never use `apply`

but exclusively Isar.

In this case, it's mostly so I can automate the reasoning with `method`

s, but I also find it nicer for certain subgoals to work backwards rather than forwards (for example, when you're repeatedly applying rules, end up with lots of subgoals, and want to know which ones disappear by `auto`

)

I guess dropping into a forward proof in these cases is by far the more maintainable option though

Another case is when I have a very complicated algebraic term, and I want to apply a lot of substitutions. In that case, my Isar proofs get very long very quickly, because I'm having to repeat myself. I find myself in this case a lot

Last updated: Nov 11 2024 at 01:24 UTC