author wenzelm Sun, 22 Nov 2015 23:19:43 +0100 changeset 61736 d6b2d638af23 parent 61735 a1b779ee035c child 61737 b91b1ebfc8a0 child 61738 c4f6031f1310
more symbols;
```--- 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 \<circ> f) S"
using assms
proof induct
case empty
@@ -512,7 +512,7 @@
lemma matrix_compose:
assumes lf: "linear (f::real^'n \<Rightarrow> real^'m)"
and lg: "linear (g::real^'m \<Rightarrow> real^_)"
-  shows "matrix (g o f) = matrix g ** matrix f"
+  shows "matrix (g \<circ> 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: "\<forall>x y. A *v x = A *v y \<longrightarrow> 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 \<circ> 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 \<Rightarrow> real ^'n" where g: "linear g" "op *v A o g = id"
+    obtain g:: "real ^'m \<Rightarrow> real ^'n" where g: "linear g" "op *v A \<circ> g = id"
by blast

have "A ** (matrix g) = mat 1"
@@ -1066,8 +1066,8 @@

lemma affinity_inverses:
assumes m0: "m \<noteq> (0::'a::field)"
-  shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
-  "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
+  shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
+  "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id"
using m0
apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1 [symmetric])```
```--- 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 \<Rightarrow> '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 \<circ> f) has_integral ((h y))) s"
proof -
interpret bounded_linear h
using assms(2) .
from pos_bounded obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
by blast
have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
-    (f has_integral y) (cbox a b) \<Longrightarrow> ((h o f) has_integral h y) (cbox a b)"
+    (f has_integral y) (cbox a b) \<Longrightarrow> ((h \<circ> 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 @@
"\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
"\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
"\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
-  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g o f) s)"
+  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
unfolding support_def by auto

lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
@@ -4636,7 +4636,7 @@
assumes "finite s"
and "g a = 0"
and "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g (f x) = 0"
-  shows "setsum g {f x |x. x \<in> s \<and> f x \<noteq> a} = setsum (g o f) s"
+  shows "setsum g {f x |x. x \<in> s \<and> f x \<noteq> a} = setsum (g \<circ> 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 = (\<lambda>i. x^m * x^i)"
+  have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)"
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 \<Rightarrow> real"
-  shows "(vec1 o f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s"
+  shows "(vec1 \<circ> f) absolutely_integrable_on s \<longleftrightarrow> 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 \<in> cbox a b"
shows "(\<lambda>y. f (x, y)) integrable_on (cbox c d)"
proof -
-  have "f o (\<lambda>y. (x, y)) integrable_on (cbox c d)"
+  have "f \<circ> (\<lambda>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)) (\<lambda>(x,y). f x y)"
shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
proof -
-  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) o prod.swap"
+  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
by auto
then show ?thesis
apply (rule ssubst)```