--- 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 @@
\<And>y. P y \<Longrightarrow> \<not> f y < f x;
\<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
\<Longrightarrow> 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:
"\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k"
for f :: "_ \<Rightarrow> '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:
"\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk>
\<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> 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 \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
for m :: "'a \<Rightarrow> 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 \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)"
for m :: "'a \<Rightarrow> 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 \<Longrightarrow> m (arg_min m P) \<le> m x"
for m :: "'a \<Rightarrow> 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:
"\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>m\<in>S. \<not>(\<exists>x\<in>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 \<Rightarrow> 'b :: order"
-shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x"
-unfolding is_arg_min_def
-using ex_min_if_finite[of "f ` S"]
-by auto
+ shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x"
+ unfolding is_arg_min_def
+ using ex_min_if_finite[of "f ` S"]
+ by auto
lemma arg_min_SOME_Min:
"finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> 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 \<Rightarrow> 'b :: order"
-assumes "finite S" "S \<noteq> {}"
-shows "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>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 \<noteq> {}"
+ shows "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>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 \<Rightarrow> 'b :: linorder"
-shows "\<lbrakk> finite S; S \<noteq> {}; y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y"
-by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)
+ shows "\<lbrakk> finite S; S \<noteq> {}; y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> 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 \<Rightarrow> 'b :: order"
shows "\<lbrakk> inj_on f {x. P x}; P a; \<forall>y. P y \<longrightarrow> f a \<le> f y \<rbrakk> \<Longrightarrow> arg_min f P = a"
@@ -1048,11 +1040,8 @@
(\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow>
(\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow>
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:
"\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k"
@@ -1086,15 +1075,13 @@
"\<lbrakk> P k; \<forall>y. P y \<longrightarrow> f y < b \<rbrakk>
\<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))"
for f :: "'a \<Rightarrow> 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 \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)"
for f :: "'a \<Rightarrow> nat"
-by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
+ using arg_max_nat_lemma by metis
end
--- 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 "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
((\<lambda>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 "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
((\<lambda>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)