# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530042529 -3600
# Node ID 6b5f15387353f99c43210b5792a4008cd8c3da85
# Parent  0854edc4d415b4fad6d8751cafa74702fa79e71f
a few new lemmas

diff -r 0854edc4d415 -r 6b5f15387353 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Tue Jun 26 20:48:49 2018 +0100
@@ -50,13 +50,9 @@
   shows "H #> x = H <#> {x}"
   unfolding r_coset_def set_mult_def by simp
 
-(* ************************************************************************** *)
-
-
-(* ************************************************************************** *)
 (* Next five lemmas contributed by Paulo Emílio de Vilhena.                    *)
 
-lemma (in subgroup) rcosets_not_empty:
+lemma (in subgroup) rcosets_non_empty:
   assumes "R \<in> rcosets H"
   shows "R \<noteq> {}"
 proof -
@@ -87,6 +83,9 @@
   thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def)
 qed
 
+lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'"
+  unfolding set_mult_def by (simp add: UN_mono)
+
 
 subsection \<open>Stable Operations for Subgroups\<close>
 
@@ -105,7 +104,17 @@
   shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I"
   using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms)
 
-                                 
+lemma set_mult_consistent [simp]:
+  "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
+  unfolding set_mult_def by simp
+
+lemma r_coset_consistent [simp]:
+  "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h"
+  unfolding r_coset_def by simp
+
+lemma l_coset_consistent [simp]:
+  "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I"
+  unfolding l_coset_def by simp
 
 subsection \<open>Basic Properties of set multiplication\<close>
 
@@ -1123,15 +1132,15 @@
     unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
   moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
                 \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) =  x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)"
-    unfolding set_mult_def apply auto apply blast+.
+    unfolding set_mult_def by force
   moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
                  \<forall>ya\<in>carrier (K Mod N).  x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)"
-    unfolding  FactGroup_def using times_eq_iff subgroup.rcosets_not_empty
+    unfolding  FactGroup_def using times_eq_iff subgroup.rcosets_non_empty
     by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
   moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) = 
                                      carrier (G \<times>\<times> K Mod H \<times> N)"
     unfolding image_def  apply auto using R apply force
-    unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def apply auto apply force.
+    unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
   ultimately show ?thesis
     unfolding iso_def hom_def bij_betw_def inj_on_def by simp
 qed
diff -r 0854edc4d415 -r 6b5f15387353 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Jun 26 20:48:49 2018 +0100
@@ -31,9 +31,7 @@
   foldD :: "['a set, 'b \<Rightarrow> 'a \<Rightarrow> 'a, 'a, 'b set] \<Rightarrow> 'a"
   where "foldD D f e A = (THE x. (A, x) \<in> foldSetD D f e)"
 
-lemma foldSetD_closed:
-  "\<lbrakk>(A, z) \<in> foldSetD D f e; e \<in> D; \<And>x y. \<lbrakk>x \<in> A; y \<in> D\<rbrakk> \<Longrightarrow> f x y \<in> D\<rbrakk>
-    \<Longrightarrow> z \<in> D"
+lemma foldSetD_closed: "(A, z) \<in> foldSetD D f e \<Longrightarrow> z \<in> D"
   by (erule foldSetD.cases) auto
 
 lemma Diff1_foldSetD:
@@ -58,8 +56,12 @@
   then show ?case ..
 qed
 
+lemma foldSetD_backwards:
+  assumes "A \<noteq> {}" "(A, z) \<in> foldSetD D f e"
+  shows "\<exists>x y. x \<in> A \<and> (A - { x }, y) \<in> foldSetD D f e \<and> z = f x y"
+  using assms(2) by (cases) (simp add: assms(1), metis Diff_insert_absorb insertI1)
 
-text \<open>Left-Commutative Operations\<close>
+subsubsection \<open>Left-Commutative Operations\<close>
 
 locale LCD =
   fixes B :: "'b set"
@@ -392,9 +394,9 @@
    \<Longrightarrow> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
   by (metis Pi_split_domain finprod_Un_Int finprod_closed finprod_empty r_one)
 
-lemma finprod_multf:
+lemma finprod_multf [simp]:
   "\<lbrakk>f \<in> A \<rightarrow> carrier G; g \<in> A \<rightarrow> carrier G\<rbrakk> \<Longrightarrow>
