lemma bounded_linear_intro
authorhuffman
Tue Aug 09 12:50:22 2011 -0700 (2011-08-09)
changeset 441277b57b9295d98
parent 44126 ce44e70d0c47
child 44128 e6c6ca74d81b
lemma bounded_linear_intro
src/HOL/Complex.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Product_Vector.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Complex.thy	Tue Aug 09 10:42:07 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Tue Aug 09 12:50:22 2011 -0700
     1.3 @@ -340,16 +340,10 @@
     1.4  subsection {* Completeness of the Complexes *}
     1.5  
     1.6  interpretation Re: bounded_linear "Re"
     1.7 -apply (unfold_locales, simp, simp)
     1.8 -apply (rule_tac x=1 in exI)
     1.9 -apply (simp add: complex_norm_def)
    1.10 -done
    1.11 +  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
    1.12  
    1.13  interpretation Im: bounded_linear "Im"
    1.14 -apply (unfold_locales, simp, simp)
    1.15 -apply (rule_tac x=1 in exI)
    1.16 -apply (simp add: complex_norm_def)
    1.17 -done
    1.18 +  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
    1.19  
    1.20  lemma tendsto_Complex [tendsto_intros]:
    1.21    assumes "(f ---> a) net" and "(g ---> b) net"
    1.22 @@ -518,11 +512,8 @@
    1.23  by (simp add: norm_mult power2_eq_square)
    1.24  
    1.25  interpretation cnj: bounded_linear "cnj"
    1.26 -apply (unfold_locales)
    1.27 -apply (rule complex_cnj_add)
    1.28 -apply (rule complex_cnj_scaleR)
    1.29 -apply (rule_tac x=1 in exI, simp)
    1.30 -done
    1.31 +  using complex_cnj_add complex_cnj_scaleR
    1.32 +  by (rule bounded_linear_intro [where K=1], simp)
    1.33  
    1.34  
    1.35  subsection{*The Functions @{term sgn} and @{term arg}*}
     2.1 --- a/src/HOL/Library/FrechetDeriv.thy	Tue Aug 09 10:42:07 2011 -0700
     2.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Tue Aug 09 12:50:22 2011 -0700
     2.3 @@ -28,29 +28,17 @@
     2.4  lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
     2.5  by (simp add: fderiv_def)
     2.6  
     2.7 -lemma bounded_linear_zero:
     2.8 -  "bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
     2.9 -proof
    2.10 -  show "(0::'b) = 0 + 0" by simp
    2.11 -  fix r show "(0::'b) = scaleR r 0" by simp
    2.12 -  have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
    2.13 -  thus "\<exists>K. \<forall>x::'a. norm (0::'b) \<le> norm x * K" ..
    2.14 -qed
    2.15 +lemma bounded_linear_zero: "bounded_linear (\<lambda>x. 0)"
    2.16 +  by (rule bounded_linear_intro [where K=0], simp_all)
    2.17  
    2.18  lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
    2.19 -by (simp add: fderiv_def bounded_linear_zero)
    2.20 +  by (simp add: fderiv_def bounded_linear_zero)
    2.21  
    2.22 -lemma bounded_linear_ident:
    2.23 -  "bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
    2.24 -proof
    2.25 -  fix x y :: 'a show "x + y = x + y" by simp
    2.26 -  fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
    2.27 -  have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
    2.28 -  thus "\<exists>K. \<forall>x::'a. norm x \<le> norm x * K" ..
    2.29 -qed
    2.30 +lemma bounded_linear_ident: "bounded_linear (\<lambda>x. x)"
    2.31 +  by (rule bounded_linear_intro [where K=1], simp_all)
    2.32  
    2.33  lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
    2.34 -by (simp add: fderiv_def bounded_linear_ident)
    2.35 +  by (simp add: fderiv_def bounded_linear_ident)
    2.36  
    2.37  subsection {* Addition *}
    2.38  
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:42:07 2011 -0700
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 09 12:50:22 2011 -0700
     3.3 @@ -435,18 +435,12 @@
     3.4  subsection {* Pair operations are linear *}
     3.5  
     3.6  interpretation fst: bounded_linear fst
     3.7 -  apply (unfold_locales)
     3.8 -  apply (rule fst_add)
     3.9 -  apply (rule fst_scaleR)
    3.10 -  apply (rule_tac x="1" in exI, simp add: norm_Pair)
    3.11 -  done
    3.12 +  using fst_add fst_scaleR
    3.13 +  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    3.14  
    3.15  interpretation snd: bounded_linear snd
    3.16 -  apply (unfold_locales)
    3.17 -  apply (rule snd_add)
    3.18 -  apply (rule snd_scaleR)
    3.19 -  apply (rule_tac x="1" in exI, simp add: norm_Pair)
    3.20 -  done
    3.21 +  using snd_add snd_scaleR
    3.22 +  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    3.23  
    3.24  text {* TODO: move to NthRoot *}
    3.25  lemma sqrt_add_le_add_sqrt:
     4.1 --- a/src/HOL/RealVector.thy	Tue Aug 09 10:42:07 2011 -0700
     4.2 +++ b/src/HOL/RealVector.thy	Tue Aug 09 12:50:22 2011 -0700
     4.3 @@ -974,6 +974,13 @@
     4.4  
     4.5  end
     4.6  
     4.7 +lemma bounded_linear_intro:
     4.8 +  assumes "\<And>x y. f (x + y) = f x + f y"
     4.9 +  assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)"
    4.10 +  assumes "\<And>x. norm (f x) \<le> norm x * K"
    4.11 +  shows "bounded_linear f"
    4.12 +  by default (fast intro: assms)+
    4.13 +
    4.14  locale bounded_bilinear =
    4.15    fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
    4.16                   \<Rightarrow> 'c::real_normed_vector"
    4.17 @@ -1030,21 +1037,19 @@
    4.18  
    4.19  lemma bounded_linear_left:
    4.20    "bounded_linear (\<lambda>a. a ** b)"
    4.21 -apply (unfold_locales)
    4.22 +apply (cut_tac bounded, safe)
    4.23 +apply (rule_tac K="norm b * K" in bounded_linear_intro)
    4.24  apply (rule add_left)
    4.25  apply (rule scaleR_left)
    4.26 -apply (cut_tac bounded, safe)
    4.27 -apply (rule_tac x="norm b * K" in exI)
    4.28  apply (simp add: mult_ac)
    4.29  done
    4.30  
    4.31  lemma bounded_linear_right:
    4.32    "bounded_linear (\<lambda>b. a ** b)"
    4.33 -apply (unfold_locales)
    4.34 +apply (cut_tac bounded, safe)
    4.35 +apply (rule_tac K="norm a * K" in bounded_linear_intro)
    4.36  apply (rule add_right)
    4.37  apply (rule scaleR_right)
    4.38 -apply (cut_tac bounded, safe)
    4.39 -apply (rule_tac x="norm a * K" in exI)
    4.40  apply (simp add: mult_ac)
    4.41  done
    4.42