数列の和と積

　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

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