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