# HG changeset patch
# User immler
# Date 1489524162 -3600
# Node ID f435640193b65f419f2c6ca3162c140eac10bbd3
# Parent  d23eded35a3325cac5b08f0968e4bd9d44ca3b82
recovered typedef with set bcontfun (amending d23eded35a33)

diff -r d23eded35a33 -r f435640193b6 src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Mar 10 23:16:40 2017 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Tue Mar 14 21:42:42 2017 +0100
@@ -7,13 +7,12 @@
 
 subsection \<open>Definition\<close>
 
-definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
-  where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
+definition "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
 
 typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
-    "{f::'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}"
+  "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
   morphisms apply_bcontfun Bcontfun
-  by (auto intro: continuous_intros simp: bounded_def)
+  by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
 
 declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
 
@@ -22,18 +21,21 @@
 lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
   and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
   using apply_bcontfun[of x]
-  by (auto simp: intro: continuous_on_subset)
+  by (auto simp: bcontfun_def intro: continuous_on_subset)
 
 lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
   by transfer auto
 
 lemma bcontfunE:
-  assumes "continuous_on UNIV f" "bounded (range f)"
+  assumes "f \<in> bcontfun"
   obtains g where "f = apply_bcontfun g"
-  by (blast intro: apply_bcontfun_cases assms)
+  by (blast intro: apply_bcontfun_cases assms )
+
+lemma const_bcontfun: "(\<lambda>x. b) \<in> bcontfun"
+  by (auto simp: bcontfun_def continuous_on_const image_def)
 
 lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
-  by (auto intro!: continuous_intros simp: image_def)
+  by (rule const_bcontfun)
 
 (* TODO: Generalize to uniform spaces? *)
 instantiation bcontfun :: (topological_space, metric_space) metric_space
@@ -55,7 +57,7 @@
 lemma dist_bounded:
   fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
   shows "dist (f x) (g x) \<le> dist f g"
-  by transfer (auto intro!: bounded_dist_le_SUP_dist)
+  by transfer (auto intro!: bounded_dist_le_SUP_dist simp: bcontfun_def)
 
 lemma dist_bound:
   fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
@@ -98,7 +100,7 @@
 end
 
 lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set"
-  is "\<lambda>I X. Pi I X \<inter> {f. continuous_on UNIV f \<and> bounded (range f)}"
+  is "\<lambda>I X. Pi I X \<inter> bcontfun"
   by auto
 
 lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X"
@@ -141,7 +143,8 @@
   obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   where "l = l'" "(f \<longlongrightarrow> l') F"
   by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
-      mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun uniform_limit_theorem)
+      bcontfun_def mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun
+      uniform_limit_theorem)
 
 lemma closed_PiC:
   fixes I :: "'a::metric_space set"
@@ -193,23 +196,38 @@
 instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
 begin
 
+lemma uminus_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. - f x) \<in> bcontfun" for f::"'a \<Rightarrow> 'b"
+  by (auto simp: bcontfun_def intro!: continuous_intros)
+
+lemma plus_cont: "f \<in> bcontfun \<Longrightarrow> g \<in> bcontfun \<Longrightarrow> (\<lambda>x. f x + g x) \<in> bcontfun" for f g::"'a \<Rightarrow> 'b"
+  by (auto simp: bcontfun_def intro!: continuous_intros bounded_plus_comp)
+
+lemma minus_cont: "f \<in> bcontfun \<Longrightarrow> g \<in> bcontfun \<Longrightarrow> (\<lambda>x. f x - g x) \<in> bcontfun" for f g::"'a \<Rightarrow> 'b"
+  by (auto simp: bcontfun_def intro!: continuous_intros bounded_minus_comp)
+
+lemma scaleR_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun" for f :: "'a \<Rightarrow> 'b"
+  by (auto simp: bcontfun_def intro!: continuous_intros bounded_scaleR_comp)
+
+lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
+  by (auto simp: bcontfun_def intro: boundedI)
+
 lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x"
-  by (auto intro!: continuous_intros)
+  by (rule uminus_cont)
 
 lift_definition plus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x + g x"
-  by (auto simp: intro!: continuous_intros bounded_plus_comp)
+  by (rule plus_cont)
 
 lift_definition minus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x - g x"
-  by (auto simp: intro!: continuous_intros bounded_minus_comp)
+  by (rule minus_cont)
 
 lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0"
-  by (auto intro!: continuous_intros simp: image_def)
+  by (rule const_bcontfun)
 
 lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
   by transfer simp
 
 lift_definition scaleR_bcontfun::"real \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>r g x. r *\<^sub>R g x"
-  by (auto simp: intro!: continuous_intros bounded_scaleR_comp)
+  by (rule scaleR_cont)
 
 lemmas [simp] =
   const_bcontfun.rep_eq
@@ -247,13 +265,14 @@
   show "norm (f + g) \<le> norm f + norm g"
     unfolding norm_bcontfun_def
     by transfer
-      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm simp: dist_norm)
+      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm
+        simp: dist_norm bcontfun_def)
   show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
     unfolding norm_bcontfun_def
     apply transfer
     by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
       (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
-        simp: bounded_norm_comp)
+        simp: bounded_norm_comp bcontfun_def)
 qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
 
 end
@@ -286,15 +305,12 @@
     "\<And>x. g x = f (clamp a b x)"
 proof -
   define g where "g \<equiv> ext_cont f a b"
-  have "continuous_on UNIV g"
+  have "g \<in> bcontfun"
     using assms
-    by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval)
-  moreover
-  have "bounded (range g)"
-    by (auto simp: g_def ext_cont_def cbox_interval
+    by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval bcontfun_def)
+      (auto simp: g_def ext_cont_def cbox_interval
         intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
-  ultimately
-  obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
+  then obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
   then have "h x = f x" if "a \<le> x" "x \<le> b" for x
     by (auto simp: h[symmetric] g_def cbox_interval that)
   moreover