状態が未知の条件付き書き直し規則

Question

私の理論では、より大きな定義があります。そこから補題を使っていくつかの簡単なプロパティを導き出します。

私の問題は、プロパティを導出するための補助定理が簡略化では使用されておらず、手動でインスタンス化する必要があるということです。これをより自動化する方法はありますか？

最小限の例を以下に示します。

definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where 
"complexFact x y z ≡ x = y + z" 

lemma useComplexFact: "complexFact x y z ⟹ x = y + z" 
by (simp add: complexFact_def) 

lemma example_1: 
assumes cf: "complexFact a b c" 
shows "a = b + c" 
apply (simp add: cf useComplexFact) (* easy, works *) 
done 

lemma example_2a: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (simp add: cf useComplexFact) (* does not work *) 
oops 

lemma example_2b: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (simp add: useComplexFact[OF cf]) (* works *) 
done 

lemma example_2c: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (subst useComplexFact) (* manually it also works*) 
apply (subst cf) 
apply simp+ 
done 

私はリファレンスマニュアルの次の段落を見つけたので、私は、私はカスタムソルバーと私の問題を解決することができると思います。 しかし、私は本当にイザベルの内部のMLの部分に触れたことはありませんし、どこから始めるべきか分かりません。

書き換えは未知数をインスタンス化しません。たとえば、 だけを書き直すと、∈Aを証明できません。なぜなら、これをインスタンス化する必要があるからです。しかし、 ソルバーは任意の手法であり、未知数 をインスタンス化することができます。これはSimplifierが条件に余分な変数を含む 条件付き書き換えルールを処理できる唯一の方法です。

Answer 1

Isabelle simplifierは、条件付き書き換えルールの前提で、未知数をインスタンス化しません。しかし、ソルバーはそれを行うことができ、最も信頼性の高いものはassumptionです。したがってcomplex_fact a b cが文字通り（simp add:または[simp]のsimpsetに追加されるのではなく）目的の前提に現れた場合、前提ソルバが起動して未知数をインスタンス化します。ただし、仮定ではcomplex_factの最初のインスタンスのみを使用します。だから、それらのいくつかがある場合、それらのすべてを試みることはありません。要約すると、あなたの例の第2の問題はaとa = b + c、b、およびcが自由であることは、左側にあるため、ヘッドシンボル、良い書き換えルールではないということです

lemma 
    assumes cf: "complexFact a b c" 
    shows "a = b + c" 
    using cf 
    apply(simp add: useComplexFact) 

を書く方が良いです定数ではなく、フリー変数aです。したがって、簡略化子は、式a = b + cを使用してaをb + cに置き換えますが、式a = b + cのリテラルをTrueに置き換えることはできません。この前処理はシンプルファイアのトレースで確認できます（ローカルでusing [[simp_trace]]を有効にしてください）。これが理由で、example_1が動作し、それ以外は動作しません。ヘッドシンボルとして定数があるように左手側を変更することができれば、カスタムソルバを書くことなく、ある程度の立派な証明自動化が可能になるはずです。

さらに、useComplexFactを破壊ルールとして使用して、いくつかの（限定的な）フォワード推論を行うことができます。つまり、

using assms 
apply(auto dest!: useComplexFact) 

でも動作する場合があります。しかし、これはスケーラビリティの定義を展開するのにはかなり近いです。

Answer 2

あなたはそれがこのような[simp]:を付加することで整理を自動的に供給されるべきであることを、あなたの定義で指定することができます。

definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where 
[simp]: "complexFact x y z ≡ x = y + z" 

今、すべてのあなたの例の補題がusing cf by simpと直接解けるはずです。