author ballarin Thu Aug 31 21:48:01 2017 +0200 (2017-08-31) changeset 66579 2db3fe23fdaf parent 66578 6a034c6c423f child 66580 e5b1d4d55bf6
Revert 5a42eddc11c1.
 src/HOL/Algebra/Complete_Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/Divisibility.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Algebra/Complete_Lattice.thy	Thu Aug 31 20:19:55 2017 +0200
1.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy	Thu Aug 31 21:48:01 2017 +0200
1.3 @@ -7,7 +7,7 @@
1.4  *)
1.5
1.6  theory Complete_Lattice
1.7 -imports Lattice Group
1.8 +imports Lattice
1.9  begin
1.10
1.11  section \<open>Complete Lattices\<close>
1.12 @@ -1192,43 +1192,8 @@
1.13    then show "EX i. greatest ?L i (Lower ?L B)" ..
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 +text \<open>Another example, that of the lattice of subgroups of a group,
1.54 +  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
1.55
1.56
1.57  subsection \<open>Limit preserving functions\<close>

     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Thu Aug 31 20:19:55 2017 +0200
2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Thu Aug 31 21:48:01 2017 +0200
2.3 @@ -6,7 +6,7 @@
2.4  section \<open>Divisibility in monoids and rings\<close>
2.5
2.6  theory Divisibility
2.7 -  imports "HOL-Library.Permutation" Coset Group Lattice
2.8 +  imports "HOL-Library.Permutation" Coset Group
2.9  begin
2.10
2.11  section \<open>Factorial Monoids\<close>

     3.1 --- a/src/HOL/Algebra/Group.thy	Thu Aug 31 20:19:55 2017 +0200
3.2 +++ b/src/HOL/Algebra/Group.thy	Thu Aug 31 21:48:01 2017 +0200
3.3 @@ -5,7 +5,7 @@
3.4  *)
3.5
3.6  theory Group
3.7 -imports Order "HOL-Library.FuncSet"
3.8 +imports Complete_Lattice "HOL-Library.FuncSet"
3.9  begin
3.10
3.11  section \<open>Monoids and Groups\<close>
3.12 @@ -817,4 +817,42 @@
3.13    show "x \<otimes> y \<in> \<Inter>A" by blast
3.14  qed
3.15
3.16 +theorem (in group) subgroups_complete_lattice:
3.17 +  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
3.18 +    (is "complete_lattice ?L")
3.19 +proof (rule partial_order.complete_lattice_criterion1)
3.20 +  show "partial_order ?L" by (rule subgroups_partial_order)
3.21 +next
3.22 +  have "greatest ?L (carrier G) (carrier ?L)"
3.23 +    by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
3.24 +  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
3.25 +next
3.26 +  fix A
3.27 +  assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
3.28 +  then have Int_subgroup: "subgroup (\<Inter>A) G"
3.29 +    by (fastforce intro: subgroups_Inter)
3.30 +  have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
3.31 +  proof (rule greatest_LowerI)
3.32 +    fix H
3.33 +    assume H: "H \<in> A"
3.34 +    with L have subgroupH: "subgroup H G" by auto
3.35 +    from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H")
3.36 +      by (rule subgroup_imp_group)
3.37 +    from groupH have monoidH: "monoid ?H"
3.38 +      by (rule group.is_monoid)
3.39 +    from H have Int_subset: "?Int \<subseteq> H" by fastforce
3.40 +    then show "le ?L ?Int H" by simp
3.41 +  next
3.42 +    fix H
3.43 +    assume H: "H \<in> Lower ?L A"
3.44 +    with L Int_subgroup show "le ?L H ?Int"
3.45 +      by (fastforce simp: Lower_def intro: Inter_greatest)
3.46 +  next
3.47 +    show "A \<subseteq> carrier ?L" by (rule L)
3.48 +  next
3.49 +    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
3.50 +  qed
3.51 +  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
3.52 +qed
3.53 +
3.54  end