Re: [isabelle] bug in application of intro rule for SOME P when its type is a function?
You are the victim of an intensional incompleteness of my implementation
of *polymorphic* higher-order unification: in some situations, where
there are infinitely many possible instantiations of a type variable,
only the simplest one is chosen and the others are ignored. See
details. The solution is to instatiate the type variable by hand:
apply (rule someI2[where 'a = "nat => nat"])
Michael Norrish wrote:
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and