115 |
115 |
116 subsection {* Rings and the summation operator *} |
116 subsection {* Rings and the summation operator *} |
117 |
117 |
118 (* Basic facts --- move to HOL!!! *) |
118 (* Basic facts --- move to HOL!!! *) |
119 |
119 |
120 lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)" |
120 lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)" |
121 by simp |
121 by simp |
122 |
122 |
123 lemma natsum_Suc [simp]: |
123 lemma natsum_Suc [simp]: |
124 "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)" |
124 "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)" |
125 by (simp add: atMost_Suc) |
125 by (simp add: atMost_Suc) |
126 |
126 |
127 lemma natsum_Suc2: |
127 lemma natsum_Suc2: |
128 "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)" |
128 "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::comm_monoid_add)" |
129 proof (induct n) |
129 proof (induct n) |
130 case 0 show ?case by simp |
130 case 0 show ?case by simp |
131 next |
131 next |
132 case Suc thus ?case by (simp add: plus_ac0.assoc) |
132 case Suc thus ?case by (simp add: semigroup_add.add_assoc) |
133 qed |
133 qed |
134 |
134 |
135 lemma natsum_cong [cong]: |
135 lemma natsum_cong [cong]: |
136 "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==> |
136 "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> |
137 setsum f {..j} = setsum g {..k}" |
137 setsum f {..j} = setsum g {..k}" |
138 by (induct j) auto |
138 by (induct j) auto |
139 |
139 |
140 lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)" |
140 lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)" |
141 by (induct n) simp_all |
141 by (induct n) simp_all |
142 |
142 |
143 lemma natsum_add [simp]: |
143 lemma natsum_add [simp]: |
144 "!!f::nat=>'a::plus_ac0. |
144 "!!f::nat=>'a::comm_monoid_add. |
145 setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" |
145 setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" |
146 by (induct n) (simp_all add: plus_ac0) |
146 by (induct n) (simp_all add: add_ac) |
147 |
147 |
148 (* Facts specific to rings *) |
148 (* Facts specific to rings *) |
149 |
149 |
150 instance ring < plus_ac0 |
150 instance ring < comm_monoid_add |
151 proof |
151 proof |
152 fix x y z |
152 fix x y z |
153 show "(x::'a::ring) + y = y + x" by (rule a_comm) |
153 show "(x::'a::ring) + y = y + x" by (rule a_comm) |
154 show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc) |
154 show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc) |
155 show "0 + (x::'a::ring) = x" by (rule l_zero) |
155 show "0 + (x::'a::ring) = x" by (rule l_zero) |