--- 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
-