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
```