--- a/NEWS Wed Mar 27 10:54:47 2024 +0100
+++ b/NEWS Wed Mar 27 15:16:09 2024 +0000
@@ -61,6 +61,9 @@
"preplay_timeout". INCOMPATIBILITY.
- Added the action "order" testing the proof method of the same name.
+* HOL-ex.Sketch_and_Explore: improvements to generate more natural and
+readable proof sketches from proof states.
+
* Explicit type class for discrete_linear_ordered_semidom for integral
semidomains with a discrete linear order.
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Mar 27 10:54:47 2024 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Mar 27 15:16:09 2024 +0000
@@ -2439,6 +2439,51 @@
\<Longrightarrow> setdist {x} S > 0"
using less_eq_real_def setdist_eq_0_closedin by fastforce
+text \<open>A consequence of the results above\<close>
+lemma compact_minkowski_sum_cball:
+ fixes A :: "'a :: heine_borel set"
+ assumes "compact A"
+ shows "compact (\<Union>x\<in>A. cball x r)"
+proof (cases "A = {}")
+ case False
+ show ?thesis
+ unfolding compact_eq_bounded_closed
+ proof safe
+ have "open (-(\<Union>x\<in>A. cball x r))"
+ unfolding open_dist
+ proof safe
+ fix x assume x: "x \<notin> (\<Union>x\<in>A. cball x r)"
+ have "\<exists>x'\<in>{x}. \<exists>y\<in>A. dist x' y = setdist {x} A"
+ using \<open>A \<noteq> {}\<close> assms
+ by (intro setdist_compact_closed) (auto simp: compact_imp_closed)
+ then obtain y where y: "y \<in> A" "dist x y = setdist {x} A"
+ by blast
+ with x have "setdist {x} A > r"
+ by (auto simp: dist_commute)
+ moreover have "False" if "dist z x < setdist {x} A - r" "u \<in> A" "z \<in> cball u r" for z u
+ by (smt (verit, del_insts) mem_cball setdist_Lipschitz setdist_sing_in_set that)
+ ultimately
+ show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> - (\<Union>x\<in>A. cball x r)"
+ by (force intro!: exI[of _ "setdist {x} A - r"])
+ qed
+ thus "closed (\<Union>x\<in>A. cball x r)"
+ using closed_open by blast
+ next
+ from assms have "bounded A"
+ by (simp add: compact_imp_bounded)
+ then obtain x c where c: "\<And>y. y \<in> A \<Longrightarrow> dist x y \<le> c"
+ unfolding bounded_def by blast
+ have "\<forall>y\<in>(\<Union>x\<in>A. cball x r). dist x y \<le> c + r"
+ proof safe
+ fix y z assume *: "y \<in> A" "z \<in> cball y r"
+ thus "dist x z \<le> c + r"
+ using * c[of y] cball_trans mem_cball by blast
+ qed
+ thus "bounded (\<Union>x\<in>A. cball x r)"
+ unfolding bounded_def by blast
+ qed
+qed auto
+
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 27 10:54:47 2024 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 27 15:16:09 2024 +0000
@@ -390,26 +390,6 @@
"DERIV_floatarith x (Num f) = Num 0" |
"DERIV_floatarith x (Var n) = (if x = n then Num 1 else Num 0)"
-lemma has_real_derivative_powr':
- fixes f g :: "real \<Rightarrow> real"
- assumes "(f has_real_derivative f') (at x)"
- assumes "(g has_real_derivative g') (at x)"
- assumes "f x > 0"
- defines "h \<equiv> \<lambda>x. f x powr g x * (g' * ln (f x) + f' * g x / f x)"
- shows "((\<lambda>x. f x powr g x) has_real_derivative h x) (at x)"
-proof (subst DERIV_cong_ev[OF refl _ refl])
- from assms have "isCont f x"
- by (simp add: DERIV_continuous)
- hence "f \<midarrow>x\<rightarrow> f x" by (simp add: continuous_at)
- with \<open>f x > 0\<close> have "eventually (\<lambda>x. f x > 0) (nhds x)"
- by (auto simp: tendsto_at_iff_tendsto_nhds dest: order_tendstoD)
- thus "eventually (\<lambda>x. f x powr g x = exp (g x * ln (f x))) (nhds x)"
- by eventually_elim (simp add: powr_def)
-next
- from assms show "((\<lambda>x. exp (g x * ln (f x))) has_real_derivative h x) (at x)"
- by (auto intro!: derivative_eq_intros simp: h_def powr_def)
-qed
-
lemma DERIV_floatarith:
assumes "n < length vs"
assumes isDERIV: "isDERIV n f (vs[n := x])"
--- a/src/HOL/Probability/Information.thy Wed Mar 27 10:54:47 2024 +0100
+++ b/src/HOL/Probability/Information.thy Wed Mar 27 15:16:09 2024 +0000
@@ -857,7 +857,7 @@
using int X by (intro entropy_le) auto
also have "\<dots> \<le> log b (measure MX (space MX))"
using Px distributed_imp_emeasure_nonzero[OF X]
- by (intro log_le)
+ by (intro Transcendental.log_mono)
(auto intro!: finite_measure_mono b_gt_1 less_le[THEN iffD2]
simp: emeasure_eq_measure cong: conj_cong)
finally show ?thesis .
@@ -1087,7 +1087,7 @@
done
have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
- proof (intro le_imp_neg_le log_le[OF b_gt_1])
+ proof (intro le_imp_neg_le Transcendental.log_mono[OF b_gt_1])
have If: "integrable ?P ?f"
unfolding real_integrable_def
proof (intro conjI)
@@ -1332,7 +1332,7 @@
by (auto simp: split_beta')
have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
- proof (intro le_imp_neg_le log_le[OF b_gt_1])
+ proof (intro le_imp_neg_le Transcendental.log_mono[OF b_gt_1])
have If: "integrable ?P ?f"
using neg fin by (force simp add: real_integrable_def)
then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Mar 27 10:54:47 2024 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Mar 27 15:16:09 2024 +0000
@@ -473,7 +473,7 @@
using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite _ refl]] by simp
also have "\<dots> \<le> log b (real (n + 1)^card observations)"
using card_T_bound not_empty
- by (auto intro!: log_le simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
+ by (auto intro!: log_mono simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
also have "\<dots> = real (card observations) * log b (real n + 1)"
by (simp add: log_nat_power add.commute)
finally show ?thesis .
--- a/src/HOL/Transcendental.thy Wed Mar 27 10:54:47 2024 +0100
+++ b/src/HOL/Transcendental.thy Wed Mar 27 15:16:09 2024 +0000
@@ -2665,7 +2665,7 @@
lemma log_le_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x \<le> log a y \<longleftrightarrow> x \<le> y"
by (simp flip: linorder_not_less)
-lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
+lemma log_mono: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
by simp
lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
@@ -3201,6 +3201,27 @@
declare has_real_derivative_powr[THEN DERIV_chain2, derivative_intros]
+text \<open>A more general version, by Johannes Hölzl\<close>
+lemma has_real_derivative_powr':
+ fixes f g :: "real \<Rightarrow> real"
+ assumes "(f has_real_derivative f') (at x)"
+ assumes "(g has_real_derivative g') (at x)"
+ assumes "f x > 0"
+ defines "h \<equiv> \<lambda>x. f x powr g x * (g' * ln (f x) + f' * g x / f x)"
+ shows "((\<lambda>x. f x powr g x) has_real_derivative h x) (at x)"
+proof (subst DERIV_cong_ev[OF refl _ refl])
+ from assms have "isCont f x"
+ by (simp add: DERIV_continuous)
+ hence "f \<midarrow>x\<rightarrow> f x" by (simp add: continuous_at)
+ with \<open>f x > 0\<close> have "eventually (\<lambda>x. f x > 0) (nhds x)"
+ by (auto simp: tendsto_at_iff_tendsto_nhds dest: order_tendstoD)
+ thus "eventually (\<lambda>x. f x powr g x = exp (g x * ln (f x))) (nhds x)"
+ by eventually_elim (simp add: powr_def)
+next
+ from assms show "((\<lambda>x. exp (g x * ln (f x))) has_real_derivative h x) (at x)"
+ by (auto intro!: derivative_eq_intros simp: h_def powr_def)
+qed
+
lemma tendsto_zero_powrI:
assumes "(f \<longlongrightarrow> (0::real)) F" "(g \<longlongrightarrow> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> 0) F"