Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs

--- a/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -666,8 +666,7 @@
           have "finite {i \<in> I. Abs_poly_mapping (?f i) \<noteq> 0}"
             by (rule finite_subset [OF _ fin]) (use \<open>i \<in> I\<close> J_def eq in \<open>auto simp: in_keys_iff\<close>)
           with \<open>i \<in> I\<close> have "?h (\<lambda>j\<in>I. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})"
-            apply (simp add: sum_diff1')
-            sorry
+            by (simp add: sum_diff1')
           then show ?thesis
             by (simp add: 1 2 Poly_Mapping.lookup_add)
         next

--- a/src/HOL/Analysis/Abstract_Limits.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -53,11 +53,11 @@
 lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
   by (simp add: limitin_def)
 
-lemma limitin_const: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
+lemma limitin_const_iff [simp]: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
   by (simp add: limitin_def)
 
-lemma limitin_real_const: "limitin euclideanreal (\<lambda>a. l) l F"
-  by (simp add: limitin_def)
+lemma limitin_const: "limitin euclidean (\<lambda>a. l) l F"
+  by simp
 
 lemma limitin_eventually:
    "\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limitin X f l F"
@@ -91,6 +91,11 @@
 qed (auto simp: limitin_def topspace_subtopology)
 
 
+lemma limitin_canonical_iff_gen [simp]:
+  assumes "open S"
+  shows "limitin (top_of_set S) f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F \<and> l \<in> S"
+  using assms by (auto simp: limitin_subtopology tendsto_def)
+
 lemma limitin_sequentially:
    "limitin X S l sequentially \<longleftrightarrow>
      l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> (\<exists>N. \<forall>n. N \<le> n \<longrightarrow> S n \<in> U))"

--- a/src/HOL/Analysis/Abstract_Topology.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -1694,7 +1694,7 @@
   "continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
   by (auto simp: continuous_map_def)
 
-lemma continuous_map_iff_continuous [simp]: "continuous_map (subtopology euclidean S) euclidean g = continuous_on S g"
+lemma continuous_map_iff_continuous [simp]: "continuous_map (top_of_set S) euclidean g = continuous_on S g"
   by (fastforce simp add: continuous_map openin_subtopology continuous_on_open_invariant)
 
 lemma continuous_map_iff_continuous2 [simp]: "continuous_map euclidean euclidean g = continuous_on UNIV g"
@@ -3782,12 +3782,17 @@
   using assms continuous_on_closed by blast
 
 lemma continuous_map_subtopology_eu [simp]:
-  "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+  "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
   apply safe
   apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
   apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
   by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
 
+lemma continuous_map_euclidean_top_of_set:
+  assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f"
+  shows "continuous_map euclidean (top_of_set S) f"
+  by (simp add: cont continuous_map_into_subtopology eq image_subset_iff_subset_vimage)
+
 subsection%unimportant \<open>Half-global and completely global cases\<close>
 
 lemma continuous_openin_preimage_gen:

--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -800,10 +800,11 @@
     unfolding comp_def by auto
 next
   assume *: "\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
-  have "continuous_map T euclidean (blinfun_apply o f)"
-    unfolding euclidean_product_topology
-    apply (rule continuous_map_coordinatewise_then_product, auto)
+  have "\<And>i. continuous_map T euclidean (\<lambda>x. blinfun_apply (f x) i)"
     using * unfolding comp_def by auto
+  then have "continuous_map T euclidean (blinfun_apply o f)"
+    unfolding o_def
+    by (metis (no_types) continuous_map_componentwise_UNIV euclidean_product_topology)
   show "continuous_map T strong_operator_topology f"
     unfolding strong_operator_topology_def
     apply (rule continuous_map_pullback')
@@ -815,6 +816,4 @@
   by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
     auto simp add: linear_continuous_on)
 
-
-
 end

--- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -3101,7 +3101,7 @@
       define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
       have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
-        apply (subst netlimit_within)
+        apply (subst Lim_ident_at)
         using \<open>n>m\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)  
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)
@@ -3130,7 +3130,7 @@
       define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
       have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
-        apply (subst netlimit_within)
+        apply (subst Lim_ident_at)
         using \<open>m>n\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)

--- a/src/HOL/Analysis/Derivative.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -2015,7 +2015,7 @@
   using *
   apply (cases "at x within S \<noteq> bot")
   apply (intro refl conj_cong filterlim_cong)
