merged
authorhuffman
Thu, 12 Sep 2013 18:09:56 -0700
changeset 53601 f2025867320a
parent 53600 8fda7ad57466 (diff)
parent 53592 5a7bf8c859f6 (current diff)
child 53602 0ae3db699a3e
merged
--- a/src/HOL/Library/Convex.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Library/Convex.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -46,6 +46,12 @@
 lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
   unfolding convex_def by auto
 
+lemma convex_INT: "\<forall>i\<in>A. convex (B i) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
+  unfolding convex_def by auto
+
+lemma convex_Times: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<times> t)"
+  unfolding convex_def by auto
+
 lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
   unfolding convex_def
   by (auto simp: inner_add intro!: convex_bound_le)
--- a/src/HOL/Library/Set_Algebras.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -90,6 +90,11 @@
 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
   by (auto simp add: set_plus_def)
 
+lemma set_plus_elim:
+  assumes "x \<in> A + B"
+  obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
+  using assms unfolding set_plus_def by fast
+
 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   by (auto simp add: elt_set_plus_def)
 
@@ -201,6 +206,11 @@
 lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
   by (auto simp add: set_times_def)
 
+lemma set_times_elim:
+  assumes "x \<in> A * B"
+  obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
+  using assms unfolding set_times_def by fast
+
 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   by (auto simp add: elt_set_times_def)
 
@@ -321,10 +331,20 @@
     - a : (- 1) *o C"
   by (auto simp add: elt_set_times_def)
 
-lemma set_plus_image:
-  fixes S T :: "'n::semigroup_add set" shows "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
+lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
   unfolding set_plus_def by (fastforce simp: image_iff)
 
+lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
+  unfolding set_times_def by (fastforce simp: image_iff)
+
+lemma finite_set_plus:
+  assumes "finite s" and "finite t" shows "finite (s + t)"
+  using assms unfolding set_plus_image by simp
+
+lemma finite_set_times:
+  assumes "finite s" and "finite t" shows "finite (s * t)"
+  using assms unfolding set_times_image by simp
+
 lemma set_setsum_alt:
   assumes fin: "finite I"
   shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -291,7 +291,7 @@
   by (metis component_le_norm_cart order_trans)
 
 lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
-  by (metis component_le_norm_cart basic_trans_rules(21))
+  by (metis component_le_norm_cart le_less_trans)
 
 lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   by (simp add: norm_vec_def setL2_le_setsum)
@@ -322,7 +322,6 @@
   shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
   by (simp add: vec_eq_iff setsum_right_distrib)
 
-(* TODO: use setsum_norm_allsubsets_bound *)
 lemma setsum_norm_allsubsets_bound_cart:
   fixes f:: "'a \<Rightarrow> real ^'n"
   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
@@ -500,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	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 12 18:09:56 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	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 12 18:09:56 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	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Thu Sep 12 18:09:56 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	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Sep 12 18:09:56 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)
@@ -4123,11 +4126,8 @@
   apply rule
   done
 
-lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
-  by (rule neutral_add) (* FIXME: duplicate *)
-
 lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
-  unfolding monoidal_def neutral_monoid
+  unfolding monoidal_def neutral_add
   by (auto simp add: algebra_simps)
 
 lemma operative_integral:
@@ -4855,12 +4855,12 @@
 proof -
   have *: "setsum f s = setsum f (support op + f s)"
     apply (rule setsum_mono_zero_right)
-    unfolding support_def neutral_monoid
+    unfolding support_def neutral_add
     using assms
     apply auto
     done
   then show ?thesis unfolding * iterate_def fold'_def setsum.eq_fold
-    unfolding neutral_monoid by (simp add: comp_def)
+    unfolding neutral_add by (simp add: comp_def)
 qed
 
 lemma additive_content_division:
@@ -5399,7 +5399,6 @@
   apply (rule iterate_nonzero_image_lemma)
   apply (rule assms monoidal_monoid)+
   unfolding assms
-  using neutral_add
   unfolding neutral_add
   using assms
   apply auto
@@ -7605,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
@@ -8506,7 +8505,7 @@
     thus ?thesis using integrable_integral unfolding g_def by auto }
 
   note iterate_eq_neutral[OF mon,unfolded neutral_lifted[OF monoidal_monoid]]
