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