simps

　計算機を用いた定理証明における楽しみの１つは（参照先が見え難くなりますが）simplifyでしょう．

lemma amgm_2_simps:
  fixes a m n
  shows "ALL k. 0 <= a k ==> GM a m (2 ^ n) <= AM a m (2 ^ n)"
proof (induct n arbitrary: m)
  case 0 then show ?case by simp
next
  case (Suc N)
  note [simp] = real_root_mult_exp real_root_mult [symmetric] setprod_Un_disjoint setprod_nonneg Suc  setsum_Un_disjoint field_simps
  have [simp]:
  "{Suc m..m + 2 * 2 ^ N} = union {Suc m..m + 2 ^ N} {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}"
    by auto
  have "GM a m (2 ^ Suc N) = root 2 (GM a m (2 ^ N) * GM a (m + 2 ^ N) (2 ^ N))"
    by auto
  also have "... <= (GM a m (2 ^ N) + GM a (m + 2 ^ N) (2 ^ N)) / 2"
    by (rule amgm2, auto)
  also have "... <= (AM a m (2 ^ N) + AM a (m + 2 ^ N) (2 ^ N)) / 2"
    by (smt Suc divide_right_mono)
  finally show ?case
    by simp
qed


lemma amgm_0_simps:
  fixes a :: "nat => real" and n
  assumes "0 < n"
  shows "ALL k. 0 <= a k ==> GM a 0 n <= AM a 0 n"
using exn2n assms
proof (induction n arbitrary: a rule: inc_induct)
  case base then show ?case
    using amgm_2 by metis
next
  case (step i a)
  let ?b = "%k. if k <= i then a k else GM a 0 i"
  note [simp] = step.prems setprod_nonneg field_simps real_of_nat_Suc
  have "ALL k. 0 <= ?b k" by simp
    from step.IH [of ?b, OF this]
  have "root (Suc i) (GM a 0 i ^ Suc i) <= (i * AM a 0 i + GM a 0 i) / Suc i" (is "?L <= _")
    by (subgoal_tac "{1..Suc i} = insert (Suc i) {1..i}", auto)
  also have "?L = GM a 0 i"
    by (rule real_root_power_cancel, auto)
  finally show ?case
    by simp
qed