Email Gateway (Aug 22 2022 at 11:44): Email Gateway (Aug 22 2022 at 11:44):From: michel levy <michel.levy@imag.fr>
I am a french beginner in Isabelle.
I write this very short theory with jEdit
theory all
imports Main
begin
lemma "∀ x. P(w,x) ⟹ P(w,a)"
apply(erule_tac x ="a" in allE)
Here I have the goal P(w,a) ==> P(w,a)
oops
lemma "∀ y. P(w,y) ⟹ P(w,a)"
apply(erule_tac y= "a" in allE)
Here I have the unexpected message No such variable in theorem : "?y"
oops
Why this difference between these proofs ?
Email Gateway (Aug 22 2022 at 11:44):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Michel,
the name ("x" and "y" in your examples) refers to variables of the fact
you are using, which is "allE", not to names inside the current goal.
allE: ∀x. ?P x ⟹ (?P ?x ⟹ ?R) ⟹ ?R
As you can see, there is an "x" in "allE", but not "y", hence the error
message.
hope this helps
chris
Email Gateway (Aug 22 2022 at 11:44):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
To clarify further, the "x" Christian is talking about is the so-called schematic variable "?x" occurring in the second assumption, not the bound "x" occurring in the first one. Although the variable's official name is "?x", there is no need to specify the question mark when instantiating it.
Jasmin
Email Gateway (Aug 22 2022 at 11:44):From: Larry Paulson <lp15@cam.ac.uk>
It is worth mentioning that Isabelle is based on a logical framework. Therefore inference rules such as allE are not built in, and variants (e.g. with different variable names) are easily introduced.
Simple examples such as the one you include in your message (there are many in the documentation) are obviously good for learning, but as you gain experience, you will see that Isabelle’s built-in notions of abstraction and generalisation provide ways of plugging values into theorems without having to do low-level reasoning with quantifiers.
Larry Paulson
Last updated: Apr 16 2024 at 16:19 UTC