let_CONV : term -> thm

SYNOPSIS

Evaluates let-terms in the HOL logic.

DESCRIPTION

The conversion let_CONV implements evaluation of object-language let-terms. When applied to a let-term of the form:

   let v1 = t1 and ... and vn = tn in t

where v1, ..., vn are variables, let_CONV proves and returns the theorem:

   |- (let v1 = t1 and ... and vn = tn in t) = t[t1,...,tn/v1,...,vn]

where t[t1,...,tn/v1,...,vn] denotes the result of substituting ti for v1 in parallel in t, with automatic renaming of bound variables to prevent free variable capture. let_CONV also works on let-terms that bind terms built up from applications of inductive type constructors. For example, if is an arbitrarily-nested tuple of distinct variables v1, ..., vn and is a structurally similar tuple of values, that is equals [t1,...,tn/v1,...,vn] for some terms t1, ..., tn, then:

   let_CONV `let  =  in t`

returns

  |- (let  =  in t) = t[t1,...,tn/v1,...,vn]

That is, the term ti is substituted for the corresponding variable vi in t. This form of let-reduction also works with simultaneous binding of tuples using and.

FAILURE CONDITIONS

let_CONV tm fails if tm is not a reducible let-term of one of the forms specified above.

EXAMPLE

A simple example of the use of let_CONV to eliminate a single local variable is the following:

  # let_CONV `let x = 1 in x+y`;;
  val it : thm = |- (let x = 1 in x + y) = 1 + y

and an example showing a tupled binding is:

  # let_CONV `let (x,y) = (1,2) in x+y`;;
  val it : thm = |- (let x,y = 1,2 in x + y) = 1 + 2

Simultaneous introduction of two bindings is illustrated by:

  # let_CONV `let x = 1 and y = 2 in x + y + z`;;
  val it : thm = |- (let x = 1 and y = 2 in x + y + z) = 1 + 2 + z

SEE ALSO

BETA_CONV, GEN_BETA_CONV, SUBLET_CONV.