summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/Group.thy

changeset 66501 | 5a42eddc11c1 |

parent 66453 | cc19f7ca2ed6 |

child 66579 | 2db3fe23fdaf |

1.1 --- a/src/HOL/Algebra/Group.thy Thu Aug 24 17:24:12 2017 +0200 1.2 +++ b/src/HOL/Algebra/Group.thy Thu Aug 24 17:41:49 2017 +0200 1.3 @@ -5,7 +5,7 @@ 1.4 *) 1.5 1.6 theory Group 1.7 -imports Complete_Lattice "HOL-Library.FuncSet" 1.8 +imports Order "HOL-Library.FuncSet" 1.9 begin 1.10 1.11 section \<open>Monoids and Groups\<close> 1.12 @@ -817,42 +817,4 @@ 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