moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.
Deleted Ring, Module from GroupTheory
Minor UNITY changes
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Coset.thy Tue Mar 18 18:07:06 2003 +0100
@@ -0,0 +1,464 @@
+(* Title: HOL/GroupTheory/Coset
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+*)
+
+header{*Theory of Cosets*}
+
+theory Coset = Group + Exponent:
+
+declare (in group) l_inv [simp] r_inv [simp]
+
+constdefs
+ r_coset :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"
+ "r_coset G H a == (% x. (mult G) x a) ` H"
+
+ l_coset :: "[('a,'b) group_scheme, 'a, 'a set] => 'a set"
+ "l_coset G a H == (% x. (mult G) a x) ` H"
+
+ rcosets :: "[('a,'b) group_scheme,'a set] => ('a set)set"
+ "rcosets G H == r_coset G H ` (carrier G)"
+
+ set_mult :: "[('a,'b) group_scheme,'a set,'a set] => 'a set"
+ "set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
+
+ set_inv :: "[('a,'b) group_scheme,'a set] => 'a set"
+ "set_inv G H == (m_inv G) ` H"
+
+ normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "<|" 60)
+ "normal H G == subgroup H G &
+ (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
+
+syntax (xsymbols)
+ normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "\<lhd>" 60)
+
+locale coset = group G +
+ fixes rcos :: "['a set, 'a] => 'a set" (infixl "#>" 60)
+ and lcos :: "['a, 'a set] => 'a set" (infixl "<#" 60)
+ and setmult :: "['a set, 'a set] => 'a set" (infixl "<#>" 60)
+ defines rcos_def: "H #> x == r_coset G H x"
+ and lcos_def: "x <# H == l_coset G x H"
+ and setmult_def: "H <#> K == set_mult G H K"
+
+
+text{*Lemmas useful for Sylow's Theorem*}
+
+lemma card_inj:
+ "[|f \<in> A\<rightarrow>B; inj_on f A; finite A; finite B|] ==> card(A) <= card(B)"
+apply (rule card_inj_on_le)
+apply (auto simp add: Pi_def)
+done
+
+lemma card_bij:
+ "[|f \<in> A\<rightarrow>B; inj_on f A;
+ g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
+by (blast intro: card_inj order_antisym)
+
+
+subsection{*Lemmas Using Locale Constants*}
+
+lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
+by (auto simp add: rcos_def r_coset_def)
+
+lemma (in coset) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}"
+by (auto simp add: lcos_def l_coset_def)
+
+lemma (in coset) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
+by (auto simp add: rcosets_def rcos_def)
+
+lemma (in coset) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}"
+by (simp add: setmult_def set_mult_def image_def)
+
+lemma (in coset) coset_mult_assoc:
+ "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
+ ==> (M #> g) #> h = M #> (g \<otimes> h)"
+by (force simp add: r_coset_eq m_assoc)
+
+lemma (in coset) coset_mult_one [simp]: "M <= carrier G ==> M #> \<one> = M"
+by (force simp add: r_coset_eq)
+
+lemma (in coset) coset_mult_inv1:
+ "[| M #> (x \<otimes> (inv y)) = M; x \<in> carrier G ; y \<in> carrier G;
+ M <= carrier G |] ==> M #> x = M #> y"
+apply (erule subst [of concl: "%z. M #> x = z #> y"])
+apply (simp add: coset_mult_assoc m_assoc)
+done
+
+lemma (in coset) coset_mult_inv2:
+ "[| M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M <= carrier G |]
+ ==> M #> (x \<otimes> (inv y)) = M "
+apply (simp add: coset_mult_assoc [symmetric])
+apply (simp add: coset_mult_assoc)
+done
+
+lemma (in coset) coset_join1:
+ "[| H #> x = H; x \<in> carrier G; subgroup H G |] ==> x\<in>H"
+apply (erule subst)
+apply (simp add: r_coset_eq)
+apply (blast intro: l_one subgroup.one_closed)
+done
+
+text{*Locales don't currently work with @{text rule_tac}, so we
+must prove this lemma separately.*}
+lemma (in coset) solve_equation:
+ "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
+apply (rule bexI [of _ "y \<otimes> (inv x)"])
+apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
+ subgroup.subset [THEN subsetD])
+done
+
+lemma (in coset) coset_join2:
+ "[| x \<in> carrier G; subgroup H G; x\<in>H |] ==> H #> x = H"
+by (force simp add: subgroup.m_closed r_coset_eq solve_equation)
+
+lemma (in coset) r_coset_subset_G:
+ "[| H <= carrier G; x \<in> carrier G |] ==> H #> x <= carrier G"
+by (auto simp add: r_coset_eq)
+
+lemma (in coset) rcosI:
+ "[| h \<in> H; H <= carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
+by (auto simp add: r_coset_eq)
+
+lemma (in coset) setrcosI:
+ "[| H <= carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
+by (auto simp add: setrcos_eq)
+
+
+text{*Really needed?*}
+lemma (in coset) transpose_inv:
+ "[| x \<otimes> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
+ ==> (inv x) \<otimes> z = y"
+by (force simp add: m_assoc [symmetric])
+
+lemma (in coset) repr_independence:
+ "[| y \<in> H #> x; x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
+by (auto simp add: r_coset_eq m_assoc [symmetric]
+ subgroup.subset [THEN subsetD]
+ subgroup.m_closed solve_equation)
+
+lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
+apply (simp add: r_coset_eq)
+apply (blast intro: l_one subgroup.subset [THEN subsetD]
+ subgroup.one_closed)
+done
+
+
+subsection{*normal subgroups*}
+
+(*????????????????
+text{*Allows use of theorems proved in the locale coset*}
+lemma subgroup_imp_coset: "subgroup H G ==> coset G"
+apply (drule subgroup_imp_group)
+apply (simp add: group_def coset_def)
+done
+*)
+
+lemma normal_imp_subgroup: "H <| G ==> subgroup H G"
+by (simp add: normal_def)
+
+
+(*????????????????
+lemmas normal_imp_group = normal_imp_subgroup [THEN subgroup_imp_group]
+lemmas normal_imp_coset = normal_imp_subgroup [THEN subgroup_imp_coset]
+*)
+
+lemma (in coset) normal_iff:
+ "(H <| G) = (subgroup H G & (\<forall>x \<in> carrier G. H #> x = x <# H))"
+by (simp add: lcos_def rcos_def normal_def)
+
+lemma (in coset) normal_imp_rcos_eq_lcos:
+ "[| H <| G; x \<in> carrier G |] ==> H #> x = x <# H"
+by (simp add: lcos_def rcos_def normal_def)
+
+lemma (in coset) normal_inv_op_closed1:
+ "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
+apply (auto simp add: l_coset_eq r_coset_eq normal_iff)
+apply (drule bspec, assumption)
+apply (drule equalityD1 [THEN subsetD], blast, clarify)
+apply (simp add: m_assoc subgroup.subset [THEN subsetD])
+apply (erule subst)
+apply (simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD])
+done
+
+lemma (in coset) normal_inv_op_closed2:
+ "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
+apply (drule normal_inv_op_closed1 [of H "(inv x)"])
+apply auto
+done
+
+lemma (in coset) lcos_m_assoc:
+ "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
+ ==> g <# (h <# M) = (g \<otimes> h) <# M"
+by (force simp add: l_coset_eq m_assoc)
+
+lemma (in coset) lcos_mult_one: "M <= carrier G ==> \<one> <# M = M"
+by (force simp add: l_coset_eq)
+
+lemma (in coset) l_coset_subset_G:
+ "[| H <= carrier G; x \<in> carrier G |] ==> x <# H <= carrier G"
+by (auto simp add: l_coset_eq subsetD)
+
+lemma (in coset) l_repr_independence:
+ "[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> x <# H = y <# H"
+apply (auto simp add: l_coset_eq m_assoc
+ subgroup.subset [THEN subsetD] subgroup.m_closed)
+apply (rule_tac x = "mult G (m_inv G h) ha" in bexI)
+ --{*FIXME: locales don't currently work with @{text rule_tac},
+ want @{term "(inv h) \<otimes> ha"}*}
+apply (auto simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD]
+ subgroup.m_inv_closed subgroup.m_closed)
+done
+
+lemma (in coset) setmult_subset_G:
+ "[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G"
+by (auto simp add: set_mult_eq subsetD)
+
+lemma (in coset) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
+apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
+apply (rule_tac x = x in bexI)
+apply (rule bexI [of _ "\<one>"])
+apply (auto simp add: subgroup.m_closed subgroup.one_closed
+ r_one subgroup.subset [THEN subsetD])
+done
+
+
+(* set of inverses of an r_coset *)
+lemma (in coset) rcos_inv:
+ assumes normalHG: "H <| G"
+ and xinG: "x \<in> carrier G"
+ shows "set_inv G (H #> x) = H #> (inv x)"
+proof -
+ have H_subset: "H <= carrier G"
+ by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
+ show ?thesis
+ proof (auto simp add: r_coset_eq image_def set_inv_def)
+ fix h
+ assume "h \<in> H"
+ hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
+ by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
+ thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
+ using prems
+ by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
+ subgroup.m_inv_closed)
+ next
+ fix h
+ assume "h \<in> H"
+ hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h"
+ by (simp add: xinG m_assoc H_subset [THEN subsetD])
+ hence "(\<exists>j\<in>H. j \<otimes> x = inv (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
+ using prems
+ by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
+ blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
+ subgroup.m_inv_closed)
+ thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
+ qed
+qed
+
+(*The old proof is something like this, but the rule_tac calls make
+illegal references to implicit structures.
+lemma (in coset) rcos_inv:
+ "[| H <| G; x \<in> carrier G |] ==> set_inv G (H #> x) = H #> (inv x)"
+apply (frule normal_imp_subgroup)
+apply (auto simp add: r_coset_eq image_def set_inv_def)
+apply (rule_tac x = "(inv x) \<otimes> (inv h) \<otimes> x" in bexI)
+apply (simp add: m_assoc inv_mult_group subgroup.subset [THEN subsetD])
+apply (simp add: subgroup.m_inv_closed, assumption+)
+apply (rule_tac x = "inv (h \<otimes> (inv x)) " in exI)
+apply (simp add: inv_mult_group subgroup.subset [THEN subsetD])
+apply (rule_tac x = "x \<otimes> (inv h) \<otimes> (inv x)" in bexI)
+apply (simp add: m_assoc subgroup.subset [THEN subsetD])
+apply (simp add: normal_inv_op_closed2 subgroup.m_inv_closed)
+done
+*)
+
+lemma (in coset) rcos_inv2:
+ "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)"
+apply (simp add: setrcos_eq, clarify)
+apply (subgoal_tac "x : carrier G")
+ prefer 2
+ apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
+apply (drule repr_independence)
+ apply assumption
+ apply (erule normal_imp_subgroup)
+apply (simp add: rcos_inv)
+done
+
+
+(* some rules for <#> with #> or <# *)
+lemma (in coset) setmult_rcos_assoc:
+ "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
+ ==> H <#> (K #> x) = (H <#> K) #> x"
+apply (auto simp add: rcos_def r_coset_def setmult_def set_mult_def)
+apply (force simp add: m_assoc)+
+done
+
+lemma (in coset) rcos_assoc_lcos:
+ "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
+ ==> (H #> x) <#> K = H <#> (x <# K)"
+apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
+ setmult_def set_mult_def Sigma_def image_def)
+apply (force intro!: exI bexI simp add: m_assoc)+
+done
+
+lemma (in coset) rcos_mult_step1:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
+by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
+ r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
+
+lemma (in coset) rcos_mult_step2:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
+by (simp add: normal_imp_rcos_eq_lcos)
+
+lemma (in coset) rcos_mult_step3:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
+by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
+ setmult_subset_G subgroup_mult_id
+ subgroup.subset normal_imp_subgroup)
+
+lemma (in coset) rcos_sum:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
+by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
+
+(*generalizes subgroup_mult_id*)
+lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
+by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
+ setmult_rcos_assoc subgroup_mult_id)
+
+
+subsection{*Lemmas Leading to Lagrange's Theorem*}
+
+lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
+apply (rule equalityI)
+apply (force simp add: subgroup.subset [THEN subsetD]
+ setrcos_eq r_coset_eq)
+apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
+done
+
+lemma (in coset) cosets_finite:
+ "[| c \<in> rcosets G H; H <= carrier G; finite (carrier G) |] ==> finite c"
+apply (auto simp add: setrcos_eq)
+apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
+done
+
+text{*The next two lemmas support the proof of @{text card_cosets_equal},
+since we can't use @{text rule_tac} with explicit terms for @{term f} and
+@{term g}.*}
+lemma (in coset) inj_on_f:
+ "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
+apply (rule inj_onI)
+apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
+ prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
+apply (simp add: subsetD)
+done
+
+lemma (in coset) inj_on_g:
+ "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H"
+by (force simp add: inj_on_def subsetD)
+
+lemma (in coset) card_cosets_equal:
+ "[| c \<in> rcosets G H; H <= carrier G; finite(carrier G) |]
+ ==> card c = card H"
+apply (auto simp add: setrcos_eq)
+apply (rule card_bij_eq)
+ apply (rule inj_on_f, assumption+)
+ apply (force simp add: m_assoc subsetD r_coset_eq)
+ apply (rule inj_on_g, assumption+)
+ apply (force simp add: m_assoc subsetD r_coset_eq)
+ txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
+ apply (simp add: r_coset_subset_G [THEN finite_subset])
+apply (blast intro: finite_subset)
+done
+
+subsection{*Two distinct right cosets are disjoint*}
+
+lemma (in coset) rcos_equation:
+ "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<otimes> a = h \<otimes> b;
+ h \<in> H; ha \<in> H; hb \<in> H|]
+ ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
+apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
+apply (simp add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
+apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
+done
+
+lemma (in coset) rcos_disjoint:
+ "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
+apply (simp add: setrcos_eq r_coset_eq)
+apply (blast intro: rcos_equation sym)
+done
+
+lemma (in coset) setrcos_subset_PowG:
+ "subgroup H G ==> rcosets G H <= Pow(carrier G)"
+apply (simp add: setrcos_eq)
+apply (blast dest: r_coset_subset_G subgroup.subset)
+done
+
+subsection {*Factorization of a Group*}
+
+constdefs
+ FactGroup :: "[('a,'b) group_scheme, 'a set] => ('a set) group"
+ (infixl "Mod" 60)
+ "FactGroup G H ==
+ (| carrier = rcosets G H,
+ mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
+ one = H,
+ m_inv = (%X: rcosets G H. set_inv G X) |)"
+
+lemma (in coset) setmult_closed:
+ "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
+ ==> K1 <#> K2 \<in> rcosets G H"
+by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
+ rcos_sum setrcos_eq)
+
+(*
+lemma setinv_closed:
+ "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
+by (auto simp add: normal_imp_subgroup
+ subgroup.subset coset.rcos_inv coset.setrcos_eq)
+*)
+
+lemma (in coset) setrcos_assoc:
+ "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
+ ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
+by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
+ subgroup.subset m_assoc)
+
+(*??
+lemma subgroup_in_rcosets: "subgroup H G ==> H \<in> rcosets G H"
+apply (frule subgroup_imp_coset)
+apply (frule subgroup_imp_group)
+apply (simp add: coset.setrcos_eq)
+apply (blast del: equalityI
+ intro!: group.subgroup.one_closed group.one_closed
+ coset.coset_join2 [symmetric])
+done
+*)
+
+lemma (in coset) setrcos_inv_mult_group_eq:
+ "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
+by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
+ subgroup.subset)
+
+(*????????????????
+theorem factorgroup_is_group: "H <| G ==> group (G Mod H)"
+apply (frule normal_imp_coset)
+apply (simp add: FactGroup_def)
+apply (rule group.intro)
+apply (rule magma.intro)
+apply (simp add: );
+ apply (simp add: restrictI coset.setmult_closed)
+ apply (rule semigroup.intro)
+ apply (simp add: restrictI coset.setmult_closed)
+ apply (simp add: coset.setmult_closed coset.setrcos_assoc)
+apply (rule group_axioms.intro)
+ apply (simp add: restrictI setinv_closed)
+ apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
+ apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq)
+apply (simp add: normal_imp_subgroup subgroup_in_rcosets coset.setrcos_mult_eq)
+done
+*)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Exponent.thy Tue Mar 18 18:07:06 2003 +0100
@@ -0,0 +1,351 @@
+(* Title: HOL/GroupTheory/Exponent
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+
+ exponent p s yields the greatest power of p that divides s.
+*)
+
+header{*The Combinatorial Argument Underlying the First Sylow Theorem*}
+
+theory Exponent = Main + Primes:
+
+constdefs
+ exponent :: "[nat, nat] => nat"
+ "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
+
+subsection{*Prime Theorems*}
+
+lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
+by (unfold prime_def, force)
+
+lemma prime_iff:
+ "(p \<in> prime) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
+apply (auto simp add: prime_imp_one_less)
+apply (blast dest!: prime_dvd_mult)
+apply (auto simp add: prime_def)
+apply (erule dvdE)
+apply (case_tac "k=0", simp)
+apply (drule_tac x = m in spec)
+apply (drule_tac x = k in spec)
+apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
+done
+
+lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
+by (force simp add: prime_iff)
+
+
+lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
+apply (rule_tac P = "%x. x <= b * c" in subst)
+apply (rule mult_1_right)
+apply (rule mult_le_mono, auto)
+done
+
+lemma insert_partition:
+ "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|]
+ ==> x \<inter> \<Union> F = {}"
+by auto
+
+(* main cardinality theorem *)
+lemma card_partition [rule_format]:
+ "finite C ==>
+ finite (\<Union> C) -->
+ (\<forall>c\<in>C. card c = k) -->
+ (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
+ k * card(C) = card (\<Union> C)"
+apply (erule finite_induct, simp)
+apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
+ finite_subset [of _ "\<Union> (insert x F)"])
+done
+
+lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
+by (rule ccontr, simp)
+
+
+lemma prime_dvd_cases:
+ "[| p*k dvd m*n; p \<in> prime |]
+ ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
+apply (simp add: prime_iff)
+apply (frule dvd_mult_left)
+apply (subgoal_tac "p dvd m | p dvd n")
+ prefer 2 apply blast
+apply (erule disjE)
+apply (rule disjI1)
+apply (rule_tac [2] disjI2)
+apply (erule_tac n = m in dvdE)
+apply (erule_tac [2] n = n in dvdE, auto)
+apply (rule_tac [2] k = p in dvd_mult_cancel)
+apply (rule_tac k = p in dvd_mult_cancel)
+apply (simp_all add: mult_ac)
+done
+
+
+lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime
+ ==> \<forall>m n. p^c dvd m*n -->
+ (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
+apply (induct_tac "c")
+ apply clarify
+ apply (case_tac "a")
+ apply simp
+ apply simp
+(*inductive step*)
+apply simp
+apply clarify
+apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
+(*case 1: p dvd m*)
+ apply (case_tac "a")
+ apply simp
+ apply clarify
+ apply (drule spec, drule spec, erule (1) notE impE)
+ apply (drule_tac x = nat in spec)
+ apply (drule_tac x = b in spec)
+ apply simp
+ apply (blast intro: dvd_refl mult_dvd_mono)
+(*case 2: p dvd n*)
+apply (case_tac "b")
+ apply simp
+apply clarify
+apply (drule spec, drule spec, erule (1) notE impE)
+apply (drule_tac x = a in spec)
+apply (drule_tac x = nat in spec, simp)
+apply (blast intro: dvd_refl mult_dvd_mono)
+done
+
+(*needed in this form in Sylow.ML*)
+lemma div_combine:
+ "[| p \<in> prime; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |]
+ ==> p ^ a dvd k"
+by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
+
+(*Lemma for power_dvd_bound*)
+lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
+apply (induct_tac "n")
+apply (simp (no_asm_simp))
+apply simp
+apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
+apply (subgoal_tac "2 * p^n <= p * p^n")
+(*?arith_tac should handle all of this!*)
+apply (rule order_trans)
+prefer 2 apply assumption
+apply (drule_tac k = 2 in mult_le_mono2, simp)
+apply (rule mult_le_mono1, simp)
+done
+
+(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
+lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; 0 < a|] ==> n < a"
+apply (drule dvd_imp_le)
+apply (drule_tac [2] n = n in Suc_le_power, auto)
+done
+
+
+subsection{*Exponent Theorems*}
+
+lemma exponent_ge [rule_format]:
+ "[|p^k dvd n; p \<in> prime; 0<n|] ==> k <= exponent p n"
+apply (simp add: exponent_def)
+apply (erule Greatest_le)
+apply (blast dest: prime_imp_one_less power_dvd_bound)
+done
+
+lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
+apply (simp add: exponent_def)
+apply clarify
+apply (rule_tac k = 0 in GreatestI)
+prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
+done
+
+lemma power_Suc_exponent_Not_dvd:
+ "[|(p * p ^ exponent p s) dvd s; p \<in> prime |] ==> s=0"
+apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
+ prefer 2 apply simp
+apply (rule ccontr)
+apply (drule exponent_ge, auto)
+done
+
+lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
+apply (simp (no_asm_simp) add: exponent_def)
+apply (rule Greatest_equality, simp)
+apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
+done
+
+lemma exponent_equalityI:
+ "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
+by (simp (no_asm_simp) add: exponent_def)
+
+lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
+by (simp (no_asm_simp) add: exponent_def)
+
+
+(* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *)
+lemma exponent_mult_add1:
+ "[| 0 < a; 0 < b |]
+ ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
+apply (case_tac "p \<in> prime")
+apply (rule exponent_ge)
+apply (auto simp add: power_add)
+apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
+done
+
+(* exponent_mult_add, opposite inclusion *)
+lemma exponent_mult_add2: "[| 0 < a; 0 < b |]
+ ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
+apply (case_tac "p \<in> prime")
+apply (rule leI, clarify)
+apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
+apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
+apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
+ prefer 3 apply assumption
+ prefer 2 apply simp
+apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
+ apply (assumption, force, simp)
+apply (blast dest: power_Suc_exponent_Not_dvd)
+done
+
+lemma exponent_mult_add:
+ "[| 0 < a; 0 < b |]
+ ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
+by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
+
+
+lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
+apply (case_tac "exponent p n", simp)
+apply (case_tac "n", simp)
+apply (cut_tac s = n and p = p in power_exponent_dvd)
+apply (auto dest: dvd_mult_left)
+done
+
+lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
+apply (case_tac "p \<in> prime")
+apply (auto simp add: prime_iff not_divides_exponent_0)
+done
+
+
+subsection{*Lemmas for the Main Combinatorial Argument*}
+
+lemma p_fac_forw_lemma:
+ "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
+apply (rule notnotD)
+apply (rule notI)
+apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
+apply (drule_tac m = a in less_imp_le)
+apply (drule le_imp_power_dvd)
+apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
+apply (frule_tac m = k in less_imp_le)
+apply (drule_tac c = m in le_extend_mult, assumption)
+apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
+prefer 2 apply assumption
+apply (rule dvd_refl [THEN dvd_mult2])
+apply (drule_tac n = k in dvd_imp_le, auto)
+done
+
+lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]
+ ==> (p^r) dvd (p^a) - k"
+apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
+apply (subgoal_tac "p^r dvd p^a*m")
+ prefer 2 apply (blast intro: dvd_mult2)
+apply (drule dvd_diffD1)
+ apply assumption
+ prefer 2 apply (blast intro: dvd_diff)
+apply (drule less_imp_Suc_add, auto)
+done
+
+
+lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
+by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
+
+lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |]
+ ==> (p^r) dvd (p^a)*m - k"
+apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
+apply (subgoal_tac "p^r dvd p^a*m")
+ prefer 2 apply (blast intro: dvd_mult2)
+apply (drule dvd_diffD1)
+ apply assumption
+ prefer 2 apply (blast intro: dvd_diff)
+apply (drule less_imp_Suc_add, auto)
+done
+
+lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat); k < p^a |]
+ ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
+apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
+done
+
+text{*Suc rules that we have to delete from the simpset*}
+lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
+
+(*The bound K is needed; otherwise it's too weak to be used.*)
+lemma p_not_div_choose_lemma [rule_format]:
+ "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
+ ==> k<K --> exponent p ((j+k) choose k) = 0"
+apply (case_tac "p \<in> prime")
+ prefer 2 apply simp
+apply (induct_tac "k")
+apply (simp (no_asm))
+(*induction step*)
+apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
+ prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
+apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) =
+ exponent p (Suc n)")
+ txt{*First, use the assumed equation. We simplify the LHS to
+ @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"}
+ the common terms cancel, proving the conclusion.*}
+ apply (simp del: bad_Sucs add: exponent_mult_add)
+txt{*Establishing the equation requires first applying
+ @{text Suc_times_binomial_eq} ...*}
+apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
+txt{*...then @{text exponent_mult_add} and the quantified premise.*}
+apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
+done
+
+(*The lemma above, with two changes of variables*)
+lemma p_not_div_choose:
+ "[| k<K; k<=n;
+ \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
+ ==> exponent p (n choose k) = 0"
+apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
+ prefer 3 apply simp
+ prefer 2 apply assumption
+apply (drule_tac x = "K - Suc i" in spec)
+apply (simp add: Suc_diff_le)
+done
+
+
+lemma const_p_fac_right:
+ "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
+apply (case_tac "p \<in> prime")
+ prefer 2 apply simp
+apply (frule_tac a = a in zero_less_prime_power)
+apply (rule_tac K = "p^a" in p_not_div_choose)
+ apply simp
+ apply simp
+ apply (case_tac "m")
+ apply (case_tac [2] "p^a")
+ apply auto
+(*now the hard case, simplified to
+ exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
+apply (subgoal_tac "0<p")
+ prefer 2 apply (force dest!: prime_imp_one_less)
+apply (subst exponent_p_a_m_k_equation, auto)
+done
+
+lemma const_p_fac:
+ "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
+apply (case_tac "p \<in> prime")
+ prefer 2 apply simp
+apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
+ prefer 2 apply (force simp add: prime_iff)
+txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
+ insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
+ first
+ transform the binomial coefficient, then use @{text exponent_mult_add}.*}
+apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
+ a + exponent p m")
+ apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff)
+txt{*one subgoal left!*}
+apply (subst times_binomial_minus1_eq, simp, simp)
+apply (subst exponent_mult_add, simp)
+apply (simp (no_asm_simp) add: zero_less_binomial_iff)
+apply arith
+apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
+done
+
+
+end
--- a/src/HOL/Algebra/ROOT.ML Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/Algebra/ROOT.ML Tue Mar 18 18:07:06 2003 +0100
@@ -6,3 +6,4 @@
with_path "abstract" time_use_thy "Abstract"; (*The ring theory*)
with_path "poly" time_use_thy "Polynomial"; (*The full theory*)
+use_thy "Sylow";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Sylow.thy Tue Mar 18 18:07:06 2003 +0100
@@ -0,0 +1,395 @@
+(* Title: HOL/GroupTheory/Sylow
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+
+See Florian Kamm\"uller and L. C. Paulson,
+ A Formal Proof of Sylow's theorem:
+ An Experiment in Abstract Algebra with Isabelle HOL
+ J. Automated Reasoning 23 (1999), 235-264
+*)
+
+header{*Sylow's theorem using locales*}
+
+theory Sylow = Coset:
+
+subsection {*Order of a Group and Lagrange's Theorem*}
+
+constdefs
+ order :: "(('a,'b) semigroup_scheme) => nat"
+ "order(S) == card(carrier S)"
+
+theorem (in coset) lagrange:
+ "[| finite(carrier G); subgroup H G |]
+ ==> card(rcosets G H) * card(H) = order(G)"
+apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
+apply (subst mult_commute)
+apply (rule card_partition)
+ apply (simp add: setrcos_subset_PowG [THEN finite_subset])
+ apply (simp add: setrcos_part_G)
+ apply (simp add: card_cosets_equal subgroup.subset)
+apply (simp add: rcos_disjoint)
+done
+
+
+text{*The combinatorial argument is in theory Exponent*}
+
+locale sylow = coset +
+ fixes p and a and m and calM and RelM
+ assumes prime_p: "p \<in> prime"
+ and order_G: "order(G) = (p^a) * m"
+ and finite_G [iff]: "finite (carrier G)"
+ defines "calM == {s. s <= carrier(G) & card(s) = p^a}"
+ and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
+ (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
+
+lemma (in sylow) RelM_refl: "refl calM RelM"
+apply (auto simp add: refl_def RelM_def calM_def)
+apply (blast intro!: coset_mult_one [symmetric])
+done
+
+lemma (in sylow) RelM_sym: "sym RelM"
+proof (unfold sym_def RelM_def, clarify)
+ fix y g
+ assume "y \<in> calM"
+ and g: "g \<in> carrier G"
+ hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def)
+ thus "\<exists>g'\<in>carrier G. y = y #> g #> g'"
+ by (blast intro: g inv_closed)
+qed
+
+lemma (in sylow) RelM_trans: "trans RelM"
+by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
+
+lemma (in sylow) RelM_equiv: "equiv calM RelM"
+apply (unfold equiv_def)
+apply (blast intro: RelM_refl RelM_sym RelM_trans)
+done
+
+lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM ==> M' <= calM"
+apply (unfold RelM_def)
+apply (blast elim!: quotientE)
+done
+
+subsection{*Main Part of the Proof*}
+
+
+locale sylow_central = sylow +
+ fixes H and M1 and M
+ assumes M_in_quot: "M \<in> calM // RelM"
+ and not_dvd_M: "~(p ^ Suc(exponent p m) dvd card(M))"
+ and M1_in_M: "M1 \<in> M"
+ defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
+
+lemma (in sylow_central) M_subset_calM: "M <= calM"
+by (rule M_in_quot [THEN M_subset_calM_prep])
+
+lemma (in sylow_central) card_M1: "card(M1) = p^a"
+apply (cut_tac M_subset_calM M1_in_M)
+apply (simp add: calM_def, blast)
+done
+
+lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
+by force
+
+lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
+apply (subgoal_tac "0 < card M1")
+ apply (blast dest: card_nonempty)
+apply (cut_tac prime_p [THEN prime_imp_one_less])
+apply (simp (no_asm_simp) add: card_M1)
+done
+
+lemma (in sylow_central) M1_subset_G [simp]: "M1 <= carrier G"
+apply (rule subsetD [THEN PowD])
+apply (rule_tac [2] M1_in_M)
+apply (rule M_subset_calM [THEN subset_trans])
+apply (auto simp add: calM_def)
+done
+
+lemma (in sylow_central) M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
+ proof -
+ from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
+ have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
+ show ?thesis
+ proof
+ show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
+ by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
+ show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
+ proof (rule restrictI)
+ fix z assume zH: "z \<in> H"
+ show "m1 \<otimes> z \<in> M1"
+ proof -
+ from zH
+ have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
+ by (auto simp add: H_def)
+ show ?thesis
+ by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
+ qed
+ qed
+ qed
+ qed
+
+
+subsection{*Discharging the Assumptions of @{text sylow_central}*}
+
+lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
+by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
+
+lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
+apply (subgoal_tac "M \<noteq> {}")
+ apply blast
+apply (cut_tac EmptyNotInEquivSet, blast)
+done
+
+lemma (in sylow) zero_less_o_G: "0 < order(G)"
+apply (unfold order_def)
+apply (blast intro: one_closed zero_less_card_empty)
+done
+
+lemma (in sylow) zero_less_m: "0 < m"
+apply (cut_tac zero_less_o_G)
+apply (simp add: order_G)
+done
+
+lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
+by (simp add: calM_def n_subsets order_G [symmetric] order_def)
+
+lemma (in sylow) zero_less_card_calM: "0 < card calM"
+by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
+
+lemma (in sylow) max_p_div_calM:
+ "~ (p ^ Suc(exponent p m) dvd card(calM))"
+apply (subgoal_tac "exponent p m = exponent p (card calM) ")
+ apply (cut_tac zero_less_card_calM prime_p)
+ apply (force dest: power_Suc_exponent_Not_dvd)
+apply (simp add: card_calM zero_less_m [THEN const_p_fac])
+done
+
+lemma (in sylow) finite_calM: "finite calM"
+apply (unfold calM_def)
+apply (rule_tac B = "Pow (carrier G) " in finite_subset)
+apply auto
+done
+
+lemma (in sylow) lemma_A1:
+ "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))"
+apply (rule max_p_div_calM [THEN contrapos_np])
+apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv])
+done
+
+
+subsubsection{*Introduction and Destruct Rules for @{term H}*}
+
+lemma (in sylow_central) H_I: "[|g \<in> carrier G; M1 #> g = M1|] ==> g \<in> H"
+by (simp add: H_def)
+
+lemma (in sylow_central) H_into_carrier_G: "x \<in> H ==> x \<in> carrier G"
+by (simp add: H_def)
+
+lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1"
+by (simp add: H_def)
+
+lemma (in sylow_central) H_m_closed: "[| x\<in>H; y\<in>H|] ==> x \<otimes> y \<in> H"
+apply (unfold H_def)
+apply (simp add: coset_mult_assoc [symmetric] m_closed)
+done
+
+lemma (in sylow_central) H_not_empty: "H \<noteq> {}"
+apply (simp add: H_def)
+apply (rule exI [of _ \<one>], simp)
+done
+
+lemma (in sylow_central) H_is_subgroup: "subgroup H G"
+apply (rule subgroupI)
+apply (rule subsetI)
+apply (erule H_into_carrier_G)
+apply (rule H_not_empty)
+apply (simp add: H_def, clarify)
+apply (erule_tac P = "%z. ?lhs(z) = M1" in subst)
+apply (simp add: coset_mult_assoc )
+apply (blast intro: H_m_closed)
+done
+
+
+lemma (in sylow_central) rcosetGM1g_subset_G:
+ "[| g \<in> carrier G; x \<in> M1 #> g |] ==> x \<in> carrier G"
+by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
+
+lemma (in sylow_central) finite_M1: "finite M1"
+by (rule finite_subset [OF M1_subset_G finite_G])
+
+lemma (in sylow_central) finite_rcosetGM1g: "g\<in>carrier G ==> finite (M1 #> g)"
+apply (rule finite_subset)
+apply (rule subsetI)
+apply (erule rcosetGM1g_subset_G, assumption)
+apply (rule finite_G)
+done
+
+lemma (in sylow_central) M1_cardeq_rcosetGM1g:
+ "g \<in> carrier G ==> card(M1 #> g) = card(M1)"
+by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal setrcosI)
+
+lemma (in sylow_central) M1_RelM_rcosetGM1g:
+ "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
+apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G)
+apply (rule conjI)
+ apply (blast intro: rcosetGM1g_subset_G)
+apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g)
+apply (rule bexI [of _ "inv g"])
+apply (simp_all add: coset_mult_assoc M1_subset_G)
+done
+
+
+
+subsection{*Equal Cardinalities of @{term M} and @{term "rcosets G H"}*}
+
+text{*Injections between @{term M} and @{term "rcosets G H"} show that
+ their cardinalities are equal.*}
+
+lemma ElemClassEquiv:
+ "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
+apply (unfold equiv_def quotient_def sym_def trans_def, blast)
+done
+
+lemma (in sylow_central) M_elem_map:
+ "M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2"
+apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]])
+apply (simp add: RelM_def)
+apply (blast dest!: bspec)
+done
+
+lemmas (in sylow_central) M_elem_map_carrier =
+ M_elem_map [THEN someI_ex, THEN conjunct1]
+
+lemmas (in sylow_central) M_elem_map_eq =
+ M_elem_map [THEN someI_ex, THEN conjunct2]
+
+lemma (in sylow_central) M_funcset_setrcos_H:
+ "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
+apply (rule setrcosI [THEN restrictI])
+apply (rule H_is_subgroup [THEN subgroup.subset])
+apply (erule M_elem_map_carrier)
+done
+
+lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets G H. inj_on f M"
+apply (rule bexI)
+apply (rule_tac [2] M_funcset_setrcos_H)
+apply (rule inj_onI, simp)
+apply (rule trans [OF _ M_elem_map_eq])
+prefer 2 apply assumption
+apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
+apply (rule coset_mult_inv1)
+apply (erule_tac [2] M_elem_map_carrier)+
+apply (rule_tac [2] M1_subset_G)
+apply (rule coset_join1 [THEN in_H_imp_eq])
+apply (rule_tac [3] H_is_subgroup)
+prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
+apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def)
+done
+
+
+(** the opposite injection **)
+
+lemma (in sylow_central) H_elem_map:
+ "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
+by (auto simp add: setrcos_eq)
+
+lemmas (in sylow_central) H_elem_map_carrier =
+ H_elem_map [THEN someI_ex, THEN conjunct1]
+
+lemmas (in sylow_central) H_elem_map_eq =
+ H_elem_map [THEN someI_ex, THEN conjunct2]
+
+
+lemma EquivElemClass:
+ "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
+apply (unfold equiv_def quotient_def sym_def trans_def, blast)
+done
+
+lemma (in sylow_central) setrcos_H_funcset_M:
+ "(\<lambda>C \<in> rcosets G H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C))
+ \<in> rcosets G H \<rightarrow> M"
+apply (simp add: setrcos_eq)
+apply (fast intro: someI2
+ intro!: restrictI M1_in_M
+ EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
+done
+
+text{*close to a duplicate of @{text inj_M_GmodH}*}
+lemma (in sylow_central) inj_GmodH_M:
+ "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)"
+apply (rule bexI)
+apply (rule_tac [2] setrcos_H_funcset_M)
+apply (rule inj_onI)
+apply (simp)
+apply (rule trans [OF _ H_elem_map_eq])
+prefer 2 apply assumption
+apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
+apply (rule coset_mult_inv1)
+apply (erule_tac [2] H_elem_map_carrier)+
+apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
+apply (rule coset_join2)
+apply (blast intro: m_closed inv_closed H_elem_map_carrier)
+apply (rule H_is_subgroup)
+apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier)
+done
+
+lemma (in sylow_central) calM_subset_PowG: "calM <= Pow(carrier G)"
+by (auto simp add: calM_def)
+
+
+lemma (in sylow_central) finite_M: "finite M"
+apply (rule finite_subset)
+apply (rule M_subset_calM [THEN subset_trans])
+apply (rule calM_subset_PowG, blast)
+done
+
+lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
+apply (insert inj_M_GmodH inj_GmodH_M)
+apply (blast intro: card_bij finite_M H_is_subgroup
+ setrcos_subset_PowG [THEN finite_subset]
+ finite_Pow_iff [THEN iffD2])
+done
+
+lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)"
+by (simp add: cardMeqIndexH lagrange H_is_subgroup)
+
+lemma (in sylow_central) lemma_leq1: "p^a <= card(H)"
+apply (rule dvd_imp_le)
+ apply (rule div_combine [OF prime_p not_dvd_M])
+ prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
+apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd
+ zero_less_m)
+done
+
+lemma (in sylow_central) lemma_leq2: "card(H) <= p^a"
+apply (subst card_M1 [symmetric])
+apply (cut_tac M1_inj_H)
+apply (blast intro!: M1_subset_G intro:
+ card_inj H_into_carrier_G finite_subset [OF _ finite_G])
+done
+
+lemma (in sylow_central) card_H_eq: "card(H) = p^a"
+by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
+
+lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
+apply (cut_tac lemma_A1, clarify)
+apply (frule existsM1inM, clarify)
+apply (subgoal_tac "sylow_central G p a m M1 M")
+ apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
+apply (simp add: sylow_central_def sylow_central_axioms_def prems)
+done
+
+text{*Needed because the locale's automatic definition refers to
+ @{term "semigroup G"} and @{term "group_axioms G"} rather than
+ simply to @{term "group G"}.*}
+lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
+by (simp add: sylow_def group_def)
+
+theorem sylow_thm:
+ "[|p \<in> prime; group(G); order(G) = (p^a) * m; finite (carrier G)|]
+ ==> \<exists>H. subgroup H G & card(H) = p^a"
+apply (rule sylow.sylow_thm [of G p a m])
+apply (simp add: sylow_eq sylow_axioms_def)
+done
+
+end
--- a/src/HOL/GroupTheory/Coset.thy Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,462 +0,0 @@
-(* Title: HOL/GroupTheory/Coset
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
-*)
-
-header{*Theory of Cosets*}
-
-theory Coset = Group + Exponent:
-
-constdefs
- r_coset :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"
- "r_coset G H a == (% x. (sum G) x a) ` H"
-
- l_coset :: "[('a,'b) group_scheme, 'a, 'a set] => 'a set"
- "l_coset G a H == (% x. (sum G) a x) ` H"
-
- rcosets :: "[('a,'b) group_scheme,'a set] => ('a set)set"
- "rcosets G H == r_coset G H ` (carrier G)"
-
- set_sum :: "[('a,'b) group_scheme,'a set,'a set] => 'a set"
- "set_sum G H K == (%(x,y). (sum G) x y) ` (H \<times> K)"
-
- set_minus :: "[('a,'b) group_scheme,'a set] => 'a set"
- "set_minus G H == (gminus G) ` H"
-
- normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "<|" 60)
- "normal H G == subgroup H G &
- (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
-
-syntax (xsymbols)
- normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "\<lhd>" 60)
-
-locale coset = group G +
- fixes rcos :: "['a set, 'a] => 'a set" (infixl "#>" 60)
- and lcos :: "['a, 'a set] => 'a set" (infixl "<#" 60)
- and setsum :: "['a set, 'a set] => 'a set" (infixl "<#>" 60)
- defines rcos_def: "H #> x == r_coset G H x"
- and lcos_def: "x <# H == l_coset G x H"
- and setsum_def: "H <#> K == set_sum G H K"
-
-
-text{*Lemmas useful for Sylow's Theorem*}
-
-lemma card_inj:
- "[|f \<in> A\<rightarrow>B; inj_on f A; finite A; finite B|] ==> card(A) <= card(B)"
-apply (rule card_inj_on_le)
-apply (auto simp add: Pi_def)
-done
-
-lemma card_bij:
- "[|f \<in> A\<rightarrow>B; inj_on f A;
- g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
-by (blast intro: card_inj order_antisym)
-
-
-subsection{*Lemmas Using Locale Constants*}
-
-lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<oplus> a = b}"
-by (auto simp add: rcos_def r_coset_def sum_def)
-
-lemma (in coset) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<oplus> h = b}"
-by (auto simp add: lcos_def l_coset_def sum_def)
-
-lemma (in coset) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
-by (auto simp add: rcosets_def rcos_def sum_def)
-
-lemma (in coset) set_sum_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<oplus> k}"
-by (simp add: setsum_def set_sum_def sum_def image_def)
-
-lemma (in coset) coset_sum_assoc:
- "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
- ==> (M #> g) #> h = M #> (g \<oplus> h)"
-by (force simp add: r_coset_eq sum_assoc)
-
-lemma (in coset) coset_sum_zero [simp]: "M <= carrier G ==> M #> \<zero> = M"
-by (force simp add: r_coset_eq)
-
-lemma (in coset) coset_sum_minus1:
- "[| M #> (x \<oplus> (\<ominus>y)) = M; x \<in> carrier G ; y \<in> carrier G;
- M <= carrier G |] ==> M #> x = M #> y"
-apply (erule subst [of concl: "%z. M #> x = z #> y"])
-apply (simp add: coset_sum_assoc sum_assoc)
-done
-
-lemma (in coset) coset_sum_minus2:
- "[| M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M <= carrier G |]
- ==> M #> (x \<oplus> (\<ominus>y)) = M "
-apply (simp add: coset_sum_assoc [symmetric])
-apply (simp add: coset_sum_assoc)
-done
-
-lemma (in coset) coset_join1:
- "[| H #> x = H; x \<in> carrier G; subgroup H G |] ==> x\<in>H"
-apply (erule subst)
-apply (simp add: r_coset_eq)
-apply (blast intro: left_zero subgroup_zero_closed)
-done
-
-text{*Locales don't currently work with @{text rule_tac}, so we
-must prove this lemma separately.*}
-lemma (in coset) solve_equation:
- "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<oplus> x = y"
-apply (rule bexI [of _ "y \<oplus> (\<ominus>x)"])
-apply (auto simp add: subgroup_sum_closed subgroup_minus_closed sum_assoc
- subgroup_imp_subset [THEN subsetD])
-done
-
-lemma (in coset) coset_join2:
- "[| x \<in> carrier G; subgroup H G; x\<in>H |] ==> H #> x = H"
-by (force simp add: subgroup_sum_closed r_coset_eq solve_equation)
-
-lemma (in coset) r_coset_subset_G:
- "[| H <= carrier G; x \<in> carrier G |] ==> H #> x <= carrier G"
-by (auto simp add: r_coset_eq)
-
-lemma (in coset) rcosI:
- "[| h \<in> H; H <= carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H #> x"
-by (auto simp add: r_coset_eq)
-
-lemma (in coset) setrcosI:
- "[| H <= carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
-by (auto simp add: setrcos_eq)
-
-
-text{*Really needed?*}
-lemma (in coset) transpose_minus:
- "[| x \<oplus> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
- ==> (\<ominus>x) \<oplus> z = y"
-by (force simp add: sum_assoc [symmetric])
-
-lemma (in coset) repr_independence:
- "[| y \<in> H #> x; x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
-by (auto simp add: r_coset_eq sum_assoc [symmetric] right_cancellation_iff
- subgroup_imp_subset [THEN subsetD]
- subgroup_sum_closed solve_equation)
-
-lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
-apply (simp add: r_coset_eq)
-apply (blast intro: left_zero subgroup_imp_subset [THEN subsetD]
- subgroup_zero_closed)
-done
-
-
-subsection{*normal subgroups*}
-
-text{*Allows use of theorems proved in the locale coset*}
-lemma subgroup_imp_coset: "subgroup H G ==> coset G"
-apply (drule subgroup_imp_group)
-apply (simp add: group_def coset_def)
-done
-
-lemma normal_imp_subgroup: "H <| G ==> subgroup H G"
-by (simp add: normal_def)
-
-lemmas normal_imp_group = normal_imp_subgroup [THEN subgroup_imp_group]
-lemmas normal_imp_coset = normal_imp_subgroup [THEN subgroup_imp_coset]
-
-lemma (in coset) normal_iff:
- "(H <| G) = (subgroup H G & (\<forall>x \<in> carrier G. H #> x = x <# H))"
-by (simp add: lcos_def rcos_def normal_def)
-
-lemma (in coset) normal_imp_rcos_eq_lcos:
- "[| H <| G; x \<in> carrier G |] ==> H #> x = x <# H"
-by (simp add: lcos_def rcos_def normal_def)
-
-lemma (in coset) normal_minus_op_closed1:
- "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus>x) \<oplus> h \<oplus> x \<in> H"
-apply (auto simp add: l_coset_eq r_coset_eq normal_iff)
-apply (drule bspec, assumption)
-apply (drule equalityD1 [THEN subsetD], blast, clarify)
-apply (simp add: sum_assoc subgroup_imp_subset [THEN subsetD])
-apply (erule subst)
-apply (simp add: sum_assoc [symmetric] subgroup_imp_subset [THEN subsetD])
-done
-
-lemma (in coset) normal_minus_op_closed2:
- "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus>x) \<in> H"
-apply (drule normal_minus_op_closed1 [of H "(\<ominus>x)"])
-apply auto
-done
-
-lemma (in coset) lcos_sum_assoc:
- "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
- ==> g <# (h <# M) = (g \<oplus> h) <# M"
-by (force simp add: l_coset_eq sum_assoc)
-
-lemma (in coset) lcos_sum_zero: "M <= carrier G ==> \<zero> <# M = M"
-by (force simp add: l_coset_eq)
-
-lemma (in coset) l_coset_subset_G:
- "[| H <= carrier G; x \<in> carrier G |] ==> x <# H <= carrier G"
-by (auto simp add: l_coset_eq subsetD)
-
-lemma (in coset) l_repr_independence:
- "[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> x <# H = y <# H"
-apply (auto simp add: l_coset_eq sum_assoc
- subgroup_imp_subset [THEN subsetD] subgroup_sum_closed)
-apply (rule_tac x = "sum G (gminus G h) ha" in bexI)
- --{*FIXME: locales don't currently work with @{text rule_tac},
- want @{term "(\<ominus>h) \<oplus> ha"}*}
-apply (auto simp add: sum_assoc [symmetric] subgroup_imp_subset [THEN subsetD]
- subgroup_minus_closed subgroup_sum_closed)
-done
-
-lemma (in coset) setsum_subset_G:
- "[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G"
-by (auto simp add: set_sum_eq subsetD)
-
-lemma (in coset) subgroup_sum_id: "subgroup H G ==> H <#> H = H"
-apply (auto simp add: subgroup_sum_closed set_sum_eq Sigma_def image_def)
-apply (rule_tac x = x in bexI)
-apply (rule bexI [of _ "\<zero>"])
-apply (auto simp add: subgroup_sum_closed subgroup_zero_closed
- right_zero subgroup_imp_subset [THEN subsetD])
-done
-
-
-(* set of inverses of an r_coset *)
-lemma (in coset) rcos_minus:
- assumes normalHG: "H <| G"
- and xinG: "x \<in> carrier G"
- shows "set_minus G (H #> x) = H #> (\<ominus>x)"
-proof -
- have H_subset: "H <= carrier G"
- by (rule subgroup_imp_subset [OF normal_imp_subgroup, OF normalHG])
- show ?thesis
- proof (auto simp add: r_coset_eq image_def set_minus_def)
- fix h
- assume "h \<in> H"
- hence "((\<ominus>x) \<oplus> (\<ominus>h) \<oplus> x) \<oplus> \<ominus>x = \<ominus>(h \<oplus> x)"
- by (simp add: xinG sum_assoc minus_sum H_subset [THEN subsetD])
- thus "\<exists>j\<in>H. j \<oplus> \<ominus>x = \<ominus>(h \<oplus> x)"
- using prems
- by (blast intro: normal_minus_op_closed1 normal_imp_subgroup
- subgroup_minus_closed)
- next
- fix h
- assume "h \<in> H"
- hence eq: "(x \<oplus> (\<ominus>h) \<oplus> (\<ominus>x)) \<oplus> x = x \<oplus> \<ominus>h"
- by (simp add: xinG sum_assoc H_subset [THEN subsetD])
- hence "(\<exists>j\<in>H. j \<oplus> x = \<ominus> (h \<oplus> (\<ominus>x))) \<and> h \<oplus> \<ominus>x = \<ominus>(\<ominus>(h \<oplus> (\<ominus>x)))"
- using prems
- by (simp add: sum_assoc minus_sum H_subset [THEN subsetD],
- blast intro: eq normal_minus_op_closed2 normal_imp_subgroup
- subgroup_minus_closed)
- thus "\<exists>y. (\<exists>h\<in>H. h \<oplus> x = y) \<and> h \<oplus> \<ominus>x = \<ominus>y" ..
- qed
-qed
-
-(*The old proof is something like this, but the rule_tac calls make
-illegal references to implicit structures.
-lemma (in coset) rcos_minus:
- "[| H <| G; x \<in> carrier G |] ==> set_minus G (H #> x) = H #> (\<ominus>x)"
-apply (frule normal_imp_subgroup)
-apply (auto simp add: r_coset_eq image_def set_minus_def)
-apply (rule_tac x = "(\<ominus>x) \<oplus> (\<ominus>h) \<oplus> x" in bexI)
-apply (simp add: sum_assoc minus_sum subgroup_imp_subset [THEN subsetD])
-apply (simp add: subgroup_minus_closed, assumption+)
-apply (rule_tac x = "\<ominus> (h \<oplus> (\<ominus>x)) " in exI)
-apply (simp add: minus_sum subgroup_imp_subset [THEN subsetD])
-apply (rule_tac x = "x \<oplus> (\<ominus>h) \<oplus> (\<ominus>x)" in bexI)
-apply (simp add: sum_assoc subgroup_imp_subset [THEN subsetD])
-apply (simp add: normal_minus_op_closed2 subgroup_minus_closed)
-done
-*)
-
-lemma (in coset) rcos_minus2:
- "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_minus G K = H #> (\<ominus>x)"
-apply (simp add: setrcos_eq, clarify)
-apply (subgoal_tac "x : carrier G")
- prefer 2
- apply (blast dest: r_coset_subset_G subgroup_imp_subset normal_imp_subgroup)
-apply (drule repr_independence)
- apply assumption
- apply (erule normal_imp_subgroup)
-apply (simp add: rcos_minus)
-done
-
-
-(* some rules for <#> with #> or <# *)
-lemma (in coset) setsum_rcos_assoc:
- "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
- ==> H <#> (K #> x) = (H <#> K) #> x"
-apply (auto simp add: rcos_def r_coset_def setsum_def set_sum_def)
-apply (force simp add: sum_assoc)+
-done
-
-lemma (in coset) rcos_assoc_lcos:
- "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
- ==> (H #> x) <#> K = H <#> (x <# K)"
-apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
- setsum_def set_sum_def Sigma_def image_def)
-apply (force intro!: exI bexI simp add: sum_assoc)+
-done
-
-lemma (in coset) rcos_sum_step1:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
-by (simp add: setsum_rcos_assoc normal_imp_subgroup [THEN subgroup_imp_subset]
- r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
-
-lemma (in coset) rcos_sum_step2:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
-by (simp add: normal_imp_rcos_eq_lcos)
-
-lemma (in coset) rcos_sum_step3:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H <#> (H #> x)) #> y = H #> (x \<oplus> y)"
-by (simp add: setsum_rcos_assoc r_coset_subset_G coset_sum_assoc
- setsum_subset_G subgroup_sum_id
- subgroup_imp_subset normal_imp_subgroup)
-
-lemma (in coset) rcos_sum:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H #> x) <#> (H #> y) = H #> (x \<oplus> y)"
-by (simp add: rcos_sum_step1 rcos_sum_step2 rcos_sum_step3)
-
-(*generalizes subgroup_sum_id*)
-lemma (in coset) setrcos_sum_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
-by (auto simp add: setrcos_eq normal_imp_subgroup subgroup_imp_subset
- setsum_rcos_assoc subgroup_sum_id)
-
-
-subsection{*Lemmas Leading to Lagrange's Theorem*}
-
-lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
-apply (rule equalityI)
-apply (force simp add: subgroup_imp_subset [THEN subsetD]
- setrcos_eq r_coset_eq)
-apply (auto simp add: setrcos_eq subgroup_imp_subset rcos_self)
-done
-
-lemma (in coset) cosets_finite:
- "[| c \<in> rcosets G H; H <= carrier G; finite (carrier G) |] ==> finite c"
-apply (auto simp add: setrcos_eq)
-apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
-done
-
-text{*The next two lemmas support the proof of @{text card_cosets_equal},
-since we can't use @{text rule_tac} with explicit terms for @{term f} and
-@{term g}.*}
-lemma (in coset) inj_on_f:
- "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> \<ominus>a) (H #> a)"
-apply (rule inj_onI)
-apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
- prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
-apply (simp add: subsetD)
-done
-
-lemma (in coset) inj_on_g:
- "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> a) H"
-by (force simp add: inj_on_def subsetD)
-
-lemma (in coset) card_cosets_equal:
- "[| c \<in> rcosets G H; H <= carrier G; finite(carrier G) |]
- ==> card c = card H"
-apply (auto simp add: setrcos_eq)
-apply (rule card_bij_eq)
- apply (rule inj_on_f, assumption+)
- apply (force simp add: sum_assoc subsetD r_coset_eq)
- apply (rule inj_on_g, assumption+)
- apply (force simp add: sum_assoc subsetD r_coset_eq)
- txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
- apply (simp add: r_coset_subset_G [THEN finite_subset])
-apply (blast intro: finite_subset)
-done
-
-subsection{*Two distinct right cosets are disjoint*}
-
-lemma (in coset) rcos_equation:
- "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<oplus> a = h \<oplus> b;
- h \<in> H; ha \<in> H; hb \<in> H|]
- ==> \<exists>h\<in>H. h \<oplus> b = hb \<oplus> a"
-apply (rule bexI [of _"hb \<oplus> ((\<ominus>ha) \<oplus> h)"])
-apply (simp add: sum_assoc transpose_minus subgroup_imp_subset [THEN subsetD])
-apply (simp add: subgroup_sum_closed subgroup_minus_closed)
-done
-
-lemma (in coset) rcos_disjoint:
- "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
-apply (simp add: setrcos_eq r_coset_eq)
-apply (blast intro: rcos_equation sym)
-done
-
-lemma (in coset) setrcos_subset_PowG:
- "subgroup H G ==> rcosets G H <= Pow(carrier G)"
-apply (simp add: setrcos_eq)
-apply (blast dest: r_coset_subset_G subgroup_imp_subset)
-done
-
-theorem (in coset) lagrange:
- "[| finite(carrier G); subgroup H G |]
- ==> card(rcosets G H) * card(H) = order(G)"
-apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
-apply (subst mult_commute)
-apply (rule card_partition)
- apply (simp add: setrcos_subset_PowG [THEN finite_subset])
- apply (simp add: setrcos_part_G)
- apply (simp add: card_cosets_equal subgroup_def)
-apply (simp add: rcos_disjoint)
-done
-
-
-subsection {*Factorization of a Group*}
-
-constdefs
- FactGroup :: "[('a,'b) group_scheme, 'a set] => ('a set) group"
- (infixl "Mod" 60)
- "FactGroup G H ==
- (| carrier = rcosets G H,
- sum = (%X: rcosets G H. %Y: rcosets G H. set_sum G X Y),
- gminus = (%X: rcosets G H. set_minus G X),
- zero = H |)"
-
-lemma (in coset) setsum_closed:
- "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
- ==> K1 <#> K2 \<in> rcosets G H"
-by (auto simp add: normal_imp_subgroup [THEN subgroup_imp_subset]
- rcos_sum setrcos_eq)
-
-lemma setminus_closed:
- "[| H <| G; K \<in> rcosets G H |] ==> set_minus G K \<in> rcosets G H"
-by (auto simp add: normal_imp_coset normal_imp_group normal_imp_subgroup
- subgroup_imp_subset coset.rcos_minus coset.setrcos_eq)
-
-lemma (in coset) setrcos_assoc:
- "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
- ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
-by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
- subgroup_imp_subset sum_assoc)
-
-lemma subgroup_in_rcosets: "subgroup H G ==> H \<in> rcosets G H"
-apply (frule subgroup_imp_coset)
-apply (frule subgroup_imp_group)
-apply (simp add: coset.setrcos_eq)
-apply (blast del: equalityI
- intro!: group.subgroup_zero_closed group.zero_closed
- coset.coset_join2 [symmetric])
-done
-
-lemma (in coset) setrcos_minus_sum_eq:
- "[|H <| G; M \<in> rcosets G H|] ==> set_minus G M <#> M = H"
-by (auto simp add: setrcos_eq rcos_minus rcos_sum normal_imp_subgroup
- subgroup_imp_subset)
-
-theorem factorgroup_is_group: "H <| G ==> (G Mod H) \<in> Group"
-apply (frule normal_imp_coset)
-apply (simp add: FactGroup_def)
-apply (rule group.intro)
- apply (rule semigroup.intro)
- apply (simp add: restrictI coset.setsum_closed)
- apply (simp add: coset.setsum_closed coset.setrcos_assoc)
-apply (rule group_axioms.intro)
- apply (simp add: restrictI setminus_closed)
- apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
- apply (simp add: setminus_closed coset.setrcos_minus_sum_eq)
-apply (simp add: normal_imp_subgroup subgroup_in_rcosets coset.setrcos_sum_eq)
-done
-
-
-end
--- a/src/HOL/GroupTheory/Exponent.thy Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-(* Title: HOL/GroupTheory/Exponent
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
-
- exponent p s yields the greatest power of p that divides s.
-*)
-
-header{*The Combinatorial Argument Underlying the First Sylow Theorem*}
-
-theory Exponent = Main + Primes:
-
-constdefs
- exponent :: "[nat, nat] => nat"
- "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
-
-subsection{*Prime Theorems*}
-
-lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
-by (unfold prime_def, force)
-
-lemma prime_iff:
- "(p \<in> prime) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
-apply (auto simp add: prime_imp_one_less)
-apply (blast dest!: prime_dvd_mult)
-apply (auto simp add: prime_def)
-apply (erule dvdE)
-apply (case_tac "k=0", simp)
-apply (drule_tac x = m in spec)
-apply (drule_tac x = k in spec)
-apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
-done
-
-lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
-by (force simp add: prime_iff)
-
-
-lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
-apply (rule_tac P = "%x. x <= b * c" in subst)
-apply (rule mult_1_right)
-apply (rule mult_le_mono, auto)
-done
-
-lemma insert_partition:
- "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|]
- ==> x \<inter> \<Union> F = {}"
-by auto
-
-(* main cardinality theorem *)
-lemma card_partition [rule_format]:
- "finite C ==>
- finite (\<Union> C) -->
- (\<forall>c\<in>C. card c = k) -->
- (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
- k * card(C) = card (\<Union> C)"
-apply (erule finite_induct, simp)
-apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
- finite_subset [of _ "\<Union> (insert x F)"])
-done
-
-lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
-by (rule ccontr, simp)
-
-
-lemma prime_dvd_cases:
- "[| p*k dvd m*n; p \<in> prime |]
- ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
-apply (simp add: prime_iff)
-apply (frule dvd_mult_left)
-apply (subgoal_tac "p dvd m | p dvd n")
- prefer 2 apply blast
-apply (erule disjE)
-apply (rule disjI1)
-apply (rule_tac [2] disjI2)
-apply (erule_tac n = m in dvdE)
-apply (erule_tac [2] n = n in dvdE, auto)
-apply (rule_tac [2] k = p in dvd_mult_cancel)
-apply (rule_tac k = p in dvd_mult_cancel)
-apply (simp_all add: mult_ac)
-done
-
-
-lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime
- ==> \<forall>m n. p^c dvd m*n -->
- (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
-apply (induct_tac "c")
- apply clarify
- apply (case_tac "a")
- apply simp
- apply simp
-(*inductive step*)
-apply simp
-apply clarify
-apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
-(*case 1: p dvd m*)
- apply (case_tac "a")
- apply simp
- apply clarify
- apply (drule spec, drule spec, erule (1) notE impE)
- apply (drule_tac x = nat in spec)
- apply (drule_tac x = b in spec)
- apply simp
- apply (blast intro: dvd_refl mult_dvd_mono)
-(*case 2: p dvd n*)
-apply (case_tac "b")
- apply simp
-apply clarify
-apply (drule spec, drule spec, erule (1) notE impE)
-apply (drule_tac x = a in spec)
-apply (drule_tac x = nat in spec, simp)
-apply (blast intro: dvd_refl mult_dvd_mono)
-done
-
-(*needed in this form in Sylow.ML*)
-lemma div_combine:
- "[| p \<in> prime; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |]
- ==> p ^ a dvd k"
-by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
-
-(*Lemma for power_dvd_bound*)
-lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
-apply (induct_tac "n")
-apply (simp (no_asm_simp))
-apply simp
-apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
-apply (subgoal_tac "2 * p^n <= p * p^n")
-(*?arith_tac should handle all of this!*)
-apply (rule order_trans)
-prefer 2 apply assumption
-apply (drule_tac k = 2 in mult_le_mono2, simp)
-apply (rule mult_le_mono1, simp)
-done
-
-(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
-lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; 0 < a|] ==> n < a"
-apply (drule dvd_imp_le)
-apply (drule_tac [2] n = n in Suc_le_power, auto)
-done
-
-
-subsection{*Exponent Theorems*}
-
-lemma exponent_ge [rule_format]:
- "[|p^k dvd n; p \<in> prime; 0<n|] ==> k <= exponent p n"
-apply (simp add: exponent_def)
-apply (erule Greatest_le)
-apply (blast dest: prime_imp_one_less power_dvd_bound)
-done
-
-lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
-apply (simp add: exponent_def)
-apply clarify
-apply (rule_tac k = 0 in GreatestI)
-prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
-done
-
-lemma power_Suc_exponent_Not_dvd:
- "[|(p * p ^ exponent p s) dvd s; p \<in> prime |] ==> s=0"
-apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
- prefer 2 apply simp
-apply (rule ccontr)
-apply (drule exponent_ge, auto)
-done
-
-lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
-apply (simp (no_asm_simp) add: exponent_def)
-apply (rule Greatest_equality, simp)
-apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
-done
-
-lemma exponent_equalityI:
- "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
-by (simp (no_asm_simp) add: exponent_def)
-
-lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
-by (simp (no_asm_simp) add: exponent_def)
-
-
-(* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *)
-lemma exponent_mult_add1:
- "[| 0 < a; 0 < b |]
- ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
-apply (case_tac "p \<in> prime")
-apply (rule exponent_ge)
-apply (auto simp add: power_add)
-apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
-done
-
-(* exponent_mult_add, opposite inclusion *)
-lemma exponent_mult_add2: "[| 0 < a; 0 < b |]
- ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
-apply (case_tac "p \<in> prime")
-apply (rule leI, clarify)
-apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
-apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
-apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
- prefer 3 apply assumption
- prefer 2 apply simp
-apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
- apply (assumption, force, simp)
-apply (blast dest: power_Suc_exponent_Not_dvd)
-done
-
-lemma exponent_mult_add:
- "[| 0 < a; 0 < b |]
- ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
-by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
-
-
-lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
-apply (case_tac "exponent p n", simp)
-apply (case_tac "n", simp)
-apply (cut_tac s = n and p = p in power_exponent_dvd)
-apply (auto dest: dvd_mult_left)
-done
-
-lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
-apply (case_tac "p \<in> prime")
-apply (auto simp add: prime_iff not_divides_exponent_0)
-done
-
-
-subsection{*Lemmas for the Main Combinatorial Argument*}
-
-lemma p_fac_forw_lemma:
- "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
-apply (rule notnotD)
-apply (rule notI)
-apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
-apply (drule_tac m = a in less_imp_le)
-apply (drule le_imp_power_dvd)
-apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
-apply (frule_tac m = k in less_imp_le)
-apply (drule_tac c = m in le_extend_mult, assumption)
-apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
-prefer 2 apply assumption
-apply (rule dvd_refl [THEN dvd_mult2])
-apply (drule_tac n = k in dvd_imp_le, auto)
-done
-
-lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]
- ==> (p^r) dvd (p^a) - k"
-apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
-apply (subgoal_tac "p^r dvd p^a*m")
- prefer 2 apply (blast intro: dvd_mult2)
-apply (drule dvd_diffD1)
- apply assumption
- prefer 2 apply (blast intro: dvd_diff)
-apply (drule less_imp_Suc_add, auto)
-done
-
-
-lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
-by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
-
-lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |]
- ==> (p^r) dvd (p^a)*m - k"
-apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
-apply (subgoal_tac "p^r dvd p^a*m")
- prefer 2 apply (blast intro: dvd_mult2)
-apply (drule dvd_diffD1)
- apply assumption
- prefer 2 apply (blast intro: dvd_diff)
-apply (drule less_imp_Suc_add, auto)
-done
-
-lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat); k < p^a |]
- ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
-apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
-done
-
-text{*Suc rules that we have to delete from the simpset*}
-lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
-
-(*The bound K is needed; otherwise it's too weak to be used.*)
-lemma p_not_div_choose_lemma [rule_format]:
- "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
- ==> k<K --> exponent p ((j+k) choose k) = 0"
-apply (case_tac "p \<in> prime")
- prefer 2 apply simp
-apply (induct_tac "k")
-apply (simp (no_asm))
-(*induction step*)
-apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
- prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
-apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) =
- exponent p (Suc n)")
- txt{*First, use the assumed equation. We simplify the LHS to
- @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"}
- the common terms cancel, proving the conclusion.*}
- apply (simp del: bad_Sucs add: exponent_mult_add)
-txt{*Establishing the equation requires first applying
- @{text Suc_times_binomial_eq} ...*}
-apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
-txt{*...then @{text exponent_mult_add} and the quantified premise.*}
-apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
-done
-
-(*The lemma above, with two changes of variables*)
-lemma p_not_div_choose:
- "[| k<K; k<=n;
- \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
- ==> exponent p (n choose k) = 0"
-apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
- prefer 3 apply simp
- prefer 2 apply assumption
-apply (drule_tac x = "K - Suc i" in spec)
-apply (simp add: Suc_diff_le)
-done
-
-
-lemma const_p_fac_right:
- "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
-apply (case_tac "p \<in> prime")
- prefer 2 apply simp
-apply (frule_tac a = a in zero_less_prime_power)
-apply (rule_tac K = "p^a" in p_not_div_choose)
- apply simp
- apply simp
- apply (case_tac "m")
- apply (case_tac [2] "p^a")
- apply auto
-(*now the hard case, simplified to
- exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
-apply (subgoal_tac "0<p")
- prefer 2 apply (force dest!: prime_imp_one_less)
-apply (subst exponent_p_a_m_k_equation, auto)
-done
-
-lemma const_p_fac:
- "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
-apply (case_tac "p \<in> prime")
- prefer 2 apply simp
-apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
- prefer 2 apply (force simp add: prime_iff)
-txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
- insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
- first
- transform the binomial coefficient, then use @{text exponent_mult_add}.*}
-apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
- a + exponent p m")
- apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff)
-txt{*one subgoal left!*}
-apply (subst times_binomial_minus1_eq, simp, simp)
-apply (subst exponent_mult_add, simp)
-apply (simp (no_asm_simp) add: zero_less_binomial_iff)
-apply arith
-apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
-done
-
-
-end
--- a/src/HOL/GroupTheory/Module.thy Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-(* Title: HOL/GroupTheory/Module
- ID: $Id$
- Author: Lawrence C Paulson
-
-*)
-
-header{*Modules*}
-
-theory Module = Ring:
-
-text{*The record includes all the group components (carrier, sum, gminus,
-zero), adding the scalar product.*}
-record ('a,'b) module = "'a group" +
- sprod :: "'b \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<star>\<index>" 70)
-
-text{*The locale assumes all the properties of a ring and an Abelian group,
-adding laws relating them.*}
-locale module = ring R + abelian_group M +
- assumes sprod_funcset: "sprod M \<in> carrier R \<rightarrow> carrier M \<rightarrow> carrier M"
- and sprod_assoc:
- "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|]
- ==> (r \<cdot>\<^sub>1 s) \<star>\<^sub>2 a = r \<star>\<^sub>2 (s \<star>\<^sub>2 a)"
- and sprod_distrib_left:
- "[|r \<in> carrier R; a \<in> carrier M; b \<in> carrier M|]
- ==> r \<star>\<^sub>2 (a \<oplus>\<^sub>2 b) = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (r \<star>\<^sub>2 b)"
- and sprod_distrib_right:
- "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|]
- ==> (r \<oplus>\<^sub>1 s) \<star>\<^sub>2 a = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (s \<star>\<^sub>2 a)"
-
-lemma module_iff:
- "module R M = (ring R & abelian_group M & module_axioms R M)"
-by (simp add: module_def ring_def abelian_group_def)
-
-text{*The sum and product in @{text R} are @{text "r \<oplus>\<^sub>1 s"} and @{text
-"r \<cdot>\<^sub>1 s"}, respectively. The sum in @{text M} is @{text "a \<oplus>\<^sub>2 b"}.*}
-
-
-text{*We have to write the ring product as @{text "\<cdot>\<^sub>2"}. But if we
-refer to the scalar product as @{text "\<cdot>\<^sub>1"} then syntactic ambiguities
-arise. This presumably happens because the subscript merely determines which
-structure argument to insert, which happens after parsing. Better to use a
-different symbol such as @{text "\<star>"}*}
-
-subsection {*Trivial Example: Every Ring is an R-Module Over Itself *}
-
-constdefs
- triv_mod :: "('a,'b) ring_scheme => ('a,'a) module"
- "triv_mod R == (|carrier = carrier R,
- sum = sum R,
- gminus = gminus R,
- zero = zero R,
- sprod = prod R|)"
-
-theorem module_triv_mod: "ring R ==> module R (triv_mod R)"
-apply (simp add: triv_mod_def module_iff module_axioms_def
- ring_def ring_axioms_def abelian_group_def
- distrib_l_def distrib_r_def semigroup_def group_axioms_def)
-apply (simp add: abelian_group_axioms_def)
- --{*Combining the two simplifications causes looping!*}
-done
-
-end
--- a/src/HOL/GroupTheory/ROOT.ML Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/GroupTheory/ROOT.ML Tue Mar 18 18:07:06 2003 +0100
@@ -1,6 +1,4 @@
-no_document use_thy "Primes";
no_document use_thy "FuncSet";
-use_thy "Sylow";
-use_thy "Module";
+use_thy "Bij";
use_thy "Summation";
\ No newline at end of file
--- a/src/HOL/GroupTheory/Ring.thy Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,222 +0,0 @@
-(* Title: HOL/GroupTheory/Ring
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
-
-*)
-
-header{*Ring Theory*}
-
-theory Ring = Bij + Coset:
-
-
-subsection{*Definition of a Ring*}
-
-record 'a ring = "'a group" +
- prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>\<index>" 70)
-
-record 'a unit_ring = "'a ring" +
- one :: 'a ("\<one>\<index>")
-
-
-text{*Abbrevations for the left and right distributive laws*}
-constdefs
- distrib_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
- "distrib_l A f g ==
- (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f x (g y z) = g (f x y) (f x z)))"
-
- distrib_r :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
- "distrib_r A f g ==
- (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f (g y z) x = g (f y x) (f z x)))"
-
-
-locale ring = abelian_group R +
- assumes prod_funcset: "prod R \<in> carrier R \<rightarrow> carrier R \<rightarrow> carrier R"
- and prod_assoc:
- "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]
- ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
- and left: "distrib_l (carrier R) (prod R) (sum R)"
- and right: "distrib_r (carrier R) (prod R) (sum R)"
-
-constdefs
- Ring :: "('a,'b) ring_scheme set"
- "Ring == Collect ring"
-
-
-lemma ring_is_abelian_group: "ring(R) ==> abelian_group(R)"
-by (simp add: ring_def abelian_group_def)
-
-text{*Construction of a ring from a semigroup and an Abelian group*}
-lemma ringI:
- "[|abelian_group R;
- semigroup(|carrier = carrier R, sum = prod R|);
- distrib_l (carrier R) (prod R) (sum R);
- distrib_r (carrier R) (prod R) (sum R)|] ==> ring R"
-by (simp add: abelian_group_def ring_def ring_axioms_def semigroup_def)
-
-lemma (in ring) prod_closed [simp]:
- "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<cdot> y \<in> carrier R"
-apply (insert prod_funcset)
-apply (blast dest: funcset_mem)
-done
-
-declare ring.prod_closed [simp]
-
-lemma (in ring) sum_closed:
- "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
-by simp
-
-declare ring.sum_closed [simp]
-
-lemma (in ring) distrib_left:
- "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]
- ==> x \<cdot> (y \<oplus> z) = (x \<cdot> y) \<oplus> (x \<cdot> z)"
-apply (insert left)
-apply (simp add: distrib_l_def)
-done
-
-lemma (in ring) distrib_right:
- "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]
- ==> (y \<oplus> z) \<cdot> x = (y \<cdot> x) \<oplus> (z \<cdot> x)"
-apply (insert right)
-apply (simp add: distrib_r_def)
-done
-
-lemma (in ring) prod_zero_left: "x \<in> carrier R ==> \<zero> \<cdot> x = \<zero>"
-by (simp add: idempotent_imp_zero distrib_right [symmetric])
-
-lemma (in ring) prod_zero_right: "x \<in> carrier R ==> x \<cdot> \<zero> = \<zero>"
-by (simp add: idempotent_imp_zero distrib_left [symmetric])
-
-lemma (in ring) prod_minus_left:
- "[|x \<in> carrier R; y \<in> carrier R|]
- ==> (\<ominus>x) \<cdot> y = \<ominus> (x \<cdot> y)"
-by (simp add: minus_unique prod_zero_left distrib_right [symmetric])
-
-lemma (in ring) prod_minus_right:
- "[|x \<in> carrier R; y \<in> carrier R|]
- ==> x \<cdot> (\<ominus>y) = \<ominus> (x \<cdot> y)"
-by (simp add: minus_unique prod_zero_right distrib_left [symmetric])
-
-
-subsection {*Example: The Ring of Integers*}
-
-constdefs
- integers :: "int ring"
- "integers == (|carrier = UNIV,
- sum = op +,
- gminus = (%x. -x),
- zero = 0::int,
- prod = op *|)"
-
-theorem ring_integers: "ring (integers)"
-by (simp add: integers_def ring_def ring_axioms_def
- distrib_l_def distrib_r_def
- zadd_zmult_distrib zadd_zmult_distrib2
- abelian_group_axioms_def group_axioms_def semigroup_def)
-
-
-subsection {*Ring Homomorphisms*}
-
-constdefs
- ring_hom :: "[('a,'c)ring_scheme, ('b,'d)ring_scheme] => ('a => 'b)set"
- "ring_hom R R' ==
- {h. h \<in> carrier R -> carrier R' &
- (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(sum R x y) = sum R' (h x) (h y)) &
- (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(prod R x y) = prod R' (h x) (h y))}"
-
- ring_auto :: "('a,'b)ring_scheme => ('a => 'a)set"
- "ring_auto R == ring_hom R R \<inter> Bij(carrier R)"
-
- RingAutoGroup :: "[('a,'c) ring_scheme] => ('a=>'a) group"
- "RingAutoGroup R == BijGroup (carrier R) (|carrier := ring_auto R |)"
-
-
-lemma ring_hom_subset_hom: "ring_hom R R' <= hom R R'"
-by (force simp add: ring_hom_def hom_def)
-
-subsection{*The Ring Automorphisms From a Group*}
-
-lemma id_in_ring_auto: "ring R ==> (%x: carrier R. x) \<in> ring_auto R"
-by (simp add: ring_auto_def ring_hom_def restrictI ring.axioms id_Bij)
-
-lemma restrict_Inv_ring_hom:
- "[|ring R; h \<in> ring_hom R R; h \<in> Bij (carrier R)|]
- ==> restrict (Inv (carrier R) h) (carrier R) \<in> ring_hom R R"
-by (simp add: ring.axioms group.axioms
- ring_hom_def Bij_Inv_mem restrictI
- semigroup.sum_funcset ring.prod_funcset Bij_Inv_lemma)
-
-text{*Ring automorphisms are a subgroup of the group of bijections over the
- ring's carrier, and thus a group*}
-lemma subgroup_ring_auto:
- "ring R ==> subgroup (ring_auto R) (BijGroup (carrier R))"
-apply (rule group.subgroupI)
- apply (rule group_BijGroup)
- apply (force simp add: ring_auto_def BijGroup_def)
- apply (blast dest: id_in_ring_auto)
- apply (simp add: ring_auto_def BijGroup_def restrict_Inv_Bij
- restrict_Inv_ring_hom)
-apply (simp add: ring_auto_def BijGroup_def compose_Bij)
-apply (simp add: ring_hom_def compose_def Pi_def)
-done
-
-lemma ring_auto: "ring R ==> group (RingAutoGroup R)"
-apply (drule subgroup_ring_auto)
-apply (simp add: subgroup_def RingAutoGroup_def)
-done
-
-
-subsection{*A Locale for a Pair of Rings and a Homomorphism*}
-
-locale ring_homomorphism = ring R + ring R' +
- fixes h
- assumes homh: "h \<in> ring_hom R R'"
-
-lemma ring_hom_sum:
- "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|]
- ==> h(sum R x y) = sum R' (h x) (h y)"
-by (simp add: ring_hom_def)
-
-lemma ring_hom_prod:
- "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|]
- ==> h(prod R x y) = prod R' (h x) (h y)"
-by (simp add: ring_hom_def)
-
-lemma ring_hom_closed:
- "[|h \<in> ring_hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'"
-by (auto simp add: ring_hom_def funcset_mem)
-
-lemma (in ring_homomorphism) ring_hom_sum [simp]:
- "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)"
-by (simp add: ring_hom_sum [OF homh])
-
-lemma (in ring_homomorphism) ring_hom_prod [simp]:
- "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<cdot>\<^sub>1 y) = (h x) \<cdot>\<^sub>2 (h y)"
-by (simp add: ring_hom_prod [OF homh])
-
-lemma (in ring_homomorphism) group_homomorphism: "group_homomorphism R R' h"
-by (simp add: group_homomorphism_def group_homomorphism_axioms_def
- prems homh ring_hom_subset_hom [THEN subsetD])
-
-lemma (in ring_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier R'"
-by (simp add: ring_hom_closed [OF homh])
-
-lemma (in ring_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2"
-by (rule group_homomorphism.hom_zero [OF group_homomorphism])
-
-lemma (in ring_homomorphism) hom_minus_closed [simp]:
- "x \<in> carrier R ==> h (\<ominus>x) \<in> carrier R'"
-by (rule group_homomorphism.hom_minus_closed [OF group_homomorphism])
-
-lemma (in ring_homomorphism) hom_minus [simp]:
- "x \<in> carrier R ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)"
-by (rule group_homomorphism.hom_minus [OF group_homomorphism])
-
-
-text{*Needed because the standard theorem @{text "ring_homomorphism.intro"}
-is unnatural.*}
-lemma ring_homomorphismI:
- "[|ring R; ring R'; h \<in> ring_hom R R'|] ==> ring_homomorphism R R' h"
-by (simp add: ring_def ring_homomorphism_def ring_homomorphism_axioms_def)
-
-end
--- a/src/HOL/GroupTheory/Sylow.thy Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,364 +0,0 @@
-(* Title: HOL/GroupTheory/Sylow
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
-
-See Florian Kamm\"uller and L. C. Paulson,
- A Formal Proof of Sylow's theorem:
- An Experiment in Abstract Algebra with Isabelle HOL
- J. Automated Reasoning 23 (1999), 235-264
-*)
-
-header{*Sylow's theorem using locales*}
-
-theory Sylow = Coset:
-
-text{*The combinatorial argument is in theory Exponent*}
-
-locale sylow = coset +
- fixes p and a and m and calM and RelM
- assumes prime_p: "p \<in> prime"
- and order_G: "order(G) = (p^a) * m"
- and finite_G [iff]: "finite (carrier G)"
- defines "calM == {s. s <= carrier(G) & card(s) = p^a}"
- and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
- (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
-
-lemma (in sylow) RelM_refl: "refl calM RelM"
-apply (auto simp add: refl_def RelM_def calM_def)
-apply (blast intro!: coset_sum_zero [symmetric])
-done
-
-lemma (in sylow) RelM_sym: "sym RelM"
-proof (unfold sym_def RelM_def, clarify)
- fix y g
- assume "y \<in> calM"
- and g: "g \<in> carrier G"
- hence "y = y #> g #> (\<ominus>g)" by (simp add: coset_sum_assoc calM_def)
- thus "\<exists>g'\<in>carrier G. y = y #> g #> g'"
- by (blast intro: g minus_closed)
-qed
-
-lemma (in sylow) RelM_trans: "trans RelM"
-by (auto simp add: trans_def RelM_def calM_def coset_sum_assoc)
-
-lemma (in sylow) RelM_equiv: "equiv calM RelM"
-apply (unfold equiv_def)
-apply (blast intro: RelM_refl RelM_sym RelM_trans)
-done
-
-lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM ==> M' <= calM"
-apply (unfold RelM_def)
-apply (blast elim!: quotientE)
-done
-
-subsection{*Main Part of the Proof*}
-
-
-locale sylow_central = sylow +
- fixes H and M1 and M
- assumes M_in_quot: "M \<in> calM // RelM"
- and not_dvd_M: "~(p ^ Suc(exponent p m) dvd card(M))"
- and M1_in_M: "M1 \<in> M"
- defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
-
-lemma (in sylow_central) M_subset_calM: "M <= calM"
-by (rule M_in_quot [THEN M_subset_calM_prep])
-
-lemma (in sylow_central) card_M1: "card(M1) = p^a"
-apply (cut_tac M_subset_calM M1_in_M)
-apply (simp add: calM_def, blast)
-done
-
-lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
-by force
-
-lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
-apply (subgoal_tac "0 < card M1")
- apply (blast dest: card_nonempty)
-apply (cut_tac prime_p [THEN prime_imp_one_less])
-apply (simp (no_asm_simp) add: card_M1)
-done
-
-lemma (in sylow_central) M1_subset_G [simp]: "M1 <= carrier G"
-apply (rule subsetD [THEN PowD])
-apply (rule_tac [2] M1_in_M)
-apply (rule M_subset_calM [THEN subset_trans])
-apply (auto simp add: calM_def)
-done
-
-lemma (in sylow_central) M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
-apply (rule exists_x_in_M1 [THEN exE])
-apply (rule_tac x = "%z: H. sum G x z" in bexI)
- apply (rule inj_onI)
- apply (rule left_cancellation)
- apply (auto simp add: H_def M1_subset_G [THEN subsetD])
-apply (rule restrictI)
-apply (simp add: H_def, clarify)
-apply (erule subst)
-apply (simp add: rcosI)
-done
-
-subsection{*Discharging the Assumptions of @{text sylow_central}*}
-
-lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
-by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
-
-lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
-apply (subgoal_tac "M \<noteq> {}")
- apply blast
-apply (cut_tac EmptyNotInEquivSet, blast)
-done
-
-lemma (in sylow) zero_less_o_G: "0 < order(G)"
-apply (unfold order_def)
-apply (blast intro: zero_closed zero_less_card_empty)
-done
-
-lemma (in sylow) zero_less_m: "0 < m"
-apply (cut_tac zero_less_o_G)
-apply (simp add: order_G)
-done
-
-lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
-by (simp add: calM_def n_subsets order_G [symmetric] order_def)
-
-lemma (in sylow) zero_less_card_calM: "0 < card calM"
-by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
-
-lemma (in sylow) max_p_div_calM:
- "~ (p ^ Suc(exponent p m) dvd card(calM))"
-apply (subgoal_tac "exponent p m = exponent p (card calM) ")
- apply (cut_tac zero_less_card_calM prime_p)
- apply (force dest: power_Suc_exponent_Not_dvd)
-apply (simp add: card_calM zero_less_m [THEN const_p_fac])
-done
-
-lemma (in sylow) finite_calM: "finite calM"
-apply (unfold calM_def)
-apply (rule_tac B = "Pow (carrier G) " in finite_subset)
-apply auto
-done
-
-lemma (in sylow) lemma_A1:
- "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))"
-apply (rule max_p_div_calM [THEN contrapos_np])
-apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv])
-done
-
-
-subsubsection{*Introduction and Destruct Rules for @{term H}*}
-
-lemma (in sylow_central) H_I: "[|g \<in> carrier G; M1 #> g = M1|] ==> g \<in> H"
-by (simp add: H_def)
-
-lemma (in sylow_central) H_into_carrier_G: "x \<in> H ==> x \<in> carrier G"
-by (simp add: H_def)
-
-lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1"
-by (simp add: H_def)
-
-lemma (in sylow_central) H_sum_closed: "[| x\<in>H; y\<in>H|] ==> x \<oplus> y \<in> H"
-apply (unfold H_def)
-apply (simp add: coset_sum_assoc [symmetric] sum_closed)
-done
-
-lemma (in sylow_central) H_not_empty: "H \<noteq> {}"
-apply (simp add: H_def)
-apply (rule exI [of _ \<zero>], simp)
-done
-
-lemma (in sylow_central) H_is_subgroup: "subgroup H G"
-apply (rule subgroupI)
-apply (rule subsetI)
-apply (erule H_into_carrier_G)
-apply (rule H_not_empty)
-apply (simp add: H_def, clarify)
-apply (erule_tac P = "%z. ?lhs(z) = M1" in subst)
-apply (simp add: coset_sum_assoc )
-apply (blast intro: H_sum_closed)
-done
-
-
-lemma (in sylow_central) rcosetGM1g_subset_G:
- "[| g \<in> carrier G; x \<in> M1 #> g |] ==> x \<in> carrier G"
-by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
-
-lemma (in sylow_central) finite_M1: "finite M1"
-by (rule finite_subset [OF M1_subset_G finite_G])
-
-lemma (in sylow_central) finite_rcosetGM1g: "g\<in>carrier G ==> finite (M1 #> g)"
-apply (rule finite_subset)
-apply (rule subsetI)
-apply (erule rcosetGM1g_subset_G, assumption)
-apply (rule finite_G)
-done
-
-lemma (in sylow_central) M1_cardeq_rcosetGM1g:
- "g \<in> carrier G ==> card(M1 #> g) = card(M1)"
-by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal setrcosI)
-
-lemma (in sylow_central) M1_RelM_rcosetGM1g:
- "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
-apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G)
-apply (rule conjI)
- apply (blast intro: rcosetGM1g_subset_G)
-apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g)
-apply (rule bexI [of _ "\<ominus>g"])
-apply (simp_all add: coset_sum_assoc M1_subset_G)
-done
-
-
-
-subsection{*Equal Cardinalities of @{term M} and @{term "rcosets G H"}*}
-
-text{*Injections between @{term M} and @{term "rcosets G H"} show that
- their cardinalities are equal.*}
-
-lemma ElemClassEquiv:
- "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
-apply (unfold equiv_def quotient_def sym_def trans_def, blast)
-done
-
-lemma (in sylow_central) M_elem_map:
- "M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2"
-apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]])
-apply (simp add: RelM_def)
-apply (blast dest!: bspec)
-done
-
-lemmas (in sylow_central) M_elem_map_carrier =
- M_elem_map [THEN someI_ex, THEN conjunct1]
-
-lemmas (in sylow_central) M_elem_map_eq =
- M_elem_map [THEN someI_ex, THEN conjunct2]
-
-lemma (in sylow_central) M_funcset_setrcos_H:
- "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
-apply (rule setrcosI [THEN restrictI])
-apply (rule H_is_subgroup [THEN subgroup_imp_subset])
-apply (erule M_elem_map_carrier)
-done
-
-lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets G H. inj_on f M"
-apply (rule bexI)
-apply (rule_tac [2] M_funcset_setrcos_H)
-apply (rule inj_onI, simp)
-apply (rule trans [OF _ M_elem_map_eq])
-prefer 2 apply assumption
-apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
-apply (rule coset_sum_minus1)
-apply (erule_tac [2] M_elem_map_carrier)+
-apply (rule_tac [2] M1_subset_G)
-apply (rule coset_join1 [THEN in_H_imp_eq])
-apply (rule_tac [3] H_is_subgroup)
-prefer 2 apply (blast intro: sum_closed M_elem_map_carrier minus_closed)
-apply (simp add: coset_sum_minus2 H_def M_elem_map_carrier subset_def)
-done
-
-
-(** the opposite injection **)
-
-lemma (in sylow_central) H_elem_map:
- "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
-by (auto simp add: setrcos_eq)
-
-lemmas (in sylow_central) H_elem_map_carrier =
- H_elem_map [THEN someI_ex, THEN conjunct1]
-
-lemmas (in sylow_central) H_elem_map_eq =
- H_elem_map [THEN someI_ex, THEN conjunct2]
-
-
-lemma EquivElemClass:
- "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
-apply (unfold equiv_def quotient_def sym_def trans_def, blast)
-done
-
-lemma (in sylow_central) setrcos_H_funcset_M:
- "(\<lambda>C \<in> rcosets G H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C))
- \<in> rcosets G H \<rightarrow> M"
-apply (simp add: setrcos_eq)
-apply (fast intro: someI2
- intro!: restrictI M1_in_M
- EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
-done
-
-text{*close to a duplicate of @{text inj_M_GmodH}*}
-lemma (in sylow_central) inj_GmodH_M:
- "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)"
-apply (rule bexI)
-apply (rule_tac [2] setrcos_H_funcset_M)
-apply (rule inj_onI)
-apply (simp)
-apply (rule trans [OF _ H_elem_map_eq])
-prefer 2 apply assumption
-apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
-apply (rule coset_sum_minus1)
-apply (erule_tac [2] H_elem_map_carrier)+
-apply (rule_tac [2] H_is_subgroup [THEN subgroup_imp_subset])
-apply (rule coset_join2)
-apply (blast intro: sum_closed minus_closed H_elem_map_carrier)
-apply (rule H_is_subgroup)
-apply (simp add: H_I coset_sum_minus2 M1_subset_G H_elem_map_carrier)
-done
-
-lemma (in sylow_central) calM_subset_PowG: "calM <= Pow(carrier G)"
-by (auto simp add: calM_def)
-
-
-lemma (in sylow_central) finite_M: "finite M"
-apply (rule finite_subset)
-apply (rule M_subset_calM [THEN subset_trans])
-apply (rule calM_subset_PowG, blast)
-done
-
-lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
-apply (insert inj_M_GmodH inj_GmodH_M)
-apply (blast intro: card_bij finite_M H_is_subgroup
- setrcos_subset_PowG [THEN finite_subset]
- finite_Pow_iff [THEN iffD2])
-done
-
-lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)"
-by (simp add: cardMeqIndexH lagrange H_is_subgroup)
-
-lemma (in sylow_central) lemma_leq1: "p^a <= card(H)"
-apply (rule dvd_imp_le)
- apply (rule div_combine [OF prime_p not_dvd_M])
- prefer 2 apply (blast intro: subgroup_card_positive H_is_subgroup)
-apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd
- zero_less_m)
-done
-
-lemma (in sylow_central) lemma_leq2: "card(H) <= p^a"
-apply (subst card_M1 [symmetric])
-apply (cut_tac M1_inj_H)
-apply (blast intro!: M1_subset_G intro:
- card_inj H_into_carrier_G finite_subset [OF _ finite_G])
-done
-
-lemma (in sylow_central) card_H_eq: "card(H) = p^a"
-by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
-
-lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
-apply (cut_tac lemma_A1, clarify)
-apply (frule existsM1inM, clarify)
-apply (subgoal_tac "sylow_central G p a m M1 M")
- apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
-apply (simp add: sylow_central_def sylow_central_axioms_def prems)
-done
-
-text{*Needed because the locale's automatic definition refers to
- @{term "semigroup G"} and @{term "group_axioms G"} rather than
- simply to @{term "group G"}.*}
-lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
-by (simp add: sylow_def group_def)
-
-theorem sylow_thm:
- "[|p \<in> prime; group(G); order(G) = (p^a) * m; finite (carrier G)|]
- ==> \<exists>H. subgroup H G & card(H) = p^a"
-apply (rule sylow.sylow_thm [of G p a m])
-apply (simp add: sylow_eq sylow_axioms_def)
-done
-
-end
--- a/src/HOL/IsaMakefile Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/IsaMakefile Tue Mar 18 18:07:06 2003 +0100
@@ -280,12 +280,8 @@
$(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
Library/Primes.thy Library/FuncSet.thy \
GroupTheory/Bij.thy \
- GroupTheory/Coset.thy \
- GroupTheory/Exponent.thy \
GroupTheory/Group.thy \
- GroupTheory/Module.thy GroupTheory/Ring.thy \
GroupTheory/Summation.thy \
- GroupTheory/Sylow.thy \
GroupTheory/ROOT.ML \
GroupTheory/document/root.tex
@$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
@@ -340,6 +336,9 @@
HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
+ Algebra/Coset.thy \
+ Algebra/Exponent.thy \
+ Algebra/Sylow.thy \
Algebra/abstract/Abstract.thy \
Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
Algebra/abstract/Field.thy \
--- a/src/HOL/UNITY/ProgressSets.thy Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy Tue Mar 18 18:07:06 2003 +0100
@@ -132,7 +132,7 @@
progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
"progress_set F T B ==
- {L. F \<in> stable T & lattice L & B \<in> L & T \<in> L & closed F T B L}"
+ {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
lemma closedD:
"[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|]
@@ -234,7 +234,7 @@
text{*The Lemma proved on page 96*}
lemma progress_set_lemma:
- "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
+ "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
apply (simp add: progress_set_def, clarify)
apply (erule wens_set.induct)
txt{*Base*}
@@ -278,12 +278,13 @@
theorem progress_set_Union:
assumes prog: "C \<in> progress_set F T B"
+ and Fstable: "F \<in> stable T"
and BB': "B \<subseteq> B'"
and B'C: "B' \<in> C"
and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
and leadsTo: "F \<in> A leadsTo B'"
shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
-apply (insert prog)
+apply (insert prog Fstable)
apply (rule leadsTo_Join [OF leadsTo])
apply (force simp add: progress_set_def awp_iff_stable [symmetric])
apply (simp add: awp_iff_constrains)
@@ -292,4 +293,10 @@
BB' [THEN subsetD])
done
+
+subsection {*Some Progress Sets*}
+
+lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
+by (simp add: progress_set_def lattice_def closed_def)
+
end
--- a/src/HOL/UNITY/UNITY.thy Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/UNITY/UNITY.thy Tue Mar 18 18:07:06 2003 +0100
@@ -244,6 +244,10 @@
apply (blast intro: constrains_UN)
done
+lemma stable_Union:
+ "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
+by (unfold stable_def constrains_def, blast)
+
(** Intersection **)
lemma stable_Int:
@@ -258,6 +262,10 @@
apply (blast intro: constrains_INT)
done
+lemma stable_Inter:
+ "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Inter>X)"
+by (unfold stable_def constrains_def, blast)
+
lemma stable_constrains_Un:
"[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
by (unfold stable_def constrains_def, blast)
@@ -267,7 +275,7 @@
by (unfold stable_def constrains_def, blast)
(*[| F \<in> stable C; F \<in> (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
-lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
+lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard]
(*** invariant ***)