Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Changing the arity of a term in ML

Email Gateway (Aug 19 2022 at 07:49):

From: John Munroe <munddr@gmail.com>
Hi,

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.

John

Email Gateway (Aug 19 2022 at 07:50):

From: Michael Chan <mchan@inf.ed.ac.uk>
Hi John,

Try eta-contracting the terms with Envir.eta_contract. That should
rewrite the lambda abstractions and running Syntax.check_term should
then reconstruct the types accordingly.

HTH

Michael

Last updated: Apr 26 2024 at 12:28 UTC