-  apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono)
+  apply (auto simp: Lim_ident_at eventually_at_filter elim: eventually_mono)
   done
 
 lemma islimpt_closure_open:

--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -620,7 +620,7 @@
     apply (simp add: norm_sgn sgn_zero_iff x)
     done
   then show ?thesis
-    by (rule netlimit_within [of a UNIV])
+    by (rule Lim_ident_at [of a UNIV])
 qed simp
 
 subsection \<open>Boundedness\<close>

--- a/src/HOL/Analysis/Elementary_Topology.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -1472,13 +1472,10 @@
 abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a"
   where "netlimit F \<equiv> Lim F (\<lambda>x. x)"
 
-lemma netlimit_within: "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
-  by (rule tendsto_Lim) (auto intro: tendsto_intros)
-
 lemma netlimit_at [simp]:
   fixes a :: "'a::{perfect_space,t2_space}"
   shows "netlimit (at a) = a"
-  using netlimit_within [of a UNIV] by simp
+  using Lim_ident_at [of a UNIV] by simp
 
 lemma lim_within_interior:
   "x \<in> interior S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at x)"
@@ -2750,5 +2747,4 @@
   finally show ?thesis .
 qed
 
-
 end
\ No newline at end of file

--- a/src/HOL/Analysis/Function_Topology.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -565,8 +565,14 @@
 
 end
 
+lemma open_PiE [intro?]:
+  fixes X::"'i \<Rightarrow> ('b::topological_space) set"
+  assumes "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+  shows "open (Pi\<^sub>E UNIV X)"
+    by (simp add: assms open_fun_def product_topology_basis)
+
 lemma euclidean_product_topology:
-  "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
+  "product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV = euclidean"
 by (metis open_openin topology_eq open_fun_def)
 
 proposition product_topology_basis':
@@ -582,8 +588,7 @@
   have **: "finite {i. X i \<noteq> UNIV}"
     unfolding X_def V_def J_def using assms(1) by auto
   have "open (Pi\<^sub>E UNIV X)"
-    unfolding open_fun_def
-    by (simp_all add: * ** product_topology_basis)
+    by (simp add: "*" "**" open_PiE)
   moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
     apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
     proof (auto)
@@ -618,8 +623,8 @@
 lemma continuous_on_product_then_coordinatewise_UNIV:
   assumes "continuous_on UNIV f"
   shows "continuous_on UNIV (\<lambda>x. f x i)"
-  using assms unfolding continuous_map_iff_continuous2 [symmetric] euclidean_product_topology
-  by fastforce
+  unfolding continuous_map_iff_continuous2 [symmetric]
+  by (rule continuous_map_product_then_coordinatewise [where I=UNIV]) (use assms in \<open>auto simp: euclidean_product_topology\<close>)
 
 lemma continuous_on_product_then_coordinatewise:
   assumes "continuous_on S f"
@@ -724,7 +729,8 @@
   text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
   define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
   have "countable (B i)" for i unfolding B_def by auto
-
+  have open_B: "\<And>X i. X \<in> B i \<Longrightarrow> open X"
+    by (auto simp: B_def A)
   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
   have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
     unfolding K_def B_def by auto
@@ -737,10 +743,7 @@
   have "x \<in> k" if "k \<in> K" for k
     using that unfolding K_def B_def apply auto using A(1) by auto
   have "open k" if "k \<in> K" for k
-    using that unfolding open_fun_def K_def B_def apply (auto)
-    apply (rule product_topology_basis)
-    unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
-
+    using that unfolding K_def  by (blast intro: open_B open_PiE elim: )
   have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
   proof -
     have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
@@ -854,9 +857,7 @@
   next
     fix U assume "U \<in> K"
     show "open U"
-      using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
-      apply (rule product_topology_basis)
-      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV by auto
+      using \<open>U \<in> K\<close> unfolding open_fun_def K_def  by clarify (metis \<open>U \<in> K\<close> i open_PiE open_fun_def)
   qed
 
   show ?thesis using i ii iii by auto

--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -32,6 +32,74 @@
     by (auto intro!: real_le_rsqrt)
 qed
 
