1

補題があり、たとえばmylem: foo ?a = bar ?aが 2 回出現するゴールにそれを適用する必要があるとしますが、これらの位置の 1 つだけです。複雑な式になる可能性のある, ...をすべて書き出す必要なく、それを行う 2 つの方法を知っています。foobaz (foo (f p q)) (foo (g r s))pq

  • 適切な数 (ここでは 0 または 1) のコマンドapply (subst mylem)が続きます。back
  • を使用します。apply (subst mylem[where a = 'foo x y', standard])ここで、xおよびyはバインドされていない名前です。

ここでの使用はsubstデモンストレーションのためだけです。私は本当に補題を変更したいと思っています。たとえば、ruleこの方法で曖昧さをなくしたい複数の可能な一致がある場合に使用します。

どちらのアプローチも、私には悪いスタイルに見えます。それを達成するためのより良い方法はありますか？

4

1 に答える 1

1

substどのオカレンスを置き換える必要があるかはわかります。一致する - 番目のオカレンスでsubst (i) mylem展開mylemされます。iこれにより、手順が節約されbackます。のように複数の位置をリストすることもできますsubst (1 2) mylem。mylem敷地内で展開する場合は、 を使用しますsubst (asm) (1 2) mylem。

apply一般に、スクリプト内で目的を達成する方法はわかりません。理論レベルでは、句とともに使用lemmasして、局所的に導入された変数を一般化できます。for

lemmas mylem' = mylem[where a="f x y"] for x y

構造化証明内では、次のように明示的に行うことができます。

{ fix x y note mylem[where a="f x y"] }
note mylem' = this
于 2013-04-09T11:43:57.613 に答える