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

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] bug in application of intro rule for SOME P when its type is a function?
*From*: Michael Norrish <michael.norrish at nicta.com.au>
*Date*: Mon, 15 Jan 2007 13:43:30 +1100
*Organization*: National ICT Australia
*User-agent*: Thunderbird 1.5.0.8 (X11/20061117)

`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.*