# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1554383973 -3600
# Node ID da5857dbcbb9326bc5da162e2c84281d5c7c57c4
# Parent  350acd3670285741742b3fe6c162c099abdf2c00
More group theory. Sum and product indexed by the non-neutral part of a set

diff -r 350acd367028 -r da5857dbcbb9 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -547,6 +547,61 @@
     finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
   unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
 
+lemma finprod_singleton_swap:
+  assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
+  shows "(\<Otimes>j\<in>A. if j = i then f j else \<one>) = f i"
+  using finprod_singleton [OF assms] by (simp add: eq_commute)
+
+lemma finprod_mono_neutral_cong_left:
+  assumes "finite B"
+    and "A \<subseteq> B"
+    and 1: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>"
+    and gh: "\<And>x. x \<in> A \<Longrightarrow> g x = h x"
+    and h: "h \<in> B \<rightarrow> carrier G"
+  shows "finprod G g A = finprod G h B"
+proof-
+  have eq: "A \<union> (B - A) = B" using \<open>A \<subseteq> B\<close> by blast
+  have d: "A \<inter> (B - A) = {}" using \<open>A \<subseteq> B\<close> by blast
+  from \<open>finite B\<close> \<open>A \<subseteq> B\<close> have f: "finite A" "finite (B - A)"
+    by (auto intro: finite_subset)
+  have "h \<in> A \<rightarrow> carrier G" "h \<in> B - A \<rightarrow> carrier G"
+    using assms by (auto simp: image_subset_iff_funcset)
+  moreover have "finprod G g A = finprod G h A \<otimes> finprod G h (B - A)"
+  proof -
+    have "finprod G h (B - A) = \<one>"
+      using "1" finprod_one_eqI by blast
+    moreover have "finprod G g A = finprod G h A"
+      using \<open>h \<in> A \<rightarrow> carrier G\<close> finprod_cong' gh by blast
+    ultimately show ?thesis
+      by (simp add: \<open>h \<in> A \<rightarrow> carrier G\<close>)
+  qed
+  ultimately show ?thesis
+    by (simp add: finprod_Un_disjoint [OF f d, unfolded eq])
+qed
+
+lemma finprod_mono_neutral_cong_right:
+  assumes "finite B"
+    and "A \<subseteq> B" "\<And>i. i \<in> B - A \<Longrightarrow> g i = \<one>" "\<And>x. x \<in> A \<Longrightarrow> g x = h x" "g \<in> B \<rightarrow> carrier G"
+  shows "finprod G g B = finprod G h A"
+  using assms  by (auto intro!: finprod_mono_neutral_cong_left [symmetric])
+
+lemma finprod_mono_neutral_cong:
+  assumes [simp]: "finite B" "finite A"
+    and *: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>" "\<And>i. i \<in> A - B \<Longrightarrow> g i = \<one>"
+    and gh: "\<And>x. x \<in> A \<inter> B \<Longrightarrow> g x = h x"
+    and g: "g \<in> A \<rightarrow> carrier G"
+    and h: "h \<in> B \<rightarrow> carrier G"
+ shows "finprod G g A = finprod G h B"
+proof-
+  have "finprod G g A = finprod G g (A \<inter> B)"
+    by (rule finprod_mono_neutral_cong_right) (use assms in auto)
+  also have "\<dots> = finprod G h (A \<inter> B)"
+    by (rule finprod_cong) (use assms in auto)
+  also have "\<dots> = finprod G h B"
+    by (rule finprod_mono_neutral_cong_left) (use assms in auto)
+  finally show ?thesis .
+qed
+
 end
 
 (* Jeremy Avigad. This should be generalized to arbitrary groups, not just commutative
diff -r 350acd367028 -r da5857dbcbb9 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -9,11 +9,6 @@
 imports Complete_Lattice "HOL-Library.FuncSet"
 begin
 
-(*MOVE*)
-lemma image_paired_Times:
-   "(\<lambda>(x,y). (f x,g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
-  by auto
-
 section \<open>Monoids and Groups\<close>
 
 subsection \<open>Definitions\<close>
diff -r 350acd367028 -r da5857dbcbb9 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -4063,7 +4063,7 @@
   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
 using openin_topology_generated_by_iff by auto
 
-lemma topology_generated_by_topspace:
+lemma topology_generated_by_topspace [simp]:
   "topspace (topology_generated_by S) = (\<Union>S)"
 proof
   {
diff -r 350acd367028 -r da5857dbcbb9 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -1459,25 +1459,6 @@
   qed
 qed
 
-text\<open>Deducing things about the limit from the elements.\<close>
-
-lemma Lim_in_closed_set:
-  assumes "closed S"
-    and "eventually (\<lambda>x. f(x) \<in> S) net"
-    and "\<not> trivial_limit net" "(f \<longlongrightarrow> l) net"
-  shows "l \<in> S"
-proof (rule ccontr)
-  assume "l \<notin> S"
-  with \<open>closed S\<close> have "open (- S)" "l \<in> - S"
-    by (simp_all add: open_Compl)
-  with assms(4) have "eventually (\<lambda>x. f x \<in> - S) net"
-    by (rule topological_tendstoD)
-  with assms(2) have "eventually (\<lambda>x. False) net"
-    by (rule eventually_elim2) simp
-  with assms(3) show "False"
-    by (simp add: eventually_False)
-qed
-
 text\<open>These are special for limits out of the same topological space.\<close>
 
 lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
diff -r 350acd367028 -r da5857dbcbb9 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Groups_Big.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -16,6 +16,8 @@
 locale comm_monoid_set = comm_monoid
 begin
 
+subsubsection \<open>Standard sum or product indexed by a finite set\<close>
+
 interpretation comp_fun_commute f
   by standard (simp add: fun_eq_iff left_commute)
 
@@ -523,6 +525,92 @@
   shows "F \<phi> A = F \<gamma> B"
   by (rule eq_general [where h=h]) (force intro: dest: A B)+
 
+subsubsection \<open>HOL Light variant: sum/product indexed by the non-neutral subset\<close>
+text \<open>NB only a subset of the properties above are proved\<close>
+
+definition G :: "['b \<Rightarrow> 'a,'b set] \<Rightarrow> 'a"
+  where "G p I \<equiv> if finite {x \<in> I. p x \<noteq> \<^bold>1} then F p {x \<in> I. p x \<noteq> \<^bold>1} else \<^bold>1"
+
+lemma finite_Collect_op:
+  shows "\<lbrakk>finite {i \<in> I. x i \<noteq> \<^bold>1}; finite {i \<in> I. y i \<noteq> \<^bold>1}\<rbrakk> \<Longrightarrow> finite {i \<in> I. x i \<^bold>* y i \<noteq> \<^bold>1}"
+  apply (rule finite_subset [where B = "{i \<in> I. x i \<noteq> \<^bold>1} \<union> {i \<in> I. y i \<noteq> \<^bold>1}"]) 
+  using left_neutral by force+
+
+lemma empty' [simp]: "G p {} = \<^bold>1"
+  by (auto simp: G_def)
+
+lemma eq_sum [simp]: "finite I \<Longrightarrow> G p I = F p I"
+  by (auto simp: G_def intro: mono_neutral_cong_left)
+
+lemma insert' [simp]:
+  assumes "finite {x \<in> I. p x \<noteq> \<^bold>1}"
+  shows "G p (insert i I) = (if i \<in> I then G p I else p i \<^bold>* G p I)"
+proof -
+  have "{x. x = i \<and> p x \<noteq> \<^bold>1 \<or> x \<in> I \<and> p x \<noteq> \<^bold>1} = (if p i = \<^bold>1 then {x \<in> I. p x \<noteq> \<^bold>1} else insert i {x \<in> I. p x \<noteq> \<^bold>1})"
+    by auto
+  then show ?thesis
+    using assms by (simp add: G_def conj_disj_distribR insert_absorb)
+qed
+
+lemma distrib_triv':
+  assumes "finite I"
+  shows "G (\<lambda>i. g i \<^bold>* h i) I = G g I \<^bold>* G h I"
+  by (simp add: assms local.distrib)
+
+lemma non_neutral': "G g {x \<in> I. g x \<noteq> \<^bold>1} = G g I"
+  by (simp add: G_def)
+
+lemma distrib':
+  assumes "finite {x \<in> I. g x \<noteq> \<^bold>1}" "finite {x \<in> I. h x \<noteq> \<^bold>1}"
+  shows "G (\<lambda>i. g i \<^bold>* h i) I = G g I \<^bold>* G h I"
+proof -
+  have "a \<^bold>* a \<noteq> a \<Longrightarrow> a \<noteq> \<^bold>1" for a
+    by auto
+  then have "G (\<lambda>i. g i \<^bold>* h i) I = G (\<lambda>i. g i \<^bold>* h i) ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1})"
+    using assms  by (force simp: G_def finite_Collect_op intro!: mono_neutral_cong)
+  also have "\<dots> = G g I \<^bold>* G h I"
+  proof -
+    have "F g ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1}) = G g I"
+         "F h ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1}) = G h I"
+      by (auto simp: G_def assms intro: mono_neutral_right)
+    then show ?thesis
+      using assms by (simp add: distrib)
+  qed
+  finally show ?thesis .
+qed
+
+lemma cong':
+  assumes "A = B"
+  assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
+  shows "G g A = G h B"
+  using assms by (auto simp: G_def cong: conj_cong intro: cong)
+
+
+lemma mono_neutral_cong_left':
+  assumes "S \<subseteq> T"
+    and "\<And>i. i \<in> T - S \<Longrightarrow> h i = \<^bold>1"
+    and "\<And>x. x \<in> S \<Longrightarrow> g x = h x"
+  shows "G g S = G h T"
+proof -
+  have *: "{x \<in> S. g x \<noteq> \<^bold>1} = {x \<in> T. h x \<noteq> \<^bold>1}"
+    using assms by (metis DiffI subset_eq) 
+  then have "finite {x \<in> S. g x \<noteq> \<^bold>1} = finite {x \<in> T. h x \<noteq> \<^bold>1}"
+    by simp
+  then show ?thesis
+    using assms by (auto simp add: G_def * intro: cong)
+qed
+
+lemma mono_neutral_cong_right':
+  "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> g x = h x) \<Longrightarrow>
+    G g T = G h S"
+  by (auto intro!: mono_neutral_cong_left' [symmetric])
+
+lemma mono_neutral_left': "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> G g S = G g T"
+  by (blast intro: mono_neutral_cong_left')
+
+lemma mono_neutral_right': "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> G g T = G g S"
+  by (blast intro!: mono_neutral_left' [symmetric])
+
 end
 
 
@@ -532,7 +620,7 @@
 begin
 
 sublocale sum: comm_monoid_set plus 0
-  defines sum = sum.F ..
+  defines sum = sum.F and sum' = sum.G ..
 
 abbreviation Sum ("\<Sum>")
   where "\<Sum> \<equiv> sum (\<lambda>x. x)"
@@ -1134,7 +1222,7 @@
 begin
 
 sublocale prod: comm_monoid_set times 1
-  defines prod = prod.F ..
+  defines prod = prod.F and prod' = prod.G ..
 
 abbreviation Prod ("\<Prod>_" [1000] 999)
   where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
diff -r 350acd367028 -r da5857dbcbb9 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Product_Type.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -1137,6 +1137,10 @@
 lemma Times_Int_Times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   by auto
 
+lemma image_paired_Times:
+   "(\<lambda>(x,y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
+  by auto
+
 lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
   by (auto simp add: set_eq_iff)