[isabelle] bug in application of intro rule for SOME P when its type is a function?



It looks to me as if someI2 should successfully eliminate any occurrence of SOME within a term, but the following doesn't work:

  lemma
     "(SOME f::nat => nat. f 2 = 3) 2 = 3"
  apply (rule someI2)

The resulting proof state is

  goal (lemma, 2 subgoals):
   1. ?P ?a
   2. !!x. ?P x ==> (SOME f. f 2 = 3) 2 = 3

(This is even an instance of someI_ex or someI, but neither of these work.)

Is there something wrong with unification that it doesn't see the match?

In the mean-time, what can I do to deal with an analogous situation? I have a term of the form (SOME f. ...) and I want to prove properties of it.

Michael.





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