[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.