--- a/NEWS Mon Sep 24 22:10:24 2018 +0200
+++ b/NEWS Mon Sep 24 23:49:43 2018 +0200
@@ -12,6 +12,9 @@
* Old-style inner comments (* ... *) within the term language are no
longer supported (legacy feature in Isabelle2018).
+* Infix operators that begin or end with a "*" can now be paranthesized
+without additional spaces, eg "(*)" instead of "( * )".
+
*** Isar ***
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Sep 24 23:49:43 2018 +0200
@@ -443,9 +443,7 @@
The alternative notation \<^verbatim>\<open>(\<close>\<open>sy\<close>\<^verbatim>\<open>)\<close> is introduced in addition. Thus any
infix operator may be written in prefix form (as in Haskell), independently of
- the number of arguments in the term. To avoid conflict with the comment brackets
- \<^verbatim>\<open>(*\<close> and \<^verbatim>\<open>*)\<close>, infix operators that begin or end with a \<^verbatim>\<open>*\<close> require
- extra spaces, e.g. \<^verbatim>\<open>( * )\<close>.
+ the number of arguments.
\<close>
--- a/src/Doc/Locales/Examples3.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Doc/Locales/Examples3.thy Mon Sep 24 23:49:43 2018 +0200
@@ -416,7 +416,7 @@
using non_neg by unfold_locales (rule mult_left_mono)
text \<open>While the proof of the previous interpretation
- is straightforward from monotonicity lemmas for~@{term "( * )"}, the
+ is straightforward from monotonicity lemmas for~@{term "(*)"}, the
second proof follows a useful pattern.\<close>
sublocale %visible non_negative \<subseteq> lattice_end "(\<le>)" "\<lambda>i. n * i"
--- a/src/Doc/Main/Main_Doc.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy Mon Sep 24 23:49:43 2018 +0200
@@ -339,7 +339,7 @@
\begin{tabular}{@ {} lllllll @ {}}
@{term "(+) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "(-) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "( * ) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "(*) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "(^) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "(div) :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
@{term "(mod) :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
@@ -367,7 +367,7 @@
@{term "(+) :: int \<Rightarrow> int \<Rightarrow> int"} &
@{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} &
@{term "uminus :: int \<Rightarrow> int"} &
-@{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} &
@{term "(^) :: int \<Rightarrow> nat \<Rightarrow> int"} &
@{term "(div) :: int \<Rightarrow> int \<Rightarrow> int"}&
@{term "(mod) :: int \<Rightarrow> int \<Rightarrow> int"}&
--- a/src/HOL/Algebra/IntRing.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Algebra/IntRing.thy Mon Sep 24 23:49:43 2018 +0200
@@ -20,7 +20,7 @@
subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
abbreviation int_ring :: "int ring" ("\<Z>")
- where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
+ where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
by simp
--- a/src/HOL/Algebra/Sym_Groups.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Algebra/Sym_Groups.thy Mon Sep 24 23:49:43 2018 +0200
@@ -13,7 +13,7 @@
where "sym_group n = \<lparr> carrier = { p. p permutes {1..n} }, mult = (\<circ>), one = id \<rparr>"
definition sign_img :: "int monoid"
- where "sign_img = \<lparr> carrier = { -1, 1 }, mult = ( * ), one = 1 \<rparr>"
+ where "sign_img = \<lparr> carrier = { -1, 1 }, mult = (*), one = 1 \<rparr>"
lemma sym_group_is_group: "group (sym_group n)"
--- a/src/HOL/Algebra/UnivPoly.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1806,7 +1806,7 @@
definition
INTEG :: "int ring"
- where "INTEG = \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
+ where "INTEG = \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
lemma INTEG_cring: "cring INTEG"
by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
--- a/src/HOL/Analysis/Ball_Volume.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Ball_Volume.thy Mon Sep 24 23:49:43 2018 +0200
@@ -147,7 +147,7 @@
(auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
(\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
- \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close>
+ \<partial>(distr lborel borel ((*) (1/r))))" using \<open>r > 0\<close>
by (subst nn_integral_distr)
(auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
--- a/src/HOL/Analysis/Bochner_Integration.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1856,7 +1856,7 @@
have sf[measurable]: "\<And>i. simple_function M (s' i)"
unfolding s'_def using s(1)
- by (intro simple_function_compose2[where h="( *\<^sub>R)"] simple_function_indicator) auto
+ by (intro simple_function_compose2[where h="(*\<^sub>R)"] simple_function_indicator) auto
{ fix i
have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Mon Sep 24 23:49:43 2018 +0200
@@ -697,7 +697,7 @@
by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
-lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "( *\<^sub>R)"
+lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "(*\<^sub>R)"
by (rule bounded_linear_scaleR_right)
declare blinfun_scaleR_right.rep_eq[simp]
@@ -713,7 +713,7 @@
by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
-lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "( * )"
+lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "(*)"
by (rule bounded_linear_mult_right)
declare blinfun_mult_right.rep_eq[simp]
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Sep 24 23:49:43 2018 +0200
@@ -203,7 +203,7 @@
lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
shows "matrix(adjoint f) = transpose(matrix f)"
proof%unimportant -
- have "matrix(adjoint f) = matrix(adjoint (( *v) (matrix f)))"
+ have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
by (simp add: lf)
also have "\<dots> = transpose(matrix f)"
unfolding adjoint_matrix matrix_of_matrix_vector_mul
@@ -212,14 +212,14 @@
finally show ?thesis .
qed
-lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
+lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
using matrix_vector_mul_linear[of A]
by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
lemma%unimportant (* FIX ME needs name*)
fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
- shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
- and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
+ shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont ((*v) A) z"
+ and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S ((*v) A)"
by (simp_all add: linear_continuous_at linear_continuous_on)
lemma%unimportant scalar_invertible:
@@ -293,24 +293,24 @@
lemma%important norm_column_le_onorm:
fixes A :: "real^'n^'m"
- shows "norm(column i A) \<le> onorm(( *v) A)"
+ shows "norm(column i A) \<le> onorm((*v) A)"
proof%unimportant -
have "norm (\<chi> j. A $ j $ i) \<le> norm (A *v axis i 1)"
by (simp add: matrix_mult_dot cart_eq_inner_axis)
- also have "\<dots> \<le> onorm (( *v) A)"
+ also have "\<dots> \<le> onorm ((*v) A)"
using onorm [OF matrix_vector_mul_bounded_linear, of A "axis i 1"] by auto
- finally have "norm (\<chi> j. A $ j $ i) \<le> onorm (( *v) A)" .
+ finally have "norm (\<chi> j. A $ j $ i) \<le> onorm ((*v) A)" .
then show ?thesis
unfolding column_def .
qed
lemma%important matrix_component_le_onorm:
fixes A :: "real^'n^'m"
- shows "\<bar>A $ i $ j\<bar> \<le> onorm(( *v) A)"
+ shows "\<bar>A $ i $ j\<bar> \<le> onorm((*v) A)"
proof%unimportant -
have "\<bar>A $ i $ j\<bar> \<le> norm (\<chi> n. (A $ n $ j))"
by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta)
- also have "\<dots> \<le> onorm (( *v) A)"
+ also have "\<dots> \<le> onorm ((*v) A)"
by (metis (no_types) column_def norm_column_le_onorm)
finally show ?thesis .
qed
@@ -322,7 +322,7 @@
lemma%important onorm_le_matrix_component_sum:
fixes A :: "real^'n^'m"
- shows "onorm(( *v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
+ shows "onorm((*v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
proof%unimportant (rule onorm_le)
fix x
have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
@@ -345,7 +345,7 @@
lemma%important onorm_le_matrix_component:
fixes A :: "real^'n^'m"
assumes "\<And>i j. abs(A$i$j) \<le> B"
- shows "onorm(( *v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
+ shows "onorm((*v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
proof%unimportant (rule onorm_le)
fix x :: "real^'n::_"
have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
@@ -403,13 +403,13 @@
by (auto simp: lambda_skolem Bex_def)
show ?thesis
proof
- have "onorm (( *v) (A - B)) \<le> real CARD('m) * real CARD('n) *
+ have "onorm ((*v) (A - B)) \<le> real CARD('m) * real CARD('n) *
(e / (2 * real CARD('m) * real CARD('n)))"
apply (rule onorm_le_matrix_component)
using Bclo by (simp add: abs_minus_commute less_imp_le)
also have "\<dots> < e"
using \<open>0 < e\<close> by (simp add: divide_simps)
- finally show "onorm (( *v) (A - B)) < e" .
+ finally show "onorm ((*v) (A - B)) < e" .
qed (use B in auto)
qed
@@ -778,7 +778,7 @@
where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
proof%unimportant -
from assms obtain s where "finite s"
- and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s"
+ and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s"
by (rule cube_convex_hull)
with that[of s] show thesis
by (simp add: const_vector_cart)
@@ -982,11 +982,11 @@
using basis_exists [of "span(rows A)"] by metis
with span_subspace have eq: "span B = span(rows A)"
by auto
- then have inj: "inj_on (( *v) A) (span B)"
+ then have inj: "inj_on ((*v) A) (span B)"
by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
- then have ind: "independent (( *v) A ` B)"
+ then have ind: "independent ((*v) A ` B)"
by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
- have "dim (span (rows A)) \<le> card (( *v) A ` B)"
+ have "dim (span (rows A)) \<le> card ((*v) A ` B)"
unfolding B(2)[symmetric]
using inj
by (auto simp: card_image inj_on_subset span_superset)
@@ -1017,7 +1017,7 @@
lemma%unimportant columns_image_basis:
fixes A :: "real^'n^'m"
- shows "columns A = ( *v) A ` (range (\<lambda>i. axis i 1))"
+ shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
by (force simp: columns_def matrix_vector_mult_basis [symmetric])
lemma%important rank_dim_range:
@@ -1025,7 +1025,7 @@
shows "rank A = dim(range (\<lambda>x. A *v x))"
unfolding column_rank_def
proof%unimportant (rule span_eq_dim)
- have "span (columns A) \<subseteq> span (range (( *v) A))" (is "?l \<subseteq> ?r")
+ have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
by (simp add: columns_image_basis image_subsetI span_mono)
then show "?l = ?r"
by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
@@ -1040,13 +1040,13 @@
lemma%unimportant full_rank_injective:
fixes A :: "real^'n^'m"
- shows "rank A = CARD('n) \<longleftrightarrow> inj (( *v) A)"
+ shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
lemma%unimportant full_rank_surjective:
fixes A :: "real^'n^'m"
- shows "rank A = CARD('m) \<longleftrightarrow> surj (( *v) A)"
+ shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
@@ -1055,7 +1055,7 @@
lemma%unimportant less_rank_noninjective:
fixes A :: "real^'n^'m"
- shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj (( *v) A)"
+ shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
lemma%unimportant matrix_nonfull_linear_equations_eq:
@@ -1071,7 +1071,7 @@
fixes A :: "real^'n^'m" and B :: "real^'p^'n"
shows "rank(A ** B) \<le> rank B"
proof%unimportant -
- have "rank(A ** B) \<le> dim (( *v) A ` range (( *v) B))"
+ have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
also have "\<dots> \<le> rank B"
by (simp add: rank_dim_range dim_image_le)
@@ -1137,7 +1137,7 @@
lemma has_derivative_vector_1:
assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
- shows "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' a))
+ shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
(at ((vec a)::real^1) within vec ` S)"
using der_g
apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
--- a/src/HOL/Analysis/Cartesian_Space.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy Mon Sep 24 23:49:43 2018 +0200
@@ -20,7 +20,7 @@
unfolding cart_basis_def Setcompr_eq_image
by (rule card_image) (auto simp: inj_on_def axis_eq_axis)
-interpretation vec: vector_space "( *s) "
+interpretation vec: vector_space "(*s) "
by unfold_locales (vector algebra_simps)+
lemma%unimportant independent_cart_basis:
@@ -90,11 +90,11 @@
qed
(*Some interpretations:*)
-interpretation vec: finite_dimensional_vector_space "( *s)" "cart_basis"
+interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis"
by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis)
lemma%unimportant matrix_vector_mul_linear_gen[intro, simp]:
- "Vector_Spaces.linear ( *s) ( *s) (( *v) A)"
+ "Vector_Spaces.linear (*s) (*s) ((*v) A)"
by unfold_locales
(vector matrix_vector_mult_def sum.distrib algebra_simps)+
@@ -108,10 +108,10 @@
lemma%important linear_componentwise:
fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
- assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
+ assumes lf: "Vector_Spaces.linear (*s) (*s) f"
shows "(f x)$j = sum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
proof%unimportant -
- interpret lf: Vector_Spaces.linear "( *s)" "( *s)" f
+ interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f
using lf .
let ?M = "(UNIV :: 'm set)"
let ?N = "(UNIV :: 'n set)"
@@ -123,13 +123,13 @@
unfolding basis_expansion by auto
qed
-interpretation vec: Vector_Spaces.linear "( *s)" "( *s)" "( *v) A"
+interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A"
using matrix_vector_mul_linear_gen.
-interpretation vec: finite_dimensional_vector_space_pair "( *s)" cart_basis "( *s)" cart_basis ..
+interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis ..
lemma%unimportant matrix_works:
- assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
+ assumes lf: "Vector_Spaces.linear (*s) (*s) f"
shows "matrix f *v x = f (x::'a::field ^ 'n)"
apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
apply clarify
@@ -140,8 +140,8 @@
by (simp add: matrix_eq matrix_works)
lemma%unimportant matrix_compose_gen:
- assumes lf: "Vector_Spaces.linear ( *s) ( *s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
- and lg: "Vector_Spaces.linear ( *s) ( *s) (g::'a^'m \<Rightarrow> 'a^_)"
+ assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
+ and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \<Rightarrow> 'a^_)"
shows "matrix (g o f) = matrix g ** matrix f"
using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]]
by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
@@ -161,11 +161,11 @@
by (metis matrix_transpose_mul transpose_mat transpose_transpose)
lemma%unimportant linear_matrix_vector_mul_eq:
- "Vector_Spaces.linear ( *s) ( *s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
+ "Vector_Spaces.linear (*s) (*s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
by (simp add: scalar_mult_eq_scaleR linear_def)
lemma%unimportant matrix_vector_mul[simp]:
- "Vector_Spaces.linear ( *s) ( *s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
+ "Vector_Spaces.linear (*s) (*s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
"linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
"bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
for f :: "real^'n \<Rightarrow> real ^'m"
@@ -173,20 +173,20 @@
lemma%important matrix_left_invertible_injective:
fixes A :: "'a::field^'n^'m"
- shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
+ shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj ((*v) A)"
proof%unimportant safe
fix B
assume B: "B ** A = mat 1"
- show "inj (( *v) A)"
+ show "inj ((*v) A)"
unfolding inj_on_def
by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
next
- assume "inj (( *v) A)"
+ assume "inj ((*v) A)"
from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
- obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \<circ> ( *v) A = id"
+ obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
by blast
have "matrix g ** A = mat 1"
- by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear ( *s) ( *s) g\<close> g matrix_compose_gen
+ by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
then show "\<exists>B. B ** A = mat 1"
by metis
@@ -206,11 +206,11 @@
{ fix x :: "'a ^ 'm"
have "A *v (B *v x) = x"
by (simp add: matrix_vector_mul_assoc AB) }
- hence "surj (( *v) A)" unfolding surj_def by metis }
+ hence "surj ((*v) A)" unfolding surj_def by metis }
moreover
- { assume sf: "surj (( *v) A)"
+ { assume sf: "surj ((*v) A)"
from vec.linear_surjective_right_inverse[OF _ this]
- obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \<circ> g = id"
+ obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
by blast
have "A ** (matrix g) = mat 1"
@@ -339,11 +339,11 @@
proof%unimportant -
{ fix A A' :: "'a ^'n^'n"
assume AA': "A ** A' = mat 1"
- have sA: "surj (( *v) A)"
+ have sA: "surj ((*v) A)"
using AA' matrix_right_invertible_surjective by auto
from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
- where f': "Vector_Spaces.linear ( *s) ( *s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
+ where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
have th: "matrix f' ** A = mat 1"
by (simp add: matrix_eq matrix_works[OF f'(1)]
matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
@@ -448,13 +448,13 @@
finally show ?thesis .
qed
-interpretation vector_space_over_itself: vector_space "( *) :: 'a::field => 'a => 'a"
+interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a"
by unfold_locales (simp_all add: algebra_simps)
lemmas [simp del] = vector_space_over_itself.scale_scale
interpretation vector_space_over_itself: finite_dimensional_vector_space
- "( *) :: 'a::field => 'a => 'a" "{1}"
+ "(*) :: 'a::field => 'a => 'a" "{1}"
by unfold_locales (auto simp: vector_space_over_itself.span_singleton)
lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Sep 24 23:49:43 2018 +0200
@@ -228,7 +228,7 @@
lemma continuous_on_joinpaths_D1:
"continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1"
- apply (rule continuous_on_eq [of _ "(g1 +++ g2) \<circ> (( *)(inverse 2))"])
+ apply (rule continuous_on_eq [of _ "(g1 +++ g2) \<circ> ((*)(inverse 2))"])
apply (rule continuous_intros | simp)+
apply (auto elim!: continuous_on_subset simp: joinpaths_def)
done
@@ -251,13 +251,13 @@
show ?thesis
unfolding piecewise_differentiable_on_def
proof (intro exI conjI ballI cont)
- show "finite (insert 1 ((( *)2) ` S))"
+ show "finite (insert 1 (((*)2) ` S))"
by (simp add: \<open>finite S\<close>)
- show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
+ show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}"
by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
- then show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x within {0..1}"
+ then show "g1 +++ g2 \<circ> (*) (inverse 2) differentiable at x within {0..1}"
by (auto intro: differentiable_chain_within)
qed (use that in \<open>auto simp: joinpaths_def\<close>)
qed
@@ -598,49 +598,49 @@
and co12: "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
and g12D: "\<forall>x\<in>{0..1} - S. g1 +++ g2 differentiable at x"
using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
- have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
+ have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
proof (rule differentiable_transform_within)
- show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x"
+ show "g1 +++ g2 \<circ> (*) (inverse 2) differentiable at x"
using that g12D
apply (simp only: joinpaths_def)
by (rule differentiable_chain_at derivative_intros | force)+
show "\<And>x'. \<lbrakk>dist x' x < dist (x/2) (1/2)\<rbrakk>
- \<Longrightarrow> (g1 +++ g2 \<circ> ( *) (inverse 2)) x' = g1 x'"
+ \<Longrightarrow> (g1 +++ g2 \<circ> (*) (inverse 2)) x' = g1 x'"
using that by (auto simp: dist_real_def joinpaths_def)
qed (use that in \<open>auto simp: dist_real_def\<close>)
- have [simp]: "vector_derivative (g1 \<circ> ( *) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
- if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
+ have [simp]: "vector_derivative (g1 \<circ> (*) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
+ if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
apply (subst vector_derivative_chain_at)
using that
apply (rule derivative_eq_intros g1D | simp)+
done
have "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
using co12 by (rule continuous_on_subset) force
- then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 \<circ> ( *)2) (at x))"
+ then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 \<circ> (*)2) (at x))"
proof (rule continuous_on_eq [OF _ vector_derivative_at])
- show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \<circ> ( *) 2) (at x)) (at x)"
+ show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \<circ> (*) 2) (at x)) (at x)"
if "x \<in> {0..1/2} - insert (1/2) S" for x
proof (rule has_vector_derivative_transform_within)
- show "(g1 \<circ> ( *) 2 has_vector_derivative vector_derivative (g1 \<circ> ( *) 2) (at x)) (at x)"
+ show "(g1 \<circ> (*) 2 has_vector_derivative vector_derivative (g1 \<circ> (*) 2) (at x)) (at x)"
using that
by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric])
- show "\<And>x'. \<lbrakk>dist x' x < dist x (1/2)\<rbrakk> \<Longrightarrow> (g1 \<circ> ( *) 2) x' = (g1 +++ g2) x'"
+ show "\<And>x'. \<lbrakk>dist x' x < dist x (1/2)\<rbrakk> \<Longrightarrow> (g1 \<circ> (*) 2) x' = (g1 +++ g2) x'"
using that by (auto simp: dist_norm joinpaths_def)
qed (use that in \<open>auto simp: dist_norm\<close>)
qed
- have "continuous_on ({0..1} - insert 1 (( *) 2 ` S))
- ((\<lambda>x. 1/2 * vector_derivative (g1 \<circ> ( *)2) (at x)) \<circ> ( *)(1/2))"
+ have "continuous_on ({0..1} - insert 1 ((*) 2 ` S))
+ ((\<lambda>x. 1/2 * vector_derivative (g1 \<circ> (*)2) (at x)) \<circ> (*)(1/2))"
apply (rule continuous_intros)+
using coDhalf
apply (simp add: scaleR_conv_of_real image_set_diff image_image)
done
- then have con_g1: "continuous_on ({0..1} - insert 1 (( *) 2 ` S)) (\<lambda>x. vector_derivative g1 (at x))"
+ then have con_g1: "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) (\<lambda>x. vector_derivative g1 (at x))"
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
have "continuous_on {0..1} g1"
using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
with \<open>finite S\<close> show ?thesis
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
- apply (rule_tac x="insert 1 ((( *)2)`S)" in exI)
+ apply (rule_tac x="insert 1 (((*)2)`S)" in exI)
apply (simp add: g1D con_g1)
done
qed
@@ -959,7 +959,7 @@
apply (rule piecewise_C1_differentiable_compose)
using assms
apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
- apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
+ apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
done
moreover have "(g2 \<circ> (\<lambda>x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
apply (rule piecewise_C1_differentiable_compose)
@@ -1030,9 +1030,9 @@
apply (auto simp: algebra_simps vector_derivative_works)
done
have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
- apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (( *)2 -` s1)"])
+ apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) ((*)2 -` s1)"])
using s1
- apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
+ apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
done
moreover have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
@@ -1608,7 +1608,7 @@
by (simp add: has_vector_derivative_def scaleR_conv_of_real)
have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
- then have fdiff: "(f has_derivative ( *) (f' (g x))) (at (g x) within g ` {a..b})"
+ then have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {a..b})"
by (simp add: has_field_derivative_def)
have "((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})"
using diff_chain_within [OF gdiff fdiff]
@@ -6158,9 +6158,9 @@
case 0 then show ?case by simp
next
case (Suc n z)
- have holo0: "f holomorphic_on ( *) u ` S"
+ have holo0: "f holomorphic_on (*) u ` S"
by (meson fg f holomorphic_on_subset image_subset_iff)
- have holo2: "(deriv ^^ n) f holomorphic_on ( * ) u ` S"
+ have holo2: "(deriv ^^ n) f holomorphic_on (*) u ` S"
by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on S"
by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
@@ -6182,7 +6182,7 @@
apply (blast intro: fg)
done
also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
- apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "( *) u", unfolded o_def])
+ apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "(*) u", unfolded o_def])
apply (rule derivative_intros)
using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv T apply blast
apply (simp add: deriv_linear)
--- a/src/HOL/Analysis/Change_Of_Vars.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Mon Sep 24 23:49:43 2018 +0200
@@ -186,7 +186,7 @@
qed
lemma%unimportant matrix_vector_mult_matrix_matrix_mult_compose:
- "( *v) (A ** B) = ( *v) A \<circ> ( *v) B"
+ "(*v) (A ** B) = (*v) A \<circ> (*v) B"
by (auto simp: matrix_vector_mul_assoc)
lemma%unimportant induct_linear_elementary:
@@ -199,17 +199,17 @@
and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
shows "P f"
proof -
- have "P (( *v) A)" for A
+ have "P ((*v) A)" for A
proof (rule induct_matrix_elementary_alt)
fix A B
- assume "P (( *v) A)" and "P (( *v) B)"
- then show "P (( *v) (A ** B))"
+ assume "P ((*v) A)" and "P ((*v) B)"
+ then show "P ((*v) (A ** B))"
by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
intro!: comp)
next
fix A :: "real^'n^'n" and i
assume "row i A = 0"
- show "P (( *v) A)"
+ show "P ((*v) A)"
using matrix_vector_mul_linear
by (rule zeroes[where i=i])
(metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta)
@@ -218,9 +218,9 @@
assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
- then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = (( *v) A)"
+ then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = ((*v) A)"
by (auto simp: 0 matrix_vector_mult_def)
- then show "P (( *v) A)"
+ then show "P ((*v) A)"
using const [of "\<lambda>i. A $ i $ i"] by simp
next
fix m n :: "'n"
@@ -229,9 +229,9 @@
(\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
for i and x :: "real^'n"
unfolding swap_def by (rule sum.cong) auto
- have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = (( *v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
+ have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
- with swap [OF \<open>m \<noteq> n\<close>] show "P (( *v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
+ with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
by (simp add: mat_def matrix_vector_mult_def)
next
fix m n :: "'n"
@@ -239,10 +239,10 @@
then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
- (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
+ ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
unfolding matrix_vector_mult_def of_bool_def
by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
- then show "P (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
+ then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
using idplus [OF \<open>m \<noteq> n\<close>] by simp
qed
then show ?thesis
@@ -1496,21 +1496,21 @@
\<le> sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}"
by (rule sum_mono) (simp add: indicator_def divide_simps)
next
- have \<alpha>: "?a = (\<Sum>k \<in> ( *)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
+ have \<alpha>: "?a = (\<Sum>k \<in> (*)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
have \<beta>: "sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
= (\<Sum>k \<in> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
- have 0: "( *) 2 ` {k \<in> \<int>. P k} \<inter> (\<lambda>x. 2 * x + 1) ` {k \<in> \<int>. P k} = {}" for P :: "real \<Rightarrow> bool"
+ have 0: "(*) 2 ` {k \<in> \<int>. P k} \<inter> (\<lambda>x. 2 * x + 1) ` {k \<in> \<int>. P k} = {}" for P :: "real \<Rightarrow> bool"
proof -
have "2 * i \<noteq> 2 * j + 1" for i j :: int by arith
thus ?thesis
unfolding Ints_def by auto (use of_int_eq_iff in fastforce)
qed
have "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
- = (\<Sum>k \<in> ( *)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
+ = (\<Sum>k \<in> (*)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
unfolding \<alpha> \<beta>
using finite_abs_int_segment [of "2 ^ (2*n)"]
@@ -1519,7 +1519,7 @@
proof (rule sum_mono2)
show "finite {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
by (rule finite_abs_int_segment)
- show "( *) 2 ` {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2^(2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2^(2*n)} \<subseteq> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
+ show "(*) 2 ` {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2^(2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2^(2*n)} \<subseteq> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
apply auto
using one_le_power [of "2::real" "2*n"] by linarith
have *: "\<lbrakk>x \<in> (S \<union> T) - U; \<And>x. x \<in> S \<Longrightarrow> x \<in> U; \<And>x. x \<in> T \<Longrightarrow> x \<in> U\<rbrakk> \<Longrightarrow> P x" for S T U P
@@ -1535,7 +1535,7 @@
qed
then show "0 \<le> b/2 ^ Suc n * indicator {y. b/2 ^ Suc n \<le> f y \<and> f y < (b + 1)/2 ^ Suc n} x"
if "b \<in> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)} -
- (( *) 2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)})" for b
+ ((*) 2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)})" for b
using that by (simp add: indicator_def divide_simps)
qed
finally show "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<le> ?b" .
@@ -2121,8 +2121,8 @@
moreover
interpret linear "f' x" by fact
have "(matrix (f' x) - B) *v w = 0" for w
- proof (rule lemma_partial_derivatives [of "( *v) (matrix (f' x) - B)"])
- show "linear (( *v) (matrix (f' x) - B))"
+ proof (rule lemma_partial_derivatives [of "(*v) (matrix (f' x) - B)"])
+ show "linear ((*v) (matrix (f' x) - B))"
by (rule matrix_vector_mul_linear)
have "((\<lambda>y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
using tendsto_minus [OF lim_df] by (simp add: algebra_simps divide_simps)
@@ -2141,19 +2141,19 @@
proof (rule eventually_sequentiallyI)
fix k :: "nat"
assume "0 \<le> k"
- have "0 \<le> onorm (( *v) (A k - B))"
+ have "0 \<le> onorm ((*v) (A k - B))"
using matrix_vector_mul_bounded_linear
by (rule onorm_pos_le)
- then show "norm (onorm (( *v) (A k - B))) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>(A k - B) $ i $ j\<bar>)"
+ then show "norm (onorm ((*v) (A k - B))) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>(A k - B) $ i $ j\<bar>)"
by (simp add: onorm_le_matrix_component_sum del: vector_minus_component)
qed
next
show "?g \<longlonglongrightarrow> 0"
using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: tendsto_null_sum)
qed
- with \<open>e > 0\<close> obtain p where "\<And>n. n \<ge> p \<Longrightarrow> \<bar>onorm (( *v) (A n - B))\<bar> < e/2"
+ with \<open>e > 0\<close> obtain p where "\<And>n. n \<ge> p \<Longrightarrow> \<bar>onorm ((*v) (A n - B))\<bar> < e/2"
unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral)
- then have pqe2: "\<bar>onorm (( *v) (A (p + q) - B))\<bar> < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*)
+ then have pqe2: "\<bar>onorm ((*v) (A (p + q) - B))\<bar> < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*)
using le_add1 by blast
show "\<exists>d>0. \<forall>y\<in>S. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow>
inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e"
@@ -2196,12 +2196,12 @@
by (simp add: algebra_simps diff lin_df matrix_vector_mul_linear scalar_mult_eq_scaleR)
qed
qed (use x in \<open>simp; auto simp: not_less\<close>)
- ultimately have "f' x = ( *v) B"
+ ultimately have "f' x = (*v) B"
by (force simp: algebra_simps scalar_mult_eq_scaleR)
show "matrix (f' x) $ m $ n \<le> b"
proof (rule tendsto_upperbound [of "\<lambda>i. (A i $ m $ n)" _ sequentially])
show "(\<lambda>i. A i $ m $ n) \<longlonglongrightarrow> matrix (f' x) $ m $ n"
- by (simp add: B \<open>f' x = ( *v) B\<close>)
+ by (simp add: B \<open>f' x = (*v) B\<close>)
show "\<forall>\<^sub>F i in sequentially. A i $ m $ n \<le> b"
by (simp add: Ab less_eq_real_def)
qed auto
@@ -2214,7 +2214,7 @@
using f [OF \<open>x \<in> S\<close>] unfolding Deriv.has_derivative_at_within Lim_within
by (auto simp: field_simps dest: spec [of _ "e/2"])
let ?A = "matrix(f' x) - (\<chi> i j. if i = m \<and> j = n then e / 4 else 0)"
- obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm(( *v) (?A - B)) < e/6"
+ obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm((*v) (?A - B)) < e/6"
using matrix_rational_approximation \<open>e > 0\<close>
by (metis zero_less_divide_iff zero_less_numeral)
show "\<exists>d>0. \<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and>
@@ -2224,7 +2224,7 @@
by (rule \<open>d>0\<close>)
show "B $ m $ n < b"
proof -
- have "\<bar>matrix (( *v) (?A - B)) $ m $ n\<bar> \<le> onorm (( *v) (?A - B))"
+ have "\<bar>matrix ((*v) (?A - B)) $ m $ n\<bar> \<le> onorm ((*v) (?A - B))"
using component_le_onorm [OF matrix_vector_mul_linear, of _ m n] by metis
then show ?thesis
using b Bo_e6 by simp
@@ -3805,12 +3805,12 @@
let ?drop = "(\<lambda>x::real^1. x $ 1)"
have S': "?lift ` S \<in> sets lebesgue"
by (auto intro: differentiable_image_in_sets_lebesgue [OF S] differentiable_vec)
- have "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' z)) (at (vec z) within ?lift ` S)"
+ have "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' z)) (at (vec z) within ?lift ` S)"
if "z \<in> S" for z
using der_g [OF that]
by (simp add: has_vector_derivative_def has_derivative_vector_1)
then have der': "\<And>x. x \<in> ?lift ` S \<Longrightarrow>
- (?lift \<circ> g \<circ> ?drop has_derivative ( *\<^sub>R) (g' (?drop x))) (at x within ?lift ` S)"
+ (?lift \<circ> g \<circ> ?drop has_derivative (*\<^sub>R) (g' (?drop x))) (at x within ?lift ` S)"
by (auto simp: o_def)
have inj': "inj_on (vec \<circ> g \<circ> ?drop) (vec ` S)"
using inj by (simp add: inj_on_def)
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 24 23:49:43 2018 +0200
@@ -16,7 +16,7 @@
lemma has_derivative_mult_right:
fixes c:: "'a :: real_normed_algebra"
- shows "((( * ) c) has_derivative (( * ) c)) F"
+ shows "(((*) c) has_derivative ((*) c)) F"
by (rule has_derivative_mult_right [OF has_derivative_ident])
lemma has_derivative_of_real[derivative_intros, simp]:
@@ -25,7 +25,7 @@
lemma has_vector_derivative_real_field:
"DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
- using has_derivative_compose[of of_real of_real a _ f "( * ) f'"]
+ using has_derivative_compose[of of_real of_real a _ f "(*) f'"]
by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
@@ -59,10 +59,10 @@
shows "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
using assms by (intro vector_derivative_cnj_within) auto
-lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
+lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
by auto
-lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
+lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
by auto
lemma uniformly_continuous_on_cmul_right [continuous_intros]:
@@ -283,7 +283,7 @@
lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
by (metis holomorphic_transform)
-lemma holomorphic_on_linear [simp, holomorphic_intros]: "(( * ) c) holomorphic_on s"
+lemma holomorphic_on_linear [simp, holomorphic_intros]: "((*) c) holomorphic_on s"
unfolding holomorphic_on_def by (metis field_differentiable_linear)
lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
@@ -572,7 +572,7 @@
finally show ?thesis .
qed
-lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on S"
+lemma analytic_on_linear [analytic_intros,simp]: "((*) c) analytic_on S"
by (auto simp add: analytic_on_holomorphic)
lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on S"
@@ -905,9 +905,9 @@
by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
"\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
- from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
+ from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
by (simp add: has_field_derivative_def S)
- have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
+ have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
--- a/src/HOL/Analysis/Conformal_Mappings.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1133,10 +1133,10 @@
done
with \<open>e>0\<close> show ?thesis by force
qed
- have "inj (( * ) (deriv f \<xi>))"
+ have "inj ((*) (deriv f \<xi>))"
using dnz by simp
- then obtain g' where g': "linear g'" "g' \<circ> ( * ) (deriv f \<xi>) = id"
- using linear_injective_left_inverse [of "( * ) (deriv f \<xi>)"]
+ then obtain g' where g': "linear g'" "g' \<circ> (*) (deriv f \<xi>) = id"
+ using linear_injective_left_inverse [of "(*) (deriv f \<xi>)"]
by (auto simp: linear_times)
show ?thesis
apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g'])
@@ -2083,10 +2083,10 @@
apply (simp add: C_def False fo)
apply (simp add: derivative_intros dfa complex_derivative_chain)
done
- have sb1: "( * ) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
+ have sb1: "(*) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
\<subseteq> f ` ball a r"
using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
- have sb2: "ball (C * r * b) r' \<subseteq> ( * ) (C * r) ` ball b t"
+ have sb2: "ball (C * r * b) r' \<subseteq> (*) (C * r) ` ball b t"
if "1 / 12 < t" for b t
proof -
have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
--- a/src/HOL/Analysis/Connected.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Connected.thy Mon Sep 24 23:49:43 2018 +0200
@@ -2257,14 +2257,14 @@
unfolding dist_norm
using norm_scaleR[of c "(1 / c) *\<^sub>R y - x", unfolded scaleR_right_diff_distrib, unfolded scaleR_scaleR] assms(1)
assms(1)[unfolded zero_less_abs_iff[symmetric]] by (simp del:zero_less_abs_iff)
- then have "y \<in> ( *\<^sub>R) c ` s"
- using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "( *\<^sub>R) c"]
+ then have "y \<in> (*\<^sub>R) c ` s"
+ using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "(*\<^sub>R) c"]
using e[THEN spec[where x="(1 / c) *\<^sub>R y"]]
using assms(1)
unfolding dist_norm scaleR_scaleR
by auto
}
- ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> ( *\<^sub>R) c ` s"
+ ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> (*\<^sub>R) c ` s"
apply (rule_tac x="e * \<bar>c\<bar>" in exI, auto)
done
}
@@ -2311,10 +2311,10 @@
proof -
have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)"
unfolding o_def ..
- have "(+) a ` ( *\<^sub>R) c ` S = ((+) a \<circ> ( *\<^sub>R) c) ` S"
+ have "(+) a ` (*\<^sub>R) c ` S = ((+) a \<circ> (*\<^sub>R) c) ` S"
by auto
then show ?thesis
- using assms open_translation[of "( *\<^sub>R) c ` S" a]
+ using assms open_translation[of "(*\<^sub>R) c ` S" a]
unfolding *
by auto
qed
@@ -2637,7 +2637,7 @@
assumes "compact s"
shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof -
- have "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
+ have "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
by auto
then show ?thesis
using compact_translation[OF compact_scaling[OF assms], of a c] by auto
@@ -3719,7 +3719,7 @@
assumes "c \<noteq> 0"
shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof -
- have *: "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
+ have *: "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
show ?thesis
using homeomorphic_trans
using homeomorphic_scaling[OF assms, of s]
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Sep 24 23:49:43 2018 +0200
@@ -664,7 +664,7 @@
assumes "convex S"
shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)"
proof -
- have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` ( *\<^sub>R) c ` S"
+ have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S"
by auto
then show ?thesis
using convex_translation[OF convex_scaling[OF assms], of a c] by auto
@@ -1229,12 +1229,12 @@
lemma closure_scaleR:
fixes S :: "'a::real_normed_vector set"
- shows "(( *\<^sub>R) c) ` (closure S) = closure ((( *\<^sub>R) c) ` S)"
+ shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
proof
- show "(( *\<^sub>R) c) ` (closure S) \<subseteq> closure ((( *\<^sub>R) c) ` S)"
+ show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
using bounded_linear_scaleR_right
by (rule closure_bounded_linear_image_subset)
- show "closure ((( *\<^sub>R) c) ` S) \<subseteq> (( *\<^sub>R) c) ` (closure S)"
+ show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
qed
@@ -1945,7 +1945,7 @@
lemma cone_iff:
assumes "S \<noteq> {}"
- shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
+ shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
proof -
{
assume "cone S"
@@ -1955,7 +1955,7 @@
{
fix x
assume "x \<in> S"
- then have "x \<in> (( *\<^sub>R) c) ` S"
+ then have "x \<in> ((*\<^sub>R) c) ` S"
unfolding image_def
using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"]
exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
@@ -1964,19 +1964,19 @@
moreover
{
fix x
- assume "x \<in> (( *\<^sub>R) c) ` S"
+ assume "x \<in> ((*\<^sub>R) c) ` S"
then have "x \<in> S"
using \<open>cone S\<close> \<open>c > 0\<close>
unfolding cone_def image_def \<open>c > 0\<close> by auto
}
- ultimately have "(( *\<^sub>R) c) ` S = S" by auto
+ ultimately have "((*\<^sub>R) c) ` S = S" by auto
}
- then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
+ then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
using \<open>cone S\<close> cone_contains_0[of S] assms by auto
}
moreover
{
- assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
+ assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
{
fix x
assume "x \<in> S"
@@ -2061,9 +2061,9 @@
then show ?thesis by auto
next
case False
- then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
+ then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
using cone_iff[of S] assms by auto
- then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` closure S = closure S)"
+ then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
using closure_subset by (auto simp: closure_scaleR)
then show ?thesis
using False cone_iff[of "closure S"] by auto
@@ -5705,19 +5705,19 @@
then show ?thesis by auto
next
case False
- then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
+ then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
using cone_iff[of S] assms by auto
{
fix c :: real
assume "c > 0"
- then have "( *\<^sub>R) c ` (convex hull S) = convex hull (( *\<^sub>R) c ` S)"
+ then have "(*\<^sub>R) c ` (convex hull S) = convex hull ((*\<^sub>R) c ` S)"
using convex_hull_scaling[of _ S] by auto
also have "\<dots> = convex hull S"
using * \<open>c > 0\<close> by auto
- finally have "( *\<^sub>R) c ` (convex hull S) = convex hull S"
+ finally have "(*\<^sub>R) c ` (convex hull S) = convex hull S"
by auto
}
- then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> (( *\<^sub>R) c ` (convex hull S)) = (convex hull S)"
+ then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> ((*\<^sub>R) c ` (convex hull S)) = (convex hull S)"
using * hull_subset[of S convex] by auto
then show ?thesis
using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto
@@ -6403,7 +6403,7 @@
assume "y \<in> cbox (x - ?d) (x + ?d)"
then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
using assms by (simp add: mem_box field_simps inner_simps)
- with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
+ with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum ((*\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
next
fix y
--- a/src/HOL/Analysis/Derivative.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy Mon Sep 24 23:49:43 2018 +0200
@@ -52,7 +52,7 @@
lemma has_derivative_right:
fixes f :: "real \<Rightarrow> real"
and y :: "real"
- shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
+ shows "(f has_derivative ((*) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
proof -
have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
@@ -983,7 +983,7 @@
assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
shows "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
proof (rule has_derivative_zero_constant)
- have A: "( * ) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
+ have A: "(*) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
using assms(2)[of x] by (simp add: has_field_derivative_def A)
qed fact
@@ -1911,9 +1911,9 @@
then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
"\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
- from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
+ from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
by (simp add: has_field_derivative_def S)
- have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
+ have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
@@ -2218,7 +2218,7 @@
unfolding field_differentiable_def
by (metis DERIV_subset top_greatest)
-lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F"
+lemma field_differentiable_linear [simp,derivative_intros]: "((*) c) field_differentiable F"
unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
by (force intro: has_derivative_mult_right)
--- a/src/HOL/Analysis/Determinants.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy Mon Sep 24 23:49:43 2018 +0200
@@ -452,7 +452,7 @@
lemma%unimportant matrix_id [simp]: "det (matrix id) = 1"
by (simp add: matrix_id_mat_1)
-lemma%important det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
+lemma%important det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
apply (subst det_diagonal)
apply (auto simp: matrix_def mat_def)
apply (simp add: cart_eq_inner_axis inner_axis_axis)
@@ -750,7 +750,7 @@
lemma%unimportant det_nz_iff_inj_gen:
fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n"
- assumes "Vector_Spaces.linear ( *s) ( *s) f"
+ assumes "Vector_Spaces.linear (*s) (*s) f"
shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
proof
assume "det (matrix f) \<noteq> 0"
@@ -780,22 +780,22 @@
lemma%important matrix_left_invertible_gen:
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
- assumes "Vector_Spaces.linear ( *s) ( *s) f"
- shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id))"
+ assumes "Vector_Spaces.linear (*s) (*s) f"
+ shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id))"
proof%unimportant safe
fix B
assume 1: "B ** matrix f = mat 1"
- show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
+ show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id"
proof (intro exI conjI)
- show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)"
+ show "Vector_Spaces.linear (*s) (*s) (\<lambda>y. B *v y)"
by simp
- show "(( *v) B) \<circ> f = id"
+ show "((*v) B) \<circ> f = id"
unfolding o_def
by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid)
qed
next
fix g
- assume "Vector_Spaces.linear ( *s) ( *s) g" "g \<circ> f = id"
+ assume "Vector_Spaces.linear (*s) (*s) g" "g \<circ> f = id"
then have "matrix g ** matrix f = mat 1"
by (metis assms matrix_compose_gen matrix_id_mat_1)
then show "\<exists>B. B ** matrix f = mat 1" ..
@@ -808,22 +808,22 @@
lemma%unimportant matrix_right_invertible_gen:
fixes f :: "'a::field^'m \<Rightarrow> 'a^'n"
- assumes "Vector_Spaces.linear ( *s) ( *s) f"
- shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id))"
+ assumes "Vector_Spaces.linear (*s) (*s) f"
+ shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id))"
proof safe
fix B
assume 1: "matrix f ** B = mat 1"
- show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id"
+ show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id"
proof (intro exI conjI)
- show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)"
+ show "Vector_Spaces.linear (*s) (*s) ((*v) B)"
by simp
- show "f \<circ> ( *v) B = id"
+ show "f \<circ> (*v) B = id"
using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
by (metis (no_types, hide_lams))
qed
next
fix g
- assume "Vector_Spaces.linear ( *s) ( *s) g" and "f \<circ> g = id"
+ assume "Vector_Spaces.linear (*s) (*s) g" and "f \<circ> g = id"
then have "matrix f ** matrix g = mat 1"
by (metis assms matrix_compose_gen matrix_id_mat_1)
then show "\<exists>B. matrix f ** B = mat 1" ..
@@ -836,8 +836,8 @@
lemma%unimportant matrix_invertible_gen:
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
- assumes "Vector_Spaces.linear ( *s) ( *s) f"
- shows "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
+ assumes "Vector_Spaces.linear (*s) (*s) f"
+ shows "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
(is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
@@ -855,7 +855,7 @@
lemma%unimportant invertible_eq_bij:
fixes m :: "'a::field^'m^'n"
- shows "invertible m \<longleftrightarrow> bij (( *v) m)"
+ shows "invertible m \<longleftrightarrow> bij ((*v) m)"
using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul]
by (metis bij_betw_def left_right_inverse_eq matrix_vector_mul_linear_gen o_bij
vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
@@ -1028,7 +1028,7 @@
let ?m1 = "mat 1 :: real ^'n^'n"
{
assume ot: ?ot
- from ot have lf: "Vector_Spaces.linear ( *s) ( *s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
+ from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR
by blast+
{
@@ -1052,7 +1052,7 @@
}
moreover
{
- assume lf: "Vector_Spaces.linear ( *s) ( *s) f" and om: "orthogonal_matrix ?mf"
+ assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
from lf om have ?lhs
unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
--- a/src/HOL/Analysis/Euclidean_Space.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy Mon Sep 24 23:49:43 2018 +0200
@@ -307,7 +307,7 @@
subsection \<open>Locale instances\<close>
lemma finite_dimensional_vector_space_euclidean:
- "finite_dimensional_vector_space ( *\<^sub>R) Basis"
+ "finite_dimensional_vector_space (*\<^sub>R) Basis"
proof unfold_locales
show "finite (Basis::'a set)" by (metis finite_Basis)
show "real_vector.independent (Basis::'a set)"
@@ -318,20 +318,20 @@
apply (drule_tac f="inner a" in arg_cong)
apply (simp add: inner_Basis inner_sum_right eq_commute)
done
- show "module.span ( *\<^sub>R) Basis = UNIV"
+ show "module.span (*\<^sub>R) Basis = UNIV"
unfolding span_finite [OF finite_Basis] span_raw_def[symmetric]
by (auto intro!: euclidean_representation[symmetric])
qed
interpretation eucl?: finite_dimensional_vector_space "scaleR :: real => 'a => 'a::euclidean_space" "Basis"
- rewrites "module.dependent ( *\<^sub>R) = dependent"
- and "module.representation ( *\<^sub>R) = representation"
- and "module.subspace ( *\<^sub>R) = subspace"
- and "module.span ( *\<^sub>R) = span"
- and "vector_space.extend_basis ( *\<^sub>R) = extend_basis"
- and "vector_space.dim ( *\<^sub>R) = dim"
- and "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
- and "Vector_Spaces.linear ( * ) ( *\<^sub>R) = linear"
+ rewrites "module.dependent (*\<^sub>R) = dependent"
+ and "module.representation (*\<^sub>R) = representation"
+ and "module.subspace (*\<^sub>R) = subspace"
+ and "module.span (*\<^sub>R) = span"
+ and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
+ and "vector_space.dim (*\<^sub>R) = dim"
+ and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
+ and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
and "finite_dimensional_vector_space.dimension Basis = DIM('a)"
and "dimension = DIM('a)"
by (auto simp add: dependent_raw_def representation_raw_def
@@ -348,15 +348,15 @@
interpretation eucl?: finite_dimensional_vector_space_prod scaleR scaleR Basis Basis
rewrites "Basis_pair = Basis"
- and "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
+ and "module_prod.scale (*\<^sub>R) (*\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
proof -
- show "finite_dimensional_vector_space_prod ( *\<^sub>R) ( *\<^sub>R) Basis Basis"
+ show "finite_dimensional_vector_space_prod (*\<^sub>R) (*\<^sub>R) Basis Basis"
by unfold_locales
- interpret finite_dimensional_vector_space_prod "( *\<^sub>R)" "( *\<^sub>R)" "Basis::'a set" "Basis::'b set"
+ interpret finite_dimensional_vector_space_prod "(*\<^sub>R)" "(*\<^sub>R)" "Basis::'a set" "Basis::'b set"
by fact
show "Basis_pair = Basis"
unfolding Basis_pair_def Basis_prod_def by auto
- show "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = scaleR"
+ show "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
by (fact module_prod_scale_eq_scaleR)
qed
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Mon Sep 24 23:49:43 2018 +0200
@@ -235,7 +235,7 @@
instantiation vec :: (times, finite) times
begin
-definition "( * ) \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))"
+definition "(*) \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))"
instance ..
end
@@ -961,7 +961,7 @@
lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
by (simp add: vec_eq_iff)
-lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear ( * ) vector_scalar_mult vec"
+lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear (*) vector_scalar_mult vec"
by unfold_locales (vector algebra_simps)+
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
@@ -1161,7 +1161,7 @@
lemma%unimportant matrix_id_mat_1: "matrix id = mat 1"
by (simp add: mat_def matrix_def axis_def)
-lemma%unimportant matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
+lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
@@ -1218,7 +1218,7 @@
lemma%unimportant inj_matrix_vector_mult:
fixes A::"'a::field^'n^'m"
assumes "invertible A"
- shows "inj (( *v) A)"
+ shows "inj ((*v) A)"
by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
lemma%important scalar_invertible:
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Mon Sep 24 23:49:43 2018 +0200
@@ -929,7 +929,7 @@
using E by (subst insert) (auto intro!: prod.cong)
also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
- using insert by (auto simp: mult.commute intro!: arg_cong2[where f="( * )"] prod.cong)
+ using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
using insert(1,2) J E by (intro prod.mono_neutral_right) auto
finally show "?\<mu> ?p = \<dots>" .
--- a/src/HOL/Analysis/Further_Topology.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Mon Sep 24 23:49:43 2018 +0200
@@ -3549,12 +3549,12 @@
by (intro conjI contg continuous_intros)
show "(complex_of_real \<circ> g) ` S \<subseteq> \<real>"
by auto
- show "continuous_on \<real> (exp \<circ> ( * )\<i>)"
+ show "continuous_on \<real> (exp \<circ> (*)\<i>)"
by (intro continuous_intros)
- show "(exp \<circ> ( * )\<i>) ` \<real> \<subseteq> sphere 0 1"
+ show "(exp \<circ> (*)\<i>) ` \<real> \<subseteq> sphere 0 1"
by (auto simp: complex_is_Real_iff)
qed (auto simp: convex_Reals convex_imp_contractible)
- moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> ( * )\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
+ moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> (*)\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
by (simp add: g)
ultimately show ?lhs
apply (rule_tac x=a in exI)
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Mon Sep 24 23:49:43 2018 +0200
@@ -2049,7 +2049,7 @@
moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
- using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "( * )2" "2*z"]
+ using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "(*)2" "2*z"]
by (intro tendsto_intros Gamma_series'_LIMSEQ)
(simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
@@ -3131,10 +3131,10 @@
case True
have "(\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \<partial>lborel) =
(\<integral>\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1))
- \<partial>distr lborel borel (( * ) (1 / u)))" (is "_ = nn_integral _ ?f")
+ \<partial>distr lborel borel ((*) (1 / u)))" (is "_ = nn_integral _ ?f")
using True
by (subst nn_integral_distr) (auto simp: indicator_def field_simps intro!: nn_integral_cong)
- also have "distr lborel borel (( * ) (1 / u)) = density lborel (\<lambda>_. u)"
+ also have "distr lborel borel ((*) (1 / u)) = density lborel (\<lambda>_. u)"
using \<open>u > 0\<close> by (subst lborel_distr_mult) auto
also have "nn_integral \<dots> ?f = (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) *
(u * (1 - x)) powr (b - 1))) \<partial>lborel)" using \<open>u > 0\<close>
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Mon Sep 24 23:49:43 2018 +0200
@@ -225,7 +225,7 @@
by (intro summable_Leibniz(1) decseq_imp_monoseq decseq_SucI) simp_all
hence A: "(\<lambda>n. \<Sum>k<n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
by (simp add: summable_sums_iff divide_inverse sums_def)
- from filterlim_compose[OF this filterlim_subseq[of "( * ) (2::nat)"]]
+ from filterlim_compose[OF this filterlim_subseq[of "(*) (2::nat)"]]
have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
by (simp add: strict_mono_def)
ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Sep 24 23:49:43 2018 +0200
@@ -5044,8 +5044,8 @@
using real_arch_simple by blast
have "ball 0 B \<subseteq> ?cube n" if n: "n \<ge> N" for n
proof -
- have "sum (( *\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
- x \<bullet> i \<le> sum (( *\<^sub>R) (real n)) Basis \<bullet> i"
+ have "sum ((*\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
+ x \<bullet> i \<le> sum ((*\<^sub>R) (real n)) Basis \<bullet> i"
if "norm x < B" "i \<in> Basis" for x i::'n
using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf)
then show ?thesis
@@ -5080,7 +5080,7 @@
fix x :: 'n
assume x: "x \<in> ball 0 B"
have "\<lbrakk>norm (0 - x) < B; i \<in> Basis\<rbrakk>
- \<Longrightarrow> sum (( *\<^sub>R) (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum (( *\<^sub>R) n) Basis \<bullet> i" for i
+ \<Longrightarrow> sum ((*\<^sub>R) (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum ((*\<^sub>R) n) Basis \<bullet> i" for i
using Basis_le_norm[of i x] n by (auto simp add: field_simps sum_negf)
then show "x \<in> ?cube n"
using x by (auto simp: mem_box dist_norm)
@@ -6180,7 +6180,7 @@
and bou: "bounded (range(\<lambda>k. integral S (f k)))"
shows "g integrable_on S \<and> (\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
proof -
- have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = ( *\<^sub>R) (- 1) ` (range(\<lambda>k. integral S (f k)))"
+ have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = (*\<^sub>R) (- 1) ` (range(\<lambda>k. integral S (f k)))"
by force
have "(\<lambda>x. - g x) integrable_on S \<and> (\<lambda>k. integral S (\<lambda>x. - f k x)) \<longlonglongrightarrow> integral S (\<lambda>x. - g x)"
proof (rule monotone_convergence_increasing)
--- a/src/HOL/Analysis/Homeomorphism.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Mon Sep 24 23:49:43 2018 +0200
@@ -835,9 +835,9 @@
have "((sphere a r \<inter> T) - {b}) homeomorphic
(+) (-a) ` ((sphere a r \<inter> T) - {b})"
by (rule homeomorphic_translation)
- also have "... homeomorphic ( *\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
+ also have "... homeomorphic (*\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
- also have "... = sphere 0 1 \<inter> (( *\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
+ also have "... = sphere 0 1 \<inter> ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
also have "... homeomorphic p"
apply (rule homeomorphic_punctured_affine_sphere_affine_01)
@@ -2210,26 +2210,26 @@
and pq'_eq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p (q' t) = (f \<circ> g +++ reversepath g') t"
using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] \<open>path q\<close> piq refl refl]
by auto
- have "q' t = (h \<circ> ( *\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
- proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> ( *\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> ( *\<^sub>R) 2" t])
- show "q' 0 = (h \<circ> ( *\<^sub>R) 2) 0"
+ have "q' t = (h \<circ> (*\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
+ proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> (*\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> (*\<^sub>R) 2" t])
+ show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
by (metis \<open>pathstart q' = pathstart q\<close> comp_def g h pastq pathstart_def pth_4(2))
- show "continuous_on {0..1/2} (f \<circ> g \<circ> ( *\<^sub>R) 2)"
+ show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
using g(2) path_image_def by fastforce+
- show "(f \<circ> g \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
+ show "(f \<circ> g \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
using g(2) path_image_def fim by fastforce
- show "(h \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
+ show "(h \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
using h path_image_def by fastforce
show "q' ` {0..1/2} \<subseteq> C"
using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
- show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p (q' x)"
+ show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p (q' x)"
by (auto simp: joinpaths_def pq'_eq)
- show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p ((h \<circ> ( *\<^sub>R) 2) x)"
+ show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p ((h \<circ> (*\<^sub>R) 2) x)"
by (simp add: phg)
show "continuous_on {0..1/2} q'"
by (simp add: continuous_on_path \<open>path q'\<close>)
- show "continuous_on {0..1/2} (h \<circ> ( *\<^sub>R) 2)"
+ show "continuous_on {0..1/2} (h \<circ> (*\<^sub>R) 2)"
apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path h\<close>], force)
done
qed (use that in auto)
--- a/src/HOL/Analysis/Inner_Product.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy Mon Sep 24 23:49:43 2018 +0200
@@ -277,7 +277,7 @@
instantiation real :: real_inner
begin
-definition inner_real_def [simp]: "inner = ( * )"
+definition inner_real_def [simp]: "inner = (*)"
instance
proof
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 24 23:49:43 2018 +0200
@@ -767,10 +767,10 @@
finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
qed
-lemma lebesgue_measurable_scaling[measurable]: "( *\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+lemma lebesgue_measurable_scaling[measurable]: "(*\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
proof cases
assume "x = 0"
- then have "( *\<^sub>R) x = (\<lambda>x. 0::'a)"
+ then have "(*\<^sub>R) x = (\<lambda>x. 0::'a)"
by (auto simp: fun_eq_iff)
then show ?thesis by auto
next
@@ -860,9 +860,9 @@
lemma lborel_distr_mult:
assumes "(c::real) \<noteq> 0"
- shows "distr lborel borel (( * ) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+ shows "distr lborel borel ((*) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
proof-
- have "distr lborel borel (( * ) c) = distr lborel lborel (( * ) c)" by (simp cong: distr_cong)
+ have "distr lborel borel ((*) c) = distr lborel lborel ((*) c)" by (simp cong: distr_cong)
also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
finally show ?thesis .
@@ -870,13 +870,13 @@
lemma lborel_distr_mult':
assumes "(c::real) \<noteq> 0"
- shows "lborel = density (distr lborel borel (( * ) c)) (\<lambda>_. \<bar>c\<bar>)"
+ shows "lborel = density (distr lborel borel ((*) c)) (\<lambda>_. \<bar>c\<bar>)"
proof-
have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp
also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)"
by (subst density_density_eq) (auto simp: ennreal_mult)
- also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (( * ) c)"
+ also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel ((*) c)"
by (rule lborel_distr_mult[symmetric])
finally show ?thesis .
qed
@@ -1119,7 +1119,7 @@
let ?f = "\<lambda>n. root DIM('a) (Suc n)"
- have vimage_eq_image: "( *\<^sub>R) (?f n) -` S = ( *\<^sub>R) (1 / ?f n) ` S" for n
+ have vimage_eq_image: "(*\<^sub>R) (?f n) -` S = (*\<^sub>R) (1 / ?f n) ` S" for n
apply safe
subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
subgoal by auto
@@ -1141,20 +1141,20 @@
by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide)
then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)"
unfolding ennreal_suminf_multc eq by simp
- also have "\<dots> = (\<Sum>n. emeasure lebesgue (( *\<^sub>R) (?f n) -` S))"
+ also have "\<dots> = (\<Sum>n. emeasure lebesgue ((*\<^sub>R) (?f n) -` S))"
unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp
- also have "\<dots> = emeasure lebesgue (\<Union>n. ( *\<^sub>R) (?f n) -` S)"
+ also have "\<dots> = emeasure lebesgue (\<Union>n. (*\<^sub>R) (?f n) -` S)"
proof (intro suminf_emeasure)
- show "disjoint_family (\<lambda>n. ( *\<^sub>R) (?f n) -` S)"
+ show "disjoint_family (\<lambda>n. (*\<^sub>R) (?f n) -` S)"
unfolding disjoint_family_on_def
proof safe
fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S"
with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}"
by auto
qed
- have "( *\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
+ have "(*\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto
- then show "range (\<lambda>i. ( *\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
+ then show "range (\<lambda>i. (*\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
by auto
qed
also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Sep 24 23:49:43 2018 +0200
@@ -279,7 +279,7 @@
lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="(+)"]
and simple_function_diff[intro, simp] = simple_function_compose2[where h="(-)"]
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
- and simple_function_mult[intro, simp] = simple_function_compose2[where h="( * )"]
+ and simple_function_mult[intro, simp] = simple_function_compose2[where h="(*)"]
and simple_function_div[intro, simp] = simple_function_compose2[where h="(/)"]
and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
@@ -760,7 +760,7 @@
using assms by (intro simple_function_partition) auto
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ennreal))`space M.
if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"
- by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="( * )"] arg_cong2[where f=emeasure] sum.cong)
+ by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="(*)"] arg_cong2[where f=emeasure] sum.cong)
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ennreal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))"
using assms by (subst sum.If_cases) (auto intro!: simple_functionD(1) simp: eq)
also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ennreal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"
--- a/src/HOL/Analysis/Path_Connected.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1737,7 +1737,7 @@
show ?thesis
unfolding path_component_def
proof (intro exI conjI)
- have "continuous_on {0..1} (p \<circ> (( *) y))"
+ have "continuous_on {0..1} (p \<circ> ((*) y))"
apply (rule continuous_intros)+
using p [unfolded path_def] y
apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
--- a/src/HOL/Analysis/Product_Vector.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Product_Vector.thy Mon Sep 24 23:49:43 2018 +0200
@@ -88,21 +88,21 @@
end
-lemma module_prod_scale_eq_scaleR: "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = scaleR"
+lemma module_prod_scale_eq_scaleR: "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
apply (rule ext) apply (rule ext)
apply (subst module_prod.scale_def)
subgoal by unfold_locales
by (simp add: scaleR_prod_def)
interpretation real_vector?: vector_space_prod "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
- rewrites "scale = (( *\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
- and "module.dependent ( *\<^sub>R) = dependent"
- and "module.representation ( *\<^sub>R) = representation"
- and "module.subspace ( *\<^sub>R) = subspace"
- and "module.span ( *\<^sub>R) = span"
- and "vector_space.extend_basis ( *\<^sub>R) = extend_basis"
- and "vector_space.dim ( *\<^sub>R) = dim"
- and "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
+ rewrites "scale = ((*\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
+ and "module.dependent (*\<^sub>R) = dependent"
+ and "module.representation (*\<^sub>R) = representation"
+ and "module.subspace (*\<^sub>R) = subspace"
+ and "module.span (*\<^sub>R) = span"
+ and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
+ and "vector_space.dim (*\<^sub>R) = dim"
+ and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
subgoal by unfold_locales
subgoal by (fact module_prod_scale_eq_scaleR)
unfolding dependent_raw_def representation_raw_def subspace_raw_def span_raw_def
@@ -539,11 +539,11 @@
proof -
interpret p1: Vector_Spaces.linear s1 scale "(\<lambda>x. (x, 0))"
by unfold_locales (auto simp: scale_def)
- interpret pair1: finite_dimensional_vector_space_pair "( *a)" B1 scale Basis_pair
+ interpret pair1: finite_dimensional_vector_space_pair "(*a)" B1 scale Basis_pair
by unfold_locales
interpret p2: Vector_Spaces.linear s2 scale "(\<lambda>x. (0, x))"
by unfold_locales (auto simp: scale_def)
- interpret pair2: finite_dimensional_vector_space_pair "( *b)" B2 scale Basis_pair
+ interpret pair2: finite_dimensional_vector_space_pair "(*b)" B2 scale Basis_pair
by unfold_locales
have ss: "p.subspace ((\<lambda>x. (x, 0)) ` S)" "p.subspace (Pair 0 ` T)"
by (rule p1.subspace_image p2.subspace_image assms)+
--- a/src/HOL/Analysis/Riemann_Mapping.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Mon Sep 24 23:49:43 2018 +0200
@@ -138,17 +138,17 @@
proof (intro bdd_aboveI exI ballI, clarify)
show "norm (deriv f 0) \<le> 1 / r" if "f \<in> F" for f
proof -
- have r01: "( * ) (complex_of_real r) ` ball 0 1 \<subseteq> S"
+ have r01: "(*) (complex_of_real r) ` ball 0 1 \<subseteq> S"
using that \<open>r > 0\<close> by (auto simp: norm_mult r [THEN subsetD])
- then have "f holomorphic_on ( * ) (complex_of_real r) ` ball 0 1"
+ then have "f holomorphic_on (*) (complex_of_real r) ` ball 0 1"
using holomorphic_on_subset [OF holF] by (simp add: that)
then have holf: "f \<circ> (\<lambda>z. (r * z)) holomorphic_on (ball 0 1)"
by (intro holomorphic_intros holomorphic_on_compose)
- have f0: "(f \<circ> ( * ) (complex_of_real r)) 0 = 0"
+ have f0: "(f \<circ> (*) (complex_of_real r)) 0 = 0"
using F_def that by auto
have "f ` S \<subseteq> ball 0 1"
using F_def that by blast
- with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> ( * )(of_real r))z) < 1"
+ with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> (*)(of_real r))z) < 1"
by force
have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
if "z \<in> ball 0 1" for z::complex
@@ -162,7 +162,7 @@
using * [of 0] by simp
have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
using DERIV_imp_deriv df0 by blast
- have "norm (deriv (f \<circ> ( * ) (complex_of_real r)) 0) \<le> 1"
+ have "norm (deriv (f \<circ> (*) (complex_of_real r)) 0) \<le> 1"
by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
with \<open>r > 0\<close> show ?thesis
by (simp add: deq norm_mult divide_simps o_def)
--- a/src/HOL/Analysis/Starlike.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy Mon Sep 24 23:49:43 2018 +0200
@@ -2902,22 +2902,22 @@
lemma rel_interior_scaleR:
fixes S :: "'n::euclidean_space set"
assumes "c \<noteq> 0"
- shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
- using rel_interior_injective_linear_image[of "(( *\<^sub>R) c)" S]
- linear_conv_bounded_linear[of "( *\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
+ shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
+ using rel_interior_injective_linear_image[of "((*\<^sub>R) c)" S]
+ linear_conv_bounded_linear[of "(*\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
by auto
lemma rel_interior_convex_scaleR:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
- shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
+ shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
by (metis assms linear_scaleR rel_interior_convex_linear_image)
lemma convex_rel_open_scaleR:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
and "rel_open S"
- shows "convex ((( *\<^sub>R) c) ` S) \<and> rel_open ((( *\<^sub>R) c) ` S)"
+ shows "convex (((*\<^sub>R) c) ` S) \<and> rel_open (((*\<^sub>R) c) ` S)"
by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
lemma convex_rel_open_finite_inter:
@@ -3086,10 +3086,10 @@
by (simp add: rel_interior_empty cone_0)
next
case False
- then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
+ then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
using cone_iff[of S] assms by auto
then have *: "0 \<in> ({0} \<union> rel_interior S)"
- and "\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
+ and "\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
by (auto simp add: rel_interior_scaleR)
then show ?thesis
using cone_iff[of "{0} \<union> rel_interior S"] by auto
@@ -3099,7 +3099,7 @@
fixes S :: "'m::euclidean_space set"
assumes "convex S"
shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow>
- c > 0 \<and> x \<in> ((( *\<^sub>R) c) ` (rel_interior S))"
+ c > 0 \<and> x \<in> (((*\<^sub>R) c) ` (rel_interior S))"
proof (cases "S = {}")
case True
then show ?thesis
@@ -3132,9 +3132,9 @@
{
fix c :: real
assume "c > 0"
- then have "f c = (( *\<^sub>R) c ` S)"
+ then have "f c = ((*\<^sub>R) c ` S)"
using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
- then have "rel_interior (f c) = ( *\<^sub>R) c ` rel_interior S"
+ then have "rel_interior (f c) = (*\<^sub>R) c ` rel_interior S"
using rel_interior_convex_scaleR[of S c] assms by auto
}
then show ?thesis using * ** by auto
@@ -8025,7 +8025,7 @@
by auto
have "b \<bullet> (v - ?u) = 0" if "b \<in> B" for b
using that \<open>finite B\<close>
- by (simp add: * algebra_simps inner_sum_right if_distrib [of "( *)v" for v] inner_commute cong: if_cong)
+ by (simp add: * algebra_simps inner_sum_right if_distrib [of "(*)v" for v] inner_commute cong: if_cong)
then show "y \<bullet> (v - ?u) = 0"
by (simp add: u inner_sum_left)
qed
--- a/src/HOL/Analysis/normarith.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/normarith.ML Mon Sep 24 23:49:43 2018 +0200
@@ -26,7 +26,7 @@
fun find_normedterms t acc = case Thm.term_of t of
@{term "(+) :: real => _"}$_$_ =>
find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
- | @{term "( * ) :: real => _"}$_$_ =>
+ | @{term "(*) :: real => _"}$_$_ =>
if not (is_ratconst (Thm.dest_arg1 t)) then acc else
augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0)
(Thm.dest_arg t) acc
@@ -83,7 +83,7 @@
fun replacenegnorms cv t = case Thm.term_of t of
@{term "(+) :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
-| @{term "( * ) :: real => _"}$_$_ =>
+| @{term "(*) :: real => _"}$_$_ =>
if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
| _ => Thm.reflexive t
(*
--- a/src/HOL/Binomial.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Binomial.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1299,7 +1299,7 @@
"n choose k =
(if k > n then 0
else if 2 * k > n then n choose (n - k)
- else (fold_atLeastAtMost_nat ( * ) (n - k + 1) n 1 div fact k))"
+ else (fold_atLeastAtMost_nat (*) (n - k + 1) n 1 div fact k))"
proof -
{
assume "k \<le> n"
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Mon Sep 24 23:49:43 2018 +0200
@@ -421,7 +421,7 @@
Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
divide plus minus unit_factor normalize
- rewrites "dvd.dvd ( * ) = Rings.dvd"
+ rewrites "dvd.dvd (*) = Rings.dvd"
by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
proof (rule ext)+
@@ -575,7 +575,7 @@
"Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
"Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
divide plus minus unit_factor normalize
- rewrites "dvd.dvd ( * ) = Rings.dvd"
+ rewrites "dvd.dvd (*) = Rings.dvd"
by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
proof (rule ext)+
@@ -612,7 +612,7 @@
"Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
"Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
divide plus minus unit_factor normalize
- rewrites "dvd.dvd ( * ) = Rings.dvd"
+ rewrites "dvd.dvd (*) = Rings.dvd"
by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
proof (rule ext)+
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Sep 24 23:49:43 2018 +0200
@@ -78,7 +78,7 @@
instantiation fps :: ("{comm_monoid_add, times}") times
begin
- definition fps_times_def: "( * ) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
+ definition fps_times_def: "(*) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
instance ..
end
@@ -2037,7 +2037,7 @@
(* If f reprents {a_n} and P is a polynomial, then
P(xD) f represents {P(n) a_n}*)
-definition "fps_XD = ( * ) fps_X \<circ> fps_deriv"
+definition "fps_XD = (*) fps_X \<circ> fps_deriv"
lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)"
by (simp add: fps_XD_def field_simps)
--- a/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 24 23:49:43 2018 +0200
@@ -891,7 +891,7 @@
lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
by (induct n) (simp_all add: monom_0 monom_Suc)
-lemma smult_Poly: "smult c (Poly xs) = Poly (map (( * ) c) xs)"
+lemma smult_Poly: "smult c (Poly xs) = Poly (map ((*) c) xs)"
by (auto simp: poly_eq_iff nth_default_def)
lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)"
@@ -3811,10 +3811,10 @@
where
"pseudo_divmod_main_list lc q r d (Suc n) =
(let
- rr = map (( * ) lc) r;
+ rr = map ((*) lc) r;
a = hd r;
- qqq = cCons a (map (( * ) lc) q);
- rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (( * ) a) d))
+ qqq = cCons a (map ((*) lc) q);
+ rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d))
in pseudo_divmod_main_list lc qqq rrr d n)"
| "pseudo_divmod_main_list lc q r d 0 = (q, r)"
@@ -3822,9 +3822,9 @@
where
"pseudo_mod_main_list lc r d (Suc n) =
(let
- rr = map (( * ) lc) r;
+ rr = map ((*) lc) r;
a = hd r;
- rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (( * ) a) d))
+ rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d))
in pseudo_mod_main_list lc rrr d n)"
| "pseudo_mod_main_list lc r d 0 = r"
@@ -3836,7 +3836,7 @@
(let
a = hd r;
qqq = cCons a q;
- rr = tl (if a = 0 then r else minus_poly_rev_list r (map (( * ) a) d))
+ rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d))
in divmod_poly_one_main_list qqq rr d n)"
| "divmod_poly_one_main_list q r d 0 = (q, r)"
@@ -3845,7 +3845,7 @@
"mod_poly_one_main_list r d (Suc n) =
(let
a = hd r;
- rr = tl (if a = 0 then r else minus_poly_rev_list r (map (( * ) a) d))
+ rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d))
in mod_poly_one_main_list rr d n)"
| "mod_poly_one_main_list r d 0 = r"
@@ -3866,7 +3866,7 @@
re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q)
in rev re))"
-lemma minus_zero_does_nothing: "minus_poly_rev_list x (map (( * ) 0) y) = x"
+lemma minus_zero_does_nothing: "minus_poly_rev_list x (map ((*) 0) y) = x"
for x :: "'a::ring list"
by (induct x y rule: minus_poly_rev_list.induct) auto
@@ -3874,8 +3874,8 @@
by (induct xs ys rule: minus_poly_rev_list.induct) auto
lemma if_0_minus_poly_rev_list:
- "(if a = 0 then x else minus_poly_rev_list x (map (( * ) a) y)) =
- minus_poly_rev_list x (map (( * ) a) y)"
+ "(if a = 0 then x else minus_poly_rev_list x (map ((*) a) y)) =
+ minus_poly_rev_list x (map ((*) a) y)"
for a :: "'a::ring"
by(cases "a = 0") (simp_all add: minus_zero_does_nothing)
@@ -3917,7 +3917,7 @@
lemma head_minus_poly_rev_list:
"length d \<le> length r \<Longrightarrow> d \<noteq> [] \<Longrightarrow>
- hd (minus_poly_rev_list (map (( * ) (last d)) r) (map (( * ) (hd r)) (rev d))) = 0"
+ hd (minus_poly_rev_list (map ((*) (last d)) r) (map ((*) (hd r)) (rev d))) = 0"
for d r :: "'a::comm_ring list"
proof (induct r)
case Nil
@@ -3927,7 +3927,7 @@
then show ?case by (cases "rev d") (simp_all add: ac_simps)
qed
-lemma Poly_map: "Poly (map (( * ) a) p) = smult a (Poly p)"
+lemma Poly_map: "Poly (map ((*) a) p) = smult a (Poly p)"
proof (induct p)
case Nil
then show ?case by simp
@@ -3955,9 +3955,9 @@
with \<open>d \<noteq> []\<close> have "r \<noteq> []"
using Suc_leI length_greater_0_conv list.size(3) by fastforce
let ?a = "(hd (rev r))"
- let ?rr = "map (( * ) lc) (rev r)"
- let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map (( * ) ?a) (rev d))))"
- let ?qq = "cCons ?a (map (( * ) lc) q)"
+ let ?rr = "map ((*) lc) (rev r)"
+ let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map ((*) ?a) (rev d))))"
+ let ?qq = "cCons ?a (map ((*) lc) q)"
from * Suc(3) have n: "n = (1 + length r - length d - 1)"
by simp
from * have rr_val:"(length ?rrr) = (length r - 1)"
@@ -3990,12 +3990,12 @@
case 2
show ?case
proof (subst Poly_on_rev_starting_with_0, goal_cases)
- show "hd (minus_poly_rev_list (map (( * ) lc) (rev r)) (map (( * ) (hd (rev r))) (rev d))) = 0"
+ show "hd (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))) = 0"
by (fold lc, subst head_minus_poly_rev_list, insert * \<open>d \<noteq> []\<close>, auto)
from * have "length d \<le> length r"
by simp
then show "smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d =
- Poly (rev (minus_poly_rev_list (map (( * ) lc) (rev r)) (map (( * ) (hd (rev r))) (rev d))))"
+ Poly (rev (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))))"
by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
minus_poly_rev_list)
qed
@@ -4100,9 +4100,9 @@
let
cf = coeffs f;
ilc = inverse (last cg);
- ch = map (( * ) ilc) cg;
+ ch = map ((*) ilc) cg;
(q, r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
- in (poly_of_list (map (( * ) ilc) q), poly_of_list (rev r)))"
+ in (poly_of_list (map ((*) ilc) q), poly_of_list (rev r)))"
proof -
note d = pdivmod_via_pseudo_divmod pseudo_divmod_impl pseudo_divmod_list_def
show ?thesis
@@ -4121,10 +4121,10 @@
have id2: "hd (rev (coeffs (smult ilc g))) = 1"
by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def)
have id3: "length (coeffs (smult ilc g)) = length (coeffs g)"
- "rev (coeffs (smult ilc g)) = rev (map (( * ) ilc) (coeffs g))"
+ "rev (coeffs (smult ilc g)) = rev (map ((*) ilc) (coeffs g))"
unfolding coeffs_smult using ilc by auto
obtain q r where pair:
- "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (( * ) ilc) (coeffs g)))
+ "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map ((*) ilc) (coeffs g)))
(1 + length (coeffs f) - length (coeffs g)) = (q, r)"
by force
show ?thesis
@@ -4137,7 +4137,7 @@
lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list"
proof (intro ext, goal_cases)
case (1 q r d n)
- have *: "map (( * ) 1) xs = xs" for xs :: "'a list"
+ have *: "map ((*) 1) xs = xs" for xs :: "'a list"
by (induct xs) auto
show ?case
by (induct n arbitrary: q r d) (auto simp: * Let_def)
@@ -4151,7 +4151,7 @@
in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let
a = cr div lc;
qq = cCons a q;
- rr = minus_poly_rev_list r (map (( * ) a) d)
+ rr = minus_poly_rev_list r (map ((*) a) d)
in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
| "divide_poly_main_list lc q r d 0 = q"
@@ -4161,7 +4161,7 @@
cr = hd r;
a = cr div lc;
qq = cCons a q;
- rr = minus_poly_rev_list r (map (( * ) a) d)
+ rr = minus_poly_rev_list r (map ((*) a) d)
in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
by (simp add: Let_def minus_zero_does_nothing)
@@ -4190,7 +4190,7 @@
let
cf = coeffs f;
ilc = inverse (last cg);
- ch = map (( * ) ilc) cg;
+ ch = map ((*) ilc) cg;
r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
in poly_of_list (rev r))"
(is "_ = ?rhs")
@@ -4209,9 +4209,9 @@
let
cf = coeffs f;
ilc = inverse (last cg);
- ch = map (( * ) ilc) cg;
+ ch = map ((*) ilc) cg;
q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
- in poly_of_list ((map (( * ) ilc) q)))"
+ in poly_of_list ((map ((*) ilc) q)))"
text \<open>We do not declare the following lemma as code equation, since then polynomial division
on non-fields will no longer be executable. However, a code-unfold is possible, since
@@ -4259,7 +4259,7 @@
with r d have id:
"?thesis \<longleftrightarrow>
Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
- (rev (rev (minus_poly_rev_list (rev rr) (rev (map (( * ) (lcr div lc)) dd))))) (rev d) n) =
+ (rev (rev (minus_poly_rev_list (rev rr) (rev (map ((*) (lcr div lc)) dd))))) (rev d) n) =
divide_poly_main lc
(monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
(Poly r - monom (lcr div lc) n * Poly d)
--- a/src/HOL/Decision_Procs/Algebra_Aux.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Algebra_Aux.thy Mon Sep 24 23:49:43 2018 +0200
@@ -234,7 +234,7 @@
by (induct n) (simp_all add: m_ac)
definition cring_class_ops :: "'a::comm_ring_1 ring"
- where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
+ where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
lemma cring_class: "cring cring_class_ops"
apply unfold_locales
--- a/src/HOL/Decision_Procs/Cooper.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Sep 24 23:49:43 2018 +0200
@@ -2402,7 +2402,7 @@
@{code Add} (num_of_term vs t1, num_of_term vs t2)
| num_of_term vs (@{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
@{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (@{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+ | num_of_term vs (@{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
(case try HOLogic.dest_number t1 of
SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
| NONE =>
@@ -2455,7 +2455,7 @@
term_of_num vs t1 $ term_of_num vs t2
| term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} $
term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} $
+ | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} $
term_of_num vs (@{code C} i) $ term_of_num vs t2
| term_of_num vs (@{code CN} (n, i, t)) =
term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Sep 24 23:49:43 2018 +0200
@@ -2476,7 +2476,7 @@
@{code Add} (num_of_term vs t1, num_of_term vs t2)
| num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
@{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (@{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
+ | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
of @{code C} i => @{code Mul} (i, num_of_term vs t2)
| _ => error "num_of_term: unsupported multiplication")
| num_of_term vs (@{term "real_of_int :: int \<Rightarrow> real"} $ t') =
@@ -2514,7 +2514,7 @@
term_of_num vs t1 $ term_of_num vs t2
| term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $
term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $
+ | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $
term_of_num vs (@{code C} i) $ term_of_num vs t2
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
--- a/src/HOL/Decision_Procs/MIR.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Sep 24 23:49:43 2018 +0200
@@ -5579,7 +5579,7 @@
@{code Add} (num_of_term vs t1, num_of_term vs t2)
| num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
@{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (@{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
(case (num_of_term vs t1)
of @{code C} i => @{code Mul} (i, num_of_term vs t2)
| _ => error "num_of_term: unsupported Multiplication")
@@ -5638,7 +5638,7 @@
term_of_num vs t1 $ term_of_num vs t2
| term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $
term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $
+ | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $
term_of_num vs (@{code C} i) $ term_of_num vs t2
| term_of_num vs (@{code Floor} t) = @{term "of_int :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ term_of_num vs t)
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Mon Sep 24 23:49:43 2018 +0200
@@ -186,7 +186,7 @@
by (cases "x = zero") (auto simp add: distrib_left ac_simps)
qed
-lemma (in comm_semiring_0) poly_cmult_map: "poly (map (( * ) c) p) x = c * poly p x"
+lemma (in comm_semiring_0) poly_cmult_map: "poly (map ((*) c) p) x = c * poly p x"
by (induct p) (auto simp add: distrib_left ac_simps)
lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
--- a/src/HOL/Deriv.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Deriv.thy Mon Sep 24 23:49:43 2018 +0200
@@ -38,7 +38,7 @@
definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
(infix "(has'_field'_derivative)" 50)
- where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative ( * ) D) F"
+ where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative (*) D) F"
lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
by simp
@@ -153,7 +153,7 @@
lemma field_has_derivative_at:
fixes x :: "'a::real_normed_field"
- shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
+ shows "(f has_derivative (*) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
proof -
have "?lhs = (\<lambda>h. norm (f (x + h) - f x - D * h) / norm h) \<midarrow>0 \<rightarrow> 0"
by (simp add: bounded_linear_mult_right has_derivative_at)
@@ -648,7 +648,7 @@
by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult.commute)
lemma has_field_derivative_imp_has_derivative:
- "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative ( * ) D) F"
+ "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative (*) D) F"
by (simp add: has_field_derivative_def)
lemma DERIV_subset:
@@ -675,7 +675,7 @@
assume "f differentiable at x within s"
then obtain f' where *: "(f has_derivative f') (at x within s)"
unfolding differentiable_def by auto
- then obtain c where "f' = (( * ) c)"
+ then obtain c where "f' = ((*) c)"
by (metis real_bounded_linear has_derivative_bounded_linear mult.commute fun_eq_iff)
with * show "\<exists>D. (f has_real_derivative D) (at x within s)"
unfolding has_field_derivative_def by auto
@@ -702,7 +702,7 @@
lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
-lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c"
+lemma mult_commute_abs: "(\<lambda>x. x * c) = (*) c"
for c :: "'a::ab_semigroup_mult"
by (simp add: fun_eq_iff mult.commute)
@@ -711,7 +711,7 @@
assumes "DERIV f (g x) :> f'"
assumes "(g has_derivative g') (at x within s)"
shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
- using assms has_derivative_compose[of g g' x s f "( * ) f'"]
+ using assms has_derivative_compose[of g g' x s f "(*) f'"]
by (auto simp: has_field_derivative_def ac_simps)
@@ -896,7 +896,7 @@
((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
using DERIV_cmult by (auto simp add: ac_simps)
-lemma DERIV_cmult_Id [simp]: "(( * ) c has_field_derivative c) (at x within s)"
+lemma DERIV_cmult_Id [simp]: "((*) c has_field_derivative c) (at x within s)"
using DERIV_ident [THEN DERIV_cmult, where c = c and x = x] by simp
lemma DERIV_cdivide:
@@ -919,7 +919,7 @@
shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x)))
(at x within s)"
proof -
- have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative ( * ) D)"
+ have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative (*) D)"
by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff)
with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)"
by (auto dest!: has_field_derivative_imp_has_derivative)
@@ -972,7 +972,7 @@
lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow>
((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
- using has_derivative_compose[of f "( * ) D" x s g "( * ) E"]
+ using has_derivative_compose[of f "(*) D" x s g "(*) E"]
by (simp only: has_field_derivative_def mult_commute_abs ac_simps)
corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
@@ -990,7 +990,7 @@
"(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow>
(g has_field_derivative Db) (at x within s) \<Longrightarrow>
(f \<circ> g has_field_derivative Da * Db) (at x within s)"
- using has_derivative_in_compose [of g "( * ) Db" x s f "( * ) Da "]
+ using has_derivative_in_compose [of g "(*) Db" x s f "(*) Da "]
by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps)
(*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
--- a/src/HOL/Enum.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Enum.thy Mon Sep 24 23:49:43 2018 +0200
@@ -585,7 +585,7 @@
definition [simp]: "Groups.zero = a\<^sub>1"
definition [simp]: "Groups.one = a\<^sub>1"
definition [simp]: "(+) = (\<lambda>_ _. a\<^sub>1)"
-definition [simp]: "( * ) = (\<lambda>_ _. a\<^sub>1)"
+definition [simp]: "(*) = (\<lambda>_ _. a\<^sub>1)"
definition [simp]: "(mod) = (\<lambda>_ _. a\<^sub>1)"
definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
@@ -690,7 +690,7 @@
definition "(-) = ((+) :: finite_2 \<Rightarrow> _)"
definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "inverse = (\<lambda>x :: finite_2. x)"
-definition "divide = (( * ) :: finite_2 \<Rightarrow> _)"
+definition "divide = ((*) :: finite_2 \<Rightarrow> _)"
definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "abs = (\<lambda>x :: finite_2. x)"
definition "sgn = (\<lambda>x :: finite_2. x)"
--- a/src/HOL/Factorial.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Factorial.thy Mon Sep 24 23:49:43 2018 +0200
@@ -403,13 +403,13 @@
subsection \<open>Misc\<close>
lemma fact_code [code]:
- "fact n = (of_nat (fold_atLeastAtMost_nat (( * )) 2 n 1) :: 'a::semiring_char_0)"
+ "fact n = (of_nat (fold_atLeastAtMost_nat ((*)) 2 n 1) :: 'a::semiring_char_0)"
proof -
have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
by (simp add: fact_prod)
also have "\<Prod>{1..n} = \<Prod>{2..n}"
by (intro prod.mono_neutral_right) auto
- also have "\<dots> = fold_atLeastAtMost_nat (( * )) 2 n 1"
+ also have "\<dots> = fold_atLeastAtMost_nat ((*)) 2 n 1"
by (simp add: prod_atLeastAtMost_code)
finally show ?thesis .
qed
--- a/src/HOL/GCD.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/GCD.thy Mon Sep 24 23:49:43 2018 +0200
@@ -976,25 +976,25 @@
lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
by (blast dest: dvd_GcdD intro: Gcd_greatest)
-lemma Gcd_mult: "Gcd (( *) c ` A) = normalize c * Gcd A"
+lemma Gcd_mult: "Gcd ((*) c ` A) = normalize c * Gcd A"
proof (cases "c = 0")
case True
then show ?thesis by auto
next
case [simp]: False
- have "Gcd (( *) c ` A) div c dvd Gcd A"
+ have "Gcd ((*) c ` A) div c dvd Gcd A"
by (intro Gcd_greatest, subst div_dvd_iff_mult)
(auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
- then have "Gcd (( *) c ` A) dvd c * Gcd A"
+ then have "Gcd ((*) c ` A) dvd c * Gcd A"
by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
- also have "Gcd (( *) c ` A) dvd \<dots> \<longleftrightarrow> Gcd (( *) c ` A) dvd normalize c * Gcd A"
+ also have "Gcd ((*) c ` A) dvd \<dots> \<longleftrightarrow> Gcd ((*) c ` A) dvd normalize c * Gcd A"
by (simp add: dvd_mult_unit_iff)
- finally have "Gcd (( *) c ` A) dvd normalize c * Gcd A" .
- moreover have "normalize c * Gcd A dvd Gcd (( *) c ` A)"
+ finally have "Gcd ((*) c ` A) dvd normalize c * Gcd A" .
+ moreover have "normalize c * Gcd A dvd Gcd ((*) c ` A)"
by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
- ultimately have "normalize (Gcd (( *) c ` A)) = normalize (normalize c * Gcd A)"
+ ultimately have "normalize (Gcd ((*) c ` A)) = normalize (normalize c * Gcd A)"
by (rule associatedI)
then show ?thesis
by (simp add: normalize_mult)
@@ -1015,10 +1015,10 @@
lemma Lcm_mult:
assumes "A \<noteq> {}"
- shows "Lcm (( *) c ` A) = normalize c * Lcm A"
+ shows "Lcm ((*) c ` A) = normalize c * Lcm A"
proof (cases "c = 0")
case True
- with assms have "( *) c ` A = {0}"
+ with assms have "(*) c ` A = {0}"
by auto
with True show ?thesis by auto
next
@@ -1027,23 +1027,23 @@
by blast
have "c dvd c * x"
by simp
- also from x have "c * x dvd Lcm (( *) c ` A)"
+ also from x have "c * x dvd Lcm ((*) c ` A)"
by (intro dvd_Lcm) auto
- finally have dvd: "c dvd Lcm (( *) c ` A)" .
-
- have "Lcm A dvd Lcm (( *) c ` A) div c"
+ finally have dvd: "c dvd Lcm ((*) c ` A)" .
+
+ have "Lcm A dvd Lcm ((*) c ` A) div c"
by (intro Lcm_least dvd_mult_imp_div)
(auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
- then have "c * Lcm A dvd Lcm (( *) c ` A)"
+ then have "c * Lcm A dvd Lcm ((*) c ` A)"
by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
- also have "\<dots> dvd Lcm (( *) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (( *) c ` A)"
+ also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
by (simp add: mult_unit_dvd_iff)
- finally have "normalize c * Lcm A dvd Lcm (( *) c ` A)" .
- moreover have "Lcm (( *) c ` A) dvd normalize c * Lcm A"
+ finally have "normalize c * Lcm A dvd Lcm ((*) c ` A)" .
+ moreover have "Lcm ((*) c ` A) dvd normalize c * Lcm A"
by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
- ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (( *) c ` A))"
+ ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm ((*) c ` A))"
by (rule associatedI)
then show ?thesis
by (simp add: normalize_mult)
--- a/src/HOL/Groups_List.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Groups_List.thy Mon Sep 24 23:49:43 2018 +0200
@@ -124,7 +124,7 @@
by (induct xss) simp_all
lemma (in monoid_add) length_product_lists:
- "length (product_lists xss) = foldr ( * ) (map length xss) 1"
+ "length (product_lists xss) = foldr (*) (map length xss) 1"
proof (induct xss)
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
qed simp
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Mon Sep 24 23:49:43 2018 +0200
@@ -60,7 +60,7 @@
and (OCaml) "Pervasives.( +. )"
code_printing
- constant "( * ) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ constant "(*) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
(SML) "Real.* ((_), (_))"
and (OCaml) "Pervasives.( *. )"
--- a/src/HOL/Library/DAList_Multiset.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Mon Sep 24 23:49:43 2018 +0200
@@ -372,7 +372,7 @@
end
-\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>( * )\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
+\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>(*)\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((+) a) ^^ n)) 0 ms"
unfolding sum_mset.eq_fold
apply (rule comp_fun_commute.DAList_Multiset_fold)
@@ -380,8 +380,8 @@
apply (auto simp: ac_simps)
done
-\<comment> \<open>we cannot use \<open>\<lambda>a n. ( * ) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
-lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((( * ) a) ^^ n)) 1 ms"
+\<comment> \<open>we cannot use \<open>\<lambda>a n. (*) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
+lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((*) a) ^^ n)) 1 ms"
unfolding prod_mset.eq_fold
apply (rule comp_fun_commute.DAList_Multiset_fold)
apply unfold_locales
--- a/src/HOL/Library/Discrete.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Discrete.thy Mon Sep 24 23:49:43 2018 +0200
@@ -274,7 +274,7 @@
then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
- moreover have "finite (( * ) q ` {m. m * m \<le> n})"
+ moreover have "finite ((*) q ` {m. m * m \<le> n})"
by (metis (mono_tags) finite_imageI finite_less_ub le_square)
moreover have "\<exists>x. x * x \<le> n"
by (metis \<open>q * q \<le> n\<close>)
@@ -282,7 +282,7 @@
by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
qed
qed
- then have "Max (( * ) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
+ then have "Max ((*) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
apply (subst Max_le_iff)
apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
apply auto
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Sep 24 23:49:43 2018 +0200
@@ -262,7 +262,7 @@
lift_definition one_ennreal :: ennreal is 1 by simp
lift_definition zero_ennreal :: ennreal is 0 by simp
lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(+)" by simp
-lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "( * )" by simp
+lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(*)" by simp
instance
by standard (transfer; auto simp: field_simps ereal_right_distrib)+
--- a/src/HOL/Library/Float.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Float.thy Mon Sep 24 23:49:43 2018 +0200
@@ -202,7 +202,7 @@
lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(+)" by simp
declare plus_float.rep_eq[simp]
-lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "( * )" by simp
+lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(*)" by simp
declare times_float.rep_eq[simp]
lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(-)" by simp
--- a/src/HOL/Library/ListVector.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/ListVector.thy Mon Sep 24 23:49:43 2018 +0200
@@ -13,7 +13,7 @@
text\<open>Multiplication with a scalar:\<close>
abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
-where "x *\<^sub>s xs \<equiv> map (( * ) x) xs"
+where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
by (induct xs) simp_all
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Sep 24 23:49:43 2018 +0200
@@ -221,7 +221,7 @@
val neg_tm = \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
val add_tm = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
val sub_tm = \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
- val mul_tm = \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close>
+ val mul_tm = \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
val inv_tm = \<^cterm>\<open>inverse :: real \<Rightarrow> _\<close>
val div_tm = \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
val pow_tm = \<^cterm>\<open>(^) :: real \<Rightarrow> _\<close>
@@ -862,7 +862,7 @@
Free (_, \<^typ>\<open>real\<close>) =>
if not (member (op aconvc) fvs tm) then (@1, tm)
else raise Failure "substitutable_monomial"
- | \<^term>\<open>( * ) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
+ | \<^term>\<open>(*) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
not (member (op aconvc) fvs (Thm.dest_arg tm))
then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
@@ -899,7 +899,7 @@
val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
val th1 =
Drule.arg_cong_rule
- (Thm.apply \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
+ (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
(mk_meta_eq th)
val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1
in fconv_rule (arg_conv (real_poly_conv ctxt)) (isolate_variable v th2) end
@@ -943,7 +943,7 @@
\<^term>\<open>(=) :: real \<Rightarrow> _\<close>, \<^term>\<open>(<) :: real \<Rightarrow> _\<close>,
\<^term>\<open>(\<le>) :: real \<Rightarrow> _\<close>,
\<^term>\<open>(+) :: real \<Rightarrow> _\<close>, \<^term>\<open>(-) :: real \<Rightarrow> _\<close>,
- \<^term>\<open>( * ) :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
+ \<^term>\<open>(*) :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
\<^term>\<open>(/) :: real \<Rightarrow> _\<close>, \<^term>\<open>inverse :: real \<Rightarrow> _\<close>,
\<^term>\<open>(^) :: real \<Rightarrow> _\<close>, \<^term>\<open>abs :: real \<Rightarrow> _\<close>,
\<^term>\<open>min :: real \<Rightarrow> _\<close>, \<^term>\<open>max :: real \<Rightarrow> _\<close>,
--- a/src/HOL/Library/positivstellensatz.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Mon Sep 24 23:49:43 2018 +0200
@@ -328,13 +328,13 @@
let
val m' = FuncUtil.dest_monomial m
val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
- in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close> s) t) vps
+ in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> s) t) vps
end
fun cterm_of_cmonomial (m,c) =
if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
else if c = @1 then cterm_of_monomial m
- else Thm.apply (Thm.apply \<^cterm>\<open>( * )::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
+ else Thm.apply (Thm.apply \<^cterm>\<open>(*)::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
fun cterm_of_poly p =
if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\<open>0::real\<close>
@@ -680,7 +680,7 @@
in
if opr aconvc \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
then linear_add (lin_of_hol l) (lin_of_hol r)
- else if opr aconvc \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close>
+ else if opr aconvc \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
else FuncUtil.Ctermfunc.onefunc (ct, @1)
end
--- a/src/HOL/Limits.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Limits.thy Mon Sep 24 23:49:43 2018 +0200
@@ -826,7 +826,7 @@
lemma continuous_on_mult_const [simp]:
fixes c::"'a::real_normed_algebra"
- shows "continuous_on s (( *) c)"
+ shows "continuous_on s ((*) c)"
by (intro continuous_on_mult_left continuous_on_id)
lemma tendsto_divide_zero:
--- a/src/HOL/Matrix_LP/Matrix.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1487,7 +1487,7 @@
begin
definition
- times_matrix_def: "A * B = mult_matrix (( * )) (+) A B"
+ times_matrix_def: "A * B = mult_matrix ((*)) (+) A B"
instance ..
@@ -1795,7 +1795,7 @@
by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
definition scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" where
- "scalar_mult a m == apply_matrix (( * ) a) m"
+ "scalar_mult a m == apply_matrix ((*) a) m"
lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"
by (simp add: scalar_mult_def)
--- a/src/HOL/Modules.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Modules.thy Mon Sep 24 23:49:43 2018 +0200
@@ -878,9 +878,9 @@
lemma module_hom_compose_scale:
"module_hom s1 s2 (\<lambda>x. s2 (f x) (c))"
- if "module_hom s1 ( *) f"
+ if "module_hom s1 (*) f"
proof -
- interpret mh: module_hom s1 "( *)" f by fact
+ interpret mh: module_hom s1 "(*)" f by fact
show ?thesis
by unfold_locales (simp_all add: mh.add mh.scale m2.scale_left_distrib)
qed
@@ -913,7 +913,7 @@
using module_axioms module_hom_iff scale_left_commute scale_right_distrib by blast
lemma module_hom_scale_left[simp]:
- "module_hom ( *) scale (\<lambda>r. scale r x)"
+ "module_hom (*) scale (\<lambda>r. scale r x)"
by unfold_locales (auto simp: algebra_simps)
lemma module_hom_id: "module_hom scale scale id"
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy Mon Sep 24 23:49:43 2018 +0200
@@ -223,7 +223,7 @@
lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1"
by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
-lemma NSDERIV_cmult_Id [simp]: "NSDERIV (( * ) c) x :> c"
+lemma NSDERIV_cmult_Id [simp]: "NSDERIV ((*) c) x :> c"
using NSDERIV_Id [THEN NSDERIV_cmult] by simp
lemma NSDERIV_inverse:
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Mon Sep 24 23:49:43 2018 +0200
@@ -413,7 +413,7 @@
instantiation star :: (times) times
begin
- definition star_mult_def: "(( * )) \<equiv> *f2* (( * ))"
+ definition star_mult_def: "((*)) \<equiv> *f2* ((*))"
instance ..
end
--- a/src/HOL/Number_Theory/Pocklington.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Mon Sep 24 23:49:43 2018 +0200
@@ -731,7 +731,7 @@
(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
-definition "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
+definition "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
lemma primefact:
fixes n :: nat
@@ -743,8 +743,8 @@
from assms have "n = prod_mset (prime_factorization n)"
by (simp add: prod_mset_prime_factorization)
also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
- also have "\<dots> = foldr ( * ) xs 1" by (induct xs) simp_all
- finally have "foldr ( * ) xs 1 = n" ..
+ also have "\<dots> = foldr (*) xs 1" by (induct xs) simp_all
+ finally have "foldr (*) xs 1 = n" ..
moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto
ultimately have "primefact xs n" by (auto simp: primefact_def)
then show ?thesis ..
@@ -763,10 +763,10 @@
next
case (Cons q qs)
from Cons.prems[unfolded primefact_def]
- have q: "prime q" "q * foldr ( * ) qs 1 = n" "\<forall>p \<in>set qs. prime p"
- and p: "prime p" "p dvd q * foldr ( * ) qs 1"
+ have q: "prime q" "q * foldr (*) qs 1 = n" "\<forall>p \<in>set qs. prime p"
+ and p: "prime p" "p dvd q * foldr (*) qs 1"
by simp_all
- consider "p dvd q" | "p dvd foldr ( * ) qs 1"
+ consider "p dvd q" | "p dvd foldr (*) qs 1"
by (metis p prime_dvd_mult_eq_nat)
then show ?case
proof cases
@@ -776,19 +776,19 @@
then show ?thesis by simp
next
case prem: 2
- from q(3) have pqs: "primefact qs (foldr ( * ) qs 1)"
+ from q(3) have pqs: "primefact qs (foldr (*) qs 1)"
by (simp add: primefact_def)
from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp
qed
qed
-lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> list_all prime ps"
+lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> list_all prime ps"
by (auto simp add: primefact_def list_all_iff)
text \<open>Variant of Lucas theorem.\<close>
lemma lucas_primefact:
assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
- and psn: "foldr ( * ) ps 1 = n - 1"
+ and psn: "foldr (*) ps 1 = n - 1"
and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
shows "prime n"
proof -
@@ -806,7 +806,7 @@
text \<open>Variant of Pocklington theorem.\<close>
lemma pocklington_primefact:
assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
- and arnb: "(a^r) mod n = b" and psq: "foldr ( * ) ps 1 = q"
+ and arnb: "(a^r) mod n = b" and psq: "foldr (*) ps 1 = q"
and bqn: "(b^q) mod n = 1"
and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
shows "prime n"
--- a/src/HOL/Number_Theory/Totient.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Number_Theory/Totient.thy Mon Sep 24 23:49:43 2018 +0200
@@ -239,11 +239,11 @@
assumes "prime p"
shows "totient (p ^ Suc n) = p ^ n * (p - 1)"
proof -
- from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - ( * ) p ` {0<..p ^ n})"
+ from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - (*) p ` {0<..p ^ n})"
unfolding totient_def by (subst totatives_prime_power_Suc) simp_all
- also from assms have "\<dots> = p ^ Suc n - card (( * ) p ` {0<..p^n})"
+ also from assms have "\<dots> = p ^ Suc n - card ((*) p ` {0<..p^n})"
by (subst card_Diff_subset) (auto intro: prime_gt_0_nat)
- also from assms have "card (( * ) p ` {0<..p^n}) = p ^ n"
+ also from assms have "card ((*) p ` {0<..p^n}) = p ^ n"
by (subst card_image) (auto simp: inj_on_def)
also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps)
finally show ?thesis .
--- a/src/HOL/Probability/Independent_Family.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1165,7 +1165,7 @@
also have "...= prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
by (auto intro!: indep_varD[where Ma=N and Mb=N])
also have "... = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
- by (auto intro!: arg_cong2[where f= "( * )"] arg_cong[where f= prob])
+ by (auto intro!: arg_cong2[where f= "(*)"] arg_cong[where f= prob])
finally show ?thesis .
qed
--- a/src/HOL/Probability/PMF_Impl.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy Mon Sep 24 23:49:43 2018 +0200
@@ -231,7 +231,7 @@
qualified lemma mapping_of_bind_pmf:
assumes "finite (set_pmf p)"
shows "mapping_of_pmf (bind_pmf p f) =
- fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
+ fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
(mapping_of_pmf (f x))) (set_pmf p)"
using assms
by (intro mapping_of_pmfI')
@@ -268,7 +268,7 @@
lemma bind_pmf_aux_code_aux:
assumes "finite A"
shows "bind_pmf_aux p f A =
- fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
+ fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
(mapping_of_pmf (f x))) A" (is "?lhs = ?rhs")
proof (intro mapping_eqI'[where d = 0])
fix x assume "x \<in> Mapping.keys ?lhs"
@@ -287,7 +287,7 @@
lemma bind_pmf_aux_code [code]:
"bind_pmf_aux p f (set xs) =
- fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
+ fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
(mapping_of_pmf (f x))) (set xs)"
by (rule bind_pmf_aux_code_aux) simp_all
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Sep 24 23:49:43 2018 +0200
@@ -78,7 +78,7 @@
done
quotient_definition
- "(( * )) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+ "((*)) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
apply(rule equivp_transp[OF int_equivp])
apply(rule times_int_raw_fst)
apply(assumption)
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Mon Sep 24 23:49:43 2018 +0200
@@ -41,7 +41,7 @@
"times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
quotient_definition
- "(( * )) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute)
+ "((*)) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute)
fun plus_rat_raw where
"plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
--- a/src/HOL/Real.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real.thy Mon Sep 24 23:49:43 2018 +0200
@@ -32,7 +32,7 @@
for x :: "'a::cancel_semigroup_add"
by (meson add_left_imp_eq injI)
-lemma inj_mult_left [simp]: "inj (( * ) x) \<longleftrightarrow> x \<noteq> 0"
+lemma inj_mult_left [simp]: "inj ((*) x) \<longleftrightarrow> x \<noteq> 0"
for x :: "'a::idom"
by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Mon Sep 24 23:49:43 2018 +0200
@@ -603,7 +603,7 @@
hence "(\<lambda>n. (-(x^2))^n) sums (1 / (1 - (-(x^2))))" by (intro geometric_sums) simp_all
also have "1 - (-(x^2)) = 1 + x^2" by simp
also have "(\<lambda>n. (-(x^2))^n) = (\<lambda>n. ?f (2*n))" by (auto simp: fun_eq_iff power_minus' power_mult)
- also have "range (( *) (2::nat)) = {n. even n}"
+ also have "range ((*) (2::nat)) = {n. even n}"
by (auto elim!: evenE)
hence "(\<lambda>n. ?f (2*n)) sums (1 / (1 + x^2)) \<longleftrightarrow> ?f sums (1 / (1 + x^2))"
by (intro sums_mono_reindex) (simp_all add: strict_mono_Suc_iff)
@@ -1225,11 +1225,11 @@
| (xs, MSLNil) \<Rightarrow> MSLNil
| (MSLCons x xs, MSLCons y ys) \<Rightarrow>
MSLCons (fst x * fst y, snd x + snd y)
- (plus_ms_aux (mslmap (map_prod (( *) (fst x)) ((+) (snd x))) ys)
+ (plus_ms_aux (mslmap (map_prod ((*) (fst x)) ((+) (snd x))) ys)
(times_ms_aux xs (MSLCons y ys))))"
definition scale_shift_ms_aux :: "('a :: times \<times> real) \<Rightarrow> ('a \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
- "scale_shift_ms_aux = (\<lambda>(a,b) xs. mslmap (map_prod (( *) a) ((+) b)) xs)"
+ "scale_shift_ms_aux = (\<lambda>(a,b) xs. mslmap (map_prod ((*) a) ((+) b)) xs)"
lemma times_ms_aux_altdef:
"times_ms_aux xs ys =
@@ -1282,7 +1282,7 @@
qed
lemma scale_shift_ms_aux_conv_mslmap:
- "scale_shift_ms_aux x = mslmap (map_prod (( *) (fst x)) ((+) (snd x)))"
+ "scale_shift_ms_aux x = mslmap (map_prod ((*) (fst x)) ((+) (snd x)))"
by (rule ext) (simp add: scale_shift_ms_aux_def map_prod_def case_prod_unfold)
fun inverse_ms_aux :: "('a :: multiseries \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
@@ -2525,7 +2525,7 @@
have "times_ms_aux (MSLCons (const_expansion 1, 0) MSLNil) xs = xs" for xs :: "('a \<times> real) msllist"
proof (coinduction arbitrary: xs rule: msllist.coinduct_upto)
case Eq_real_prod_msllist
- have "map_prod (( *) (const_expansion 1 :: 'a)) ((+) (0::real)) = (\<lambda>x. x)"
+ have "map_prod ((*) (const_expansion 1 :: 'a)) ((+) (0::real)) = (\<lambda>x. x)"
by (rule ext) (simp add: map_prod_def times_const_expansion_1 case_prod_unfold)
moreover have "mslmap \<dots> = (\<lambda>x. x)" by (rule ext) (simp add: msllist.map_ident)
ultimately have "scale_shift_ms_aux (const_expansion 1 :: 'a, 0) = (\<lambda>x. x)"
--- a/src/HOL/Real_Asymp/Real_Asymp_Approx.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/Real_Asymp_Approx.thy Mon Sep 24 23:49:43 2018 +0200
@@ -39,7 +39,7 @@
fun eval_nat (@{term "(+) :: nat => _"} $ a $ b) = bin (op +) (a, b)
| eval_nat (@{term "(-) :: nat => _"} $ a $ b) = bin (clamp o op -) (a, b)
- | eval_nat (@{term "( * ) :: nat => _"} $ a $ b) = bin (op *) (a, b)
+ | eval_nat (@{term "(*) :: nat => _"} $ a $ b) = bin (op *) (a, b)
| eval_nat (@{term "(div) :: nat => _"} $ a $ b) = bin Int.div (a, b)
| eval_nat (@{term "(^) :: nat => _"} $ a $ b) = bin (fn (a,b) => Integer.pow a b) (a, b)
| eval_nat (t as (@{term "numeral :: _ => nat"} $ _)) = snd (HOLogic.dest_number t)
@@ -65,7 +65,7 @@
fun eval (@{term "(+) :: real => _"} $ a $ b) = eval a + eval b
| eval (@{term "(-) :: real => _"} $ a $ b) = eval a - eval b
- | eval (@{term "( * ) :: real => _"} $ a $ b) = eval a * eval b
+ | eval (@{term "(*) :: real => _"} $ a $ b) = eval a * eval b
| eval (@{term "(/) :: real => _"} $ a $ b) =
let val a = eval a; val b = eval b in
if Real.==(b, Real.fromInt 0) then nan else a / b
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Mon Sep 24 23:49:43 2018 +0200
@@ -257,7 +257,7 @@
| expr_to_term' (Add (a, b)) =
@{term "(+) :: real => _"} $ expr_to_term' a $ expr_to_term' b
| expr_to_term' (Mult (a, b)) =
- @{term "( *) :: real => _"} $ expr_to_term' a $ expr_to_term' b
+ @{term "(*) :: real => _"} $ expr_to_term' a $ expr_to_term' b
| expr_to_term' (Minus (a, b)) =
@{term "(-) :: real => _"} $ expr_to_term' a $ expr_to_term' b
| expr_to_term' (Div (a, b)) =
@@ -354,7 +354,7 @@
Add (reify' s, reify' t)
| reify'' (@{term "(-) :: real => _"} $ s $ t) =
Minus (reify' s, reify' t)
- | reify'' (@{term "( *) :: real => _"} $ s $ t) =
+ | reify'' (@{term "(*) :: real => _"} $ s $ t) =
Mult (reify' s, reify' t)
| reify'' (@{term "(/) :: real => _"} $ s $ t) =
Div (reify' s, reify' t)
@@ -435,7 +435,7 @@
Add (reify'' s, reify'' t)
| reify'' (@{term "(-) :: real => _"} $ s $ t) =
Minus (reify'' s, reify'' t)
- | reify'' (@{term "( *) :: real => _"} $ s $ t) =
+ | reify'' (@{term "(*) :: real => _"} $ s $ t) =
Mult (reify'' s, reify'' t)
| reify'' (@{term "(/) :: real => _"} $ s $ t) =
Div (reify'' s, reify'' t)
@@ -509,7 +509,7 @@
"(" ^ simple_print_const a ^ "+" ^ simple_print_const b ^ ")"
| simple_print_const (@{term "(-) :: real => _"} $ a $ b) =
"(" ^ simple_print_const a ^ "-" ^ simple_print_const b ^ ")"
- | simple_print_const (@{term "( * ) :: real => _"} $ a $ b) =
+ | simple_print_const (@{term "(*) :: real => _"} $ a $ b) =
"(" ^ simple_print_const a ^ "*" ^ simple_print_const b ^ ")"
| simple_print_const (@{term "inverse :: real => _"} $ a) =
"(1 / " ^ simple_print_const a ^ ")"
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML Mon Sep 24 23:49:43 2018 +0200
@@ -2262,7 +2262,7 @@
else if b aconv @{term "\<lambda>_::real. -1 :: real"} then
Term.betapply (@{term "\<lambda>(f::real\<Rightarrow>real) x. -f x"}, a)
else
- Abs ("x", @{typ real}, @{term "( *) :: real => _"} $
+ Abs ("x", @{typ real}, @{term "(*) :: real => _"} $
(Term.betapply (a, Bound 0)) $ (Term.betapply (b, Bound 0)))
fun mk_powr b e =
--- a/src/HOL/Real_Vector_Spaces.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Sep 24 23:49:43 2018 +0200
@@ -53,8 +53,8 @@
end
global_interpretation real_vector?: vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
- rewrites "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
- and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
+ rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
+ and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
defines dependent_raw_def: dependent = real_vector.dependent
and representation_raw_def: representation = real_vector.representation
and subspace_raw_def: subspace = real_vector.subspace
@@ -82,8 +82,8 @@
abbreviation "independent x \<equiv> \<not> dependent x"
global_interpretation real_vector?: vector_space_pair "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
- rewrites "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
- and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
+ rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
+ and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
defines construct_raw_def: construct = real_vector.construct
apply unfold_locales
unfolding linear_def real_scaleR_def
@@ -1316,7 +1316,7 @@
corollary real_linearD:
fixes f :: "real \<Rightarrow> real"
- assumes "linear f" obtains c where "f = ( *) c"
+ assumes "linear f" obtains c where "f = (*) c"
by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
lemma linear_times_of_real: "linear (\<lambda>x. a * of_real x)"
@@ -1439,7 +1439,7 @@
lemma comp1:
assumes "bounded_linear g"
- shows "bounded_bilinear (\<lambda>x. ( **) (g x))"
+ shows "bounded_bilinear (\<lambda>x. (**) (g x))"
proof unfold_locales
interpret g: bounded_linear g by fact
show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
@@ -1537,7 +1537,7 @@
qed
qed
-lemma bounded_bilinear_mult: "bounded_bilinear (( *) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
+lemma bounded_bilinear_mult: "bounded_bilinear ((*) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
apply (rule bounded_bilinear.intro)
apply (auto simp: algebra_simps)
apply (rule_tac x=1 in exI)
--- a/src/HOL/SMT.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/SMT.thy Mon Sep 24 23:49:43 2018 +0200
@@ -134,7 +134,7 @@
lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
lemma nat_plus_as_int: "(+) = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
lemma nat_minus_as_int: "(-) = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
-lemma nat_times_as_int: "( * ) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
+lemma nat_times_as_int: "(*) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
lemma nat_div_as_int: "(div) = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
lemma nat_mod_as_int: "(mod) = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
--- a/src/HOL/SMT_Examples/boogie.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML Mon Sep 24 23:49:43 2018 +0200
@@ -139,7 +139,7 @@
parse_bin_expr cx (mk_binary @{term "(<=) :: int => _"} o swap) ls
| parse_expr cx (["+"] :: ls) = parse_bin_expr cx (mk_binary @{term "(+) :: int => _"}) ls
| parse_expr cx (["-"] :: ls) = parse_bin_expr cx (mk_binary @{term "(-) :: int => _"}) ls
- | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "( * ) :: int => _"}) ls
+ | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "(*) :: int => _"}) ls
| parse_expr cx (["/"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_div}) ls
| parse_expr cx (["%"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
| parse_expr cx (["select", n] :: ls) =
--- a/src/HOL/Set_Interval.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Set_Interval.thy Mon Sep 24 23:49:43 2018 +0200
@@ -1015,12 +1015,12 @@
context linordered_field begin
lemma image_mult_atLeastAtMost [simp]:
- "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
+ "((*) d ` {a..b}) = {d*a..d*b}" if "d>0"
using that
by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
lemma image_mult_atLeastAtMost_if:
- "( * ) c ` {x .. y} =
+ "(*) c ` {x .. y} =
(if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
proof -
consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
@@ -1028,7 +1028,7 @@
then show ?thesis
proof cases
case 1
- have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
+ have "(*) c ` {x .. y} = uminus ` (*) (- c) ` {x .. y}"
by (simp add: image_image)
also have "\<dots> = {c * y .. c * x}"
using \<open>c < 0\<close>
@@ -1049,7 +1049,7 @@
else if 0 \<le> m then {m*a + c .. m *b + c}
else {m*b + c .. m*a + c})"
proof -
- have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
+ have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o (*) m)"
unfolding image_comp[symmetric]
by (simp add: o_def)
then show ?thesis
@@ -2474,7 +2474,7 @@
lemma prod_atLeastAtMost_code:
"prod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
proof -
- have "comp_fun_commute (\<lambda>a. ( * ) (f a))"
+ have "comp_fun_commute (\<lambda>a. (*) (f a))"
by unfold_locales (auto simp: o_def mult_ac)
thus ?thesis
by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)
--- a/src/HOL/TLA/Intensional.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/TLA/Intensional.thy Mon Sep 24 23:49:43 2018 +0200
@@ -119,7 +119,7 @@
"_liftIf" == "_lift3 (CONST If)"
"_liftPlus" == "_lift2 (+)"
"_liftMinus" == "_lift2 (-)"
- "_liftTimes" == "_lift2 (( * ))"
+ "_liftTimes" == "_lift2 ((*))"
"_liftDiv" == "_lift2 (div)"
"_liftMod" == "_lift2 (mod)"
"_liftLess" == "_lift2 (<)"
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Sep 24 23:49:43 2018 +0200
@@ -23,7 +23,7 @@
val allowed_consts =
[@{term "(+) :: int => _"}, @{term "(+) :: nat => _"},
@{term "(-) :: int => _"}, @{term "(-) :: nat => _"},
- @{term "( * ) :: int => _"}, @{term "( * ) :: nat => _"},
+ @{term "(*) :: int => _"}, @{term "(*) :: nat => _"},
@{term "(div) :: int => _"}, @{term "(div) :: nat => _"},
@{term "(mod) :: int => _"}, @{term "(mod) :: nat => _"},
@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
@@ -171,7 +171,7 @@
val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP;
val cadd = @{cterm "(+) :: int => _"}
-val cmulC = @{cterm "( * ) :: int => _"}
+val cmulC = @{cterm "(*) :: int => _"}
val cminus = @{cterm "(-) :: int => _"}
val cone = @{cterm "1 :: int"}
val [addC, mulC, subC] = map Thm.term_of [cadd, cmulC, cminus]
@@ -662,7 +662,7 @@
| term_of_num vs (Proc.Sub (t1, t2)) =
@{term "(-) :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
| term_of_num vs (Proc.Mul (i, t2)) =
- @{term "( * ) :: int => _"} $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2
+ @{term "(*) :: int => _"} $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2
| term_of_num vs (Proc.CN (n, i, t')) =
term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
@@ -765,7 +765,7 @@
if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t))
then false
else case Thm.term_of t of
- c$l$r => if member (op =) [@{term"( * )::int => _"}, @{term"( * )::nat => _"}] c
+ c$l$r => if member (op =) [@{term"(*)::int => _"}, @{term"(*)::nat => _"}] c
then not (isnum l orelse isnum r)
else not (member (op aconv) cts c)
| c$_ => not (member (op aconv) cts c)
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Mon Sep 24 23:49:43 2018 +0200
@@ -61,13 +61,13 @@
definition dependent :: "'b set \<Rightarrow> bool"
where dependent_on_def: "dependent s \<longleftrightarrow> (\<exists>t u. finite t \<and> t \<subseteq> s \<and> (sum (\<lambda>v. u v *s v) t = 0 \<and> (\<exists>v\<in>t. u v \<noteq> 0)))"
-lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 ( *s) = subspace"
+lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 (*s) = subspace"
unfolding subspace_on_def subspace_with_def ..
-lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 ( *s) = dependent"
+lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 (*s) = dependent"
unfolding dependent_on_def dependent_with_def sum_with ..
-lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 ( *s) = span"
+lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 (*s) = span"
unfolding span_on_def span_with_def sum_with ..
end
@@ -109,7 +109,7 @@
then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V)
else 0)"
-lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 ( *s) = dim"
+lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 (*s) = dim"
unfolding dim_on_with_def dim_def implicit_ab_group_add ..
end
--- a/src/HOL/Vector_Spaces.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy Mon Sep 24 23:49:43 2018 +0200
@@ -77,10 +77,10 @@
lemma linear_imp_scale:
fixes D::"'a \<Rightarrow> 'b"
- assumes "linear ( *) scale D"
+ assumes "linear (*) scale D"
obtains d where "D = (\<lambda>x. scale x d)"
proof -
- interpret linear "( *)" scale D by fact
+ interpret linear "(*)" scale D by fact
show ?thesis
by (metis mult.commute mult.left_neutral scale that)
qed
@@ -806,7 +806,7 @@
lemma in_span_in_range_construct:
"x \<in> range (construct B f)" if i: "vs1.independent B" and x: "x \<in> vs2.span (f ` B)"
proof -
- interpret linear "( *a)" "( *b)" "construct B f"
+ interpret linear "(*a)" "(*b)" "construct B f"
using i by (rule linear_construct)
obtain bb :: "('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'b set \<Rightarrow> 'b" where
"\<forall>x0 x1 x2. (\<exists>v4. v4 \<in> x2 \<and> x1 v4 \<noteq> x0 v4) = (bb x0 x1 x2 \<in> x2 \<and> x1 (bb x0 x1 x2) \<noteq> x0 (bb x0 x1 x2))"
@@ -853,7 +853,7 @@
have fB: "vs2.independent (f ` B)"
using independent_injective_image[OF B f] .
let ?g = "p.construct (f ` B) (the_inv_into B f)"
- show "linear ( *b) ( *a) ?g"
+ show "linear (*b) (*a) ?g"
by (rule p.linear_construct[OF fB])
have "?g b \<in> vs1.span (the_inv_into B f ` f ` B)" for b
by (intro p.construct_in_span fB)
@@ -864,13 +864,13 @@
by (auto simp: V_eq)
have "(?g \<circ> f) v = id v" if "v \<in> vs1.span B" for v
proof (rule vector_space_pair.linear_eq_on[where x=v])
- show "vector_space_pair ( *a) ( *a)" by unfold_locales
- show "linear ( *a) ( *a) (?g \<circ> f)"
- proof (rule Vector_Spaces.linear_compose[of _ "( *b)"])
- show "linear ( *a) ( *b) f"
+ show "vector_space_pair (*a) (*a)" by unfold_locales
+ show "linear (*a) (*a) (?g \<circ> f)"
+ proof (rule Vector_Spaces.linear_compose[of _ "(*b)"])
+ show "linear (*a) (*b) f"
by unfold_locales
qed fact
- show "linear ( *a) ( *a) id" by (rule vs1.linear_id)
+ show "linear (*a) (*a) id" by (rule vs1.linear_id)
show "v \<in> vs1.span B" by fact
show "b \<in> B \<Longrightarrow> (p.construct (f ` B) (the_inv_into B f) \<circ> f) b = id b" for b
by (simp add: p.construct_basis fB the_inv_into_f_f inj_on_subset[OF f vs1.span_superset])
@@ -895,7 +895,7 @@
proof (intro exI ballI conjI)
interpret p: vector_space_pair s2 s1 by unfold_locales
let ?g = "p.construct C g"
- show "linear ( *b) ( *a) ?g"
+ show "linear (*b) (*a) ?g"
by (rule p.linear_construct[OF C])
have "?g v \<in> vs1.span (g ` C)" for v
by (rule p.construct_in_span[OF C])
@@ -903,10 +903,10 @@
finally show "?g ` UNIV \<subseteq> V" by auto
have "(f \<circ> ?g) v = id v" if v: "v \<in> f ` V" for v
proof (rule vector_space_pair.linear_eq_on[where x=v])
- show "vector_space_pair ( *b) ( *b)" by unfold_locales
- show "linear ( *b) ( *b) (f \<circ> ?g)"
- by (rule Vector_Spaces.linear_compose[of _ "( *a)"]) fact+
- show "linear ( *b) ( *b) id" by (rule vs2.linear_id)
+ show "vector_space_pair (*b) (*b)" by unfold_locales
+ show "linear (*b) (*b) (f \<circ> ?g)"
+ by (rule Vector_Spaces.linear_compose[of _ "(*a)"]) fact+
+ show "linear (*b) (*b) id" by (rule vs2.linear_id)
have "vs2.span (f ` B) = vs2.span C"
using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
by auto
--- a/src/HOL/Word/Word.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Word/Word.thy Mon Sep 24 23:49:43 2018 +0200
@@ -273,7 +273,7 @@
lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
by (auto simp add: bintrunc_mod2p intro: mod_minus_cong)
-lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "( * )"
+lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(*)"
by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
definition word_div_def: "a div b = word_of_int (uint a div uint b)"
--- a/src/HOL/ex/LocaleTest2.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/ex/LocaleTest2.thy Mon Sep 24 23:49:43 2018 +0200
@@ -738,7 +738,7 @@
locale Dgrp = Dmonoid +
- assumes unit [intro, simp]: "Dmonoid.unit (( ** )) one x"
+ assumes unit [intro, simp]: "Dmonoid.unit ((**)) one x"
begin
--- a/src/HOL/ex/Transfer_Int_Nat.thy Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Mon Sep 24 23:49:43 2018 +0200
@@ -38,7 +38,7 @@
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (+) (+)"
unfolding rel_fun_def ZN_def by simp
-lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (( * )) (( * ))"
+lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) ((*)) ((*))"
unfolding rel_fun_def ZN_def by simp
definition tsub :: "int \<Rightarrow> int \<Rightarrow> int"
--- a/src/Pure/Syntax/mixfix.ML Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Pure/Syntax/mixfix.ML Mon Sep 24 23:49:43 2018 +0200
@@ -172,12 +172,8 @@
val binder_name = suffix "_binder";
fun mk_prefix sy =
- let
- fun star1 sys = (fst(hd sys) = "*");
- val sy' = Input.source_explode (Input.reset_pos sy);
- val lpar = Symbol_Pos.explode0 ("'(" ^ (if star1 sy' then " " else ""));
- val rpar = Symbol_Pos.explode0 ((if star1(rev sy') then " " else "") ^ "')")
- in lpar @ sy' @ rpar end
+ let val sy' = Input.source_explode (Input.reset_pos sy);
+ in Symbol_Pos.explode0 "'(" @ sy' @ Symbol_Pos.explode0 "')" end
fun syn_ext_consts logical_types const_decls =
let