# HG changeset patch # User wenzelm # Date 1448230783 -3600 # Node ID d6b2d638af231aa96fb863a797a2e7d9937d2e4d # Parent a1b779ee035cfbf670198fc80fdfbd1910a7d7b6 more symbols; diff -r a1b779ee035c -r d6b2d638af23 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Nov 22 23:13:02 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Nov 22 23:19:43 2015 +0100 @@ -151,7 +151,7 @@ lemma vec_setsum: assumes "finite S" - shows "vec(setsum f S) = setsum (vec o f) S" + shows "vec(setsum f S) = setsum (vec \ f) S" using assms proof induct case empty @@ -512,7 +512,7 @@ lemma matrix_compose: assumes lf: "linear (f::real^'n \ real^'m)" and lg: "linear (g::real^'m \ real^_)" - shows "matrix (g o f) = matrix g ** matrix f" + shows "matrix (g \ f) = matrix g ** matrix f" using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) @@ -581,7 +581,7 @@ { assume A: "\x y. A *v x = A *v y \ x = y" hence i: "inj (op *v A)" unfolding inj_on_def by auto from linear_injective_left_inverse[OF matrix_vector_mul_linear i] - obtain g where g: "linear g" "g o op *v A = id" by blast + obtain g where g: "linear g" "g \ op *v A = id" by blast have "matrix g ** A = mat 1" unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] using g(2) by (simp add: fun_eq_iff) @@ -607,7 +607,7 @@ moreover { assume sf: "surj (op *v A)" from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf] - obtain g:: "real ^'m \ real ^'n" where g: "linear g" "op *v A o g = id" + obtain g:: "real ^'m \ real ^'n" where g: "linear g" "op *v A \ g = id" by blast have "A ** (matrix g) = mat 1" @@ -1066,8 +1066,8 @@ lemma affinity_inverses: assumes m0: "m \ (0::'a::field)" - shows "(\x. m *s x + c) o (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" - "(\x. inverse(m) *s x + (-(inverse(m) *s c))) o (\x. m *s x + c) = id" + shows "(\x. m *s x + c) \ (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" + "(\x. inverse(m) *s x + (-(inverse(m) *s c))) \ (\x. m *s x + c) = id" using m0 apply (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1 [symmetric]) diff -r a1b779ee035c -r d6b2d638af23 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Nov 22 23:13:02 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Nov 22 23:19:43 2015 +0100 @@ -2388,14 +2388,14 @@ fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" assumes "(f has_integral y) s" and "bounded_linear h" - shows "((h o f) has_integral ((h y))) s" + shows "((h \ f) has_integral ((h y))) s" proof - interpret bounded_linear h using assms(2) . from pos_bounded obtain B where B: "0 < B" "\x. norm (h x) \ norm x * B" by blast have lem: "\(f :: 'n \ 'a) y a b. - (f has_integral y) (cbox a b) \ ((h o f) has_integral h y) (cbox a b)" + (f has_integral y) (cbox a b) \ ((h \ f) has_integral h y) (cbox a b)" unfolding has_integral proof (clarify, goal_cases) case prems: (1 f y a b e) @@ -3580,7 +3580,7 @@ "\f g s. support opp f (s \ t) = (support opp f s) \ (support opp f t)" "\f g s. support opp f (s \ t) = (support opp f s) \ (support opp f t)" "\f g s. support opp f (s - t) = (support opp f s) - (support opp f t)" - "\f g s. support opp g (f ` s) = f ` (support opp (g o f) s)" + "\f g s. support opp g (f ` s) = f ` (support opp (g \ f) s)" unfolding support_def by auto lemma finite_support[intro]: "finite s \ finite (support opp f s)" @@ -4636,7 +4636,7 @@ assumes "finite s" and "g a = 0" and "\x\s. \y\s. f x = f y \ x \ y \ g (f x) = 0" - shows "setsum g {f x |x. x \ s \ f x \ a} = setsum (g o f) s" + shows "setsum g {f x |x. x \ s \ f x \ a} = setsum (g \ f) s" apply (subst setsum_iterate) using assms monoidal_monoid unfolding setsum_iterate[OF assms(1)] @@ -9601,7 +9601,7 @@ apply (auto simp add: image_iff Bex_def) apply presburger done - have th: "op ^ x o op + m = (\i. x^m * x^i)" + have th: "op ^ x \ op + m = (\i. x^m * x^i)" by (rule ext) (simp add: power_add power_mult) from setsum.reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]] have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" @@ -10281,7 +10281,7 @@ (*lemma absolutely_integrable_on_trans[simp]: fixes f::"'n::euclidean_space \ real" - shows "(vec1 o f) absolutely_integrable_on s \ f absolutely_integrable_on s" + shows "(vec1 \ f) absolutely_integrable_on s \ f absolutely_integrable_on s" unfolding absolutely_integrable_on_def o_def by auto*) lemma integral_norm_bound_integral: @@ -11992,7 +11992,7 @@ assumes con: "continuous_on (cbox (a,c) (b,d)) f" and x: "x \ cbox a b" shows "(\y. f (x, y)) integrable_on (cbox c d)" proof - - have "f o (\y. (x, y)) integrable_on (cbox c d)" + have "f \ (\y. (x, y)) integrable_on (cbox c d)" apply (rule integrable_continuous) apply (rule continuous_on_compose [OF _ continuous_on_subset [OF con]]) using x @@ -12276,7 +12276,7 @@ assumes "continuous_on (cbox (a,c) (b,d)) (\(x,y). f x y)" shows "continuous_on (cbox (c,a) (d,b)) (\(x, y). f y x)" proof - - have "(\(x, y). f y x) = (\(x, y). f x y) o prod.swap" + have "(\(x, y). f y x) = (\(x, y). f x y) \ prod.swap" by auto then show ?thesis apply (rule ssubst)