証明の流れ

　これで記号の準備が出来ました．証明は項数についての帰納法，すなわち，２の累乗の場合をまず示し，それを元に，Suc n から n への（見かけ上）後ろ向きの帰納法で隙間を埋めます．

　まず，それぞれのstatementを書いてみます．

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

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

このようにsorryと書けばIsarは証明したことにしてくれますので，骨組みを見るのに便利です．なお，fixesでaやm,nのtypeを略せるのは，showsにおけるAM,GMの引数であることからの推量の結果であり，実際にはfixes自体も略せます．