[isabelle] Partial functions


I am trying out the new functions package which shipped with Isabelle 2007. The
function I am trying to create a function for parallel substitution where I
want to reason about the domain and range of the substitution at top level,
i.e. I want to be able to write P[xvec:=Tvec] where xvec and Tvec are lists
rather than P[S] where S is a tuple list. The problem with this approach is
that the function is only defined if the lists xvec and Tvec are of the same
length. I tried writing the following function:

function (domintros) substName :: "name => name list => trm list => trm"
("_[_:=_]" [100, 100, 100] 100)
  "substName a [] [] = (Name a)"
| "length xs = length Ts ==> substName a (x#xs) (T#Ts) = (if a = x then T else
(substName a xs Ts))"

But at the top of the proof obligations I get a goal which seems pretty
unsolvable to me:

/\P x. [|a. x = (a, [], []) ==> P;
         /\xs Ts a xa T. [|length xs = length Ts;
                           x = (a, xa # xs, T # Ts)|] ==> P|]
       ==> P
It seems to be some sort of completeness condition for the function.

I've read through the guide of the function package and it is a bit unclear if
it is possible to do what I'm trying to do. There are of course work arounds,
but this would be nicer.

Many thanks.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.