src/HOL/Algebra/Group.thy
 changeset 26805 27941d7d9a11 parent 26199 04817a8802f2 child 27611 2c01c0bdb385
```     1.1 --- a/src/HOL/Algebra/Group.thy	Wed May 07 10:56:55 2008 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 07 10:56:58 2008 +0200
1.3 @@ -735,38 +735,42 @@
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 -  have "greatest ?L (carrier G) (carrier ?L)"
1.8 -    by (unfold greatest_def)
1.9 -      (simp add: subgroup.subset subgroup_self)
1.10 -  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
1.11 +  show "\<exists>G. greatest ?L G (carrier ?L)"
1.12 +  proof
1.13 +    show "greatest ?L (carrier G) (carrier ?L)"
1.14 +      by (unfold greatest_def)
1.15 +        (simp add: subgroup.subset subgroup_self)
1.16 +  qed
1.17  next
1.18    fix A
1.19    assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
1.20    then have Int_subgroup: "subgroup (\<Inter>A) G"
1.21      by (fastsimp intro: subgroups_Inter)
1.22 -  have "greatest ?L (\<Inter>A) (Lower ?L A)"
1.23 -    (is "greatest _ ?Int _")
1.24 -  proof (rule greatest_LowerI)
1.25 -    fix H
1.26 -    assume H: "H \<in> A"
1.27 -    with L have subgroupH: "subgroup H G" by auto
1.28 -    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
1.29 -      by (rule subgroup_imp_group)
1.30 -    from groupH have monoidH: "monoid ?H"
1.31 -      by (rule group.is_monoid)
1.32 -    from H have Int_subset: "?Int \<subseteq> H" by fastsimp
1.33 -    then show "le ?L ?Int H" by simp
1.34 -  next
1.35 -    fix H
1.36 -    assume H: "H \<in> Lower ?L A"
1.37 -    with L Int_subgroup show "le ?L H ?Int"
1.38 -      by (fastsimp simp: Lower_def intro: Inter_greatest)
1.39 -  next
1.40 -    show "A \<subseteq> carrier ?L" by (rule L)
1.41 -  next
1.42 -    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
1.43 +  show "\<exists>I. greatest ?L I (Lower ?L A)"
1.44 +  proof
1.45 +    show "greatest ?L (\<Inter>A) (Lower ?L A)"
1.46 +      (is "greatest _ ?Int _")
1.47 +    proof (rule greatest_LowerI)
1.48 +      fix H
1.49 +      assume H: "H \<in> A"
1.50 +      with L have subgroupH: "subgroup H G" by auto
1.51 +      from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
1.52 +	by (rule subgroup_imp_group)
1.53 +      from groupH have monoidH: "monoid ?H"
1.54 +	by (rule group.is_monoid)
1.55 +      from H have Int_subset: "?Int \<subseteq> H" by fastsimp
1.56 +      then show "le ?L ?Int H" by simp
1.57 +    next
1.58 +      fix H
1.59 +      assume H: "H \<in> Lower ?L A"
1.60 +      with L Int_subgroup show "le ?L H ?Int"
1.61 +	by (fastsimp simp: Lower_def intro: Inter_greatest)
1.62 +    next
1.63 +      show "A \<subseteq> carrier ?L" by (rule L)
1.64 +    next
1.65 +      show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
1.66 +    qed
1.67    qed
1.68 -  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
1.69  qed
1.70
1.71  end
```