-  note * = this[unfolded neutral_monoid]
+  note * = this[unfolded neutral_add]
   have iterate:"iterate (lifted op +) (p - {{c..d}})
       (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
   proof(rule *,rule) case goal1 hence "x\<in>p" by auto note div = division_ofD(2-5)[OF p(1) this]
@@ -9415,7 +9414,7 @@
   next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
   next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
   next case goal4 thus ?case apply-apply(rule tendsto_diff)
-      using seq_offset[OF assms(3)[rule_format],of x 1] by auto
+      using LIMSEQ_ignore_initial_segment[OF assms(3)[rule_format],of x 1] by auto
   next case goal5 thus ?case using assms(4) unfolding bounded_iff
       apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
       apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
@@ -9423,7 +9422,7 @@
   note conjunctD2[OF this] note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]]
     integrable_add[OF this(1) assms(1)[rule_format,of 0]]
   thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub)
-    using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed
+    using assms(1) apply auto by(rule LIMSEQ_imp_Suc) qed
 
 lemma monotone_convergence_decreasing: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
   assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<le> (f k x)"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 12 18:09:56 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:
@@ -560,6 +561,9 @@
 lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
   unfolding hull_def by blast
 
+lemma hull_UNIV: "S hull UNIV = UNIV"
+  unfolding hull_def by auto
+
 lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
   unfolding hull_def by auto
 
@@ -744,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
@@ -753,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)
@@ -984,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))"
@@ -1521,7 +1525,7 @@
   by (metis Basis_le_norm order_trans)
 
 lemma norm_bound_Basis_lt: "b \<in> Basis \<Longrightarrow> norm x < e \<Longrightarrow> \<bar>x \<bullet> b\<bar> < e"
-  by (metis Basis_le_norm basic_trans_rules(21))
+  by (metis Basis_le_norm le_less_trans)
 
 lemma norm_le_l1: "norm x \<le> (\<Sum>b\<in>Basis. \<bar>x \<bullet> b\<bar>)"
   apply (subst euclidean_representation[of x, symmetric])
@@ -1639,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)
@@ -1653,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':
@@ -1725,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"
@@ -2444,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
@@ -2613,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])
 
@@ -2623,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/Multivariate_Analysis/Path_Connected.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -587,7 +587,7 @@
 qed
 
 lemma open_path_component:
-  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s"
   shows "open {y. path_component s x y}"
   unfolding open_contains_ball
@@ -620,7 +620,7 @@
 qed
 
 lemma open_non_path_component:
-  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s"
   shows "open(s - {y. path_component s x y})"
   unfolding open_contains_ball
@@ -648,7 +648,7 @@
 qed
 
 lemma connected_open_path_connected:
-  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s" "connected s"
   shows "path_connected s"
   unfolding path_connected_component_set
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -978,9 +978,6 @@
     unfolding th0 th1 by simp
 qed
 
-lemma connected_empty[simp, intro]: "connected {}"  (* FIXME duplicate? *)
-  by simp
-
 
 subsection{* Limit points *}
 
@@ -2125,32 +2122,20 @@
 
 text{* Some other lemmas about sequences. *}
 
-lemma sequentially_offset:
+lemma sequentially_offset: (* TODO: move to Topological_Spaces.thy *)
   assumes "eventually (\<lambda>i. P i) sequentially"
   shows "eventually (\<lambda>i. P (i + k)) sequentially"
-  using assms unfolding eventually_sequentially by (metis trans_le_add1)
-
-lemma seq_offset:
-  assumes "(f ---> l) sequentially"
-  shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
-  using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
-
-lemma seq_offset_neg:
+  using assms by (rule eventually_sequentially_seg [THEN iffD2])
+
+lemma seq_offset_neg: (* TODO: move to Topological_Spaces.thy *)
   "(f ---> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) ---> l) sequentially"
-  apply (rule topological_tendstoI)
-  apply (drule (2) topological_tendstoD)
-  apply (simp only: eventually_sequentially)
-  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n \<Longrightarrow> N <= n - k")
-  apply metis
+  apply (erule filterlim_compose)
+  apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially)
   apply arith
   done
 
