; We will define what it is to be an expression. ; We will define how to substitute an expression for a variable in an expression. ; We will prove that that produces an expression. ; Example Expressions: X, (F X), (F X (G Y)), (F A (G (G (G (H X Y))))) ; expr := variable | (sym expr-lst) ; expr-lst := {} | expr expr-lst ; Informally, an expression is either a variable symbol or a function symbol ; followed by a list of expressions. (mutual-recursion (defun exprp (x) ; An expression is either a symbol, or a list beginning with a symbol and ; followed by a list of expressions. (if (atom x) (symbolp x) (and (symbolp (car x)) (expr-listp (cdr x))))) (defun expr-listp (x) ; An expression list is either nil or an expression followed by an expression list. (if (atom x) (equal x nil) (and (exprp (car x)) (expr-listp (cdr x)))))) ; Test: (exprp '(F A (G B (H (H (H X)))))) (exprp '(F A (G B (123 (H (H X)))))) (exprp '(F A (G B (H (H (H X . 27)))))) (mutual-recursion (defun subst-expr-for-var (z v x) ; Substitute expression z for variable v in expression x. (cond ((atom x) (if (equal x v) z x)) (t (cons (car x) (subst-expr-for-var-in-expr-list z v (cdr x)))))) (defun subst-expr-for-var-in-expr-list (z v x) (cond ((endp x) nil) (t (cons (subst-expr-for-var z v (car x)) (subst-expr-for-var-in-expr-list z v (cdr x))))))) (subst-expr-for-var '(AAA X Y) 'V '(F A (G V (H (H (H X V)))))) ; This formula is not provable right now... ;(defthm main-theorem ; (implies (and (exprp z) ; (symbolp v) ; (exprp x)) ; (exprp (subst-expr-for-var z v x)))) (defun expr-fn (fn x) ; An expression is either a symbol, or a list beginning with a symbol and ; followed by a list of expressions. (if (equal fn 'expr) (if (atom x) (symbolp x) (and (symbolp (car x)) (expr-fn 'list (cdr x)))) ; An expression list is either nil or an expression followed by an expression list. (if (atom x) (equal x nil) (and (expr-fn 'expr (car x)) (expr-fn 'list (cdr x)))))) (expr-fn 'expr '(F A (G B (H (H (H X)))))) (defun subst-fn (fn z v x) ; Substitute expression z for variable v in expression x. (if (equal fn 'expr) (cond ((atom x) (if (equal x v) z x)) (t (cons (car x) (subst-fn 'list z v (cdr x))))) (cond ((endp x) nil) (t (cons (subst-fn 'expr z v (car x)) (subst-fn 'list z v (cdr x))))))) (subst-fn 'expr '(AAA X Y) 'V '(F V (G B (H (V V (H X)))))) (defthm very-strong-main (implies (and (expr-fn 'expr z) (symbolp v) (expr-fn fnx x)) (expr-fn fnx (subst-fn fnx z v x)))) ; In the proof of main-theorem below, we use very-strong-main above. ; That use produces this subgoal: ; Goal' ; (IMPLIES (IMPLIES (AND (EXPR-FN 'EXPR Z) ; (SYMBOLP V) ; (EXPR-FN 'EXPR X)) ; (EXPR-FN 'EXPR (SUBST-FN 'EXPR Z V X))) ; (IMPLIES (AND (EXPRP Z) (SYMBOLP V) (EXPRP X)) ; (EXPRP (SUBST-EXPR-FOR-VAR Z V X)))) (defthm expr-revealed (equal (expr-fn fn x) (if (equal fn 'expr) (exprp x) (expr-listp x)))) (defthm subst-revealed (equal (subst-fn fn z v x) (if (equal fn 'expr) (subst-expr-for-var z v x) (subst-expr-for-var-in-expr-list z v x)))) (defthm main-theorem (implies (and (exprp z) (symbolp v) (exprp x)) (exprp (subst-expr-for-var z v x))) :hints (("Goal" :use (:instance very-strong-main (fnx 'expr))))) (defthm main-theorem-list-version (implies (and (exprp z) (symbolp v) (expr-listp x)) (expr-listp (subst-expr-for-var-in-expr-list z v x))) :hints (("Goal" :use (:instance very-strong-main (fnx 'list))))) ; To deal with mutual recursion we usually have two choices: ; (1) eliminate one of the functions in favor of the other -- this is only possible ; if one of the functions calls the other but not itself. ; (2) define a ``dispatcher'' function which mimics both mutually-recursive functions ; and then prove general theorems about the dispatcher and later instantiate them ; Method (2) always works. You can always eliminate mutual recursion by using the ; dispatcher trick.