# HG changeset patch # User huffman # Date 1379034596 25200 # Node ID f2025867320a903ba1cad67c4de5d2fd51a06eff # Parent 8fda7ad57466111559f27e39067bb587c740a139# Parent 5a7bf8c859f67dc6d7a85687b8b585e7c53c89f2 merged diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Library/Convex.thy --- 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 \ convex t \ convex (s \ t)" unfolding convex_def by auto +lemma convex_INT: "\i\A. convex (B i) \ convex (\i\A. B i)" + unfolding convex_def by auto + +lemma convex_Times: "convex s \ convex t \ convex (s \ t)" + unfolding convex_def by auto + lemma convex_halfspace_le: "convex {x. inner a x \ b}" unfolding convex_def by (auto simp: inner_add intro!: convex_bound_le) diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Library/Set_Algebras.thy --- 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 \ A + B" + obtains a b where "x = a + b" and "a \ A" and "b \ 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 \ A * B" + obtains a b where "x = a * b" and "a \ A" and "b \ 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 = (\(x, y). x + y) ` (S \ T)" +lemma set_plus_image: "S + T = (\(x, y). x + y) ` (S \ T)" unfolding set_plus_def by (fastforce simp: image_iff) +lemma set_times_image: "S * T = (\(x, y). x * y) ` (S \ 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. \i\I. s i \ S i}" diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- 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 ==> \x$i\ < 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(\i. \x$i\) UNIV" by (simp add: norm_vec_def setL2_le_setsum) @@ -322,7 +322,6 @@ shows "setsum (\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 \ real ^'n" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" @@ -500,7 +499,7 @@ where "matrix f = (\ i j. (f(axis j 1))$i)" lemma matrix_vector_mul_linear: "linear(\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 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 (\x. scaleR c x)" - by (simp add: linear_def scaleR_add_right) + by (simp add: linear_iff scaleR_add_right) lemma injective_scaleR: "c \ 0 \ inj (\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 \ S" using convex_rel_interior_iff[of S "f z"] z assms `S \ {}` 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 "\e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ 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 \ 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 "\e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R f z \ S \ range f" using e by auto } diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Derivative.thy --- 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 "\e>0. \d>0. \y\s. norm (y - x) < d \ norm (g y - g x - g' x (y - x)) \ e * norm (y - x)" diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Determinants.thy --- 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 diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Integration.thy --- 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 "\x y. f (x + y) = f x + f y" and "\r x. f (r *\<^sub>R x) = r *\<^sub>R f x" and "\x. norm (f x) \ 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 (\x::'a::euclidean_space. x \ k)" by (rule bounded_linear_inner_left) @@ -4123,11 +4126,8 @@ apply rule done -lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \ 'a \ 'a) = 0" - by (rule neutral_add) (* FIXME: duplicate *) - lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \ 'a \ '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}}) (\i. if g integrable_on i then Some (integral i g) else None) = Some 0" proof(rule *,rule) case goal1 hence "x\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 (\x. f 0 x))" in exI) apply safe apply(erule_tac x="integral s (\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 \ 'n::ordered_euclidean_space \ real" assumes "\k. (f k) integrable_on s" "\k. \x\s. (f (Suc k) x) \ (f k x)" diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- 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 \ 'b::real_vector) \ bool" - where "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" - -lemma linearI: - assumes "\x y. f (x + y) = f x + f y" - 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 \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" + (is "linear f \ ?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 \ linear (\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 \ linear (\x. - f x)" - by (simp add: linear_def) + by (simp add: linear_iff) lemma linear_compose_add: "linear f \ linear g \ linear (\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 \ linear g \ linear (\x. f x - g x)" - by (simp add: linear_def algebra_simps) + by (simp add: linear_iff algebra_simps) lemma linear_compose: "linear f \ linear g \ linear (g \ 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 (\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 \ 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 \ 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 \ f (- x) = - f x" using linear_cmul [where c="-1"] by simp lemma linear_add: "linear f \ f(x + y) = f x + f y" - by (metis linear_def) + by (metis linear_iff) lemma linear_sub: "linear f \ f(x - y) = f x - f y" by (simp add: diff_minus linear_add linear_neg) @@ -354,16 +355,16 @@ definition "bilinear f \ (\x. linear (\y. f x y)) \ (\y. linear (\x. f x y))" lemma bilinear_ladd: "bilinear h \ 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 \ 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 \ 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 \ 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 \ h (- x) y = - h x y" by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul) @@ -475,7 +476,7 @@ fixes f:: "'n::euclidean_space \ '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 \ S hull s \ t \ s \ t" unfolding hull_def by blast +lemma hull_UNIV: "S hull UNIV = UNIV" + unfolding hull_def by auto + lemma hull_unique: "s \ t \ S t \ (\t'. s \ t' \ S t' \ t \ t') \ (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 \ subspace S \ 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 \ subspace S \ subspace {x. f x \ 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 (\(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 \ span B)" by (intro subspace_Times subspace_span) ultimately show "subspace ((\(a, b). a + b) ` (span A \ span B))" @@ -1521,7 +1525,7 @@ by (metis Basis_le_norm order_trans) lemma norm_bound_Basis_lt: "b \ Basis \ norm x < e \ \x \ b\ < e" - by (metis Basis_le_norm basic_trans_rules(21)) + by (metis Basis_le_norm le_less_trans) lemma norm_le_l1: "norm x \ (\b\Basis. \x \ b\)" 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 "\B. \x. norm (f x) \ 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 "\B. \x y. norm (h x y) \ B * norm x * norm y" @@ -2444,7 +2448,7 @@ (\x\ span C. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) \ (\x\ 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. \y\ 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 diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Path_Connected.thy --- 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 diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 (\i. P i) sequentially" shows "eventually (\i. P (i + k)) sequentially" - using assms unfolding eventually_sequentially by (metis trans_le_add1) - -lemma seq_offset: - assumes "(f ---> l) sequentially" - shows "((\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 \ ((\i. f(i - k)) ---> l) sequentially" - apply (rule topological_tendstoI) - apply (drule (2) topological_tendstoD) - apply (simp only: eventually_sequentially) - apply (subgoal_tac "\N k (n::nat). N + k <= n \ 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: - "((\i. f(i + k)) ---> l) sequentially \ (f ---> l) sequentially" - by (rule LIMSEQ_offset) (* FIXME: redundant *) - lemma seq_harmonic: "((\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 *} diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/NthRoot.thy --- 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) diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Number_Theory/Primes.thy --- 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) \ p dvd x^n \ 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) \ p dvd x^n \ p dvd x" + apply (induct n) apply (frule prime_ge_0_int) apply auto done +lemma prime_dvd_power_nat_iff: "prime (p::nat) \ n > 0 \ + p dvd x^n \ p dvd x" + by (cases n) (auto elim: prime_dvd_power_nat) + +lemma prime_dvd_power_int_iff: "prime (p::int) \ n > 0 \ + p dvd x^n \ 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)" diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Real_Vector_Spaces.thy --- 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 \ 'b::real_normed_vector" + +locale linear = additive f for f :: "'a::real_vector \ 'b::real_vector" + assumes scaleR: "f (scaleR r x) = scaleR r (f x)" + +lemma linearI: + assumes "\x y. f (x + y) = f x + f y" + assumes "\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 \ 'b::real_normed_vector" + assumes bounded: "\K. \x. norm (f x) \ norm x * K" begin @@ -1547,4 +1555,3 @@ qed end - diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/Transcendental.thy --- 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 "\z\ < \x\"}.*} lemma powser_insidea: - fixes x z :: "'a::real_normed_field" + fixes x z :: "'a::real_normed_div_algebra" assumes 1: "summable (\n. f n * x ^ n)" and 2: "norm z < norm x" shows "summable (\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 (\n. norm (z * inverse x) ^ n)" by (rule summable_geometric) hence "summable (\n. K * norm (z * inverse x) ^ n)" @@ -110,7 +110,7 @@ qed lemma powser_inside: - fixes f :: "nat \ 'a::{real_normed_field,banach}" + fixes f :: "nat \ 'a::{real_normed_div_algebra,banach}" shows "summable (\n. f n * (x ^ n)) \ norm z < norm x \ summable (\n. f n * (z ^ n))" diff -r 5a7bf8c859f6 -r f2025867320a src/HOL/ex/Sqrt.thy --- 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 \ 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 "\ * 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 \ 1" by (simp add: dvd_imp_le) @@ -103,4 +103,3 @@ qed end -