--- 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}*}
--- 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 *}
--- 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:
--- 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