amgm_2 - ATPとCASのこと

　それでは２のべき乗の場合を証明していきます．lemmaの名前とstatementは

lemma amgm_2:
  fixes a m n
  shows "ALL k. 0 <= a k ==> GM a m (2 ^ n) <= AM a m (2 ^ n)"

証明は項数についての帰納法ですが，数列はaとして固定し，その隣接する任意の2^N項についての成立から，隣接する任意の2^(N+1)項についての成立を導きます．その位置の任意性は m の任意性に他ならないので，イニシャルプルーフメソッドには arbitrary: m を付して

proof (induct n arbitrary: m)

と指定します．するとOutputは

proof (state): step 1
goal (2 subgoals):
1. ⋀m. ∀k. 0 ≤ a k ⟹ GM a m (2 ^ 0) ≤ AM a m (2 ^ 0)
2. ⋀n m.
(⋀m. ∀k. 0 ≤ a k ⟹ GM a m (2 ^ n) ≤ AM a m (2 ^ n)) ⟹
∀k. 0 ≤ a k ⟹ GM a m (2 ^ Suc n) ≤ AM a m (2 ^ Suc n)

となり，各サブゴール全体と仮定がmについて全称量化されることが判ります．

　では証明です．まずprint_casesで場合分けの設定を確認します．

cases:
0:
fix m
let "?case" = "GM a m (2 ^ 0) ≤ AM a m (2 ^ 0)"
assume 0.prems: "∀k. 0 ≤ a k"
Suc:
fix n_ m
let "?case" = "GM a m (2 ^ Suc n_) ≤ AM a m (2 ^ Suc n_)"
assume Suc.hyps: "⋀m. ∀k. 0 ≤ a k ⟹ GM a m (2 ^ n_) ≤ AM a m (2 ^ n_)"
and Suc.prems: "∀k. 0 ≤ a k"

　case 0のサブゴールは

  case 0 then show ?case by simp

で解決です．実際

have "GM a m (2 ^ 0) = a (Suc m)" by simp
have "AM a m (2 ^ 0) = a (Suc m)" by simp

が確認できます．

　次は case Suc です．帰納法の変数は上記の通りNにします．

next
  case (Suc N)

この後もprint_casesでは（生成時の）n_のままですが，print_factsを用いると

facts:
:
∀k. 0 ≤ a k
∀k. 0 ≤ a k ⟹ GM a ?m (2 ^ N) ≤ AM a ?m (2 ^ N)
Suc:
∀k. 0 ≤ a k ⟹ GM a ?m (2 ^ N) ≤ AM a ?m (2 ^ N)
∀k. 0 ≤ a k
Suc.hyps: ∀k. 0 ≤ a k ⟹ GM a ?m (2 ^ N) ≤ AM a ?m (2 ^ N)
Suc.prems: ∀k. 0 ≤ a k
assms:
this:
∀k. 0 ≤ a k ⟹ GM a ?m (2 ^ N) ≤ AM a ?m (2 ^ N)
∀k. 0 ≤ a k

のようにNになっています．で，目標は

GM a m (2 ^ Suc N) ≤ AM a m (2 ^ Suc N)

なので，この左辺を GM a m (2^N) と GM a (m+2^N) (2^N) の相乗平均として，項数が2の場合の補題を適用，得られた相加平均の分子の2項に帰納法の仮定を用いれば，AM a m (2^Suc N)となる仕組みです．

　従ってスタートは

  have "GM a m (2 ^ Suc N) = root 2 (GM a m (2 ^ N) * GM a (m + 2 ^ N) (2 ^ N))"

なのですが，どう証明するか．．．こんなときは

　simpやautoの手に余る部分を定理で補う

のが基本です．そこで，まず

proof simp

と試してみると

goal (1 subgoal):
 1. root (2 * 2 ^ N) (setprod a {Suc m..m + 2 * 2 ^ N}) =
    root 2
     (root (2 ^ N) (setprod a {Suc m..m + 2 ^ N}) *
      root (2 ^ N) (setprod a {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}))

まではやってくれますので，根号を消去するための定理を

find_theorems "root (?m * ?n)"
find_theorems "root _ (?x * ?y)"

により

0 < ?m ⟹ 0 < ?n ⟹ root (?m * ?n) ?x = root ?m (root ?n ?x)
0 < ?n ⟹ root ?n (?x * ?y) = root ?n ?x * root ?n ?y

のように見つけ，イニシャルプルーフを

proof (simp add: real_root_mult_exp real_root_mult [symmetric])

と改めれば，サブゴールが根号の付く前の

goal (1 subgoal):
 1. setprod a {Suc m..m + 2 * 2 ^ N} =
    setprod a {Suc m..m + 2 ^ N} *
    setprod a {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}

まで遡れます．