: "exp (s * Ln z) * inverse z = exp ((s - 1) * Ln z)" + by (simp add: divide_complex_def exp_diff left_diff_distrib') show ?thesis unfolding powr_def proof (rule has_field_derivative_transform_within) show "((\z. exp (s * Ln z)) has_field_derivative s * (if z = 0 then 0 else exp ((s - 1) * Ln z))) (at z)" - apply (intro derivative_eq_intros | simp add: assms)+ - by (simp add: False divide_complex_def exp_diff left_diff_distrib') + by (intro derivative_eq_intros | simp add: assms False \

)+ qed (use False in auto) qed (use assms in auto) @@ -2281,11 +2293,11 @@ lemma has_field_derivative_powr_of_int: fixes z :: complex - assumes gderiv:"(g has_field_derivative gd) (at z within s)" and "g z\0" - shows "((\z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within s)" + assumes gderiv:"(g has_field_derivative gd) (at z within S)" and "g z\0" + shows "((\z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within S)" proof - define dd where "dd = of_int n * g z powr (of_int (n - 1)) * gd" - obtain e where "e>0" and e_dist:"\y\s. dist z y < e \ g y \ 0" + obtain e where "e>0" and e_dist:"\y\S. dist z y < e \ g y \ 0" using DERIV_continuous[OF gderiv,THEN continuous_within_avoid] \g z\0\ by auto have ?thesis when "n\0" proof - @@ -2298,19 +2310,19 @@ using powr_of_int[OF \g z\0\,of "n-1"] by (simp add: nat_diff_distrib') then show ?thesis unfolding dd_def dd'_def by simp qed (simp add:dd_def dd'_def) - then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s) - \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within s)" + then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within S) + \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within S)" by simp - also have "... \ ((\z. g z ^ nat n) has_field_derivative dd') (at z within s)" + also have "... \ ((\z. g z ^ nat n) has_field_derivative dd') (at z within S)" proof (rule has_field_derivative_cong_eventually) - show "\\<^sub>F x in at z within s. g x powr of_int n = g x ^ nat n" + show "\\<^sub>F x in at z within S. g x powr of_int n = g x ^ nat n" unfolding eventually_at apply (rule exI[where x=e]) using powr_of_int that \e>0\ e_dist by (simp add: dist_commute) qed (use powr_of_int \g z\0\ that in simp) also have "..." unfolding dd'_def using gderiv that by (auto intro!: derivative_eq_intros) - finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)" . + 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 qed moreover have ?thesis when "n<0" @@ -2323,12 +2335,12 @@ then show ?thesis unfolding dd_def dd'_def by (simp add: divide_inverse) qed - then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s) - \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within s)" + then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within S) + \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within S)" by simp - also have "... \ ((\z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within s)" + also have "... \ ((\z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within S)" proof (rule has_field_derivative_cong_eventually) - show "\\<^sub>F x in at z within s. g x powr of_int n = inverse (g x ^ nat (- n))" + show "\\<^sub>F x in at z within S. g x powr of_int n = inverse (g x ^ nat (- n))" unfolding eventually_at apply (rule exI[where x=e]) using powr_of_int that \e>0\ e_dist by (simp add: dist_commute) @@ -2341,7 +2353,7 @@ unfolding dd'_def using gderiv that \g z\0\ 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)" . + 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 qed ultimately show ?thesis by force @@ -2349,27 +2361,25 @@ lemma field_differentiable_powr_of_int: fixes z :: complex - assumes gderiv:"g field_differentiable (at z within s)" and "g z\0" - shows "(\z. g z powr of_int n) field_differentiable (at z within s)" + assumes gderiv: "g field_differentiable (at z within S)" and "g z \ 0" + shows "(\z. g z powr of_int n) field_differentiable (at z within S)" using has_field_derivative_powr_of_int assms(2) field_differentiable_def gderiv by blast lemma holomorphic_on_powr_of_int [holomorphic_intros]: - assumes "f holomorphic_on s" "\z\s. f z\0" - shows "(\z. (f z) powr of_int n) holomorphic_on s" + assumes holf: "f holomorphic_on S" and 0: "\z. z\S \ f z \ 0" + shows "(\z. (f z) powr of_int n) holomorphic_on S" proof (cases "n\0") case True - then have "?thesis \ (\z. (f z) ^ nat n) holomorphic_on s" - apply (rule_tac holomorphic_cong) - using assms(2) by (auto simp add:powr_of_int) - moreover have "(\z. (f z) ^ nat n) holomorphic_on s" - using assms(1) by (auto intro:holomorphic_intros) + then have "?thesis \ (\z. (f z) ^ nat n) holomorphic_on S" + by (metis (no_types, lifting) 0 holomorphic_cong powr_of_int) + moreover have "(\z. (f z) ^ nat n) holomorphic_on S" + using holf by (auto intro: holomorphic_intros) ultimately show ?thesis by auto next case False - then have "?thesis \ (\z. inverse (f z) ^ nat (-n)) holomorphic_on s" - apply (rule_tac holomorphic_cong) - using assms(2) by (auto simp add:powr_of_int power_inverse) - moreover have "(\z. inverse (f z) ^ nat (-n)) holomorphic_on s" + then have "?thesis \ (\z. inverse (f z) ^ nat (-n)) holomorphic_on S" + by (metis (no_types, lifting) "0" holomorphic_cong power_inverse powr_of_int) + moreover have "(\z. inverse (f z) ^ nat (-n)) holomorphic_on S" using assms by (auto intro!:holomorphic_intros) ultimately show ?thesis by auto qed @@ -2580,10 +2590,12 @@ then obtain xo where "xo > 0" and xo: "\x. x \ xo \ x < e * exp (Re s * x)" 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 field_split_simps) - apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff) - done + proof - + have "ln (real n) \ xo" + using that exp_gt_zero ln_ge_iff [of n] nat_ceiling_le_eq by fastforce + then show ?thesis + using e xo [of "ln n"] by (auto simp: norm_divide norm_powr_real field_split_simps) + qed then show "\no. \n\no. norm (Ln (of_nat n) / of_nat n powr s) < e" by blast qed @@ -2594,17 +2606,17 @@ lemma lim_ln_over_power: fixes s :: real assumes "0 < s" - shows "((\n. ln n / (n powr s)) \ 0) sequentially" - using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms - apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) - done + shows "((\n. ln n / (n powr s)) \ 0) sequentially" +proof - + have "(\n. ln (Suc n) / (Suc n) powr s) \ 0" + using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms + by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) + then show ?thesis + using filterlim_sequentially_Suc[of "\n::nat. ln n / n powr s"] by auto +qed lemma lim_ln_over_n [tendsto_intros]: "((\n. ln(real_of_nat n) / of_nat n) \ 0) sequentially" - using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]] - apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm) - done + using lim_ln_over_power [of 1] by auto lemma lim_log_over_n [tendsto_intros]: "(\n. log k n/n) \ 0" @@ -2633,12 +2645,10 @@ lemma lim_1_over_real_power: fixes s :: real assumes "0 < s" - shows "((\n. 1 / (of_nat n powr s)) \ 0) sequentially" + shows "((\n. 1 / (of_nat n powr s)) \ 0) sequentially" using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm) - apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide) - done + by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) lemma lim_1_over_Ln: "((\n. 1 / Ln(of_nat n)) \ 0) sequentially" proof (clarsimp simp add: lim_sequentially dist_norm norm_divide field_split_simps) @@ -2665,9 +2675,7 @@ lemma lim_1_over_ln: "((\n. 1 / ln(real_of_nat n)) \ 0) sequentially" using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm) - apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide) - done + by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) lemma lim_ln1_over_ln: "(\n. ln(Suc n) / ln n) \ 1" proof (rule Lim_transform_eventually) @@ -2719,10 +2727,9 @@ finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)" by simp also have "... = exp (Ln z / 2)" - apply (subst csqrt_square) + apply (rule csqrt_square) using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms - apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+) - done + by (fastforce simp: Re_exp Im_exp ) finally show ?thesis using assms csqrt_square by simp qed @@ -2804,19 +2811,24 @@ "continuous (at z within (\ \ {w. 0 \ Re(w)})) csqrt" proof (cases "z \ \\<^sub>\\<^sub>0") case True - have *: "\e. \0 < e\ - \ \x'\\ \ {w. 0 \ Re w}. cmod x' < e^2 \ cmod (csqrt x') < e" - by (auto simp: Reals_def real_less_lsqrt) - have "Im z = 0" "Re z < 0 \ z = 0" + have [simp]: "Im z = 0" and 0: "Re z < 0 \ z = 0" using True cnj.code complex_cnj_zero_iff by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce - with * show ?thesis - apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge]) - apply (auto simp: continuous_within_eps_delta) - using zero_less_power by blast -next - case False - then show ?thesis by (blast intro: continuous_within_csqrt) -qed + show ?thesis + using 0 + proof + assume "Re z < 0" + then show ?thesis + by (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge]) + next + assume "z = 0" + moreover + have "\e. 0 < e + \ \x'\\ \ {w. 0 \ Re w}. cmod x' < e^2 \ cmod (csqrt x') < e" + by (auto simp: Reals_def real_less_lsqrt) + ultimately show ?thesis + using zero_less_power by (fastforce simp: continuous_within_eps_delta) + qed +qed (blast intro: continuous_within_csqrt) subsection\Complex arctangent\ @@ -2870,32 +2882,32 @@ assumes "\Re z\ < pi/2" shows "Arctan(tan z) = z" proof - - have ge_pi2: "\n::int. \of_int (2*n + 1) * pi/2\ \ pi/2" - by (case_tac n rule: int_cases) (auto simp: abs_mult) - have "exp (\*z)*exp (\*z) = -1 \ exp (2*\*z) = -1" - by (metis distrib_right exp_add mult_2) - also have "... \ exp (2*\*z) = exp (\*pi)" - using cis_conv_exp cis_pi by auto - also have "... \ exp (2*\*z - \*pi) = 1" - by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute) - also have "... \ Re(\*2*z - \*pi) = 0 \ (\n::int. Im(\*2*z - \*pi) = of_int (2 * n) * pi)" - by (simp add: exp_eq_1) - also have "... \ Im z = 0 \ (\n::int. 2 * Re z = of_int (2*n + 1) * pi)" - by (simp add: algebra_simps) - also have "... \ False" - using assms ge_pi2 - apply (auto simp: algebra_simps) - by (metis abs_mult_pos not_less of_nat_less_0_iff of_nat_numeral) - finally have *: "exp (\*z)*exp (\*z) + 1 \ 0" - by (auto simp: add.commute minus_unique) - show ?thesis - using assms * - apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps - i_times_eq_iff power2_eq_square [symmetric]) - apply (rule Ln_unique) - apply (auto simp: divide_simps exp_minus) - apply (simp add: algebra_simps exp_double [symmetric]) - done + have "Ln ((1 - \ * tan z) / (1 + \ * tan z)) = 2 * z / \" + proof (rule Ln_unique) + have ge_pi2: "\n::int. \of_int (2*n + 1) * pi/2\ \ pi/2" + by (case_tac n rule: int_cases) (auto simp: abs_mult) + have "exp (\*z)*exp (\*z) = -1 \ exp (2*\*z) = -1" + by (metis distrib_right exp_add mult_2) + also have "... \ exp (2*\*z) = exp (\*pi)" + using cis_conv_exp cis_pi by auto + also have "... \ exp (2*\*z - \*pi) = 1" + by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute) + also have "... \ Re(\*2*z - \*pi) = 0 \ (\n::int. Im(\*2*z - \*pi) = of_int (2 * n) * pi)" + by (simp add: exp_eq_1) + also have "... \ Im z = 0 \ (\n::int. 2 * Re z = of_int (2*n + 1) * pi)" + by (simp add: algebra_simps) + also have "... \ False" + using assms ge_pi2 + apply (auto simp: algebra_simps) + by (metis abs_mult_pos not_less of_nat_less_0_iff of_nat_numeral) + finally have "exp (\*z)*exp (\*z) + 1 \ 0" + by (auto simp: add.commute minus_unique) + then show "exp (2 * z / \) = (1 - \ * tan z) / (1 + \ * tan z)" + apply (simp add: tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps) + by (simp add: algebra_simps flip: power2_eq_square exp_double) + qed (use assms in auto) + then show ?thesis + by (auto simp: Arctan_def) qed lemma @@ -2930,12 +2942,11 @@ show "\Re(Arctan z)\ < pi/2" unfolding Arctan_def divide_complex_def using mpi_less_Im_Ln [OF nzi] - apply (auto simp: abs_if intro!: Im_Ln_less_pi * [unfolded divide_complex_def]) - done + by (auto simp: abs_if intro!: Im_Ln_less_pi * [unfolded divide_complex_def]) show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)" unfolding Arctan_def scaleR_conv_of_real apply (intro derivative_eq_intros | simp add: nz0 *)+ - using nz0 nz1 zz + using nz1 zz apply (simp add: field_split_simps power2_eq_square) apply algebra done @@ -3077,10 +3088,12 @@ proof - have ne: "1 + x\<^sup>2 \ 0" by (metis power_one sum_power2_eq_zero_iff zero_neq_one) + have ne1: "1 + \ * complex_of_real x \ 0" + using Complex_eq complex_eq_cancel_iff2 by fastforce have "Re (Ln ((1 - \ * x) * inverse (1 + \ * x))) = 0" apply (rule norm_exp_imaginary) - apply (subst exp_Ln) - using ne apply (simp_all add: cmod_def complex_eq_iff) + using ne + apply (simp add: ne1 cmod_def) apply (auto simp: field_split_simps) apply algebra done @@ -3090,11 +3103,10 @@ lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))" proof (rule arctan_unique) - show "- (pi / 2) < Re (Arctan (complex_of_real x))" - apply (simp add: Arctan_def) - apply (rule Im_Ln_less_pi) - apply (auto simp: Im_complex_div_lemma complex_nonpos_Reals_iff) - done + have "(1 - \ * x) / (1 + \ * x) \ \\<^sub>\\<^sub>0" + by (auto simp: Im_complex_div_lemma complex_nonpos_Reals_iff) + then show "- (pi / 2) < Re (Arctan (complex_of_real x))" + by (simp add: Arctan_def Im_Ln_less_pi) next have *: " (1 - \*x) / (1 + \*x) \ 0" by (simp add: field_split_simps) ( simp add: complex_eq_iff) @@ -3103,12 +3115,14 @@ by (simp add: Arctan_def) next have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))" - apply (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos) - apply (simp add: field_simps) - by (simp add: power2_eq_square) + by (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos field_simps power2_eq_square) also have "... = x" - apply (subst tan_Arctan, auto) - by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one) + proof - + have "(complex_of_real x)\<^sup>2 \ - 1" + by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one) + then show ?thesis + by simp + qed finally show "tan (Re (Arctan (complex_of_real x))) = x" . qed @@ -3169,18 +3183,14 @@ assumes "\x * y\ < 1" shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))" proof (cases "x = 0 \ y = 0") - case True then show ?thesis - by auto -next 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: field_split_simps abs_mult) - done - show ?thesis - apply (rule arctan_add_raw) - using * by linarith -qed + with assms have "\x\ < inverse \y\" + by (simp add: field_split_simps abs_mult) + with False have "\arctan x\ < pi / 2 - \arctan y\" using assms + by (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff) + then show ?thesis + by (intro arctan_add_raw) linarith +qed auto lemma abs_arctan_le: fixes x::real shows "\arctan x\ \ \x\" @@ -3190,9 +3200,8 @@ have "cmod (Arctan w - Arctan z) \ 1 * cmod (w-z)" if "w \ \" "z \ \" for w z apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1]) apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan]) - using 1 that apply (auto simp: Reals_def) - done - then have "cmod (Arctan (of_real x) - Arctan 0) \ 1 * cmod (of_real x -0)" + using 1 that by (auto simp: Reals_def) + then have "cmod (Arctan (of_real x) - Arctan 0) \ 1 * cmod (of_real x - 0)" using Reals_0 Reals_of_real by blast then show ?thesis by (simp add: Arctan_of_real) @@ -3254,8 +3263,7 @@ lemma Arcsin_body_lemma: "\ * z + csqrt(1 - z\<^sup>2) \ 0" using power2_csqrt [of "1 - z\<^sup>2"] - apply auto - by (metis complex_i_mult_minus diff_add_cancel diff_minus_eq_add diff_self mult.assoc mult.left_commute numeral_One power2_csqrt power2_eq_square zero_neq_numeral) + by (metis add.inverse_inverse complex_i_mult_minus diff_0 diff_add_cancel diff_minus_eq_add mult.assoc mult.commute numeral_One power2_eq_square zero_neq_numeral) lemma Arcsin_range_lemma: "\Re z\ < 1 \ 0 < Re(\ * z + csqrt(1 - z\<^sup>2))" using Complex.cmod_power2 [of z, symmetric] @@ -3268,12 +3276,19 @@ by (simp add: Arcsin_def Arcsin_body_lemma) lemma one_minus_z2_notin_nonpos_Reals: - assumes "(Im z = 0 \ \Re z\ < 1)" + assumes "Im z = 0 \ \Re z\ < 1" shows "1 - z\<^sup>2 \ \\<^sub>\\<^sub>0" - using assms - apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2) - using power2_less_0 [of "Im z"] apply force - using abs_square_less_1 not_le by blast +proof (cases "Im z = 0") + case True + with assms show ?thesis + by (simp add: complex_nonpos_Reals_iff flip: abs_square_less_1) +next + case False + have "\ (Im z)\<^sup>2 \ - 1" + using False power2_less_eq_zero_iff by fastforce + with False show ?thesis + by (auto simp add: complex_nonpos_Reals_iff Re_power2 Im_power2) +qed lemma isCont_Arcsin_lemma: assumes le0: "Re (\ * z + csqrt (1 - z\<^sup>2)) \ 0" and "(Im z = 0 \ \Re z\ < 1)" @@ -3356,9 +3371,7 @@ by (simp add: field_simps power2_eq_square) also have "... = - (\ * Ln (((exp (\*z) + inverse (exp (\*z)))/2) - (inverse (exp (\*z)) - exp (\*z)) / 2))" apply (subst csqrt_square) - using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma - apply auto - done + using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma by auto also have "... = - (\ * Ln (exp (\*z)))" by (simp add: field_simps power2_eq_square) also have "... = z" @@ -3453,11 +3466,8 @@ then show False using False by (simp add: power2_eq_square algebra_simps) qed - moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)" - apply (subst Imz) - using abs_Re_le_cmod [of "1-z\<^sup>2"] - apply (simp add: Re_power2) - done + moreover have "(Im z)\<^sup>2 = (1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2" + using abs_Re_le_cmod [of "1-z\<^sup>2"] by (subst Imz) (simp add: Re_power2) ultimately show False by (simp add: cmod_power2) qed @@ -3469,14 +3479,12 @@ have "z + \ * csqrt (1 - z\<^sup>2) \ \\<^sub>\\<^sub>0" by (metis complex_nonpos_Reals_iff isCont_Arccos_lemma assms) with assms show ?thesis - apply (simp add: Arccos_def) - apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+ - apply (simp_all add: one_minus_z2_notin_nonpos_Reals assms) - done + unfolding Arccos_def + by (simp_all add: one_minus_z2_notin_nonpos_Reals assms) qed lemma isCont_Arccos' [simp]: - shows "isCont f z \ (Im (f z) = 0 \ \Re (f z)\ < 1) \ isCont (\x. Arccos (f x)) z" + "isCont f z \ (Im (f z) = 0 \ \Re (f z)\ < 1) \ isCont (\x. Arccos (f x)) z" by (blast intro: isCont_o2 [OF _ isCont_Arccos]) lemma cos_Arccos [simp]: "cos(Arccos z) = z" @@ -3486,15 +3494,13 @@ moreover have "... \ z + \ * csqrt (1 - z\<^sup>2) = 0" by (metis distrib_right mult_eq_0_iff zero_neq_numeral) ultimately show ?thesis - apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps) - apply (simp add: power2_eq_square [symmetric]) - done + by (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps flip: power2_eq_square) qed lemma Arccos_cos: - assumes "0 < Re z & Re z < pi \ - Re z = 0 & 0 \ Im z \ - Re z = pi & Im z \ 0" + assumes "0 < Re z \ Re z < pi \ + Re z = 0 \ 0 \ Im z \ + Re z = pi \ Im z \ 0" shows "Arccos(cos z) = z" proof - have *: "((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z))) = sin z" @@ -3508,14 +3514,12 @@ \ * ((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z)))))" apply (subst csqrt_square) using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z] - apply (auto simp: * Re_sin Im_sin) - done + by (auto simp: * Re_sin Im_sin) also have "... = - (\ * Ln (exp (\*z)))" by (simp add: field_simps power2_eq_square) also have "... = z" using assms - apply (subst Complex_Transcendental.Ln_exp, auto) - done + by (subst Complex_Transcendental.Ln_exp, auto) finally show ?thesis . qed @@ -3596,9 +3600,7 @@ proof - 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: field_split_simps) - done + by (simp only: abs_le_square_iff) (simp add: field_split_simps) also have "... \ (cmod w)\<^sup>2" by (auto simp: cmod_power2) finally show ?thesis @@ -3651,7 +3653,7 @@ by (metis mult_cancel_left zero_neq_numeral) then have "(\ * z + csqrt (1 - z\<^sup>2))\<^sup>2 \ -1" using assms - apply (auto simp: power2_sum) + apply (simp add: power2_sum) apply (simp add: power2_eq_square algebra_simps) done then show ?thesis @@ -3685,9 +3687,7 @@ by (metis mult_cancel_left2 zero_neq_numeral) (*FIXME cancel_numeral_factor*) then have "(z + \ * csqrt (1 - z\<^sup>2))\<^sup>2 \ 1" using assms - apply (auto simp: Power.comm_semiring_1_class.power2_sum power_mult_distrib) - apply (simp add: power2_eq_square algebra_simps) - done + by (metis Arccos_def add.commute add.left_neutral cancel_comm_monoid_add_class.diff_cancel cos_Arccos csqrt_0 mult_zero_right) then show ?thesis apply (simp add: sin_exp_eq Arccos_def exp_minus) apply (simp add: divide_simps Arccos_body_lemma) @@ -3698,20 +3698,18 @@ lemma cos_sin_csqrt: assumes "0 < cos(Re z) \ cos(Re z) = 0 \ Im z * sin(Re z) \ 0" shows "cos z = csqrt(1 - (sin z)\<^sup>2)" - apply (rule csqrt_unique [THEN sym]) - apply (simp add: cos_squared_eq) - using assms - apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff) - done +proof (rule csqrt_unique [THEN sym]) + show "(cos z)\<^sup>2 = 1 - (sin z)\<^sup>2" + by (simp add: cos_squared_eq) +qed (use assms in \auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff\) lemma sin_cos_csqrt: assumes "0 < sin(Re z) \ sin(Re z) = 0 \ 0 \ Im z * cos(Re z)" shows "sin z = csqrt(1 - (cos z)\<^sup>2)" - apply (rule csqrt_unique [THEN sym]) - apply (simp add: sin_squared_eq) - using assms - apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff) - done +proof (rule csqrt_unique [THEN sym]) + show "(sin z)\<^sup>2 = 1 - (cos z)\<^sup>2" + by (simp add: sin_squared_eq) +qed (use assms in \auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff\) lemma Arcsin_Arccos_csqrt_pos: "(0 < Re z | Re z = 0 & 0 \ Im z) \ Arcsin z = Arccos(csqrt(1 - z\<^sup>2))" @@ -3770,10 +3768,8 @@ fix x' assume "- (pi / 2) \ x'" "x' \ pi / 2" "x = sin x'" then show "x' = Re (Arcsin (complex_of_real (sin x')))" - apply (simp add: sin_of_real [symmetric]) - apply (subst Arcsin_sin) - apply (auto simp: ) - done + unfolding sin_of_real [symmetric] + by (subst Arcsin_sin) auto qed lemma of_real_arcsin: "\x\ \ 1 \ of_real(arcsin x) = Arcsin(of_real x)" @@ -3820,10 +3816,8 @@ fix x' assume "0 \ x'" "x' \ pi" "x = cos x'" then show "x' = Re (Arccos (complex_of_real (cos x')))" - apply (simp add: cos_of_real [symmetric]) - apply (subst Arccos_cos) - apply (auto simp: ) - done + unfolding cos_of_real [symmetric] + by (subst Arccos_cos) auto qed lemma of_real_arccos: "\x\ \ 1 \ of_real(arccos x) = Arccos(of_real x)" @@ -3861,8 +3855,7 @@ have "arcsin x = pi/2 - arccos x" apply (rule sin_inj_pi) using assms arcsin [OF assms] arccos [OF assms] - apply (auto simp: algebra_simps sin_diff) - done + by (auto simp: algebra_simps sin_diff) then show ?thesis by (simp add: algebra_simps) qed @@ -3975,7 +3968,7 @@ then show ?thesis apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler) apply (simp only: * cos_of_real sin_of_real) - apply (simp add: ) + apply simp done qed @@ -3993,10 +3986,7 @@ also have "... \ (\z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))" by simp also have "... \ (\z::int. of_nat j = of_nat k + of_nat n * z)" - apply (rule HOL.iff_exI) - apply (auto simp: ) - using of_int_eq_iff apply fastforce - by (metis of_int_add of_int_mult of_int_of_nat_eq) + by (metis (mono_tags, hide_lams) of_int_add of_int_eq_iff of_int_mult of_int_of_nat_eq) also have "... \ int j mod int n = int k mod int n" by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps) also have "... \ j mod n = k mod n" @@ -4038,7 +4028,7 @@ lemma complex_roots_unity: assumes "1 \ n" - shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \ * of_nat j / of_nat n) | j::nat. j < n}" + shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \ * of_nat j / of_nat n) | j. j < n}" apply (rule Finite_Set.card_seteq [symmetric]) using assms apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity) @@ -4053,6 +4043,4 @@ apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler) done - - end diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Analysis/Polytope.thy --- a/src/HOL/Analysis/Polytope.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Analysis/Polytope.thy Fri Sep 25 17:13:12 2020 +0100 @@ -2783,7 +2783,7 @@ proof (cases "affine_dependent S") case True have [iff]: "finite S" - using assms using card_infinite by force + using assms using card.infinite by force then have ccs: "closed (convex hull S)" by (simp add: compact_imp_closed finite_imp_compact_convex_hull) { fix x T @@ -2839,7 +2839,7 @@ by (auto simp: assms segment_convex_hull frontier_def empty_interior_convex_hull insert_commute card_insert_le_m1 hull_inc insert_absorb) next case False then have [simp]: "card {a, b, c} = Suc (DIM('a))" - by (simp add: card_insert Set.insert_Diff_if assms) + by (simp add: card.insert_remove Set.insert_Diff_if assms) show ?thesis proof show "?lhs \ ?rhs" @@ -3125,7 +3125,7 @@ proof assume "n simplex {}" then show "n = -1" - unfolding simplex by (metis card_empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0) + unfolding simplex by (metis card.empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0) next assume "n = -1" then show "n simplex {}" by (fastforce simp: simplex) @@ -3141,7 +3141,7 @@ lemma zero_simplex_sing: "0 simplex {a}" apply (simp add: simplex_def) - by (metis affine_independent_1 card_empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI) + by (metis affine_independent_1 card.empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI) lemma simplex_sing [simp]: "n simplex {a} \ n = 0" using aff_dim_simplex aff_dim_sing zero_simplex_sing by blast diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Analysis/Simplex_Content.thy --- a/src/HOL/Analysis/Simplex_Content.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Analysis/Simplex_Content.thy Fri Sep 25 17:13:12 2020 +0100 @@ -89,7 +89,7 @@ also have "t ^ n / n / fact (card A) = t ^ n / fact n" by (simp add: n_def) also have "n = card (insert b A)" - using insert.hyps by (subst card_insert) (auto simp: n_def) + using insert.hyps by (subst card.insert_remove) (auto simp: n_def) finally show ?case . qed diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Analysis/Starlike.thy Fri Sep 25 17:13:12 2020 +0100 @@ -3270,7 +3270,7 @@ fix a b assume "b \ S" "b \ affine hull (S - {b})" then have "interior(affine hull S) = {}" using assms - by (metis DIM_positive One_nat_def Suc_mono card.remove card_infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one) + by (metis DIM_positive One_nat_def Suc_mono card.remove card.infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one) then show "interior (convex hull S) = {}" using affine_hull_nonempty_interior by fastforce qed diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Binomial.thy Fri Sep 25 17:13:12 2020 +0100 @@ -81,11 +81,11 @@ proof - from \n \ K\ obtain L where "K = insert n L" and "n \ L" by (blast elim: Set.set_insert) - with that show ?thesis by (simp add: card_insert) + with that show ?thesis by (simp add: card.insert_remove) qed show "K \ ?A \ K \ ?B" by (subst in_image_insert_iff) - (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite + (auto simp add: card.insert_remove subset_eq_atLeast0_lessThan_finite Diff_subset_conv K_finite Suc_card_K) qed also have "{K\?Q. n \ K} = ?P n (Suc k)" diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Finite_Set.thy Fri Sep 25 17:13:12 2020 +0100 @@ -1387,12 +1387,6 @@ defines card = "folding.F (\_. Suc) 0" by standard rule -lemma card_infinite: "\ finite A \ card A = 0" - by (fact card.infinite) - -lemma card_empty: "card {} = 0" - by (fact card.empty) - lemma card_insert_disjoint: "finite A \ x \ A \ card (insert x A) = Suc (card A)" by (fact card.insert) @@ -1417,17 +1411,20 @@ lemma card_gt_0_iff: "0 < card A \ A \ {} \ finite A" by (simp add: neq0_conv [symmetric] card_eq_0_iff) -lemma card_Suc_Diff1: "finite A \ x \ A \ Suc (card (A - {x})) = card A" - apply (rule insert_Diff [THEN subst, where t = A]) - apply assumption - apply (simp del: insert_Diff_single) - done +lemma card_Suc_Diff1: + assumes "finite A" "x \ A" shows "Suc (card (A - {x})) = card A" +proof - + have "Suc (card (A - {x})) = card (insert x (A - {x}))" + using assms by (simp add: card.insert_remove) + also have "... = card A" + using assms by (simp add: card_insert_if) + finally show ?thesis . +qed -lemma card_insert_le_m1: "n > 0 \ card y \ n - 1 \ card (insert x y) \ n" - apply (cases "finite y") - apply (cases "x \ y") - apply (auto simp: insert_absorb) - done +lemma card_insert_le_m1: + assumes "n > 0" "card y \ n - 1" shows "card (insert x y) \ n" + using assms + by (cases "finite y") (auto simp: card_insert_if) lemma card_Diff_singleton: "finite A \ x \ A \ card (A - {x}) = card A - 1" by (simp add: card_Suc_Diff1 [symmetric]) @@ -1446,9 +1443,6 @@ using assms by (simp add: card_Diff_singleton) qed -lemma card_insert: "finite A \ card (insert x A) = Suc (card (A - {x}))" - by (fact card.insert_remove) - lemma card_insert_le: "finite A \ card A \ card (insert x A)" by (simp add: card_insert_if) @@ -1482,21 +1476,24 @@ qed qed -lemma card_seteq: "finite B \ (\A. A \ B \ card B \ card A \ A = B)" - apply (induct rule: finite_induct) - apply simp - apply clarify - apply (subgoal_tac "finite A \ A - {x} \ F") - prefer 2 apply (blast intro: finite_subset, atomize) - apply (drule_tac x = "A - {x}" in spec) - apply (simp add: card_Diff_singleton_if split: if_split_asm) - apply (case_tac "card A", auto) - done +lemma card_seteq: + assumes "finite B" and A: "A \ B" "card B \ card A" + shows "A = B" + using assms +proof (induction arbitrary: A rule: finite_induct) + case (insert b B) + then have A: "finite A" "A - {b} \ B" + by force+ + then have "card B \ card (A - {b})" + using insert by (auto simp add: card_Diff_singleton_if) + then have "A - {b} = B" + using A insert.IH by auto + then show ?case + using insert.hyps insert.prems by auto +qed auto lemma psubset_card_mono: "finite B \ A < B \ card A < card B" - apply (simp add: psubset_eq linorder_not_le [symmetric]) - apply (blast dest: card_seteq) - done + using card_seteq [of B A] by (auto simp add: psubset_eq) lemma card_Un_Int: assumes "finite A" "finite B" @@ -1579,15 +1576,29 @@ finally show ?thesis . qed +lemma card_Diff1_less_iff: "card (A - {x}) < card A \ finite A \ x \ A" +proof (cases "finite A \ x \ A") + case True + then show ?thesis + by (auto simp: card_gt_0_iff intro: diff_less) +qed auto + lemma card_Diff1_less: "finite A \ x \ A \ card (A - {x}) < card A" - by (rule Suc_less_SucD) (simp add: card_Suc_Diff1 del: card_Diff_insert) + unfolding card_Diff1_less_iff by auto -lemma card_Diff2_less: "finite A \ x \ A \ y \ A \ card (A - {x} - {y}) < card A" - apply (cases "x = y") - apply (simp add: card_Diff1_less del:card_Diff_insert) - apply (rule less_trans) - prefer 2 apply (auto intro!: card_Diff1_less simp del: card_Diff_insert) - done +lemma card_Diff2_less: + assumes "finite A" "x \ A" "y \ A" shows "card (A - {x} - {y}) < card A" +proof (cases "x = y") + case True + with assms show ?thesis + by (simp add: card_Diff1_less del: card_Diff_insert) +next + case False + then have "card (A - {x} - {y}) < card (A - {x})" "card (A - {x}) < card A" + using assms by (intro card_Diff1_less; simp)+ + then show ?thesis + by (blast intro: less_trans) +qed lemma card_Diff1_le: "finite A \ card (A - {x}) \ card A" by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le) @@ -1618,10 +1629,8 @@ obtain f where "f ` s \ t" "inj_on f s" by blast with "2.prems"(2) "2.hyps"(2) show ?case - apply - - apply (rule exI[where x = "\z. if z = x then y else f z"]) - apply (auto simp add: inj_on_def) - done + unfolding inj_on_def + by (rule_tac x = "\z. if z = x then y else f z" in exI) auto qed qed @@ -1800,10 +1809,7 @@ lemma card_Suc_eq: "card A = Suc k \ (\b B. A = insert b B \ b \ B \ card B = k \ (k = 0 \ B = {}))" - apply (auto elim!: card_eq_SucD) - apply (subst card.insert) - apply (auto simp add: intro:ccontr) - done + by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD) lemma card_1_singletonE: assumes "card A = 1" @@ -1836,10 +1842,11 @@ lemma card_le_Suc_iff: "Suc n \ card A = (\a B. A = insert a B \ a \ B \ n \ card B \ finite B)" -apply(cases "finite A") - apply (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff - dest: subset_singletonD split: nat.splits if_splits) -by auto +proof (cases "finite A") + case True + then show ?thesis + by (fastforce simp: card_Suc_eq less_eq_nat.simps split: nat.splits) +qed auto lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \ 'b) set)" @@ -1886,7 +1893,7 @@ case False obtain n::nat where n: "n > max C 0" by auto obtain G where G: "G \ F" "card G = n" using infinite_arbitrarily_large[OF False] by auto - hence "finite G" using \n > max C 0\ using card_infinite gr_implies_not0 by blast + hence "finite G" using \n > max C 0\ using card.infinite gr_implies_not0 by blast hence False using assms G n not_less by auto thus ?thesis .. next @@ -2042,12 +2049,11 @@ case empty show ?case by simp next - case insert - then show ?case - apply simp - apply (subst card_Un_disjoint) - apply (auto simp add: disjoint_eq_subset_Compl) - done + case (insert c C) + then have "c \ \C = {}" + by auto + with insert show ?case + by (simp add: card_Un_disjoint) qed qed @@ -2209,10 +2215,10 @@ then have "X (A - {x})" using psubset.hyps by blast show False - apply (rule psubset.IH [where B = "A - {x}"]) - apply (use \x \ A\ in blast) - apply (simp add: \X (A - {x})\) - done + proof (rule psubset.IH [where B = "A - {x}"]) + show "A - {x} \ A" + using \x \ A\ by blast + qed fact qed qed diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Library/FSet.thy Fri Sep 25 17:13:12 2020 +0100 @@ -600,7 +600,7 @@ lemma fcard_fempty: "fcard {||} = 0" - by transfer (rule card_empty) + by transfer (rule card.empty) lemma fcard_finsert_disjoint: "x |\| A \ fcard (finsert x A) = Suc (fcard A)" @@ -632,7 +632,7 @@ using assms by transfer (rule card_Diff_insert) lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A |-| {|x|}))" -by transfer (rule card_insert) +by transfer (rule card.insert_remove) lemma fcard_finsert_le: "fcard A \ fcard (finsert x A)" by transfer (rule card_insert_le) diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Library/Infinite_Set.thy Fri Sep 25 17:13:12 2020 +0100 @@ -417,7 +417,7 @@ proof (induction n arbitrary: S) case 0 then show ?case - by (metis all_not_in_conv card_empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1)) + by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1)) next case (Suc n) show ?case diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Library/Perm.thy --- a/src/HOL/Library/Perm.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Library/Perm.thy Fri Sep 25 17:13:12 2020 +0100 @@ -365,7 +365,7 @@ then obtain B b where "affected f = insert b B" by blast with finite_affected [of f] have "card (affected f) \ 1" - by (simp add: card_insert) + by (simp add: card.insert_remove) case False then have "order f a = 1" by (simp add: order_eq_one_iff) with \card (affected f) \ 1\ show ?thesis diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Library/Permutations.thy Fri Sep 25 17:13:12 2020 +0100 @@ -347,7 +347,7 @@ by auto then have "finite ?pF" by (auto intro: card_ge_0_finite) - with \finite F\ card_insert have pF'f: "finite ?pF'" + with \finite F\ card.insert_remove have pF'f: "finite ?pF'" apply (simp only: Collect_case_prod Collect_mem_eq) apply (rule finite_cartesian_product) apply simp_all diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/List.thy --- a/src/HOL/List.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/List.thy Fri Sep 25 17:13:12 2020 +0100 @@ -5326,7 +5326,7 @@ assumes "k < card A" shows "card {xs. length xs = k \ distinct xs \ set xs \ A} = \{card A - k + 1 .. card A}" proof - - from \k < card A\ have "finite A" and "k \ card A" using card_infinite by force+ + from \k < card A\ have "finite A" and "k \ card A" using card.infinite by force+ from this show ?thesis by (rule card_lists_distinct_length_eq) qed diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Number_Theory/Quadratic_Reciprocity.thy --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Fri Sep 25 17:13:12 2020 +0100 @@ -294,7 +294,7 @@ have "B \ C = {}" "finite B" "finite C" "B \ C = BuC" unfolding B_def C_def BuC_def by fastforce+ then show ?thesis - unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce + unfolding b_def c_def using card.empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce qed definition f_2:: "int \ int" diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy --- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Fri Sep 25 17:13:12 2020 +0100 @@ -235,7 +235,7 @@ assume H: "liseq' xs j = card is" "is \ iseq xs (Suc j)" "finite is" "Max is = j" "is \ {}" from H j have "card is + 1 = card (is \ {i})" - by (simp add: card_insert max_notin) + by (simp add: card.insert_remove max_notin) moreover { from H j have "xs (Max is) \ xs i" by simp moreover from \j < i\ have "Suc j \ i" by simp @@ -367,7 +367,7 @@ apply (rule_tac xs=xs and i=i in liseq'_expand) apply simp apply (rule_tac js="isa \ {j}" in liseq_eq [symmetric]) - apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (simp add: card.insert_remove card_Diff_singleton_if max_notin) apply (rule iseq_insert) apply simp apply (erule iseq_mono) @@ -388,9 +388,9 @@ apply simp apply (rule le_diff_iff [THEN iffD1, of 1]) apply (simp add: card_0_eq [symmetric] del: card_0_eq) - apply (simp add: card_insert) + apply (simp add: card.insert_remove) apply (subgoal_tac "card (js' - {j}) = card js' - 1") - apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (simp add: card.insert_remove card_Diff_singleton_if max_notin) apply (frule_tac A=js' in Max_in) apply assumption apply (simp add: card_Diff_singleton_if) @@ -411,7 +411,7 @@ apply (rule_tac xs=xs and i=i in liseq'_expand) apply simp apply (rule_tac js="isa \ {j}" in liseq'_eq [symmetric]) - apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (simp add: card.insert_remove card_Diff_singleton_if max_notin) apply (rule iseq_insert) apply simp apply (erule iseq_mono) @@ -434,9 +434,9 @@ apply simp apply (rule le_diff_iff [THEN iffD1, of 1]) apply (simp add: card_0_eq [symmetric] del: card_0_eq) - apply (simp add: card_insert) + apply (simp add: card.insert_remove) apply (subgoal_tac "card (js' - {j}) = card js' - 1") - apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (simp add: card.insert_remove card_Diff_singleton_if max_notin) apply (frule_tac A=js' in Max_in) apply assumption apply (simp add: card_Diff_singleton_if) diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Set_Interval.thy Fri Sep 25 17:13:12 2020 +0100 @@ -1538,7 +1538,7 @@ also have "\ = Suc (card ({k \ M. k < Suc i} - {0}))" by (force intro: arg_cong [where f=card]) also have "\ = card (insert 0 ({k \ M. k < Suc i} - {0}))" - by (simp add: card_insert) + by (simp add: card.insert_remove) also have "... = card {k \ M. k < Suc i}" using assms by (force simp add: intro: arg_cong [where f=card]) diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Vector_Spaces.thy --- a/src/HOL/Vector_Spaces.thy Fri Sep 25 16:32:41 2020 +0200 +++ b/src/HOL/Vector_Spaces.thy Fri Sep 25 17:13:12 2020 +0100 @@ -1453,7 +1453,7 @@ have "b \ f ` B1" using vs2.span_base[of b "f ` B1"] b by auto then have "Suc (card B1) = card (insert b (f ` B1))" - using sf[THEN inj_on_subset, of B1] by (subst card_insert) (auto intro: vs1.finite_Basis simp: card_image) + using sf[THEN inj_on_subset, of B1] by (subst card.insert_remove) (auto intro: vs1.finite_Basis simp: card_image) also have "\ = vs2.dim (insert b (f ` B1))" using vs2.dim_eq_card_independent[OF **] by simp also have "vs2.dim (insert b (f ` B1)) \ vs2.dim B2"