[isabelle] Partial functions



Greetings

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)
where
  "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.

/Jesper





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