# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1711552569 0
# Node ID 95b4fb2b5359e51ee6cc953923905379df0d5c3f
# Parent  b0a46cf73aa478c6559cc8d92276664e78420bf2
New material and a bit of refactoring

diff -r b0a46cf73aa4 -r 95b4fb2b5359 NEWS
--- 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.
 
diff -r b0a46cf73aa4 -r 95b4fb2b5359 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- 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)
 
diff -r b0a46cf73aa4 -r 95b4fb2b5359 src/HOL/Decision_Procs/Approximation.thy
--- 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])"
diff -r b0a46cf73aa4 -r 95b4fb2b5359 src/HOL/Probability/Information.thy
--- 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)"
diff -r b0a46cf73aa4 -r 95b4fb2b5359 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- 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  .
diff -r b0a46cf73aa4 -r 95b4fb2b5359 src/HOL/Transcendental.thy
--- 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"