数列の和と積
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 を対応させるものです.書式は上記の通り
です.
このように定義すると,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の明示的な利用は廃止の傾向にあります.