定理証明手習い (87) equality/def

パターンに分けてequality/pathを呼びます

(defun equality/def (claim path app def)

claim 主張
path フォーカスへのパス
app 関数適用
def 定義

  (if (rator? def)
      (equality/path
       claim path
       (app-c 'equal (list2 app (eval-op app))))

defが組み込み関数なら
主張のフォーカスをappとその値を使って書き換えます
(equality/path e path thm)という引数の名前を尊重すると、
関数適用と、その値が等しいという定理を即席で作ってることになりますね
equality/pathは（というかequalityは）両方向への書き換えが可能なので
関数適用を値に置き換えるだけでなく、値を関数適用に置き換えることもできます
そういうのも出てきました

ところでdefには単にcarとかが入ってくるってことですよね
(car x y)とかじゃrator?にならないもんなあ

次

      (if (defun? def)
          (equality/path
           claim path
           (sub-e (defun.formals def)
                  (app.args app)
                  (app-c 'equal
                         (list2 (app-c (defun.name def)
                                       (defun.formals def))
                                (defun.body def)))))

defが関数定義なら
主張のフォーカスをdefで書き換えます
ただしそのままではなく、関数定義本体の仮引数をappの実引数に置き換えて
これも双方向いけます

最後

          (if (dethm? def)
              (equality/path
               claim path
               (sub-e (dethm.formals def)
                      (app.args app)
                      (dethm.body def)))
              claim))))

defが定理なら
主張のフォーカスをdefで書き換えます
仮引数の置き換えは行いますが関数のときと違って
定理の中身をそのまま渡せばいいので少し単純

どれでもなければそのまま主張を返します
これは失敗