--- 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:
--- 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"
--- 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 +
--- 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)" . }
--- 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
--- 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