# HG changeset patch
# User huffman
# Date 1312919422 25200
# Node ID 7b57b9295d98c2bc7b7a4306bb0c1d686f4ecc84
# Parent  ce44e70d0c474d60557c4c613dcde87dd8384713
lemma bounded_linear_intro

diff -r ce44e70d0c47 -r 7b57b9295d98 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Aug 09 10:42:07 2011 -0700
+++ b/src/HOL/Complex.thy	Tue Aug 09 12:50:22 2011 -0700
@@ -340,16 +340,10 @@
 subsection {* Completeness of the Complexes *}
 
 interpretation Re: bounded_linear "Re"
-apply (unfold_locales, simp, simp)
-apply (rule_tac x=1 in exI)
-apply (simp add: complex_norm_def)
-done
+  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
 
 interpretation Im: bounded_linear "Im"
-apply (unfold_locales, simp, simp)
-apply (rule_tac x=1 in exI)
-apply (simp add: complex_norm_def)
-done
+  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
 
 lemma tendsto_Complex [tendsto_intros]:
   assumes "(f ---> a) net" and "(g ---> b) net"
@@ -518,11 +512,8 @@
 by (simp add: norm_mult power2_eq_square)
 
 interpretation cnj: bounded_linear "cnj"
-apply (unfold_locales)
-apply (rule complex_cnj_add)
-apply (rule complex_cnj_scaleR)
-apply (rule_tac x=1 in exI, simp)
-done
+  using complex_cnj_add complex_cnj_scaleR
+  by (rule bounded_linear_intro [where K=1], simp)
 
 
 subsection{*The Functions @{term sgn} and @{term arg}*}
diff -r ce44e70d0c47 -r 7b57b9295d98 src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Tue Aug 09 10:42:07 2011 -0700
+++ b/src/HOL/Library/FrechetDeriv.thy	Tue Aug 09 12:50:22 2011 -0700
@@ -28,29 +28,17 @@
 lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
 by (simp add: fderiv_def)
 
-lemma bounded_linear_zero:
-  "bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
-proof
-  show "(0::'b) = 0 + 0" by simp
-  fix r show "(0::'b) = scaleR r 0" by simp
-  have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
-  thus "\<exists>K. \<forall>x::'a. norm (0::'b) \<le> norm x * K" ..
-qed
+lemma bounded_linear_zero: "bounded_linear (\<lambda>x. 0)"
+  by (rule bounded_linear_intro [where K=0], simp_all)
 
 lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
-by (simp add: fderiv_def bounded_linear_zero)
+  by (simp add: fderiv_def bounded_linear_zero)
 
-lemma bounded_linear_ident:
-  "bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
-proof
-  fix x y :: 'a show "x + y = x + y" by simp
-  fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
-  have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
-  thus "\<exists>K. \<forall>x::'a. norm x \<le> norm x * K" ..
-qed
+lemma bounded_linear_ident: "bounded_linear (\<lambda>x. x)"
+  by (rule bounded_linear_intro [where K=1], simp_all)
 
 lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
-by (simp add: fderiv_def bounded_linear_ident)
+  by (simp add: fderiv_def bounded_linear_ident)
 
 subsection {* Addition *}
 
diff -r ce44e70d0c47 -r 7b57b9295d98 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:42:07 2011 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 09 12:50:22 2011 -0700
@@ -435,18 +435,12 @@
 subsection {* Pair operations are linear *}
 
 interpretation fst: bounded_linear fst
-  apply (unfold_locales)
-  apply (rule fst_add)
-  apply (rule fst_scaleR)
-  apply (rule_tac x="1" in exI, simp add: norm_Pair)
-  done
+  using fst_add fst_scaleR
+  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
 interpretation snd: bounded_linear snd
-  apply (unfold_locales)
-  apply (rule snd_add)
-  apply (rule snd_scaleR)
-  apply (rule_tac x="1" in exI, simp add: norm_Pair)
-  done
+  using snd_add snd_scaleR
+  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
 text {* TODO: move to NthRoot *}
 lemma sqrt_add_le_add_sqrt:
diff -r ce44e70d0c47 -r 7b57b9295d98 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Tue Aug 09 10:42:07 2011 -0700
+++ b/src/HOL/RealVector.thy	Tue Aug 09 12:50:22 2011 -0700
@@ -974,6 +974,13 @@
 
 end
 
+lemma bounded_linear_intro:
+  assumes "\<And>x y. f (x + y) = f x + f y"
+  assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)"
+  assumes "\<And>x. norm (f x) \<le> norm x * K"
+  shows "bounded_linear f"
+  by default (fast intro: assms)+
+
 locale bounded_bilinear =
   fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
                  \<Rightarrow> 'c::real_normed_vector"
@@ -1030,21 +1037,19 @@
 
 lemma bounded_linear_left:
   "bounded_linear (\<lambda>a. a ** b)"
-apply (unfold_locales)
+apply (cut_tac bounded, safe)
+apply (rule_tac K="norm b * K" in bounded_linear_intro)
 apply (rule add_left)
 apply (rule scaleR_left)
-apply (cut_tac bounded, safe)
-apply (rule_tac x="norm b * K" in exI)
 apply (simp add: mult_ac)
 done
 
 lemma bounded_linear_right:
   "bounded_linear (\<lambda>b. a ** b)"
-apply (unfold_locales)
+apply (cut_tac bounded, safe)
+apply (rule_tac K="norm a * K" in bounded_linear_intro)
 apply (rule add_right)
 apply (rule scaleR_right)
-apply (cut_tac bounded, safe)
-apply (rule_tac x="norm a * K" in exI)
 apply (simp add: mult_ac)
 done