# HG changeset patch
# User huffman
# Date 1379034557 25200
# Node ID 8fda7ad57466111559f27e39067bb587c740a139
# Parent  78ea983f79875ee36343f2107fb4d9524eb69417
make 'linear' into a sublocale of 'bounded_linear';
replace 'linear_def' with 'linear_iff'

diff -r 78ea983f7987 -r 8fda7ad57466 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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:
diff -r 78ea983f7987 -r 8fda7ad57466 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- 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
     }
diff -r 78ea983f7987 -r 8fda7ad57466 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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)"
diff -r 78ea983f7987 -r 8fda7ad57466 src/HOL/Multivariate_Analysis/Determinants.thy
--- 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
 
diff -r 78ea983f7987 -r 8fda7ad57466 src/HOL/Multivariate_Analysis/Integration.thy
--- 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
diff -r 78ea983f7987 -r 8fda7ad57466 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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
diff -r 78ea983f7987 -r 8fda7ad57466 src/HOL/Real_Vector_Spaces.thy
--- 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
-