[isabelle] Changing the arity of a term in ML


Say, given the terms

val trm = @{term "%(a::nat => nat) b. a = b"}
val arg = @{term "c::nat=>nat"}
val arg' = @{term "d::nat=>bool"}

if I'd like to create a new term in ML, which is essentially the same
as "trm $ arg' " but 'a' and 'b' are to have the type "nat => bool"
instead, I could change the type of every term in the trm part to
dummyT (call it trm') and call Syntax.check_term on "trm' $ arg' " to
reconstruct the types for the trm' part.

Now, what if I want to decrease the arity of "a" and "b", e.g., from
"nat => nat" to "nat"? I can't seem to use the same method. In trm,
the = operator takes two lambda abstracted terms as arguments, but if
'a' and 'b' are to be of type 'nat', then = should take two bound
variables instead.

Is there a nice way to manipulate the type in this kind of situations
such that the arity is decreased?

Thanks a lot for the time.


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