src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 67155 9e5b05d54f9d
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Aug 18 20:47:47 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Dec 07 15:48:50 2017 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
     1.8 +  "dist x y = L2_set (\<lambda>i. dist (x$i) (y$i)) UNIV"
     1.9  
    1.10  instance ..
    1.11  end
    1.12 @@ -364,19 +364,19 @@
    1.13  begin
    1.14  
    1.15  lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
    1.16 -  unfolding dist_vec_def by (rule member_le_setL2) simp_all
    1.17 +  unfolding dist_vec_def by (rule member_le_L2_set) simp_all
    1.18  
    1.19  instance proof
    1.20    fix x y :: "'a ^ 'b"
    1.21    show "dist x y = 0 \<longleftrightarrow> x = y"
    1.22      unfolding dist_vec_def
    1.23 -    by (simp add: setL2_eq_0_iff vec_eq_iff)
    1.24 +    by (simp add: L2_set_eq_0_iff vec_eq_iff)
    1.25  next
    1.26    fix x y z :: "'a ^ 'b"
    1.27    show "dist x y \<le> dist x z + dist y z"
    1.28      unfolding dist_vec_def
    1.29 -    apply (rule order_trans [OF _ setL2_triangle_ineq])
    1.30 -    apply (simp add: setL2_mono dist_triangle2)
    1.31 +    apply (rule order_trans [OF _ L2_set_triangle_ineq])
    1.32 +    apply (simp add: L2_set_mono dist_triangle2)
    1.33      done
    1.34  next
    1.35    fix S :: "('a ^ 'b) set"
    1.36 @@ -407,13 +407,13 @@
    1.37        define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b
    1.38        from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i"
    1.39          unfolding r_def by simp_all
    1.40 -      from \<open>0 < e\<close> have e: "e = setL2 r UNIV"
    1.41 -        unfolding r_def by (simp add: setL2_constant)
    1.42 +      from \<open>0 < e\<close> have e: "e = L2_set r UNIV"
    1.43 +        unfolding r_def by (simp add: L2_set_constant)
    1.44        define A where "A i = {y. dist (x $ i) y < r i}" for i
    1.45        have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
    1.46          unfolding A_def by (simp add: open_ball r)
    1.47        moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
    1.48 -        by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute)
    1.49 +        by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute)
    1.50        ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
    1.51          (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
    1.52      qed
    1.53 @@ -447,10 +447,10 @@
    1.54    {
    1.55      fix m n :: nat
    1.56      assume "M \<le> m" "M \<le> n"
    1.57 -    have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
    1.58 +    have "dist (X m) (X n) = L2_set (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
    1.59        unfolding dist_vec_def ..
    1.60      also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
    1.61 -      by (rule setL2_le_sum [OF zero_le_dist])
    1.62 +      by (rule L2_set_le_sum [OF zero_le_dist])
    1.63      also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV"
    1.64        by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>)
    1.65      also have "\<dots> = r"
    1.66 @@ -480,7 +480,7 @@
    1.67  instantiation vec :: (real_normed_vector, finite) real_normed_vector
    1.68  begin
    1.69  
    1.70 -definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV"
    1.71 +definition "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"
    1.72  
    1.73  definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
    1.74  
    1.75 @@ -488,15 +488,15 @@
    1.76    fix a :: real and x y :: "'a ^ 'b"
    1.77    show "norm x = 0 \<longleftrightarrow> x = 0"
    1.78      unfolding norm_vec_def
    1.79 -    by (simp add: setL2_eq_0_iff vec_eq_iff)
    1.80 +    by (simp add: L2_set_eq_0_iff vec_eq_iff)
    1.81    show "norm (x + y) \<le> norm x + norm y"
    1.82      unfolding norm_vec_def
    1.83 -    apply (rule order_trans [OF _ setL2_triangle_ineq])
    1.84 -    apply (simp add: setL2_mono norm_triangle_ineq)
    1.85 +    apply (rule order_trans [OF _ L2_set_triangle_ineq])
    1.86 +    apply (simp add: L2_set_mono norm_triangle_ineq)
    1.87      done
    1.88    show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
    1.89      unfolding norm_vec_def
    1.90 -    by (simp add: setL2_right_distrib)
    1.91 +    by (simp add: L2_set_right_distrib)
    1.92    show "sgn x = scaleR (inverse (norm x)) x"
    1.93      by (rule sgn_vec_def)
    1.94    show "dist x y = norm (x - y)"
    1.95 @@ -508,7 +508,7 @@
    1.96  
    1.97  lemma norm_nth_le: "norm (x $ i) \<le> norm x"
    1.98  unfolding norm_vec_def
    1.99 -by (rule member_le_setL2) simp_all
   1.100 +by (rule member_le_L2_set) simp_all
   1.101  
   1.102  lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
   1.103  apply standard
   1.104 @@ -545,7 +545,7 @@
   1.105      unfolding inner_vec_def
   1.106      by (simp add: vec_eq_iff sum_nonneg_eq_0_iff)
   1.107    show "norm x = sqrt (inner x x)"
   1.108 -    unfolding inner_vec_def norm_vec_def setL2_def
   1.109 +    unfolding inner_vec_def norm_vec_def L2_set_def
   1.110      by (simp add: power2_norm_eq_inner)
   1.111  qed
   1.112