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