;; Requires sets and alists libraries.

Event: Start with the library "alists".

;; This is a library of events about terms, including substitutions.
;; A TERMP is either a variable or the application of a function
;; symbol to a "proper list" of terms.  Variables and function symbols
;; are introduced with CONSTRAIN.
;; NOTE:  In functions like TERMP that have a flag, it seems to be
;; important to use T and F rather than, say, T and 'LIST.  That's
;; because otherwise, the "worse-than" heuristic will otherwise
;; prevent some necessary backchaining in cases where the hypothesis
;; to be relieved is of the form (TERMP 'LIST ...) and an "ancestor"
;; is of the form (TERMP T ...).
;; Definitions:
;; (deftheory term-defns
;;  (variablep-intro variable-listp termp function-symbol-intro all-vars))
;; (deftheory substitution-defns
;;   (instance var-substp compose apply-to-subst subst
;;    nullify-subst ;; returns a substitution whose range has no variables
;;    ))

Conservative Axiom: variablep-intro (listp (x) → (¬ variablep (x))) ∧ (truep (variablep (x)) ∨ falsep (variablep (x)))

Simultaneously, we introduce the new function symbol variablep.

Definition: variable-listp (x) = if listp (x) then variablep (car (x)) ∧ variable-listp (cdr (x))

else x = nil endif

Theorem: variable-listp-implies-properp variable-listp (x) → properp (x)

Theorem: variable-listp-cons variable-listp (cons (a, x)) = (variablep (a) ∧ variable-listp (x))

Theorem: variable-nlistp (x ≃ nil) → (variable-listp (x) = (x = nil))

Event: Disable variable-listp.

Conservative Axiom: function-symbol-intro function-symbol-p (fn)

Simultaneously, we introduce the new function symbols function-symbol-p and fn.

Definition: termp (flg, x) = if flg

then if variablep (x) then t elseif listp (x) then function-symbol-p (car (x)) ∧ termp (f, cdr (x)) else f endif

elseif listp (x) then termp (t, car (x)) ∧ termp (f, cdr (x))

else x = nil endif

Theorem: termp-list-cons termp (f, cons (a, x)) = (termp (t, a) ∧ termp (f, x))

Theorem: termp-list-nlistp (x ≃ nil) → (termp (f, x) = (x = nil))

Theorem: termp-t-cons flg → (termp (flg, cons (a, x)) = (function-symbol-p (a) ∧ termp (f, x)))

Theorem: termp-t-nlistp (flg ∧ (¬ listp (x))) → (termp (flg, x) = variablep (x))

Event: Disable termp.

Theorem: termp-list-implies-properp termp (f, x) → properp (x)

Definition: all-vars (flg, x) = if flg

then if variablep (x) then list (x)

elseif listp (x) then all-vars (f, cdr (x))

else nil endif elseif listp (x) then append (all-vars (t, car (x)), all-vars (f, cdr (x))) else nil endif Theorem: properp-all-vars properp (all-vars (flg, x))

Theorem: all-vars-list-cons all-vars (f, cons (a, x)) = append (all-vars (t, a), all-vars (f, x))

Theorem: all-vars-t-cons flg → (all-vars (flg, cons (a, x)) = all-vars (f, x))

;; Here is a hack to deal with the flags.

Theorem: all-vars-subsetp-append-hack (flg1 ∧ flg2 ) → (subsetp (all-vars (flg1 , x), append (all-vars (flg2 , x), y))

∧ subsetp (all-vars (flg1 , x), append (y, all-vars (flg2 , x))))

;; The following is used later in the proof of MEMBER-PRESERVES-DISJOINT-ALL-VARS
;; and could conceivably be of use elsewhere.

Theorem: all-vars-flg-boolean flg → (all-vars (flg, x) = all-vars (t, x))

Event: Disable all-vars.

Event: Let us define the theory term-defns to consist of the following events: variablep-intro, variable-listp, termp, function-symbol-intro, all-vars.

;;;;; lemmas about termps

Theorem: variable-listp-set-diff variable-listp (x) → variable-listp (set-diff (x, y))

Theorem: all-vars-variablep (flg ∧ variablep (x)) → (all-vars (flg, x) = list (x))

Theorem: member-variable-listp-implies-variablep ((a ∈ x) ∧ variable-listp (x)) → variablep (a)

;; The following was proved in the course of the final run through the
;; generalization proof.  But in fact it's useful for the next result,
;; especially in the presence of domain-restrict -- so I don't need to
;; enable restrict there any longer.  Similarly for the lemma after
;; that.

Theorem: variable-listp-intersection (variable-listp (x) ∨ variable-listp (y)) → variable-listp (intersection (x, y))

Theorem: variable-listp-domain-restrict variable-listp (domain (s)) → variable-listp (domain (restrict (s, x)))

Theorem: variable-listp-domain-co-restrict variable-listp (domain (s)) → variable-listp (domain (co-restrict (s, x)))

Theorem: termp-range-restrict termp (f, range (s)) → termp (f, range (restrict (s, x)))

Theorem: termp-range-co-restrict termp (f, range (s)) → termp (f, range (co-restrict (s, x)))

Theorem: member-preserves-disjoint-all-vars-lemma (disjoint (y, all-vars (f, x)) ∧ (g ∈ x)) → disjoint (y, all-vars (t, g))

Theorem: member-preserves-disjoint-all-vars (flg ∧ disjoint (y, all-vars (f, x)) ∧ (g ∈ x)) → disjoint (y, all-vars (flg, g))

Theorem: member-all-vars-subsetp (flg ∧ (a ∈ x)) → subsetp (all-vars (flg, a), all-vars (f, x))

Theorem: all-vars-f-monotone subsetp (x, y) → subsetp (all-vars (f, x), all-vars (f, y))

;;;;; substitutions:  definitions

Definition: var-substp (s) = (mapping (s) ∧ variable-listp (domain (s)) ∧ termp (f, range (s)))

Definition: subst (flg, s, x) = if flg

then if x ∈ domain (s) then value (x, s) elseif variablep (x) then x elseif listp (x) then cons (car (x), subst (f, s, cdr (x))) else f endif

elseif listp (x) then cons (subst (t, s, car (x)), subst (f, s, cdr (x))) else nil endif Definition: apply-to-subst (s1 , s2 ) = if listp (s2 )

then if listp (car (s2 ))

then cons (cons (caar (s2 ), subst (t, s1 , cdar (s2 ))), apply-to-subst (s1 , cdr (s2 )))

else apply-to-subst (s1 , cdr (s2 )) endif else nil endif

Definition: compose (s1 , s2 ) = append (apply-to-subst (s2 , s1 ), s2 )

;; Later we may wish to prove correctness of one-way-unify

Definition: instance (flg, term1 , term2 ) ↔ ∃ one-way-unifier (var-substp (one-way-unifier)

∧ (term1 = subst (flg, one-way-unifier, term2 )))

;;;;; substitution lemmas

Theorem: subst-list-cons subst (f, s, cons (a, x)) = cons (subst (t, s, a), subst (f, s, x))

Theorem: subst-list-nlistp (x ≃ nil) → (subst (f, s, x) = nil)

Theorem: subst-t-variablep (flg ∧ variablep (x)) → (subst (flg, s, x)

= if x ∈ domain (s) then value (x, s) else x endif)

Theorem: subst-t-non-variablep flg → (subst (flg, s, cons (fn, x))

= if cons (fn, x) ∈ domain (s) then value (cons (fn, x), s) else cons (fn, subst (f, s, x)) endif)

Theorem: all-vars-subst-lemma (flg ∧ (x ∈ domain (s))) → subsetp (all-vars (flg, value (x, s)), all-vars (f, range (s)))

Theorem: all-vars-subst termp (flg, x) → subsetp (all-vars (flg, subst (flg, s, x)),

append (all-vars (flg, x), all-vars (f, range (s))))

Theorem: subst-occur (flg ∧ (x ∈ domain (s))) → (subst (flg, s, x) = value (x, s))

Theorem: boundp-in-var-substp-implies-variablep (variable-listp (domain (s)) ∧ (¬ variablep (a))) → (a ∉ domain (s))

Theorem: variablep-value-invert (variable-listp (domain (s)) ∧ (x ∈ range (s))) → variablep (value (x, invert (s)))

Theorem: subst-invert (termp (flg, x) ∧ disjoint (domain (s), all-vars (flg, x)) ∧ var-substp (s)) → (subst (flg, s, subst (flg, invert (s), x)) = x)

Theorem: boundp-apply-to-subst (x ∈ domain (apply-to-subst (s1 , s2 ))) = (x ∈ domain (s2 ))

Theorem: mapping-apply-to-subst mapping (s) → mapping (apply-to-subst (s1 , s))

Theorem: alistp-apply-to-subst alistp (apply-to-subst (s1 , s2 ))

Theorem: subst-flg-not-list flg → (((subst (flg, s, x) = subst (t, s, x)) = t)

∧ ((subst (t, s, x) = subst (flg, s, x)) = t))

Theorem: subst-co-restrict (disjoint (x, intersection (domain (s), all-vars (flg, term))) ∧ variable-listp (domain (s)) ∧ termp (flg, term)) → (subst (flg, co-restrict (s, x), term) = subst (flg, s, term))

Theorem: subst-restrict (subsetp (intersection (domain (s), all-vars (flg, term)), x) ∧ variable-listp (domain (s)) ∧ termp (flg, term)) → (subst (flg, restrict (s, x), term) = subst (flg, s, term))

Theorem: termp-value (flg ∧ (x ∈ domain (s)) ∧ termp (f, range (s))) → termp (flg, value (x, s))

Theorem: termp-subst (termp (flg, x) ∧ termp (f, range (s))) → termp (flg, subst (flg, s, x))

Theorem: termp-domain variable-listp (domain (s)) → termp (f, domain (s))

Theorem: domain-apply-to-subst domain (apply-to-subst (s1 , s2 )) = domain (s2 )

Theorem: var-substp-apply-to-subst (termp (f, range (s)) ∧ termp (f, range (sg))) → termp (f, range (apply-to-subst (sg, s)))

Theorem: value-apply-to-subst (g ∈ domain (s)) → (value (g, apply-to-subst (sg, s)) = subst (t, sg, value (g, s)))

Theorem: non-variablep-not-member-of-variable-listp (variable-listp (d) ∧ (¬ variablep (term))) → (term ∉ d)

Theorem: compose-property (variable-listp (domain (s2 )) ∧ termp (flg, x)) → (subst (flg, compose (s1 , s2 ), x) = subst (flg, s2 , subst (flg, s1 , x)))

Theorem: compose-property-reversed (variable-listp (domain (s2 )) ∧ termp (flg, x)) → (subst (flg, s2 , subst (flg, s1 , x)) = subst (flg, compose (s1 , s2 ), x))

Event: Disable compose-property.

Theorem: subst-not-occur (termp (flg, x) ∧ variable-listp (domain (s)) ∧ disjoint (domain (s), all-vars (flg, x))) → (subst (flg, s, x) = x)

Theorem: disjoint-range-implies-disjoint-value ((x ∈ domain (s)) ∧ flg ∧ disjoint (z, all-vars (f, range (s)))) → disjoint (z, all-vars (flg, value (x, s)))

Theorem: disjoint-all-vars-subst (termp (flg, x) ∧ disjoint (z, all-vars (flg, x)) ∧ disjoint (z, all-vars (f, range (s)))) → disjoint (z, all-vars (flg, subst (flg, s, x)))

Theorem: all-vars-variable-listp variable-listp (x) → (all-vars (f, x) = x)

Theorem: variable-listp-append variable-listp (append (x, y)) = (variable-listp (fix-properp (x)) ∧ variable-listp (y))

Theorem: termp-list-append termp (f, append (x, y)) = (termp (f, fix-properp (x)) ∧ termp (f, y))

Theorem: apply-to-subst-append apply-to-subst (sg, append (s1 , s2 )) = append (apply-to-subst (sg, s1 ), apply-to-subst (sg, s2 ))

Theorem: subst-apply-to-subst (flg ∧ (g ∈ domain (s))) → (subst (flg, apply-to-subst (sg, s), g) = subst (flg, sg, value (g, s)))

Theorem: subst-append-not-occur-1 (termp (flg, x) ∧ variable-listp (domain (s1 )) ∧ disjoint (all-vars (f, domain (s1 )), all-vars (flg, x))) → (subst (flg, append (s1 , s2 ), x) = subst (flg, s2 , x))

Theorem: subst-append-not-occur-2 (termp (flg, x) ∧ variable-listp (domain (s2 )) ∧ disjoint (all-vars (f, domain (s2 )), all-vars (flg, x))) → (subst (flg, append (s1 , s2 ), x) = subst (flg, s1 , x))

Theorem: apply-to-subst-is-no-op-for-disjoint-domain (variable-listp (domain (s1 )) ∧ alistp (s2 ) ∧ termp (f, range (s2 )) ∧ disjoint (domain (s1 ), all-vars (f, range (s2 )))) → (apply-to-subst (s1 , s2 ) = s2 )

Theorem: member-subst (flg ∧ (a ∈ x)) → (subst (flg, s, a) ∈ subst (f, s, x))

Theorem: subsetp-subst subsetp (x, y) → subsetp (subst (f, s, x), subst (f, s, y))

Event: Disable instance.

;;;(disable compose) -- COMPOSE is left enabled for use with COMPOSE-PROPERTY-REVERSED

Event: Disable apply-to-subst.

Event: Disable subst.

Event: Disable rembind.

Event: Disable bind.

;;;;; nullify-subst:  a substitution that has a range containing
;;                    no variables

Definition: nullify-subst (s) = if listp (s)

then if listp (car (s)) then cons (cons (caar (s), list (fn)), nullify-subst (cdr (s))) else nullify-subst (cdr (s)) endif

else nil endif

Theorem: properp-nullify-subst properp (nullify-subst (s))

Theorem: all-vars-f-range-nullify-subst all-vars (f, range (nullify-subst (s))) = nil

Theorem: termp-range-nullify-subst termp (f, range (nullify-subst (s)))

Theorem: domain-nullify-subst domain (nullify-subst (s)) = domain (s)

Theorem: mapping-nullify-subst alistp (s) → (mapping (nullify-subst (s)) = mapping (s))

Theorem: disjoint-all-vars-subst-nullify-subst termp (flg, term) → disjoint (domain (sg), all-vars (flg, subst (flg, nullify-subst (sg), term)))

Theorem: disjoint-all-vars-range-apply-subst-nullify-subst termp (f, range (s)) → disjoint (domain (sg),

all-vars (f, range (apply-to-subst (nullify-subst (sg), s))))

Event: Disable nullify-subst.

Event: Let us define the theory substitution-defns to consist of the following events: instance, var-substp, compose, apply-to-subst, subst, nullify-subst.

Event: Make the library "terms".

Index

alistp, 6, 8, 9 alistp-apply-to-subst, 6 all-vars, 2–9 all-vars-f-monotone, 4 all-vars-f-range-nullify-subst, 9 all-vars-flg-boolean, 3 all-vars-list-cons, 3 all-vars-subsetp-append-hack, 3 all-vars-subst, 5 all-vars-subst-lemma, 5 all-vars-t-cons, 3 all-vars-variable-listp, 7 all-vars-variablep, 3 apply-to-subst, 5–9 apply-to-subst-append, 8 apply-to-subst-is-no-op-for-dis

joint-domain, 8

boundp-apply-to-subst, 6 boundp-in-var-substp-implies-va

riablep, 6

co-restrict, 4, 6 compose, 5, 7 compose-property, 7 compose-property-reversed, 7

disjoint, 4, 6–9 disjoint-all-vars-range-apply-s

ubst-nullify-subst, 9 disjoint-all-vars-subst, 7 disjoint-all-vars-subst-nullify

-subst, 9 disjoint-range-implies-disjoint

-value, 7 domain, 4–9 domain-apply-to-subst, 7 domain-nullify-subst, 9

exists, 5

fix-properp, 7, 8 fn, 2, 9 function-symbol-intro, 2 function-symbol-p, 2

instance, 5

intersection, 4, 6

invert, 6

mapping, 4, 6, 9

mapping-apply-to-subst, 6 mapping-nullify-subst, 9 member-all-vars-subsetp, 4 member-preserves-disjoint-all-v

ars, 4

ars-lemma, 4 member-subst, 8 member-variable-listp-implies-v

ariablep, 3

non-variablep-not-member-of-vari

able-listp, 7 nullify-subst, 9

properp, 1–3, 9 properp-all-vars, 3 properp-nullify-subst, 9

range, 4–9 restrict, 4, 6

set-diff, 3

subsetp, 3–6, 8 subsetp-subst, 8 subst, 4–9 subst-append-not-occur-1, 8 subst-append-not-occur-2, 8 subst-apply-to-subst, 8 subst-co-restrict, 6 subst-flg-not-list, 6 subst-invert, 6 subst-list-cons, 5 subst-list-nlistp, 5 subst-not-occur, 7 subst-occur, 6 subst-restrict, 6 subst-t-non-variablep, 5 subst-t-variablep, 5 substitution-defns, 9

term-defns, 3 termp, 2, 4–9 termp-domain, 6 termp-list-append, 8 termp-list-cons, 2 termp-list-implies-properp, 2 termp-list-nlistp, 2 termp-range-co-restrict, 4 termp-range-nullify-subst, 9 termp-range-restrict, 4 termp-subst, 6 termp-t-cons, 2 termp-t-nlistp, 2 termp-value, 6

value, 4–8 value-apply-to-subst, 7 var-substp, 4–6 var-substp-apply-to-subst, 7 variable-listp, 1–4, 6–8 variable-listp-append, 7 variable-listp-cons, 1 variable-listp-domain-co-restri

ct, 4 variable-listp-domain-restrict, 4 variable-listp-implies-properp, 1 variable-listp-intersection, 4 variable-listp-set-diff, 3 variable-nlistp, 2 variablep, 1–7 variablep-intro, 1 variablep-value-invert, 6