相加平均と相乗平均
前回の和と積,更に割り算と累乗根を用いると
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の明示的な利用は廃止の傾向にあります.