# HG changeset patch # User haftmann # Date 1570632714 0 # Node ID dd675800469d3e6294ce1f0daa94613268997613 # Parent 5bc338cee4a0814f6d183d440b4705cdcd488483 dedicated fact collections for algebraic simplification rules potentially splitting goals diff -r 5bc338cee4a0 -r dd675800469d NEWS --- a/NEWS Wed Oct 09 23:00:52 2019 +0200 +++ b/NEWS Wed Oct 09 14:51:54 2019 +0000 @@ -71,10 +71,11 @@ 1): theory HOL/Library/Bit.thy has been renamed accordingly. INCOMPATIBILITY. -* Fact collection sign_simps contains only simplification rules for -products being less / greater / equal to zero; combine with existing -collections algebra_simps or field_simps to obtain reasonable -simplification. INCOMPATIBILITY. +* Fact collections algebra_split_simps and field_split_simps correspond +to algebra_simps and field_simps but contain more aggressive rules +potentially splitting goals; algebra_split_simps roughly replaces +sign_simps and field_split_simps can be used instead of divide_simps. +INCOMPATIBILITY. * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) associates to the left now as is customary. diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Abstract_Euclidean_Space.thy --- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Oct 09 14:51:54 2019 +0000 @@ -270,7 +270,7 @@ done next have 1: "\x i. \ i \ n; x i \ 0\ \ (\i\n. (x i / sqrt (\j\n. (x j)\<^sup>2))\<^sup>2) = 1" - by (force simp: sum_nonneg sum_nonneg_eq_0_iff divide_simps simp flip: sum_divide_distrib) + by (force simp: sum_nonneg sum_nonneg_eq_0_iff field_split_simps simp flip: sum_divide_distrib) have cm: "continuous_map ?Y (nsphere n) (\x i. x i / sqrt (\j\n. (x j)\<^sup>2))" unfolding Euclidean_space_def nsphere subtopology_subtopology continuous_map_in_subtopology proof (intro continuous_intros conjI) @@ -390,7 +390,7 @@ have 2: "(?g \ ?h) (0, x) = f x" if "x \ topspace (nsphere p)" for x using that f1 by simp have 3: "(?g \ ?h) (1, x) = (\i. - a i)" for x - using a by (force simp: divide_simps nsphere) + using a by (force simp: field_split_simps nsphere) then show "homotopic_with (\x. True) (nsphere p) (nsphere p) f (\x. (\i. - a i))" by (force simp: homotopic_with intro: 1 2 3) qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Arcwise_Connected.thy --- a/src/HOL/Analysis/Arcwise_Connected.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Arcwise_Connected.thy Wed Oct 09 14:51:54 2019 +0000 @@ -211,7 +211,7 @@ proof assume "of_nat m = (4 * of_nat k + 1) / (2 * 2^n :: 'a)" then have "of_nat (m * (2 * 2^n)) = (of_nat (Suc (4 * k)) :: 'a)" - by (simp add: divide_simps) + by (simp add: field_split_simps) then have "m * (2 * 2^n) = Suc (4 * k)" using of_nat_eq_iff by blast then have "odd (m * (2 * 2^n))" @@ -224,7 +224,7 @@ proof assume "of_nat m = (4 * of_nat k + 3) / (2 * 2^n :: 'a)" then have "of_nat (m * (2 * 2^n)) = (of_nat (4 * k + 3) :: 'a)" - by (simp add: divide_simps) + by (simp add: field_split_simps) then have "m * (2 * 2^n) = (4 * k) + 3" using of_nat_eq_iff by blast then have "odd (m * (2 * 2^n))" @@ -520,7 +520,7 @@ lemma dyadics_in_open_unit_interval: "{0<..<1} \ (\k m. {real m / 2^k}) = (\k. \m \ {0<..<2^k}. {real m / 2^k})" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) @@ -738,9 +738,9 @@ by simp finally have "(real i * 2^n - real j * 2^m) / 2^m \ \" . with True Ints_abs show "\2^n\ * \real i / 2^m - real j / 2^n\ \ \" - by (fastforce simp: divide_simps) + by (fastforce simp: field_split_simps) show "\\2^n\ * \real i / 2^m - real j / 2^n\\ < 1" - using less.prems by (auto simp: divide_simps) + using less.prems by (auto simp: field_split_simps) qed then have "real i / 2^m = real j / 2^n" by auto @@ -770,7 +770,7 @@ proof (cases "real i / 2^m" "real j / 2^n" rule: linorder_cases) case less moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n" - using k by (force simp: divide_simps) + using k by (force simp: field_split_simps) moreover have "\real i / 2 ^ m - real j / 2 ^ n\ < 2 / (2 ^ Suc n)" using less.prems by simp ultimately have closer: "\real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\ < 1 / (2 ^ Suc n)" @@ -778,7 +778,7 @@ have *: "a (real (4 * k + 1) / 2 ^ Suc n) \ c (real i / 2 ^ m) \ c (real i / 2 ^ m) \ b (real (4 * k + 1) / 2 ^ Suc n)" apply (rule less.IH [OF _ refl]) - using closer \n < m\ \d = m - n\ apply (auto simp: divide_simps \n < m\ diff_less_mono2) + using closer \n < m\ \d = m - n\ apply (auto simp: field_split_simps \n < m\ diff_less_mono2) done show ?thesis using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] @@ -791,7 +791,7 @@ next case greater moreover have "real (4 * k + 3) / 2 ^ Suc n - 1 / (2 ^ Suc n) = real j / 2 ^ n" - using k by (force simp: divide_simps) + using k by (force simp: field_split_simps) moreover have "\real i / 2 ^ m - real j / 2 ^ n\ < 2 * 1 / (2 ^ Suc n)" using less.prems by simp ultimately have closer: "\real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\ < 1 / (2 ^ Suc n)" @@ -799,7 +799,7 @@ have *: "a (real (4 * k + 3) / 2 ^ Suc n) \ c (real i / 2 ^ m) \ c (real i / 2 ^ m) \ b (real (4 * k + 3) / 2 ^ Suc n)" apply (rule less.IH [OF _ refl]) - using closer \n < m\ \d = m - n\ apply (auto simp: divide_simps \n < m\ diff_less_mono2) + using closer \n < m\ \d = m - n\ apply (auto simp: field_split_simps \n < m\ diff_less_mono2) done show ?thesis using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] @@ -963,7 +963,7 @@ obtain n where n: "1/2^n < min d 1" by (metis \0 < d\ divide_less_eq_1 less_numeral_extra(1) min_def one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral) with gr0I have "n > 0" - by (force simp: divide_simps) + by (force simp: field_split_simps) show "\d>0. \x\D01. \x'\D01. dist x' x < d \ dist (f (c x')) (f (c x)) < e" proof (intro exI ballI impI conjI) show "(0::real) < 1/2^n" by auto @@ -1100,12 +1100,12 @@ by auto show "\real i / 2 ^ m - real j / 2 ^ n\ < 1/2 ^ n" using clo less_j1 j_le - apply (auto simp: le_max_iff_disj divide_simps dist_norm) + apply (auto simp: le_max_iff_disj field_split_simps dist_norm) apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2) done show "\real k / 2 ^ p - real j / 2 ^ n\ < 1/2 ^ n" using clo less_j1 j_le - apply (auto simp: le_max_iff_disj divide_simps dist_norm) + apply (auto simp: le_max_iff_disj field_split_simps dist_norm) apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2) done qed (use False in simp) @@ -1392,7 +1392,7 @@ proof cases case 1 with less.prems show ?thesis - by (rule_tac x=1 in exI)+ (fastforce simp: divide_simps) + by (rule_tac x=1 in exI)+ (fastforce simp: field_split_simps) next case 2 show ?thesis proof (cases m) @@ -1415,7 +1415,7 @@ then show ?thesis using less.IH [of "m'+p'" i m' k p'] less.prems \m = Suc m'\ 2 Suc apply atomize - apply (force simp: divide_simps) + apply (force simp: field_split_simps) done qed qed @@ -1464,7 +1464,7 @@ have "c(i / 2^m) \ b(real(4 * q + 1) / 2 ^ (Suc n'))" apply (rule ci_le_bj, force) apply (rule * [OF less]) - using i_le_j clo_ij q apply (auto simp: divide_simps) + using i_le_j clo_ij q apply (auto simp: field_split_simps) done then show ?thesis using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] b41 [of n' q] \n' \ 0\ @@ -1484,7 +1484,7 @@ have "a(real(4*q + 3) / 2 ^ (Suc n')) \ c(j / 2^n)" apply (rule aj_le_ci, force) apply (rule * [OF less]) - using j_le_j clo_jj q apply (auto simp: divide_simps) + using j_le_j clo_jj q apply (auto simp: field_split_simps) done then show ?thesis using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] a43 [of n' q] \n' \ 0\ @@ -1589,7 +1589,7 @@ then show ?thesis by (metis that) qed have m_div: "0 < m / 2^n" "m / 2^n < 1" - using m by (auto simp: divide_simps) + using m by (auto simp: field_split_simps) have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \ (\k m. {real m / 2 ^ k}))" by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m) have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \ (\k m. {real m / 2 ^ k}))" @@ -1611,7 +1611,7 @@ fix p q assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n" then have [simp]: "0 < p" "p < 2 ^ q" - apply (simp add: divide_simps) + apply (simp add: field_split_simps) apply (blast intro: p less_2I m_div less_trans) done have "f (c (real p / 2 ^ q)) \ f ` {0..c (real m / 2 ^ n)}" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Ball_Volume.thy --- a/src/HOL/Analysis/Ball_Volume.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Ball_Volume.thy Wed Oct 09 14:51:54 2019 +0000 @@ -46,7 +46,7 @@ (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def) also have "\ = (\\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel)" by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) - (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac) + (auto simp: indicator_def powr_minus powr_half_sqrt field_split_simps ennreal_mult' mult_ac) also have "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel) + (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel)" (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Oct 09 14:51:54 2019 +0000 @@ -289,7 +289,7 @@ apply (rule onorm_le_matrix_component) using Bclo by (simp add: abs_minus_commute less_imp_le) also have "\ < e" - using \0 < e\ by (simp add: divide_simps) + using \0 < e\ by (simp add: field_split_simps) finally show "onorm ((*v) (A - B)) < e" . qed (use B in auto) qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Oct 09 14:51:54 2019 +0000 @@ -323,7 +323,7 @@ show "(g1 +++ g2 \ (\x. (x + 1) / 2)) x' = g2 x'" if "x' \ {0..1}" "dist x' x < dist ((x + 1) / 2) (1/2)" for x' proof - have [simp]: "(2*x'+2)/2 = x'+1" - by (simp add: divide_simps) + by (simp add: field_split_simps) show ?thesis using that by (auto simp: joinpaths_def) qed @@ -691,7 +691,7 @@ show "g1 +++ g2 \ (\x. (x + 1) / 2) differentiable at x" using g12D that apply (simp only: joinpaths_def) - apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps) + apply (drule_tac x= "(x+1) / 2" in bspec, force simp: field_split_simps) apply (rule differentiable_chain_at derivative_intros | force)+ done show "\x'. dist x' x < dist ((x + 1) / 2) (1/2) \ (g1 +++ g2 \ (\x. (x + 1) / 2)) x' = g2 x'" @@ -699,7 +699,7 @@ qed (use that in \auto simp: dist_norm\) have [simp]: "vector_derivative (g2 \ (\x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)" if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` S)" for x - using that by (auto simp: vector_derivative_chain_at divide_simps g2D) + using that by (auto simp: vector_derivative_chain_at field_split_simps g2D) have "continuous_on ({1/2..1} - insert (1/2) S) (\x. vector_derivative (g1 +++ g2) (at x))" using co12 by (rule continuous_on_subset) force then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) S) (\x. vector_derivative (g2 \ (\x. 2*x-1)) (at x))" @@ -1926,7 +1926,7 @@ { assume *: "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R c) * (c - a)) has_integral i) {0..1}" have **: "\x. ((k - x) / k) *\<^sub>R a + (x / k) *\<^sub>R c = (1 - x) *\<^sub>R a + x *\<^sub>R b" using False apply (simp add: c' algebra_simps) - apply (simp add: real_vector.scale_left_distrib [symmetric] divide_simps) + apply (simp add: real_vector.scale_left_distrib [symmetric] field_split_simps) done have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}" using k has_integral_affinity01 [OF *, of "inverse k" "0"] @@ -2185,28 +2185,28 @@ case 1 then have "?\ a c' b'" using assms apply (clarsimp simp: c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) - apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) + apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast next case 2 then have "?\ a' c' b" using assms apply (clarsimp simp: a'_def c'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) - apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) + apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast next case 3 then have "?\ a' c b'" using assms apply (clarsimp simp: a'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) - apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) + apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast next case 4 then have "?\ a' b' c'" using assms apply (clarsimp simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) - apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) + apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast qed @@ -2576,7 +2576,7 @@ by (simp add: algebra_simps) have "cmod y / (24 * C) \ cmod y / cmod (b - a) / 12" using False \C>0\ diff_2C [of b a] ynz - by (auto simp: divide_simps hull_inc) + by (auto simp: field_split_simps hull_inc) have less_C: "\u \ convex hull {a, b, c}; 0 \ x; x \ 1\ \ x * cmod u < C" for x u apply (cases "x=0", simp add: \0) using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast @@ -2610,7 +2610,7 @@ by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull) also have "\ \ cmod y / cmod (v - u) / 12" using False uv \C>0\ diff_2C [of v u] ynz - by (auto simp: divide_simps hull_inc) + by (auto simp: field_split_simps hull_inc) finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \ cmod y / cmod (v - u) / 12" by simp then have cmod_12_le: "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) * 12 \ cmod y" @@ -3993,7 +3993,7 @@ using eq by (simp add: exp_eq_1 complex_is_Int_iff) have "exp (contour_integral p (\w. 1 / (w - z))) = (\ 1 - z) / (\ 0 - z)" using p winding_number_exp_integral(2) [of p 0 1 z] - apply (simp add: valid_path_def path_defs contour_integral_integral exp_minus divide_simps) + apply (simp add: valid_path_def path_defs contour_integral_integral exp_minus field_split_simps) by (metis path_image_def pathstart_def pathstart_in_path_image) then have "winding_number p z \ \ \ pathfinish p = pathstart p" using p wneq iff by (auto simp: path_defs) @@ -4528,7 +4528,7 @@ define z' where "z' = z - (d / (2 * cmod a)) *\<^sub>R a" have *: "a \ z' \ b - d / 3 * cmod a" unfolding z'_def inner_mult_right' divide_inverse - apply (simp add: divide_simps algebra_simps dot_square_norm power2_eq_square anz) + apply (simp add: field_split_simps algebra_simps dot_square_norm power2_eq_square anz) apply (metis \0 < d\ add_increasing azb less_eq_real_def mult_nonneg_nonneg mult_right_mono norm_ge_zero norm_numeral) done have "cmod (winding_number \ z' - winding_number \ z) < \Re (winding_number \ z)\ - 1/2" @@ -4542,7 +4542,7 @@ moreover have "\Re (winding_number \ z')\ < 1/2" apply (rule winding_number_lt_half [OF \ *]) using azb \d>0\ pag - apply (auto simp: add_strict_increasing anz divide_simps algebra_simps dest!: subsetD) + apply (auto simp: add_strict_increasing anz field_split_simps algebra_simps dest!: subsetD) done ultimately have False by simp @@ -4620,7 +4620,7 @@ show ?thesis apply (rule has_contour_integral_eq) using znotin has_contour_integral_add [OF has_contour_integral_lmul [OF has_contour_integral_winding_number [OF vpg znotin], of "f z"] *] - apply (auto simp: mult_ac divide_simps) + apply (auto simp: ac_simps divide_simps) done qed @@ -5009,7 +5009,7 @@ then have "z + of_real r * exp (\ * of_real z) \ (\x. z + of_real r * exp (\ * linepath s t x)) ` {0..1}" apply (rule_tac x="(z - s)/(t - s)" in image_eqI) apply (simp add: linepath_def scaleR_conv_of_real divide_simps exp_eq) - apply (auto simp: algebra_simps divide_simps) + apply (auto simp: field_split_simps) done } ultimately show ?thesis @@ -5148,7 +5148,7 @@ have *: "finite {x. cmod (complex_of_real (2 * real_of_int x * pi) * \) \ b + cmod (Ln w)}" apply (simp add: norm_mult finite_int_iff_bounded_le) apply (rule_tac x="\(b + cmod (Ln w)) / (2*pi)\" in exI) - apply (auto simp: divide_simps le_floor_iff) + apply (auto simp: field_split_simps le_floor_iff) done have [simp]: "\P f. {z. P z \ (\n. z = f n)} = f ` {n. P (f n)}" by blast @@ -5274,7 +5274,8 @@ proof (rule ccontr) assume "\ \s - t\ \ 2 * pi" then have *: "\n. t - s \ of_int n * \s - t\" - using False that [of "2*pi / \t - s\"] by (simp add: abs_minus_commute divide_simps) + using False that [of "2*pi / \t - s\"] + by (simp add: abs_minus_commute divide_simps) show False using * [of 1] * [of "-1"] by auto qed @@ -5292,7 +5293,7 @@ apply (subst abs_away) apply (auto simp: 1) apply (rule ccontr) - apply (auto simp: 2 divide_simps abs_mult dest: of_int_leD) + apply (auto simp: 2 field_split_simps abs_mult dest: of_int_leD) done qed @@ -5408,7 +5409,7 @@ apply (rule sincos_total_2pi [of "Re(w/of_real(norm w))" "Im(w/of_real(norm w))"]) apply (simp add: divide_simps \w \ 0\ cmod_power2 [symmetric]) apply (rule_tac x="t / (2*pi)" in image_eqI) - apply (simp add: divide_simps \w \ 0\) + apply (simp add: field_simps \w \ 0\) using False ** apply (auto simp: w_def) done @@ -5565,7 +5566,7 @@ using eventually_happens [OF eventually_conj] by (fastforce simp: contour_integrable_on path_image_def) have Ble: "B * e / (\B\ + 1) \ e" - using \0 \ B\ \0 < e\ by (simp add: divide_simps) + using \0 \ B\ \0 < e\ by (simp add: field_split_simps) have "\h. (\x\{0..1}. cmod (l (\ x) * vector_derivative \ (at x) - h x) \ e) \ h integrable_on {0..1}" proof (intro exI conjI ballI) show "cmod (l (\ x) * vector_derivative \ (at x) - f a (\ x) * vector_derivative \ (at x)) \ e" @@ -5693,7 +5694,8 @@ qed { fix a::real and b::real assume ab: "a > 0" "b > 0" then have "k * (1 + real k) * (1 / a) \ k * (1 + real k) * (4 / b) \ b \ 4 * a" - by (subst mult_le_cancel_left_pos) (use \k \ 0\ in \auto simp: divide_simps\) + by (subst mult_le_cancel_left_pos) + (use \k \ 0\ in \auto simp: divide_simps\) with ab have "real k * (1 + real k) / a \ (real k * 4 + real k * real k * 4) / b \ b \ 4 * a" by (simp add: field_simps) } note canc = this @@ -5706,14 +5708,14 @@ using lessd d x by (auto simp add: dist_norm path_image_def ball_def not_less [symmetric] del: divide_const_simps) then have "d \ cmod (x - v) * 2" - by (simp add: divide_simps) + by (simp add: field_split_simps) then have dpow_le: "d ^ (k+2) \ (cmod (x - v) * 2) ^ (k+2)" using \0 < d\ order_less_imp_le power_mono by blast have "x \ v" using that using \x \ path_image \\ ball_divide_subset_numeral d by fastforce then show ?thesis using \d > 0\ apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc) - using dpow_le apply (simp add: algebra_simps divide_simps mult_less_0_iff) + using dpow_le apply (simp add: algebra_simps field_split_simps mult_less_0_iff) done qed have ub: "u \ ball w (d/2)" @@ -6370,7 +6372,7 @@ show ?thes1 using * using contour_integrable_on_def by blast show ?thes2 - unfolding contour_integral_unique [OF *] by (simp add: divide_simps) + unfolding contour_integral_unique [OF *] by (simp add: field_split_simps) qed corollary Cauchy_contour_integral_circlepath: @@ -6461,7 +6463,7 @@ also have "\ \ e * norm (u - w)" using r kle \0 < e\ by (simp add: dist_commute dist_norm) finally show ?thesis - by (simp add: divide_simps norm_divide del: power_Suc) + by (simp add: field_split_simps norm_divide del: power_Suc) qed with \0 < r\ show "\\<^sub>F n in sequentially. \x\sphere z r. norm ((\kR > 0\ fz show False using has_contour_integral_bound_circlepath [OF *, of "norm(f z)/2/R"] - by (auto simp: less_imp_le norm_mult norm_divide divide_simps) + by (auto simp: less_imp_le norm_mult norm_divide field_split_simps) qed proposition Liouville_weak: @@ -6546,7 +6548,7 @@ have 2: "((\x. 1 / f x) \ 0) at_infinity" apply (rule tendstoI [OF eventually_mono]) apply (rule_tac B="2/e" in unbounded) - apply (simp add: dist_norm norm_divide divide_simps mult_ac) + apply (simp add: dist_norm norm_divide field_split_simps mult_ac) done have False using Liouville_weak_0 [OF 1 2] f by simp @@ -6679,7 +6681,7 @@ then have f': "f' n w = 1 / (2 * of_real pi * \) * ?conint (\u. f n u / (u - w)\<^sup>2)" using DERIV_unique [OF fnd] w by blast show ?thesis - by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] divide_simps) + by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] field_split_simps) qed define d where "d = (r - norm(w - z))^2" have "d > 0" @@ -6703,7 +6705,7 @@ fix e::real assume "0 < e" with \r > 0\ show "\\<^sub>F n in F. \x\sphere z r. dist (f n x / (x - w)\<^sup>2) (g x / (x - w)\<^sup>2) < e" - apply (simp add: norm_divide divide_simps sphere_def dist_norm) + apply (simp add: norm_divide field_split_simps sphere_def dist_norm) apply (rule eventually_mono [OF uniform_limitD [OF ulim], of "e*d"]) apply (simp add: \0 < d\) apply (force simp: dist_norm dle intro: less_le_trans) @@ -6949,7 +6951,7 @@ have inb: "z + complex_of_real ((dist z w + r) / 2) \ ball z r" proof - have wz: "cmod (w - z) < r" using w - by (auto simp: divide_simps dist_norm norm_minus_commute) + by (auto simp: field_split_simps dist_norm norm_minus_commute) then have "0 \ r" by (meson less_eq_real_def norm_ge_zero order_trans) show ?thesis @@ -7145,7 +7147,7 @@ shows "(\z. if z = a then deriv g a else f z - g a/(z - a)) holomorphic_on S" using pole_lemma [OF holg a] - by (rule holomorphic_transform) (simp add: eq divide_simps) + by (rule holomorphic_transform) (simp add: eq field_split_simps) lemma pole_lemma_open: assumes "f holomorphic_on S" "open S" @@ -7175,7 +7177,7 @@ and [simp]: "f a = deriv g a" "g a = 0" shows "f holomorphic_on S" using pole_theorem [OF holg a eq] - by (rule holomorphic_transform) (auto simp: eq divide_simps) + by (rule holomorphic_transform) (auto simp: eq field_split_simps) lemma pole_theorem_open_0: assumes holg: "g holomorphic_on S" and S: "open S" @@ -7183,7 +7185,7 @@ and [simp]: "f a = deriv g a" "g a = 0" shows "f holomorphic_on S" using pole_theorem_open [OF holg S eq] - by (rule holomorphic_transform) (auto simp: eq divide_simps) + by (rule holomorphic_transform) (auto simp: eq field_split_simps) lemma pole_theorem_analytic: assumes g: "g analytic_on S" @@ -7379,7 +7381,7 @@ then have "((\x. f z * (1 / (x - z))) has_contour_integral 0) \" using has_contour_integral_lmul by fastforce then have "((\x. f z / (x - z)) has_contour_integral 0) \" - by (simp add: divide_simps) + by (simp add: field_split_simps) moreover have "((\x. (f x - f z) / (x - z)) has_contour_integral contour_integral \ (d z)) \" using z apply (auto simp: v_def) @@ -7467,7 +7469,7 @@ apply (rule mult_mono) using that D interior_subset apply blast using \L>0\ \e>0\ \D>0\ DL2 - apply (auto simp: norm_divide divide_simps algebra_simps) + apply (auto simp: norm_divide field_split_simps algebra_simps) done finally show ?thesis . qed @@ -7701,7 +7703,7 @@ then have "((\w. f z * (1 / (w - z))) has_contour_integral complex_of_real (2 * pi) * \ * winding_number \ z * f z) \" by (metis mult.commute has_contour_integral_lmul) then have 1: "((\w. f z / (w - z)) has_contour_integral complex_of_real (2 * pi) * \ * winding_number \ z * f z) \" - by (simp add: divide_simps) + by (simp add: field_split_simps) moreover have 2: "((\w. (f w - f z) / (w - z)) has_contour_integral 0) \" using U [OF z] pasz d_def by (force elim: has_contour_integral_eq [where g = "\w. (f w - f z)/(w - z)"]) show ?thesis diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed Oct 09 14:51:54 2019 +0000 @@ -540,9 +540,9 @@ then have "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) = norm (f' x (y - x) /\<^sub>R r - (f y - f x) /\<^sub>R r)" by (simp add: dist_norm) also have "\ = norm (f' x (y - x) - (f y - f x)) / r" - using \r > 0\ by (simp add: scale_right_diff_distrib [symmetric] divide_simps) + using \r > 0\ by (simp add: divide_simps scale_right_diff_distrib [symmetric]) also have "\ \ norm (f y - (f x + f' x (y - x))) / norm (y - x)" - using that \r > 0\ False by (simp add: algebra_simps divide_simps dist_norm norm_minus_commute mult_right_mono) + using that \r > 0\ False by (simp add: algebra_simps field_split_simps dist_norm norm_minus_commute mult_right_mono) also have "\ < k" using that \0 < \\ by (simp add: dist_commute r_def \ [OF \y \ S\ False]) finally show "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) < k" . @@ -883,7 +883,7 @@ with ml have 0: "0 < - (m - ?\ (f ` S))/2 / ?\ S" using that zero_less_measure_iff by force then show ?thesis - using * [OF 0] that by (auto simp: divide_simps m_def split: if_split_asm) + using * [OF 0] that by (auto simp: field_split_simps m_def split: if_split_asm) qed then show "?\ (f ` S) \ integral S (\x. \det (matrix (f' x))\)" by fastforce @@ -991,7 +991,7 @@ fix k::real assume "k \ \" and k: "\k\ \ 2 ^ (2*n)" show "0 \ k/2^n * ?\ n k x" - using f \k \ \\ apply (auto simp: indicator_def divide_simps Ints_def) + using f \k \ \\ apply (auto simp: indicator_def field_split_simps Ints_def) apply (drule spec [where x=x]) using zero_le_power [of "2::real" n] mult_nonneg_nonneg [of "f x" "2^n"] by linarith @@ -1002,7 +1002,7 @@ (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * (indicator {y. k/2^n \ f y \ f y < (k+1/2)/2^n} x + indicator {y. (k+1/2)/2^n \ f y \ f y < (k+1)/2^n} x))" - by (rule sum.cong [OF refl]) (simp add: indicator_def divide_simps) + by (rule sum.cong [OF refl]) (simp add: indicator_def field_split_simps) also have "\ = (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * indicator {y. k/2^n \ f y \ f y < (k+1/2)/2^n} x) + (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n \ f y \ f y < (k+1)/2^n} x)" by (simp add: comm_monoid_add_class.sum.distrib algebra_simps) @@ -1021,7 +1021,7 @@ show "(\k | k \ \ \ \k\ \ 2 ^ (2*n). 2 * k/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \ f y \ f y < (2 * k+1 + 1)/2 ^ Suc n} x) \ sum ?h {k \ \. \k\ \ 2 ^ (2*n)}" - by (rule sum_mono) (simp add: indicator_def divide_simps) + by (rule sum_mono) (simp add: indicator_def field_split_simps) next have \: "?a = (\k \ (*)2 ` {k \ \. \k\ \ 2 ^ (2*n)}. k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x)" @@ -1183,7 +1183,7 @@ ultimately have lim_dl: "((\x. (\d \ x\ - k)) \ (?\ \ \)) \ (\d \ l\ - k)" by (meson continuous_imp_tendsto) have "\\<^sub>F i in sequentially. 0 \ ((\x. \d \ x\ - k) \ ((\n. \ n /\<^sub>R norm (\ n)) \ \)) i" - using \ kd by (auto simp: divide_simps) + using \ kd by (auto simp: field_split_simps) then have "k \ \d \ l\" using tendsto_lowerbound [OF lim_dl, of 0] by auto moreover have "d \ l = 0" @@ -1606,7 +1606,7 @@ also have "\ = norm ((A i - A j) *v (\ p - x)) / norm (\ p - x)" by (simp add: divide_inverse matrix_vector_mult_scaleR) also have "\ \ 2 / N" - using no_le by (auto simp: divide_simps) + using no_le by (auto simp: field_split_simps) finally show "norm (?V i p - ?V j p) \ 2 / N" . qed have "isCont (\w. (norm(A i *v w - A j *v w) - 2 / N)) z" @@ -1652,7 +1652,7 @@ show "linear ((*v) (matrix (f' x) - B))" by (rule matrix_vector_mul_linear) have "((\y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \ 0) (at x within S)" - using tendsto_minus [OF lim_df] by (simp add: algebra_simps divide_simps) + using tendsto_minus [OF lim_df] by (simp add: algebra_simps field_split_simps) then show "((\y. (matrix (f' x) - B) *v (y - x) /\<^sub>R norm (y - x)) \ 0) (at x within S)" proof (rule Lim_transform) have "((\y. ((f y + B *v x - (f x + B *v y)) /\<^sub>R norm (y - x))) \ 0) (at x within S)" @@ -1704,7 +1704,7 @@ also have "\ \ (e - 1 / (Suc (p + q))) * norm (y - x)" proof (rule mult_right_mono) have "1 / Suc (p + q) \ 1 / q" - using \q \ 0\ by (auto simp: divide_simps) + using \q \ 0\ by (auto simp: field_split_simps) also have "\ < e/2" using qe2 by auto finally show "e / 2 \ e - 1 / real (Suc (p + q))" @@ -1714,7 +1714,7 @@ by (simp add: algebra_simps) qed then show "inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e" - using \y \ x\ by (simp add: divide_simps algebra_simps) + using \y \ x\ by (simp add: field_split_simps algebra_simps) qed qed then show "((\y. (matrix (f' x) - B) *v (y - x) /\<^sub>R @@ -1784,7 +1784,7 @@ by (rule Bo_e6) finally have "norm ((?A - B) *v (y - x)) / norm (y - x) < e / 6" . then show "norm ((?A - B) *v (y - x)) \ e * norm (y - x) / 6" - by (simp add: divide_simps False) + by (simp add: field_split_simps False) have "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) = norm ((\ i j. if i = m \ j = n then e / 4 else 0) *v (y - x))" by (simp add: algebra_simps) also have "\ = norm((e/4) *\<^sub>R (y - x)$n *\<^sub>R axis m (1::real))" @@ -2192,7 +2192,7 @@ finally show ?thesis . qed finally have *: "1 / real (?m ^ ?m) * norm (v - u) ^ ?n \ ?\ K" - by (simp add: divide_simps) + by (simp add: field_split_simps) show ?thesis using mult_left_mono [OF *, of "e / (2*c) ^ ?m"] \c > 0\ \e > 0\ by auto qed @@ -2235,7 +2235,7 @@ using \c > 0\ by (simp add: content_cbox_if_cart) finally have "sum ?\ \ \ (2 ^ ?m * c ^ ?m)" . then show ?thesis - using \e > 0\ \c > 0\ by (auto simp: divide_simps mult_less_0_iff) + using \e > 0\ \c > 0\ by (auto simp: field_split_simps mult_less_0_iff) qed finally show ?thesis . qed @@ -2362,7 +2362,7 @@ show "norm (if x \ {t. h n (g t) = y} then ?D x else 0) \ ?D x *\<^sub>R f (g x) /\<^sub>R y" if "x \ S" for x using nonneg_h [of n x] \y > 0\ nonneg_fg [of x] h_le_f [of x n] that - by (auto simp: divide_simps ordered_semiring_class.mult_left_mono) + by (auto simp: divide_simps mult_left_mono) qed (use S in auto) then have int_det: "(\t. \det (matrix (g' t))\) integrable_on ({t. h n (g t) = y} \ S)" using integrable_restrict_Int by force diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed Oct 09 14:51:54 2019 +0000 @@ -401,13 +401,13 @@ "\f field_differentiable at z; f z \ 0\ \ deriv (\w. inverse (f w)) z = - deriv f z / f z ^ 2" unfolding DERIV_deriv_iff_field_differentiable[symmetric] - by (safe intro!: DERIV_imp_deriv derivative_eq_intros) (auto simp: divide_simps power2_eq_square) + by (safe intro!: DERIV_imp_deriv derivative_eq_intros) (auto simp: field_split_simps power2_eq_square) lemma deriv_divide [simp]: "\f field_differentiable at z; g field_differentiable at z; g z \ 0\ \ deriv (\w. f w / g w) z = (deriv f z * g z - f z * deriv g z) / g z ^ 2" by (simp add: field_class.field_divide_inverse field_differentiable_inverse) - (simp add: divide_simps power2_eq_square) + (simp add: field_split_simps power2_eq_square) lemma deriv_cdivide_right: "f field_differentiable at z \ deriv (\w. f w / c) z = deriv f z / c" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Wed Oct 09 14:51:54 2019 +0000 @@ -332,11 +332,11 @@ proof - have "cos (\ j - \) = ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)" for j apply (subst cmod_diff_squared) - using assms by (auto simp: divide_simps less_le) + using assms by (auto simp: field_split_simps less_le) moreover have "(\j. ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)) \ ((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R))" by (intro L rR tendsto_intros) (use \R > 0\ in force) moreover have "((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R)) = 1" - using \R > 0\ by (simp add: power2_eq_square divide_simps) + using \R > 0\ by (simp add: power2_eq_square field_split_simps) ultimately have "(\j. cos (\ j - \)) \ 1" by auto then show ?thesis @@ -582,7 +582,7 @@ lemma sinh_complex: fixes z :: complex shows "(exp z - inverse (exp z)) / 2 = -\ * sin(\ * z)" - by (simp add: sin_exp_eq divide_simps exp_minus) + by (simp add: sin_exp_eq field_split_simps exp_minus) lemma sin_i_times: fixes z :: complex @@ -597,12 +597,12 @@ lemma cosh_complex: fixes z :: complex shows "(exp z + inverse (exp z)) / 2 = cos(\ * z)" - by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real) + by (simp add: cos_exp_eq field_split_simps exp_minus exp_of_real) lemma cosh_real: fixes x :: real shows "of_real((exp x + inverse (exp x)) / 2) = cos(\ * of_real x)" - by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real) + by (simp add: cos_exp_eq field_split_simps exp_minus exp_of_real) lemmas cos_i_times = cosh_complex [symmetric] @@ -612,7 +612,7 @@ apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq) apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide) apply (simp only: left_diff_distrib [symmetric] power_mult_distrib sin_squared_eq) - apply (simp add: power2_eq_square algebra_simps divide_simps) + apply (simp add: power2_eq_square algebra_simps field_split_simps) done lemma norm_sin_squared: @@ -621,7 +621,7 @@ apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq) apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide) apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq) - apply (simp add: power2_eq_square algebra_simps divide_simps) + apply (simp add: power2_eq_square algebra_simps field_split_simps) done lemma exp_uminus_Im: "exp (- Im z) \ exp (cmod z)" @@ -928,7 +928,7 @@ unfolding is_Arg_def apply (rule complex_eqI) using t False ReIm - apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps) + apply (auto simp: exp_Euler sin_of_real cos_of_real field_split_simps) done show ?thesis apply (simp add: Arg2pi_def False) @@ -1055,7 +1055,7 @@ using assms Arg2pi_eq [of z] Arg2pi_eq [of w] apply auto apply (rule_tac x="norm w / norm z" in exI) - apply (simp add: divide_simps) + apply (simp add: field_split_simps) by (metis mult.commute mult.left_commute) lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \ Arg2pi z = 0" @@ -1102,7 +1102,7 @@ by auto lemma Arg2pi_cnj_eq_inverse: "z\0 \ Arg2pi (cnj z) = Arg2pi (inverse z)" - apply (simp add: Arg2pi_eq_iff divide_simps complex_norm_square [symmetric] mult.commute) + apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric] mult.commute) by (metis of_real_power zero_less_norm_iff zero_less_power) lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \ \ then Arg2pi z else 2*pi - Arg2pi z)" @@ -1166,10 +1166,10 @@ proof - obtain \ where z: "z / (cmod z) = Complex (cos \) (sin \)" using complex_unimodular_polar [of "z / (norm z)"] assms - by (auto simp: norm_divide divide_simps) + by (auto simp: norm_divide field_split_simps) obtain \ where \: "- pi < \" "\ \ pi" "sin \ = sin \" "cos \ = cos \" using sincos_principal_value [of "\"] assms - by (auto simp: norm_divide divide_simps) + by (auto simp: norm_divide field_split_simps) have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \ pi" unfolding ln_complex_def apply (rule theI [where a = "Complex (ln(norm z)) \"]) using z assms \ @@ -1437,7 +1437,7 @@ by (intro summable_norm) (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc) also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \ norm ((-z)^2 * (-z)^i) * 1" for i - by (intro mult_left_mono) (simp_all add: divide_simps) + by (intro mult_left_mono) (simp_all add: field_split_simps) hence "(\i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i)) \ (\i. norm (-(z^2) * (-z)^i))" using A assms @@ -1907,14 +1907,14 @@ using assms Arg_eq [of z] Arg_eq [of w] apply auto apply (rule_tac x="norm w / norm z" in exI) - apply (simp add: divide_simps) + apply (simp add: field_split_simps) by (metis mult.commute mult.left_commute) lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \ Arg z = 0" by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq) lemma Arg_cnj_eq_inverse: "z\0 \ Arg (cnj z) = Arg (inverse z)" - apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute) + apply (simp add: Arg_eq_iff field_split_simps complex_norm_square [symmetric] mult.commute) by (metis of_real_power zero_less_norm_iff zero_less_power) lemma Arg_cnj: "Arg(cnj z) = (if z \ \ then Arg z else - Arg z)" @@ -2307,7 +2307,7 @@ by auto then show ?thesis unfolding dd'_def using gderiv that \g z\0\ - by (auto intro!: derivative_eq_intros simp add:divide_simps power_add[symmetric]) + by (auto intro!: derivative_eq_intros simp add:field_split_simps power_add[symmetric]) qed finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)" . then show ?thesis unfolding dd_def by simp @@ -2549,7 +2549,7 @@ using e by (auto simp: field_simps) have "norm (Ln (of_nat n) / of_nat n powr s) < e" if "n \ nat \exp xo\" for n using e xo [of "ln n"] that - apply (auto simp: norm_divide norm_powr_real divide_simps) + apply (auto simp: norm_divide norm_powr_real field_split_simps) apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff) done then show "\no. \n\no. norm (Ln (of_nat n) / of_nat n powr s) < e" @@ -2593,7 +2593,7 @@ using ln_272_gt_1 by (force intro: order_trans [of _ "ln (272/100)"]) then show "\\<^sub>F x in sequentially. cmod (1 / of_nat x powr s) \ cmod (Ln (of_nat x) / of_nat x powr s)" - by (auto simp: norm_divide divide_simps eventually_sequentially) + by (auto simp: norm_divide field_split_simps eventually_sequentially) show "(\n. cmod (Ln (of_nat n) / of_nat n powr s)) \ 0" using lim_Ln_over_power [OF assms] by (metis tendsto_norm_zero_iff) qed @@ -2609,7 +2609,7 @@ done lemma lim_1_over_Ln: "((\n. 1 / Ln(of_nat n)) \ 0) sequentially" -proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps) +proof (clarsimp simp add: lim_sequentially dist_norm norm_divide field_split_simps) fix r::real assume "0 < r" have ir: "inverse (exp (inverse r)) > 0" @@ -2618,7 +2618,7 @@ using ex_less_of_nat_mult [of _ 1, OF ir] by auto then have "exp (inverse r) < of_nat n" - by (simp add: divide_simps) + by (simp add: field_split_simps) then have "ln (exp (inverse r)) < ln (of_nat n)" by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff) with \0 < r\ have "1 < r * ln (real_of_nat n)" @@ -2627,7 +2627,7 @@ using neq0_conv by fastforce ultimately show "\no. \k. Ln (of_nat k) \ 0 \ no \ k \ 1 < r * cmod (Ln (of_nat k))" using n \0 < r\ - by (rule_tac x=n in exI) (force simp: divide_simps intro: less_le_trans) + by (rule_tac x=n in exI) (force simp: field_split_simps intro: less_le_trans) qed lemma lim_1_over_ln: "((\n. 1 / ln(real_of_nat n)) \ 0) sequentially" @@ -2650,7 +2650,7 @@ then have "ln 3 \ ln n" and ln0: "0 \ ln n" by auto with ln3_gt_1 have "1/ ln n \ 1" - by (simp add: divide_simps) + by (simp add: field_split_simps) moreover have "ln (1 + 1 / real n) \ 1/n" by (simp add: ln_add_one_self_le_self) ultimately have "ln (1 + 1 / real n) * (1 / ln n) \ (1/n) * 1" @@ -2662,7 +2662,7 @@ then show "(\n. 1 + ln(1 + 1/n) / ln n) \ 1" by (metis (full_types) add.right_neutral tendsto_add_const_iff) show "\\<^sub>F k in sequentially. 1 + ln (1 + 1 / k) / ln k = ln(Suc k) / ln k" - by (simp add: divide_simps ln_div eventually_sequentiallyI [of 2]) + by (simp add: field_split_simps ln_div eventually_sequentiallyI [of 2]) qed lemma lim_ln_over_ln1: "(\n. ln n / ln(Suc n)) \ 1" @@ -2721,7 +2721,7 @@ have z: "z \ 0" using assms by auto then have *: "inverse z = inverse (2*z) * 2" - by (simp add: divide_simps) + by (simp add: field_split_simps) have [simp]: "exp (Ln z / 2) * inverse z = inverse (csqrt z)" by (simp add: z field_simps csqrt_exp_Ln [symmetric]) (metis power2_csqrt power2_eq_square) have "Im z = 0 \ 0 < Re z" @@ -2904,7 +2904,7 @@ unfolding Arctan_def scaleR_conv_of_real apply (intro derivative_eq_intros | simp add: nz0 *)+ using nz0 nz1 zz - apply (simp add: algebra_simps divide_simps power2_eq_square) + apply (simp add: algebra_simps field_split_simps power2_eq_square) apply algebra done qed @@ -2954,12 +2954,12 @@ have "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) * ereal (((2*Suc n+1) / (Suc n)) / ((2*Suc n-1) / (Suc n)))" - by (simp add: h_def norm_mult norm_power norm_divide divide_simps + by (simp add: h_def norm_mult norm_power norm_divide field_split_simps power2_eq_square eval_nat_numeral del: of_nat_add of_nat_Suc) also have "of_nat (2*Suc n+1) / of_nat (Suc n) = (2::real) + inverse (real (Suc n))" - by (auto simp: divide_simps simp del: of_nat_Suc) simp_all? + by (auto simp: field_split_simps simp del: of_nat_Suc) simp_all? also have "of_nat (2*Suc n-1) / of_nat (Suc n) = (2::real) - inverse (real (Suc n))" - by (auto simp: divide_simps simp del: of_nat_Suc) simp_all? + by (auto simp: field_split_simps simp del: of_nat_Suc) simp_all? finally show "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) * ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n))))" . qed @@ -2968,7 +2968,7 @@ finally have "liminf (\n. ereal (cmod (h u n) / cmod (h u (Suc n)))) = inverse (norm u)^2" by (intro lim_imp_Liminf) simp_all moreover from power_strict_mono[OF that, of 2] u have "inverse (norm u)^2 > 1" - by (simp add: divide_simps) + by (simp add: field_split_simps) ultimately have A: "liminf (\n. ereal (cmod (h u n) / cmod (h u (Suc n)))) > 1" by simp from u have "summable (h u)" by (intro summable_norm_cancel[OF ratio_test_convergence[OF _ A]]) @@ -3049,7 +3049,7 @@ apply (rule norm_exp_imaginary) apply (subst exp_Ln) using ne apply (simp_all add: cmod_def complex_eq_iff) - apply (auto simp: divide_simps) + apply (auto simp: field_split_simps) apply algebra done then show ?thesis @@ -3065,7 +3065,7 @@ done next have *: " (1 - \*x) / (1 + \*x) \ 0" - by (simp add: divide_simps) ( simp add: complex_eq_iff) + by (simp add: field_split_simps) ( simp add: complex_eq_iff) show "Re (Arctan (complex_of_real x)) < pi / 2" using mpi_less_Im_Ln [OF *] by (simp add: Arctan_def) @@ -3143,7 +3143,7 @@ case False then have *: "\arctan x\ < pi / 2 - \arctan y\" using assms apply (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff) - apply (simp add: divide_simps abs_mult) + apply (simp add: field_split_simps abs_mult) done show ?thesis apply (rule arctan_add_raw) @@ -3192,7 +3192,7 @@ have nonneg: "0 \ ?a n" for n by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms) have le: "?a (Suc n) \ ?a n" for n - by (rule mult_mono[OF _ power_decreasing]) (auto simp: divide_simps assms less_imp_le) + by (rule mult_mono[OF _ power_decreasing]) (auto simp: field_split_simps assms less_imp_le) from summable_Leibniz'(4)[of ?a, OF tendsto_zero nonneg le, of n] summable_Leibniz'(2)[of ?a, OF tendsto_zero nonneg le, of n] assms @@ -3565,7 +3565,7 @@ have "(Im (Arccos w))\<^sup>2 \ (cmod (cos (Arccos w)))\<^sup>2 - (cos (Re (Arccos w)))\<^sup>2" using norm_cos_squared [of "Arccos w"] real_le_abs_sinh [of "Im (Arccos w)"] apply (simp only: abs_le_square_iff) - apply (simp add: divide_simps) + apply (simp add: field_split_simps) done also have "... \ (cmod w)\<^sup>2" by (auto simp: cmod_power2) @@ -3974,7 +3974,7 @@ note * = this show ?thesis using assms - by (simp add: exp_eq divide_simps mult_ac of_real_numeral *) + by (simp add: exp_eq field_split_simps mult_ac of_real_numeral *) qed corollary bij_betw_roots_unity: @@ -4059,7 +4059,7 @@ then h (fst z, Arg2pi (snd z) / (2 * pi)) else h (fst z, 1 - Arg2pi (cnj (snd z)) / (2 * pi))" have Arg2pi_eq: "1 - Arg2pi (cnj y) / (2 * pi) = Arg2pi y / (2 * pi) \ Arg2pi y = 0 \ Arg2pi (cnj y) = 0" if "cmod y = 1" for y - using that Arg2pi_eq_0_pi Arg2pi_eq_pi by (force simp: Arg2pi_cnj divide_simps) + using that Arg2pi_eq_0_pi Arg2pi_eq_pi by (force simp: Arg2pi_cnj field_split_simps) show ?thesis proof (simp add: homotopic_with; intro conjI ballI exI) show "continuous_on ({0..1} \ sphere 0 1) (\w. h (fst w, Arg2pi (snd w) / (2 * pi)))" @@ -4250,7 +4250,7 @@ next case False then have *: "(Arg2pi (exp (\*(2* of_real pi* of_real x))) / (2*pi)) = x" - using that by (auto simp: Arg2pi_exp divide_simps) + using that by (auto simp: Arg2pi_exp field_split_simps) show ?thesis by (rule_tac x="exp(\ * of_real(2*pi*x))" in bexI) (auto simp: *) qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Wed Oct 09 14:51:54 2019 +0000 @@ -39,7 +39,7 @@ define a where "a = (2 * pi)/(fact n)" have "0 < a" by (simp add: a_def) have "B0/r^(Suc n)*2 * pi * r = a*((fact n)*B0/r^n)" - using \0 < r\ by (simp add: a_def divide_simps) + using \0 < r\ by (simp add: a_def field_split_simps) have der_dif: "(deriv ^^ n) (\w. f w - y) z = (deriv ^^ n) f z" using \0 < r\ \0 < n\ by (auto simp: higher_deriv_diff [OF holf holomorphic_on_const]) @@ -123,7 +123,7 @@ then have wge: "fact k * B / cmod ((deriv ^^ k) f 0) < norm w" by (metis norm_of_real w_def) then have "fact k * B / norm w < cmod ((deriv ^^ k) f 0)" - using False by (simp add: divide_simps mult.commute split: if_split_asm) + using False by (simp add: field_split_simps mult.commute split: if_split_asm) also have "... \ fact k * (B * norm w ^ n) / norm w ^ k" apply (rule Cauchy_inequality) using holf holomorphic_on_subset apply force @@ -132,7 +132,7 @@ by (metis nof wgeA dist_0_norm dist_norm) also have "... = fact k * (B * 1 / cmod w ^ (k-n))" apply (simp only: mult_cancel_left times_divide_eq_right [symmetric]) - using \k>n\ \w \ 0\ \0 < B\ apply (simp add: divide_simps semiring_normalization_rules) + using \k>n\ \w \ 0\ \0 < B\ apply (simp add: field_split_simps semiring_normalization_rules) done also have "... = fact k * B / cmod w ^ (k-n)" by simp @@ -862,7 +862,7 @@ have h0: "(h has_field_derivative 0) (at \)" apply (simp add: h_def has_field_derivative_iff) apply (rule Lim_transform_within [OF that, of 1]) - apply (auto simp: divide_simps power2_eq_square) + apply (auto simp: field_split_simps power2_eq_square) done have holh: "h holomorphic_on S" proof (simp add: holomorphic_on_def, clarify) @@ -952,7 +952,7 @@ have "cmod (f z) \ cmod z ^ n / B" if "2/e \ cmod z" for z proof - have ize: "inverse z \ ball 0 e - {0}" using that \0 < e\ - by (auto simp: norm_divide divide_simps algebra_simps) + by (auto simp: norm_divide field_split_simps algebra_simps) then have [simp]: "z \ 0" and izr: "inverse z \ ball 0 r - {0}" using \e \ r\ by auto then have [simp]: "f z \ 0" @@ -960,7 +960,7 @@ have [simp]: "f z = inverse (g (inverse z))" using izr geq [of "inverse z"] by simp show ?thesis using ize leg [of "inverse z"] \0 < B\ \0 < e\ - by (simp add: divide_simps norm_divide algebra_simps) + by (simp add: field_split_simps norm_divide algebra_simps) qed then show ?thesis apply (rule_tac a = "\k. (deriv ^^ k) f 0 / (fact k)" and n=n in that) @@ -1852,7 +1852,7 @@ apply (rule Le1) using r x \0 < r\ by simp also have "... \ norm (x *\<^sub>R z) / (r - norm z) * C" using r x \0 < r\ - apply (simp add: divide_simps) + apply (simp add: field_split_simps) by (simp add: \0 < C\ mult.assoc mult_left_le_one_le ordered_comm_semiring_class.comm_mult_left_mono) finally have "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \ norm (x *\<^sub>R z) / (r - norm z) * C * norm z" by (rule mult_right_mono) simp @@ -1994,7 +1994,7 @@ then have "norm (deriv f y) * abs (r - norm (y - a)) \ norm (deriv f p) * abs (r - norm (p - a))" by (simp only: dist_norm g_def norm_mult norm_of_real) with that \norm (p - a) < r\ show ?thesis - by (simp add: dist_norm divide_simps) + by (simp add: dist_norm field_split_simps) qed have le_norm_dfp: "r / (r - norm (p - a)) \ norm (deriv f p)" using gen_le_dfp [of a] \r > 0\ by auto @@ -3044,7 +3044,7 @@ by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"] filterlim_compose[OF filterlim_inverse_at_infinity])+ (insert assms, auto simp: isCont_def) - thus ?thesis by (simp add: divide_simps is_pole_def) + thus ?thesis by (simp add: field_split_simps is_pole_def) qed lemma is_pole_basic: @@ -3526,7 +3526,7 @@ apply (elim filterlim_transform_within[OF _ _ \r1>0\],simp) apply (subst fg_times,simp add:dist_commute) apply (subst powr_of_int) - using that by (auto simp add:divide_simps) + using that by (auto simp add:field_split_simps) then show ?thesis unfolding not_essential_def fg_def by auto qed ultimately show ?thesis unfolding not_essential_def fg_def by fastforce @@ -4573,7 +4573,7 @@ have "eventually (\w. w \ z) (at z)" by (auto simp: eventually_at_filter) hence "eventually (\w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z)) = f w / g w) (at z)" - by eventually_elim (simp add: assms divide_simps) + by eventually_elim (simp add: assms field_split_simps) moreover have "((\w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) \ f' / g') (at z)" by (intro tendsto_divide has_field_derivativeD assms) ultimately have "((\w. f w / g w) \ f' / g') (at z)" @@ -4654,7 +4654,7 @@ show "(g has_field_derivative g') (at z)" by fact qed (insert assms, auto) then show "((\w. (f w / g w) * (w - z)) \ f z / g') (at z)" - by (simp add: divide_simps) + by (simp add: field_split_simps) qed qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Continuous_Extension.thy --- a/src/HOL/Analysis/Continuous_Extension.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Continuous_Extension.thy Wed Oct 09 14:51:54 2019 +0000 @@ -91,7 +91,7 @@ done qed moreover have "\U \ \; x \ S\ \ 0 \ F U x" for U x - using nonneg [of x] by (simp add: F_def divide_simps setdist_pos_le) + using nonneg [of x] by (simp add: F_def field_split_simps setdist_pos_le) ultimately show "\U. U \ \ \ continuous_on S (F U) \ (\x\S. 0 \ F U x)" by metis next @@ -100,7 +100,7 @@ next show "supp_sum (\W. F W x) \ = 1" if "x \ S" for x using that ss_pos [OF that] - by (simp add: F_def divide_simps supp_sum_divide_distrib [symmetric]) + by (simp add: F_def field_split_simps supp_sum_divide_distrib [symmetric]) next show "\V. open V \ x \ V \ finite {U \ \. \x\V. F U x \ 0}" if "x \ S" for x using fin [OF that] that @@ -157,7 +157,7 @@ done also have "... \ setdist {x} T = 0 \ setdist {x} S \ 0" using sdpos that - by (simp add: divide_simps) linarith + by (simp add: field_split_simps) linarith also have "... \ x \ T" using \S \ {}\ \T \ {}\ \S \ T = {}\ that by (force simp: S0 T0) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Convex.thy --- a/src/HOL/Analysis/Convex.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Convex.thy Wed Oct 09 14:51:54 2019 +0000 @@ -988,7 +988,7 @@ assume "u \ {0<..}" "v \ {0<..}" "u \ v" with assms show "-inverse (u^2) \ -inverse (v^2)" by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all) -qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square) +qed (insert assms, auto intro!: derivative_eq_intros simp: field_split_simps power2_eq_square) lemma convex_onD_Icc': assumes "convex_on {x..y} f" "c \ {x..y}" @@ -999,7 +999,7 @@ then have d: "d > 0" by (simp add: d_def) from assms(2) less have A: "0 \ (c - x) / d" "(c - x) / d \ 1" - by (simp_all add: d_def divide_simps) + by (simp_all add: d_def field_split_simps) have "f c = f (x + (c - x) * 1)" by simp also from less have "1 = ((y - x) / d)" @@ -1022,7 +1022,7 @@ then have d: "d > 0" by (simp add: d_def) from assms(2) less have A: "0 \ (y - c) / d" "(y - c) / d \ 1" - by (simp_all add: d_def divide_simps) + by (simp_all add: d_def field_split_simps) have "f c = f (y - (y - c) * 1)" by simp also from less have "1 = ((y - x) / d)" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1602,7 +1602,7 @@ by simp also have "\ < norm(x - closest_point S x)" using clo_notx \e > 0\ - by (auto simp: mult_less_cancel_right2 divide_simps) + by (auto simp: mult_less_cancel_right2 field_split_simps) finally have no_less: "norm (x - y) < norm (x - closest_point S x)" . have "y \ affine hull S" unfolding y_def @@ -2394,7 +2394,7 @@ using \0 < t\ \2 < t\ and \y \ S\ \w \ S\ by (auto simp:field_simps) also have "\ = (f w + t * f y) / (1 + t)" - using \t > 0\ by (auto simp: divide_simps) + using \t > 0\ by (simp add: add_divide_distrib) also have "\ < e + f y" using \t > 0\ * \e > 0\ by (auto simp: field_simps) finally have "f x - f y < e" by auto @@ -2504,7 +2504,7 @@ have "e \ e * real DIM('a)" using e(2) real_of_nat_ge_one_iff by auto then have "d \ e" - by (simp add: d_def divide_simps) + by (simp add: d_def field_split_simps) then have dsube: "cball x d \ cball x e" by (rule subset_cball) have conv: "convex_on (cball x d) f" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Derivative.thy Wed Oct 09 14:51:54 2019 +0000 @@ -2111,7 +2111,10 @@ let ?e = "\i x. (inverse (1 + real i) * inverse (fact i) * (x - t) ^ i) *\<^sub>R (A * A ^ i)" have "\\<^sub>F n in sequentially. \x\T \ {t - 1<.. norm (A ^ (n + 1) /\<^sub>R fact (n + 1))" - by (auto simp: divide_simps power_abs intro!: mult_left_le_one_le power_le_one eventuallyI) + apply (auto simp: algebra_split_simps intro!: eventuallyI) + apply (rule mult_left_mono) + apply (auto simp add: field_simps power_abs intro!: divide_right_mono power_le_one) + done then have "uniform_limit (T \ {t - 1<..n x. \ix. \i. ?e i x) sequentially" by (rule Weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp) moreover @@ -2156,7 +2159,7 @@ also have "(\ - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t) = (x - t) *\<^sub>R ((\n. ?e n x) - A) /\<^sub>R norm (x - t)" by (simp add: algebra_simps) finally show ?case - by (simp add: divide_simps) + by simp (simp add: field_simps) qed ultimately have "((\y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \ 0) (at t within T)" @@ -2165,7 +2168,7 @@ show "((\y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \ 0) (at t within T)" by (rule Lim_transform_eventually) - (auto simp: algebra_simps divide_simps exp_add_commuting[symmetric]) + (auto simp: algebra_simps field_split_simps exp_add_commuting[symmetric]) qed (rule bounded_linear_scaleR_left) lemma exp_times_scaleR_commute: "exp (t *\<^sub>R A) * A = A * exp (t *\<^sub>R A)" @@ -2262,7 +2265,7 @@ using interior_subset[of A] by (intro convex_onD_Icc' convex_on_subset[OF convex] connected_contains_Icc) auto hence "f y - f c \ (f x - f c) / (x - c) * (y - c)" by simp - thus "(f y - f c) / (y - c) \ (f x - f c) / (x - c)" using y xc by (simp add: divide_simps) + thus "(f y - f c) / (y - c) \ (f x - f c) / (x - c)" using y xc by (simp add: field_split_simps) qed hence "eventually (\y. (f y - f c) / (y - c) \ (f x - f c) / (x - c)) (at c within ?A')" by (blast intro: filter_leD at_le) @@ -2286,7 +2289,7 @@ hence "f y - f c \ (f x - f c) * ((c - y) / (c - x))" by simp also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps) finally show "(f y - f c) / (y - c) \ (f x - f c) / (x - c)" using y xc - by (simp add: divide_simps) + by (simp add: field_split_simps) qed hence "eventually (\y. (f y - f c) / (y - c) \ (f x - f c) / (x - c)) (at c within ?A')" by (blast intro: filter_leD at_le) @@ -2418,8 +2421,8 @@ let ?le = "\x'. norm (f x' y - f x y - (fx) (x' - x)) \ norm (x' - x) * e" from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \0 < e\] have "\\<^sub>F x' in at x within X. ?le x'" - by eventually_elim - (simp add: dist_norm divide_simps diff_diff_add ac_simps split: if_split_asm) + by eventually_elim (simp, + simp add: dist_norm field_split_simps split: if_split_asm) then have "\\<^sub>F (x', y') in at (x, y) within X \ Y. ?le x'" by (rule eventually_at_Pair_within_TimesI1) (simp add: blinfun.bilinear_simps) @@ -2476,7 +2479,7 @@ using \0 < e'\ nz by (auto simp: e_def) finally show "norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'" - by (auto simp: divide_simps dist_norm mult.commute) + by (simp add: dist_norm) (auto simp add: field_split_simps) qed then show ?case by eventually_elim (auto simp: dist_norm field_simps) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Oct 09 14:51:54 2019 +0000 @@ -210,9 +210,9 @@ lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e" apply (cases "e \ 0") - apply (simp add: ball_empty divide_simps) + apply (simp add: ball_empty field_split_simps) apply (rule subset_ball) - apply (simp add: divide_simps) + apply (simp add: field_split_simps) done lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e" @@ -220,7 +220,7 @@ lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e" apply (cases "e < 0") - apply (simp add: divide_simps) + apply (simp add: field_split_simps) apply (rule subset_cball) apply (metis div_by_1 frac_le not_le order_refl zero_less_one) done @@ -1335,7 +1335,7 @@ then have "diameter(closure(S)) - d / 2 < diameter(closure(S))" by simp have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2" - by (simp add: d_def divide_simps) + by (simp add: d_def field_split_simps) have bocl: "bounded (closure S)" using assms by blast moreover have "0 \ diameter S" @@ -2423,7 +2423,7 @@ then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))" by simp also have "... \ 1 / real (Suc (max N1 N2))" - apply (simp add: divide_simps del: max.bounded_iff) + apply (simp add: field_split_simps del: max.bounded_iff) using \strict_mono r\ seq_suble by blast also have "... \ 1 / real (Suc N2)" by (simp add: field_simps) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Elementary_Normed_Spaces.thy --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Wed Oct 09 14:51:54 2019 +0000 @@ -599,7 +599,7 @@ qed show "\\<^sub>F x in net. dist (f x *\<^sub>R g x) 0 < \" apply (rule eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB] ]) - apply (auto simp: \0 < \\ divide_simps * split: if_split_asm) + apply (auto simp: \0 < \\ field_split_simps * split: if_split_asm) done qed @@ -1562,17 +1562,17 @@ proof have "x \ (\z. z /\<^sub>R (1 - norm z)) ` ball 0 1" for x::'a apply (rule_tac x="x /\<^sub>R (1 + norm x)" in image_eqI) - apply (auto simp: divide_simps) + apply (auto simp: field_split_simps) using norm_ge_zero [of x] apply linarith+ done then show "(\z::'a. z /\<^sub>R (1 - norm z)) ` ?B = ?U" by blast have "x \ range (\z. (1 / (1 + norm z)) *\<^sub>R z)" if "norm x < 1" for x::'a apply (rule_tac x="x /\<^sub>R (1 - norm x)" in image_eqI) - using that apply (auto simp: divide_simps) + using that apply (auto simp: field_split_simps) done then show "(\z::'a. z /\<^sub>R (1 + norm z)) ` ?U = ?B" - by (force simp: divide_simps dest: add_less_zeroD) + by (force simp: field_split_simps dest: add_less_zeroD) show "continuous_on (ball 0 1) (\z. z /\<^sub>R (1 - norm z))" by (rule continuous_intros | force)+ show "continuous_on UNIV (\z. z /\<^sub>R (1 + norm z))" @@ -1581,9 +1581,9 @@ done show "\x. x \ ball 0 1 \ x /\<^sub>R (1 - norm x) /\<^sub>R (1 + norm (x /\<^sub>R (1 - norm x))) = x" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) show "\y. y /\<^sub>R (1 + norm y) /\<^sub>R (1 - norm (y /\<^sub>R (1 + norm y))) = y" - apply (auto simp: divide_simps) + apply (auto simp: field_split_simps) apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one) done qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Oct 09 14:51:54 2019 +0000 @@ -147,7 +147,7 @@ then have "x \ ball (T X k) (1 / (3 * Suc m))" using in_s[OF \(x, k) \ s\] by (auto simp: C_def subset_eq dist_commute) then have "ball x (1 / (3 * Suc m)) \ ball (T X k) (1 / Suc m)" - by (rule ball_trans) (auto simp: divide_simps) + by (rule ball_trans) (auto simp: field_split_simps) with k in_s[OF \(x, k) \ s\] have "k \ d (T X k)" by (auto simp: C_def) } then have "d fine ?p" @@ -1423,7 +1423,7 @@ then have "negligible (cbox ?p ?q)" by (meson \cball a e \ S\ neg negligible_subset) with \e > 0\ show False - by (simp add: negligible_interval box_eq_empty algebra_simps divide_simps mult_le_0_iff) + by (simp add: negligible_interval box_eq_empty algebra_simps field_split_simps mult_le_0_iff) qed lemma negligible_convex_interior: @@ -1661,7 +1661,7 @@ then have "S \ sets lebesgue" by blast have e22: "0 < e/2 / (2 * B * real DIM('M)) ^ DIM('N)" - using \0 < e\ \0 < B\ by (simp add: divide_simps) + using \0 < e\ \0 < B\ by (simp add: field_split_simps) obtain T where "open T" "S \ T" "(T - S) \ lmeasurable" "measure lebesgue (T - S) < e/2 / (2 * B * DIM('M)) ^ DIM('N)" using sets_lebesgue_outer_open [OF \S \ sets lebesgue\ e22] @@ -3040,7 +3040,7 @@ have 1: "cbox a b - S \ lmeasurable" by (simp add: fmeasurable.Diff that) have 2: "0 < e / (1 + \m\)" - using \e > 0\ by (simp add: divide_simps abs_add_one_gt_zero) + using \e > 0\ by (simp add: field_split_simps abs_add_one_gt_zero) obtain \ where "countable \" and cbox: "\K. K \ \ \ K \ cbox a b \ K \ {} \ (\c d. K = cbox c d)" @@ -3075,7 +3075,7 @@ fix e :: real assume "e > 0" have em: "0 < e / (1 + \m\)" - using \e > 0\ by (simp add: divide_simps abs_add_one_gt_zero) + using \e > 0\ by (simp add: field_split_simps abs_add_one_gt_zero) obtain \ where "countable \" and cbox: "\K. K \ \ \ K \ cbox a b \ K \ {} \ (\c d. K = cbox c d)" @@ -3163,7 +3163,7 @@ by (metis (no_types) abs_minus_commute mult.commute right_diff_distrib' mm) qed also have "\ < e" - using \e > 0\ by (auto simp: divide_simps) + using \e > 0\ by (cases "m \ 0") (simp_all add: field_simps) finally have "\?\ (f ` S \ cbox a b) - m * ?\ S\ < e" . with 1 show ?thesis by auto qed @@ -4138,7 +4138,7 @@ show "{m} \ {k \ \. \k\ \ 2 ^ (2*n)}" using assms by auto show "\i\{k \ \. \k\ \ 2 ^ (2*n)} - {m}. ?f i = 0" - using assms by (auto simp: indicator_def Ints_def abs_le_iff divide_simps) + using assms by (auto simp: indicator_def Ints_def abs_le_iff field_split_simps) qed also have "\ = m/2^n" using assms by (auto simp: indicator_def not_less) @@ -4196,7 +4196,7 @@ proof - define m where "m \ floor(2^n * (f x))" have "1 \ \2^n\ * e" - using n N2 \e > 0\ less_eq_real_def less_le_trans by (fastforce simp add: divide_simps) + using n N2 \e > 0\ less_eq_real_def less_le_trans by (fastforce simp add: field_split_simps) then have *: "\x \ y; y < x + 1\ \ abs(x - y) < \2^n\ * e" for x y::real by linarith have "\2^n\ * \m/2^n - f x\ = \2^n * (m/2^n - f x)\" @@ -4243,7 +4243,7 @@ by (metis abs_of_nonneg floor_mono le_floor_iff m_def of_int_0_le_iff power2_eq_square power_mult real_mult_le_cancel_iff1 zero_less_numeral mult.commute zero_less_power) qed then have "?g n x = m/2^n" - by (rule indicator_sum_eq) (auto simp: m_def mult.commute divide_simps) + by (rule indicator_sum_eq) (auto simp add: m_def field_split_simps, linarith) then have "norm (?g n x - f x) = norm (m/2^n - f x)" by simp also have "\ < e" @@ -4779,7 +4779,7 @@ proof - have "1 / real (max i j) < \" using j \j \ 0\ \0 < \\ - by (auto simp: divide_simps max_mult_distrib_left of_nat_max) + by (auto simp: field_split_simps max_mult_distrib_left of_nat_max) then have "norm (y - x) < \" using less by linarith with \ \y \ S\ have le: "norm (f y - f x - f' x (y - x)) \ B * norm (y - x) - norm (y - x)/i" @@ -4789,7 +4789,7 @@ using norm_triangle_ineq3 [of "f - f'" y] by simp show ?thesis apply (rule * [OF le B]) - using \i \ 0\ \j \ 0\ by (simp add: divide_simps max_mult_distrib_left of_nat_max less_max_iff_disj) + using \i \ 0\ \j \ 0\ by (simp add: field_split_simps max_mult_distrib_left of_nat_max less_max_iff_disj) qed with \x \ S\ \i \ 0\ \j \ 0\ show "\n\{0<..}. x \ U n" by (rule_tac x="max i j" in bexI) (auto simp: field_simps U_def less_max_iff_disj) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy --- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Wed Oct 09 14:51:54 2019 +0000 @@ -114,7 +114,7 @@ using \lm less.prems(2) by auto qed then have "measure lebesgue (\\ - cbox a3 b3) / 3 ^ DIM('a) \ measure lebesgue (\ \')" - using \'m by (simp add: divide_simps) + using \'m by (simp add: field_split_simps) then show ?thesis by (simp add: m3 field_simps) qed @@ -129,7 +129,7 @@ qed (simp add: \lm \D \ \\) qed finally show "measure lebesgue (\\) / 3 ^ DIM('a) \ measure lebesgue (\(insert D \'))" - by (simp add: divide_simps) + by (simp add: field_split_simps) qed qed qed @@ -421,7 +421,7 @@ unfolding fine_def \_def using BOX_\ \\ \ \\ \\ \ \\ tag_in_E by blast qed finally show ?thesis - using \\ > 0\ by (auto simp: divide_simps) + using \\ > 0\ by (auto simp: field_split_simps) qed finally show ?thesis . qed @@ -448,7 +448,7 @@ qed ultimately have "measure lebesgue (\\) \ e/2" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) then show "measure lebesgue (\\) \ e" using \ by linarith qed @@ -620,7 +620,7 @@ have no: "norm (y - x) < 1" using that by (auto simp: dist_norm) have le1: "inverse (1 + real n) \ 1" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) have "norm (integral (cbox y (y + One /\<^sub>R real (Suc n))) f - integral (cbox x (x + One /\<^sub>R real (Suc n))) f) < e / (1 + real n) ^ DIM('a)" @@ -742,7 +742,7 @@ show "continuous_on UNIV (g \ (\ n))" for n :: nat unfolding \_def apply (intro continuous_on_compose2 [OF contg] continuous_intros conth) - apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj algebra_simps divide_simps) + apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj algebra_simps field_split_simps) done show "(\n. (g \ \ n) x) \ g (f x)" if "x \ N" for x @@ -1278,7 +1278,7 @@ proof - have "{a<.. \ norm (fps_nth f i) * inverse (\ ^ (Suc n - i))" using 1 by (intro mult_left_mono less.IH) auto also have "\ = norm (fps_nth f i) / \ ^ (Suc n - i)" - by (simp add: divide_simps) + by (simp add: field_split_simps) finally show ?case . qed also have "\ = (\i = Suc 0..Suc n. norm (fps_nth f i) * \ ^ i) / \ ^ Suc n" @@ -360,7 +360,7 @@ using \\ > 0\ by (intro sum_le_suminf ballI mult_nonneg_nonneg zero_le_power summable) auto also have "\ \ 1" by fact finally show ?thesis using \\ > 0\ - by (simp add: divide_right_mono divide_simps) + by (simp add: divide_right_mono field_split_simps) qed qed @@ -457,7 +457,7 @@ have "(\n. norm (c * z) ^ n /\<^sub>R fact n) sums exp (norm (c * z))" by (rule exp_converges) also have "(\n. norm (c * z) ^ n /\<^sub>R fact n) = (\n. norm (fps_nth (fps_exp c) n * z ^ n))" - by (rule ext) (simp add: norm_divide norm_mult norm_power divide_simps power_mult_distrib) + by (rule ext) (simp add: norm_divide norm_mult norm_power field_split_simps power_mult_distrib) finally have "summable \" by (simp add: sums_iff) thus "summable (\n. fps_nth (fps_exp c) n * z ^ n)" by (rule summable_norm_cancel) @@ -494,7 +494,7 @@ by (intro Suc.IH [symmetric]) auto also have "\ / of_nat (Suc n) = fps_nth f (Suc n)" by (simp add: fps_deriv_def del: of_nat_Suc) - finally show ?case by (simp add: divide_simps) + finally show ?case by (simp add: field_split_simps) qed theorem eval_fps_eqD: @@ -613,7 +613,7 @@ lemma eval_fps_exp [simp]: fixes c :: "'a :: {banach, real_normed_field}" shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def - by (simp add: eval_fps_def exp_def scaleR_conv_of_real divide_simps power_mult_distrib) + by (simp add: eval_fps_def exp_def scaleR_conv_of_real field_split_simps power_mult_distrib) lemma fixes f :: "complex fps" and r :: ereal @@ -716,7 +716,7 @@ by (intro eval_fps_inverse[where r = r] less_le_trans[OF z] nz) (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) also have "f * inverse g = f / g" by fact - finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: divide_simps) + finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: field_split_simps) qed lemma @@ -1000,7 +1000,7 @@ by (subst eval_fps_mult) auto also have "eval_fps (inverse F * F) z = 1" using assms by (simp add: inverse_mult_eq_1) - finally show ?case by (auto simp: divide_simps) + finally show ?case by (auto simp: field_split_simps) qed with radius show ?thesis by (auto simp: has_fps_expansion_def) qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Function_Topology.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1005,7 +1005,7 @@ also have "... \ (1/2)^(to_nat i) * e i" unfolding m_def apply (rule Min_le) using \finite I\ \i \ I\ by auto ultimately have "min (dist (x i) (y i)) 1 < e i" - by (auto simp add: divide_simps) + by (auto simp add: field_split_simps) then have "dist (x i) (y i) < e i" using \e i < 1\ by auto then show "y i \ X i" using \ball (x i) (e i) \ X i\ by auto @@ -1058,7 +1058,7 @@ have "dist x y \ 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \ N} + (1/2)^N" by (rule dist_fun_le_dist_first_terms) also have "... \ 2 * f + e / 8" - apply (rule add_mono) using ** \2^N > 8/e\ by(auto simp add: algebra_simps divide_simps) + apply (rule add_mono) using ** \2^N > 8/e\ by(auto simp add: algebra_simps field_split_simps) also have "... \ e/2 + e/8" unfolding f_def by auto also have "... < e" @@ -1202,7 +1202,7 @@ also have "... < (1/2)^k * min e 1" using C \m \ N\ \n \ N\ by auto finally have "min (dist (u m i) (u n i)) 1 < min e 1" - by (auto simp add: algebra_simps divide_simps) + by (auto simp add: algebra_simps field_split_simps) then show "dist (u m i) (u n i) < e" by auto qed then show "\N. \m n. N \ m \ N \ n \ dist (u m i) (u n i) < e" @@ -1242,7 +1242,7 @@ using dist_fun_le_dist_first_terms by auto also have "... \ 2 * e/4 + e/4" apply (rule add_mono) - using ** \2^N > 4/e\ less_imp_le by (auto simp add: algebra_simps divide_simps) + using ** \2^N > 4/e\ less_imp_le by (auto simp add: algebra_simps field_split_simps) also have "... < e" by auto finally show ?thesis by simp qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Further_Topology.thy Wed Oct 09 14:51:54 2019 +0000 @@ -3148,7 +3148,7 @@ using Suc_leI assms \2 \ n\ complex_roots_unity [THEN eqset_imp_iff, of n "w/z"] by force have "cmod (w/z - 1) < 2 * sin (pi / real n)" - using lt assms \z \ 0\ by (simp add: divide_simps norm_divide) + using lt assms \z \ 0\ by (simp add: field_split_simps norm_divide) then have "cmod (exp (\ * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)" by (simp add: j field_simps) then have "2 * \sin((2 * pi * j / n) / 2)\ < 2 * sin (pi / real n)" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Gamma_Function.thy --- a/src/HOL/Analysis/Gamma_Function.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Gamma_Function.thy Wed Oct 09 14:51:54 2019 +0000 @@ -66,7 +66,7 @@ proof assume "of_int m / (of_int n :: 'a) \ \" then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases) - with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: divide_simps) + with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps) hence "m = k * n" by (subst (asm) of_int_eq_iff) hence "n dvd m" by simp with assms(1) show False by contradiction @@ -295,7 +295,7 @@ by (cases n, simp) (auto simp add: Gamma_series_def Gamma_series'_def pochhammer_rec' dest: pochhammer_eq_0_imp_nonpos_Int plus_of_nat_eq_0_imp) - also from n have "\ = z / of_nat n + 1" by (simp add: divide_simps) + also from n have "\ = z / of_nat n + 1" by (simp add: field_split_simps) finally show "z / of_nat n + 1 = Gamma_series' z n / Gamma_series z n" .. qed have "(\x. z / of_nat x) \ 0" @@ -403,7 +403,7 @@ moreover have "N \ 2" "N \ M" unfolding N_def by simp_all moreover have "(\k=m..n. 1/(of_nat k)\<^sup>2) < e'" if "m \ N" for m n using M[OF order.trans[OF \N \ M\ that]] unfolding real_norm_def - by (subst (asm) abs_of_nonneg) (auto intro: sum_nonneg simp: divide_simps) + by (subst (asm) abs_of_nonneg) (auto intro: sum_nonneg simp: field_split_simps) moreover note calculation } note N = this @@ -437,7 +437,7 @@ by (intro sum_cong_Suc) (simp_all del: of_nat_Suc add: field_simps Ln_of_nat Ln_of_nat_over_of_nat) also have "of_nat (k - 1) / of_nat k = 1 - 1 / (of_nat k :: complex)" if "k \ {Suc m..n}" for k - using that of_nat_eq_0_iff[of "Suc i" for i] by (cases k) (simp_all add: divide_simps) + using that of_nat_eq_0_iff[of "Suc i" for i] by (cases k) (simp_all add: field_split_simps) hence "(\k = Suc m..n. t * Ln (of_nat (k - 1) / of_nat k)) = (\k = Suc m..n. t * Ln (1 - 1 / of_nat k))" using mn N by (intro sum.cong) simp_all @@ -516,7 +516,7 @@ unfolding pochhammer_prod by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost) also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n" - unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def) + unfolding Gamma_series_def using assms by (simp add: field_split_simps powr_def) finally show ?thesis . qed @@ -582,9 +582,9 @@ hence t': "t \ -of_nat (Suc n)" by (intro notI) (simp del: of_nat_Suc) with t_nz have "?f n t = 1 / (of_nat (Suc n) * (1 + of_nat (Suc n)/t))" - by (simp add: divide_simps eq_neg_iff_add_eq_0 del: of_nat_Suc) + by (simp add: field_split_simps eq_neg_iff_add_eq_0 del: of_nat_Suc) also have "norm \ = inverse (of_nat (Suc n)) * inverse (norm (of_nat (Suc n)/t + 1))" - by (simp add: norm_divide norm_mult divide_simps add_ac del: of_nat_Suc) + by (simp add: norm_divide norm_mult field_split_simps add_ac del: of_nat_Suc) also { from z t_nz ball[OF t] have "of_nat (Suc n) / (4 * norm z) \ of_nat (Suc n) / (2 * norm t)" by (intro divide_left_mono mult_pos_pos) simp_all @@ -592,11 +592,11 @@ using t_nz n by (simp add: field_simps norm_divide del: of_nat_Suc) also have "\ \ norm (of_nat (Suc n)/t + 1)" by (rule norm_diff_ineq) finally have "inverse (norm (of_nat (Suc n)/t + 1)) \ 4 * norm z / of_nat (Suc n)" - using z by (simp add: divide_simps norm_divide mult_ac del: of_nat_Suc) + using z by (simp add: field_split_simps norm_divide mult_ac del: of_nat_Suc) } also have "inverse (real_of_nat (Suc n)) * (4 * norm z / real_of_nat (Suc n)) = 4 * norm z * inverse (of_nat (Suc n)^2)" - by (simp add: divide_simps power2_eq_square del: of_nat_Suc) + by (simp add: field_split_simps power2_eq_square del: of_nat_Suc) finally show "norm (?f n t) \ 4 * norm z * inverse (of_nat (Suc n)^2)" by (simp del: of_nat_Suc) qed @@ -1094,7 +1094,7 @@ have A: "eventually (\n. rGamma_series 1 n = of_nat (Suc n) / of_nat n) sequentially" using eventually_gt_at_top[of "0::nat"] by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact - divide_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int) + field_split_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int) have "rGamma_series 1 \ 1" by (subst tendsto_cong[OF A]) (rule LIMSEQ_Suc_n_over_n) moreover have "rGamma_series 1 \ rGamma 1" by (rule tendsto_intros) ultimately show ?thesis by (intro LIMSEQ_unique) @@ -1111,7 +1111,7 @@ pochhammer z (Suc (Suc n)) / (fact n * exp (z * of_real (ln (of_nat n))))" by (subst pochhammer_rec) (simp add: rGamma_series_def field_simps exp_add exp_of_real) also from n have "\ = ?f n * rGamma_series z n" - by (subst pochhammer_rec') (simp_all add: divide_simps rGamma_series_def add_ac) + by (subst pochhammer_rec') (simp_all add: field_split_simps rGamma_series_def add_ac) finally show "?f n * rGamma_series z n = z * rGamma_series (z + 1) n" .. qed moreover have "(\n. ?f n * rGamma_series z n) \ ((z+1) * 0 + 1) * rGamma z" @@ -1315,7 +1315,7 @@ pochhammer z (Suc (Suc n)) / (fact n * exp (z * of_real (ln (of_nat n))))" by (subst pochhammer_rec) (simp add: rGamma_series_def field_simps exp_add exp_of_real) also from n have "\ = ?f n * rGamma_series z n" - by (subst pochhammer_rec') (simp_all add: divide_simps rGamma_series_def add_ac) + by (subst pochhammer_rec') (simp_all add: field_split_simps rGamma_series_def add_ac) finally show "?f n * rGamma_series z n = z * rGamma_series (z + 1) n" .. qed moreover have "(\n. ?f n * rGamma_series z n) \ ((z+1) * 0 + 1) * rGamma z" @@ -1374,7 +1374,7 @@ have A: "eventually (\n. rGamma_series 1 n = of_nat (Suc n) / of_nat n) sequentially" using eventually_gt_at_top[of "0::nat"] by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact - divide_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int) + field_split_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int) have "rGamma_series 1 \ 1" by (subst tendsto_cong[OF A]) (rule LIMSEQ_Suc_n_over_n) thus "rGamma 1 = (1 :: complex)" unfolding rGamma_complex_def by (rule limI) qed @@ -2042,7 +2042,7 @@ moreover from z have "pochhammer (z + 1/2) n \ 0" by (auto dest: pochhammer_eq_0_imp_nonpos_Int) ultimately have "?powr 2 (2*z) * (Gamma_series' z n * Gamma_series' (z + 1/2) n) / Gamma_series' (2*z) (2*n) = ?f^2 / ?f' * of_nat (2^(2*n)) * (?powr n ((4*z + 1)/2) * ?powr n (-2*z))" - using n unfolding A B by (simp add: divide_simps exp_minus) + using n unfolding A B by (simp add: field_split_simps exp_minus) also have "?powr n ((4*z + 1)/2) * ?powr n (-2*z) = ?powr n (1/2)" by (simp add: algebra_simps exp_add[symmetric] add_divide_distrib) finally show "?g n = ?h n" by (simp only: mult_ac) @@ -2062,7 +2062,7 @@ by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all with lim[of "1/2 :: 'a"] have "?h \ 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real) from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis - by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps) + by (simp add: field_split_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps) qed theorem Gamma_reflection_complex: @@ -2330,7 +2330,7 @@ show ?thesis proof (cases "z \ \") case False - with \g z = pi\ show ?thesis by (auto simp: g_def divide_simps) + with \g z = pi\ show ?thesis by (auto simp: g_def field_split_simps) next case True then obtain n where n: "z = of_int n" by (elim Ints_cases) @@ -2344,7 +2344,7 @@ lemma rGamma_reflection_complex: "rGamma z * rGamma (1 - z :: complex) = sin (of_real pi * z) / of_real pi" using Gamma_reflection_complex[of z] - by (simp add: Gamma_def divide_simps split: if_split_asm) + by (simp add: Gamma_def field_split_simps split: if_split_asm) lemma rGamma_reflection_complex': "rGamma z * rGamma (- z :: complex) = -z * sin (of_real pi * z) / of_real pi" @@ -2358,7 +2358,7 @@ lemma Gamma_reflection_complex': "Gamma z * Gamma (- z :: complex) = - of_real pi / (z * sin (of_real pi * z))" - using rGamma_reflection_complex'[of z] by (force simp add: Gamma_def divide_simps mult_ac) + using rGamma_reflection_complex'[of z] by (force simp add: Gamma_def field_split_simps mult_ac) @@ -2403,7 +2403,7 @@ from eventually_at_ball'[OF zero_less_one, of "- of_nat n :: 'a" UNIV] show "eventually (\z. rGamma z / (z + of_nat n) = ?f z) (at (- of_nat n))" by (subst pochhammer_rGamma[of _ "Suc n"]) - (auto elim!: eventually_mono simp: divide_simps pochhammer_rec' eq_neg_iff_add_eq_0) + (auto elim!: eventually_mono simp: field_split_simps pochhammer_rec' eq_neg_iff_add_eq_0) have "isCont ?f (- of_nat n)" by (intro continuous_intros) thus "?f \ (- of_nat n) \ (- 1) ^ n * fact n" unfolding isCont_def by (simp add: pochhammer_same) @@ -2437,7 +2437,7 @@ from eventually_at_ball'[OF zero_less_one, of "- of_nat n :: 'a" UNIV] show "eventually (\z. Gamma z * (z + of_nat n) = inverse (rGamma z / (z + of_nat n))) (at (- of_nat n))" - by (auto elim!: eventually_mono simp: divide_simps rGamma_inverse_Gamma) + by (auto elim!: eventually_mono simp: field_split_simps rGamma_inverse_Gamma) have "(\z. inverse (rGamma z / (z + of_nat n))) \ (- of_nat n) \ inverse ((- 1) ^ n * fact n :: 'a)" by (intro tendsto_intros rGamma_zeros) simp_all @@ -2484,9 +2484,9 @@ also have "(\k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\k=1..n. 1 + 1 / real_of_nat k)" by (subst ln_prod [symmetric]) (auto intro!: add_pos_nonneg) also have "(\k=1..n. 1 + 1 / of_nat k :: real) = (\k=1..n. (of_nat k + 1) / of_nat k)" - by (intro prod.cong) (simp_all add: divide_simps) + by (intro prod.cong) (simp_all add: field_split_simps) also have "(\k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1" - by (induction n) (simp_all add: prod.nat_ivl_Suc' divide_simps) + by (induction n) (simp_all add: prod.nat_ivl_Suc' field_split_simps) finally show ?thesis .. qed @@ -2500,7 +2500,7 @@ from z have z': "z \ 0" by auto have "eventually (\n. ?r' n = ?r n) sequentially" - using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac + using z by (auto simp: field_split_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int) moreover have "?r' \ exp (z * of_real (ln 1))" by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all @@ -2572,7 +2572,7 @@ by (simp add: exp_add exp_sum exp_diff mult_ac Gamma_complex_altdef A) from tendsto_mult[OF tendsto_const[of "exp (-euler_mascheroni * z) / z"] this] z show "Gamma_series_Weierstrass z \ Gamma z" - by (simp add: exp_minus divide_simps Gamma_series_Weierstrass_def [abs_def]) + by (simp add: exp_minus field_split_simps Gamma_series_Weierstrass_def [abs_def]) qed lemma tendsto_complex_of_real_iff: "((\x. complex_of_real (f x)) \ of_real c) F = (f \ c) F" @@ -2616,7 +2616,7 @@ from False have "((z + of_nat n) gchoose n) = pochhammer z (Suc n) / z / fact n" by (simp add: gbinomial_pochhammer' pochhammer_rec) also have "pochhammer z (Suc n) / z / fact n * ?powr n (-z) = rGamma_series z n / z" - by (simp add: rGamma_series_def divide_simps exp_minus) + by (simp add: rGamma_series_def field_split_simps exp_minus) finally show "rGamma_series z n / z = ((z + of_nat n) gchoose n) * ?powr n (-z)" .. qed @@ -2644,7 +2644,7 @@ have "(\n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n)))) \ 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \ _") using Gamma_gbinomial[of "of_nat k :: 'a"] - by (simp add: binomial_gbinomial add_ac Gamma_def divide_simps exp_of_real [symmetric] exp_minus) + by (simp add: binomial_gbinomial add_ac Gamma_def field_split_simps exp_of_real [symmetric] exp_minus) also have "Gamma (of_nat (Suc k)) = fact k" by (simp add: Gamma_fact) finally show "?f \ 1 / fact k" . @@ -2710,7 +2710,7 @@ have "(z gchoose n) = Gamma (z + 2) / (z + 1) / (fact n * Gamma (z - of_nat n + 1))" by (subst gbinomial_Beta[OF assms]) (simp_all add: Beta_def Gamma_fact [symmetric] add_ac) also from assms have "Gamma (z + 2) / (z + 1) = Gamma (z + 1)" - using Gamma_plus1[of "z+1"] by (auto simp add: divide_simps mult_ac add_ac) + using Gamma_plus1[of "z+1"] by (auto simp add: field_split_simps mult_ac add_ac) finally show ?thesis . qed @@ -2847,7 +2847,7 @@ using Suc.IH[of "z+1"] Suc.prems by (intro has_integral_mult_left) (simp_all add: add_ac pochhammer_rec) also have "?A = (\t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps) also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))" - by (simp add: divide_simps pochhammer_rec + by (simp add: field_split_simps pochhammer_rec prod.shift_bounds_cl_Suc_ivl del: of_nat_Suc) finally show "((\t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}" by simp @@ -2957,7 +2957,7 @@ fix x :: real and n :: nat assume x: "x \ of_nat n" have "(1 - complex_of_real x / of_nat n) = complex_of_real ((1 - x / of_nat n))" by simp also have "norm \ = \(1 - x / real n)\" by (subst norm_of_real) (rule refl) - also from x have "\ = (1 - x / real n)" by (intro abs_of_nonneg) (simp_all add: divide_simps) + also from x have "\ = (1 - x / real n)" by (intro abs_of_nonneg) (simp_all add: field_split_simps) finally have "cmod (1 - complex_of_real x / of_nat n) = 1 - x / real n" . } note D = this from D[of x k] x @@ -3196,10 +3196,10 @@ (\k=1..n. 1 - z^2 / of_nat k ^ 2)" by (intro prod.cong) (simp_all add: power2_eq_square field_simps) finally show "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = of_real pi * z * \" - by (simp add: divide_simps) + by (simp add: field_split_simps) qed also have "(- of_real pi * inverse z) * (rGamma z * rGamma (- z)) = sin (of_real pi * z)" - by (subst rGamma_reflection_complex') (simp add: divide_simps) + by (subst rGamma_reflection_complex') (simp add: field_split_simps) finally show ?thesis . qed @@ -3228,7 +3228,7 @@ by (simp add: prod_inversef [symmetric]) also have "(\n. (\k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) = (\n. (\k=1..n. (4*real k^2)/(4*real k^2 - 1)))" - by (intro ext prod.cong refl) (simp add: divide_simps) + by (intro ext prod.cong refl) (simp add: field_split_simps) finally show ?thesis . qed @@ -3295,7 +3295,7 @@ by (simp add: eval_nat_numeral) from sums_divide[OF this, of "x^3 * pi"] x have "(\n. - (sin_coeff (n+3) * pi^(n+2) * x^n)) sums ((1 - sin (pi*x) / (pi*x)) / x^2)" - by (simp add: divide_simps eval_nat_numeral power_mult_distrib mult_ac) + by (simp add: field_split_simps eval_nat_numeral power_mult_distrib mult_ac) with x have "(\n. - (sin_coeff (n+3) * pi^(n+2) * x^n)) sums (g x / x^2)" by (simp add: g_def) hence "f' x = g x / x^2" by (simp add: sums_iff f'_def) @@ -3310,7 +3310,7 @@ assume x: "x \ 0" from summable_divide[OF sums_summable[OF sums_split_initial_segment[OF sin_converges[of "pi*x"]], of 3], of "-pi*x^3"] x - show ?thesis by (simp add: mult_ac power_mult_distrib divide_simps eval_nat_numeral) + show ?thesis by (simp add: mult_ac power_mult_distrib field_split_simps eval_nat_numeral) qed (simp only: summable_0_powser) qed hence "f' \ 0 \ f' 0" by (simp add: isCont_def) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Great_Picard.thy --- a/src/HOL/Analysis/Great_Picard.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Great_Picard.thy Wed Oct 09 14:51:54 2019 +0000 @@ -70,7 +70,7 @@ fix n::nat assume "0 < n" "ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi \ x" then have "ln (n + sqrt ((real n)\<^sup>2 - 1)) \ x * pi" - by (simp add: divide_simps) + by (simp add: field_split_simps) then have *: "exp (ln (n + sqrt ((real n)\<^sup>2 - 1))) \ exp (x * pi)" by blast have 0: "0 \ sqrt ((real n)\<^sup>2 - 1)" @@ -130,10 +130,10 @@ by (auto simp: real_le_lsqrt power2_eq_square algebra_simps 1 **) then have "((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \ 2" - using Schottky_lemma1 \0 < n\ by (simp add: divide_simps) + using Schottky_lemma1 \0 < n\ by (simp add: field_split_simps) then have "ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \ ln 2" apply (subst ln_le_cancel_iff) - using Schottky_lemma1 \0 < n\ by auto (force simp: divide_simps) + using Schottky_lemma1 \0 < n\ by auto (force simp: field_split_simps) also have "... \ 3" using ln_add_one_self_le_self [of 1] by auto finally show ?thesis . @@ -141,7 +141,7 @@ also have "... < pi" using pi_approx by simp finally show ?thesis - by (simp add: a_def b_def divide_simps) + by (simp add: a_def b_def field_split_simps) qed ultimately have "\x - a\ < 1/2 \ \x - b\ < 1/2" by (auto simp: abs_if) @@ -255,8 +255,8 @@ also have "... \ 2 + cmod (f 0) * 3" by simp finally have "1 + norm(2 * f 0 - 1) / 3 \ (2 + norm(f 0) - 1) * 3" - apply (simp add: divide_simps) - using norm_ge_zero [of "2 * f 0 - 1"] + apply (simp add: field_split_simps) + using norm_ge_zero [of "f 0 * 2 - 1"] by linarith with nh0 have "norm(h 0) \ (2 + norm(f 0) - 1) * 3" by linarith @@ -349,7 +349,7 @@ using has_contour_integral_bound_linepath [OF int_g', of "12/(1 - t)"] assms by simp with \cmod z \ t\ \t < 1\ show ?thesis - by (simp add: divide_simps) + by (simp add: field_split_simps) qed have fz: "f z = (1 + cos(of_real pi * h z)) / 2" using h \z \ ball 0 1\ by (auto simp: field_simps) @@ -880,13 +880,13 @@ then have r4_le_xy: "r/4 \ cmod (x - y)" using \r > 0\ by simp then have neq: "x \ y" "x \ z" - using that \r > 0\ by (auto simp: divide_simps norm_minus_commute) + using that \r > 0\ by (auto simp: field_split_simps norm_minus_commute) have leM: "cmod (\ n x) \ M" by (simp add: M dist_commute dist_norm that) have "cmod (\ n x / (x - y) - \ n x / (x - z)) = cmod (\ n x) * cmod (1 / (x - y) - 1 / (x - z))" by (metis (no_types, lifting) divide_inverse mult.left_neutral norm_mult right_diff_distrib') also have "... = cmod (\ n x) * cmod ((y - z) / ((x - y) * (x - z)))" - using neq by (simp add: divide_simps) + using neq by (simp add: field_split_simps) also have "... = cmod (\ n x) * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))" by (simp add: norm_mult norm_divide that) also have "... \ M * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))" @@ -899,7 +899,7 @@ apply (simp add: field_simps mult_less_0_iff norm_minus_commute) done also have "... \ e/r" - using \e > 0\ \r > 0\ r4_le_xy by (simp add: divide_simps) + using \e > 0\ \r > 0\ r4_le_xy by (simp add: field_split_simps) finally show ?thesis by simp qed have "(2 * pi) * cmod (\ n y - \ n z) = cmod ((2 * pi) * \ * \ n y - (2 * pi) * \ * \ n z)" @@ -908,7 +908,7 @@ apply (rule has_contour_integral_bound_circlepath [OF has_contour_integral_diff [OF y z], of "e/r"]) using \e > 0\ \r > 0\ le_er by auto also have "... = (2 * pi) * e * ((2 / 3))" - using \r > 0\ by (simp add: divide_simps) + using \r > 0\ by (simp add: field_split_simps) finally have "cmod (\ n y - \ n z) \ e * (2 / 3)" by simp also have "... < e" @@ -1142,7 +1142,7 @@ done qed with \0 < r\ \0 < m\ w w_inb show "deriv g w / g w = of_nat m / (w - z0) + deriv h w / h w" - by (auto simp: geq divide_simps hnz) + by (auto simp: geq field_split_simps hnz) qed moreover have "contour_integral (circlepath z0 (r/2)) (\z. m / (z - z0) + deriv h z / h z) = @@ -1268,7 +1268,7 @@ apply (rule subsetD [OF e]) using \0 < e\ by (auto simp: dist_norm norm_mult) have "cmod (h z) \ cmod (h (w + of_real e * (inverse e * (z - w))))" - using \0 < e\ by (simp add: divide_simps) + using \0 < e\ by (simp add: field_split_simps) also have "... \ exp (pi * exp (pi * (14 + 2 * r)))" using r [OF \h \ Y\] Schottky [OF hol_h_o norm_le_r _ _ _ le12] non01 by auto finally @@ -1483,7 +1483,7 @@ have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n by (metis norm_of_nat of_nat_Suc) have *: "(\x::complex. x / of_nat (Suc n)) ` (ball 0 1 - {0}) \ ball 0 1 - {0}" for n - by (auto simp: norm_divide divide_simps split: if_split_asm) + by (auto simp: norm_divide field_split_simps split: if_split_asm) define h where "h \ \n z::complex. f (z / (Suc n))" have holh: "(h n) holomorphic_on ball 0 1 - {0}" for n unfolding h_def @@ -1606,7 +1606,7 @@ then have "B > 0" by (metis \0 < \\ dense leI order.asym vector_choose_size) then have "inverse B > 0" - by (simp add: divide_simps) + by (simp add: field_split_simps) then show ?thesis apply (rule that [OF \0 < \\ \\ < 1\]) using \ by auto @@ -1632,7 +1632,7 @@ using \0 < r\ \a \ 0\ r by (auto simp: dist_norm norm_mult subset_eq) show "\w. w \ ball 0 1 - {0} \ f (z + of_real r * w) / a \ 0 \ f (z + of_real r * w) / a \ 1" - apply (simp add: divide_simps \a \ 0\) + apply (simp add: field_split_simps \a \ 0\) apply (rule f0a) using \0 < r\ r by (auto simp: dist_norm norm_mult subset_eq) qed @@ -1652,14 +1652,14 @@ case 1 have "\dist z w < e * r; w \ z\ \ cmod (f w) \ B * norm a" for w using \a \ 0\ \0 < r\ 1 [of "(w - z) / r"] - by (simp add: norm_divide dist_norm divide_simps) + by (simp add: norm_divide dist_norm field_split_simps) then show ?thesis by (force simp: intro!: boundedI) next case 2 have "\dist z w < e * r; w \ z\ \ cmod (f w) \ B * norm a" for w using \a \ 0\ \0 < r\ 2 [of "(w - z) / r"] - by (simp add: norm_divide dist_norm divide_simps) + by (simp add: norm_divide dist_norm field_split_simps) then have "\dist z w < e * r; w \ z\ \ inverse (cmod (f w)) \ inverse (B * norm a)" for w by (metis \0 < B\ \a \ 0\ mult_pos_pos norm_inverse norm_inverse_le_norm zero_less_norm_iff) then show ?thesis @@ -1754,7 +1754,7 @@ apply (rule tendsto_eq_intros refl gz \g z \ 0\)+ by (simp add: True) show "\x. \x \ ball z r; x \ z\ \ (1 + a * g x) / g x = f x" - using fab fab zrM by (fastforce simp add: gf divide_simps) + using fab fab zrM by (fastforce simp add: gf field_split_simps) qed (use \0 < r\ in auto) then show ?thesis using that by blast diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Harmonic_Numbers.thy --- a/src/HOL/Analysis/Harmonic_Numbers.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy Wed Oct 09 14:51:54 2019 +0000 @@ -258,7 +258,7 @@ shows "ln (x + a) - ln x \ a * (inverse x + inverse (x + a))/2" (is "_ \ ?A") proof - define f' where "f' = (inverse (x + a) - inverse x)/a" - have f'_nonpos: "f' \ 0" using assms by (simp add: f'_def divide_simps) + have f'_nonpos: "f' \ 0" using assms by (simp add: f'_def field_simps) let ?f = "\t. (t - x) * f' + inverse x" let ?F = "\t. (t - x)^2 * f' / 2 + t * inverse x" have diff: "\t. t \ {x..x+a} \ (?F has_vector_derivative ?f t) (at t within {x..x+a})" @@ -271,14 +271,14 @@ intro!: derivative_eq_intros) also have "?F (x+a) - ?F x = (a*2 + f'*a\<^sup>2*x) / (2*x)" using assms by (simp add: field_simps) also have "f'*a^2 = - (a^2) / (x*(x + a))" using assms - by (simp add: divide_simps f'_def power2_eq_square) + by (simp add: f'_def power2_eq_square) (simp add: field_simps) also have "(a*2 + - a\<^sup>2/(x*(x+a))*x) / (2*x) = ?A" using assms - by (simp add: divide_simps power2_eq_square) (simp add: algebra_simps) + by (simp add: power2_eq_square) (simp add: field_split_simps) finally have int1: "((\t. (t - x) * f' + inverse x) has_integral ?A) {x..x + a}" . from assms have int2: "(inverse has_integral (ln (x + a) - ln x)) {x..x+a}" by (intro fundamental_theorem_of_calculus) - (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] divide_simps + (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] field_split_simps intro!: derivative_eq_intros) hence "ln (x + a) - ln x = integral {x..x+a} inverse" by (simp add: integral_unique) also have ineq: "\xa\{x..x + a}. inverse xa \ (xa - x) * f' + inverse x" @@ -291,7 +291,7 @@ from convex_onD_Icc[OF this _ t] assms have "?A \ (1 - (t - x) / a) * inverse x + (t - x) / a * inverse (x + a)" by simp also have "\ = (t - x) * f' + inverse x" using assms - by (simp add: f'_def divide_simps) (simp add: f'_def field_simps) + by (simp add: f'_def divide_simps) (simp add: field_simps) finally show "inverse t \ (t - x) * f' + inverse x" . qed hence "integral {x..x+a} inverse \ integral {x..x+a} ?f" using f'_nonpos assms @@ -310,7 +310,7 @@ let ?F = "\t. (t - m)^2 * f' / 2 + t / m" from assms have "((\t. (t - m) * f' + inverse m) has_integral (?F y - ?F x)) {x..y}" by (intro fundamental_theorem_of_calculus) - (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] divide_simps + (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] field_split_simps intro!: derivative_eq_intros) also from m have "?F y - ?F x = ((y - m)^2 - (x - m)^2) * f' / 2 + (y - x) / m" by (simp add: field_simps) @@ -320,7 +320,7 @@ from assms have int2: "(inverse has_integral (ln y - ln x)) {x..y}" by (intro fundamental_theorem_of_calculus) - (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] divide_simps + (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] field_split_simps intro!: derivative_eq_intros) hence "ln y - ln x = integral {x..y} inverse" by (simp add: integral_unique) also have ineq: "\xa\{x..y}. inverse xa \ (xa - m) * f' + inverse m" @@ -484,7 +484,7 @@ hence "inverse c * (ln x - (\k (1 / (1-y^2) / of_nat (2*n+1))" by simp hence "(ln x - (\k (1 / (1 - y^2) / of_nat (2*n+1))" - by (auto simp add: divide_simps) + by (auto simp add: field_split_simps) with c_pos have "ln x \ c / (1 - y^2) / of_nat (2*n+1) + approx" by (subst (asm) pos_divide_le_eq) (simp_all add: mult_ac approx_def) moreover { diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1848,7 +1848,7 @@ using g_near_f[OF x, of n] g_near_f[OF x, of m] by simp also have "\ \ 1 / (real M) + 1 / (real M)" apply (rule add_mono) - using \M \ 0\ m n by (auto simp: divide_simps) + using \M \ 0\ m n by (auto simp: field_split_simps) also have "\ = 2 / real M" by auto finally show "norm (g n x - g m x) \ 2 / real M" @@ -1900,7 +1900,7 @@ then have norm_less: "norm ((\(x,K) \ \. content K *\<^sub>R g (N1 + N2) x) - h (N1 + N2)) < e/3" using g' by blast have "content (cbox a b) < e/3 * (of_nat N2)" - using \N2 \ 0\ N2 using True by (auto simp: divide_simps) + using \N2 \ 0\ N2 using True by (auto simp: field_split_simps) moreover have "e/3 * of_nat N2 \ e/3 * (of_nat (N1 + N2) + 1)" using \e>0\ by auto ultimately have "content (cbox a b) < e/3 * (of_nat (N1 + N2) + 1)" @@ -2904,7 +2904,7 @@ "Dg n s = (if n < p then (-1)^n * (b - s)^(p - 1 - n) / fact (p - 1 - n) else 0)" for n s have g0: "Dg 0 = g" using \p > 0\ - by (auto simp add: Dg_def divide_simps g_def split: if_split_asm) + by (auto simp add: Dg_def field_split_simps g_def split: if_split_asm) { fix m assume "p > Suc m" @@ -2916,7 +2916,7 @@ have Dg: "\m t. m < p \ a \ t \ t \ b \ (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a..b})" unfolding Dg_def - by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def fact_eq divide_simps) + by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def fact_eq field_split_simps) let ?sum = "\t. \iR Dg i t *\<^sub>R Df (p - Suc i) t" from sum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df, OF \p > 0\ g0 Dg f0 Df] @@ -6582,7 +6582,7 @@ integrable_continuous continuous_intros) also have "\ < e'" using \0 < e'\ \e > 0\ - by (auto simp: e_def divide_simps) + by (auto simp: e_def field_split_simps) finally show "dist (integral (cbox a b) (f y)) (integral (cbox a b) (f x)) < e'" . qed qed @@ -6672,8 +6672,8 @@ also have "\ < e' * norm (x - x0)" using \e' > 0\ apply (intro mult_strict_right_mono[OF _ \0 < norm (x - x0)\]) - apply (auto simp: divide_simps e_def) - by (metis \0 < e\ e_def order.asym zero_less_divide_iff) + apply (simp add: divide_simps e_def not_less) + done finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" . then show ?case by (auto simp: divide_simps) @@ -7263,10 +7263,10 @@ \ e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)" apply (rule integrable_bound [OF _ _ normint_wz]) using cbp \0 < e/content ?CBOX\ - apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const) + apply (auto simp: field_split_simps content_pos_le integrable_diff int_integrable integrable_const) done also have "... \ e * content (cbox (u,w) (v,z)) / content ?CBOX/2" - by (simp add: content_Pair divide_simps) + by (simp add: content_Pair field_split_simps) finally have 2: "norm (integral (cbox u v) (\x. integral (cbox w z) (\y. f (x,y))) - integral (cbox u v) (\x. integral (cbox w z) (\y. f (t1,t2)))) \ e * content (cbox (u,w) (v,z)) / content ?CBOX/2" @@ -7561,7 +7561,7 @@ with assms have "a powr (e + 1) \ n powr (e + 1)" by (intro powr_mono2') simp_all with assms show ?thesis by (auto simp: divide_simps F_def integral_f) - qed (insert assms, simp add: integral_f F_def divide_simps) + qed (insert assms, simp add: integral_f F_def field_split_simps) thus "bounded (range(\k. integral {a..} (f k)))" unfolding bounded_iff by (intro exI[of _ "-F a"]) auto qed @@ -7591,12 +7591,12 @@ note has_integral_powr_to_inf[OF this \a > 0\] also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) = 1 / (real (n - 1) * a powr (real (n - 1)))" using assms - by (simp add: divide_simps powr_add [symmetric] of_nat_diff) + by (simp add: field_split_simps powr_add [symmetric] of_nat_diff) also from assms have "a powr (real (n - 1)) = a ^ (n - 1)" by (intro powr_realpow) finally show ?thesis by (rule has_integral_eq [rotated]) - (insert assms, simp_all add: powr_minus powr_realpow divide_simps) + (insert assms, simp_all add: powr_minus powr_realpow field_split_simps) qed subsubsection \Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\ diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Homeomorphism.thy Wed Oct 09 14:51:54 2019 +0000 @@ -95,7 +95,7 @@ then have [simp]: "(norm x / norm y) *\<^sub>R y = x" by (rule eqI) (simp add: \y \ 0\) have no: "0 \ norm x / norm y" "norm x / norm y < 1" - using * by (auto simp: divide_simps) + using * by (auto simp: field_split_simps) then show "x = y" using starI [OF \y \ S\ no] xynot by auto next @@ -107,7 +107,7 @@ then have [simp]: "(norm y / norm x) *\<^sub>R x = y" by (rule eqI) (simp add: \x \ 0\) have no: "0 \ norm y / norm x" "norm y / norm x < 1" - using * by (auto simp: divide_simps) + using * by (auto simp: field_split_simps) then show "x = y" using starI [OF \x \ S\ no] xynot by auto qed @@ -133,7 +133,7 @@ show "x \ (\x. x /\<^sub>R norm x) ` (S - rel_interior S)" apply (rule_tac x="d *\<^sub>R x" in image_eqI) using \0 < d\ - using dx \closed S\ apply (auto simp: rel_frontier_def divide_simps nox) + using dx \closed S\ apply (auto simp: rel_frontier_def field_split_simps nox) done qed qed @@ -265,7 +265,7 @@ show ?thesis apply (rule_tac x="inverse(norm(surf (proj x))) *\<^sub>R x" in image_eqI) apply (metis (no_types, hide_lams) mult.commute scaleproj abs_inverse abs_norm_cancel divide_inverse norm_scaleR nxx positive_imp_inverse_positive proj_scaleR psp sproj_nz zero_less_norm_iff) - apply (auto simp: divide_simps nole affineI) + apply (auto simp: field_split_simps nole affineI) done qed ultimately have im_cball: "(\x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S" @@ -503,24 +503,28 @@ define f where "f \ \x. 2 *\<^sub>R b + (2 / (1 - b\x)) *\<^sub>R (x - b)" define g where "g \ \y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y - 2 *\<^sub>R b)" have [simp]: "\x. \x \ T; b\x = 0\ \ f (g x) = x" - unfolding f_def g_def by (simp add: algebra_simps divide_simps add_nonneg_eq_0_iff) - have no: "\x. \norm x = 1; b\x \ 1\ \ (norm (f x))\<^sup>2 = 4 * (1 + b\x) / (1 - b\x)" - apply (simp add: dot_square_norm [symmetric]) - apply (simp add: f_def vector_add_divide_simps divide_simps norm_eq_1) - apply (simp add: algebra_simps inner_commute) + unfolding f_def g_def by (simp add: algebra_simps field_split_simps add_nonneg_eq_0_iff) + have no: "(norm (f x))\<^sup>2 = 4 * (1 + b \ x) / (1 - b \ x)" + if "norm x = 1" and "b \ x \ 1" for x + using that + apply (simp flip: dot_square_norm add: norm_eq_1 nonzero_eq_divide_eq) + apply (simp add: f_def vector_add_divide_simps inner_simps) + apply (use sum_sqs_eq [of 1 "b \ x"] + in \auto simp add: field_split_simps inner_commute\) done have [simp]: "\u::real. 8 + u * (u * 8) = u * 16 \ u=1" by algebra have [simp]: "\x. \norm x = 1; b \ x \ 1\ \ g (f x) = x" - unfolding g_def no by (auto simp: f_def divide_simps) - have [simp]: "\x. \x \ T; b \ x = 0\ \ norm (g x) = 1" - unfolding g_def + unfolding g_def no by (auto simp: f_def field_split_simps) + have [simp]: "norm (g x) = 1" if "x \ T" and "b \ x = 0" for x + using that + apply (simp only: g_def) apply (rule power2_eq_imp_eq) apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps) apply (simp add: algebra_simps inner_commute) done - have [simp]: "\x. \x \ T; b \ x = 0\ \ b \ g x \ 1" - unfolding g_def + have [simp]: "b \ g x \ 1" if "x \ T" and "b \ x = 0" for x + using that unfolding g_def apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff) apply (auto simp: algebra_simps) done @@ -547,7 +551,7 @@ apply (auto simp: power2_eq_square algebra_simps inner_commute) done have [simp]: "\x. \norm x = 1; b \ x \ 1\ \ b \ f x = 0" - by (simp add: f_def algebra_simps divide_simps) + by (simp add: f_def algebra_simps field_split_simps) have [simp]: "\x. \x \ T; norm x = 1; b \ x \ 1\ \ f x \ T" unfolding f_def by (blast intro: \subspace T\ \b \ T\ subspace_add subspace_mul subspace_diff) @@ -1442,9 +1446,9 @@ obtain t where "t \ tk" and t: "{real n / real N .. (1 + real n) / real N} \ K t" proof (rule bexE [OF \]) show "{real n / real N .. (1 + real n) / real N} \ {0..1}" - using Suc.prems by (auto simp: divide_simps algebra_simps) + using Suc.prems by (auto simp: field_split_simps algebra_simps) show diameter_less: "diameter {real n / real N .. (1 + real n) / real N} < \" - using \0 < \\ N by (auto simp: divide_simps algebra_simps) + using \0 < \\ N by (auto simp: field_split_simps algebra_simps) qed blast have t01: "t \ {0..1}" using \t \ tk\ \tk \ {0..1}\ by blast @@ -1454,7 +1458,7 @@ and homuu: "\U. U \ \ \ \q. homeomorphism U (UU (X t)) p q" using inUS [OF t01] UU by meson have n_div_N_in: "real n / real N \ {real n / real N .. (1 + real n) / real N}" - using N by (auto simp: divide_simps algebra_simps) + using N by (auto simp: field_split_simps algebra_simps) with t have nN_in_kkt: "real n / real N \ K t" by blast have "k (real n / real N, y) \ C \ p -` UU (X t)" @@ -1466,7 +1470,7 @@ also have "... \ h ` (({0..1} \ K t) \ (U \ NN t))" apply (rule imageI) using \y \ V\ t01 \n \ N\ - apply (simp add: nN_in_kkt \y \ U\ inUS divide_simps) + apply (simp add: nN_in_kkt \y \ U\ inUS field_split_simps) done also have "... \ UU (X t)" using him t01 by blast @@ -1514,7 +1518,7 @@ then have "y \ Q'" "Q \ (U \ NN(t)) \ N' \ V" by blast+ have neq: "{0..real n / real N} \ {real n / real N..(1 + real n) / real N} = {0..(1 + real n) / real N}" - apply (auto simp: divide_simps) + apply (auto simp: field_split_simps) by (metis mult_zero_left of_nat_0_le_iff of_nat_0_less_iff order_trans real_mult_le_cancel_iff1) then have neqQ': "{0..real n / real N} \ Q' \ {real n / real N..(1 + real n) / real N} \ Q' = {0..(1 + real n) / real N} \ Q'" by blast diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Homotopy.thy Wed Oct 09 14:51:54 2019 +0000 @@ -4624,7 +4624,7 @@ using norm_triangle_ineq by blast also have "\ = norm y + (norm x - norm y) * (norm u / r)" using yx \r > 0\ - by (simp add: divide_simps) + by (simp add: field_split_simps) also have "\ < norm y + (norm x - norm y) * 1" apply (subst add_less_cancel_left) apply (rule mult_strict_left_mono) @@ -5039,7 +5039,7 @@ using assms by auto have "f ` {a..b} = {c..d}" unfolding f_def image_affinity_atLeastAtMost - using assms sum_sqs_eq by (auto simp: divide_simps algebra_simps) + using assms sum_sqs_eq by (auto simp: field_split_simps algebra_simps) then show "f ` cbox a b = cbox c d" by auto show "inj_on f (cbox a b)" @@ -5051,7 +5051,7 @@ show "f a = c" by (simp add: f_def) show "f b = d" - using assms sum_sqs_eq [of a b] by (auto simp: f_def divide_simps algebra_simps) + using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps algebra_simps) qed qed @@ -5631,7 +5631,7 @@ also have "\ < e" apply (rule d [unfolded dist_norm]) using greater \0 < d\ \b1 \ Basis\ that - by (auto simp: dist_norm divide_simps) + by (simp_all add: dist_norm) (simp add: field_simps) finally show ?thesis . qed show ?thesis diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Improper_Integral.thy --- a/src/HOL/Analysis/Improper_Integral.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Improper_Integral.thy Wed Oct 09 14:51:54 2019 +0000 @@ -725,7 +725,7 @@ case False have prod_if: "(\k\Basis \ - {i}. f k) = (\k\Basis. f k) / f i" if "f i \ (0::real)" for f using that mk_disjoint_insert [OF i] - apply (clarsimp simp add: divide_simps) + apply (clarsimp simp add: field_split_simps) by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf mult.commute order_refl prod.insert subset_Compl_singleton) have abc: "a \ i < c" "c < b \ i" using False assms by auto @@ -733,7 +733,7 @@ \ content(cbox a b') / (c - a \ i)" "(\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K) \ content(cbox a' b) / (b \ i - c)" - using lec gec by (simp_all add: divide_simps mult.commute) + using lec gec by (simp_all add: field_split_simps mult.commute) moreover have "(\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K) + @@ -780,7 +780,7 @@ \ 2 * content (cbox a b) / (b \ i - a \ i)" by linarith then show ?thesis - using abc by (simp add: divide_simps mult.commute) + using abc by (simp add: field_split_simps mult.commute) qed qed @@ -856,8 +856,8 @@ have "gauge (\x. ball x (\ * (INF m\Basis. b \ m - a \ m) / ((8 * norm (f x) + 8) * content (cbox a b))))" using \0 < content (cbox a b)\ \0 < \\ a_less_b - apply (auto simp: gauge_def divide_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff) - apply (meson add_nonneg_nonneg mult_nonneg_nonneg norm_ge_zero not_less zero_le_numeral) + apply (auto simp: gauge_def field_split_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff) + apply (meson add_increasing measure_nonneg mult_nonneg_nonneg norm_ge_zero not_le zero_le_numeral) done then have "gauge \" unfolding \_def using \gauge \0\ gauge_Int by auto @@ -936,7 +936,7 @@ by simp also have "... < \ * (b \ i - a \ i) / dist u v / (4 * content (cbox a b))" using duv dist_uv contab_gt0 - apply (simp add: divide_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm) + apply (simp add: field_split_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm) by (meson add_nonneg_nonneg linorder_not_le measure_nonneg mult_nonneg_nonneg norm_ge_zero zero_le_numeral) also have "... = \ * (b \ i - a \ i) / norm (v - u) / (4 * content (cbox a b))" by (simp add: dist_norm norm_minus_commute) @@ -953,7 +953,7 @@ using mult_left_mono by fastforce also have "... = \/4 * (b \ i - a \ i) / content (cbox a b) * content K / ?\" - by (simp add: divide_simps) + by (simp add: field_split_simps) finally show ?thesis . qed qed @@ -1533,7 +1533,7 @@ using n \n \ 0\ emin [OF \i \ Basis\] by (simp_all add: inverse_eq_divide) show "1 / real (Suc m) \ 1 / real n" - using \n \ 0\ \m \ n\ by (simp add: divide_simps) + using \n \ 0\ \m \ n\ by (simp add: field_split_simps) qed then show ?thesis by (simp add: mem_box) qed @@ -1684,7 +1684,7 @@ with N have "k > ((b - a) \ i) / ((x - a) \ i)" using \N \ k\ by linarith with x that show ?thesis - by (auto simp: mem_box algebra_simps divide_simps) + by (auto simp: mem_box algebra_simps field_split_simps) qed have bx_gt: "(b - x) \ i > ((b - a) \ i) / k" if "i \ Basis" for i proof - @@ -1696,7 +1696,7 @@ with N have "k > ((b - a) \ i) / ((b - x) \ i)" using \N \ k\ by linarith with x that show ?thesis - by (auto simp: mem_box algebra_simps divide_simps) + by (auto simp: mem_box algebra_simps field_split_simps) qed show "x \ cbox (a + (b - a) /\<^sub>R k) (b - (b - a) /\<^sub>R k)" using that \ \k > 0\ @@ -1883,7 +1883,7 @@ then obtain m::nat where m: "floor(n * f x) = int m" using nonneg_int_cases zero_le_floor by blast then have kn: "real k / real n \ f x \ k \ m" for k - using \n \ 0\ by (simp add: divide_simps mult.commute) linarith + using \n \ 0\ by (simp add: field_split_simps mult.commute) linarith then have "Suc n / real n \ f x \ Suc n \ m" by blast have "real n * f x \ real n" @@ -1894,7 +1894,7 @@ by (subst sum.inter_restrict) (auto simp: kn) also have "\ < inverse n" using \m \ n\ \n \ 0\ m - by (simp add: min_absorb2 divide_simps mult.commute) linarith + by (simp add: min_absorb2 field_split_simps mult.commute) linarith finally show ?thesis . qed @@ -2156,7 +2156,7 @@ by (metis Suc_n_not_le_n non0) qed (use x 01 non0 in auto) also have "\ \ inverse N" - using seq_suble [OF \] \N \ 0\ non0 that by (auto intro: order_trans simp: divide_simps) + using seq_suble [OF \] \N \ 0\ non0 that by (auto intro: order_trans simp: field_split_simps) finally show ?thesis by linarith qed @@ -2222,7 +2222,7 @@ proof (subst has_integral_cong) show "g x * f x - g a * f x = (g b - g a) * h x *\<^sub>R f x" if "x \ {a..b}" for x - using 1 that by (simp add: h_def divide_simps algebra_simps) + using 1 that by (simp add: h_def field_split_simps algebra_simps) show "((\x. (g b - g a) * h x *\<^sub>R f x) has_integral (g b - g a) * integral {c..b} f) {a..b}" using has_integral_mult_right [OF c, of "g b - g a"] . qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Infinite_Products.thy --- a/src/HOL/Analysis/Infinite_Products.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Infinite_Products.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1732,7 +1732,7 @@ have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)" by (auto simp: norm_divide norm_mult norm_power) also have "\ \ cmod (z k) ^ n" - by (auto simp: divide_simps mult_le_cancel_left1 in_Reals_norm) + by (auto simp: field_split_simps mult_le_cancel_left1 in_Reals_norm) also have "\ \ (1 / 2) ^ n" using N [OF that] by (simp add: power_mono) finally show "norm (?f n) \ (1 / 2) ^ n" . diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1001,7 +1001,7 @@ using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq) with le c show "emeasure ?D (box l u) = (\b\?B. (u - l) \ b)" by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps - field_simps divide_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric] + field_simps field_split_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric] intro!: prod.cong) qed simp diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Linear_Algebra.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1806,7 +1806,7 @@ show "pairwise orthogonal ?S" using \pairwise orthogonal S\ by (auto simp: pairwise_def orthogonal_def) show "\x. x \ (\x. x /\<^sub>R norm x) ` S \ norm x = 1" - using \0 \ S\ by (auto simp: divide_simps) + using \0 \ S\ by (auto simp: field_split_simps) then show "independent ?S" by (metis \pairwise orthogonal ((\x. x /\<^sub>R norm x) ` S)\ norm_zero pairwise_orthogonal_independent zero_neq_one) have "inj_on (\x. x /\<^sub>R norm x) S" @@ -1932,7 +1932,7 @@ proof (rule eventually_mono) show "norm (h (f x) - h l) < e" if "norm (f x - l) < e / B" for x using that B - apply (simp add: divide_simps) + apply (simp add: field_split_simps) by (metis \linear h\ le_less_trans linear_diff mult.commute) qed qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Lipschitz.thy --- a/src/HOL/Analysis/Lipschitz.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Lipschitz.thy Wed Oct 09 14:51:54 2019 +0000 @@ -595,7 +595,7 @@ have "?d \ e/2/(L + 1)" by simp also have "(L + 1) * \ \ e / 2" using \0 < e\ \L \ 0\ - by (auto simp: divide_simps) + by (auto simp: field_split_simps) finally have le1: "(L + 1) * dist y b < e / 2" using \L \ 0\ by simp have "dist x a \ dist (x, y) (a, b)" @@ -684,7 +684,7 @@ from this elim d[of "rx (ry (rt n))"] have "\ < dist (f (?t n) (?y n)) (f (?t n) (?x n)) / rx (ry (rt (n)))" using lx'(2) ly'(2) lt'(2) \0 < rx _\ - by (auto simp add: divide_simps algebra_simps strict_mono_def) + by (auto simp add: field_split_simps algebra_simps strict_mono_def) also have "\ \ diameter ?S / n" by (force intro!: \0 < n\ strict_mono_def xy diameter_bounded_bound frac_le compact_imp_bounded compact t diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Path_Connected.thy Wed Oct 09 14:51:54 2019 +0000 @@ -642,14 +642,14 @@ assume "g2 x = g2 y" "0 \ x" "x \ 1" "0 \ y" "y \ 1" then show "x = y" using * [of "(x + 1) / 2" "(y + 1) / 2"] - by (force simp: joinpaths_def split_ifs divide_simps) + by (force simp: joinpaths_def split_ifs field_split_simps) qed ultimately have "arc g2" using assms by (simp add: arc_def) have "g2 y = g1 0 \ g2 y = g1 1" if "g1 x = g2 y" "0 \ x" "x \ 1" "0 \ y" "y \ 1" for x y using * [of "x / 2" "(y + 1) / 2"] that - by (auto simp: joinpaths_def split_ifs divide_simps) + by (auto simp: joinpaths_def split_ifs field_split_simps) then have "path_image g1 \ path_image g2 \ {pathstart g1, pathstart g2}" by (fastforce simp: pathstart_def pathfinish_def path_image_def) with \arc g1\ \arc g2\ show ?thesis using that by blast @@ -674,7 +674,7 @@ using assms by (simp add: simple_path_def) have False if "g1 0 = g2 u" "0 \ u" "u \ 1" for u using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \?lhs\] - by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps) + by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs field_split_simps) then have n1: "pathstart g1 \ path_image g2" unfolding pathstart_def path_image_def using atLeastAtMost_iff by blast @@ -848,9 +848,9 @@ { fix x y assume "x \ closed_segment u v" "y \ closed_segment u v" "g x = g y" then have "x = y \ x = u \ y = v \ x = v \ y = u" - using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p - by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost divide_simps - split: if_split_asm) + using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p + by (auto split: if_split_asm simp add: closed_segment_real_eq image_affinity_atLeastAtMost) + (simp_all add: field_split_simps) } moreover have "path(subpath u v g) \ u\v" using sim [of "1/3" "2/3"] p @@ -884,9 +884,10 @@ { fix x y assume "x \ closed_segment u v" "y \ closed_segment u v" "g x = g y" then have "x = y" - using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p - by (force simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps - split: if_split_asm) + using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p + by (cases "v = u") + (simp_all split: if_split_asm add: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost, + simp add: field_simps) } moreover have "path(subpath u v g) \ u\v" using sim [of "1/3" "2/3"] p @@ -937,7 +938,7 @@ done lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p" - by (rule ext) (simp add: joinpaths_def subpath_def divide_simps) + by (rule ext) (simp add: joinpaths_def subpath_def field_split_simps) subsection\<^marker>\tag unimportant\\There is a subpath to the frontier\ @@ -2457,9 +2458,8 @@ { fix u assume u: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + C *\<^sub>R (x - a)) \ s" and "0 \ u" "u \ 1" have CC: "1 \ 1 + (C - 1) * u" - using \x \ a\ \0 \ u\ - apply (simp add: C_def divide_simps norm_minus_commute) - using Bx by auto + using \x \ a\ \0 \ u\ Bx + by (auto simp add: C_def norm_minus_commute) have *: "\v. (1 - u) *\<^sub>R x + u *\<^sub>R (a + v *\<^sub>R (x - a)) = a + (1 + (v - 1) * u) *\<^sub>R (x - a)" by (simp add: algebra_simps) have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) = @@ -2492,9 +2492,8 @@ { fix u assume u: "(1 - u) *\<^sub>R y + u *\<^sub>R (a + D *\<^sub>R (y - a)) \ s" and "0 \ u" "u \ 1" have DD: "1 \ 1 + (D - 1) * u" - using \y \ a\ \0 \ u\ - apply (simp add: D_def divide_simps norm_minus_commute) - using By by auto + using \y \ a\ \0 \ u\ By + by (auto simp add: D_def norm_minus_commute) have *: "\v. (1 - u) *\<^sub>R y + u *\<^sub>R (a + v *\<^sub>R (y - a)) = a + (1 + (v - 1) * u) *\<^sub>R (y - a)" by (simp add: algebra_simps) have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) = @@ -3008,11 +3007,20 @@ case True with B Bno show ?thesis by force next case False - with B C have "closed_segment x (((B + C) / norm x) *\<^sub>R x) \ - ball 0 B" - apply (clarsimp simp add: closed_segment_def ball_def dist_norm real_vector_class.scaleR_add_left [symmetric] divide_simps) - using segment_bound_lemma [of B "norm x" "B+C" ] Bno - by (meson le_add_same_cancel1 less_eq_real_def not_le) + proof + fix w + assume "w \ closed_segment x (((B + C) / norm x) *\<^sub>R x)" + then obtain u where + w: "w = (1 - u + u * (B + C) / norm x) *\<^sub>R x" "0 \ u" "u \ 1" + by (auto simp add: closed_segment_def real_vector_class.scaleR_add_left [symmetric]) + with False B C have "B \ (1 - u) * norm x + u * (B + C)" + using segment_bound_lemma [of B "norm x" "B + C" u] Bno + by simp + with False B C show "w \ - ball 0 B" + using distrib_right [of _ _ "norm x"] + by (simp add: ball_def w not_less) + qed also have "... \ -S" by (simp add: B) finally have "\T. connected T \ T \ - S \ x \ T \ ((B + C) / norm x) *\<^sub>R x \ T" @@ -3303,7 +3311,7 @@ by (metis mem_Collect_eq) define C where "C = (B + 1 + norm z) / norm (z-a)" have "C > 0" - using \0 < B\ zna by (simp add: C_def divide_simps add_strict_increasing) + using \0 < B\ zna by (simp add: C_def field_split_simps add_strict_increasing) have "\norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\ \ norm z" by (metis add_diff_cancel norm_triangle_ineq3) moreover have "norm (C *\<^sub>R (z-a)) > norm z + B" @@ -3314,10 +3322,10 @@ then have Cpos: "1 + u * C > 0" by (meson \0 < C\ add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one) then have *: "(1 / (1 + u * C)) *\<^sub>R z + (u * C / (1 + u * C)) *\<^sub>R z = z" - by (simp add: scaleR_add_left [symmetric] divide_simps) + by (simp add: scaleR_add_left [symmetric] field_split_simps) then have False using convexD_alt [OF s \a \ s\ ins, of "1/(u*C + 1)"] \C>0\ \z \ s\ Cpos u - by (simp add: * divide_simps algebra_simps) + by (simp add: * field_split_simps algebra_simps) } note contra = this have "connected_component (- s) z (z + C *\<^sub>R (z-a))" apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]]) @@ -3327,7 +3335,7 @@ done then have False using zna B [of "z + C *\<^sub>R (z-a)"] C - by (auto simp: divide_simps max_mult_distrib_right) + by (auto simp: field_split_simps max_mult_distrib_right) } then show ?thesis by (auto simp: outside_def z) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Polytope.thy --- a/src/HOL/Analysis/Polytope.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Polytope.thy Wed Oct 09 14:51:54 2019 +0000 @@ -192,7 +192,7 @@ have nbc: "norm (b - c) + e > 0" using \e > 0\ by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero) then have [simp]: "d \ c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c] - by (simp add: algebra_simps d_def) (simp add: divide_simps) + by (simp add: algebra_simps d_def) (simp add: field_split_simps) have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))" using False nbc by (simp add: divide_simps) (simp add: algebra_simps) @@ -287,7 +287,7 @@ proof - have "inverse(k) *\<^sub>R (x - y) = (1 - inverse k) *\<^sub>R inverse(1 - k) *\<^sub>R y + inverse(k) *\<^sub>R x" using assms - by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] divide_simps) + by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] field_split_simps) then show ?thesis using \affine S\ xy by (auto simp: affine_alt) qed @@ -1316,7 +1316,7 @@ apply (rule_tac x="u/x" in exI) apply (rule_tac x="v/x" in exI) apply (rule_tac x="w/x" in exI) - using x apply (auto simp: algebra_simps divide_simps) + using x apply (auto simp: algebra_simps field_split_simps) done ultimately show ?thesis by force qed @@ -1445,14 +1445,14 @@ have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux" by (metis \ux \ 0\ uxx mult.commute right_inverse scaleR_one scaleR_scaleR) also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" - using \ux \ 0\ equx apply (auto simp: algebra_simps divide_simps) + using \ux \ 0\ equx apply (auto simp: algebra_simps field_split_simps) by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left) finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" . then have "x \ open_segment b c" apply (simp add: in_segment \b \ c\) apply (rule_tac x="(v * uc) / ux" in exI) using \0 \ ux\ \ux \ 0\ \0 < uc\ \0 < v\ \0 < ub\ \v < 1\ equx - apply (force simp: algebra_simps divide_simps) + apply (force simp: algebra_simps field_split_simps) done then show ?thesis by (rule face_ofD [OF F _ b c \x \ F\]) @@ -1841,7 +1841,7 @@ also have "... = \ * norm (x - z)" using \e > 0\ by (simp add: \_def) also have "... < e" - using \z \ x\ \e > 0\ by (simp add: \_def min_def divide_simps norm_minus_commute) + using \z \ x\ \e > 0\ by (simp add: \_def min_def field_split_simps norm_minus_commute) finally have lte: "norm (\ *\<^sub>R x - \ *\<^sub>R z) < e" . have \_aff: "\ *\<^sub>R z + (1 - \) *\<^sub>R x \ affine hull S" by (metis \x \ S\ add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff) @@ -2034,7 +2034,7 @@ define w where "w = (1 - l) *\<^sub>R x + l *\<^sub>R z" have "0 < l" "l < 1" using able xltz \b h < a h \ z\ \h \ F\ - by (auto simp: l_def divide_simps) + by (auto simp: l_def field_split_simps) have awlt: "a i \ w < b i" if "i \ F" "i \ h" for i proof - have "(1 - l) * (a i \ x) < (1 - l) * b i" @@ -2116,7 +2116,7 @@ done then show ?thesis using \0 < inff\ awlt [OF that] mult_strict_left_mono - by (fastforce simp add: algebra_simps divide_simps split: if_split_asm) + by (fastforce simp add: algebra_simps field_split_simps split: if_split_asm) next case False with \0 < inff\ have "inff * (a j \ y - a j \ w) \ 0" @@ -3002,7 +3002,7 @@ apply (simp add: C_def) apply (erule rev_finite_subset) using \0 < e\ - apply (auto simp: divide_simps) + apply (auto simp: field_split_simps) done then have "finite I" by (simp add: I_def) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Radon_Nikodym.thy --- a/src/HOL/Analysis/Radon_Nikodym.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Radon_Nikodym.thy Wed Oct 09 14:51:54 2019 +0000 @@ -89,7 +89,7 @@ show "summable (\n. (\x. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))) \M))" apply (rule summable_comparison_test'[of "\n. (1/2)^(Suc n)" 0], auto) using power_half_series summable_def apply auto[1] - apply (auto simp add: divide_simps) using measure_nonneg[of M] not_less by fastforce + apply (auto simp add: field_split_simps) using measure_nonneg[of M] not_less by fastforce qed define f where "f = (\x. if x \ space M then g x else 1)" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Riemann_Mapping.thy --- a/src/HOL/Analysis/Riemann_Mapping.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Riemann_Mapping.thy Wed Oct 09 14:51:54 2019 +0000 @@ -525,7 +525,7 @@ by (metis d1 dist_norm less_le_trans not_less not_less_iff_gr_or_eq segment_bound1 that(4)) qed (use \e > 0\ in auto) with \e > 0\ have "inverse (norm (y - x)) * norm (z - f x * (y - x)) \ e/2" - by (simp add: divide_simps) + by (simp add: field_split_simps) also have "... < e" using \e > 0\ by simp finally show ?thesis @@ -701,7 +701,7 @@ apply (rule 3) unfolding norm_divide using \r > 0\ g_not_r [OF \z \ S\] g_not_r [OF \a \ S\] - by (simp_all add: divide_simps dist_commute dist_norm) + by (simp_all add: field_split_simps dist_commute dist_norm) then show "?f ` S \ ball 0 1" by auto show "inj_on ?f S" @@ -945,9 +945,9 @@ then obtain n where n: "1 / (1 - norm x) < of_nat n" using reals_Archimedean2 by blast with \cmod x < 1\ gr0I have XX: "1 / of_nat n < 1 - norm x" and "n > 0" - by (fastforce simp: divide_simps algebra_simps)+ + by (fastforce simp: field_split_simps algebra_simps)+ have "f x \ f ` (D n)" - using n \cmod x < 1\ by (auto simp: divide_simps algebra_simps D_def) + using n \cmod x < 1\ by (auto simp: field_split_simps algebra_simps D_def) moreover have " f ` D n \ closure (f ` A n) = {}" proof - have op_fDn: "open(f ` (D n))" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Simplex_Content.thy --- a/src/HOL/Analysis/Simplex_Content.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Simplex_Content.thy Wed Oct 09 14:51:54 2019 +0000 @@ -252,7 +252,7 @@ ((a + b + c) - 2 * c)" unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps) also have "\ = 16 * s * (s - a) * (s - b) * (s - c)" - by (simp add: s_def divide_simps mult_ac) + by (simp add: s_def field_split_simps mult_ac) finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)" by simp also have "\ = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Starlike.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1221,7 +1221,7 @@ show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \ interior S" apply (clarsimp simp add: min_def a) apply (rule mem_interior_closure_convex_shrink [OF \convex S\ a x]) - using \0 < e\ False apply (auto simp: divide_simps) + using \0 < e\ False apply (auto simp: field_split_simps) done qed qed @@ -3433,7 +3433,7 @@ qed qed then show False - using \0 < e\ \l \ 0\ by (simp add: d_def [symmetric] divide_simps) + using \0 < e\ \l \ 0\ by (simp add: d_def [symmetric] field_simps) qed moreover have "a + d *\<^sub>R l \ closure S" proof (clarsimp simp: closure_approachable) @@ -3444,7 +3444,7 @@ have "norm l * min d (\ / (norm l * 2)) \ norm l * (\ / (norm l * 2))" by (metis min_def mult_left_mono norm_ge_zero order_refl) also have "... < \" - using \l \ 0\ \0 < \\ by (simp add: divide_simps) + using \l \ 0\ \0 < \\ by (simp add: field_simps) finally have 2: "norm l * min d (\ / (norm l * 2)) < \" . show "\y\S. dist y (a + d *\<^sub>R l) < \" apply (rule_tac x="a + (d - min d (\ / 2 / norm l)) *\<^sub>R l" in bexI) @@ -3498,7 +3498,7 @@ using xy apply (auto simp: in_segment) apply (rule_tac x="d" in exI) - using \0 < d\ that apply (auto simp: divide_simps algebra_simps) + using \0 < d\ that apply (auto simp: algebra_simps) done ultimately have "1 \ d" using df rel_frontier_def by fastforce @@ -3507,7 +3507,7 @@ ultimately show "y \ closed_segment x (x + d *\<^sub>R (y - x))" apply (auto simp: in_segment) apply (rule_tac x="1/d" in exI) - apply (auto simp: divide_simps algebra_simps) + apply (auto simp: algebra_simps) done next show "open_segment x (x + d *\<^sub>R (y - x)) \ rel_interior S" @@ -5972,7 +5972,7 @@ ultimately have ass: "a /\<^sub>R (norm a) \ span S \ sphere 0 1" by simp have aa: "a /\<^sub>R (norm a) \ (\c\C. {x. 0 \ c \ x})" - apply (clarsimp simp add: divide_simps) + apply (clarsimp simp add: field_split_simps) using ab \0 < b\ by (metis hull_inc inner_commute less_eq_real_def less_trans) show ?thesis @@ -7446,7 +7446,7 @@ by (intro closure_minimal UN_mono ball_subset_cball order_refl cl) also have "... \ (\x \ -S. \y\ball 0 (1 / (1 + real n)). {x + y})" apply (intro UN_mono order_refl) - apply (simp add: cball_subset_ball_iff divide_simps) + apply (simp add: cball_subset_ball_iff field_split_simps) done finally show "closure (\x\- S. \y\ball 0 (1 / (2 + real n)). {x + y}) \ (\x \ -S. \y\ball 0 (1 / (1 + real n)). {x + y})" . @@ -7463,7 +7463,7 @@ obtain N2 where N2: "norm(x - a) \ real N2" by (meson real_arch_simple) have N12: "inverse((N1 + N2) + 1) \ inverse(N1)" - using \N1 > 0\ by (auto simp: divide_simps) + using \N1 > 0\ by (auto simp: field_split_simps) have "x \ y + z" if "y \ S" "norm z < 1 / (1 + (real N1 + real N2))" for y z proof - have "e * real N1 < e * (1 + (real N1 + real N2))" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Summation_Tests.thy --- a/src/HOL/Analysis/Summation_Tests.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Summation_Tests.thy Wed Oct 09 14:51:54 2019 +0000 @@ -396,7 +396,7 @@ from this and \summable f\ have "summable (\n. p N * f N * inverse (p n))" by (rule summable_comparison_test_ev) from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl] - have "summable (\n. inverse (p n))" by (simp add: divide_simps) + have "summable (\n. inverse (p n))" by (simp add: field_split_simps) with divergent_p show False by contradiction qed @@ -757,7 +757,7 @@ fix r assume r: "0 < r" "ereal r < c" let ?l = "liminf (\n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))" have "?l = liminf (\n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))" - using r by (simp add: norm_mult norm_power divide_simps) + using r by (simp add: norm_mult norm_power field_split_simps) also from r have "\ = liminf (\n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)" by (intro Liminf_ereal_mult_right) simp_all also have "liminf (\n. ereal (norm (f n) / (norm (f (Suc n))))) = c" @@ -771,7 +771,7 @@ fix r assume r: "0 < r" "ereal r > c" let ?l = "limsup (\n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))" have "?l = limsup (\n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))" - using r by (simp add: norm_mult norm_power divide_simps) + using r by (simp add: norm_mult norm_power field_split_simps) also from r have "\ = limsup (\n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)" by (intro Limsup_ereal_mult_right) simp_all also have "limsup (\n. ereal (norm (f n) / (norm (f (Suc n))))) = c" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Tagged_Division.thy --- a/src/HOL/Analysis/Tagged_Division.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Tagged_Division.thy Wed Oct 09 14:51:54 2019 +0000 @@ -9,8 +9,6 @@ imports Topology_Euclidean_Space begin -term comm_monoid - lemma sum_Sigma_product: assumes "finite S" and "\i. i \ S \ finite (T i)" @@ -2337,13 +2335,14 @@ show "\?D0 \ cbox a b" apply (simp add: UN_subset_iff) apply (intro conjI allI ballI subset_box_imp) - apply (simp add: divide_simps zero_le_mult_iff aibi) - apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem) + apply (simp add: field_simps) + apply (auto intro: mult_right_mono aibi) + apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem intro: mult_right_mono) done next show "\K. K \ ?D0 \ interior K \ {} \ (\c d. K = cbox c d)" using \box a b \ {}\ - by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem) + by (clarsimp simp: box_eq_empty) (fastforce simp add: field_split_simps dest: PiE_mem) next have realff: "(real w) * 2^m < (real v) * 2^n \ w * 2^m < v * 2^n" for m n v w using of_nat_less_iff less_imp_of_nat_less by fastforce @@ -2359,7 +2358,9 @@ apply (drule_tac x=i in bspec, assumption) using \m\n\ realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"] apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff) - apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+ + apply (simp_all add: power_add) + apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc) + apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc) done then show "?K0(m,v) \ ?K0(n,w) \ ?K0(n,w) \ ?K0(m,v) \ interior(?K0(m,v)) \ interior(?K0(n,w)) = {}" by meson @@ -2387,7 +2388,7 @@ also have "... \ DIM('a) * (\ / (2 * real DIM('a)))" by (meson sum_bounded_above that) also have "... = \ / 2" - by (simp add: divide_simps) + by (simp add: field_split_simps) also have "... < \" by (simp add: \0 < \\) finally show ?thesis . @@ -2399,9 +2400,9 @@ using \x \ S\ \S \ cbox a b\ by blast obtain n where n: "norm (b - a) / 2^n < e" using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \0 < e\ - by (auto simp: divide_simps) + by (auto simp: field_split_simps) then have "norm (b - a) < e * 2^n" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) then have bai: "b \ i - a \ i < e * 2 ^ n" if "i \ Basis" for i proof - have "b \ i - a \ i \ norm (b - a)" @@ -2423,7 +2424,7 @@ x \ i \ a \ i + (real k + 1) * (b \ i - a \ i) / 2 ^ n)" proof cases case 1 then show ?thesis - by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \i \ Basis\ aibi) + by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps field_split_simps of_nat_diff \i \ Basis\ aibi) next case 2 then have abi_less: "a \ i < b \ i" @@ -2433,20 +2434,20 @@ proof (intro exI conjI) show "?k < 2 ^ n" using aibi xab \i \ Basis\ - by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box) + by (force simp: nat_less_iff floor_less_iff field_split_simps 2 mem_box) next have "a \ i + real ?k * (b \ i - a \ i) / 2 ^ n \ a \ i + (2 ^ n * (x \ i - a \ i) / (b \ i - a \ i)) * (b \ i - a \ i) / 2 ^ n" apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor) using aibi [OF \i \ Basis\] xab 2 - apply (simp_all add: \i \ Basis\ mem_box divide_simps) + apply (simp_all add: \i \ Basis\ mem_box field_split_simps) done also have "... = x \ i" - using abi_less by (simp add: divide_simps) + using abi_less by (simp add: field_split_simps) finally show "a \ i + real ?k * (b \ i - a \ i) / 2 ^ n \ x \ i" . next have "x \ i \ a \ i + (2 ^ n * (x \ i - a \ i) / (b \ i - a \ i)) * (b \ i - a \ i) / 2 ^ n" - using abi_less by (simp add: divide_simps algebra_simps) + using abi_less by (simp add: field_split_simps algebra_simps) also have "... \ a \ i + (real ?k + 1) * (b \ i - a \ i) / 2 ^ n" apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor) using aibi [OF \i \ Basis\] xab @@ -2467,7 +2468,8 @@ apply (drule bspec D, assumption)+ apply (erule order_trans) apply (simp add: divide_simps) - using bai by (force simp: algebra_simps) + using bai apply (force simp add: algebra_simps) + done ultimately show ?thesis by auto qed qed @@ -2486,12 +2488,12 @@ proof - have dd: "w / m \ v / n \ (v+1) / n \ (w+1) / m \ inverse n \ inverse m" for w m v n::real - by (auto simp: divide_simps algebra_simps) + by (auto simp: field_split_simps algebra_simps) have bjaj: "b \ j - a \ j > 0" using \j \ Basis\ \box a b \ {}\ box_eq_empty(1) by fastforce have "((g j) / 2 ^ m) * (b \ j - a \ j) \ ((f j) / 2 ^ n) * (b \ j - a \ j) \ (((f j) + 1) / 2 ^ n) * (b \ j - a \ j) \ (((g j) + 1) / 2 ^ m) * (b \ j - a \ j)" - using that \j \ Basis\ by (simp add: subset_box algebra_simps divide_simps aibi) + using that \j \ Basis\ by (simp add: subset_box algebra_simps field_split_simps aibi) then have "((g j) / 2 ^ m) \ ((f j) / 2 ^ n) \ ((real(f j) + 1) / 2 ^ n) \ ((real(g j) + 1) / 2 ^ m)" by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Oct 09 14:51:54 2019 +0000 @@ -66,7 +66,7 @@ have "sqrt ((representation B x b)\<^sup>2 * (norm b)\<^sup>2) \ sqrt (\b\B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)" using \b \ B\ \finite B\ by (auto intro: member_le_sum) then have "\representation B x b\ \ (1 / norm b) * sqrt (\b\B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)" - using \b \ 0\ by (simp add: divide_simps real_sqrt_mult del: real_sqrt_le_iff) + using \b \ 0\ by (simp add: field_split_simps real_sqrt_mult del: real_sqrt_le_iff) ultimately show "\representation B x b\ \ (1 / norm b) * norm x" by simp next @@ -2028,7 +2028,7 @@ lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)" proof - have "{a .. b} = cball ((a+b)/2) ((b-a)/2)" - by (auto simp: dist_norm abs_if divide_simps split: if_split_asm) + by (auto simp: dist_norm abs_if field_split_simps split: if_split_asm) then show ?thesis by simp qed @@ -2036,7 +2036,7 @@ lemma diameter_open_interval [simp]: "diameter {a<..e>0. \y. dist y (f x) < e \ y \ f ` A" proof (intro exI conjI) show "\ > 0" - using \e > 0\ \B > 0\ by (simp add: \_def divide_simps) + using \e > 0\ \B > 0\ by (simp add: \_def field_split_simps) have "y \ f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y proof - define u where "u \ y - f x" @@ -2095,7 +2095,7 @@ qed then show "\y. dist y (f x) < \ \ y \ f ` A" using \e > 0\ \B > 0\ - by (auto simp: \_def divide_simps mult_less_0_iff) + by (auto simp: \_def field_split_simps mult_less_0_iff) qed qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Uniform_Limit.thy --- a/src/HOL/Analysis/Uniform_Limit.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Uniform_Limit.thy Wed Oct 09 14:51:54 2019 +0000 @@ -596,7 +596,7 @@ using \e > 0\ that b [OF \y \ S\] apply (simp add: power2_eq_square) by (metis \b > 0\ less_eq_real_def mult.left_commute mult_mono') finally show ?thesis - by (auto simp: dist_norm divide_simps norm_mult norm_divide) + by (auto simp: dist_norm field_split_simps norm_mult norm_divide) qed have "\\<^sub>F n in F. \x\S. dist (f n x) (l x) < b/2" using uniform_limitD [OF f, of "b/2"] by (simp add: \b > 0\) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Vitali_Covering_Theorem.thy --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy Wed Oct 09 14:51:54 2019 +0000 @@ -99,7 +99,7 @@ proof assume "i \ C" have "B/2 ^ Suc n \ B/2 ^ n" - using \B > 0\ by (simp add: divide_simps) + using \B > 0\ by (simp add: field_split_simps) also have "\ \ r i" using Ble \i \ C\ by blast finally show ?thesis . @@ -224,7 +224,7 @@ then obtain n where "(1/2) ^ n < r i / B" using \B > 0\ assms real_arch_pow_inv by fastforce then have B2: "B/2 ^ n < r i" - using \B > 0\ by (simp add: divide_simps) + using \B > 0\ by (simp add: field_split_simps) have "0 < r i" "r i \ B" by (auto simp: \i \ K\ assms) show "\j. j \ (Union(range F)) \ @@ -467,7 +467,7 @@ by simp qed ultimately show ?thesis - by (simp add: divide_simps) + by (simp add: field_split_simps) qed have co: "countable (D - D1)" by (simp add: \countable D\) @@ -576,7 +576,7 @@ using ball_subset_ball_iff k by auto finally show "ball x r \ ball z 1" . have "?\ * ?\ (ball x r) \ e * content (ball x r) / content (ball z 1)" - using r \e > 0\ by (simp add: ord_class.min_def divide_simps) + using r \e > 0\ by (simp add: ord_class.min_def field_split_simps) with mU show "?\ U < e * content (ball x r) / content (ball z 1)" by auto qed (use r U x in auto) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Weierstrass_Theorems.thy --- a/src/HOL/Analysis/Weierstrass_Theorems.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Wed Oct 09 14:51:54 2019 +0000 @@ -110,12 +110,12 @@ then have "(\k\n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n" by (simp add: power2_eq_square) then show ?thesis - using n by (simp add: sum_divide_distrib divide_simps mult.commute power2_commute) + using n by (simp add: sum_divide_distrib field_split_simps mult.commute power2_commute) qed { fix k assume k: "k \ n" then have kn: "0 \ k / n" "k / n \ 1" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) consider (lessd) "\x - k / n\ < d" | (ged) "d \ \x - k / n\" by linarith then have "\(f x - f (k/n))\ \ e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2" @@ -158,7 +158,7 @@ also have "... < e" apply (simp add: field_simps) using \d>0\ nbig e \n>0\ - apply (simp add: divide_simps algebra_simps) + apply (simp add: field_split_simps algebra_simps) using ed0 by linarith finally have "\f x - (\k\n. f (real k / real n) * Bernstein n k x)\ < e" . } @@ -282,7 +282,7 @@ obtain i where i: "i \ subU" "t \ Uf i" using subU t by blast show ?thesis using subU i t - apply (clarsimp simp: p_def divide_simps) + apply (clarsimp simp: p_def field_split_simps) apply (rule sum_pos2 [OF \finite subU\]) using Uf t pf01 apply auto apply (force elim!: subsetCE) @@ -292,12 +292,12 @@ proof - have "0 \ p x" using subU cardp t - apply (simp add: p_def divide_simps sum_nonneg) + apply (simp add: p_def field_split_simps sum_nonneg) apply (rule sum_nonneg) using pf01 by force moreover have "p x \ 1" using subU cardp t - apply (simp add: p_def divide_simps sum_nonneg) + apply (simp add: p_def field_split_simps sum_nonneg) apply (rule sum_bounded_above [where 'a=real and K=1, simplified]) using pf01 by force ultimately show ?thesis @@ -331,12 +331,12 @@ with \01 have "k \ (1+\)/\" by (auto simp: algebra_simps add_divide_distrib) also have "... < 2/\" - using \01 by (auto simp: divide_simps) + using \01 by (auto simp: field_split_simps) finally have k2\: "k < 2/\" . have "1/\ < k" using \01 unfolding k_def by linarith with \01 k2\ have k\: "1 < k*\" "k*\ < 2" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) define q where [abs_def]: "q n t = (1 - p t ^ n) ^ (k^n)" for n t have qR: "q n \ R" for n by (simp add: q_def const diff power pR) @@ -484,12 +484,12 @@ proof - have "0 \ pff x" using subA cardp t - apply (simp add: pff_def divide_simps sum_nonneg) + apply (simp add: pff_def field_split_simps sum_nonneg) apply (rule Groups_Big.linordered_semidom_class.prod_nonneg) using ff by fastforce moreover have "pff x \ 1" using subA cardp t - apply (simp add: pff_def divide_simps sum_nonneg) + apply (simp add: pff_def field_split_simps sum_nonneg) apply (rule prod_mono [where g = "\x. 1", simplified]) using ff by fastforce ultimately show ?thesis @@ -512,7 +512,7 @@ using ff [THEN conjunct2, THEN conjunct2, THEN conjunct1] v subA x by auto also have "... \ e" - using cardp e by (simp add: divide_simps) + using cardp e by (simp add: field_split_simps) finally have "pff x < e" . } then have "\x. x \ A \ pff x < e" @@ -532,7 +532,7 @@ apply (rule prod_mono_strict [where f = "\x. 1 - e / card subA", simplified]) apply (simp_all add: subA(2)) apply (intro ballI conjI) - using e apply (force simp: divide_simps) + using e apply (force simp: field_split_simps) using ff [THEN conjunct2, THEN conjunct2, THEN conjunct2] subA B x apply blast done diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Winding_Numbers.thy --- a/src/HOL/Analysis/Winding_Numbers.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/Winding_Numbers.thy Wed Oct 09 14:51:54 2019 +0000 @@ -997,15 +997,17 @@ fix t :: "real" assume t: "t \ {0..1}" show "vector_derivative (exp \ g) (at t) / exp (g t) = vector_derivative g (at t)" - proof (simp add: divide_simps, rule vector_derivative_unique_at) - show "(exp \ g has_vector_derivative vector_derivative (exp \ g) (at t)) (at t)" + proof - + have "(exp \ g has_vector_derivative vector_derivative (exp \ g) (at t)) (at t)" by (meson DERIV_exp differentiable_def field_vector_diff_chain_at has_vector_derivative_def has_vector_derivative_polynomial_function pfg vector_derivative_works) - show "(exp \ g has_vector_derivative vector_derivative g (at t) * exp (g t)) (at t)" + moreover have "(exp \ g has_vector_derivative vector_derivative g (at t) * exp (g t)) (at t)" apply (rule field_vector_diff_chain_at) apply (metis has_vector_derivative_polynomial_function pfg vector_derivative_at) using DERIV_exp has_field_derivative_def apply blast done + ultimately show ?thesis + by (simp add: divide_simps, rule vector_derivative_unique_at) qed qed also have "... = (pathfinish p - pathstart p) / (2 * of_real pi * \)" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/ex/Approximations.thy --- a/src/HOL/Analysis/ex/Approximations.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Analysis/ex/Approximations.thy Wed Oct 09 14:51:54 2019 +0000 @@ -114,7 +114,7 @@ from assms have "(\k. (x^n / fact n) * (x / 2)^k) sums ((x^n / fact n) * (1 / (1 - x / 2)))" by (intro sums_mult geometric_sums) simp_all also from assms have "((x^n / fact n) * (1 / (1 - x / 2))) = (2 * x^n / (2 - x)) / fact n" - by (auto simp: divide_simps) + by (auto simp: field_split_simps) finally have "(\k. (x^n / fact n) * (x / 2)^k) sums \" . } ultimately show "(exp x - approx) \ (2 * x^n / (2 - x)) / fact n" @@ -130,7 +130,7 @@ proof - from assms have "x^n / (2 - x) \ x^n / 1" by (intro frac_le) simp_all hence "(2 * x^n / (2 - x)) / fact n \ 2 * x^n / fact n" - using assms by (simp add: divide_simps) + using assms by (simp add: field_split_simps) with exp_approx[of n x] assms have "exp (x::real) - (\k {0..2 * x^n / fact n}" by simp moreover have "(\k\n. x^k / fact k) = (\kexp x - (\k\n. x ^ k / fact k)\ \ x ^ n / fact n" by (rule exp_approx') - also from assms have "\ \ 1 / fact n" by (simp add: divide_simps power_le_one) + also from assms have "\ \ 1 / fact n" by (simp add: field_split_simps power_le_one) finally show ?thesis . qed @@ -169,7 +169,7 @@ lemma exp_1_approx: "n > 0 \ \exp (1::real) - euler_approx n\ \ 1 / fact n" - using exp_approx''[of n 1] by (simp add: euler_approx_def divide_simps) + using exp_approx''[of n 1] by (simp add: euler_approx_def field_split_simps) text \ The following allows us to compute the numerator and the denominator of the result @@ -282,7 +282,7 @@ also have "2 * y * (\k2 ^ k) = (\k {-?l..?u1 + ?u2}") apply ((rule combine_bounds(1,2))+; (rule combine_bounds(3); (rule arctan_approx)?)?) apply (simp_all add: n) - apply (simp_all add: divide_simps)? + apply (simp_all add: field_split_simps)? done also { have "?l \ (1/8) * (1/2)^(46*n)" - unfolding power_mult by (intro mult_mono power_mono) (simp_all add: divide_simps) + unfolding power_mult by (intro mult_mono power_mono) (simp_all add: field_split_simps) also have "\ \ (1/2) ^ (46 * n - 1)" - by (cases n; simp_all add: power_add divide_simps) + by (cases n; simp_all add: power_add field_split_simps) finally have "?l \ (1/2) ^ (46 * n - 1)" . moreover { have "?u1 + ?u2 \ 4 * (1/2)^(48*n) + 1 * (1/2)^(46*n)" - unfolding power_mult by (intro add_mono mult_mono power_mono) (simp_all add: divide_simps) + unfolding power_mult by (intro add_mono mult_mono power_mono) (simp_all add: field_split_simps) also from \n > 0\ have "4 * (1/2::real)^(48*n) \ (1/2)^(46*n)" by (cases n) (simp_all add: field_simps power_add) also from \n > 0\ have "(1/2::real) ^ (46 * n) + 1 * (1 / 2) ^ (46 * n) = (1/2) ^ (46 * n - 1)" @@ -650,7 +650,7 @@ by (subst atLeastatMost_subset_iff) simp_all } finally have "\pi - pi_approx2 n\ \ ((1/2) ^ (46 * n - 1))" by auto - thus ?thesis by (simp add: divide_simps) + thus ?thesis by (simp add: field_split_simps) qed lemma pi_approx2': diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Complex.thy --- a/src/HOL/Complex.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Complex.thy Wed Oct 09 14:51:54 2019 +0000 @@ -92,8 +92,7 @@ by (simp add: divide_complex_def add_divide_distrib) lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)" - unfolding divide_complex_def times_complex.sel inverse_complex.sel - by (simp add: divide_simps) + by (simp add: divide_complex_def diff_divide_distrib) lemma Complex_divide: "(x / y) = Complex ((Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)) @@ -184,10 +183,10 @@ by (simp add: Im_divide sqr_conv_mult) lemma Re_divide_of_nat [simp]: "Re (z / of_nat n) = Re z / of_nat n" - by (cases n) (simp_all add: Re_divide divide_simps power2_eq_square del: of_nat_Suc) + by (cases n) (simp_all add: Re_divide field_split_simps power2_eq_square del: of_nat_Suc) lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n" - by (cases n) (simp_all add: Im_divide divide_simps power2_eq_square del: of_nat_Suc) + by (cases n) (simp_all add: Im_divide field_split_simps power2_eq_square del: of_nat_Suc) lemma of_real_Re [simp]: "z \ \ \ of_real (Re z) = z" by (auto simp: Reals_def) @@ -397,7 +396,7 @@ done lemma complex_unit_circle: "z \ 0 \ (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1" - by (simp add: norm_complex_def divide_simps complex_eq_iff) + by (simp add: norm_complex_def complex_eq_iff power2_eq_square add_divide_distrib [symmetric]) text \Properties of complex signum.\ @@ -1043,7 +1042,8 @@ then obtain m :: int where "2 * pi * (real k - real l) / real n = real_of_int m * 2 * pi" by (subst (asm) cos_one_2pi_int) blast hence "real_of_int (int k - int l) = real_of_int (m * int n)" - unfolding of_int_diff of_int_mult using assms by (simp add: divide_simps) + unfolding of_int_diff of_int_mult using assms + by (simp add: nonzero_divide_eq_eq) also note of_int_eq_iff finally have *: "abs m * n = abs (int k - int l)" by (simp add: abs_mult) also have "\ < int n" using kl by linarith diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Computational_Algebra/Computational_Algebra.thy --- a/src/HOL/Computational_Algebra/Computational_Algebra.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Computational_Algebra/Computational_Algebra.thy Wed Oct 09 14:51:54 2019 +0000 @@ -19,4 +19,3 @@ begin end - diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Computational_Algebra/Field_as_Ring.thy --- a/src/HOL/Computational_Algebra/Field_as_Ring.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy Wed Oct 09 14:51:54 2019 +0000 @@ -35,7 +35,7 @@ instance by standard - (simp_all add: dvd_field_iff divide_simps split: if_splits) + (simp_all add: dvd_field_iff field_split_simps split: if_splits) end @@ -66,7 +66,7 @@ instance by standard - (simp_all add: dvd_field_iff divide_simps split: if_splits) + (simp_all add: dvd_field_iff field_split_simps split: if_splits) end @@ -97,7 +97,7 @@ instance by standard - (simp_all add: dvd_field_iff divide_simps split: if_splits) + (simp_all add: dvd_field_iff field_split_simps split: if_splits) end diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Computational_Algebra/Formal_Laurent_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Oct 09 14:51:54 2019 +0000 @@ -2832,26 +2832,25 @@ qed lemma fls_lr_inverse_power_divring: - fixes f :: "'a::division_ring fls" - shows "fls_left_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = - (fls_left_inverse f (inverse (f $$ fls_subdegree f))) ^ n" - "fls_right_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = - (fls_right_inverse f (inverse (f $$ fls_subdegree f))) ^ n" + "fls_left_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = + (fls_left_inverse f (inverse (f $$ fls_subdegree f))) ^ n" (is ?P) + and "fls_right_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = + (fls_right_inverse f (inverse (f $$ fls_subdegree f))) ^ n" (is ?Q) + for f :: "'a::division_ring fls" proof - - have + note fls_left_inverse_eq_inverse [of f] fls_right_inverse_eq_inverse[of f] + moreover have "fls_right_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = inverse f ^ n" + using fls_right_inverse_eq_inverse [of "f ^ n"] + by (simp add: fls_subdegree_pow power_inverse) + moreover have "fls_left_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = inverse f ^ n" - using fls_left_inverse_eq_inverse[of "f^n"] fls_right_inverse_eq_inverse[of "f^n"] - by (auto simp add: divide_simps fls_subdegree_pow) - thus - "fls_left_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = - (fls_left_inverse f (inverse (f $$ fls_subdegree f))) ^ n" - "fls_right_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = - (fls_right_inverse f (inverse (f $$ fls_subdegree f))) ^ n" - using fls_left_inverse_eq_inverse[of f] fls_right_inverse_eq_inverse[of f] - by auto + using fls_left_inverse_eq_inverse [of "f ^ n"] + by (simp add: fls_subdegree_pow power_inverse) + ultimately show ?P and ?Q + by simp_all qed instance fls :: (field) field diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Computational_Algebra/Formal_Power_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1489,7 +1489,7 @@ have "dist (?s n) a < r" if nn0: "n \ n0" for n proof - from that have thnn0: "(1/2)^n \ (1/2 :: real)^n0" - by (simp add: divide_simps) + by (simp add: field_split_simps) show ?thesis proof (cases "?s n = a") case True @@ -1505,7 +1505,7 @@ then have "dist (?s n) a < (1/2)^n" by (simp add: field_simps dist_fps_def) also have "\ \ (1/2)^n0" - using nn0 by (simp add: divide_simps) + using nn0 by (simp add: field_split_simps) also have "\ < r" using n0 by simp finally show ?thesis . diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Decision_Procs/Approximation_Bounds.thy --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Wed Oct 09 14:51:54 2019 +0000 @@ -305,7 +305,7 @@ case (Float m e) hence "0 < m" using assms - by (auto simp: sign_simps) + by (auto simp: algebra_split_simps) hence "0 < sqrt m" by auto have int_nat_bl: "(nat (bitlen m)) = bitlen m" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Fields.thy --- a/src/HOL/Fields.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Fields.thy Wed Oct 09 14:51:54 2019 +0000 @@ -87,7 +87,6 @@ lemmas [arith_split] = nat_diff_split split_min split_max - text\Lemmas \divide_simps\ move division to the outside and eliminates them on (in)equalities.\ named_theorems divide_simps "rewrite rules to eliminate divisions" @@ -198,7 +197,7 @@ lemma divide_self [simp]: "a \ 0 \ a / a = 1" by (simp add: divide_inverse) -lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a" +lemma inverse_eq_divide [field_simps, field_split_simps, divide_simps]: "inverse a = 1 / a" by (simp add: divide_inverse) lemma add_divide_distrib: "(a+b) / c = a/c + b/c" @@ -332,7 +331,7 @@ by (cases "b = 0 \ c = 0") (auto simp: divide_inverse mult.assoc nonzero_inverse_mult_distrib) -lemma add_divide_eq_if_simps [divide_simps]: +lemma add_divide_eq_if_simps [field_split_simps, divide_simps]: "a + b / z = (if z = 0 then a else (a * z + b) / z)" "a / z + b = (if z = 0 then b else (a + b * z) / z)" "- (a / z) + b = (if z = 0 then b else (-a + b * z) / z)" @@ -342,7 +341,7 @@ by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff minus_divide_diff_eq_iff) -lemma [divide_simps]: +lemma [field_split_simps, divide_simps]: shows divide_eq_eq: "b / c = a \ (if c \ 0 then b = a * c else a = 0)" and eq_divide_eq: "a = b / c \ (if c \ 0 then a * c = b else a = 0)" and minus_divide_eq_eq: "- (b / c) = a \ (if c \ 0 then - b = a * c else a = 0)" @@ -1096,7 +1095,7 @@ lemma inverse_le_1_iff: "inverse x \ 1 \ x \ 0 \ 1 \ x" by (simp add: not_less [symmetric] one_less_inverse_iff) -lemma [divide_simps]: +lemma [field_split_simps, divide_simps]: shows le_divide_eq: "a \ b / c \ (if 0 < c then a * c \ b else if c < 0 then b \ a * c else a \ 0)" and divide_le_eq: "b / c \ a \ (if 0 < c then b \ a * c else if c < 0 then a * c \ b else 0 \ a)" and less_divide_eq: "a < b / c \ (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)" @@ -1114,7 +1113,7 @@ and divide_less_0_iff: "a / b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" and zero_le_divide_iff: "0 \ a / b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0" and divide_le_0_iff: "a / b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b" - by (auto simp add: divide_simps) + by (auto simp add: field_split_simps) text \Division and the Number One\ @@ -1193,19 +1192,19 @@ lemma divide_nonneg_nonneg [simp]: "0 \ x \ 0 \ y \ 0 \ x / y" - by (auto simp add: divide_simps) + by (auto simp add: field_split_simps) lemma divide_nonpos_nonpos: "x \ 0 \ y \ 0 \ 0 \ x / y" - by (auto simp add: divide_simps) + by (auto simp add: field_split_simps) lemma divide_nonneg_nonpos: "0 \ x \ y \ 0 \ x / y \ 0" - by (auto simp add: divide_simps) + by (auto simp add: field_split_simps) lemma divide_nonpos_nonneg: "x \ 0 \ 0 \ y \ x / y \ 0" - by (auto simp add: divide_simps) + by (auto simp add: field_split_simps) text \Conditional Simplification Rules: No Case Splits\ diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Groups.thy --- a/src/HOL/Groups.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Groups.thy Wed Oct 09 14:51:54 2019 +0000 @@ -16,8 +16,9 @@ named_theorems ac_simps "associativity and commutativity simplification rules" and algebra_simps "algebra simplification rules for rings" + and algebra_split_simps "algebra simplification rules for rings, with potential goal splitting" and field_simps "algebra simplification rules for fields" - and sign_simps "algebra simplification rules for comparision with zero" + and field_split_simps "algebra simplification rules for fields, with potential goal splitting" text \ The rewrites accumulated in \algebra_simps\ deal with the classical @@ -34,9 +35,9 @@ inequalities). Can be too aggressive and is therefore separate from the more benign \algebra_simps\. - Lemmas \sign_simps\ is a first attempt to automate proofs - of positivity/negativity needed for \field_simps\. Have not added \sign_simps\ to \field_simps\ - because the former can lead to case explosions. + Collections \algebra_split_simps\ and \field_split_simps\ + correspond to \algebra_simps\ and \field_simps\ + but contain more aggresive rules that may lead to goal splitting. \ @@ -206,7 +207,8 @@ subsection \Semigroups and Monoids\ class semigroup_add = plus + - assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" + assumes add_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "(a + b) + c = a + (b + c)" begin sublocale add: semigroup plus @@ -217,13 +219,14 @@ hide_fact add_assoc class ab_semigroup_add = semigroup_add + - assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" + assumes add_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a + b = b + a" begin sublocale add: abel_semigroup plus by standard (fact add_commute) -declare add.left_commute [algebra_simps, field_simps] +declare add.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps] lemmas add_ac = add.assoc add.commute add.left_commute @@ -234,7 +237,8 @@ lemmas add_ac = add.assoc add.commute add.left_commute class semigroup_mult = times + - assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" + assumes mult_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "(a * b) * c = a * (b * c)" begin sublocale mult: semigroup times @@ -245,13 +249,14 @@ hide_fact mult_assoc class ab_semigroup_mult = semigroup_mult + - assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" + assumes mult_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a * b = b * a" begin sublocale mult: abel_semigroup times by standard (fact mult_commute) -declare mult.left_commute [algebra_simps, field_simps] +declare mult.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps] lemmas mult_ac = mult.assoc mult.commute mult.left_commute @@ -326,7 +331,8 @@ class cancel_ab_semigroup_add = ab_semigroup_add + minus + assumes add_diff_cancel_left' [simp]: "(a + b) - a = b" - assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)" + assumes diff_diff_add [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a - b - c = a - (b + c)" begin lemma add_diff_cancel_right' [simp]: "(a + b) - b = a" @@ -547,19 +553,23 @@ lemma minus_diff_eq [simp]: "- (a - b) = b - a" by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp -lemma add_diff_eq [algebra_simps, field_simps]: "a + (b - c) = (a + b) - c" +lemma add_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a + (b - c) = (a + b) - c" by (simp only: diff_conv_add_uminus add.assoc) lemma diff_add_eq_diff_diff_swap: "a - (b + c) = a - c - b" by (simp only: diff_conv_add_uminus add.assoc minus_add) -lemma diff_eq_eq [algebra_simps, field_simps]: "a - b = c \ a = c + b" +lemma diff_eq_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a - b = c \ a = c + b" by auto -lemma eq_diff_eq [algebra_simps, field_simps]: "a = c - b \ a + b = c" +lemma eq_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a = c - b \ a + b = c" by auto -lemma diff_diff_eq2 [algebra_simps, field_simps]: "a - (b - c) = (a + c) - b" +lemma diff_diff_eq2 [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a - (b - c) = (a + c) - b" by (simp only: diff_conv_add_uminus add.assoc) simp lemma diff_eq_diff_eq: "a - b = c - d \ a = b \ c = d" @@ -592,7 +602,8 @@ lemma minus_add_distrib [simp]: "- (a + b) = - a + - b" by (simp add: algebra_simps) -lemma diff_add_eq [algebra_simps, field_simps]: "(a - b) + c = (a + c) - b" +lemma diff_add_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "(a - b) + c = (a + c) - b" by (simp add: algebra_simps) end @@ -938,13 +949,15 @@ lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric] -lemma diff_less_eq [algebra_simps, field_simps]: "a - b < c \ a < c + b" +lemma diff_less_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a - b < c \ a < c + b" apply (subst less_iff_diff_less_0 [of a]) apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) apply (simp add: algebra_simps) done -lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \ a + b < c" +lemma less_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a < c - b \ a + b < c" apply (subst less_iff_diff_less_0 [of "a + b"]) apply (subst less_iff_diff_less_0 [of a]) apply (simp add: algebra_simps) @@ -953,10 +966,12 @@ lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \ a > b" by (simp add: less_diff_eq) -lemma diff_le_eq [algebra_simps, field_simps]: "a - b \ c \ a \ c + b" +lemma diff_le_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a - b \ c \ a \ c + b" by (auto simp add: le_less diff_less_eq ) -lemma le_diff_eq [algebra_simps, field_simps]: "a \ c - b \ a + b \ c" +lemma le_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]: + "a \ c - b \ a + b \ c" by (auto simp add: le_less less_diff_eq) lemma diff_le_0_iff_le [simp]: "a - b \ 0 \ a \ b" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Homology/Simplices.thy --- a/src/HOL/Homology/Simplices.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Homology/Simplices.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1229,7 +1229,7 @@ by simp with False show "(\j\p. x (Suc j) * inverse (1 - x 0)) = 1" by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero right_inverse sum_distrib_right) - qed (use x01 x0 xle \x 0 < 1\ in \auto simp: divide_simps\) + qed (use x01 x0 xle \x 0 < 1\ in \auto simp: field_split_simps\) then show "(\i. inverse (1 - x 0) * (\j\p. l j i * x (Suc j))) \ S" by (simp add: field_simps sum_divide_distrib) qed (use x01 in auto) @@ -1448,11 +1448,11 @@ have "(\i. \j\Suc p. l j i * ((if j \ Suc p then (1 - u) * inverse (p + 2) + u * x j else 0))) \ S" proof (rule l) have i2p: "inverse (2 + real p) \ 1" - by (simp add: divide_simps) + by (simp add: field_split_simps) show "(\j. if j \ Suc p then (1 - u) * inverse (real (p + 2)) + u * x j else 0) \ standard_simplex (Suc p)" using x \0 \ u\ \u \ 1\ apply (simp add: sum.distrib standard_simplex_def i2p linepath_le_1 flip: sum_distrib_left del: sum.atMost_Suc) - apply (simp add: divide_simps) + apply (simp add: field_split_simps) done qed moreover have "(\i. \j\Suc p. l j i * ((1 - u) * inverse (2 + real p) + u * x j)) @@ -1604,7 +1604,7 @@ done show "\l i k - l i' k\ / real (p + 2) \ (1 + real p) * d / real (p + 2) / real (card ({..Suc p} - {i}))" using i i' lf [of i] lf [of i'] 2 - by (auto simp: divide_simps image_iff) + by (auto simp: image_iff divide_simps) qed auto finally have "(\j\Suc p. \l i k / (p + 2) - l j k / (p + 2)\) \ (1 + real p) * d / (p + 2)" . then have "\\j\Suc p. l i k / (p + 2) - l j k / (p + 2)\ \ (1 + real p) * d / (p + 2)" @@ -1810,7 +1810,7 @@ \ standard_simplex (Suc p)" by (simp add: simplicial_vertex_def standard_simplex_def del: sum.atMost_Suc) have ss_Sp: "(\i. (if i \ Suc p then 1 else 0) / (real p + 2)) \ standard_simplex (Suc p)" - by (simp add: standard_simplex_def divide_simps) + by (simp add: standard_simplex_def field_split_simps) obtain l where feq: "f = oriented_simplex (Suc p) l" using one unfolding simplicial_simplex by blast then have 3: "f (\i. (\j\Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2)) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Library/Float.thy Wed Oct 09 14:51:54 2019 +0000 @@ -492,13 +492,13 @@ qed lemma mantissa_pos_iff: "0 < mantissa x \ 0 < x" - by (auto simp: mantissa_exponent sign_simps) + by (auto simp: mantissa_exponent algebra_split_simps) lemma mantissa_nonneg_iff: "0 \ mantissa x \ 0 \ x" - by (auto simp: mantissa_exponent sign_simps) + by (auto simp: mantissa_exponent algebra_split_simps) lemma mantissa_neg_iff: "0 > mantissa x \ 0 > x" - by (auto simp: mantissa_exponent sign_simps) + by (auto simp: mantissa_exponent algebra_split_simps) lemma fixes m e :: int @@ -1139,7 +1139,7 @@ auto intro!: floor_eq2 intro: powr_strict powr - simp: powr_diff powr_add divide_simps algebra_simps)+ + simp: powr_diff powr_add field_split_simps algebra_simps)+ finally show ?thesis by simp qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Library/Landau_Symbols.thy --- a/src/HOL/Library/Landau_Symbols.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Library/Landau_Symbols.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1833,7 +1833,7 @@ by (rule asymp_equivD) from order_tendstoD(1)[OF this zero_less_one] show ?th1 ?th2 ?th3 - by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+ + by (eventually_elim; force simp: sgn_if field_split_simps split: if_splits)+ qed lemma asymp_equiv_tendsto_transfer: @@ -1900,7 +1900,7 @@ have ev: "eventually (\x. g x = 0 \ h x = 0) F" by eventually_elim auto have "(\x. f x + h x) \[F] g \ ((\x. ?T f g x + h x / g x) \ 1) F" unfolding asymp_equiv_def using ev - by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps) + by (intro tendsto_cong) (auto elim!: eventually_mono simp: field_split_simps) also have "\ \ ((\x. ?T f g x + h x / g x) \ 1 + 0) F" by simp also have \ by (intro tendsto_intros asymp_equivD assms smalloD_tendsto) finally show "(\x. f x + h x) \[F] g" . @@ -2154,7 +2154,7 @@ proof eventually_elim case (elim x) from elim have "norm (f x - g x) \ norm (f x / g x - 1) * norm (g x)" - by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps) + by (subst norm_mult [symmetric]) (auto split: if_splits simp add: algebra_simps) also have "norm (f x / g x - 1) * norm (g x) \ c * norm (g x)" using elim by (auto split: if_splits simp: mult_right_mono) finally show ?case . diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Library/Nonpos_Ints.thy --- a/src/HOL/Library/Nonpos_Ints.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Library/Nonpos_Ints.thy Wed Oct 09 14:51:54 2019 +0000 @@ -265,7 +265,7 @@ apply (auto intro: nonpos_Reals_mult_I2) apply (auto simp: nonpos_Reals_def) apply (rule_tac x="r/n" in exI) - apply (auto simp: divide_simps) + apply (auto simp: field_split_simps) done lemma nonpos_Reals_inverse_I: @@ -288,7 +288,7 @@ apply (auto intro: nonpos_Reals_divide_I2) apply (auto simp: nonpos_Reals_def) apply (rule_tac x="r*n" in exI) - apply (auto simp: divide_simps mult_le_0_iff) + apply (auto simp: field_split_simps mult_le_0_iff) done lemma nonpos_Reals_inverse_iff [simp]: diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Limits.thy --- a/src/HOL/Limits.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Limits.thy Wed Oct 09 14:51:54 2019 +0000 @@ -285,7 +285,7 @@ with Bfun_const have "Bseq (\x. inverse c * (c * f x))" by (rule Bseq_mult) with \c \ 0\ show "Bseq f" - by (simp add: divide_simps) + by (simp add: field_split_simps) qed (intro Bseq_mult Bfun_const) lemma Bseq_subseq: "Bseq f \ Bseq (\x. f (g x))" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/MacLaurin.thy Wed Oct 09 14:51:54 2019 +0000 @@ -57,7 +57,7 @@ by (rule nonzero_divide_eq_eq[THEN iffD2]) auto moreover have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))" - using \0 < n - m\ by (simp add: divide_simps fact_reduce) + using \0 < n - m\ by (simp add: field_split_simps fact_reduce) ultimately show "DERIV (difg m) t :> difg (Suc m) t" unfolding difg_def by (simp add: mult.commute) qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Modules.thy --- a/src/HOL/Modules.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Modules.thy Wed Oct 09 14:51:54 2019 +0000 @@ -48,8 +48,10 @@ spaces by replacing the scalar field by a scalar ring.\ locale module = fixes scale :: "'a::comm_ring_1 \ 'b::ab_group_add \ 'b" (infixr "*s" 75) - assumes scale_right_distrib [algebra_simps]: "a *s (x + y) = a *s x + a *s y" - and scale_left_distrib [algebra_simps]: "(a + b) *s x = a *s x + b *s x" + assumes scale_right_distrib [algebra_simps, algebra_split_simps]: + "a *s (x + y) = a *s x + a *s y" + and scale_left_distrib [algebra_simps, algebra_split_simps]: + "(a + b) *s x = a *s x + b *s x" and scale_scale [simp]: "a *s (b *s x) = (a * b) *s x" and scale_one [simp]: "1 *s x = x" begin @@ -59,7 +61,8 @@ lemma scale_zero_left [simp]: "0 *s x = 0" and scale_minus_left [simp]: "(- a) *s x = - (a *s x)" - and scale_left_diff_distrib [algebra_simps]: "(a - b) *s x = a *s x - b *s x" + and scale_left_diff_distrib [algebra_simps, algebra_split_simps]: + "(a - b) *s x = a *s x - b *s x" and scale_sum_left: "(sum f A) *s x = (\a\A. (f a) *s x)" proof - interpret s: additive "\a. a *s x" @@ -72,7 +75,8 @@ lemma scale_zero_right [simp]: "a *s 0 = 0" and scale_minus_right [simp]: "a *s (- x) = - (a *s x)" - and scale_right_diff_distrib [algebra_simps]: "a *s (x - y) = a *s x - a *s y" + and scale_right_diff_distrib [algebra_simps, algebra_split_simps]: + "a *s (x - y) = a *s x - a *s y" and scale_sum_right: "a *s (sum f A) = (\x\A. a *s (f x))" proof - interpret s: additive "\x. a *s x" @@ -93,7 +97,7 @@ context module begin -lemma [field_simps]: +lemma [field_simps, field_split_simps]: shows scale_left_distrib_NO_MATCH: "NO_MATCH (x div y) c \ (a + b) *s x = a *s x + b *s x" and scale_right_distrib_NO_MATCH: "NO_MATCH (x div y) a \ a *s (x + y) = a *s x + a *s y" and scale_left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \ (a - b) *s x = a *s x - b *s x" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Number_Theory/Fib.thy --- a/src/HOL/Number_Theory/Fib.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Number_Theory/Fib.thy Wed Oct 09 14:51:54 2019 +0000 @@ -200,8 +200,10 @@ by (rule LIMSEQ_power_zero) (simp_all add: \_def \_def field_simps add_pos_pos) then have "(\n. 1 - (\ / \) ^ n) \ 1 - 0" by (intro tendsto_diff tendsto_const) - with * show ?thesis - by (simp add: divide_simps fib_closed_form [folded \_def \_def]) + with * have "(\n. (\ ^ n - \ ^ n) / \ ^ n) \ 1" + by (simp add: field_simps) + then show ?thesis + by (simp add: fib_closed_form \_def \_def) qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Power.thy Wed Oct 09 14:51:54 2019 +0000 @@ -123,8 +123,9 @@ context comm_monoid_mult begin -lemma power_mult_distrib [field_simps]: "(a * b) ^ n = (a ^ n) * (b ^ n)" - by (induct n) (simp_all add: ac_simps) +lemma power_mult_distrib [algebra_simps, algebra_split_simps, field_simps, field_split_simps, divide_simps]: + "(a * b) ^ n = (a ^ n) * (b ^ n)" + by (induction n) (simp_all add: ac_simps) end @@ -378,7 +379,7 @@ begin text \Perhaps these should be simprules.\ -lemma power_inverse [field_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)" +lemma power_inverse [field_simps, field_split_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)" proof (cases "a = 0") case True then show ?thesis by (simp add: power_0_left) @@ -389,7 +390,7 @@ then show ?thesis by simp qed -lemma power_one_over [field_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n" +lemma power_one_over [field_simps, field_split_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n" using power_inverse [of a] by (simp add: divide_inverse) end @@ -397,7 +398,7 @@ context field begin -lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n" +lemma power_divide [field_simps, field_split_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n" by (induct n) simp_all end diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Probability/Conditional_Expectation.thy --- a/src/HOL/Probability/Conditional_Expectation.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Probability/Conditional_Expectation.thy Wed Oct 09 14:51:54 2019 +0000 @@ -855,7 +855,7 @@ fixes c::real assumes "integrable M f" shows "AE x in M. real_cond_exp M F (\x. f x / c) x = real_cond_exp M F f x / c" -using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: divide_simps) +using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: field_split_simps) lemma real_cond_exp_diff [intro, simp]: assumes [measurable]: "integrable M f" "integrable M g" @@ -1140,7 +1140,7 @@ have "q x + phi x * (y-x) \ q y" unfolding phi_def apply (rule convex_le_Inf_differential) using \convex_on I q\ that \interior I = I\ by auto then have "phi x \ (q x - q y) / (x - y)" - using that \x < y\ by (auto simp add: divide_simps algebra_simps) + using that \x < y\ by (auto simp add: field_split_simps algebra_simps) moreover have "(q x - q y)/(x - y) \ phi y" unfolding phi_def proof (rule cInf_greatest, auto) fix t assume "t \ I" "y < t" @@ -1172,7 +1172,7 @@ using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto have int1: "integrable (restr_to_subalg M F) (\x. g x * q (real_cond_exp M F X x))" apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg \integrable (restr_to_subalg M F) f\) - unfolding g_def by (auto simp add: divide_simps abs_mult algebra_simps) + unfolding g_def by (auto simp add: field_split_simps abs_mult algebra_simps) have int2: "integrable M (\x. G x * (X x - real_cond_exp M F X x))" apply (rule Bochner_Integration.integrable_bound[of _ "\x. \X x\ + \real_cond_exp M F X x\"]) apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int \integrable M X\ AE_I2) @@ -1208,7 +1208,7 @@ ultimately have "AE x in M. g x * real_cond_exp M F (\x. q (X x)) x \ g x * q (real_cond_exp M F X x)" by auto then show "AE x in M. real_cond_exp M F (\x. q (X x)) x \ q (real_cond_exp M F X x)" - using g(1) by (auto simp add: divide_simps) + using g(1) by (auto simp add: field_split_simps) qed text \Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Probability/Distributions.thy --- a/src/HOL/Probability/Distributions.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Probability/Distributions.thy Wed Oct 09 14:51:54 2019 +0000 @@ -612,7 +612,7 @@ also have "\ = (ln l - 1) / ln b" by simp finally show ?thesis - by (simp add: log_def divide_simps ln_div) + by (simp add: log_def ln_div) (simp add: field_split_simps) qed subsection \Uniform distribution\ @@ -999,7 +999,7 @@ case (Suc k) note step[OF this] also have "(real (2 * k + 1 + 1) / (2::real) * ((fact k) / 2)) = (fact (Suc k)) / 2" - by (simp add: field_simps of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps) + by (simp add: field_simps of_nat_Suc field_split_simps del: fact_Suc) (simp add: field_simps) finally show ?case by simp qed (insert gaussian_moment_1, simp) @@ -1230,7 +1230,7 @@ apply (intro ext nn_integral_cong) apply (simp add: normal_density_def \'_def[symmetric] \'_def[symmetric] sqrt mult_exp_exp) apply (simp add: divide_simps power2_eq_square) - apply (simp add: field_simps) + apply (simp add: algebra_simps) done also have "... = @@ -1365,7 +1365,7 @@ by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt) also have "\ = - (\x. - (normal_density \ \ x * (ln (2 * pi * \\<^sup>2)) + (normal_density \ \ x * (x - \)\<^sup>2) / \\<^sup>2) / (2 * ln b) \lborel)" - by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: divide_simps field_simps) + by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: field_split_simps field_simps) also have "\ = (\x. normal_density \ \ x * (ln (2 * pi * \\<^sup>2)) + (normal_density \ \ x * (x - \)\<^sup>2) / \\<^sup>2 \lborel) / (2 * ln b)" by (simp del: minus_add_distrib) also have "\ = (ln (2 * pi * \\<^sup>2) + 1) / (2 * ln b)" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Probability/Levy.thy --- a/src/HOL/Probability/Levy.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Probability/Levy.thy Wed Oct 09 14:51:54 2019 +0000 @@ -106,7 +106,7 @@ by (intro interval_lebesgue_integral_add(2) [symmetric] interval_integrable_mirror[THEN iffD2]) simp_all also have "\ = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) - (iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (\ * t))" - using \T \ 0\ by (intro interval_integral_cong) (auto simp add: divide_simps) + using \T \ 0\ by (intro interval_integral_cong) (auto simp add: field_split_simps) also have "\ = (CLBINT t=(0::real)..T. complex_of_real( 2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))" using \T \ 0\ diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Oct 09 14:51:54 2019 +0000 @@ -1785,7 +1785,7 @@ assumes "A \ {}" "finite A" "\x. x \ A \ finite (set_pmf (f x))" shows "measure_pmf.expectation (pmf_of_set A \ f) h = (\a\A. measure_pmf.expectation (f a) h /\<^sub>R real (card A))" - using assms by (subst pmf_expectation_bind[of A]) (auto simp: divide_simps) + using assms by (subst pmf_expectation_bind[of A]) (auto simp: field_split_simps) lemma map_pmf_of_set: assumes "finite A" "A \ {}" @@ -1995,7 +1995,7 @@ by (simp add: indicator_def) show "pmf (binomial_pmf (Suc n) p) k = pmf ?rhs k" by (cases k; cases "k > n") - (insert assms, auto simp: pmf_bind measure_pmf_single A divide_simps algebra_simps + (insert assms, auto simp: pmf_bind measure_pmf_single A field_split_simps algebra_simps not_less less_eq_Suc_le [symmetric] power_diff') qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Probability/Random_Permutations.thy --- a/src/HOL/Probability/Random_Permutations.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Probability/Random_Permutations.thy Wed Oct 09 14:51:54 2019 +0000 @@ -215,7 +215,7 @@ also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))" by (subst binomial_fact) (auto intro!: card_mono assms) also have "\ / fact (card A) = 1 / (fact ?n1 * fact ?n2)" - by (simp add: divide_simps card_eq) + by (simp add: field_split_simps card_eq) also have "\ = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair) finally show ?thesis . next diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Real.thy --- a/src/HOL/Real.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Real.thy Wed Oct 09 14:51:54 2019 +0000 @@ -816,7 +816,7 @@ then have "\n. y < r * 2 ^ n" by (metis divide_less_eq less_trans mult.commute of_nat_less_two_power that) then show ?thesis - by (simp add: divide_simps) + by (simp add: field_split_simps) qed have PA: "\ P (A n)" for n by (induct n) (simp_all add: a) diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Real_Asymp/Multiseries_Expansion.thy --- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Oct 09 14:51:54 2019 +0000 @@ -184,7 +184,7 @@ "convergent_powser' (msllist_of_msstream exp_series_stream) exp" proof - have "(\n. lcoeff (msllist_of_msstream exp_series_stream) n * x ^ n) sums exp x" for x :: real - using exp_converges[of x] by (simp add: mssnth_exp_series_stream divide_simps) + using exp_converges[of x] by (simp add: mssnth_exp_series_stream field_split_simps) thus ?thesis by (auto intro: exI[of _ "1::real"] simp: convergent_powser'_def) qed @@ -617,7 +617,7 @@ show "\N. \n\N. norm (arctan_coeffs n * x ^ n) \ 1 * norm x ^ n" unfolding norm_mult norm_power by (intro exI[of _ "0::nat"] allI impI mult_right_mono) - (simp_all add: arctan_coeffs_def divide_simps) + (simp_all add: arctan_coeffs_def field_split_simps) from that show "summable (\n. 1 * norm x ^ n)" by (intro summable_mult summable_geometric) simp_all qed @@ -3334,7 +3334,7 @@ lemma expands_to_div': assumes "basis_wf basis" "(f expands_to F) basis" "((\x. inverse (g x)) expands_to G) basis" shows "((\x. f x / g x) expands_to F * G) basis" - using expands_to_mult[OF assms] by (simp add: divide_simps) + using expands_to_mult[OF assms] by (simp add: field_split_simps) lemma expands_to_basic: assumes "basis_wf (b # basis)" "length basis = expansion_level TYPE('a::multiseries)" @@ -4270,7 +4270,7 @@ from assms(2) have "eventually (\x. b x > 0) at_top" by (simp add: filterlim_at_top_dense basis_wf_Cons) with assms(3) show "eventually (\x. b x powr c * g x = g x / b x ^ n) at_top" - by (auto elim!: eventually_mono simp: powr_realpow powr_minus divide_simps) + by (auto elim!: eventually_mono simp: powr_realpow powr_minus field_split_simps) qed lemma eval_monom_collapse: "c * eval_monom (c', es) basis x = eval_monom (c * c', es) basis x" @@ -4492,7 +4492,7 @@ by (auto simp: compare_expansions_def trimmed_imp_dominant_term_nz split: cmp_result.splits) have "(\x. inverse c * (c' * f x)) \[at_top] (\x. inverse c * (c * g x))" by (rule asymp_equiv_mult[OF asymp_equiv_refl]) (rule compare_expansions_EQ[OF assms(1-6)]) - with assms(7) show ?thesis by (simp add: divide_simps) + with assms(7) show ?thesis by (simp add: field_split_simps) qed lemma compare_expansions_EQ_imp_bigtheta: @@ -4573,7 +4573,7 @@ (auto intro: expands_to_hd'' simp: trimmed_ms_aux_MSLCons basis_wf_Cons) have "(\x. inverse c' * (c' * eval C x)) \[at_top] (\x. inverse c' * (c * g x))" by (rule asymp_equiv_mult) (insert *, simp_all) - hence "eval C \[at_top] (\x. c / c' * g x)" by (simp add: divide_simps) + hence "eval C \[at_top] (\x. c / c' * g x)" by (simp add: field_split_simps) finally show ?thesis . qed diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy --- a/src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy Wed Oct 09 14:51:54 2019 +0000 @@ -411,7 +411,7 @@ (* TODO Move *) lemma powr_mono': "a \ (b::real) \ x \ 0 \ x \ 1 \ x powr b \ x powr a" - using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div divide_simps) + using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps) qualified lemma powr_left_bounds: fixes f g :: "real \ real" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Real_Asymp/Real_Asymp_Examples.thy --- a/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Wed Oct 09 14:51:54 2019 +0000 @@ -438,7 +438,7 @@ by (subst binomial_gbinomial) (simp add: gbinomial_pochhammer' numeral_3_eq_3 pochhammer_Suc add_ac) moreover have "\ \ (\n. 3 / ln 2 * ln n)" - by (real_asymp simp: divide_simps) + by (real_asymp simp: field_split_simps) ultimately show ?thesis by simp qed @@ -487,7 +487,7 @@ by real_asymp lemma "A > 1 \ (\n. ((1 + 1 / sqrt A) / 2) powr real_of_int (2 ^ Suc n)) \ 0" - by (real_asymp simp: divide_simps add_pos_pos) + by (real_asymp simp: field_split_simps add_pos_pos) lemma assumes "c > (1 :: real)" "k \ 0" diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Oct 09 14:51:54 2019 +0000 @@ -566,6 +566,30 @@ for a b :: "'a :: ordered_real_vector" using that by (simp add: less_le_not_le neg_le_minus_divideR_eq neg_minus_divideR_le_eq) +lemma [field_split_simps]: + "a = b /\<^sub>R c \ (if c = 0 then a = 0 else c *\<^sub>R a = b)" + "b /\<^sub>R c = a \ (if c = 0 then a = 0 else b = c *\<^sub>R a)" + "a + b /\<^sub>R c = (if c = 0 then a else (c *\<^sub>R a + b) /\<^sub>R c)" + "a /\<^sub>R c + b = (if c = 0 then b else (a + c *\<^sub>R b) /\<^sub>R c)" + "a - b /\<^sub>R c = (if c = 0 then a else (c *\<^sub>R a - b) /\<^sub>R c)" + "a /\<^sub>R c - b = (if c = 0 then - b else (a - c *\<^sub>R b) /\<^sub>R c)" + "- (a /\<^sub>R c) + b = (if c = 0 then b else (- a + c *\<^sub>R b) /\<^sub>R c)" + "- (a /\<^sub>R c) - b = (if c = 0 then - b else (- a - c *\<^sub>R b) /\<^sub>R c)" + for a b :: "'a :: real_vector" + by (auto simp add: field_simps) + +lemma [field_split_simps]: + "0 < c \ a \ b /\<^sub>R c \ (if c > 0 then c *\<^sub>R a \ b else if c < 0 then b \ c *\<^sub>R a else a \ 0)" + "0 < c \ a < b /\<^sub>R c \ (if c > 0 then c *\<^sub>R a < b else if c < 0 then b < c *\<^sub>R a else a < 0)" + "0 < c \ b /\<^sub>R c \ a \ (if c > 0 then b \ c *\<^sub>R a else if c < 0 then c *\<^sub>R a \ b else a \ 0)" + "0 < c \ b /\<^sub>R c < a \ (if c > 0 then b < c *\<^sub>R a else if c < 0 then c *\<^sub>R a < b else a > 0)" + "0 < c \ a \ - (b /\<^sub>R c) \ (if c > 0 then c *\<^sub>R a \ - b else if c < 0 then - b \ c *\<^sub>R a else a \ 0)" + "0 < c \ a < - (b /\<^sub>R c) \ (if c > 0 then c *\<^sub>R a < - b else if c < 0 then - b < c *\<^sub>R a else a < 0)" + "0 < c \ - (b /\<^sub>R c) \ a \ (if c > 0 then - b \ c *\<^sub>R a else if c < 0 then c *\<^sub>R a \ - b else a \ 0)" + "0 < c \ - (b /\<^sub>R c) < a \ (if c > 0 then - b < c *\<^sub>R a else if c < 0 then c *\<^sub>R a < - b else a > 0)" + for a b :: "'a :: ordered_real_vector" + by (clarsimp intro!: field_simps)+ + lemma scaleR_nonneg_nonneg: "0 \ a \ 0 \ x \ 0 \ a *\<^sub>R x" for x :: "'a::ordered_real_vector" using scaleR_left_mono [of 0 x a] by simp @@ -1052,7 +1076,7 @@ shows "norm (z^m - w^m) \ m * norm (z - w)" proof - have "norm (z^m - w^m) = norm ((\ i < m. z) - (\ i < m. w))" - by (simp add: prod_constant) + by simp also have "\ \ (\i = m * norm (z - w)" @@ -2003,7 +2027,7 @@ have "inverse e < of_nat (nat \inverse e + 1\)" by linarith also assume "n \ nat \inverse e + 1\" finally show "dist (1 / of_nat n :: 'a) 0 < e" - using e by (simp add: divide_simps mult.commute norm_divide) + using e by (simp add: field_split_simps norm_divide) qed lemma (in metric_space) complete_def: diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Rings.thy --- a/src/HOL/Rings.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Rings.thy Wed Oct 09 14:51:54 2019 +0000 @@ -16,8 +16,8 @@ subsection \Semirings and rings\ class semiring = ab_semigroup_add + semigroup_mult + - assumes distrib_right [algebra_simps]: "(a + b) * c = a * c + b * c" - assumes distrib_left [algebra_simps]: "a * (b + c) = a * b + a * c" + assumes distrib_right [algebra_simps, algebra_split_simps]: "(a + b) * c = a * c + b * c" + assumes distrib_left [algebra_simps, algebra_split_simps]: "a * (b + c) = a * b + a * c" begin text \For the \combine_numerals\ simproc\ @@ -250,14 +250,16 @@ class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult + - assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c" + assumes right_diff_distrib' [algebra_simps, algebra_split_simps]: + "a * (b - c) = a * b - a * c" begin subclass semiring_1_cancel .. subclass comm_semiring_0_cancel .. subclass comm_semiring_1 .. -lemma left_diff_distrib' [algebra_simps]: "(b - c) * a = b * a - c * a" +lemma left_diff_distrib' [algebra_simps, algebra_split_simps]: + "(b - c) * a = b * a - c * a" by (simp add: algebra_simps) lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \ a dvd b" @@ -331,10 +333,12 @@ lemma minus_mult_commute: "- a * b = a * - b" by simp -lemma right_diff_distrib [algebra_simps]: "a * (b - c) = a * b - a * c" +lemma right_diff_distrib [algebra_simps, algebra_split_simps]: + "a * (b - c) = a * b - a * c" using distrib_left [of a b "-c "] by simp -lemma left_diff_distrib [algebra_simps]: "(a - b) * c = a * c - b * c" +lemma left_diff_distrib [algebra_simps, algebra_split_simps]: + "(a - b) * c = a * c - b * c" using distrib_right [of a "- b" c] by simp lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib @@ -646,7 +650,7 @@ context semiring begin -lemma [field_simps]: +lemma [field_simps, field_split_simps]: shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \ a * (b + c) = a * b + a * c" and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \ (a + b) * c = a * c + b * c" by (rule distrib_left distrib_right)+ @@ -656,7 +660,7 @@ context ring begin -lemma [field_simps]: +lemma [field_simps, field_split_simps]: shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \ (a - b) * c = a * c - b * c" and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \ a * (b - c) = a * b - a * c" by (rule left_diff_distrib right_diff_distrib)+ @@ -2176,17 +2180,21 @@ by (simp add: neq_iff) qed -lemma zero_less_mult_iff [sign_simps]: "0 < a * b \ 0 < a \ 0 < b \ a < 0 \ b < 0" +lemma zero_less_mult_iff [algebra_split_simps, field_split_simps]: + "0 < a * b \ 0 < a \ 0 < b \ a < 0 \ b < 0" by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2) -lemma zero_le_mult_iff [sign_simps]: "0 \ a * b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0" +lemma zero_le_mult_iff [algebra_split_simps, field_split_simps]: + "0 \ a * b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0" by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) -lemma mult_less_0_iff [sign_simps]: "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" +lemma mult_less_0_iff [algebra_split_simps, field_split_simps]: + "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" using zero_less_mult_iff [of "- a" b] by auto -lemma mult_le_0_iff [sign_simps]: "a * b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b" +lemma mult_le_0_iff [algebra_split_simps, field_split_simps]: + "a * b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b" using zero_le_mult_iff [of "- a" b] by auto text \ diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Set_Interval.thy Wed Oct 09 14:51:54 2019 +0000 @@ -2247,7 +2247,7 @@ fixes x :: "'a::{comm_ring,division_ring}" shows "(\i\n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" using sum_gp_basic[of x n] - by (simp add: mult.commute divide_simps) + by (simp add: mult.commute field_split_simps) lemma sum_power_add: fixes x :: "'a::{comm_ring,monoid_mult}" @@ -2264,7 +2264,7 @@ lemma sum_gp_strict: fixes x :: "'a::{comm_ring,division_ring}" shows "(\iThe formulae for arithmetic sums\ diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Wed Oct 09 23:00:52 2019 +0200 +++ b/src/HOL/Transcendental.thy Wed Oct 09 14:51:54 2019 +0000 @@ -102,7 +102,7 @@ also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps) also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) = (n choose (Suc k)) * ((real k + 1) / (real n - real k))" - using k by (simp add: divide_simps binomial_fact) + using k by (simp add: field_split_simps binomial_fact) also from assms have "(real k + 1) / (real n - real k) < 1" by simp finally show ?thesis using k by (simp add: mult_less_cancel_left) qed @@ -299,7 +299,7 @@ shows "(\n. of_nat n * x ^ n) \ 0" proof - have "norm x / (1 - norm x) \ 0" - using assms by (auto simp: divide_simps) + using assms by (auto simp: field_split_simps) moreover obtain N where N: "norm x / (1 - norm x) < of_int N" using ex_le_of_int by (meson ex_less_of_int) ultimately have N0: "N>0" @@ -326,7 +326,7 @@ fixes x :: "'a::{real_normed_field,banach}" shows "1 < norm x \ ((\n. of_nat n / x^n) \ 0) sequentially" using powser_times_n_limit_0 [of "inverse x"] - by (simp add: norm_divide divide_simps) + by (simp add: norm_divide field_split_simps) lemma sum_split_even_odd: fixes f :: "nat \ real" @@ -955,7 +955,7 @@ by (intro termdiff_converges[OF norm] sums_summable[OF sums]) from norm have "eventually (\z. z \ norm -` {..z. (\n. c n * z^n) = f z) (nhds z)" by eventually_elim (insert sums, simp add: sums_iff) @@ -1534,12 +1534,14 @@ then show ?thesis by simp next case False - then have [simp]: "x * of_nat n / (1 + of_nat n) / of_nat n = x / (1 + of_nat n)" + have [simp]: "1 + (of_nat n * of_nat n + of_nat n * 2) \ (0::'a)" + using of_nat_eq_iff [of "1 + n * n + n * 2" "0"] + by simp + from False have [simp]: "x * of_nat n / (1 + of_nat n) / of_nat n = x / (1 + of_nat n)" by simp have [simp]: "x / (1 + of_nat n) + x * of_nat n / (1 + of_nat n) = x" - apply (simp add: divide_simps) - using of_nat_eq_0_iff apply (fastforce simp: distrib_left) - done + using of_nat_neq_0 + by (auto simp add: field_split_simps) show ?thesis using Suc.IH [of "x * of_nat n / (1 + of_nat n)"] False by (simp add: exp_add [symmetric]) @@ -3049,7 +3051,7 @@ have "((\x. exp (f x * ln (g x))) has_derivative (\h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)" using pos - by (auto intro!: derivative_eq_intros simp: divide_simps powr_def) + by (auto intro!: derivative_eq_intros simp: field_split_simps powr_def) then show ?thesis by (rule has_derivative_transform_within[OF _ \d > 0\ \x \ X\]) (auto simp: powr_def dest: pos') qed @@ -3158,7 +3160,7 @@ proof (rule filterlim_mono_eventually) from reals_Archimedean2 [of "\x\"] obtain n :: nat where *: "real n > \x\" .. then have "eventually (\n :: nat. 0 < 1 + x / real n) at_top" - by (intro eventually_sequentiallyI [of n]) (auto simp: divide_simps) + by (intro eventually_sequentiallyI [of n]) (auto simp: field_split_simps) then show "eventually (\n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top" by (rule eventually_mono) (erule powr_realpow) show "(\n. (1 + x / real n) powr real n) \ exp x" @@ -3636,7 +3638,7 @@ then have "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)" by (intro mult_strict_right_mono zero_less_power \0 < x\) then show "0 < ?f n" - by (simp add: divide_simps mult_ac del: mult_Suc) + by (simp add: ac_simps divide_less_eq) qed have sums: "?f sums sin x" by (rule sin_paired [THEN sums_group]) simp @@ -4014,12 +4016,12 @@ lemma sin_pi_divide_n_ge_0 [simp]: assumes "n \ 0" shows "0 \ sin (pi / real n)" - by (rule sin_ge_zero) (use assms in \simp_all add: divide_simps\) + by (rule sin_ge_zero) (use assms in \simp_all add: field_split_simps\) lemma sin_pi_divide_n_gt_0: assumes "2 \ n" shows "0 < sin (pi / real n)" - by (rule sin_gt_zero) (use assms in \simp_all add: divide_simps\) + by (rule sin_gt_zero) (use assms in \simp_all add: field_split_simps\) text\Proof resembles that of \cos_is_zero\ but with \<^term>\pi\ for the upper bound\ lemma cos_total: @@ -4482,9 +4484,9 @@ lemma sincos_principal_value: "\y. (- pi < y \ y \ pi) \ (sin y = sin x \ cos y = cos x)" apply (rule exI [where x="pi - (2 * pi) * frac ((pi - x) / (2 * pi))"]) apply (auto simp: field_simps frac_lt_1) - apply (simp_all add: frac_def divide_simps) + apply (simp_all add: frac_def field_simps) apply (simp_all add: add_divide_distrib diff_divide_distrib) - apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi) + apply (simp_all add: sin_add cos_add mult.assoc [symmetric]) done @@ -4810,11 +4812,11 @@ lemma cos_tan: "\x\ < pi/2 \ cos x = 1 / sqrt (1 + tan x ^ 2)" using cos_gt_zero_pi [of x] - by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm) + by (simp add: field_split_simps tan_def real_sqrt_divide abs_if split: if_split_asm) lemma sin_tan: "\x\ < pi/2 \ sin x = tan x / sqrt (1 + tan x ^ 2)" using cos_gt_zero [of "x"] cos_gt_zero [of "-x"] - by (force simp: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm) + by (force simp: field_split_simps tan_def real_sqrt_divide abs_if split: if_split_asm) lemma tan_mono_le: "-(pi/2) < x \ x \ y \ y < pi/2 \ tan x \ tan y" using less_eq_real_def tan_monotone by auto @@ -6450,8 +6452,23 @@ lemma cosh_ln_real: "x > 0 \ cosh (ln x :: real) = (x + inverse x) / 2" by (simp add: cosh_def exp_minus) -lemma tanh_ln_real: "x > 0 \ tanh (ln x :: real) = (x ^ 2 - 1) / (x ^ 2 + 1)" - by (simp add: tanh_def sinh_ln_real cosh_ln_real divide_simps power2_eq_square) +lemma tanh_ln_real: + "tanh (ln x :: real) = (x ^ 2 - 1) / (x ^ 2 + 1)" if "x > 0" +proof - + from that have "(x * 2 - inverse x * 2) * (x\<^sup>2 + 1) = + (x\<^sup>2 - 1) * (2 * x + 2 * inverse x)" + by (simp add: field_simps power2_eq_square) + moreover have "x\<^sup>2 + 1 > 0" + using that by (simp add: ac_simps add_pos_nonneg) + moreover have "2 * x + 2 * inverse x > 0" + using that by (simp add: add_pos_pos) + ultimately have "(x * 2 - inverse x * 2) / + (2 * x + 2 * inverse x) = + (x\<^sup>2 - 1) / (x\<^sup>2 + 1)" + by (simp add: frac_eq_eq) + with that show ?thesis + by (simp add: tanh_def sinh_ln_real cosh_ln_real) +qed lemma has_field_derivative_scaleR_right [derivative_intros]: "(f has_field_derivative D) F \ ((\x. c *\<^sub>R f x) has_field_derivative (c *\<^sub>R D)) F" @@ -6470,7 +6487,7 @@ lemma has_field_derivative_tanh [THEN DERIV_chain2, derivative_intros]: "cosh x \ 0 \ (tanh has_field_derivative 1 - tanh x ^ 2) (at (x :: 'a :: {banach, real_normed_field}))" - unfolding tanh_def by (auto intro!: derivative_eq_intros simp: power2_eq_square divide_simps) + unfolding tanh_def by (auto intro!: derivative_eq_intros simp: power2_eq_square field_split_simps) lemma has_derivative_sinh [derivative_intros]: fixes g :: "'a \ ('a :: {banach, real_normed_field})" @@ -6560,8 +6577,21 @@ by (simp add: sinh_def cosh_def algebra_simps scaleR_conv_of_real exp_add [symmetric]) lemma tanh_add: - "cosh x \ 0 \ cosh y \ 0 \ tanh (x + y) = (tanh x + tanh y) / (1 + tanh x * tanh y)" - by (simp add: tanh_def sinh_add cosh_add divide_simps) + "tanh (x + y) = (tanh x + tanh y) / (1 + tanh x * tanh y)" + if "cosh x \ 0" "cosh y \ 0" +proof - + have "(sinh x * cosh y + cosh x * sinh y) * (1 + sinh x * sinh y / (cosh x * cosh y)) = + (cosh x * cosh y + sinh x * sinh y) * ((sinh x * cosh y + sinh y * cosh x) / (cosh y * cosh x))" + using that by (simp add: field_split_simps) + also have "(sinh x * cosh y + sinh y * cosh x) / (cosh y * cosh x) = sinh x / cosh x + sinh y / cosh y" + using that by (simp add: field_split_simps) + finally have "(sinh x * cosh y + cosh x * sinh y) * (1 + sinh x * sinh y / (cosh x * cosh y)) = + (sinh x / cosh x + sinh y / cosh y) * (cosh x * cosh y + sinh x * sinh y)" + by simp + then show ?thesis + using that by (auto simp add: tanh_def sinh_add cosh_add eq_divide_eq) + (simp_all add: field_split_simps) +qed lemma sinh_double: "sinh (2 * x) = 2 * sinh x * cosh x" using sinh_add[of x] by simp @@ -6658,7 +6688,7 @@ have "arsinh (-x) = ln (sqrt (x\<^sup>2 + 1) - x)" by (simp add: arsinh_real_def) also have "sqrt (x^2 + 1) - x = inverse (sqrt (x^2 + 1) + x)" - using arsinh_real_aux[of x] by (simp add: divide_simps algebra_simps power2_eq_square) + using arsinh_real_aux[of x] by (simp add: field_split_simps algebra_simps power2_eq_square) also have "ln \ = -arsinh x" using arsinh_real_aux[of x] by (simp add: arsinh_real_def ln_inverse) finally show ?thesis . @@ -6680,7 +6710,7 @@ lemma tanh_real_gt_neg1: "tanh (x :: real) > -1" proof - - have "- cosh x < sinh x" by (simp add: sinh_def cosh_def divide_simps) + have "- cosh x < sinh x" by (simp add: sinh_def cosh_def field_split_simps) thus ?thesis by (simp add: tanh_def field_simps) qed @@ -6700,7 +6730,7 @@ lemma artanh_tanh_real: "artanh (tanh x) = x" proof - have "artanh (tanh x) = ln (cosh x * (cosh x + sinh x) / (cosh x * (cosh x - sinh x))) / 2" - by (simp add: artanh_def tanh_def divide_simps) + by (simp add: artanh_def tanh_def field_split_simps) also have "cosh x * (cosh x + sinh x) / (cosh x * (cosh x - sinh x)) = (cosh x + sinh x) / (cosh x - sinh x)" by simp also have "\ = (exp x)^2" @@ -6921,7 +6951,7 @@ proof - have pos: "1 + x ^ 2 > 0" by (intro add_pos_nonneg) auto from pos arsinh_real_aux[of x] show ?thesis unfolding arsinh_def [abs_def] - by (auto intro!: derivative_eq_intros simp: powr_minus powr_half_sqrt divide_simps) + by (auto intro!: derivative_eq_intros simp: powr_minus powr_half_sqrt field_split_simps) qed lemma arcosh_real_has_field_derivative [derivative_intros]: @@ -6932,21 +6962,21 @@ from assms have "x + sqrt (x\<^sup>2 - 1) > 0" by (simp add: add_pos_pos) thus ?thesis using assms unfolding arcosh_def [abs_def] by (auto intro!: derivative_eq_intros - simp: powr_minus powr_half_sqrt divide_simps power2_eq_1_iff) + simp: powr_minus powr_half_sqrt field_split_simps power2_eq_1_iff) qed lemma artanh_real_has_field_derivative [derivative_intros]: - fixes x :: real - assumes "abs x < 1" - shows "(artanh has_field_derivative (1 / (1 - x ^ 2))) (at x within A)" -proof - - from assms have "x > -1" "x < 1" by linarith+ + "(artanh has_field_derivative (1 / (1 - x ^ 2))) (at x within A)" if + "\x\ < 1" for x :: real +proof - + from that have "- 1 < x" "x < 1" by linarith+ hence "(artanh has_field_derivative (4 - 4 * x) / ((1 + x) * (1 - x) * (1 - x) * 4)) (at x within A)" unfolding artanh_def [abs_def] by (auto intro!: derivative_eq_intros simp: powr_minus powr_half_sqrt) also have "(4 - 4 * x) / ((1 + x) * (1 - x) * (1 - x) * 4) = 1 / ((1 + x) * (1 - x))" - by (simp add: divide_simps) - also have "(1 + x) * (1 - x) = 1 - x ^ 2" by (simp add: algebra_simps power2_eq_square) + using \-1 < x\ \x < 1\ by (simp add: frac_eq_eq) + also have "(1 + x) * (1 - x) = 1 - x ^ 2" + by (simp add: algebra_simps power2_eq_square) finally show ?thesis . qed