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

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