equal
deleted
inserted
replaced
4 Author: Clemens Ballarin, started 4 February 2003 |
4 Author: Clemens Ballarin, started 4 February 2003 |
5 |
5 |
6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. |
6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. |
7 *) |
7 *) |
8 |
8 |
9 theory Group imports FuncSet Lattice begin |
9 theory Group |
|
10 imports Lattice FuncSet |
|
11 begin |
10 |
12 |
11 |
13 |
12 section {* Monoids and Groups *} |
14 section {* Monoids and Groups *} |
13 |
15 |
14 subsection {* Definitions *} |
16 subsection {* Definitions *} |
278 from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>" |
280 from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>" |
279 by (fast intro: l_inv r_inv) |
281 by (fast intro: l_inv r_inv) |
280 qed |
282 qed |
281 then have carrier_subset_Units: "carrier G <= Units G" |
283 then have carrier_subset_Units: "carrier G <= Units G" |
282 by (unfold Units_def) fast |
284 by (unfold Units_def) fast |
283 show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units) |
285 show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units) |
284 qed |
286 qed |
285 |
287 |
286 lemma (in monoid) group_l_invI: |
288 lemma (in monoid) group_l_invI: |
287 assumes l_inv_ex: |
289 assumes l_inv_ex: |
288 "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" |
290 "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" |
683 |
685 |
684 lemma (in group) group_comm_groupI: |
686 lemma (in group) group_comm_groupI: |
685 assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> |
687 assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> |
686 x \<otimes> y = y \<otimes> x" |
688 x \<otimes> y = y \<otimes> x" |
687 shows "comm_group G" |
689 shows "comm_group G" |
688 by unfold_locales (simp_all add: m_comm) |
690 proof qed (simp_all add: m_comm) |
689 |
691 |
690 lemma comm_groupI: |
692 lemma comm_groupI: |
691 fixes G (structure) |
693 fixes G (structure) |
692 assumes m_closed: |
694 assumes m_closed: |
693 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
695 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
711 |
713 |
712 text_raw {* \label{sec:subgroup-lattice} *} |
714 text_raw {* \label{sec:subgroup-lattice} *} |
713 |
715 |
714 theorem (in group) subgroups_partial_order: |
716 theorem (in group) subgroups_partial_order: |
715 "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" |
717 "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" |
716 by unfold_locales simp_all |
718 proof qed simp_all |
717 |
719 |
718 lemma (in group) subgroup_self: |
720 lemma (in group) subgroup_self: |
719 "subgroup (carrier G) G" |
721 "subgroup (carrier G) G" |
720 by (rule subgroupI) auto |
722 by (rule subgroupI) auto |
721 |
723 |