# HG changeset patch # User ballarin # Date 1084555762 -7200 # Node ID 0d7850e27fed4b30d7d2743b0e127dd13b85f045 # Parent 8f1ee65bd3ea57e55b1b8eab2cf15dbb1fedcf8c Change of theory hierarchy: Group is now based in Lattice. diff -r 8f1ee65bd3ea -r 0d7850e27fed lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Fri May 14 16:54:13 2004 +0200 +++ b/lib/texinputs/isabellesym.sty Fri May 14 19:29:22 2004 +0200 @@ -248,7 +248,7 @@ \newcommand{\isasymsqunion}{\isamath{\sqcup}} \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymsqinter}{\isamath{\sqcap}} -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires masmath +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath \newcommand{\isasymuplus}{\isamath{\uplus}} \newcommand{\isasymUplus}{\isamath{\biguplus\,}} \newcommand{\isasymnoteq}{\isamath{\not=}} diff -r 8f1ee65bd3ea -r 0d7850e27fed src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Fri May 14 16:54:13 2004 +0200 +++ b/src/HOL/Algebra/Group.thy Fri May 14 19:29:22 2004 +0200 @@ -8,7 +8,7 @@ header {* Groups *} -theory Group = FuncSet: +theory Group = FuncSet + Lattice: section {* From Magmas to Groups *} @@ -20,11 +20,6 @@ subsection {* Definitions *} -(* Object with a carrier set. *) - -record 'a partial_object = - carrier :: "'a set" - record 'a semigroup = "'a partial_object" + mult :: "['a, 'a] => 'a" (infixl "\\" 70) @@ -375,15 +370,6 @@ declare (in submagma) magma.intro [intro] semigroup.intro [intro] semigroup_axioms.intro [intro] -(* -alternative definition of submagma - -locale submagma = var H + struct G + - assumes subset [intro, simp]: "carrier H \ carrier G" - and m_equal [simp]: "mult H = mult G" - and m_closed [intro, simp]: - "[| x \ carrier H; y \ carrier H |] ==> x \ y \ carrier H" -*) lemma submagma_imp_subset: "submagma H G ==> H \ carrier G" @@ -727,4 +713,96 @@ "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv x \ inv y" by (simp add: m_ac inv_mult_group) +subsection {* Lattice of subgroups of a group *} + +text_raw {* \label{sec:subgroup-lattice} *} + +theorem (in group) subgroups_partial_order: + "partial_order (| carrier = {H. subgroup H G}, le = op \ |)" + by (rule partial_order.intro) simp_all + +lemma (in group) subgroup_self: + "subgroup (carrier G) G" + by (rule subgroupI) auto + +lemma (in group) subgroup_imp_group: + "subgroup H G ==> group (G(| carrier := H |))" + using subgroup.groupI [OF _ group.intro] . + +lemma (in group) is_monoid [intro, simp]: + "monoid G" + by (rule monoid.intro) + +lemma (in group) subgroup_inv_equality: + "[| subgroup H G; x \ H |] ==> m_inv (G (| carrier := H |)) x = inv x" +apply (rule_tac inv_equality [THEN sym]) + apply (rule group.l_inv [OF subgroup_imp_group, simplified]) + apply assumption+ + apply (rule subsetD [OF subgroup.subset]) + apply assumption+ +apply (rule subsetD [OF subgroup.subset]) + apply assumption +apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified]) + apply assumption+ +done + +theorem (in group) subgroups_Inter: + assumes subgr: "(!!H. H \ A ==> subgroup H G)" + and not_empty: "A ~= {}" + shows "subgroup (\A) G" +proof (rule subgroupI) + from subgr [THEN subgroup.subset] and not_empty + show "\A \ carrier G" by blast +next + from subgr [THEN subgroup.one_closed] + show "\A ~= {}" by blast +next + fix x assume "x \ \A" + with subgr [THEN subgroup.m_inv_closed] + show "inv x \ \A" by blast +next + fix x y assume "x \ \A" "y \ \A" + with subgr [THEN subgroup.m_closed] + show "x \ y \ \A" by blast +qed + +theorem (in group) subgroups_complete_lattice: + "complete_lattice (| carrier = {H. subgroup H G}, le = op \ |)" + (is "complete_lattice ?L") +proof (rule partial_order.complete_lattice_criterion1) + show "partial_order ?L" by (rule subgroups_partial_order) +next + have "greatest ?L (carrier G) (carrier ?L)" + by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) + then show "EX G. greatest ?L G (carrier ?L)" .. +next + fix A + assume L: "A \ carrier ?L" and non_empty: "A ~= {}" + then have Int_subgroup: "subgroup (\A) G" + by (fastsimp intro: subgroups_Inter) + have "greatest ?L (\A) (Lower ?L A)" + (is "greatest ?L ?Int _") + proof (rule greatest_LowerI) + fix H + assume H: "H \ A" + with L have subgroupH: "subgroup H G" by auto + from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms) + from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") + by (rule subgroup_imp_group) + from groupH have monoidH: "monoid ?H" + by (rule group.is_monoid) + from H have Int_subset: "?Int \ H" by fastsimp + then show "le ?L ?Int H" by simp + next + fix H + assume H: "H \ Lower ?L A" + with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest) + next + show "A \ carrier ?L" by (rule L) + next + show "?Int \ carrier ?L" by simp (rule Int_subgroup) + qed + then show "EX I. greatest ?L I (Lower ?L A)" .. +qed + end diff -r 8f1ee65bd3ea -r 0d7850e27fed src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Fri May 14 16:54:13 2004 +0200 +++ b/src/HOL/Algebra/Lattice.thy Fri May 14 19:29:22 2004 +0200 @@ -7,7 +7,12 @@ header {* Orders and Lattices *} -theory Lattice = Group: +theory Lattice = Main: + +text {* Object with a carrier set. *} + +record 'a partial_object = + carrier :: "'a set" subsection {* Partial Orders *} @@ -844,94 +849,7 @@ then show "EX i. greatest ?L i (Lower ?L B)" .. qed -subsubsection {* Lattice of subgroups of a group *} - -theorem (in group) subgroups_partial_order: - "partial_order (| carrier = {H. subgroup H G}, le = op \ |)" - by (rule partial_order.intro) simp_all - -lemma (in group) subgroup_self: - "subgroup (carrier G) G" - by (rule subgroupI) auto - -lemma (in group) subgroup_imp_group: - "subgroup H G ==> group (G(| carrier := H |))" - using subgroup.groupI [OF _ group.intro] . - -lemma (in group) is_monoid [intro, simp]: - "monoid G" - by (rule monoid.intro) - -lemma (in group) subgroup_inv_equality: - "[| subgroup H G; x \ H |] ==> m_inv (G (| carrier := H |)) x = inv x" -apply (rule_tac inv_equality [THEN sym]) - apply (rule group.l_inv [OF subgroup_imp_group, simplified]) - apply assumption+ - apply (rule subsetD [OF subgroup.subset]) - apply assumption+ -apply (rule subsetD [OF subgroup.subset]) - apply assumption -apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified]) - apply assumption+ -done - -theorem (in group) subgroups_Inter: - assumes subgr: "(!!H. H \ A ==> subgroup H G)" - and not_empty: "A ~= {}" - shows "subgroup (\A) G" -proof (rule subgroupI) - from subgr [THEN subgroup.subset] and not_empty - show "\A \ carrier G" by blast -next - from subgr [THEN subgroup.one_closed] - show "\A ~= {}" by blast -next - fix x assume "x \ \A" - with subgr [THEN subgroup.m_inv_closed] - show "inv x \ \A" by blast -next - fix x y assume "x \ \A" "y \ \A" - with subgr [THEN subgroup.m_closed] - show "x \ y \ \A" by blast -qed - -theorem (in group) subgroups_complete_lattice: - "complete_lattice (| carrier = {H. subgroup H G}, le = op \ |)" - (is "complete_lattice ?L") -proof (rule partial_order.complete_lattice_criterion1) - show "partial_order ?L" by (rule subgroups_partial_order) -next - have "greatest ?L (carrier G) (carrier ?L)" - by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) - then show "EX G. greatest ?L G (carrier ?L)" .. -next - fix A - assume L: "A \ carrier ?L" and non_empty: "A ~= {}" - then have Int_subgroup: "subgroup (\A) G" - by (fastsimp intro: subgroups_Inter) - have "greatest ?L (\A) (Lower ?L A)" - (is "greatest ?L ?Int _") - proof (rule greatest_LowerI) - fix H - assume H: "H \ A" - with L have subgroupH: "subgroup H G" by auto - from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms) - from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") - by (rule subgroup_imp_group) - from groupH have monoidH: "monoid ?H" - by (rule group.is_monoid) - from H have Int_subset: "?Int \ H" by fastsimp - then show "le ?L ?Int H" by simp - next - fix H - assume H: "H \ Lower ?L A" - with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest) - next - show "A \ carrier ?L" by (rule L) - next - show "?Int \ carrier ?L" by simp (rule Int_subgroup) - qed - then show "EX I. greatest ?L I (Lower ?L A)" .. -qed +text {* An other example, that of the lattice of subgroups of a group, + can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} end diff -r 8f1ee65bd3ea -r 0d7850e27fed src/HOL/Algebra/ROOT.ML --- a/src/HOL/Algebra/ROOT.ML Fri May 14 16:54:13 2004 +0200 +++ b/src/HOL/Algebra/ROOT.ML Fri May 14 19:29:22 2004 +0200 @@ -16,7 +16,6 @@ use_thy "FiniteProduct"; (* Product operator for commutative groups *) use_thy "Sylow"; (* Sylow's theorem *) use_thy "Bij"; (* Automorphism Groups *) -use_thy "Lattice"; (* Lattices, and the complete lattice of subgroups *) (* Rings *)