Isabelleの非常に単純な補題

Question

私はちょうどIsabelleとの最初のステップを開始していますが、定理証明者と証明補助人には新しく、少し失われています。私は主に機能解析や代数への応用に興味があります。ドキュメンテーションを見ましたが、ロケールを使って独自の例を得ようとしていますが、いくつかの非常に基本的な問題に遭遇しました。私のコードは

theory MyTheory 
imports Main 
begin 

locale semigroup_mult = 
    fixes f :: "'a ⇒ 'a ⇒ 'a" (infixl "x" 70) 
    and e :: 'a ("e") 
    assumes assocm : "a x b x c = a x (b x c)" 
    and right_neutralm : "(a x e) = a" 
    and left_neutralm : "(e x a) = a" 
begin 

lemma assoc_general: "b x (a x c) = (b x a) x c" 
    apply (rule assocm) 
    done 

end 

end 

これは証明ちょうど一歩ですが、私はイザベルが動作することはできません...私は適用行を削除した場合、それは証明を完了することはできませんと言うと、applyコマンドはエラーを与えています

「証明」モードでの証明コマンドの不正なアプリケーション

私が間違って何をしているのですか？どんな助けもありがとう。例えば、 "show ... by"構文と "apply"構文、 "proof ... qed"と "done"の使用の違いです。

二次問題は、Isabelleが学部の数学の教科書に見られるものと同様の証明を出力できるかどうかです。

Answer 1

私はイザベル/ jEditの（Isabelle2016）を使用してコードをしようとすると、私はエラーメッセージ

を取得するには、証明method⌂を適用するために失敗しました：
目標（1つのサブゴール）：
1. BX（AXC） =

bxaxc現在のサブゴールに与えられたルール（assocm）を適用することができなかったことを教えてくれる。その理由は、ruleがassocm（これは補題全体である）の結論を現在の副目標に統一しようとするからです。成功すれば、現在の副目標を補題の仮定で置き換えますが、あなたの例では成功しません。

二つの方法があります周り：

1）あなたはスワップ左側と右側であなたの補題を言い換えることができます。あなたの現在の証明はうまくいくはずです（たぶん、assocmと同じです）。

2）実際には "equal equals by equals"と置き換えたい場合、ruleではなく、simpまたはautoを使用してください。例えば。最初ちょうどその右側でassocmの左側を置き換え、最終的に平等の再帰性によって証拠を終了二つのステップ

unfolding assocm 
by (rule HOL.refl) 

で

apply (simp add: assocm) 

または代わりに。

あなたの二次的な質問に答えるには：任意の証明をいくつかの教科書に類似したものに自動的に変換することはできません。ただし、十分な努力とsimp、blast、およびのような自動ツールを適切に設定すると、そのようなスタイル（Isar構文の範囲内）でプルーフを書くことが可能です。例えば。次の例では、証明はより人間読みやすくするいくつかイザールの特徴を示しています。

lemma "(b x e) x e x (a x c) = b x a x c" 
    by (simp add: right_neutralm assocm) 

：しかし

lemma "(b x e) x e x (a x c) = b x a x c" 
proof - 
    have "b x e = b" by (rule right_neutralm) 
    then have "(b x e) x e x (a x c) = b x (a x c)" by simp 
    also have "... = b x a x c" by (rule assocm [symmetric]) 
    finally show ?thesis . 
qed 

を、のようなより多くの自動証明のために行くことが一般的です