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 for 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 MHonArc.