[isabelle] Avoid variable's capture



Hello everybody,
in a proof I used the "cases" method and it introduces a new universal
quantification on the variable 'a', but this variable already exists so I
can't fix it. I must fix a new variable 'k' and rewrite the later "assume"
and "show" replacing 'a' with 'k'.

In other words:

       (have) P1 ==> P2             (* in P1 and P2 there are some
occurrences of an already fixed variable 'a' *)
apply (cases ad)
       (produces) \<And>a. P1 ==> P2
(* now I can't execute "fix a; assume P1; show P2" because this 'a' capture
the already existing 'a' in P1 and P2 *)

There is a way to avoid the introduction of an already existing variable?

Thanks
Gabriele




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.