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.