|
|
|---|
|
|
|
|---|
Set of free variables in a (translated) term.
(tterm-free-vars term) → vars
Even though ACL2 internally closes all lambda expressions, in our formalization of translated terms we do not assume or enforce that. In fact, we want to have more flexibility, and allow non-closed lambda expression. Thus, the free variables of a lambda expression, as common in other languages, are the ones in the body minus the formal parameters.
Theorem:
(defthm return-type-of-tterm-free-vars.vars (b* ((?vars (tterm-free-vars term))) (symbol-value-setp vars)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-tfunction-free-vars.vars (b* ((?vars (tfunction-free-vars fun))) (symbol-value-setp vars)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-tterm-list-free-vars.vars (b* ((?vars (tterm-list-free-vars terms))) (symbol-value-setp vars)) :rule-classes :rewrite)
Theorem:
(defthm tterm-free-vars-of-tterm-fix-term (equal (tterm-free-vars (tterm-fix term)) (tterm-free-vars term)))
Theorem:
(defthm tfunction-free-vars-of-tfunction-fix-fun (equal (tfunction-free-vars (tfunction-fix fun)) (tfunction-free-vars fun)))
Theorem:
(defthm tterm-list-free-vars-of-tterm-list-fix-terms (equal (tterm-list-free-vars (tterm-list-fix terms)) (tterm-list-free-vars terms)))
Theorem:
(defthm tterm-free-vars-tterm-equiv-congruence-on-term (implies (tterm-equiv term term-equiv) (equal (tterm-free-vars term) (tterm-free-vars term-equiv))) :rule-classes :congruence)
Theorem:
(defthm tfunction-free-vars-tfunction-equiv-congruence-on-fun (implies (tfunction-equiv fun fun-equiv) (equal (tfunction-free-vars fun) (tfunction-free-vars fun-equiv))) :rule-classes :congruence)
Theorem:
(defthm tterm-list-free-vars-tterm-list-equiv-congruence-on-terms (implies (tterm-list-equiv terms terms-equiv) (equal (tterm-list-free-vars terms) (tterm-list-free-vars terms-equiv))) :rule-classes :congruence)