[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 220.127.116.11 (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:
"(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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and