# HG changeset patch # User paulson # Date 1529061486 -3600 # Node ID c027dfbfad302d700d9fb8d35b13c2bb2d24ff36 # Parent 6d0f1a5a16ea84b522872457f9294db7efa61e45 more on infinite products. Also subgroup_imp_subset -> subgroup.subset diff -r 6d0f1a5a16ea -r c027dfbfad30 src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Thu Jun 14 17:50:23 2018 +0200 +++ b/src/HOL/Algebra/Coset.thy Fri Jun 15 12:18:06 2018 +0100 @@ -303,7 +303,7 @@ shows "subgroup (H <#> K) G" proof (rule subgroup.intro) show "H <#> K \ carrier G" - by (simp add: setmult_subset_G assms subgroup_imp_subset) + by (simp add: setmult_subset_G assms subgroup.subset) next have "\ \ \ \ H <#> K" unfolding set_mult_def using assms subgroup.one_closed by blast @@ -821,7 +821,7 @@ apply (rule card_partition) apply (simp add: rcosets_subset_PowG [THEN finite_subset]) apply (simp add: rcosets_part_G) - apply (simp add: card_rcosets_equal subgroup_imp_subset) + apply (simp add: card_rcosets_equal subgroup.subset) apply (simp add: rcos_disjoint) done @@ -843,11 +843,11 @@ hence finite_rcos: "finite (rcosets H)" by simp hence "card (\(rcosets H)) = (\R\(rcosets H). card R)" using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)] - rcosets_finite[where ?H = H] by (simp add: assms subgroup_imp_subset) + rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset) hence "order G = (\R\(rcosets H). card R)" by (simp add: assms order_def rcosets_part_G) hence "order G = (\R\(rcosets H). card H)" - using card_rcosets_equal by (simp add: assms subgroup_imp_subset) + using card_rcosets_equal by (simp add: assms subgroup.subset) hence "order G = (card H) * (card (rcosets H))" by simp hence "order G \ 0" using finite_rcos finite_H assms ex_in_conv rcosets_part_G subgroup.one_closed by fastforce @@ -1094,13 +1094,13 @@ show "\x h. x \ carrier (G\\K) \ h \ H\N \ x \\<^bsub>G\\K\<^esub> h \\<^bsub>G\\K\<^esub> inv\<^bsub>G\\K\<^esub> x \ H\N" proof- fix x h assume xGK : "x \ carrier (G \\ K)" and hHN : " h \ H \ N" - hence hGK : "h \ carrier (G \\ K)" using subgroup_imp_subset[OF sub] by auto + hence hGK : "h \ carrier (G \\ K)" using subgroup.subset[OF sub] by auto from xGK obtain x1 x2 where x1x2 :"x1 \ carrier G" "x2 \ carrier K" "x = (x1,x2)" unfolding DirProd_def by fastforce from hHN obtain h1 h2 where h1h2 : "h1 \ H" "h2 \ N" "h = (h1,h2)" unfolding DirProd_def by fastforce hence h1h2GK : "h1 \ carrier G" "h2 \ carrier K" - using normal_imp_subgroup subgroup_imp_subset assms apply blast+. + using normal_imp_subgroup subgroup.subset assms apply blast+. have "inv\<^bsub>G \\ K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)" using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto hence "x \\<^bsub>G \\ K\<^esub> h \\<^bsub>G \\ K\<^esub> inv\<^bsub>G \\ K\<^esub> x = (x1 \ h1 \ inv x1,x2 \\<^bsub>K\<^esub> h2 \\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)" @@ -1160,7 +1160,7 @@ shows "(carrier G) <#> H = carrier G" proof show "(carrier G)<#>H \ carrier G" - unfolding set_mult_def using subgroup_imp_subset assms by blast + unfolding set_mult_def using subgroup.subset assms by blast next have " (carrier G) #> \ = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp moreover have "(carrier G) #> \ \ (carrier G) <#> H" unfolding set_mult_def r_coset_def @@ -1173,7 +1173,7 @@ assumes "subgroup H G" and "subgroup N (G\carrier:=H\)" shows "H<#>N = H" - using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms + using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms by (metis monoid.cases_scheme order_refl partial_object.simps(1) partial_object.update_convs(1) subgroup_set_mult_equality) @@ -1196,9 +1196,9 @@ and "subgroup K (G\carrier:=H\)" shows "K<#>N = N<#>K" proof- - have "N \ carrier (G\carrier := H\)" using assms normal_imp_subgroup subgroup_imp_subset by blast + have "N \ carrier (G\carrier := H\)" using assms normal_imp_subgroup subgroup.subset by blast hence NH : "N \ H" by simp - have "K \ carrier(G\carrier := H\)" using subgroup_imp_subset assms by blast + have "K \ carrier(G\carrier := H\)" using subgroup.subset assms by blast hence KH : "K \ H" by simp have Egal : "K <#>\<^bsub>G\carrier := H\\<^esub> N = N <#>\<^bsub>G\carrier := H\\<^esub> K" using group.commut_normal[where ?G = "G\carrier :=H\", of K N,OF subgroup_imp_group[OF assms(1)] @@ -1235,7 +1235,7 @@ show "subgroup (H\K) G" using HK_def subgroups_Inter_pair assms by auto next have "H1 \ (carrier (G\carrier:=H\))" - using assms(3) normal_imp_subgroup subgroup_imp_subset by blast + using assms(3) normal_imp_subgroup subgroup.subset by blast also have "... \ H" by simp thus "H1K \H\K" using H1K_def calculation by auto @@ -1256,7 +1256,7 @@ hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x" using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp have "H1\carrier(GH)" - using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast + using assms GH_def normal_imp_subgroup subgroup.subset by blast hence hHK:"h\HK" using p2 H1K_def HK_def GH_def by auto hence xhx_egal : "x \\<^bsub>GHK\<^esub> h \\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub>x = x \\<^bsub>GH\<^esub> h \\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x" @@ -1291,7 +1291,7 @@ moreover have "normal N (G \carrier :=K\)" using assms K_def by simp ultimately have "N \ H \ G\carrier := K \ H\" using normal_inter[of K H N] assms(1) by blast - moreover have "K \ H = H" using K_def assms subgroup_imp_subset by blast + moreover have "K \ H = H" using K_def assms subgroup.subset by blast ultimately show "normal (N\H) (G\carrier := H\)" by auto qed diff -r 6d0f1a5a16ea -r c027dfbfad30 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Thu Jun 14 17:50:23 2018 +0200 +++ b/src/HOL/Algebra/Group.thy Fri Jun 15 12:18:06 2018 +0100 @@ -1274,9 +1274,9 @@ and "subgroup I (G\carrier:=J\)" shows "subgroup I G" unfolding subgroup_def proof - have H1: "I \ carrier (G\carrier:=J\)" using assms(2) subgroup_imp_subset by blast + have H1: "I \ carrier (G\carrier:=J\)" using assms(2) subgroup.subset by blast also have H2: "...\J" by simp - also have "...\(carrier G)" by (simp add: assms(1) subgroup_imp_subset) + also have "...\(carrier G)" by (simp add: assms(1) subgroup.subset) finally have H: "I \ carrier G" by simp have "(\x y. \x \ I ; y \ I\ \ x \ y \ I)" using assms(2) by (auto simp add: subgroup_def) thus "I \ carrier G \ (\x y. x \ I \ y \ I \ x \ y \ I)" using H by blast diff -r 6d0f1a5a16ea -r c027dfbfad30 src/HOL/Algebra/Zassenhaus.thy --- a/src/HOL/Algebra/Zassenhaus.thy Thu Jun 14 17:50:23 2018 +0200 +++ b/src/HOL/Algebra/Zassenhaus.thy Fri Jun 15 12:18:06 2018 +0100 @@ -11,22 +11,22 @@ shows "normal H (G\carrier:= (normalizer G H)\)" proof(intro group.normal_invI) show "Group.group (G\carrier := normalizer G H\)" - by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup_imp_subset) + by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset) have K:"H \ (normalizer G H)" unfolding normalizer_def proof fix x assume xH: "x \ H" - from xH have xG : "x \ carrier G" using subgroup_imp_subset assms by auto + from xH have xG : "x \ carrier G" using subgroup.subset assms by auto have "x <# H = H" by (metis \x \ H\ assms group.lcos_mult_one is_group - l_repr_independence one_closed subgroup_imp_subset) + l_repr_independence one_closed subgroup.subset) 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" - using assms xG subgroup_imp_subset unfolding stabilizer_def by auto + using assms xG subgroup.subset unfolding stabilizer_def by auto qed thus "subgroup H (G\carrier:= (normalizer G H)\)" - using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup_imp_subset) + using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset) show " \x h. x \ carrier (G\carrier := normalizer G H\) \ h \ H \ x \\<^bsub>G\carrier := normalizer G H\\<^esub> h \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x \ H" @@ -37,7 +37,7 @@ ultimately have "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h = x \ h" by simp moreover have " inv\<^bsub>G\carrier := normalizer G H\\<^esub> x = inv x" using xnormalizer - by (simp add: assms normalizer_imp_subgroup subgroup_imp_subset subgroup_inv_equality) + by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality) ultimately have xhxegal: "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x = x \h \ inv x" @@ -45,7 +45,7 @@ have "x \h \ inv x \ (x <# H #> inv x)" unfolding l_coset_def r_coset_def using hH by auto moreover have "x <# H #> inv x = H" - using xnormalizer assms subgroup_imp_subset[OF assms] + using xnormalizer assms subgroup.subset[OF assms] unfolding normalizer_def stabilizer_def by auto ultimately have "x \h \ inv x \ H" by simp thus " x \\<^bsub>G\carrier := normalizer G H\\<^esub> h @@ -61,12 +61,12 @@ shows "subgroup H (G\carrier := normalizer G N\)" proof- have N_carrierG : "N \ carrier(G)" - using assms normal_imp_subgroup subgroup_imp_subset + using assms normal_imp_subgroup subgroup.subset by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1)) {have "H \ normalizer G N" unfolding normalizer_def stabilizer_def proof fix x assume xH : "x \ H" - hence xcarrierG : "x \ carrier(G)" using assms subgroup_imp_subset by auto + hence xcarrierG : "x \ carrier(G)" using assms subgroup.subset by auto have " N #> x = x <# N" using assms xH unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto hence "x <# N #> inv x =(N #> x) #> inv x" @@ -79,7 +79,7 @@ qed} thus "subgroup H (G\carrier := normalizer G N\)" using subgroup_incl[OF assms(1) normalizer_imp_subgroup] - assms normal_imp_subgroup subgroup_imp_subset + assms normal_imp_subgroup subgroup.subset by (metis group.incl_subgroup is_group) qed @@ -92,7 +92,7 @@ shows "subgroup (N<#>H) G" unfolding subgroup_def proof- have A :"N <#> H \ carrier G" - using assms setmult_subset_G by (simp add: normal_imp_subgroup subgroup_imp_subset) + using assms setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset) have B :"\ x y. \x \ (N <#> H); y \ (N <#> H)\ \ (x \ y) \ (N<#>H)" proof- @@ -102,7 +102,7 @@ obtain n2 h2 where B3:"n2 \ N \ h2 \ H \ n2\h2 = y" 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_imp_subset by blast + using normalI B2 assms normal.coset_eq subgroup.subset by blast 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" @@ -132,7 +132,7 @@ 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_imp_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 @@ -159,10 +159,10 @@ proof- have Hyp:"subgroup (N <#>\<^bsub>G\carrier := K\\<^esub> H) (G\carrier := K\)" using group.mult_norm_subgroup[where ?G = "G\carrier := K\"] assms subgroup_imp_group by auto - have "H \ carrier(G\carrier := K\)" using assms subgroup_imp_subset by blast + have "H \ carrier(G\carrier := K\)" using assms subgroup.subset by blast also have "... \ K" by simp finally have Incl1:"H \ K" by simp - have "N \ carrier(G\carrier := K\)" using assms normal_imp_subgroup subgroup_imp_subset by blast + have "N \ carrier(G\carrier := K\)" using assms normal_imp_subgroup subgroup.subset by blast also have "... \ K" by simp finally have Incl2:"N \ K" by simp have "(N <#>\<^bsub>G\carrier := K\\<^esub> H) = (N <#> H)" @@ -209,7 +209,7 @@ have GroupNH : "Group.group (G\carrier := N<#>H\)" using subgroup_imp_group assms mult_norm_subgroup by simp have HcarrierNH :"H \ carrier(G\carrier := N<#>H\)" - using assms subgroup_of_normal_set_mult subgroup_imp_subset by blast + using assms subgroup_of_normal_set_mult subgroup.subset by blast hence HNH :"H \ N<#>H" by simp have op_hom : "f \ hom (G\carrier := H\) (G\carrier := N <#> H\ Mod N)" unfolding hom_def proof @@ -277,7 +277,7 @@ have "x = (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N (n \ h)" using K nhnh by simp hence "x = (#>) N (n \ h)" using K nhnh unfolding r_coset_def by auto also have "... = (N #> n) #>h" - using coset_mult_assoc hH nN assms subgroup_imp_subset normal_imp_subgroup + using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup by (metis subgroup.mem_carrier) finally have "x = (#>) N h" using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier) @@ -326,9 +326,9 @@ 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_imp_subset[OF assms(2)]], of N H] - subgroup_imp_subset[OF assms(3)] - subgroup_imp_subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]] + 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 ultimately have "G\carrier := normalizer G N, carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ @@ -338,7 +338,7 @@ carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ G\carrier := normalizer G N, carrier := H\ Mod N \ H" using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF - subgroup_imp_subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]] + subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]] by simp 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 @@ -350,7 +350,7 @@ and "subgroup N G" and "subgroup H (G\carrier:= (normalizer G N)\)" shows "(G\carrier:= H<#>N\ Mod N) \ (G\carrier:= H\ Mod (H\N))" - by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup_imp_subset + by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset normalizer_imp_subgroup snd_iso_thme) @@ -365,29 +365,29 @@ shows "subgroup (H\K) (G\carrier:=(normalizer G (H1<#>(H\K1))) \)" proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]]) show "subgroup (normalizer G (H1 <#> H \ K1)) G" - using normalizer_imp_subgroup assms normal_imp_subgroup subgroup_imp_subset + using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair) next show "H \ K \ normalizer G (H1 <#> H \ K1)" unfolding normalizer_def stabilizer_def proof fix x assume xHK : "x \ H \ K" hence xG : "{x} \ carrier G" "{inv x} \ carrier G" - using subgroup_imp_subset assms inv_closed xHK by auto + using subgroup.subset assms inv_closed xHK by auto have allG : "H \ carrier G" "K \ carrier G" "H1 \ carrier G" "K1 \ carrier G" - using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+ . + using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ . have HK1_normal: "H\K1 \ (G\carrier := H \ K\)" using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add : inf_commute) have "H \ K \ normalizer G (H \ K1)" - using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF + using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF assms(1)assms(3)]HK1_normal]] by auto hence "x <# (H \ K1) #> inv x = (H \ K1)" - using xHK subgroup_imp_subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3) + using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3) normal_imp_subgroup[OF assms(4)]]]] unfolding normalizer_def stabilizer_def by auto moreover have "H \ normalizer G H1" - using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto + using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto hence "x <# H1 #> inv x = H1" - using xHK subgroup_imp_subset[OF incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]] + using xHK subgroup.subset[OF incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]] unfolding normalizer_def stabilizer_def by auto ultimately have "H1 <#> H \ K1 = (x <# H1 #> inv x) <#> (x <# H \ K1 #> inv x)" by auto also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \ K1 <#> {inv x})" @@ -418,31 +418,31 @@ shows " (H\K) \ (H1<#>(H\K1)) = (H1\K)<#>(H\K1)" proof have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G" - using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+. + using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+. show "H \ K \ (H1 <#> H \ K1) \ H1 \ K <#> H \ K1" proof fix x assume x_def : "x \ (H \ K) \ (H1 <#> (H \ K1))" from x_def have x_incl : "x \ H" "x \ K" "x \ (H1 <#> (H \ K1))" by auto then obtain h1 hk1 where h1hk1_def : "h1 \ H1" "hk1 \ H \ K1" "h1 \ hk1 = x" using assms unfolding set_mult_def by blast - hence "hk1 \ H \ K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(4)]] by auto + hence "hk1 \ H \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto hence "inv hk1 \ H \ K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto moreover have "h1 \ hk1 \ H \ K" using x_incl h1hk1_def by auto ultimately have "h1 \ hk1 \ inv hk1 \ H \ K" using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto - hence "h1 \ H \ K" using h1hk1_def assms subgroup_imp_subset incl_subgroup normal_imp_subgroup + hence "h1 \ H \ K" using h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup by (metis Int_iff contra_subsetD inv_solve_right m_closed) hence "h1 \ H1 \ H \ K" using h1hk1_def by auto - hence "h1 \ H1 \ K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(2)]] by auto + hence "h1 \ H1 \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto hence "h1 \ hk1 \ (H1\