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)
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
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
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
methods, 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
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: Dec 07 2023 at 08:19 UTC