Re: [isabelle] x is a special variable

Dear Michel,
> 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 MHonArc.