質問する
128 次
2 に答える
2
結合性と可換性に至るまでの推論は、通常、Isabelle で単純化と順序付けられた書き換えを使用して行われます。あなたの例では、結合規則 (左から右への向き)、交換規則、および左交換規則を単純化子に提供します。詳細は、Isabelle/HOL のチュートリアル (セクション 9.1、順列書き換え規則) で説明されています。
次に、整理器は方程式の両辺を、Isabelle の暗黙の項の順序によって決定される正規形に並べ替えます。したがって、再帰性によって等しいことが示されている両側で等しい項が得られます。オペレーターがキャンセル規則も満たしていない限り、このアプローチは 2 番目の例を異なる部分に還元しません。運が良ければ、簡約器はこれらの項の両方を同じ位置で回転させます。という形式の導入規則の束を使用できますa = b ==> a ⊔ c = b ⊔ c。ただし、これはかなり脆弱です。変数の名前を変更すると、順序が変更され、証明が破られる可能性があります。ただし、ccProd可換性もあると思われるので、単純化器にも可換性の法則を追加してください。次に、これらの部分項を最初に正規化し、すべてを解決します。
于 2014-12-03T13:07:49.520 に答える
1
于 2014-12-03T13:08:10.923 に答える