-   finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
+   finprod G (\<lambda>x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
 proof (induct A rule: infinite_finite_induct)
   case empty show ?case by simp
 next
@@ -472,7 +474,20 @@
 
 lemma finprod_0 [simp]:
   "f \<in> {0::nat} \<rightarrow> carrier G \<Longrightarrow> finprod G f {..0} = f 0"
-by (simp add: Pi_def)
+  by (simp add: Pi_def)
+
+lemma finprod_0':
+  "f \<in> {..n} \<rightarrow> carrier G \<Longrightarrow> (f 0) \<otimes> finprod G f {Suc 0..n} = finprod G f {..n}"
+proof -
+  assume A: "f \<in> {.. n} \<rightarrow> carrier G"
+  hence "(f 0) \<otimes> finprod G f {Suc 0..n} = finprod G f {..0} \<otimes> finprod G f {Suc 0..n}"
+    using finprod_0[of f] by (simp add: funcset_mem)
+  also have " ... = finprod G f ({..0} \<union> {Suc 0..n})"
+    using finprod_Un_disjoint[of "{..0}" "{Suc 0..n}" f] A by (simp add: funcset_mem)
+  also have " ... = finprod G f {..n}"
+    by (simp add: atLeastAtMost_insertL atMost_atLeast0)
+  finally show ?thesis .
+qed
 
 lemma finprod_Suc [simp]:
   "f \<in> {..Suc n} \<rightarrow> carrier G \<Longrightarrow>
@@ -488,11 +503,19 @@
   case Suc thus ?case by (simp add: m_assoc Pi_def)
 qed
 
-lemma finprod_mult [simp]:
-  "\<lbrakk>f \<in> {..n} \<rightarrow> carrier G; g \<in> {..n} \<rightarrow> carrier G\<rbrakk> \<Longrightarrow>
-     finprod G (%i. f i \<otimes> g i) {..n::nat} =
-     finprod G f {..n} \<otimes> finprod G g {..n}"
-  by (induct n) (simp_all add: m_ac Pi_def)
+lemma finprod_Suc3:
+  assumes "f \<in> {..n :: nat} \<rightarrow> carrier G"
+  shows "finprod G f {.. n} = (f n) \<otimes> finprod G f {..< n}"
+proof (cases "n = 0")
+  case True thus ?thesis
+   using assms atMost_Suc by simp
+next
+  case False
+  then obtain k where "n = Suc k"
+    using not0_implies_Suc by blast
+  thus ?thesis
+    using finprod_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp
+qed
 
 (* The following two were contributed by Jeremy Avigad. *)
 
@@ -546,7 +569,6 @@
   also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
     by (auto simp add: finprod_const)
   finally show ?thesis
-(* uses the preceeding lemma *)
     by auto
 qed
 
@@ -573,8 +595,6 @@
 lemma (in comm_monoid) finprod_Union_disjoint:
   "\<lbrakk>finite C; \<And>A. A \<in> C \<Longrightarrow> finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G); pairwise disjnt C\<rbrakk> \<Longrightarrow>
     finprod G f (\<Union>C) = finprod G (finprod G f) C"
-  apply (frule finprod_UN_disjoint [of C id f])
-  apply auto
-  done
+  by (frule finprod_UN_disjoint [of C id f]) auto
 
 end
diff -r 0854edc4d415 -r 6b5f15387353 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jun 26 20:48:49 2018 +0100
@@ -535,6 +535,32 @@
   show "\<one> \<in> H " using monoid.one_closed[OF assms(2)] assms by simp
 qed
 
+lemma (in monoid) inv_unique':
+  assumes "x \<in> carrier G" "y \<in> carrier G"
+  shows "\<lbrakk> x \<otimes> y = \<one>; y \<otimes> x = \<one> \<rbrakk> \<Longrightarrow> y = inv x"
+proof -
+  assume "x \<otimes> y = \<one>" and l_inv: "y \<otimes> x = \<one>"
+  hence unit: "x \<in> Units G"
+    using assms unfolding Units_def by auto
+  show "y = inv x"
+    using inv_unique[OF l_inv Units_r_inv[OF unit] assms Units_inv_closed[OF unit]] .
+qed
+
+lemma (in monoid) m_inv_monoid_consistent: (* contributed by Paulo *)
+  assumes "x \<in> Units (G \<lparr> carrier := H \<rparr>)" and "submonoid H G"
+  shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
+proof -
+  have monoid: "monoid (G \<lparr> carrier := H \<rparr>)"
+    using submonoid.submonoid_is_monoid[OF assms(2) monoid_axioms] .
+  obtain y where y: "y \<in> H" "x \<otimes> y = \<one>" "y \<otimes> x = \<one>"
+    using assms(1) unfolding Units_def by auto
+  have x: "x \<in> H" and in_carrier: "x \<in> carrier G" "y \<in> carrier G"
+    using y(1) submonoid.subset[OF assms(2)] assms(1) unfolding Units_def by auto
+  show ?thesis
+    using monoid.inv_unique'[OF monoid, of x y] x y
+    using inv_unique'[OF in_carrier y(2-3)] by auto
+qed
+
 subsection \<open>Subgroups\<close>
 
 locale subgroup =
@@ -620,16 +646,13 @@
   show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
 qed
 
-
 lemma (in group) subgroupE:
   assumes "subgroup H G"
   shows "H \<subseteq> carrier G"
     and "H \<noteq> {}"
     and "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
-    and "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
-  using assms subgroup.subset apply blast
-  using assms subgroup_def apply auto[1]
-  by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)+
+    and "\<And>a b. \<lbrakk> a \<in> H; b \<in> H \<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
+  using assms unfolding subgroup_def[of H G] by auto
 
 declare monoid.one_closed [iff] group.inv_closed [simp]
   monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
