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
```