# HG changeset patch # User paulson # Date 1529406871 -3600 # Node ID ae42b0f6885d9988c1513958fcac78416629d1d1 # Parent 3ead36cbe6b7540faecae738d2d58c409105825d# Parent 44ffc5b9cd764c5ad40c7b4dde734bbc748d6e87 merged diff -r 3ead36cbe6b7 -r ae42b0f6885d CONTRIBUTORS --- a/CONTRIBUTORS Mon Jun 18 22:20:55 2018 +0100 +++ b/CONTRIBUTORS Tue Jun 19 12:14:31 2018 +0100 @@ -6,6 +6,9 @@ Contributions to Isabelle2018 ----------------------------- +* June 2018: Martin Baillon and Paulo Emílio de Vilhena + A variety of contributions to HOL-Algebra. + * May 2018: Manuel Eberl Landau symbols and asymptotic equivalence (moved from the AFP). diff -r 3ead36cbe6b7 -r ae42b0f6885d NEWS --- a/NEWS Mon Jun 18 22:20:55 2018 +0100 +++ b/NEWS Tue Jun 19 12:14:31 2018 +0100 @@ -375,6 +375,10 @@ * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new infix/prefix notation. +* Session HOL-Algebra: Revamped with much new material. +The set of isomorphisms between two groups is now denoted iso rather than iso_set. +INCOMPATIBILITY. + * Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping theorem, the Vitali covering theorem, change-of-variables results for integration and measures. diff -r 3ead36cbe6b7 -r ae42b0f6885d src/HOL/Algebra/Zassenhaus.thy --- a/src/HOL/Algebra/Zassenhaus.thy Mon Jun 18 22:20:55 2018 +0100 +++ b/src/HOL/Algebra/Zassenhaus.thy Tue Jun 19 12:14:31 2018 +0100 @@ -1,12 +1,18 @@ +(* Title: HOL/Algebra/Zassenhaus.thy + Author: Martin Baillon +*) + +section \The Zassenhaus Lemma\ + theory Zassenhaus imports Coset Group_Action begin - -subsubsection \Lemmas about normalizer\ +text \Proves the second isomorphism theorem and the Zassenhaus lemma.\ +subsection \Lemmas about normalizer\ -lemma (in group) subgroup_in_normalizer: +lemma (in group) subgroup_in_normalizer: assumes "subgroup H G" shows "normal H (G\carrier:= (normalizer G H)\)" proof(intro group.normal_invI) @@ -19,7 +25,7 @@ have "x <# H = H" by (metis \x \ H\ assms group.lcos_mult_one is_group l_repr_independence one_closed subgroup.subset) - moreover have "H #> inv x = H" + moreover have "H #> inv x = H" by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed) ultimately have "x <# H #> (inv x) = H" by simp thus " x \ stabilizer G (\g. \H\{H. H \ carrier G}. g <# H #> inv g) H" @@ -58,7 +64,7 @@ lemma (in group) normal_imp_subgroup_normalizer: assumes "subgroup H G" and "N \ (G\carrier := H\)" - shows "subgroup H (G\carrier := normalizer G N\)" + shows "subgroup H (G\carrier := normalizer G N\)" proof- have N_carrierG : "N \ carrier(G)" using assms normal_imp_subgroup subgroup.subset @@ -72,7 +78,7 @@ hence "x <# N #> inv x =(N #> x) #> inv x" by simp also have "... = N #> \" - using assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp + using assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp finally have "x <# N #> inv x = N" by (simp add: N_carrierG) thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) N = N}" using xcarrierG by (simp add : N_carrierG) @@ -103,10 +109,10 @@ using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD) have "N #> h1 = h1 <# N" using normalI B2 assms normal.coset_eq subgroup.subset by blast - hence "h1\n2 \ N #> h1" + hence "h1\n2 \ N #> h1" using B2 B3 assms l_coset_def by fastforce - from this obtain y2 where y2_def:"y2 \ N" and y2_prop:"y2\h1 = h1\n2" - using singletonD by (metis (no_types, lifting) UN_E r_coset_def) + from this obtain y2 where y2_def:"y2 \ N" and y2_prop:"y2\h1 = h1\n2" + using singletonD by (metis (no_types, lifting) UN_E r_coset_def) have " x\y = n1 \ y2 \ h1 \ h2" using y2_def B2 B3 by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier) moreover have B4 :"n1 \ y2 \N" @@ -129,10 +135,10 @@ hence "... \h \ N" using assms C2 by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier) - hence C4:"(inv h \ inv n \ h) \ inv h \ (N<#>H)" + hence C4:"(inv h \ inv n \ h) \ inv h \ (N<#>H)" using C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto have "inv h \ inv n \ h \ inv h = inv h \ inv n" - using subgroup.subset[OF assms(2)] + using subgroup.subset[OF assms(2)] by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE) thus "inv(x)\N<#>H" using C4 C2 C3 by simp qed @@ -149,7 +155,7 @@ thus "(N <#> H \ carrier G \ (\x y. x \ N <#> H \ y \ N <#> H \ x \ y \ N <#> H)) \ \ \ N <#> H \ (\x. x \ N <#> H \ inv x \ N <#> H)" using A B C D assms by blast qed - + lemma (in group) mult_norm_sub_in_sub: assumes "normal N (G\carrier:=K\)" @@ -201,7 +207,7 @@ proposition (in group) weak_snd_iso_thme: - assumes "subgroup H G" + assumes "subgroup H G" and "N\G" shows "(G\carrier := N<#>H\ Mod N \ G\carrier:=H\ Mod (N\H))" proof- @@ -325,8 +331,8 @@ carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ G\carrier := normalizer G N, carrier := H\ Mod N \ H = (G\carrier:= N<#>H\ Mod N) \ - G\carrier := normalizer G N, carrier := H\ Mod N \ H" - using subgroup_set_mult_equality[OF normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H] + G\carrier := normalizer G N, carrier := H\ Mod N \ H" + using subgroup_set_mult_equality[OF normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H] subgroup.subset[OF assms(3)] subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]] by simp @@ -343,7 +349,7 @@ moreover have "H\N = N\H" using assms by auto ultimately show "(G\carrier:= N<#>H\ Mod N) \ G\carrier := H\ Mod H \ N" by auto qed - + corollary (in group) snd_iso_thme_recip : assumes "subgroup H G" @@ -358,9 +364,9 @@ lemma (in group) distinc: - assumes "subgroup H G" - and "H1\G\carrier := H\" - and "subgroup K G" + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" and "K1\G\carrier:=K\" shows "subgroup (H\K) (G\carrier:=(normalizer G (H1<#>(H\K1))) \)" proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]]) @@ -401,7 +407,7 @@ by auto also have "... = {x} <#> (H1 <#> H \ K1) <#> {inv x}" using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2) - finally have "H1 <#> H \ K1 = x <# (H1 <#> H \ K1) #> inv x" + finally have "H1 <#> H \ K1 = x <# (H1 <#> H \ K1) #> inv x" using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult) thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) (H1 <#> H \ K1) = H1 <#> H \ K1}" @@ -411,9 +417,9 @@ qed lemma (in group) preliminary1: - assumes "subgroup H G" - and "H1\G\carrier := H\" - and "subgroup K G" + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" and "K1\G\carrier:=K\" shows " (H\K) \ (H1<#>(H\K1)) = (H1\K)<#>(H\K1)" proof @@ -452,15 +458,15 @@ qed lemma (in group) preliminary2: - assumes "subgroup H G" + assumes "subgroup H G" and "H1\G\carrier := H\" - and "subgroup K G" + and "subgroup K G" and "K1\G\carrier:=K\" shows "(H1<#>(H\K1)) \ G\carrier:=(H1<#>(H\K))\" proof- have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G" using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+. - have subH1:"subgroup (H1 <#> H \ K) (G\carrier := H\)" + have subH1:"subgroup (H1 <#> H \ K) (G\carrier := H\)" using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)] assms(1)]] assms by auto have "Group.group (G\carrier:=(H1<#>(H\K))\)" @@ -541,7 +547,7 @@ finally have "H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x =H1 <#> H \ K1 #> hk" using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp - thus " H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x = + thus " H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x = x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1)" using eq1 by simp qed ultimately show "H1 <#> H \ K1 \ G\carrier := H1 <#> H \ K\" @@ -550,9 +556,9 @@ proposition (in group) Zassenhaus_1: - assumes "subgroup H G" - and "H1\G\carrier := H\" - and "subgroup K G" + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" and "K1\G\carrier:=K\" shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>H\K1)) \ (G\carrier:= (H\K)\ Mod ((H1\K)<#>(H\K1)))" proof- @@ -572,7 +578,7 @@ also have "... = ((H\K)<#>H1) <#>(H\K1)" using set_mult_assoc[where ?M = "H\K"] K1_incl_G H1_incl_G assms by (simp add: inf.coboundedI2 subgroup.subset) - also have "... = (H1<#>(H\K))<#>(H\K1)" + also have "... = (H1<#>(H\K))<#>(H\K1)" using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto also have "... = H1 <#> ((H\K)<#>(H\K1))" using set_mult_assoc K1_incl_G H1_incl_G assms @@ -585,25 +591,25 @@ incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms normal_imp_subgroup by (metis inf_commute normal_inter) qed - hence " H1 <#> ((H\K)<#>(H\K1)) = H1 <#> ((H\K))" + hence " H1 <#> ((H\K)<#>(H\K1)) = H1 <#> ((H\K))" by simp thus "N <#> N1 = H1 <#> H \ K" by (simp add: calculation) qed - have "N\N1 = (H1\K)<#>(H\K1)" - using preliminary1 assms N_def N1_def by simp + have "N\N1 = (H1\K)<#>(H\K1)" + using preliminary1 assms N_def N1_def by simp thus "(G\carrier:= H1 <#> (H\K)\ Mod N1) \ (G\carrier:= N\ Mod ((H1\K)<#>(H\K1)))" using H_simp Hp by auto qed theorem (in group) Zassenhaus: - assumes "subgroup H G" - and "H1\G\carrier := H\" - and "subgroup K G" + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" and "K1\G\carrier:=K\" - shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) \ + shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) \ (G\carrier:= K1 <#> (H\K)\ Mod (K1<#>(K\H1)))" proof- define Gmod1 Gmod2 Gmod3 Gmod4 @@ -620,8 +626,8 @@ show "K1 \ H \ G\carrier := H \ K\" using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute) next - show "subgroup (K \ H1) (G\carrier := H \ K\)" - using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter) + show "subgroup (K \ H1) (G\carrier := H \ K\)" + using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter) qed hence "Gmod3 = Gmod4" using Hp Gmod4_def by simp hence "Gmod1 \ Gmod2" diff -r 3ead36cbe6b7 -r ae42b0f6885d src/HOL/Analysis/Analysis.thy --- a/src/HOL/Analysis/Analysis.thy Mon Jun 18 22:20:55 2018 +0100 +++ b/src/HOL/Analysis/Analysis.thy Tue Jun 19 12:14:31 2018 +0100 @@ -7,6 +7,7 @@ Radon_Nikodym Fashoda_Theorem Determinants + Cross3 Homeomorphism Bounded_Continuous_Function Function_Topology diff -r 3ead36cbe6b7 -r ae42b0f6885d src/HOL/Analysis/Cross3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Cross3.thy Tue Jun 19 12:14:31 2018 +0100 @@ -0,0 +1,227 @@ +(* Title: HOL/Analysis/Cross3.thy + Author: L C Paulson, University of Cambridge + +Ported from HOL Light +*) + +section\Vector Cross Products in 3 Dimensions.\ + +theory "Cross3" + imports Determinants +begin + +context includes no_Set_Product_syntax +begin \\locally disable syntax for set product, to avoid warnings\ + +definition cross3 :: "[real^3, real^3] \ real^3" (infixr "\" 80) + where "a \ b \ + vector [a$2 * b$3 - a$3 * b$2, + a$3 * b$1 - a$1 * b$3, + a$1 * b$2 - a$2 * b$1]" + +end + +bundle cross3_syntax begin +notation cross3 (infixr "\" 80) +no_notation Product_Type.Times (infixr "\" 80) +end + +bundle no_cross3_syntax begin +no_notation cross3 (infixr "\" 80) +notation Product_Type.Times (infixr "\" 80) +end + +unbundle cross3_syntax + +subsection\ Basic lemmas.\ + +lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps + +lemma dot_cross_self: "x \ (x \ y) = 0" "x \ (y \ x) = 0" "(x \ y) \ y = 0" "(y \ x) \ y = 0" + by (simp_all add: orthogonal_def cross3_simps) + +lemma orthogonal_cross: "orthogonal (x \ y) x" "orthogonal (x \ y) y" + "orthogonal y (x \ y)" "orthogonal (x \ y) x" + by (simp_all add: orthogonal_def dot_cross_self) + +lemma cross_zero_left [simp]: "0 \ x = 0" and cross_zero_right [simp]: "x \ 0 = 0" for x::"real^3" + by (simp_all add: cross3_simps) + +lemma cross_skew: "(x \ y) = -(y \ x)" for x::"real^3" + by (simp add: cross3_simps) + +lemma cross_refl [simp]: "x \ x = 0" for x::"real^3" + by (simp add: cross3_simps) + +lemma cross_add_left: "(x + y) \ z = (x \ z) + (y \ z)" for x::"real^3" + by (simp add: cross3_simps) + +lemma cross_add_right: "x \ (y + z) = (x \ y) + (x \ z)" for x::"real^3" + by (simp add: cross3_simps) + +lemma cross_mult_left: "(c *\<^sub>R x) \ y = c *\<^sub>R (x \ y)" for x::"real^3" + by (simp add: cross3_simps) + +lemma cross_mult_right: "x \ (c *\<^sub>R y) = c *\<^sub>R (x \ y)" for x::"real^3" + by (simp add: cross3_simps) + +lemma cross_minus_left [simp]: "(-x) \ y = - (x \ y)" for x::"real^3" + by (simp add: cross3_simps) + +lemma cross_minus_right [simp]: "x \ -y = - (x \ y)" for x::"real^3" + by (simp add: cross3_simps) + +lemma left_diff_distrib: "(x - y) \ z = x \ z - y \ z" for x::"real^3" + by (simp add: cross3_simps) + +lemma right_diff_distrib: "x \ (y - z) = x \ y - x \ z" for x::"real^3" + by (simp add: cross3_simps) + +hide_fact (open) left_diff_distrib right_diff_distrib + +lemma Jacobi: "x \ (y \ z) + y \ (z \ x) + z \ (x \ y) = 0" for x::"real^3" + by (simp add: cross3_simps) + +lemma Lagrange: "x \ (y \ z) = (x \ z) *\<^sub>R y - (x \ y) *\<^sub>R z" + by (simp add: cross3_simps) (metis (full_types) exhaust_3) + +lemma cross_triple: "(x \ y) \ z = (y \ z) \ x" + by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) + +lemma cross_components: + "(x \ y)$1 = x$2 * y$3 - y$2 * x$3" "(x \ y)$2 = x$3 * y$1 - y$3 * x$1" "(x \ y)$3 = x$1 * y$2 - y$1 * x$2" + by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) + +lemma cross_basis: "(axis 1 1) \ (axis 2 1) = axis 3 1" "(axis 2 1) \ (axis 1 1) = -(axis 3 1)" + "(axis 2 1) \ (axis 3 1) = axis 1 1" "(axis 3 1) \ (axis 2 1) = -(axis 1 1)" + "(axis 3 1) \ (axis 1 1) = axis 2 1" "(axis 1 1) \ (axis 3 1) = -(axis 2 1)" + using exhaust_3 + by (force simp add: axis_def cross3_simps)+ + +lemma cross_basis_nonzero: + "u \ 0 \ ~(u \ axis 1 1 = 0) \ ~(u \ axis 2 1 = 0) \ ~(u \ axis 3 1 = 0)" + by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3) + +lemma cross_dot_cancel: + fixes x::"real^3" + assumes deq: "x \ y = x \ z" and veq: "x \ y = x \ z" and x: "x \ 0" + shows "y = z" +proof - + have "x \ x \ 0" + by (simp add: x) + then have "y - z = 0" + using veq + by (metis (no_types, lifting) Cross3.right_diff_distrib Lagrange deq eq_iff_diff_eq_0 inner_diff_right scale_eq_0_iff) + then show ?thesis + using eq_iff_diff_eq_0 by blast +qed + +lemma norm_cross_dot: "(norm (x \ y))\<^sup>2 + (x \ y)\<^sup>2 = (norm x * norm y)\<^sup>2" + unfolding power2_norm_eq_inner power_mult_distrib + by (simp add: cross3_simps power2_eq_square) + +lemma dot_cross_det: "x \ (y \ z) = det(vector[x,y,z])" + by (simp add: cross3_simps) + +lemma cross_cross_det: "(w \ x) \ (y \ z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>R z" + using exhaust_3 by (force simp add: cross3_simps) + +lemma dot_cross: "(w \ x) \ (y \ z) = (w \ y) * (x \ z) - (w \ z) * (x \ y)" + by (force simp add: cross3_simps) + +lemma norm_cross: "(norm (x \ y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \ y)\<^sup>2" + unfolding power2_norm_eq_inner power_mult_distrib + by (simp add: cross3_simps power2_eq_square) + +lemma cross_eq_0: "x \ y = 0 \ collinear{0,x,y}" +proof - + have "x \ y = 0 \ norm (x \ y) = 0" + by simp + also have "... \ (norm x * norm y)\<^sup>2 = (x \ y)\<^sup>2" + using norm_cross [of x y] by (auto simp: power_mult_distrib) + also have "... \ \x \ y\ = norm x * norm y" + using power2_eq_iff + by (metis (mono_tags, hide_lams) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def) + also have "... \