@@ -638,14 +661,8 @@
   "\<not> subgroup {} G"
   by (blast dest: subgroup.one_closed)
 
-lemma (in subgroup) finite_imp_card_positive:
-  "finite (carrier G) ==> 0 < card H"
-proof (rule classical)
-  assume "finite (carrier G)" and a: "\<not> 0 < card H"
-  then have "finite H" by (blast intro: finite_subset [OF subset])
-  with is_subgroup a have "subgroup {} G" by simp
-  with subgroup_nonempty show ?thesis by contradiction
-qed
+lemma (in subgroup) finite_imp_card_positive: "finite (carrier G) \<Longrightarrow> 0 < card H"
+  using subset one_closed card_gt_0_iff finite_subset by blast
 
 (*Following 3 lemmas contributed by Martin Baillon*)
 
@@ -1219,21 +1236,24 @@
   finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
 qed
 
+lemma (in comm_group) hom_imp_img_comm_group:
+  assumes "h \<in> hom G H"
+  shows "comm_group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
+  unfolding comm_group_def
+  using hom_imp_img_group[OF assms] hom_imp_img_comm_monoid[OF assms] by simp
+
 lemma (in comm_group) iso_imp_img_comm_group:
   assumes "h \<in> iso G H"
   shows "comm_group (H \<lparr> one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
 proof -
   let ?h_img = "H \<lparr> carrier := h ` (carrier G), one := h \<one> \<rparr>"
-  have "comm_monoid ?h_img"
-    using hom_imp_img_comm_monoid[of h H] assms unfolding iso_def by simp
+  have "comm_group ?h_img"
+    using hom_imp_img_comm_group[of h H] assms unfolding iso_def by auto
   moreover have "carrier H = carrier ?h_img"
     using assms unfolding iso_def bij_betw_def by simp
   hence "H \<lparr> one := h \<one> \<rparr> = ?h_img"
     by simp
-  ultimately have "comm_monoid (H \<lparr> one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
-    by simp
-  thus ?thesis
-    unfolding comm_group_def using iso_imp_img_group[OF assms] by simp
+  ultimately show ?thesis by simp
 qed
 
 lemma (in comm_group) iso_imp_comm_group:
diff -r 0854edc4d415 -r 6b5f15387353 src/HOL/Algebra/Group_Action.thy
--- a/src/HOL/Algebra/Group_Action.thy	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/HOL/Algebra/Group_Action.thy	Tue Jun 26 20:48:49 2018 +0100
@@ -319,7 +319,7 @@
 corollary (in group_action) stab_rcosets_not_empty:
   assumes "x \<in> E" "R \<in> rcosets (stabilizer G \<phi> x)"
   shows "R \<noteq> {}"
-  using subgroup.rcosets_not_empty[OF stabilizer_subgroup[OF assms(1)] assms(2)] by simp
+  using subgroup.rcosets_non_empty[OF stabilizer_subgroup[OF assms(1)] assms(2)] by simp
 
 corollary (in group_action) diff_stabilizes:
   assumes "x \<in> E" "R \<in> rcosets (stabilizer G \<phi> x)"
diff -r 0854edc4d415 -r 6b5f15387353 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/HOL/Algebra/Ring.thy	Tue Jun 26 20:48:49 2018 +0100
@@ -103,7 +103,7 @@
 
 lemma (in abelian_monoid) a_monoid:
   "monoid (add_monoid G)"
-by (rule comm_monoid.axioms, rule a_comm_monoid) 
+by (rule comm_monoid.axioms, rule a_comm_monoid)
 
 lemma (in abelian_group) a_group:
   "group (add_monoid G)"
@@ -125,7 +125,7 @@
 context abelian_monoid
 begin
 
