metis からの挑戦

　定理自体はともかく，an_am_coprime の "0" の証明に even_zero_int 等を持ち出さないあたり，さすが metis といったところでしょう．

theory prob01 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin

fun a :: "nat => int" where
  "a 0 = 3" | "a (Suc n) = a n * a n - 2"

lemma an_odd: "odd (a n)" by (induct n, auto)

lemma an_am_gcd [rule_format]:
  "∀m. m < n --> (∃d. a n = d * a m - 2 ∨ a n = d * a m + 2)"
proof (induct n)
  case 0 thus ?case by auto
next
  case (Suc n)
 {fix m assume 0: "m < Suc n"
  have "∃d. a (Suc n) = d * a m - 2 ∨ a (Suc n) = d * a m + 2"
  proof (cases "m = n")
    case True thus "?thesis" by auto
  next
    case False hence "m < n" using 0 by auto
    with Suc.hyps obtain "d" where "a n = d * a m - 2 ∨ a n = d * a m + 2" by auto
    moreover have "a (Suc n) = (a n + 2) * (a n - 2) + 2" by simp algebra
    ultimately show "?thesis" by auto
  qed}
  thus ?case by auto
qed

theorem an_am_coprime:
  assumes "m < n" shows "coprime (a m) (a n)"
proof -
  let ?g = "gcd (a m) (a n)"
  have 0: "odd (?g)"
    using an_odd even_product gcd_coprime_exists_int gcd_zero_int
    by metis
  obtain "d" where "a n = d * a m - 2 ∨ a n = d * a m + 2"
    using assms an_am_gcd
    by auto
  moreover obtain "p" "q" where "a m = p * ?g ∧ a n = q * ?g"
    using 0 even_zero_int gcd_coprime_exists_int
    by metis
  ultimately have "(d * p - q) * ?g = 2 ∨ (q - d * p) * ?g = 2"
    by algebra
  thus "?g = 1"
    using two_is_prime_int prime_int_altdef 0 dvd_triv_right even_numeral_int gcd_ge_0_int
    by metis
qed

end