author immler Tue Mar 14 21:42:42 2017 +0100 (2017-03-14) changeset 65205 f435640193b6 parent 65204 d23eded35a33 child 65270 ed8043342c9c
recovered typedef with set bcontfun (amending d23eded35a33)
1.1 --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Mar 10 23:16:40 2017 +0100
1.2 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Tue Mar 14 21:42:42 2017 +0100
1.3 @@ -7,13 +7,12 @@
1.5  subsection \<open>Definition\<close>
1.7 -definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
1.8 -  where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
1.9 +definition "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
1.11  typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
1.12 -    "{f::'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}"
1.13 +  "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
1.14    morphisms apply_bcontfun Bcontfun
1.15 -  by (auto intro: continuous_intros simp: bounded_def)
1.16 +  by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
1.18  declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
1.20 @@ -22,18 +21,21 @@
1.21  lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
1.22    and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
1.23    using apply_bcontfun[of x]
1.24 -  by (auto simp: intro: continuous_on_subset)
1.25 +  by (auto simp: bcontfun_def intro: continuous_on_subset)
1.27  lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
1.28    by transfer auto
1.30  lemma bcontfunE:
1.31 -  assumes "continuous_on UNIV f" "bounded (range f)"
1.32 +  assumes "f \<in> bcontfun"
1.33    obtains g where "f = apply_bcontfun g"
1.34 -  by (blast intro: apply_bcontfun_cases assms)
1.35 +  by (blast intro: apply_bcontfun_cases assms )
1.36 +
1.37 +lemma const_bcontfun: "(\<lambda>x. b) \<in> bcontfun"
1.38 +  by (auto simp: bcontfun_def continuous_on_const image_def)
1.40  lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
1.41 -  by (auto intro!: continuous_intros simp: image_def)
1.42 +  by (rule const_bcontfun)
1.44  (* TODO: Generalize to uniform spaces? *)
1.45  instantiation bcontfun :: (topological_space, metric_space) metric_space
1.46 @@ -55,7 +57,7 @@
1.47  lemma dist_bounded:
1.48    fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
1.49    shows "dist (f x) (g x) \<le> dist f g"
1.50 -  by transfer (auto intro!: bounded_dist_le_SUP_dist)
1.51 +  by transfer (auto intro!: bounded_dist_le_SUP_dist simp: bcontfun_def)
1.53  lemma dist_bound:
1.54    fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
1.55 @@ -98,7 +100,7 @@
1.56  end
1.58  lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set"
1.59 -  is "\<lambda>I X. Pi I X \<inter> {f. continuous_on UNIV f \<and> bounded (range f)}"
1.60 +  is "\<lambda>I X. Pi I X \<inter> bcontfun"
1.61    by auto
1.63  lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X"
1.64 @@ -141,7 +143,8 @@
1.65    obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
1.66    where "l = l'" "(f \<longlongrightarrow> l') F"
1.67    by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
1.68 -      mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun uniform_limit_theorem)
1.69 +      bcontfun_def mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun
1.70 +      uniform_limit_theorem)
1.72  lemma closed_PiC:
1.73    fixes I :: "'a::metric_space set"
1.74 @@ -193,23 +196,38 @@
1.75  instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
1.76  begin
1.78 +lemma uminus_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. - f x) \<in> bcontfun" for f::"'a \<Rightarrow> 'b"
1.79 +  by (auto simp: bcontfun_def intro!: continuous_intros)
1.80 +
1.81 +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"
1.82 +  by (auto simp: bcontfun_def intro!: continuous_intros bounded_plus_comp)
1.83 +
1.84 +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"
1.85 +  by (auto simp: bcontfun_def intro!: continuous_intros bounded_minus_comp)
1.86 +
1.87 +lemma scaleR_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun" for f :: "'a \<Rightarrow> 'b"
1.88 +  by (auto simp: bcontfun_def intro!: continuous_intros bounded_scaleR_comp)
1.89 +
1.90 +lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
1.91 +  by (auto simp: bcontfun_def intro: boundedI)
1.92 +
1.93  lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x"
1.94 -  by (auto intro!: continuous_intros)
1.95 +  by (rule uminus_cont)
1.97  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"
1.98 -  by (auto simp: intro!: continuous_intros bounded_plus_comp)
1.99 +  by (rule plus_cont)
1.101  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"
1.102 -  by (auto simp: intro!: continuous_intros bounded_minus_comp)
1.103 +  by (rule minus_cont)
1.105  lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0"
1.106 -  by (auto intro!: continuous_intros simp: image_def)
1.107 +  by (rule const_bcontfun)
1.109  lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
1.110    by transfer simp
1.112  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"
1.113 -  by (auto simp: intro!: continuous_intros bounded_scaleR_comp)
1.114 +  by (rule scaleR_cont)
1.116  lemmas [simp] =
1.117    const_bcontfun.rep_eq
1.118 @@ -247,13 +265,14 @@
1.119    show "norm (f + g) \<le> norm f + norm g"
1.120      unfolding norm_bcontfun_def
1.121      by transfer
1.122 -      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm simp: dist_norm)
1.123 +      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm
1.124 +        simp: dist_norm bcontfun_def)
1.125    show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
1.126      unfolding norm_bcontfun_def
1.127      apply transfer
1.128      by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
1.129        (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
1.130 -        simp: bounded_norm_comp)
1.131 +        simp: bounded_norm_comp bcontfun_def)
1.132  qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
1.134  end
1.135 @@ -286,15 +305,12 @@
1.136      "\<And>x. g x = f (clamp a b x)"
1.137  proof -
1.138    define g where "g \<equiv> ext_cont f a b"
1.139 -  have "continuous_on UNIV g"
1.140 +  have "g \<in> bcontfun"
1.141      using assms
1.142 -    by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval)
1.143 -  moreover
1.144 -  have "bounded (range g)"
1.145 -    by (auto simp: g_def ext_cont_def cbox_interval
1.146 +    by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval bcontfun_def)
1.147 +      (auto simp: g_def ext_cont_def cbox_interval
1.148          intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
1.149 -  ultimately
1.150 -  obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
1.151 +  then obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
1.152    then have "h x = f x" if "a \<le> x" "x \<le> b" for x
1.153      by (auto simp: h[symmetric] g_def cbox_interval that)
1.154    moreover