src/HOL/Analysis/Brouwer_Fixpoint.thy
 changeset 64267 b9a1486e79be parent 64122 74fde524799e child 64394 141e1ed8d5a0
```     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Oct 16 22:43:51 2016 +0200
1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Oct 17 11:46:22 2016 +0200
1.3 @@ -52,13 +52,13 @@
1.4  lemmas Zero_notin_Suc = zero_notin_Suc_image
1.5  lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
1.6
1.7 -lemma setsum_union_disjoint':
1.8 +lemma sum_union_disjoint':
1.9    assumes "finite A"
1.10      and "finite B"
1.11      and "A \<inter> B = {}"
1.12      and "A \<union> B = C"
1.13 -  shows "setsum g C = setsum g A + setsum g B"
1.14 -  using setsum.union_disjoint[OF assms(1-3)] and assms(4) by auto
1.15 +  shows "sum g C = sum g A + sum g B"
1.16 +  using sum.union_disjoint[OF assms(1-3)] and assms(4) by auto
1.17
1.18  lemma pointwise_minimal_pointwise_maximal:
1.19    fixes s :: "(nat \<Rightarrow> nat) set"
1.20 @@ -139,19 +139,19 @@
1.21    shows "odd (card {s\<in>S. compo s})"
1.22  proof -
1.23    have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + (\<Sum>s | s \<in> S \<and> compo s. nF s) = (\<Sum>s\<in>S. nF s)"
1.24 -    by (subst setsum.union_disjoint[symmetric]) (auto intro!: setsum.cong)
1.25 +    by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
1.26    also have "\<dots> = (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> bnd f}. face f s}) +
1.27                    (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> \<not> bnd f}. face f s})"
1.28 -    unfolding setsum.distrib[symmetric]
1.29 +    unfolding sum.distrib[symmetric]
1.30      by (subst card_Un_disjoint[symmetric])
1.31 -       (auto simp: nF_def intro!: setsum.cong arg_cong[where f=card])
1.32 +       (auto simp: nF_def intro!: sum.cong arg_cong[where f=card])
1.33    also have "\<dots> = 1 * card {f\<in>F. compo' f \<and> bnd f} + 2 * card {f\<in>F. compo' f \<and> \<not> bnd f}"
1.34 -    using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] setsum_multicount)
1.35 +    using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] sum_multicount)
1.36    finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
1.37      using assms(6,8) by simp
1.38    moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
1.39      (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 0. nF s) + (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 2. nF s)"
1.40 -    using assms(7) by (subst setsum.union_disjoint[symmetric]) (fastforce intro!: setsum.cong)+
1.41 +    using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+
1.42    ultimately show ?thesis
1.43      by auto
1.44  qed
1.45 @@ -1417,9 +1417,9 @@
1.46    fix y :: 'a assume y: "y \<in> unit_cube"
1.47    have "dist 0 y = norm y" by (rule dist_0_norm)
1.48    also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
1.49 -  also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_setsum)
1.50 +  also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_sum)
1.51    also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
1.52 -    by (rule setsum_mono, simp add: y [unfolded mem_unit_cube])
1.53 +    by (rule sum_mono, simp add: y [unfolded mem_unit_cube])
1.54    finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
1.55  qed
1.56
1.57 @@ -1679,7 +1679,7 @@
1.58        unfolding inner_diff_left[symmetric]
1.59        by (rule norm_le_l1)
1.60      also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
1.61 -      apply (rule setsum_strict_mono)
1.62 +      apply (rule sum_strict_mono)
1.63        using as
1.64        apply auto
1.65        done
1.66 @@ -1731,7 +1731,7 @@
1.67      by auto
1.68    {
1.69      have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
1.70 -      apply (rule setsum_mono)
1.71 +      apply (rule sum_mono)
1.72        using rs(1)[OF b'_im]
1.73        apply (auto simp add:* field_simps simp del: of_nat_Suc)
1.74        done
1.75 @@ -1743,7 +1743,7 @@
1.76    moreover
1.77    {
1.78      have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
1.79 -      apply (rule setsum_mono)
1.80 +      apply (rule sum_mono)
1.81        using rs(2)[OF b'_im]
1.82        apply (auto simp add:* field_simps simp del: of_nat_Suc)
1.83        done
1.84 @@ -1757,7 +1757,7 @@
1.85      unfolding r'_def s'_def z_def
1.86      using \<open>p > 0\<close>
1.87      apply (rule_tac[!] le_less_trans[OF norm_le_l1])
1.88 -    apply (auto simp add: field_simps setsum_divide_distrib[symmetric] inner_diff_left)
1.89 +    apply (auto simp add: field_simps sum_divide_distrib[symmetric] inner_diff_left)
1.90      done
1.91    then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
1.92      using rs(3) i
```