Isabelle/Isar（その11）

　前回２つのproofコマンドの引数ととしたmethodは，simpとrule 1でした．

　simpは見ての通り計算も出来ますし

lemma "A & B --> A" by simp

のようにロジックも解し，かなり多才ですがあまり深いことは出来ません．例えば

lemma "(0::real) <= x ^ 2 + 1" by simp

は通りますが

lemma "(0::real) <= x ^ 2 + x + 1" by simp

のOutputは

Failed to finish proof

です．なお，simpがどのように証明に成功し，失敗しているかを見るには証明の外，すなわち，theoryモード内で

declare [[simp_trace]]

として，トレースをオンにします．すると１つ目の場合には

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
0 ≤ x² + 1
[1]Applying instance of rewrite rule "Groups.ordered_comm_monoid_add_class.add_nonneg_nonneg":
0 ≤ ?a1 ⟹ 0 ≤ ?b1 ⟹ 0 ≤ ?a1 + ?b1 ≡ True
[1]Trying to rewrite:
0 ≤ x² ⟹ 0 ≤ 1 ⟹ 0 ≤ x² + 1 ≡ True
simp_trace_depth_limit exceeded!
simp_trace_depth_limit exceeded!
[1]SUCCEEDED
0 ≤ x² + 1 ≡ True

２つ目の場合には

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
0 ≤ x² + x + 1
[1]Applying instance of rewrite rule "Groups.ordered_comm_monoid_add_class.add_nonneg_nonneg":
0 ≤ ?a1 ⟹ 0 ≤ ?b1 ⟹ 0 ≤ ?a1 + ?b1 ≡ True
[1]Trying to rewrite:
0 ≤ x² + x ⟹ 0 ≤ 1 ⟹ 0 ≤ x² + x + 1 ≡ True
simp_trace_depth_limit exceeded!
[1]FAILED
0 ≤ x² + x ⟹ 0 ≤ 1 ⟹ 0 ≤ x² + x + 1 ≡ True
Failed to apply initial proof method:
goal (1 subgoal):
0 ≤ x² + x + 1
1. 0 ≤ x² + x + 1

と表示されるはずです．同様に今回の証明の各所にあるsimpにカーソルを合わせるとsimpが参照している定理などが表示されますが，トレースの後は

declare [[simp_trace=false]]

としておかないとシステムの負荷が大きくなります．なお，simpの手に余ったこのレンマの証明にはcsdpを用いるか，中間の目標をhaveコマンドで設定，それにグレブナー基底による代数計算methodであるalgebraを適用した後，simpすれば

lemma "(0::real) <= x ^ 2 + x + 1"
proof -
  have "x ^ 2 + x + 1 = (x + 1 / 2) ^ 2 + 3 / 4"
    by algebra
  thus ?thesis by simp
qed

となります．

　もう１つのruleコマンドは，apply-doneスタイルの基本ですが，Isarではsimp add:に吸収されており

proof (simp add: 1)

とすることもできます．