# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1705412409 0
# Node ID c1b0f64eb8659d334956820b1a519f908d8b9b19
# Parent  1e19abf373ac590273e3d46044b4b56c730d826c
A few new results (mostly brought in from other developments)

diff -r 1e19abf373ac -r c1b0f64eb865 src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sun Jan 14 20:02:58 2024 +0000
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Tue Jan 16 13:40:09 2024 +0000
@@ -1033,11 +1033,8 @@
    "\<lbrakk>retraction_map X Y r; t0_space X\<rbrakk> \<Longrightarrow> t0_space Y"
   using hereditary_imp_retractive_property homeomorphic_t0_space t0_space_subtopology by blast
 
-lemma XY: "{x}\<times>{y} = {(x,y)}"
-  by simp
-
 lemma t0_space_prod_topologyI: "\<lbrakk>t0_space X; t0_space Y\<rbrakk> \<Longrightarrow> t0_space (prod_topology X Y)"
-  by (simp add: t0_space_closure_of_sing closure_of_Times closure_of_eq_empty_gen times_eq_iff flip: XY insert_Times_insert)
+  by (simp add: t0_space_closure_of_sing closure_of_Times closure_of_eq_empty_gen times_eq_iff flip: sing_Times_sing insert_Times_insert)
 
 
 lemma t0_space_prod_topology_iff:
diff -r 1e19abf373ac -r c1b0f64eb865 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Jan 14 20:02:58 2024 +0000
+++ b/src/HOL/Groups_Big.thy	Tue Jan 16 13:40:09 2024 +0000
@@ -409,6 +409,11 @@
   qed
 qed
 
+lemma cartesian_product':
+  "F g (A \<times> B) = F (\<lambda>x. F (\<lambda>y. g (x,y)) B) A"
+  unfolding cartesian_product by simp
+
+
 lemma inter_restrict:
   assumes "finite A"
   shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A"
diff -r 1e19abf373ac -r c1b0f64eb865 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Sun Jan 14 20:02:58 2024 +0000
+++ b/src/HOL/Probability/Information.thy	Tue Jan 16 13:40:09 2024 +0000
@@ -10,20 +10,6 @@
   Independent_Family
 begin
 
-lemma log_le: "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"
-  by simp
-
-lemma sum_cartesian_product':
-  "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. sum (\<lambda>y. f (x, y)) B)"
-  unfolding sum.cartesian_product by simp
-
-lemma split_pairs:
-  "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
-  "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
-
 subsection "Information theory"
 
 locale information_space = prob_space +
diff -r 1e19abf373ac -r c1b0f64eb865 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Jan 14 20:02:58 2024 +0000
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Jan 16 13:40:09 2024 +0000
@@ -96,7 +96,7 @@
     by force+
   show ?case unfolding *
     using Suc[of "\<lambda>i. P (Suc i)"]
-    by (simp add: sum.reindex sum_cartesian_product'
+    by (simp add: sum.reindex sum.cartesian_product'
       lessThan_Suc_eq_insert_0 prod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
 qed
 
@@ -157,7 +157,7 @@
 
   note sum_distrib_left[symmetric, simp]
   note sum_distrib_right[symmetric, simp]
-  note sum_cartesian_product'[simp]
+  note sum.cartesian_product'[simp]
 
   have "(\<Sum>ms | set ms \<subseteq> messages \<and> length ms = n. \<Prod>x<length ms. M (ms ! x)) = 1"
   proof (induct n)
@@ -255,7 +255,7 @@
   show "(\<P>(fst) {k}) = K k"
     apply (simp add: \<mu>'_eq)
     apply (simp add: * P_def)
-    apply (simp add: sum_cartesian_product')
+    apply (simp add: sum.cartesian_product')
     using prod_sum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] \<open>k \<in> keys\<close>
     by (auto simp add: sum_distrib_left[symmetric] subset_eq prod.neutral_const)
 qed
@@ -352,7 +352,7 @@
       also have "\<dots> =
           (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
         unfolding P_def using \<open>K k \<noteq> 0\<close> \<open>k \<in> keys\<close>
-        apply (simp add: sum_cartesian_product' sum_divide_distrib msgs_def ** cong: conj_cong)
+        apply (simp add: sum.cartesian_product' sum_divide_distrib msgs_def ** cong: conj_cong)
         apply (subst prod_sum_distrib_lists[OF M.finite_space]) ..
       finally have "(\<P>(OB ; fst) {(obs, k)}) / K k =
             (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
diff -r 1e19abf373ac -r c1b0f64eb865 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Jan 14 20:02:58 2024 +0000
+++ b/src/HOL/Product_Type.thy	Tue Jan 16 13:40:09 2024 +0000
@@ -987,6 +987,10 @@
 lemma snd_swap [simp]: "snd (prod.swap x) = fst x"
   by (cases x) simp
 
+lemma split_pairs:
+  "(A,B) = X \<longleftrightarrow> fst X = A \<and> snd X = B" and "X = (A,B) \<longleftrightarrow> fst X = A \<and> snd X = B" 
+  by auto
+
 text \<open>Disjoint union of a family of sets -- Sigma.\<close>
 
 definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set"
@@ -1162,6 +1166,9 @@
   "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> {a} \<times> B)"
   by blast
 
+lemma sing_Times_sing: "{x}\<times>{y} = {(x,y)}"
+  by simp
+
 lemma vimage_Times: "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
 proof (rule set_eqI)
   show "x \<in> f -` (A \<times> B) \<longleftrightarrow> x \<in> (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B" for x
diff -r 1e19abf373ac -r c1b0f64eb865 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Jan 14 20:02:58 2024 +0000
+++ b/src/HOL/Transcendental.thy	Tue Jan 16 13:40:09 2024 +0000
@@ -2640,7 +2640,13 @@
 qed
 
 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 add: linorder_not_less [symmetric])
+  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"
+  by simp
+
+lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
+  by simp
 
 lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
   using log_less_cancel_iff[of a 1 x] by simp