# [isabelle] some problems with the /\ quantifier

I have a certain predicate whose definition is not important for this
question, so assume it is
definition P :: "real â bool"
where "P x = False"
and assume I proved it holds for x's that equal 'real_of_int(y)',
lemma tl1:
fixes x :: real and
y :: int
assumes "x = real_of_int(y)"
shows "P(x)"
sorry
now I want to prove something equivalent but easier to use,
lemma
fixes w :: real
assumes "w \<in> Ints"
shows "P(w)"
I want to use lemma tl1, so I start the proof with
apply (rule_tac q=w in Ints_cases)
apply (rule assms)
after which the goal is
goal (1 subgoal):
1. â z. w = real_of_int z ==> P w
so, the only thing left is to substitute w and z in tl1 :
apply (rule tl1 [of w z])
but this doesn't work as I expected, and I get a new goal with a new
variable za.
goal (1 subgoal):
1. â za. w = real_of_int za ==> w = real_of_int z
what am I doing wrong ?

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