[isabelle] Avoid variable's capture
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and