+subsection \<open>Continuity of the representation WRT an orthogonal basis\<close>
+
+lemma representation_bound:
+  fixes B :: "'N::real_inner set"
+  assumes "finite B" "independent B" "b \<in> B" and orth: "pairwise orthogonal B"
+  obtains m where "m > 0" "\<And>x. x \<in> span B \<Longrightarrow> \<bar>representation B x b\<bar> \<le> m * norm x"
+proof 
+  fix x
+  assume x: "x \<in> span B"
+  have "b \<noteq> 0"
+    using \<open>independent B\<close> \<open>b \<in> B\<close> dependent_zero by blast
+  have [simp]: "b \<bullet> b' = (if b' = b then (norm b)\<^sup>2 else 0)"
+    if "b \<in> B" "b' \<in> B" for b b'
+    using orth by (simp add: orthogonal_def pairwise_def norm_eq_sqrt_inner that)
+  have "norm x = norm (\<Sum>b\<in>B. representation B x b *\<^sub>R b)"
+    using real_vector.sum_representation_eq [OF \<open>independent B\<close> x \<open>finite B\<close> order_refl]
+    by simp
+  also have "\<dots> = sqrt ((\<Sum>b\<in>B. representation B x b *\<^sub>R b) \<bullet> (\<Sum>b\<in>B. representation B x b *\<^sub>R b))"
+    by (simp add: norm_eq_sqrt_inner)
+  also have "\<dots> = sqrt (\<Sum>b\<in>B. (representation B x b *\<^sub>R b) \<bullet> (representation B x b *\<^sub>R b))"
+    using \<open>finite B\<close>
+    by (simp add: inner_sum_left inner_sum_right if_distrib [of "\<lambda>x. _ * x"] cong: if_cong sum.cong_simp)
+  also have "\<dots> = sqrt (\<Sum>b\<in>B. (norm (representation B x b *\<^sub>R b))\<^sup>2)"
+    by (simp add: mult.commute mult.left_commute power2_eq_square)
+  also have "\<dots> = sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
+    by (simp add: norm_mult power_mult_distrib)
+  finally have "norm x = sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)" .
+  moreover
+  have "sqrt ((representation B x b)\<^sup>2 * (norm b)\<^sup>2) \<le> sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
+    using \<open>b \<in> B\<close> \<open>finite B\<close> by (auto intro: member_le_sum)
+  then have "\<bar>representation B x b\<bar> \<le> (1 / norm b) * sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
+    using \<open>b \<noteq> 0\<close> by (simp add: divide_simps real_sqrt_mult del: real_sqrt_le_iff)
+  ultimately show "\<bar>representation B x b\<bar> \<le> (1 / norm b) * norm x"
+    by simp
+next
+  show "0 < 1 / norm b"
+    using \<open>independent B\<close> \<open>b \<in> B\<close> dependent_zero by auto
+qed 
+
+lemma continuous_on_representation:
+  fixes B :: "'N::euclidean_space set"
+  assumes "finite B" "independent B" "b \<in> B" "pairwise orthogonal B" 
+  shows "continuous_on (span B) (\<lambda>x. representation B x b)"
+proof
+  show "\<exists>d>0. \<forall>x'\<in>span B. dist x' x < d \<longrightarrow> dist (representation B x' b) (representation B x b) \<le> e"
+    if "e > 0" "x \<in> span B" for x e
+  proof -
+    obtain m where "m > 0" and m: "\<And>x. x \<in> span B \<Longrightarrow> \<bar>representation B x b\<bar> \<le> m * norm x"
+      using assms representation_bound by blast
+    show ?thesis
+      unfolding dist_norm
+    proof (intro exI conjI ballI impI)
+      show "e/m > 0"
+        by (simp add: \<open>e > 0\<close> \<open>m > 0\<close>)
+      show "norm (representation B x' b - representation B x b) \<le> e"
+        if x': "x' \<in> span B" and less: "norm (x'-x) < e/m" for x' 
+      proof -
+        have "\<bar>representation B (x'-x) b\<bar> \<le> m * norm (x'-x)"
+          using m [of "x'-x"] \<open>x \<in> span B\<close> span_diff x' by blast
+        also have "\<dots> < e"
+          by (metis \<open>m > 0\<close> less mult.commute pos_less_divide_eq)
+        finally have "\<bar>representation B (x'-x) b\<bar> \<le> e" by simp
+        then show ?thesis
+          by (simp add: \<open>x \<in> span B\<close> \<open>independent B\<close> representation_diff x')
+      qed
+    qed
+  qed
+qed
 
 subsection%unimportant\<open>Balls in Euclidean Space\<close>