corrections to markup
authorpaulson <lp15@cam.ac.uk>
Mon Jun 18 15:56:03 2018 +0100 (12 months ago)
changeset 684663d8241f4198b
parent 68465 e699ca8e22b7
child 68467 44ffc5b9cd76
corrections to markup
CONTRIBUTORS
NEWS
src/HOL/Algebra/Zassenhaus.thy
src/HOL/Analysis/Cross3.thy
     1.1 --- a/CONTRIBUTORS	Mon Jun 18 14:22:26 2018 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Jun 18 15:56:03 2018 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to Isabelle2018
     1.5  -----------------------------
     1.6  
     1.7 +* June 2018: Martin Baillon and Paulo Emílio de Vilhena
     1.8 +  A variety of contributions to HOL-Algebra.
     1.9 +
    1.10  * May 2018: Manuel Eberl
    1.11    Landau symbols and asymptotic equivalence (moved from the AFP).
    1.12  
     2.1 --- a/NEWS	Mon Jun 18 14:22:26 2018 +0100
     2.2 +++ b/NEWS	Mon Jun 18 15:56:03 2018 +0100
     2.3 @@ -375,6 +375,10 @@
     2.4  * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
     2.5  infix/prefix notation.
     2.6  
     2.7 +* Session HOL-Algebra: Revamped with much new material.
     2.8 +The set of isomorphisms between two groups is now denoted iso rather than iso_set.
     2.9 +INCOMPATIBILITY.
    2.10 +
    2.11  * Session HOL-Analysis: infinite products, Moebius functions, the
    2.12  Riemann mapping theorem, the Vitali covering theorem,
    2.13  change-of-variables results for integration and measures.
     3.1 --- a/src/HOL/Algebra/Zassenhaus.thy	Mon Jun 18 14:22:26 2018 +0100
     3.2 +++ b/src/HOL/Algebra/Zassenhaus.thy	Mon Jun 18 15:56:03 2018 +0100
     3.3 @@ -1,12 +1,18 @@
     3.4 +(*  Title:      HOL/Algebra/Zassenhaus.thy
     3.5 +    Author:     Martin Baillon
     3.6 +*)
     3.7 +
     3.8 +section \<open>The Zassenhaus Lemma\<close>
     3.9 +
    3.10  theory Zassenhaus
    3.11    imports Coset Group_Action
    3.12  begin
    3.13  
    3.14 -
    3.15 -subsubsection \<open>Lemmas about normalizer\<close>
    3.16 +text \<open>Proves the second isomorphism theorem and the Zassenhaus lemma.\<close>
    3.17  
    3.18 +subsection \<open>Lemmas about normalizer\<close>
    3.19  
    3.20 -lemma (in group) subgroup_in_normalizer: 
    3.21 +lemma (in group) subgroup_in_normalizer:
    3.22    assumes "subgroup H G"
    3.23    shows "normal H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
    3.24  proof(intro group.normal_invI)
    3.25 @@ -19,7 +25,7 @@
    3.26      have "x <# H = H"
    3.27        by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group
    3.28           l_repr_independence one_closed subgroup.subset)
    3.29 -    moreover have "H #> inv x = H" 
    3.30 +    moreover have "H #> inv x = H"
    3.31        by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
    3.32      ultimately have "x <# H #> (inv x) = H" by simp
    3.33      thus " x \<in> stabilizer G (\<lambda>g. \<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H"
    3.34 @@ -58,7 +64,7 @@
    3.35  lemma (in group) normal_imp_subgroup_normalizer:
    3.36    assumes "subgroup H G"
    3.37      and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
    3.38 -  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
    3.39 +  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
    3.40  proof-
    3.41    have N_carrierG : "N \<subseteq> carrier(G)"
    3.42      using assms normal_imp_subgroup subgroup.subset
    3.43 @@ -72,7 +78,7 @@
    3.44        hence "x <# N #> inv x =(N #> x) #> inv x"
    3.45          by simp
    3.46        also have "... = N #> \<one>"
    3.47 -        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
    3.48 +        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp
    3.49        finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
    3.50        thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
    3.51          using xcarrierG by (simp add : N_carrierG)
    3.52 @@ -103,10 +109,10 @@
    3.53        using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
    3.54      have "N #> h1 = h1 <# N"
    3.55        using normalI B2 assms normal.coset_eq subgroup.subset by blast
    3.56 -    hence "h1\<otimes>n2 \<in> N #> h1" 
    3.57 +    hence "h1\<otimes>n2 \<in> N #> h1"
    3.58        using B2 B3 assms l_coset_def by fastforce
    3.59 -    from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2" 
    3.60 -      using singletonD by (metis (no_types, lifting) UN_E r_coset_def) 
    3.61 +    from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2"
    3.62 +      using singletonD by (metis (no_types, lifting) UN_E r_coset_def)
    3.63      have " x\<otimes>y =  n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3
    3.64        by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier)
    3.65      moreover have B4 :"n1 \<otimes> y2 \<in>N"
    3.66 @@ -129,10 +135,10 @@
    3.67      hence "... \<otimes>h \<in> N"
    3.68        using assms C2
    3.69        by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier)
    3.70 -    hence  C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)" 
    3.71 +    hence  C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)"
    3.72        using   C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
    3.73      have "inv h \<otimes> inv n \<otimes> h \<otimes> inv h = inv h \<otimes> inv n"
    3.74 -      using  subgroup.subset[OF assms(2)] 
    3.75 +      using  subgroup.subset[OF assms(2)]
    3.76        by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
    3.77      thus "inv(x)\<in>N<#>H" using C4 C2 C3 by simp
    3.78    qed
    3.79 @@ -149,7 +155,7 @@
    3.80    thus "(N <#> H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> N <#> H \<longrightarrow> y \<in> N <#> H \<longrightarrow> x \<otimes> y \<in> N <#> H)) \<and>
    3.81      \<one> \<in> N <#> H \<and> (\<forall>x. x \<in> N <#> H \<longrightarrow> inv x \<in> N <#> H)" using A B C D assms by blast
    3.82  qed
    3.83 -    
    3.84 +
    3.85  
    3.86  lemma (in group) mult_norm_sub_in_sub:
    3.87    assumes "normal N (G\<lparr>carrier:=K\<rparr>)"
    3.88 @@ -201,7 +207,7 @@
    3.89  
    3.90  
    3.91  proposition (in group) weak_snd_iso_thme:
    3.92 -  assumes "subgroup  H G" 
    3.93 +  assumes "subgroup  H G"
    3.94      and "N\<lhd>G"
    3.95    shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))"
    3.96  proof-
    3.97 @@ -325,8 +331,8 @@
    3.98            carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
    3.99           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
   3.100            (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
   3.101 -         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H" 
   3.102 -    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H] 
   3.103 +         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
   3.104 +    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
   3.105            subgroup.subset[OF assms(3)]
   3.106            subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
   3.107      by simp
   3.108 @@ -343,7 +349,7 @@
   3.109    moreover have "H\<inter>N = N\<inter>H" using assms  by auto
   3.110    ultimately show "(G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod H \<inter> N" by auto
   3.111  qed
   3.112 - 
   3.113 +
   3.114  
   3.115  corollary (in group) snd_iso_thme_recip :
   3.116    assumes "subgroup H G"
   3.117 @@ -358,9 +364,9 @@
   3.118  
   3.119  
   3.120  lemma (in group) distinc:
   3.121 -  assumes "subgroup  H G" 
   3.122 -    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   3.123 -    and  "subgroup K G" 
   3.124 +  assumes "subgroup  H G"
   3.125 +    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   3.126 +    and  "subgroup K G"
   3.127      and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   3.128    shows "subgroup (H\<inter>K) (G\<lparr>carrier:=(normalizer G (H1<#>(H\<inter>K1))) \<rparr>)"
   3.129  proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
   3.130 @@ -401,7 +407,7 @@
   3.131        by auto
   3.132      also have "... = {x} <#> (H1 <#> H \<inter> K1) <#> {inv x}"
   3.133        using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2)
   3.134 -    finally have "H1 <#> H \<inter> K1 = x <# (H1 <#> H \<inter> K1) #> inv x" 
   3.135 +    finally have "H1 <#> H \<inter> K1 = x <# (H1 <#> H \<inter> K1) #> inv x"
   3.136        using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
   3.137      thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H1 <#> H \<inter> K1)
   3.138                                                                         = H1 <#> H \<inter> K1}"
   3.139 @@ -411,9 +417,9 @@
   3.140  qed
   3.141  
   3.142  lemma (in group) preliminary1:
   3.143 -  assumes "subgroup  H G" 
   3.144 -    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   3.145 -    and  "subgroup K G" 
   3.146 +  assumes "subgroup  H G"
   3.147 +    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   3.148 +    and  "subgroup K G"
   3.149      and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   3.150    shows " (H\<inter>K) \<inter> (H1<#>(H\<inter>K1)) = (H1\<inter>K)<#>(H\<inter>K1)"
   3.151  proof
   3.152 @@ -452,15 +458,15 @@
   3.153  qed
   3.154  
   3.155  lemma (in group) preliminary2:
   3.156 -  assumes "subgroup  H G" 
   3.157 +  assumes "subgroup  H G"
   3.158      and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   3.159 -    and  "subgroup K G" 
   3.160 +    and  "subgroup K G"
   3.161      and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   3.162    shows "(H1<#>(H\<inter>K1)) \<lhd> G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>"
   3.163  proof-
   3.164    have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
   3.165      using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
   3.166 -  have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)" 
   3.167 +  have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)"
   3.168      using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
   3.169            assms(1)]] assms by auto
   3.170    have "Group.group (G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>)"
   3.171 @@ -541,7 +547,7 @@
   3.172      finally  have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =H1 <#> H \<inter> K1  #> hk"
   3.173        using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
   3.174             assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
   3.175 -    thus " H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = 
   3.176 +    thus " H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =
   3.177               x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1)" using eq1 by simp
   3.178    qed
   3.179    ultimately show "H1 <#> H \<inter> K1 \<lhd> G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>"
   3.180 @@ -550,9 +556,9 @@
   3.181  
   3.182  
   3.183  proposition (in group)  Zassenhaus_1:
   3.184 -  assumes "subgroup  H G" 
   3.185 -    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   3.186 -    and  "subgroup K G" 
   3.187 +  assumes "subgroup  H G"
   3.188 +    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   3.189 +    and  "subgroup K G"
   3.190      and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   3.191    shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>H\<inter>K1)) \<cong> (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
   3.192  proof-
   3.193 @@ -572,7 +578,7 @@
   3.194      also have "... = ((H\<inter>K)<#>H1) <#>(H\<inter>K1)"
   3.195        using set_mult_assoc[where ?M = "H\<inter>K"] K1_incl_G H1_incl_G assms
   3.196        by (simp add: inf.coboundedI2 subgroup.subset)
   3.197 -    also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)" 
   3.198 +    also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)"
   3.199        using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
   3.200      also have "... =  H1 <#> ((H\<inter>K)<#>(H\<inter>K1))"
   3.201        using set_mult_assoc K1_incl_G H1_incl_G assms
   3.202 @@ -585,25 +591,25 @@
   3.203                incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms
   3.204                normal_imp_subgroup by (metis inf_commute normal_inter)
   3.205      qed
   3.206 -    hence " H1 <#> ((H\<inter>K)<#>(H\<inter>K1)) =  H1 <#> ((H\<inter>K))" 
   3.207 +    hence " H1 <#> ((H\<inter>K)<#>(H\<inter>K1)) =  H1 <#> ((H\<inter>K))"
   3.208        by simp
   3.209      thus "N <#> N1 = H1 <#> H \<inter> K"
   3.210        by (simp add: calculation)
   3.211    qed
   3.212  
   3.213 -  have "N\<inter>N1 = (H1\<inter>K)<#>(H\<inter>K1)" 
   3.214 -    using preliminary1 assms N_def N1_def by simp 
   3.215 +  have "N\<inter>N1 = (H1\<inter>K)<#>(H\<inter>K1)"
   3.216 +    using preliminary1 assms N_def N1_def by simp
   3.217    thus  "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod N1)  \<cong> (G\<lparr>carrier:= N\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
   3.218      using H_simp Hp by auto
   3.219  qed
   3.220  
   3.221  
   3.222  theorem (in group) Zassenhaus:
   3.223 -  assumes "subgroup  H G" 
   3.224 -    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   3.225 -    and  "subgroup K G" 
   3.226 +  assumes "subgroup  H G"
   3.227 +    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   3.228 +    and  "subgroup K G"
   3.229      and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   3.230 -  shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1)))  \<cong> 
   3.231 +  shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1)))  \<cong>
   3.232           (G\<lparr>carrier:= K1 <#> (H\<inter>K)\<rparr> Mod (K1<#>(K\<inter>H1)))"
   3.233  proof-
   3.234    define Gmod1 Gmod2 Gmod3 Gmod4
   3.235 @@ -620,8 +626,8 @@
   3.236      show "K1 \<inter> H \<lhd> G\<lparr>carrier := H \<inter> K\<rparr>"
   3.237        using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute)
   3.238     next
   3.239 -    show "subgroup (K \<inter> H1) (G\<lparr>carrier := H \<inter> K\<rparr>)" 
   3.240 -      using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter) 
   3.241 +    show "subgroup (K \<inter> H1) (G\<lparr>carrier := H \<inter> K\<rparr>)"
   3.242 +      using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter)
   3.243    qed
   3.244    hence  "Gmod3  = Gmod4" using Hp Gmod4_def by simp
   3.245    hence "Gmod1 \<cong> Gmod2"
     4.1 --- a/src/HOL/Analysis/Cross3.thy	Mon Jun 18 14:22:26 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Cross3.thy	Mon Jun 18 15:56:03 2018 +0100
     4.3 @@ -1,16 +1,22 @@
     4.4 +(* Title:      HOL/Analysis/Cross3.thy
     4.5 +   Author:     L C Paulson, University of Cambridge
     4.6 +
     4.7 +Ported from HOL Light
     4.8 +*)
     4.9 +
    4.10 +section\<open>Vector Cross Products in 3 Dimensions.\<close>
    4.11 +
    4.12  theory "Cross3"
    4.13    imports Determinants
    4.14  begin
    4.15  
    4.16 -subsection\<open>Vector Cross products in real^3.                                                 \<close>
    4.17 -
    4.18  definition cross3 :: "[real^3, real^3] \<Rightarrow> real^3"  (infixr "\<times>" 80)
    4.19    where "a \<times> b \<equiv>
    4.20      vector [a$2 * b$3 - a$3 * b$2,
    4.21              a$3 * b$1 - a$1 * b$3,
    4.22              a$1 * b$2 - a$2 * b$1]"
    4.23  
    4.24 -subsubsection\<open> Basic lemmas.\<close>
    4.25 +subsection\<open> Basic lemmas.\<close>
    4.26  
    4.27  lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
    4.28