2013-05-14

Isabelle/Isar（その26)

　とはいえ，絶対を場合分けで処理するのはやはり面倒なので，２つ目のサブゴールの別の証明を考えましょう（ここは人間の仕事です）．

　．．．考えました．次の恒等式を用います．

lemma lem_max:
  "ALL (x::real) p q. abs (x - p) + abs (x - q)
 = max (abs(2 * x - (p + q))) (abs (p - q))" by auto

これなら?Qが直接導けます．この補題はグラフを考えれば判りますが，数学としては

lemma
  "ALL (p::real) q . abs p + abs q
 = max (abs (p + q)) (abs (p - q))" by auto

つまり，|p|+|q|=max{p+q,-(p+q),p-q,-(p-q)}=max{max{p+q,-(p+q)},max{p-q,-(p-q)}}ということです．

　ということで，後半は

  assume "?Q"
  hence "ALL x. max (abs(2 * x - (c + d))) (abs (c - d)) 
             <= max (abs(2 * x - (a + b))) (abs (a - b))"
    by auto
  thus "?P"
  using lem_max
    by simp

とすることもできます．

2013-05-14

Isabelle/Isar（その27)

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

　複数個の仮定をとる（ように見える）タイプ．まず，数列xを定義します．

fun x :: "nat => real" where
  "x 0 = 0" | "x (Suc 0) = 2" | "x (Suc (Suc 0)) = 6" |
  "x (Suc (Suc (Suc n))) = 3 * x (Suc (Suc n)) - 3 * x (Suc n) + x n"

あとは，これまでと同じくx.inductを参照させれば．．．

lemma
  fixes n :: "nat"
  shows "x n = n * (n + 1)"
  by (induction n rule: x.induct, simp_all)

Outputは

Failed to finish proof:
goal (1 subgoal):
x n = real (n * (n + (1∷nat)))
1. ⋀n∷nat.
x (Suc (Suc n)) =
real (Suc (Suc (Suc (Suc (Suc (Suc (n + (n + (n + (n + (n + n * n))))))))))) ⟹
x (Suc n) = real (Suc (Suc (n + (n + (n + n * n))))) ⟹
x n = real n + real n * real n ⟹
(3∷real) *
real (Suc (Suc (Suc (Suc (Suc (Suc (n + (n + (n + (n + (n + n * n))))))))))) -
(3∷real) * real (Suc (Suc (n + (n + (n + n * n))))) +
(real n + real n * real n) =
real (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (n + (n + (n + (n + (n + (n + (n + n * n)))))))))))))))))))
variables:
n :: nat

となります（笑）．これを見ると最後のreal (Suc ...の等式までは来ているので，HOL LightでのREAL，!n. &(SUC n) = &n + &1にあたる

thm real_of_nat_Suc

real (Suc (?n&#8759;nat)) = real ?n + (1&#8759;real)

を参照させれば

lemma x_n:
  fixes n :: "nat"
  shows "x n = n * (n + 1)"
  by (induction n rule: x.induct, simp_all add: real_of_nat_Suc)

print_statement x_n

Outputは

theorem x_n:
fixes n :: "nat"
shows "x (n∷nat) = real (n * (n + (1∷nat)))"

となります．

2013-05-14

Isabelle/Isar（その28)

　次は

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)
  case (1 n)
  moreover
  have "odd n ==> (n = 2 ^ 0 * n & odd n)" by auto
  moreover
  have "even n ==> n = 0 | (EX k. n = 2 * k & k < n)"
    by presburger
  ultimately show ?case
    by (metis mult_assoc power_Suc mult_0_right)
qed

　caseの名前が1であることは，イニシャルプルーフのあと

print_cases
cases:
1:
fix n_
let "?case∷bool" =
"(n_∷nat) = (0∷nat) ∨ (∃(d∷nat) m∷nat. n_ = (2∷nat) ^ d * m ∧ odd m)"
assume
1.IH: "∀m

のように確認できます．

　そして，presburgerはその名の通り自然数についてのプルーバー，また

thm mult_assoc power_Suc mult_0_right
(?a∷?'a) * (?b∷?'a) * (?c∷?'a) = ?a * (?b * ?c)
(?a∷?'a) ^ Suc (?n∷nat) = ?a * ?a ^ ?n
(?m∷nat) * (0∷nat) = (0∷nat)

は帰納法の下請けの結果を元に戻した際に必要な計算規則です．

　なお，odd n | even n が不要なのは odd が ~even の別名であること(Parity.thy)をシステムが知っているからです．

　さらに，odd n の場合の結論は

thm power_0 nat_mult_1
(?a∷?'a) ^ (0∷nat) = (1∷?'a)
(1∷nat) * (?n∷nat) = ?n

から構成できるので

proof (induction n rule: nat_less_induct)
  case (1 n)
  moreover
  have "even n ==> n = 0 | (EX k. n = 2 * k & k < n)"
    by presburger
  ultimately show ?case
    by (metis mult_assoc power_Suc mult_0_right power_0 nat_mult_1)
qed

のようにmetisに任せても構いません．

　参考までに．．．HOL Lightでは

# EVEN_ODD_DECOMPOSITION;;
val it : thm = |- !n. (?k m. ODD m /\ n = 2 EXP k * m) <=> ~(n = 0)

のように実装されています．