Revert 5a42eddc11c1.
authorballarin
Thu Aug 31 21:48:01 2017 +0200 (2017-08-31)
changeset 665792db3fe23fdaf
parent 66578 6a034c6c423f
child 66580 e5b1d4d55bf6
Revert 5a42eddc11c1.
src/HOL/Algebra/Complete_Lattice.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Group.thy
     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