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.