make 'linear' into a sublocale of 'bounded_linear';
replace 'linear_def' with 'linear_iff'
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Sep 12 18:09:17 2013 -0700
@@ -499,7 +499,7 @@
where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
- by (simp add: linear_def matrix_vector_mult_def vec_eq_iff
+ by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
field_simps setsum_right_distrib setsum_addf)
lemma matrix_works:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 12 18:09:17 2013 -0700
@@ -18,7 +18,7 @@
(* ------------------------------------------------------------------------- *)
lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
- by (simp add: linear_def scaleR_add_right)
+ by (simp add: linear_iff scaleR_add_right)
lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
by (simp add: inj_on_def)
@@ -303,13 +303,13 @@
qed
lemma fst_linear: "linear fst"
- unfolding linear_def by (simp add: algebra_simps)
+ unfolding linear_iff by (simp add: algebra_simps)
lemma snd_linear: "linear snd"
- unfolding linear_def by (simp add: algebra_simps)
+ unfolding linear_iff by (simp add: algebra_simps)
lemma fst_snd_linear: "linear (%(x,y). x + y)"
- unfolding linear_def by (simp add: algebra_simps)
+ unfolding linear_iff by (simp add: algebra_simps)
lemma scaleR_2:
fixes x :: "'a::real_vector"
@@ -8098,7 +8098,7 @@
then obtain e where e: "e > 1" "(1 - e) *\<^sub>R f x + e *\<^sub>R f z \<in> S"
using convex_rel_interior_iff[of S "f z"] z assms `S \<noteq> {}` by auto
moreover have "(1 - e) *\<^sub>R f x + e *\<^sub>R f z = f ((1 - e) *\<^sub>R x + e *\<^sub>R z)"
- using `linear f` by (simp add: linear_def)
+ using `linear f` by (simp add: linear_iff)
ultimately have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> f -` S"
using e by auto
}
@@ -8116,7 +8116,7 @@
then obtain e where e: "e > 1" "(1 - e) *\<^sub>R y + e *\<^sub>R z \<in> f -` S"
using convex_rel_interior_iff[of "f -` S" z] z conv by auto
moreover have "(1 - e) *\<^sub>R x + e *\<^sub>R f z = f ((1 - e) *\<^sub>R y + e *\<^sub>R z)"
- using `linear f` y by (simp add: linear_def)
+ using `linear f` y by (simp add: linear_iff)
ultimately have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R f z \<in> S \<inter> range f"
using e by auto
}
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Sep 12 18:09:17 2013 -0700
@@ -14,7 +14,7 @@
assume "bounded_linear f"
then interpret f: bounded_linear f .
show "linear f"
- by (simp add: f.add f.scaleR linear_def)
+ by (simp add: f.add f.scaleR linear_iff)
qed
lemma netlimit_at_vector: (* TODO: move *)
@@ -1278,7 +1278,7 @@
qed
qed
show "bounded_linear (g' x)"
- unfolding linear_linear linear_def
+ unfolding linear_linear linear_iff
apply(rule,rule,rule) defer
proof(rule,rule)
fix x' y z::"'m" and c::real
@@ -1286,12 +1286,12 @@
show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
apply(rule tendsto_unique[OF trivial_limit_sequentially])
apply(rule lem3[rule_format])
- unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format]
+ unfolding lin[THEN bounded_linear_imp_linear, THEN linear_cmul]
apply (intro tendsto_intros) by(rule lem3[rule_format])
show "g' x (y + z) = g' x y + g' x z"
apply(rule tendsto_unique[OF trivial_limit_sequentially])
apply(rule lem3[rule_format])
- unfolding lin[unfolded bounded_linear_def additive_def,THEN conjunct1,rule_format]
+ unfolding lin[THEN bounded_linear_imp_linear, THEN linear_add]
apply(rule tendsto_add) by(rule lem3[rule_format])+
qed
show "\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Thu Sep 12 18:09:17 2013 -0700
@@ -1080,7 +1080,7 @@
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
note fc = this
show ?thesis
- unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
+ unfolding linear_iff vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
by (simp add: inner_add fc field_simps)
qed
--- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Sep 12 18:09:17 2013 -0700
@@ -136,18 +136,21 @@
"f 0 = 0"
"f (- a) = - f a"
"f (s *\<^sub>R v) = s *\<^sub>R (f v)"
- apply (rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR)
- using assms unfolding bounded_linear_def additive_def
- apply auto
- done
+proof -
+ interpret f: bounded_linear f by fact
+ show "f (a + b) = f a + f b" by (rule f.add)
+ show "f (a - b) = f a - f b" by (rule f.diff)
+ show "f 0 = 0" by (rule f.zero)
+ show "f (- a) = - f a" by (rule f.minus)
+ show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
+qed
lemma bounded_linearI:
assumes "\<And>x y. f (x + y) = f x + f y"
and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
and "\<And>x. norm (f x) \<le> norm x * K"
shows "bounded_linear f"
- unfolding bounded_linear_def additive_def bounded_linear_axioms_def
- using assms by auto
+ using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
by (rule bounded_linear_inner_left)
@@ -7601,7 +7604,7 @@
apply rule
apply (rule linear_continuous_at)
unfolding linear_linear
- unfolding linear_def inner_simps euclidean_eq_iff[where 'a='a]
+ unfolding linear_iff inner_simps euclidean_eq_iff[where 'a='a]
apply (auto simp add: field_simps)
done
qed auto
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Sep 12 18:09:17 2013 -0700
@@ -248,35 +248,36 @@
subsection {* Linear functions. *}
-definition linear :: "('a::real_vector \<Rightarrow> 'b::real_vector) \<Rightarrow> bool"
- where "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)"
-
-lemma linearI:
- assumes "\<And>x y. f (x + y) = f x + f y"
- and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
- shows "linear f"
- using assms unfolding linear_def by auto
+lemma linear_iff:
+ "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)"
+ (is "linear f \<longleftrightarrow> ?rhs")
+proof
+ assume "linear f" then interpret f: linear f .
+ show "?rhs" by (simp add: f.add f.scaleR)
+next
+ assume "?rhs" then show "linear f" by unfold_locales simp_all
+qed
lemma linear_compose_cmul: "linear f \<Longrightarrow> linear (\<lambda>x. c *\<^sub>R f x)"
- by (simp add: linear_def algebra_simps)
+ by (simp add: linear_iff algebra_simps)
lemma linear_compose_neg: "linear f \<Longrightarrow> linear (\<lambda>x. - f x)"
- by (simp add: linear_def)
+ by (simp add: linear_iff)
lemma linear_compose_add: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x + g x)"
- by (simp add: linear_def algebra_simps)
+ by (simp add: linear_iff algebra_simps)
lemma linear_compose_sub: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x - g x)"
- by (simp add: linear_def algebra_simps)
+ by (simp add: linear_iff algebra_simps)
lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g \<circ> f)"
- by (simp add: linear_def)
+ by (simp add: linear_iff)
lemma linear_id: "linear id"
- by (simp add: linear_def id_def)
+ by (simp add: linear_iff id_def)
lemma linear_zero: "linear (\<lambda>x. 0)"
- by (simp add: linear_def)
+ by (simp add: linear_iff)
lemma linear_compose_setsum:
assumes fS: "finite S"
@@ -288,20 +289,20 @@
done
lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
- unfolding linear_def
+ unfolding linear_iff
apply clarsimp
apply (erule allE[where x="0::'a"])
apply simp
done
lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
- by (simp add: linear_def)
+ by (simp add: linear_iff)
lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
using linear_cmul [where c="-1"] by simp
lemma linear_add: "linear f \<Longrightarrow> f(x + y) = f x + f y"
- by (metis linear_def)
+ by (metis linear_iff)
lemma linear_sub: "linear f \<Longrightarrow> f(x - y) = f x - f y"
by (simp add: diff_minus linear_add linear_neg)
@@ -354,16 +355,16 @@
definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
- by (simp add: bilinear_def linear_def)
+ by (simp add: bilinear_def linear_iff)
lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
- by (simp add: bilinear_def linear_def)
+ by (simp add: bilinear_def linear_iff)
lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
- by (simp add: bilinear_def linear_def)
+ by (simp add: bilinear_def linear_iff)
lemma bilinear_rmul: "bilinear h \<Longrightarrow> h x (c *\<^sub>R y) = c *\<^sub>R h x y"
- by (simp add: bilinear_def linear_def)
+ by (simp add: bilinear_def linear_iff)
lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul)
@@ -475,7 +476,7 @@
fixes f:: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes lf: "linear f"
shows "linear (adjoint f)"
- by (simp add: lf linear_def euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
+ by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
adjoint_clauses[OF lf] inner_simps)
lemma adjoint_adjoint:
@@ -747,7 +748,7 @@
and sS: "subspace S"
shows "subspace (f ` S)"
using lf sS linear_0[OF lf]
- unfolding linear_def subspace_def
+ unfolding linear_iff subspace_def
apply (auto simp add: image_iff)
apply (rule_tac x="x + y" in bexI)
apply auto
@@ -756,10 +757,10 @@
done
lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
- by (auto simp add: subspace_def linear_def linear_0[of f])
+ by (auto simp add: subspace_def linear_iff linear_0[of f])
lemma subspace_linear_preimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace {x. f x \<in> S}"
- by (auto simp add: subspace_def linear_def linear_0[of f])
+ by (auto simp add: subspace_def linear_iff linear_0[of f])
lemma subspace_trivial: "subspace {0}"
by (simp add: subspace_def)
@@ -987,7 +988,7 @@
by safe (force intro: span_clauses)+
next
have "linear (\<lambda>(a, b). a + b)"
- by (simp add: linear_def scaleR_add_right)
+ by (simp add: linear_iff scaleR_add_right)
moreover have "subspace (span A \<times> span B)"
by (intro subspace_Times subspace_span)
ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
@@ -1642,11 +1643,11 @@
proof
fix x y
show "f (x + y) = f x + f y"
- using `linear f` unfolding linear_def by simp
+ using `linear f` unfolding linear_iff by simp
next
fix r x
show "f (scaleR r x) = scaleR r (f x)"
- using `linear f` unfolding linear_def by simp
+ using `linear f` unfolding linear_iff by simp
next
have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
using `linear f` by (rule linear_bounded)
@@ -1656,7 +1657,7 @@
next
assume "bounded_linear f"
then interpret f: bounded_linear f .
- show "linear f" by (simp add: f.add f.scaleR linear_def)
+ show "linear f" by (simp add: f.add f.scaleR linear_iff)
qed
lemma bounded_linearI':
@@ -1728,20 +1729,20 @@
proof
fix x y z
show "h (x + y) z = h x z + h y z"
- using `bilinear h` unfolding bilinear_def linear_def by simp
+ using `bilinear h` unfolding bilinear_def linear_iff by simp
next
fix x y z
show "h x (y + z) = h x y + h x z"
- using `bilinear h` unfolding bilinear_def linear_def by simp
+ using `bilinear h` unfolding bilinear_def linear_iff by simp
next
fix r x y
show "h (scaleR r x) y = scaleR r (h x y)"
- using `bilinear h` unfolding bilinear_def linear_def
+ using `bilinear h` unfolding bilinear_def linear_iff
by simp
next
fix r x y
show "h x (scaleR r y) = scaleR r (h x y)"
- using `bilinear h` unfolding bilinear_def linear_def
+ using `bilinear h` unfolding bilinear_def linear_iff
by simp
next
have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
@@ -2447,7 +2448,7 @@
(\<forall>x\<in> span C. \<forall>c. g (c*\<^sub>R x) = c *\<^sub>R g x) \<and>
(\<forall>x\<in> C. g x = f x)" by blast
from g show ?thesis
- unfolding linear_def
+ unfolding linear_iff
using C
apply clarsimp
apply blast
@@ -2616,7 +2617,7 @@
proof -
let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
from bf bg have sp: "subspace ?P"
- unfolding bilinear_def linear_def subspace_def bf bg
+ unfolding bilinear_def linear_iff subspace_def bf bg
by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
intro: bilinear_ladd[OF bf])
@@ -2626,7 +2627,7 @@
apply (rule span_induct')
apply (simp add: fg)
apply (auto simp add: subspace_def)
- using bf bg unfolding bilinear_def linear_def
+ using bf bg unfolding bilinear_def linear_iff
apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
intro: bilinear_ladd[OF bf])
done
--- a/src/HOL/Real_Vector_Spaces.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Sep 12 18:09:17 2013 -0700
@@ -934,8 +934,16 @@
subsection {* Bounded Linear and Bilinear Operators *}
-locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
+locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
+
+lemma linearI:
+ assumes "\<And>x y. f (x + y) = f x + f y"
+ assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
+ shows "linear f"
+ by default (rule assms)+
+
+locale bounded_linear = linear f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
begin
@@ -1547,4 +1555,3 @@
qed
end
-