*To*: Michael Norrish <michael.norrish at nicta.com.au>*Subject*: Re: [isabelle] bug in application of intro rule for SOME P when its type is a function?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 15 Jan 2007 08:21:25 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <45AAEA52.6080408@nicta.com.au>*References*: <45AAEA52.6080408@nicta.com.au>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Michael,

apply (rule someI2[where 'a = "nat => nat"]) Tobias Michael Norrish wrote:

It looks to me as if someI2 should successfully eliminate any occurrenceof 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? Ihave a term of the form (SOME f. ...) and I want to prove properties of it.Michael.

**References**:**[isabelle] bug in application of intro rule for SOME P when its type is a function?***From:*Michael Norrish

- Previous by Date: [isabelle] bug in application of intro rule for SOME P when its type is a function?
- Next by Date: [isabelle] Questions about number representation in Isabelle
- Previous by Thread: [isabelle] bug in application of intro rule for SOME P when its type is a function?
- Next by Thread: [isabelle] Questions about number representation in Isabelle
- Cl-isabelle-users January 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list