This is the alpha renaming conversion. It replaces the binding variable and all occurrences of it in the supplied lambda abstraction term (the 2nd argument) with the supplied variable (the 1st argument). The supplied variable must have the same type as the original binding variable, and must not occur free in the original body. `y` `\x. t` ------------------------- |- (\x. t) = (\y. t[y/x])

This is the alpha linking conversion. It takes two alpha-equivalent terms and returns a theorem stating that the second is equal to the first, under no assumptions. Fails if the supplied terms are not alpha-equivalent. `t'` `t` ---------- |- t = t'

This rule is for expanding a function defined in terms of a lambda abstraction. It takes an equality theorem and a term argument, where the theorem RHS is a lambda abstraction with a binding variable of the same type as the term argument. It returns a theorem stating that the theorem argument's LHS applied to the term argument is equal to the beta reduction of the lambda abstraction applied to the term argument. A |- f = (\v. t) `s` ---------------------- A |- f s = t[s/v]

app_beta_rule : thm -> term -> thm A |- (\v1. t1) = (\v2. t2) `s` -------------------------------- A |- t1[s/v1] = t2[s/v2]

The internal constant for let-expressions is called "LET". It has special support in the parser/printer, so that the quotation `let x1 = s1 and x2 = s2 in t` is parsed/printed for the internal term `LET (LET (\x1 x2. t) s1) s2`. |- LET = (\(f:'a->'b) x. f x)

Force module evaluation

This is the equality congruence rule for function application functions. It takes an equality theorem over functions and a term, and supplies the term as the argument to each side of the theorem. The type of the supplied term must be the same as the domain type of the functions. A |- f1 = f2 `t` ------------------ A |- f1 t = f2 t See also: mk_comb2_rule, mk_comb_rule.

This is the equality congruence rule for function application arguments. It takes a function term and an equality theorem, and applies the function to each side of the theorem. The domain type of the supplied function must be the same as the type of the theorem LHS/RHS. `f` A |- t1 = t2 ------------------ A |- f t1 = f t2 See also: mk_comb1_rule, mk_comb_rule.

ONTO |- ONTO = (\(f:'a->'b). !y. ?x. y = f x)

This is the basic substitution conversion. It takes a list of equality theorems and a term, and transforms the term by performing a single parallel substitution of its free subterms according to the equality theorems. All free occurrences of equality theorem LHSs in the term get replaced. The resulting theorem has the unioned assumptions of all the supplied theorems (regardless of whether they apply to the supplied theorem). Binding variables in the resulting theorem's RHS are renamed as necessary to avoid variable capture. Note that if one equality theorem's LHS occurs free in another's, then the theorem with the larger LHS gets used in preference, and if two equality theorems have alpha-equivalent LHSs, then the earlier theorem in the list gets used in preference. If no equality theorems apply, then the returned theorem's conclusion's RHS is the same as its LHS. A1 |- s1 = t1 A2 |- s2 = t2 .. `t` ---------------------------------------- A1 u A2 u .. |- t = t[t1/s1,t2/s2,..] See also: subs_rule, subst_conv, inst_rule.

This is the basic substitution rule. It takes a list of equality theorems and a theorem, and performs a single parallel substitution of free subterms in the theorem's conclusion according to the equality theorems. All free occurrences of equality theorem LHSs in the theorem get replaced. The resulting theorem has the unioned assumptions of all the supplied theorems (regardless of whether they apply to the supplied theorem). Binding variables in the resulting theorem are renamed as necessary to avoid variable capture. Note that if one equality theorem's LHS occurs free in another's, then the theorem with the larger LHS gets used in preference, and if two equality theorems have alpha-equivalent LHSs, then the earlier theorem in the list gets used in preference. If no equality theorems apply, then the returned theorem's conclusion is the same as the input's. A1 |- s1 = t1 A2 |- s2 = t2 .. A |- t -------------------------------------------- A1 u A2 u .. |- t[t1/s1,t2/s2,..] See also: subs_conv, subst_rule, inst_rule.

This is the template substitution conversion. It takes a substitution scheme (in the form of an association list and a template term) followed by a main term, and transforms the main term by performing a single parallel substitution of its free subterms, according to the substitution scheme. The template term determines which free occurrences of equality theorem LHSs in the main term get replaced, and reflects the syntactic structure of the term, except having template variable atoms in place of subterms due for replacement. The association list maps each template variable to an equality theorem, with equality theorem LHS for the main term's original subterm and RHS for the subterm that replaces it. The resulting theorem has the unioned assumptions of all the supplied theorems (regardless of whether they apply to the supplied template). Binding variables in the resulting theorem are renamed as necessary to avoid variable capture. Note that if two entries appear in the association list for the same template variable, then the earlier entry gets used, and that entries for variables that don't appear in the template are ignored. If no entries apply, then the returned theorem's conclusion's RHS is the same as its LHS. `v1` `v2` .. A1 |- s1 = t1 A2 |- s2 = t2 .. `t` `t[s1/v1,s2/v2,..]` -------------------------------------------------------------- A1 u A2 u .. |- t[s1/v1,s2/v2,..] = t[t1/v1,t2/v2,..] See also: subst_rule, subs_conv, inst_rule.

This is the template substitution rule. It takes a substitution scheme (in the form of an association list and a template term) followed by a theorem, and performs a single parallel substitution of free subterms in the theorem's conclusion, according to the substitution scheme. The template term determines which free occurrences of equality theorem LHSs in the supplied theorem get replaced, and reflects the syntactic structure of the theorem's conclusion, except having template variable atoms in place of subterms due for replacement. The association list maps each template variable to an equality theorem, with equality theorem LHS for the supplied theorem's original subterm and RHS for the subterm that replaces it. The resulting theorem has the unioned assumptions of all the supplied theorems (regardless of whether they apply to the supplied template). Abstraction variables in the resulting theorem are renamed as necessary to avoid variable capture. Note that if two entries appear in the association list for the same template variable, then the earlier entry gets used, and that entries for variables that don't appear in the template are ignored. If no entries apply, then the returned theorem's conclusion is the same as the input's. `v1` `v2` .. A1 |- s1 = t1 A2 |- s2 = t2 .. `t` A |- t[s1/v1,s2/v2,..] ----------------------------------------------------------------- A1 u A2 u .. |- t[t1/v1,t2/v2,..] See also: subst_conv, subs_rule, inst_rule.

This is the symmetry rule for equality. It swaps the LHS with the RHS in the supplied equality theorem. A |- t1 = t2 ------------ A |- t2 = t1 See also: sym_conv, refl_conv, trans_rule.

This is the transitivity rule for equality. It takes two equality theorem arguments, where the first theorem's RHS is the same (modulo alpha- equivalence) as the second theorem's LHS. It returns a theorem stating that the first theorem's LHS equals the second theorem's RHS, under the unioned assumptions of the two theorems. A1 |- t1 = t2 A2 |- t2 = t3 ------------------------------ A1 u A2 |- t1 = t3 See also: list_trans_rule, refl_conv, sym_rule, imp_trans_rule.