計算機を用いた定理証明における楽しみの１つは（参照先が見え難くなりますが）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 …

以下は正数である分母 Suc i を払う，両辺から同じものを減ずる，そして，両辺を正数 i で割るといった代数計算です．この種の処理で参照すべき定理は，多くの場合，nat上の性質のreal上への書き換えであり，ここでも thm real_of_nat_Sucreal (Suc ?n) = re…

次は，step ケースです． next case (step i a) 先述の通り，帰納法の変数はi，目標の数列はaとします．証明の流れは，letを用いて，項数がi+1である数列?bを ?b k = a k (k=1,...,i)，GM a 0 i (k=i+1)のように設定，帰納法の仮定 step.IH を適用して，以下…

後半です．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での成立を導くというもので，前半は数列を固定し，…

それでは，次に，後ろ向きの帰納法を find_theorems name: induct "?P (Suc ?n) ==> ?P ?n" のように探してみると searched for: name: "induct" "?P (Suc ?n) ⟹ ?P ?n"found 4 theorem(s):Nat.inc_induct: ?i ≤ ?j ⟹ ?P ?j ⟹ (⋀i. i Nat.strict_inc_induct:…

ということで，次は have "... ですが，今回はsimpを試すまでももなく Suc.hyps: ∀k. 0 ≤ a k ⟹ GM a ?m (2 ^ N) ≤ AM a ?m (2 ^ N) Suc.prems: ∀k. 0 ≤ a k を用いる訳で，そのためにthoremレベルのinst属性であるOF，および，termレベルのinst属性であるof…

ということでamgm2は準備出来たのですが，今度はGMがその仮定を満たすこと，つまり lemma GMge0: "ALL k. 0 0 0 GM a m n" が入用になります．例によって proof simp と試すと goal (1 subgoal): 1. ∀k. 0 ≤ a k ⟹ 0 までは出来ているので find_theorems "0 …

この結果の右辺は引き続き用いるので also とすれば calculation: GM a m (2 ^ Suc N) = root 2 (GM a m (2 ^ N) * GM a (m + 2 ^ N) (2 ^ N)) のように記憶され，右辺が...で参照できます． 従って，次は have "... GM a m (2 ^ N) + GM a (m + 2 ^ N) (2 ^…

よって今度は find_theorems "setprod ?f ?A * setprod ?f ?B" とすれば使えそうな定理 Big_Operators.setprod_Un_disjoint: finite ?A ⟹ finite ?B ⟹ ?A ∩ ?B = {} ⟹ setprod ?g (?A ∪ ?B) = setprod ?g ?A * setprod ?g ?B が見付かりますので，これを用い…

それでは２のべき乗の場合を証明していきます．lemmaの名前とstatementは lemma amgm_2: fixes a m n shows "ALL k. 0 <= a k ==> GM a m (2 ^ n) <= AM a m (2 ^ n)" 証明は項数についての帰納法ですが，数列はaとして固定し，その隣接する任意の2^N項につ…

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

前回の和と積，更に割り算と累乗根を用いると fun AM :: "(nat => real) => nat => nat => real" where "AM a m n = setsum a {Suc m..m + n} / n" fun GM :: "(nat => real) => nat => nat => real" where "GM a m n = root n (setprod a {Suc m..m + n})" …

Isarにおいて，数列の有限項の和，積を得るには，setsum，setprod を用います．引数として，数列と定義域を与えると，その値域の要素の和，積になります．例えば lemma "setsum (a::nat=>real) {0,2,3,100} = a 0 + a 2 + a 3 + a 100" by simp lemma "setpr…

定理証明システムは巷で言われるようなプログラムや約款？の検証ツールではなく，あくまで計算機上に数学の理論を公理論的に構成する為のものです． しかしながら，数学の人間はこうしたソフトをあまり（というか全く）利用していないのが現状であり，その理…

Isarの証明は対話的，つまりシステムが生成するサブゴールを次の目標とするのが基本ですが，過信は禁物です．例えば lemma fixes a b :: "real" assumes "a + b = 0" shows "a < 0 | b <= 0" proof に対するOutputは proof (state): step 1goal (1 subgoal):…

次は 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…

次は逆です． next とすれば proof (state): step 26goal (1 subgoal): 1. a + b = c + d ∧ ¦c - d¦ ≤ ¦a - b¦ ⟹ ∀x∷real. ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦ variables: a, b, c, d :: real なので assume 0: "?Q" とします．nextによりproofのブロッ…

この?Q1を今から導く?Q2と併せて?Qとするので moreover により calculation: (a∷real) + (b∷real) = (c∷real) + (d∷real) のように蓄積し，また，thisとして0と併せて直ちに利用します． with 0 have "?L ((c + d) / 2) <= ?R ((a + b) / 2)" by metis このw…

まず (is "?P <-> ?Q" is "(ALL x. ?LR x) <-> ?Q" is "(ALL x. ?L x <= ?R x) <-> ?Q1 & ?Q2") によりマッチングを設定し，入力の反復を避けています（可読性は落ちます）．今回は，isを並べて３通り設定しました． 次のproofコマンドにより，イニシャルプ…

では，次の例として lemma fixes a b c d :: "real" shows "(ALL x. abs (x - c) + abs (x - d) <= abs (x - a) + abs(x - b)) <-> (a + b = c + d & abs (c - d) <= abs (a - b))" を取り上げます． 普通の証明は，２つの含意に分けて，xとしてmax{a,b,c,d}…

0とは限らない自然数からの帰納法は，Nat.thyのdec_inductという定理となっています． print_statement dec_inducttheorem dec_induct: fixes i :: "nat" and j :: "nat" and P :: "nat ⇒ bool" assumes "i ≤ j" and "P i" and "⋀n. i ≤ n ⟹ P n ⟹ P (Suc n)…

さて，これまでは数列を定理の中で，言わば局所的に定義しましたが，セッション全体を通して大域的に定義すると，システムが証明に便利な定理を自動的に用意してくれます． まず，数列Xを次のように定義します． fun X :: "nat => real" where "X 0 = 0" | "…

次に帰納法の２つ目のサブゴールに移ります． next case (Suc m) と入力すると，Outputは proof (state): step 7this: 1 ≤ m ⟹ a m = 2 ^ m - 1 1 ≤ Suc mgoal (1 subgoal): 1. ⋀n. (1 ≤ n ⟹ a n = 2 ^ n - 1) ⟹ 1 ≤ Suc n ⟹ a (Suc n) = 2 ^ Suc n - 1 さら…

premsを参照する例として lemma fixes "a" :: "nat => real" and "n" :: "nat" assumes "a 1 = 1" and "!!n. 1 <= n ==> a (Suc n) = 2 * a n + 1" shows "1 <= n ==> a n = 2 ^ n - 1" の証明を考えます．これは自然数の成り立ちからすれば途中から始まる帰…

更に２つ目のサブゴールは，帰納法の変数nが1以上，つまり，Suc n_の形の場合なので，場合を設定するコマンドcase Suc を用いて簡素化出来ます．それは lemma fixes "a" :: "nat => real" and "n" :: "nat" assumes "a 0 = 0" and "ALL n. a (Suc n) = 2 * a…

Isarに負けないよう，くどく続けます． 仮に以上の計算過程を省略するなら，これまでの話から，次のように書けることが判るでしょう． lemma fixes "a" :: "nat => real" and "n" :: "nat" assumes "a 0 = 0" and "ALL n. a (Suc n) = 2 * a n + 1" shows "a…

では帰納法の２つ目のサブゴールの証明部分を解説しましょう． まず，１つ目の証明から２つ目に移ることをシステムに告げているのが next です．するとIsarは proof (state): step 14goal (1 subgoal): 1. ⋀nat. a nat = 2 ^ nat - 1 ⟹ a (Suc nat) = 2 ^ Su…

さらに１つ目のサブゴールの証明は from 1 have "a 0 = 0" by simp also have "... = 1 - 1" by simp also have "... = 2 ^ 0 - 1" by simp finally show "a 0 = 2 ^ 0 - 1" by this のように，calculationを生成するコマンドalsoと，その結果をthisとして参…