[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|]
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and