数列の和と積

 Isarにおいて,数列の有限項の和,積を得るには,setsum,setprod を用います.引数として,数列と定義域を与えると,その値域の要素の和,積になります.例えば

lemma "setsum (a::nat=>real) {0,2,3,100} = a 0 + a 2 + a 3 + a 100"
  by simp
lemma "setprod (a::nat=>real) {7,0} = a 0 * a 7"
  by simp

といった具合です.定義域が自然数区間の場合は

lemma "{(1::nat)..4} = {1,2,3,4}" by auto

のように両端の値で指定することも出来ますが,一般に「簡単→複雑」の書き換えは自動的には行われない(無限ループになる可能性が大きい)ので,例えば

lemma "setprod (a::nat=>real) {1..4} = a 1 * a 2 * a 3 * a 4"
  by (subgoal_tac "{(1::nat)..4} = {1,2,3,4}") auto

あるいは

lemma "setprod (a::nat=>real) {1..4} = a 1 * a 2 * a 3 * a 4"
proof -
  have "{(1::nat)..4} = {1,2,3,4}" by auto
  then show ?thesis by simp
qed

のように書き換えを新たなゴールに設定し,まとめて証明することになります.

相加平均と相乗平均

 前回の和と積,更に割り算と累乗根を用いると

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})" 

のように a_{m+1},...,a_{m+n} の相加平均と相乗平均を与える関数が定義できます.定義域を{1..n}としていなのは,項数についての帰納法を用いる為です.

 funはいわゆるカリー化による写像汎関数)を定義するコマンドであり,例えば,AMはnatからrealへの関数(つまり数列)であるaに対して,natタイプ(つまり自然数)であるmに対して定まるnatからrealへの関数 AM a m : n |→ setsum a {Suc m..m + n} / n を対応させる,汎関数 AM a を対応させるものです.書式は上記の通り

 fun 写像の名前 :: "写像のタイプ" where "像の定義"

です.

 このように定義すると,Isarは

searched for:
name: "amgm"

found 4 theorem(s):

amgm.AM.cases: (⋀a m n. ?x = (a, m, n) ⟹ ?P) ⟹ ?P
amgm.AM.induct: (⋀a m n. ?P a m n) ⟹ ?P ?a0.0 ?a1.0 ?a2.0
amgm.AM.simps: AM ?a ?m ?n = setsum ?a {Suc ?m..?m + ?n} / real ?n
amgm.GM.simps: GM ?a ?m ?n = root ?n (setprod ?a {Suc ?m..?m + ?n})

という定理を生成し,AM.simps,GM.simpsにはsimp属性が付くので,simpやautoが自動的に参照します.従って,例えば

lemma "AM a 0 3 = (a 1 + a 2 + a 3) / 3"

にまず

  apply simp

のようにsimpを適用すると,Outputは

proof (prove): step 1

goal (1 subgoal):
1. setsum a {Suc 0..3} = a (Suc 0) + a 2 + a 3

となるので,前回に習って

  by (subgoal_tac "{Suc 0..3} = {Suc 0,2,3}") auto

あるいは

lemma "GM a 0 3 = root 3 (a 1 * a 2 * a 3)"
proof simp
  show "setprod a {Suc 0..3} = a (Suc 0) * a 2 * a 3"
  proof -
    have "{Suc 0..3} = {Suc 0,2,3}" by auto
    then show ?thesis by simp
  qed
qed

と出来ます.なお,Isarではtacticの明示的な利用は廃止の傾向にあります.