--- a/src/HOL/Algebra/Coset.thy Tue Jun 26 23:15:48 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy Tue Jun 26 23:39:28 2018 +0200
@@ -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 23:15:48 2018 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Tue Jun 26 23:39:28 2018 +0200
@@ -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 23:15:48 2018 +0200
+++ b/src/HOL/Algebra/Group.thy Tue Jun 26 23:39:28 2018 +0200
@@ -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 23:15:48 2018 +0200
+++ b/src/HOL/Algebra/Group_Action.thy Tue Jun 26 23:39:28 2018 +0200
@@ -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 23:15:48 2018 +0200
+++ b/src/HOL/Algebra/Ring.thy Tue Jun 26 23:39:28 2018 +0200
@@ -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 23:15:48 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Jun 26 23:39:28 2018 +0200
@@ -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 23:15:48 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Tue Jun 26 23:39:28 2018 +0200
@@ -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)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Trie.thy Tue Jun 26 23:39:28 2018 +0200
@@ -0,0 +1,278 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Trie and Patricia Trie Implementations of \mbox{\<open>bool list set\<close>}\<close>
+
+theory Trie
+imports Set_Specs
+begin
+
+hide_const (open) insert
+
+declare Let_def[simp]
+
+
+subsection "Trie"
+
+datatype trie = Leaf | Node bool "trie * trie"
+
+text \<open>The pairing allows things like \<open>Node b (if \<dots> then (l,r) else (r,l))\<close>.\<close>
+
+fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
+"isin Leaf ks = False" |
+"isin (Node b (l,r)) ks =
+ (case ks of
+ [] \<Rightarrow> b |
+ k#ks \<Rightarrow> isin (if k then r else l) ks)"
+
+fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"insert [] Leaf = Node True (Leaf,Leaf)" |
+"insert [] (Node b lr) = Node True lr" |
+"insert (k#ks) Leaf =
+ Node False (if k then (Leaf, insert ks Leaf)
+ else (insert ks Leaf, Leaf))" |
+"insert (k#ks) (Node b (l,r)) =
+ Node b (if k then (l, insert ks r)
+ else (insert ks l, r))"
+
+fun shrink_Node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
+"shrink_Node b lr = (if \<not> b \<and> lr = (Leaf,Leaf) then Leaf else Node b lr)"
+
+fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"delete ks Leaf = Leaf" |
+"delete ks (Node b (l,r)) =
+ (case ks of
+ [] \<Rightarrow> shrink_Node False (l,r) |
+ k#ks' \<Rightarrow> shrink_Node b (if k then (l, delete ks' r) else (delete ks' l, r)))"
+
+fun invar :: "trie \<Rightarrow> bool" where
+"invar Leaf = True" |
+"invar (Node b (l,r)) = ((\<not> b \<longrightarrow> l \<noteq> Leaf \<or> r \<noteq> Leaf) \<and> invar l \<and> invar r)"
+
+
+subsubsection \<open>Functional Correctness\<close>
+
+lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
+apply(induction as t arbitrary: bs rule: insert.induct)
+apply(auto split: list.splits)
+done
+
+lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
+apply(induction as t arbitrary: bs rule: delete.induct)
+ apply simp
+apply (auto split: list.splits; fastforce)
+done
+
+lemma insert_not_Leaf: "insert ks t \<noteq> Leaf"
+by(cases "(ks,t)" rule: insert.cases) auto
+
+lemma invar_insert: "invar t \<Longrightarrow> invar (insert ks t)"
+by(induction ks t rule: insert.induct)(auto simp: insert_not_Leaf)
+
+lemma invar_delete: "invar t \<Longrightarrow> invar (delete ks t)"
+by(induction ks t rule: delete.induct)(auto split: list.split)
+
+interpretation T: Set
+where empty = Leaf and insert = insert and delete = delete and isin = isin
+and set = "\<lambda>t. {x. isin t x}" and invar = invar
+proof (standard, goal_cases)
+ case 1 thus ?case by simp
+next
+ case 2 thus ?case by simp
+next
+ case 3 thus ?case by (auto simp add: isin_insert)
+next
+ case 4 thus ?case by (auto simp add: isin_delete)
+next
+ case 5 thus ?case by simp
+next
+ case 6 thus ?case by (auto simp add: invar_insert)
+next
+ case 7 thus ?case by (auto simp add: invar_delete)
+qed
+
+
+subsection "Patricia Trie"
+
+datatype trieP = LeafP | NodeP "bool list" bool "trieP * trieP"
+
+fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
+"isinP LeafP ks = False" |
+"isinP (NodeP ps b (l,r)) ks =
+ (let n = length ps in
+ if ps = take n ks
+ then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (if k then r else l) ks'
+ else False)"
+
+text \<open>\<open>split xs ys = (zs, xs', ys')\<close> iff
+ \<open>zs\<close> is the longest common prefix of \<open>xs\<close> and \<open>ys\<close> and
+ \<open>xs = zs @ xs'\<close> and \<open>ys = zs @ ys'\<close>\<close>
+fun split where
+"split [] ys = ([],[],ys)" |
+"split xs [] = ([],xs,[])" |
+"split (x#xs) (y#ys) =
+ (if x\<noteq>y then ([],x#xs,y#ys)
+ else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
+
+fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
+"insertP ks LeafP = NodeP ks True (LeafP,LeafP)" |
+"insertP ks (NodeP ps b (l,r)) =
+ (case split ks ps of
+ (qs,k#ks',p#ps') \<Rightarrow>
+ let tp = NodeP ps' b (l,r); tk = NodeP ks' True (LeafP,LeafP)
+ in NodeP qs False (if k then (tp,tk) else (tk,tp)) |
+ (qs,k#ks',[]) \<Rightarrow>
+ NodeP ps b (if k then (l,insertP ks' r) else (insertP ks' l, r)) |
+ (qs,[],p#ps') \<Rightarrow>
+ let t = NodeP ps' b (l,r)
+ in NodeP qs True (if p then (LeafP, t) else (t, LeafP)) |
+ (qs,[],[]) \<Rightarrow> NodeP ps True (l,r))"
+
+fun shrink_NodeP where
+"shrink_NodeP ps b lr = (if b then NodeP ps b lr else
+ case lr of
+ (LeafP, LeafP) \<Rightarrow> LeafP |
+ (LeafP, NodeP ps' b' lr') \<Rightarrow> NodeP (ps @ True # ps') b' lr' |
+ (NodeP ps' b' lr', LeafP) \<Rightarrow> NodeP (ps @ False # ps') b' lr' |
+ _ \<Rightarrow> NodeP ps b lr)"
+
+fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
+"deleteP ks LeafP = LeafP" |
+"deleteP ks (NodeP ps b (l,r)) =
+ (case split ks ps of
+ (qs,_,p#ps') \<Rightarrow> NodeP ps b (l,r) |
+ (qs,k#ks',[]) \<Rightarrow>
+ shrink_NodeP ps b (if k then (l, deleteP ks' r) else (deleteP ks' l, r)) |
+ (qs,[],[]) \<Rightarrow> shrink_NodeP ps False (l,r))"
+
+fun invarP :: "trieP \<Rightarrow> bool" where
+"invarP LeafP = True" |
+"invarP (NodeP ps b (l,r)) = ((\<not>b \<longrightarrow> l \<noteq> LeafP \<or> r \<noteq> LeafP) \<and> invarP l \<and> invarP r)"
+
+text \<open>The abstraction function(s):\<close>
+
+fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"prefix_trie [] t = t" |
+"prefix_trie (k#ks) t =
+ (let t' = prefix_trie ks t in shrink_Node False (if k then (Leaf,t') else (t',Leaf)))"
+
+fun abs_trieP :: "trieP \<Rightarrow> trie" where
+"abs_trieP LeafP = Leaf" |
+"abs_trieP (NodeP ps b (l,r)) = prefix_trie ps (Node b (abs_trieP l, abs_trieP r))"
+
+
+subsubsection \<open>Functional Correctness\<close>
+
+text \<open>IsinP:\<close>
+
+lemma isin_prefix_trie: "isin (prefix_trie ps t) ks =
+ (length ks \<ge> length ps \<and>
+ (let n = length ps in ps = take n ks \<and> isin t (drop n ks)))"
+by(induction ps arbitrary: ks)(auto split: list.split)
+
+lemma isinP: "isinP t ks = isin (abs_trieP t) ks"
+apply(induction t arbitrary: ks rule: abs_trieP.induct)
+ apply(auto simp: isin_prefix_trie split: list.split)
+ using nat_le_linear apply force
+using nat_le_linear apply force
+done
+
+text \<open>Insert:\<close>
+
+lemma prefix_trie_Leaf_iff: "prefix_trie ps t = Leaf \<longleftrightarrow> t = Leaf"
+by (induction ps) auto
+
+lemma prefix_trie_Leafs: "prefix_trie ks (Node True (Leaf,Leaf)) = insert ks Leaf"
+by(induction ks) (auto simp: prefix_trie_Leaf_iff)
+
+lemma prefix_trie_Leaf: "prefix_trie ps Leaf = Leaf"
+by(induction ps) auto
+
+lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
+by(induction ks) (auto simp: prefix_trie_Leaf_iff insert_not_Leaf prefix_trie_Leaf)
+
+lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
+by(induction ps) auto
+
+lemma split_iff: "split xs ys = (zs, xs', ys') \<longleftrightarrow>
+ xs = zs @ xs' \<and> ys = zs @ ys' \<and> (xs' \<noteq> [] \<and> ys' \<noteq> [] \<longrightarrow> hd xs' \<noteq> hd ys')"
+proof(induction xs ys arbitrary: zs xs' ys' rule: split.induct)
+ case 1 thus ?case by auto
+next
+ case 2 thus ?case by auto
+next
+ case 3 thus ?case by(clarsimp simp: Cons_eq_append_conv split: prod.splits if_splits) auto
+qed
+
+lemma abs_trieP_insertP:
+ "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
+apply(induction t arbitrary: ks)
+apply(auto simp: prefix_trie_Leafs insert_append prefix_trie_append
+ prefix_trie_Leaf_iff split_iff split: list.split prod.split)
+done
+
+corollary isinP_insertP: "isinP (insertP ks t) ks' = (ks=ks' \<or> isinP t ks')"
+by (simp add: isin_insert isinP abs_trieP_insertP)
+
+lemma insertP_not_LeafP: "insertP ks t \<noteq> LeafP"
+apply(induction ks t rule: insertP.induct)
+apply(auto split: prod.split list.split)
+done
+
+lemma invarP_insertP: "invarP t \<Longrightarrow> invarP (insertP ks t)"
+apply(induction ks t rule: insertP.induct)
+apply(auto simp: insertP_not_LeafP split: prod.split list.split)
+done
+
+text \<open>Delete:\<close>
+
+lemma invar_shrink_NodeP: "\<lbrakk> invarP l; invarP r \<rbrakk> \<Longrightarrow> invarP (shrink_NodeP ps b (l,r))"
+by(auto split: trieP.split)
+
+lemma invarP_deleteP: "invarP t \<Longrightarrow> invarP (deleteP ks t)"
+apply(induction t arbitrary: ks)
+apply(auto simp: invar_shrink_NodeP split_iff simp del: shrink_NodeP.simps
+ split!: list.splits prod.split if_splits)
+done
+
+lemma delete_append:
+ "delete (ks @ ks') (prefix_trie ks t) = prefix_trie ks (delete ks' t)"
+by(induction ks) auto
+
+lemma abs_trieP_shrink_NodeP:
+ "abs_trieP (shrink_NodeP ps b (l,r)) = prefix_trie ps (shrink_Node b (abs_trieP l, abs_trieP r))"
+apply(induction ps arbitrary: b l r)
+apply (auto simp: prefix_trie_Leaf prefix_trie_Leaf_iff prefix_trie_append
+ split!: trieP.splits if_splits)
+done
+
+lemma abs_trieP_deleteP:
+ "abs_trieP (deleteP ks t) = delete ks (abs_trieP t)"
+apply(induction t arbitrary: ks)
+apply(auto simp: prefix_trie_Leafs delete_append prefix_trie_Leaf
+ abs_trieP_shrink_NodeP prefix_trie_append split_iff
+ simp del: shrink_NodeP.simps split!: list.split prod.split if_splits)
+done
+
+corollary isinP_deleteP: "isinP (deleteP ks t) ks' = (ks\<noteq>ks' \<and> isinP t ks')"
+by (simp add: isin_delete isinP abs_trieP_deleteP)
+
+interpretation PT: Set
+where empty = LeafP and insert = insertP and delete = deleteP
+and isin = isinP and set = "\<lambda>t. {x. isinP t x}" and invar = invarP
+proof (standard, goal_cases)
+ case 1 thus ?case by (simp)
+next
+ case 2 thus ?case by (simp)
+next
+ case 3 thus ?case by (auto simp add: isinP_insertP)
+next
+ case 4 thus ?case by (auto simp add: isinP_deleteP)
+next
+ case 5 thus ?case by (simp)
+next
+ case 6 thus ?case by (simp add: invarP_insertP)
+next
+ case 7 thus ?case by (auto simp add: invarP_deleteP)
+qed
+
+end
--- a/src/HOL/ROOT Tue Jun 26 23:15:48 2018 +0200
+++ b/src/HOL/ROOT Tue Jun 26 23:39:28 2018 +0200
@@ -201,6 +201,7 @@
Brother12_Map
AA_Map
Set2_Join_RBT
+ Trie
Leftist_Heap
Binomial_Heap
document_files "root.tex" "root.bib"