204 hence "?UPROD = card \<dots>" by simp |
204 hence "?UPROD = card \<dots>" by simp |
205 also have "\<dots> = card (SIGMA x:{0..<?A}. {..x})" |
205 also have "\<dots> = card (SIGMA x:{0..<?A}. {..x})" |
206 apply(rule card_image) |
206 apply(rule card_image) |
207 using bij[THEN bij_betw_imp_inj_on] |
207 using bij[THEN bij_betw_imp_inj_on] |
208 by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans) |
208 by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans) |
209 also have "\<dots> = sum (\<lambda>n. n + 1) {0..<?A}" |
209 also have "\<dots> = sum Suc {0..<?A}" |
210 by(subst card_SigmaI) simp_all |
210 by (subst card_SigmaI) simp_all |
211 also have "\<dots> = 2 * sum of_nat {1..?A} div 2" |
211 also have "\<dots> = sum of_nat {Suc 0..?A}" |
212 using sum.reindex[where g="of_nat :: nat \<Rightarrow> nat" and h="\<lambda>x. x + 1" and A="{0..<?A}", symmetric] True |
212 using sum.atLeast_lessThan_reindex [symmetric, of Suc 0 ?A id] |
213 by(simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost) |
213 by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost) |
214 also have "\<dots> = ?A * (?A + 1) div 2" |
214 also have "\<dots> = ?A * (?A + 1) div 2" |
215 by(subst gauss_sum) simp |
215 using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp |
216 finally show ?thesis . |
216 finally show ?thesis . |
217 qed simp |
217 qed simp |
218 |
218 |
219 end |
219 end |