定理証明手習い (86) follow-premsの復習とequality/path

(app-of-equal e) equalの適用か
(equality focus a b) focusを書き換えられる式
(equality/equation focus concl-inst) 帰結でフォーカスを書き換える

conclはきっとconclusionでDethmの法則でいうところの帰結のこと

次の場合、置き換えた結果であるbody(e)を使ってフォーカスの書き換えができる。

• body(e)は、(equal p q)または(equal q p)という 帰結 を含む。

instはなんだろう？instance？
はずれではない気もするけどぴったりかというと・・・

次は文脈から言って

(equality/path e path thm) pathが指す部分式をthmの表す定理で置き換える

のはずだな
ただし、thmは定理と言っても、仮引数が具体化された形になって・・・
あ、だからinstanceなのか
それっぽいな

(defun equality/path (e path thm)
  (if (focus-is-at-path? path e)

pathがeの部分式を指していれば

      (rewrite-focus-at-path
       path e

eの、pathが指す部分式＝フォーカスを置き換える

       (equality/equation (find-focus-at-path path e)
                          (follow-prems path e thm)))

なにでかというと(follow-prems path e thm)で
ここちょっとよくわかってなかったところ
周辺がわかってきたので今ならきっともっとわかる

返してほしいのは帰結
この前はなにかぜんぜん違うことを考えてた気がする

再掲

(defun prem-A? (prem path e)
  (if (atom path)
      'nil
      (if (equal (car path) 'A)
          (if (equal (if.Q e) prem)
              't
              (prem-A? prem (cdr path)
                       (find-focus-at-direction (car path) e)))
          (prem-A? prem (cdr path)
                   (find-focus-at-direction (car path) e)))))

premには、定理の前提(Q部)が入ってきます
フォーカスに至るpathに含まれるA部の前提(Q部)に、premと一致するものがあるか、ということ
prem-E?はE部の前提から探す

(defun follow-prems (path e thm)
  (if (if? thm)
      (if (prem-A? (if.Q thm) path e)
          (follow-prems path e (if.A thm))
          (if (prem-E? (if.Q thm) path e)
              (follow-prems path e (if.E thm))
              thm))
      thm))

定理の前提(Q部)がpathのA側にあるかE側にあるかで分岐しながら
ifじゃなくなるまでたどった先の式(=帰結)を返す

follow-premsは手続き的名前じゃないのか
conclusion-on-pathとかの方がよくないか

結局

その帰結がifのAnswer部（あるいはElse部）に含まれているなら、書き換え対象のフォーカスも同じQuestion部を持つifのAnswer部（あるいはElse部）に含まれていなければならない。

これをやってるってこと
わかった・・・はず

えーとちょっと残ってるな

pathがeの部分式を指していなければ

      e))

元のままの式を返す
他の関数も、ちゃんとしてなければどれも書き換えない式を返してます