src/HOL/Library/Formal_Power_Series.thy
 changeset 62101 26c0a70f78a3 parent 61969 e01015e49041 child 62102 877463945ce9
1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 16:37:56 2016 +0100
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 17:40:59 2016 +0100
1.3 @@ -815,13 +815,14 @@
1.4  instantiation fps :: (comm_ring_1) metric_space
1.5  begin
1.7 -definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
1.8 -
1.9 +definition uniformity_fps_def [code del]:
1.10 +  "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
1.11 +
1.12 +definition open_fps_def' [code del]:
1.13 +  "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
1.15  instance
1.16  proof
1.17 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" for S :: "'a fps set"
1.18 -    by (auto simp add: open_fps_def ball_def subset_eq)
1.19    show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
1.20      by (simp add: dist_fps_def split: split_if_asm)
1.21    then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
1.22 @@ -853,10 +854,12 @@
1.23      qed
1.24      thus ?thesis by (auto simp add: not_le[symmetric])
1.25    qed
1.26 -qed
1.27 +qed (rule open_fps_def' uniformity_fps_def)+
1.29  end
1.31 +lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
1.32 +  unfolding open_dist ball_def subset_eq by simp
1.34  text \<open>The infinite sums and justification of the notation in textbooks.\<close>