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



Michael,

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 http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ctrs90.html for details. The solution is to instatiate the type variable by hand:

  apply (rule someI2[where 'a = "nat => nat"])

Tobias

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:

  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.