step

　次は，step ケースです．

next
  case (step i a)

先述の通り，帰納法の変数はi，目標の数列はaとします．証明の流れは，letを用いて，項数がi+1である数列?bを ?b k = a k (k=1,...,i)，GM a 0 i (k=i+1)のように設定，帰納法の仮定 step.IH を適用して，以下は代数計算です．

　ということで

  let ?b = "%k. if k <= i then a k else GM a 0 i"

と設定，GM a 0 (Suc i) の根号内を

  have "setprod ?b {1..Suc i} = setprod a {1..i} * GM a 0 i"

と分解します．ただし，前半とは違い区間への分解ではなく，１つの項を分離（右辺から見れば挿入）するだけであり，幸い？

thm "Big_Operators.comm_monoid_mult_class.setprod.insert"

finite ?A ⟹ ?x ∉ ?A ⟹ setprod ?g (insert ?x ?A) = ?g ?x * setprod ?g ?A

にはsimp属性が付いていますので，定理自体の明示は不要で

    by (subgoal_tac "{1..Suc i} = insert (Suc i) {1..i}", auto)

で通ります（右辺は union {1..i} {Suc i} でも構いません）．なお，?b の定義は

(∏k = 1..Suc i. if k ≤ i then a k else GM a 0 i)

のように直ちに適用されます．

　続いて，右辺の第１因子が GM a 0 i ^ i，また，x ^ i * x = x ^ Suc i（こちらはsimpも知っている"Power.power_class.power.simps_2"）なので

  also have "... = GM a 0 i ^ Suc i"

と書き換えたいのですが，これは根号の消去ですので，根号内つまり左辺が非負であることが必要となり， GMge0 と同じく

    using step.prems

すなわち

using this:
∀k. 0 ≤ a k
0 < i

のもとで

    by (simp add: setprod_nonneg)

とすれば通ります．なお，theory mode で declaresimp_trace しておくと，根号の消去自体は

[1]Applying instance of rewrite rule "NthRoot.real_root_pow_pos2":
0 < ?n1 ⟹ 0 ≤ ?y ⟹ root ?n1 ?y ^ ?n1 ≡ ?y

のように自動的に適用されていることが確認できます．

　従って

  finally have "GM ?b 0 (Suc i) = GM a 0 i"

と行きたいのですが，根号内が累乗のタイプのreal_root_power_cancel(real_root_pos2)

0 < ?n ⟹ 0 ≤ ?x ⟹ root ?n (?x ^ ?n) = ?x

はsimp属性を持たないので

    using real_root_power_cancel [of "Suc i", OF _ GMge0 [OF step.prems, of 0]]

すなわち

using this:
(∏k = 1..Suc i. if k ≤ i then a k else GM a 0 i) = GM a 0 i ^ Suc i
0 < Suc i ⟹ root (Suc i) (GM a 0 i ^ Suc i) = GM a 0 i

と指定した後

    by simp

とすれば通ります．

　そして ?b に帰納法の仮定

thm step.IH

∀k. 0 ≤ ?a k ⟹ 0 < Suc i ⟹ GM ?a 0 (Suc i) ≤ AM ?a 0 (Suc i)

を用いる為の

  moreover have "ALL k. 0 <= ?b k"

です．これは

thm step.prems GMge0

∀k. 0 ≤ a k
0 < i
∀k. 0 ≤ ?a k ⟹ 0 < ?n ⟹ 0 ≤ GM ?a ?m ?n

の参照でよい訳ですが，metisでもデフォルトでは難しく，検索範囲を拡大して

    by (metis (full_types))

とせねばなりません．simpに任せるには更に補助が入用で

    using step.prems(1) GMge0 [OF step.prems, of 0]
    by simp

といった具合になります．

　これで

  ultimately have "GM a 0 i <= (i * AM a 0 i + GM a 0 i) / Suc i"
    using step.IH [of ?b]

using this:
GM (λk. if k ≤ i then a k else GM a 0 i) 0 (Suc i) = GM a 0 i
∀k. 0 ≤ (if k ≤ i then a k else GM a 0 i)
∀k. 0 ≤ (if k ≤ i then a k else GM a 0 i) ⟹
0 < Suc i ⟹
GM (λa. if a ≤ i then a a else GM a 0 i) 0 (Suc i)
≤ AM (λa. if a ≤ i then a a else GM a 0 i) 0 (Suc i)

goal (1 subgoal):
1. GM a 0 i ≤ (real i * AM a 0 i + GM a 0 i) / real (Suc i)

のように出揃いましたので，

      by simp

とします．