Re: [isabelle] Better way to beta apply two terms



On Fri, 26 Aug 2011, Steve Wong wrote:

What is a better way to beta-apply two terms without using betapply, which
can cause a type mismatch. For example:

consts
a :: nat
F :: "'a => nat"
ML {*
val ftrm = @{term "F"};
val atrm = @{term "a"};
val res = betapply((ftrm,atrm));
type_of res
*}

The application succeeds, but the resulting term isn't well-typed (thus type_of fails). betapply doesn't seem to change the input type of F from a variable to "Nat.nat". Is there a better way of beta applying such that the input type can automatically be updated?

Term.betapply is not used that often, although there is nothing wrong with it. Other term constructions (even plain Abs and $) are used more frequently.

The experiment above has failed for other reasons: the example terms are internalized independently, i.e. the system did not know they are correlated. Normally you use something like Syntax.read_terms, Syntax.check_terms or even Specification.read_specification / check_specification for simultaneous processing of formal input in an shared syntactic context.

An alternative is to compose untyped preterms (using dummyT) in some places and then let Syntax.check_term(s) work out the details. (It also requires some care because many basic term operations assume fully typed terms.)

Another note concerning readability of ML sources: "ftrm" and "atrm" are rather long and unwieldy names for plain formal entities that could be just called "f" and "a", or "t" and "u".


	Makarius





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