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

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