# HG changeset patch # User paulson # Date 1724603082 -3600 # Node ID 77f7aa898ced4f3a2c3561b490256078d657c72d # Parent 8f96e1329845348c1d82e8180e2194fd680bf587 A bit more tidying diff -r 8f96e1329845 -r 77f7aa898ced src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Sat Aug 24 23:44:05 2024 +0100 +++ b/src/HOL/Lattices_Big.thy Sun Aug 25 17:24:42 2024 +0100 @@ -935,41 +935,33 @@ \y. P y \ \ f y < f x; \x. \ P x; \y. P y \ \ f y < f x \ \ Q x \ \ Q (arg_min f P)" -apply (simp add: arg_min_def is_arg_min_def) -apply (rule someI2_ex) - apply blast -apply blast -done + unfolding arg_min_def is_arg_min_def + by (blast intro!: someI2_ex) lemma arg_min_equality: "\ P k; \x. P x \ f k \ f x \ \ f (arg_min f P) = f k" for f :: "_ \ 'a::order" -apply (rule arg_minI) - apply assumption - apply (simp add: less_le_not_le) -by (metis le_less) + by (rule arg_minI; force simp: not_less less_le_not_le) lemma wf_linord_ex_has_least: "\ wf r; \x y. (x, y) \ r\<^sup>+ \ (y, x) \ r\<^sup>*; P k \ \ \x. P x \ (\y. P y \ (m x, m y) \ r\<^sup>*)" -apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) -apply (drule_tac x = "m ` Collect P" in spec) -by force + by (force dest!: wf_trancl [THEN wf_eq_minimal [THEN iffD1, THEN spec], where x = "m ` Collect P"]) lemma ex_has_least_nat: "P k \ \x. P x \ (\y. P y \ m x \ m y)" for m :: "'a \ nat" -apply (simp only: pred_nat_trancl_eq_le [symmetric]) -apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) - apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le) -by assumption + unfolding pred_nat_trancl_eq_le [symmetric] + apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) + apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le) + by assumption lemma arg_min_nat_lemma: "P k \ P(arg_min m P) \ (\y. P y \ m (arg_min m P) \ m y)" for m :: "'a \ nat" -apply (simp add: arg_min_def is_arg_min_linorder) -apply (rule someI_ex) -apply (erule ex_has_least_nat) -done + unfolding arg_min_def is_arg_min_linorder + apply (rule someI_ex) + apply (erule ex_has_least_nat) + done lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1] @@ -979,35 +971,35 @@ lemma arg_min_nat_le: "P x \ m (arg_min m P) \ m x" for m :: "'a \ nat" -by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) + by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) lemma ex_min_if_finite: "\ finite S; S \ {} \ \ \m\S. \(\x\S. x < (m::'a::order))" -by(induction rule: finite.induct) (auto intro: order.strict_trans) + by(induction rule: finite.induct) (auto intro: order.strict_trans) lemma ex_is_arg_min_if_finite: fixes f :: "'a \ 'b :: order" -shows "\ finite S; S \ {} \ \ \x. is_arg_min f (\x. x \ S) x" -unfolding is_arg_min_def -using ex_min_if_finite[of "f ` S"] -by auto + shows "\ finite S; S \ {} \ \ \x. is_arg_min f (\x. x \ S) x" + unfolding is_arg_min_def + using ex_min_if_finite[of "f ` S"] + by auto lemma arg_min_SOME_Min: "finite S \ arg_min_on f S = (SOME y. y \ S \ f y = Min(f ` S))" -unfolding arg_min_on_def arg_min_def is_arg_min_linorder -apply(rule arg_cong[where f = Eps]) -apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric]) -done + unfolding arg_min_on_def arg_min_def is_arg_min_linorder + apply(rule arg_cong[where f = Eps]) + apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric]) + done lemma arg_min_if_finite: fixes f :: "'a \ 'b :: order" -assumes "finite S" "S \ {}" -shows "arg_min_on f S \ S" and "\(\x\S. f x < f (arg_min_on f S))" -using ex_is_arg_min_if_finite[OF assms, of f] -unfolding arg_min_on_def arg_min_def is_arg_min_def -by(auto dest!: someI_ex) + assumes "finite S" "S \ {}" + shows "arg_min_on f S \ S" and "\(\x\S. f x < f (arg_min_on f S))" + using ex_is_arg_min_if_finite[OF assms, of f] + unfolding arg_min_on_def arg_min_def is_arg_min_def + by(auto dest!: someI_ex) lemma arg_min_least: fixes f :: "'a \ 'b :: linorder" -shows "\ finite S; S \ {}; y \ S \ \ f(arg_min_on f S) \ f y" -by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f) + shows "\ finite S; S \ {}; y \ S \ \ f(arg_min_on f S) \ f y" + by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f) lemma arg_min_inj_eq: fixes f :: "'a \ 'b :: order" shows "\ inj_on f {x. P x}; P a; \y. P y \ f a \ f y \ \ arg_min f P = a" @@ -1048,11 +1040,8 @@ (\y. P y \ \ f y > f x) \ (\x. P x \ \y. P y \ \ f y > f x \ Q x) \ Q (arg_max f P)" -apply (simp add: arg_max_def is_arg_max_def) -apply (rule someI2_ex) - apply blast -apply blast -done + unfolding arg_max_def is_arg_max_def + by (blast intro!: someI2_ex elim: ) lemma arg_max_equality: "\ P k; \x. P x \ f x \ f k \ \ f (arg_max f P) = f k" @@ -1086,15 +1075,13 @@ "\ P k; \y. P y \ f y < b \ \ P (arg_max f P) \ (\y. P y \ f y \ f (arg_max f P))" for f :: "'a \ nat" -apply (simp add: arg_max_def is_arg_max_linorder) -apply (rule someI_ex) -apply (erule (1) ex_has_greatest_nat) -done + unfolding arg_max_def is_arg_max_linorder + by (rule someI_ex) (metis ex_has_greatest_nat) lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1] lemma arg_max_nat_le: "P x \ \y. P y \ f y < b \ f x \ f (arg_max f P)" for f :: "'a \ nat" -by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P]) + using arg_max_nat_lemma by metis end diff -r 8f96e1329845 -r 77f7aa898ced src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Sat Aug 24 23:44:05 2024 +0100 +++ b/src/HOL/MacLaurin.thy Sun Aug 25 17:24:42 2024 +0100 @@ -341,9 +341,7 @@ show "\m t. m < n \ 0 \ t \ t \ x \ ((\u. sin (u + 1/2 * real m * pi)) has_real_derivative sin (t + 1/2 * real (Suc m) * pi)) (at t)" - apply (simp add: sin_expansion_lemma del: of_nat_Suc) - apply (force intro!: derivative_eq_intros) - done + using DERIV_shift sin_expansion_lemma by fastforce qed (use assms in auto) then show ?thesis apply (rule ex_forward, simp) @@ -362,9 +360,7 @@ show "\m t. m < n \ 0 \ t \ t \ x \ ((\u. sin (u + 1/2 * real m * pi)) has_real_derivative sin (t + 1/2 * real (Suc m) * pi)) (at t)" - apply (simp add: sin_expansion_lemma del: of_nat_Suc) - apply (force intro!: derivative_eq_intros) - done + using DERIV_shift sin_expansion_lemma by fastforce qed (use assms in auto) then show ?thesis apply (rule ex_forward, simp) @@ -477,8 +473,7 @@ apply (subst t2) apply (rule sin_bound_lemma) apply (rule sum.cong[OF refl]) - unfolding sin_coeff_def - apply (subst diff_m_0, simp) + apply (simp add: diff_m_0 sin_coeff_def) using est apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono simp: ac_simps divide_inverse power_abs [symmetric] abs_mult)