amgm_0

　後半です．statementは

lemma amgm_0:
  fixes a n
  assumes "0 < n"
  shows "ALL k. 0 <= a k ==> GM a 0 n <= AM a 0 n"

でした．方針は項数がSuc iである任意の数列bでの成立から，項数がiである任意の数列aでの成立を導くというもので，前半は数列を固定し，成立する番号の位置の任意性を利用したのに対して，ここでは，成立する番号は1からに固定し，数列bの任意性を利用するので，induction には arbitrary: a（このaは上でfixesされたaの位置にあるものということ）を付し，前回の inc_inductをrule とします．

using exn2n assms
proof (induction n arbitrary: a rule: inc_induct)

なお，inc_inductの ?i <= ?j マッチさせる為に前回の exn2n を，証明本編で用いる GMge0 などの仮定に 0 < n をそれぞれ，using により与えています．

goal (2 subgoals):
1. ⋀a. ∀k. 0 ≤ a k ⟹ 0 < 2 ^ n ⟹ GM a 0 (2 ^ n) ≤ AM a 0 (2 ^ n)
2. ⋀i a.
i < 2 ^ n ⟹
(⋀a. ∀k. 0 ≤ a k ⟹
0 < Suc i ⟹ GM a 0 (Suc i) ≤ AM a 0 (Suc i)) ⟹
∀k. 0 ≤ a k ⟹ 0 < i ⟹ GM a 0 i ≤ AM a 0 i

また，print_casesの結果は

cases:
base:
fix a
let "?case" = "GM a 0 (2 ^ n) ≤ AM a 0 (2 ^ n)"
assume base.prems: "∀k. 0 ≤ a k" "0 < 2 ^ n"
step:
fix i_ a
let "?case" = "GM a 0 i_ ≤ AM a 0 i_"
assume step.hyps: "i_ < 2 ^ n" and
step.IH:
"⋀a. ∀k. 0 ≤ a k ⟹
0 < Suc i_ ⟹ GM a 0 (Suc i_) ≤ AM a 0 (Suc i_)"
and step.prems: "∀k. 0 ≤ a k" "0 < i_"

なので，base ケースは

  case base then show ?case
    using amgm_2 by metis

とすれば

show GM a 0 (2 ^ n) ≤ AM a 0 (2 ^ n)
Successful attempt to solve goal by exported rule:
(∀k. 0 ≤ ?aa2 k) ⟹
(0 < 2 ^ n) ⟹ GM ?aa2 0 (2 ^ n) ≤ AM ?aa2 0 (2 ^ n)
proof (state): step 6

this:
GM a 0 (2 ^ n) ≤ AM a 0 (2 ^ n)

goal (1 subgoal):
1. ⋀i a.
i < 2 ^ n ⟹
(⋀a. ∀k. 0 ≤ a k ⟹
0 < Suc i ⟹ GM a 0 (Suc i) ≤ AM a 0 (Suc i)) ⟹
∀k. 0 ≤ a k ⟹ 0 < i ⟹ GM a 0 i ≤ AM a 0 i

と解決します．