-lemmas a_closed = add.m_closed 
+lemmas a_closed = add.m_closed
 lemmas zero_closed = add.one_closed
 lemmas a_assoc = add.m_assoc
 lemmas l_zero = add.l_one
@@ -160,7 +160,6 @@
 lemmas finsum_0 = add.finprod_0
 lemmas finsum_Suc = add.finprod_Suc
 lemmas finsum_Suc2 = add.finprod_Suc2
-lemmas finsum_add = add.finprod_mult
 lemmas finsum_infinite = add.finprod_infinite
 
 lemmas finsum_cong = add.finprod_cong
@@ -228,7 +227,7 @@
   by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def add_pow_def)
 
 lemmas (in abelian_group) minus_add = add.inv_mult
- 
+
 text \<open>Derive an \<open>abelian_group\<close> from a \<open>comm_group\<close>\<close>
 
 lemma comm_group_abelian_groupI:
@@ -316,7 +315,7 @@
     note [simp] = comm_monoid.axioms [OF comm_monoid]
       abelian_group.axioms [OF abelian_group]
       abelian_monoid.a_closed
-        
+
     from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
       by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
     also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
@@ -351,7 +350,7 @@
   "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> (x \<oplus> y) = y"
 proof -
   assume G: "x \<in> carrier G" "y \<in> carrier G"
-  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 
+  then have "(\<ominus> x \<oplus> x) \<oplus> y = y"
     by (simp only: l_neg l_zero)
   with G show ?thesis by (simp add: a_ac)
 qed
@@ -439,7 +438,7 @@
   [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
   a_closed zero_closed  m_closed one_closed
   a_assoc l_zero  a_comm m_assoc l_one l_distr r_zero
-  a_lcomm r_distr l_null r_null 
+  a_lcomm r_distr l_null r_null
 
 lemmas (in ring) ring_simprules
   [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
@@ -549,7 +548,7 @@
   by (simp add: add_pow_def int_pow_def nat_pow_def)
 
 lemma add_pow_int_lt: "(k :: int) < 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = \<ominus>\<^bsub>R\<^esub> ([ nat (- k) ] \<cdot>\<^bsub>R\<^esub> a)"
-  by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def) 
+  by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def)
 
 corollary (in semiring) add_pow_ldistr:
   assumes "a \<in> carrier R" "b \<in> carrier R"
@@ -575,7 +574,7 @@
   also have " ... = [k] \<cdot> (a \<otimes> b)"
     using add.finprod_const[of "a \<otimes> b" "{..<k}"] assms by simp
   finally show ?thesis .
-qed 
+qed
 
 (* For integers, we need the uniqueness of the additive inverse *)
 lemma (in ring) add_pow_ldistr_int:
@@ -587,7 +586,7 @@
 next
   case False thus ?thesis
     using add_pow_int_lt[of k R a] add_pow_int_lt[of k R "a \<otimes> b"]
-          add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto 
+          add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto
 qed
 
 lemma (in ring) add_pow_rdistr_int:
@@ -599,7 +598,7 @@
 next
   case False thus ?thesis
     using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a \<otimes> b"]
-          add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto 
+          add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto
 qed
 
 
@@ -628,7 +627,7 @@
   assume eq: "a \<otimes> b = a \<otimes> c"
   with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
   with R have "a = \<zero> \<or> (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
-  with prem and R have "b \<ominus> c = \<zero>" by auto 
+  with prem and R have "b \<ominus> c = \<zero>" by auto
   with R have "b = b \<ominus> (b \<ominus> c)" by algebra
   also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
   finally show "b = c" .
diff -r 0854edc4d415 -r 6b5f15387353 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jun 26 20:48:49 2018 +0100
@@ -777,6 +777,23 @@
 definition Arg2pi :: "complex \<Rightarrow> real"
   where "Arg2pi z \<equiv> if z = 0 then 0 else THE t. 0 \<le> t \<and> t < 2*pi \<and> is_Arg z t"
 
+lemma is_Arg_2pi_iff: "is_Arg z (r + of_int k * (2 * pi)) \<longleftrightarrow> is_Arg z r"
+  by (simp add: algebra_simps is_Arg_def)
+
+lemma is_Arg_eqI:
+  assumes r: "is_Arg z r" and s: "is_Arg z s" and rs: "abs (r-s) < 2*pi" and "z \<noteq> 0"
+  shows "r = s"
+proof -
+  have zr: "z = (cmod z) * exp (\<i> * r)" and zs: "z = (cmod z) * exp (\<i> * s)"
+    using r s by (auto simp: is_Arg_def)
+  with \<open>z \<noteq> 0\<close> have eq: "exp (\<i> * r) = exp (\<i> * s)"
+    by (metis mult_eq_0_iff vector_space_over_itself.scale_left_imp_eq)
+  have  "\<i> * r = \<i> * s"
+    by (rule exp_complex_eqI) (use rs in \<open>auto simp: eq exp_complex_eqI\<close>)
+  then show ?thesis
+    by simp
+qed
+
 text\<open>This function returns the angle of a complex number from its representation in polar coordinates.
 Due to periodicity, its range is arbitrary. @{term Arg2pi} follows HOL Light in adopting the interval $[0,2\pi)$.
 But we have the same periodicity issue with logarithms, and it is usual to adopt the same interval
