src/HOL/Algebra/Group.thy
changeset 66579 2db3fe23fdaf
parent 66501 5a42eddc11c1
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Algebra/Group.thy	Thu Aug 31 20:19:55 2017 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Thu Aug 31 21:48:01 2017 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  *)
     1.5  
     1.6  theory Group
     1.7 -imports Order "HOL-Library.FuncSet"
     1.8 +imports Complete_Lattice "HOL-Library.FuncSet"
     1.9  begin
    1.10  
    1.11  section \<open>Monoids and Groups\<close>
    1.12 @@ -817,4 +817,42 @@
    1.13    show "x \<otimes> y \<in> \<Inter>A" by blast
    1.14  qed
    1.15  
    1.16 +theorem (in group) subgroups_complete_lattice:
    1.17 +  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
    1.18 +    (is "complete_lattice ?L")
    1.19 +proof (rule partial_order.complete_lattice_criterion1)
    1.20 +  show "partial_order ?L" by (rule subgroups_partial_order)
    1.21 +next
    1.22 +  have "greatest ?L (carrier G) (carrier ?L)"
    1.23 +    by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
    1.24 +  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
    1.25 +next
    1.26 +  fix A
    1.27 +  assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
    1.28 +  then have Int_subgroup: "subgroup (\<Inter>A) G"
    1.29 +    by (fastforce intro: subgroups_Inter)
    1.30 +  have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
    1.31 +  proof (rule greatest_LowerI)
    1.32 +    fix H
    1.33 +    assume H: "H \<in> A"
    1.34 +    with L have subgroupH: "subgroup H G" by auto
    1.35 +    from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H")
    1.36 +      by (rule subgroup_imp_group)
    1.37 +    from groupH have monoidH: "monoid ?H"
    1.38 +      by (rule group.is_monoid)
    1.39 +    from H have Int_subset: "?Int \<subseteq> H" by fastforce
    1.40 +    then show "le ?L ?Int H" by simp
    1.41 +  next
    1.42 +    fix H
    1.43 +    assume H: "H \<in> Lower ?L A"
    1.44 +    with L Int_subgroup show "le ?L H ?Int"
    1.45 +      by (fastforce simp: Lower_def intro: Inter_greatest)
    1.46 +  next
    1.47 +    show "A \<subseteq> carrier ?L" by (rule L)
    1.48 +  next
    1.49 +    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
    1.50 +  qed
    1.51 +  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
    1.52 +qed
    1.53 +
    1.54  end