-lemma seq_offset_rev:
-  "((\<lambda>i. f(i + k)) ---> l) sequentially \<Longrightarrow> (f ---> l) sequentially"
-  by (rule LIMSEQ_offset) (* FIXME: redundant *)
-
 lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
-  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc)
+  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) (* TODO: move to Limits.thy *)
 
 subsection {* More properties of closed balls *}
 
--- a/src/HOL/NthRoot.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/NthRoot.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -410,17 +410,17 @@
 lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
 unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
 
-lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, simplified]
-lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, simplified]
-lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, simplified]
-lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, simplified]
-lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, simplified]
+lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero]
+lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero]
+lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero]
+lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, unfolded real_sqrt_zero]
+lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, unfolded real_sqrt_zero]
 
-lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, simplified]
-lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, simplified]
-lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, simplified]
-lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, simplified]
-lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified]
+lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, unfolded real_sqrt_one]
+lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, unfolded real_sqrt_one]
+lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, unfolded real_sqrt_one]
+lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, unfolded real_sqrt_one]
+lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, unfolded real_sqrt_one]
 
 lemma isCont_real_sqrt: "isCont sqrt x"
 unfolding sqrt_def by (rule isCont_real_root)
--- a/src/HOL/Number_Theory/Primes.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -167,18 +167,24 @@
   by (metis div_mult_self1_is_id div_mult_self2_is_id
       int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
 
-lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
-    n > 0 --> (p dvd x^n --> p dvd x)"
-  by (induct n rule: nat_induct) auto
+lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
+  by (induct n) auto
 
-lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
-    n > 0 --> (p dvd x^n --> p dvd x)"
-  apply (induct n rule: nat_induct)
-  apply auto
+lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
+  apply (induct n)
   apply (frule prime_ge_0_int)
   apply auto
   done
 
+lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
+    p dvd x^n \<longleftrightarrow> p dvd x"
+  by (cases n) (auto elim: prime_dvd_power_nat)
+
+lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
+    p dvd x^n \<longleftrightarrow> p dvd x"
+  by (cases n) (auto elim: prime_dvd_power_int)
+
+
 subsubsection {* Make prime naively executable *}
 
 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
--- a/src/HOL/Real_Vector_Spaces.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Sep 12 18:09:56 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
-
--- a/src/HOL/Transcendental.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/Transcendental.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -57,7 +57,7 @@
   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
 
 lemma powser_insidea:
-  fixes x z :: "'a::real_normed_field"
+  fixes x z :: "'a::real_normed_div_algebra"
   assumes 1: "summable (\<lambda>n. f n * x ^ n)"
     and 2: "norm z < norm x"
   shows "summable (\<lambda>n. norm (f n * z ^ n))"
@@ -95,7 +95,7 @@
   proof -
     from 2 have "norm (norm (z * inverse x)) < 1"
       using x_neq_0
-      by (simp add: nonzero_norm_divide divide_inverse [symmetric])
+      by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
     hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
       by (rule summable_geometric)
     hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
@@ -110,7 +110,7 @@
 qed
 
 lemma powser_inside:
-  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
+  fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   shows
     "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
       summable (\<lambda>n. f n * (z ^ n))"
--- a/src/HOL/ex/Sqrt.thy	Fri Sep 13 02:55:04 2013 +0200
+++ b/src/HOL/ex/Sqrt.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -31,12 +31,12 @@
   have "p dvd m \<and> p dvd n"
   proof
     from eq have "p dvd m\<^sup>2" ..
-    with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat)
+    with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
     then obtain k where "m = p * k" ..
     with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
     with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
     then have "p dvd n\<^sup>2" ..
-    with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat)
+    with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
   qed
   then have "p dvd gcd m n" ..
   with gcd have "p dvd 1" by simp
@@ -71,12 +71,12 @@
   also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
   finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
   then have "p dvd m\<^sup>2" ..
-  with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
+  with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
   then obtain k where "m = p * k" ..
   with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
   with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
   then have "p dvd n\<^sup>2" ..
-  with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat)
+  with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
   with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
   with gcd have "p dvd 1" by simp
   then have "p \<le> 1" by (simp add: dvd_imp_le)
@@ -103,4 +103,3 @@
 qed
 
 end
-