@@ -924,9 +941,6 @@
   using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order
   unfolding nonneg_Reals_def by fastforce
 
-lemma Arg2pi_of_real: "Arg2pi(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
-  by (simp add: Arg2pi_eq_0)
-
 lemma Arg2pi_eq_pi: "Arg2pi z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
     using Arg2pi_le_pi [of z] Arg2pi_lt_pi [of z] Arg2pi_eq_0 [of z] Arg2pi_ge_0 [of z] 
     by (fastforce simp: complex_is_Real_iff)
@@ -934,6 +948,9 @@
 lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \<or> Arg2pi z = pi \<longleftrightarrow> z \<in> \<real>"
   using Arg2pi_eq_0 Arg2pi_eq_pi not_le by auto
 
+lemma Arg2pi_of_real: "Arg2pi (of_real r) = (if r<0 then pi else 0)"
+  using Arg2pi_eq_0_pi Arg2pi_eq_pi by fastforce
+
 lemma Arg2pi_real: "z \<in> \<real> \<Longrightarrow> Arg2pi z = (if 0 \<le> Re z then 0 else pi)"
   using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto
 
@@ -1654,8 +1671,8 @@
 corollary Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
   using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
 
-lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
-  by (simp add: Arg_eq_0)
+lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
+  by (simp add: Im_Ln_eq_pi Arg_def)
 
 lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
 proof (cases "z=0")
@@ -1712,6 +1729,22 @@
 lemma Ln_Arg: "z\<noteq>0 \<Longrightarrow> Ln(z) = ln(norm z) + \<i> * Arg(z)"
   by (metis Arg_def Re_Ln complex_eq)
 
+lemma continuous_at_Arg:
+  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
+    shows "continuous (at z) Arg"
+proof -
+  have [simp]: "(\<lambda>z. Im (Ln z)) \<midarrow>z\<rightarrow> Arg z"
+    using Arg_def assms continuous_at by fastforce
+  show ?thesis
+    unfolding continuous_at
+  proof (rule Lim_transform_within_open)
+    show "\<And>w. \<lbrakk>w \<in> - \<real>\<^sub>\<le>\<^sub>0; w \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln w) = Arg w"
+      by (metis Arg_def Compl_iff nonpos_Reals_zero_I)
+  qed (use assms in auto)
+qed
+
+lemma continuous_within_Arg: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Arg"
+  using continuous_at_Arg continuous_at_imp_continuous_within by blast
 
 
 subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
@@ -4061,10 +4094,8 @@
      moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg2pi z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
      proof (cases "x=1")
        case True
-       then show ?thesis
-         apply (rule_tac x=1 in bexI)
-         apply (metis loop Arg2pi_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
-         done
+       with Arg2pi_of_real [of 1] loop show ?thesis
+         by (rule_tac x=1 in bexI) (auto simp: pathfinish_def pathstart_def \<open>0 \<le> x\<close>)
      next
        case False
        then have *: "(Arg2pi (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
diff -r 0854edc4d415 -r 6b5f15387353 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jun 26 20:48:49 2018 +0100
@@ -1418,14 +1418,16 @@
   assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))"
   shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"
 proof -
-  have "summable f" 
+  have "summable f"
     using ac unfolding abs_convergent_prod_conv_summable
   proof (elim summable_comparison_test')
     fix n
-    show "norm (f n) \<le> norm (exp (f n) - 1)" 
-      using ge0[of n] 
-      by (metis abs_of_nonneg add.commute diff_add_cancel diff_ge_0_iff_ge exp_ge_add_one_self 
-          exp_le_cancel_iff one_le_exp_iff real_norm_def)
+    have "\<bar>f n\<bar> = f n"
+      by (simp add: ge0)
+    also have "\<dots> \<le> exp (f n) - 1"
+      by (metis diff_diff_add exp_ge_add_one_self ge_iff_diff_ge_0)
+    finally show "norm (f n) \<le> norm (exp (f n) - 1)"
+      by simp
   qed
   then show ?thesis
     by (simp add: prodinf_exp)