recovered typedef with set bcontfun (amending d23eded35a33)
authorimmler
Tue Mar 14 21:42:42 2017 +0100 (2017-03-14)
changeset 65205f435640193b6
parent 65204 d23eded35a33
child 65270 ed8043342c9c
recovered typedef with set bcontfun (amending d23eded35a33)
src/HOL/Analysis/Bounded_Continuous_Function.thy
     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.4  
     1.5  subsection \<open>Definition\<close>
     1.6  
     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.10  
    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.17  
    1.18  declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
    1.19  
    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.26  
    1.27  lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
    1.28    by transfer auto
    1.29  
    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.39  
    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.43  
    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.52  
    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.57  
    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.62  
    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.71  
    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.77  
    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.96  
    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.100  
   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.104  
   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.108  
   1.109  lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
   1.110    by transfer simp
   1.111  
   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.115  
   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.133  
   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