次は thm nat_less_induct(⋀n∷nat. ∀m を用いる例．任意の自然数は0か，2の自然数冪と奇数との積かの何れかであるという性質です． lemma fixes n :: "nat" shows "n = 0 | (EX d m. n = 2 ^ d * m & odd m)" proof (induction n rule: nat_less_induct) cas…

Isabelleのマニュアルを斜め読みしていると，帰納法の例として，リストの形によるものが丁寧に書かれていますが，普通の数学の例は数列の和，しかもnat上での甘いものくらいなので，少し補います（リストも項数が有限の列と見ればよいのでしょうが）． 複数…

とはいえ，絶対を場合分けで処理するのはやはり面倒なので，２つ目のサブゴールの別の証明を考えましょう（ここは人間の仕事です）． ．．．考えました．次の恒等式を用います． lemma lem_max: "ALL (x::real) p q. abs (x - p) + abs (x - q) = max (abs(2…