# Re: [isabelle] Partial functions

Jesper,

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

`This is not partiality in the sense of the function package. The special
``support with domain predicate, domintros and all that is for functions
``which have a possibly nonterminating recursion. Here, you simply want to
``omit some cases and leave them undefined in some sense.
`
What you would do is simply
function (sequential) substName :: "name => name list => trm list => trm"
("_[_:=_]" [100, 100, 100] 100)
where
"substName a [] [] = (Name a)"
| "substName a (x#xs) (T#Ts) =
(if a = x then T else (substName a xs Ts))"

`The (sequential) option will add the missing cases and map them to the
``unspecified constant "undefined".
`

`You would only need section 7 from the function tutorial if you function
``had a recursion that could fail to terminate.
`

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.
`

`Yes. And it is unsolvable, because your equations are incomplete. The
``(sequential) option will add the remaining patterns, and you get a
``better proof obligation. (solvable with the usual "by pat_completeness
``auto"). Or, you simply use "fun", which has (sequential) implicit and
``does all proofs for you...
`
Cheers,
Alex

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