Re: [isabelle] x is a special variable
> But why am I obliged to use x in instantiating the quantifier (x = "f a").
> If I use y = "f a" to instantiate the quantifier, I have a message "no
> such variable in theorem".
you can have a look at the theorem using the command "thm allE". The
system will print:
âx. ?P x â (?P ?x â ?R) â ?R
As you can see, the theorem itself uses the variable "x". When
instantiating rules like "x1 = t1", "x2 = t2", ... the variables on the
left-hand side must occur in the theorem you're instantiating.
(I think this also answers your other question.)
PS: Proof methods ending with "_tac" are considered "legacy" and should
only be used if you know what you're doing. If you're a beginner, I
would strongly recommend sticking to modern Isar-style proofs.
This archive was generated by a fusion of
Pipermail (Mailman edition) and