free_in : term -> term -> bool

- STRUCTURE
- SYNOPSIS
- Tests if one term is free in another.
- DESCRIPTION
- When applied to two terms t1 and t2, the function free_in returns true if t1 is free in t2, and false otherwise. It is not necessary that t1 be simply a variable. A term M occurs free in N when there is some occurrence of M in N such that each free variable of M in that occurrence is not bound by a binder in N.
- FAILURE
- Never fails.
- EXAMPLE
- In the following example free_in returns false because the x in SUC x in the second term is bound:whereas the following call returns true because the first instance of x in the second term is free, even though there is also a bound instance:
- free_in ``SUC x`` ``!x. SUC x = x + 1``; > val it = false : bool

- free_in ``x:bool`` ``!y. x /\ ?x. x = y``; > val it = true : bool

- SEEALSO

HOL Kananaskis-14