src/HOL/Algebra/Group.thy
changeset 46008 c296c75f4cf4
parent 44890 22f665a2e91c
child 46559 69a273fcd53a
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Dec 28 15:08:12 2011 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Dec 28 20:03:13 2011 +0100
     1.3 @@ -771,42 +771,36 @@
     1.4  proof (rule partial_order.complete_lattice_criterion1)
     1.5    show "partial_order ?L" by (rule subgroups_partial_order)
     1.6  next
     1.7 -  show "\<exists>G. greatest ?L G (carrier ?L)"
     1.8 -  proof
     1.9 -    show "greatest ?L (carrier G) (carrier ?L)"
    1.10 -      by (unfold greatest_def)
    1.11 -        (simp add: subgroup.subset subgroup_self)
    1.12 -  qed
    1.13 +  have "greatest ?L (carrier G) (carrier ?L)"
    1.14 +    by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
    1.15 +  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
    1.16  next
    1.17    fix A
    1.18    assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
    1.19    then have Int_subgroup: "subgroup (\<Inter>A) G"
    1.20      by (fastforce intro: subgroups_Inter)
    1.21 -  show "\<exists>I. greatest ?L I (Lower ?L A)"
    1.22 -  proof
    1.23 -    show "greatest ?L (\<Inter>A) (Lower ?L A)"
    1.24 -      (is "greatest _ ?Int _")
    1.25 -    proof (rule greatest_LowerI)
    1.26 -      fix H
    1.27 -      assume H: "H \<in> A"
    1.28 -      with L have subgroupH: "subgroup H G" by auto
    1.29 -      from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
    1.30 -        by (rule subgroup_imp_group)
    1.31 -      from groupH have monoidH: "monoid ?H"
    1.32 -        by (rule group.is_monoid)
    1.33 -      from H have Int_subset: "?Int \<subseteq> H" by fastforce
    1.34 -      then show "le ?L ?Int H" by simp
    1.35 -    next
    1.36 -      fix H
    1.37 -      assume H: "H \<in> Lower ?L A"
    1.38 -      with L Int_subgroup show "le ?L H ?Int"
    1.39 -        by (fastforce simp: Lower_def intro: Inter_greatest)
    1.40 -    next
    1.41 -      show "A \<subseteq> carrier ?L" by (rule L)
    1.42 -    next
    1.43 -      show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
    1.44 -    qed
    1.45 +  have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
    1.46 +  proof (rule greatest_LowerI)
    1.47 +    fix H
    1.48 +    assume H: "H \<in> A"
    1.49 +    with L have subgroupH: "subgroup H G" by auto
    1.50 +    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
    1.51 +      by (rule subgroup_imp_group)
    1.52 +    from groupH have monoidH: "monoid ?H"
    1.53 +      by (rule group.is_monoid)
    1.54 +    from H have Int_subset: "?Int \<subseteq> H" by fastforce
    1.55 +    then show "le ?L ?Int H" by simp
    1.56 +  next
    1.57 +    fix H
    1.58 +    assume H: "H \<in> Lower ?L A"
    1.59 +    with L Int_subgroup show "le ?L H ?Int"
    1.60 +      by (fastforce simp: Lower_def intro: Inter_greatest)
    1.61 +  next
    1.62 +    show "A \<subseteq> carrier ?L" by (rule L)
    1.63 +  next
    1.64 +    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
    1.65    qed
    1.66 +  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
    1.67  qed
    1.68  
    1.69  end