定理証明手習い (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
で書き換えます
仮引数の置き換えは行いますが関数のときと違って
定理の中身をそのまま渡せばいいので少し単純
どれでもなければそのまま主張を返します
これは失敗