# HG changeset patch # User paulson # Date 1530564335 -3600 # Node ID c0b978f6ecd16011a0ab0a0f96958bb746e6f90b # Parent 0307cdca646249d5e159ee483e3f26dc60e41384# Parent b6cc5c265b045411bd5a544dc43bda5121e85344 merged diff -r 0307cdca6462 -r c0b978f6ecd1 src/HOL/Algebra/Generated_Groups.thy --- a/src/HOL/Algebra/Generated_Groups.thy Mon Jul 02 20:28:09 2018 +0200 +++ b/src/HOL/Algebra/Generated_Groups.thy Mon Jul 02 21:45:35 2018 +0100 @@ -51,7 +51,7 @@ show "\h. h \ generate G H \ inv h \ generate G H" using generate_m_inv_closed[OF assms] by blast show "\h1 h2. \ h1 \ generate G H; h2 \ generate G H \ \ h1 \ h2 \ generate G H" - by (simp add: generate.eng) + by (simp add: generate.eng) qed @@ -64,11 +64,11 @@ proof fix h show "h \ generate G H \ h \ E" proof (induct rule: generate.induct) - case one thus ?case using subgroup.one_closed[OF assms(2)] by simp + case one thus ?case using subgroup.one_closed[OF assms(2)] by simp case incl thus ?case using assms(3) by blast case inv thus ?case using subgroup.m_inv_closed[OF assms(2)] assms(3) by blast next - case eng thus ?case using subgroup.m_closed[OF assms(2)] by simp + case eng thus ?case using subgroup.m_closed[OF assms(2)] by simp qed qed @@ -119,14 +119,14 @@ where "norm G (One) = \\<^bsub>G\<^esub>" | "norm G (Inv h) = (inv\<^bsub>G\<^esub> h)" - | "norm G (Leaf h) = h" + | "norm G (Leaf h) = h" | "norm G (Mult h1 h2) = (norm G h1) \\<^bsub>G\<^esub> (norm G h2)" fun elts :: "'a repr \ 'a set" where "elts (One) = {}" | "elts (Inv h) = { h }" - | "elts (Leaf h) = { h }" + | "elts (Leaf h) = { h }" | "elts (Mult h1 h2) = (elts h1) \ (elts h2)" lemma (in group) generate_repr_iff: @@ -136,7 +136,7 @@ show "h \ generate G H \ \r. (elts r) \ H \ norm G r = h" proof (induction rule: generate.induct) case one thus ?case - using elts.simps(1) norm.simps(1)[of G] by fastforce + using elts.simps(1) norm.simps(1)[of G] by fastforce next case (incl h) hence "elts (Leaf h) \ H \ norm G (Leaf h) = h" by simp @@ -150,7 +150,7 @@ then obtain r1 r2 where r1: "elts r1 \ H" "norm G r1 = h1" and r2: "elts r2 \ H" "norm G r2 = h2" by blast hence "elts (Mult r1 r2) \ H \ norm G (Mult r1 r2) = h1 \ h2" by simp - thus ?case by blast + thus ?case by blast qed show "\r. elts r \ H \ norm G r = h \ h \ generate G H" @@ -161,7 +161,7 @@ proof (induction arbitrary: h rule: repr.induct) case One thus ?case using generate.one by auto next - case Inv thus ?case using generate.simps by force + case Inv thus ?case using generate.simps by force next case Leaf thus ?case using generate.simps by force next @@ -207,10 +207,10 @@ proof (induction r rule: repr.induct) case One thus ?case by simp next - case (Inv k) hence "k \ K" using A by simp + case (Inv k) hence "k \ K" using A by simp thus ?case using m_inv_consistent[OF assms(1)] assms(2) by auto next - case (Leaf k) hence "k \ K" using A by simp + case (Leaf k) hence "k \ K" using A by simp thus ?case using m_inv_consistent[OF assms(1)] assms(2) by auto next case (Mult k1 k2) thus ?case using mult_eq by auto @@ -259,7 +259,7 @@ thus "(g \ (norm G r) \ (inv g)) \ (generate G H)" proof (induction r rule: repr.induct) case One thus ?case - by (simp add: generate.one) + by (simp add: generate.one) next case (Inv h) hence "g \ h \ (inv g) \ H" using assms(2) by simp @@ -267,7 +267,7 @@ using Inv.prems(1) Inv.prems(2) assms(1) inv_mult_group m_assoc by auto ultimately have "\r. elts r \ H \ norm G r = g \ (inv h) \ (inv g)" by (metis elts.simps(2) empty_subsetI insert_subset) - thus ?case by (simp add: assms(1) generate_repr_iff) + thus ?case by (simp add: assms(1) generate_repr_iff) next case (Leaf h) thus ?case using assms(2)[of h g] generate.incl[of "g \ h \ inv g" H] by simp @@ -305,16 +305,16 @@ proof fix h show "h \ generate G { a } \ h \ { a [^] k | k. k \ (UNIV :: int set) }" proof (induction rule: generate.induct) - case one thus ?case by (metis (mono_tags, lifting) UNIV_I int_pow_0 mem_Collect_eq) + case one thus ?case by (metis (mono_tags, lifting) UNIV_I int_pow_0 mem_Collect_eq) next case (incl h) hence "h = a" by auto thus ?case - by (metis (mono_tags, lifting) CollectI UNIV_I assms group.int_pow_1 is_group) + by (metis (mono_tags, lifting) CollectI UNIV_I assms group.int_pow_1 is_group) next case (inv h) hence "h = a" by auto thus ?case by (metis (mono_tags, lifting) mem_Collect_eq UNIV_I assms group.int_pow_1 int_pow_neg is_group) next case (eng h1 h2) thus ?case - by (smt assms group.int_pow_mult is_group iso_tuple_UNIV_I mem_Collect_eq) + by (smt assms group.int_pow_mult is_group iso_tuple_UNIV_I mem_Collect_eq) qed qed @@ -444,7 +444,7 @@ qed thus ?thesis by simp qed - thus ?thesis unfolding derived_def using generate_empty generate_one by presburger + thus ?thesis unfolding derived_def using generate_empty generate_one by presburger qed lemma (in group) derived_set_in_carrier: @@ -569,7 +569,7 @@ have "group (G \ carrier := H \)" using assms subgroup_imp_group by auto thus ?thesis - using group.derived_quot_is_comm_group subgroup_derived_equality[OF assms] by fastforce + using group.derived_quot_is_comm_group subgroup_derived_equality[OF assms] by fastforce qed lemma (in group) mono_derived: @@ -610,8 +610,8 @@ also have " ... \ (derived G) (carrier G)" using mono_derived[of "carrier G" "(derived G ^^ n) H" 1] Suc by simp also have " ... \ carrier G" unfolding derived_def - by (simp add: derived_set_incl generate_min_subgroup1 subgroup_self) - finally show ?case . + by (simp add: derived_set_incl generate_min_subgroup1 subgroup_self) + finally show ?case . qed lemma (in group) exp_of_derived_is_subgroup: @@ -624,8 +624,10 @@ have "(derived G ^^ n) H \ carrier G" by (simp add: Suc.IH assms subgroup.subset) hence "subgroup ((derived G) ((derived G ^^ n) H)) G" - unfolding derived_def using derived_set_in_carrier generate_is_subgroup by auto + unfolding derived_def using derived_set_in_carrier generate_is_subgroup by auto thus ?case by simp qed -end \ No newline at end of file +hide_const (open) norm + +end diff -r 0307cdca6462 -r c0b978f6ecd1 src/HOL/Algebra/Multiplicative_Group.thy --- a/src/HOL/Algebra/Multiplicative_Group.thy Mon Jul 02 20:28:09 2018 +0200 +++ b/src/HOL/Algebra/Multiplicative_Group.thy Mon Jul 02 21:45:35 2018 +0100 @@ -9,6 +9,7 @@ Group Coset UnivPoly + Generated_Groups begin section \Simplification Rules for Polynomials\ @@ -120,7 +121,7 @@ $\sum_{d | n}^n \varphi(d) = n$ holds. \ -lemma dvd_div_ge_1 : +lemma dvd_div_ge_1: fixes a b :: nat assumes "a \ 1" "b dvd a" shows "a div b \ 1" @@ -129,7 +130,7 @@ with \a \ 1\ show ?thesis by simp qed -lemma dvd_nat_bounds : +lemma dvd_nat_bounds: fixes n p :: nat assumes "p > 0" "n dvd p" shows "n > 0 \ n \ p" @@ -142,7 +143,7 @@ notation (latex output) phi' ("\ _") -lemma phi'_nonzero : +lemma phi'_nonzero: assumes "m > 0" shows "phi' m > 0" proof - @@ -207,7 +208,7 @@ @{term "(\d \ {d. d dvd n}. {m \ {1::nat .. n}. n div gcd m n = d}) \ {1 .. n}"} (this is our counting argument) the thesis follows. \ -lemma sum_phi'_factors : +lemma sum_phi'_factors: fixes n :: nat assumes "n > 0" shows "(\d | d dvd n. phi' d) = n" @@ -266,7 +267,7 @@ context group begin -lemma pow_eq_div2 : +lemma pow_eq_div2: fixes m n :: nat assumes x_car: "x \ carrier G" assumes pow_eq: "x [^] m = x [^] n" @@ -319,7 +320,7 @@ by (auto simp: order_def) qed -lemma finite_group_elem_finite_ord : +lemma finite_group_elem_finite_ord: assumes "finite (carrier G)" "x \ carrier G" shows "\ d::nat. d \ 1 \ x [^] d = \" using assms ord_ge_1 pow_ord_eq_1 by auto @@ -345,7 +346,7 @@ qed qed -lemma ord_inj : +lemma ord_inj: assumes finite: "finite (carrier G)" assumes a: "a \ carrier G" shows "inj_on (\ x . a [^] x) {0 .. ord a - 1}" @@ -377,7 +378,7 @@ show False by fastforce qed -lemma ord_inj' : +lemma ord_inj': assumes finite: "finite (carrier G)" assumes a: "a \ carrier G" shows "inj_on (\ x . a [^] x) {1 .. ord a}" @@ -402,7 +403,7 @@ ultimately show False using A by force qed -lemma ord_elems : +lemma ord_elems: assumes "finite (carrier G)" "a \ carrier G" shows "{a[^]x | x. x \ (UNIV :: nat set)} = {a[^]x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R") proof @@ -422,6 +423,75 @@ thus "?L \ ?R" by auto qed +(* Next three lemmas contributed by Paulo Emílio de Vilhena*) +lemma generate_pow_on_finite_carrier: + assumes "finite (carrier G)" and "a \ carrier G" + shows "generate G { a } = { a [^] k | k. k \ (UNIV :: nat set) }" +proof + show "{ a [^] k | k. k \ (UNIV :: nat set) } \ generate G { a }" + proof + fix b assume "b \ { a [^] k | k. k \ (UNIV :: nat set) }" + then obtain k :: nat where "b = a [^] k" by blast + hence "b = a [^] (int k)" + using int_pow_def2 by auto + thus "b \ generate G { a }" + unfolding generate_pow[OF assms(2)] by blast + qed +next + show "generate G { a } \ { a [^] k | k. k \ (UNIV :: nat set) }" + proof + fix b assume "b \ generate G { a }" + then obtain k :: int where k: "b = a [^] k" + unfolding generate_pow[OF assms(2)] by blast + show "b \ { a [^] k | k. k \ (UNIV :: nat set) }" + proof (cases "k < 0") + assume "\ k < 0" + hence "b = a [^] (nat k)" + using k int_pow_def2 by auto + thus ?thesis by blast + next + assume "k < 0" + hence b: "b = inv (a [^] (nat (- k)))" + using k int_pow_def2 by auto + + obtain m where m: "ord a * m \ nat (- k)" + by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1) + hence "a [^] (ord a * m) = \" + by (metis assms nat_pow_one nat_pow_pow pow_ord_eq_1) + then obtain k' :: nat where "(a [^] (nat (- k))) \ (a [^] k') = \" + using m assms(2) nat_le_iff_add nat_pow_mult by auto + hence "b = a [^] k'" + using b assms(2) by (metis inv_unique' nat_pow_closed nat_pow_comm) + thus "b \ { a [^] k | k. k \ (UNIV :: nat set) }" by blast + qed + qed +qed + +lemma generate_pow_card: + assumes "finite (carrier G)" and "a \ carrier G" + shows "ord a = card (generate G { a })" +proof - + have "generate G { a } = (([^]) a) ` {0..ord a - 1}" + using generate_pow_on_finite_carrier[OF assms] unfolding ord_elems[OF assms] by auto + thus ?thesis + using ord_inj[OF assms] ord_ge_1[OF assms] by (simp add: card_image) +qed + +(* This lemma was a suggestion of generalization given by Jeremy Avigad + at the end of the theory FiniteProduct. *) +corollary power_order_eq_one_group_version: + assumes "finite (carrier G)" and "a \ carrier G" + shows "a [^] (order G) = \" +proof - + have "(ord a) dvd (order G)" + using lagrange[OF generate_is_subgroup[of " { a }"]] assms(2) + unfolding generate_pow_card[OF assms] + by (metis dvd_triv_right empty_subsetI insert_subset) + then obtain k :: nat where "order G = ord a * k" by blast + thus ?thesis + using assms(2) pow_ord_eq_1[OF assms] by (metis nat_pow_one nat_pow_pow) +qed + lemma ord_dvd_pow_eq_1 : assumes "finite (carrier G)" "a \ carrier G" "a [^] k = \" shows "ord a dvd k" @@ -514,57 +584,20 @@ shows "ord \ = 1" using assms ord_ge_1 ord_min[of 1 \] by force -theorem lagrange_dvd: - assumes "finite(carrier G)" "subgroup H G" shows "(card H) dvd (order G)" - using assms by (simp add: lagrange[symmetric]) - lemma element_generates_subgroup: assumes finite[simp]: "finite (carrier G)" assumes a[simp]: "a \ carrier G" shows "subgroup {a [^] i | i. i \ {0 .. ord a - 1}} G" -proof - show "{a[^]i | i. i \ {0 .. ord a - 1} } \ carrier G" by auto -next - fix x y - assume A: "x \ {a[^]i | i. i \ {0 .. ord a - 1}}" "y \ {a[^]i | i. i \ {0 .. ord a - 1}}" - obtain i::nat where i:"x = a[^]i" and i2:"i \ UNIV" using A by auto - obtain j::nat where j:"y = a[^]j" and j2:"j \ UNIV" using A by auto - have "a[^](i+j) \ {a[^]i | i. i \ {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto - thus "x \ y \ {a[^]i | i. i \ {0 .. ord a - 1}}" - using i j a ord_elems assms by (auto simp add: nat_pow_mult) -next - show "\ \ {a[^]i | i. i \ {0 .. ord a - 1}}" by force -next - fix x assume x: "x \ {a[^]i | i. i \ {0 .. ord a - 1}}" - hence x_in_carrier: "x \ carrier G" by auto - then obtain d::nat where d:"x [^] d = \" and "d\1" - using finite_group_elem_finite_ord by auto - have inv_1:"x[^](d - 1) \ x = \" using \d\1\ d nat_pow_Suc[of x "d - 1"] by simp - have elem:"x [^] (d - 1) \ {a[^]i | i. i \ {0 .. ord a - 1}}" - proof - - obtain i::nat where i:"x = a[^]i" using x by auto - hence "x[^](d - 1) \ {a[^]i | i. i \ (UNIV::nat set)}" by (auto simp add: nat_pow_pow) - thus ?thesis using ord_elems[of a] by auto - qed - have inv:"inv x = x[^](d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast - thus "inv x \ {a[^]i | i. i \ {0 .. ord a - 1}}" using elem inv by auto -qed + using generate_is_subgroup[of "{ a }"] assms(2) + generate_pow_on_finite_carrier[OF assms] + unfolding ord_elems[OF assms] by auto -lemma ord_dvd_group_order : - assumes finite[simp]: "finite (carrier G)" - assumes a[simp]: "a \ carrier G" - shows "ord a dvd order G" -proof - - have card_dvd:"card {a[^]i | i. i \ {0 .. ord a - 1}} dvd card (carrier G)" - using lagrange_dvd element_generates_subgroup unfolding order_def by simp - have "inj_on (\ i . a[^]i) {0..ord a - 1}" using ord_inj by simp - hence cards_eq:"card ( (\ i . a[^]i) ` {0..ord a - 1}) = card {0..ord a - 1}" - using card_image[of "\ i . a[^]i" "{0..ord a - 1}"] by auto - have "(\ i . a[^]i) ` {0..ord a - 1} = {a[^]i | i. i \ {0..ord a - 1}}" by auto - hence "card {a[^]i | i. i \ {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp - also have "\ = ord a" using ord_ge_1[of a] by simp - finally show ?thesis using card_dvd by (simp add: order_def) -qed +lemma ord_dvd_group_order: (* <- DELETE *) + assumes "finite (carrier G)" and "a \ carrier G" + shows "(ord a) dvd (order G)" + using lagrange[OF generate_is_subgroup[of " { a }"]] assms(2) + unfolding generate_pow_card[OF assms] + by (metis dvd_triv_right empty_subsetI insert_subset) end @@ -590,16 +623,16 @@ lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of -context field +context field begin -lemma mult_of_is_Units: "mult_of R = units_of R" +lemma mult_of_is_Units: "mult_of R = units_of R" unfolding mult_of_def units_of_def using field_Units by auto lemma m_inv_mult_of : "\x. x \ carrier (mult_of R) \ m_inv (mult_of R) x = m_inv R x" using mult_of_is_Units units_of_inv unfolding units_of_def - by simp + by simp lemma field_mult_group : shows "group (mult_of R)" diff -r 0307cdca6462 -r c0b978f6ecd1 src/HOL/Algebra/Solvable_Groups.thy --- a/src/HOL/Algebra/Solvable_Groups.thy Mon Jul 02 20:28:09 2018 +0200 +++ b/src/HOL/Algebra/Solvable_Groups.thy Mon Jul 02 21:45:35 2018 +0100 @@ -174,9 +174,9 @@ show "generate H (h ` K) \ h ` generate G K" proof fix x assume "x \ generate H (h ` K)" - then obtain r where r: "elts r \ (h ` K)" "norm H r = x" + then obtain r where r: "elts r \ (h ` K)" "Generated_Groups.norm H r = x" using H.generate_repr_iff img_in_carrier by auto - from \elts r \ (h ` K)\ have "norm H r \ h ` generate G K" + from \elts r \ (h ` K)\ have "Generated_Groups.norm H r \ h ` generate G K" proof (induct r rule: repr.induct) case One have "\\<^bsub>G\<^esub> \ generate G K" using generate.one[of G] by simp @@ -193,11 +193,11 @@ thus ?case by (simp add: generate.incl) next case (Mult x1 x2) hence A: "elts x1 \ elts x2 \ h ` K" by simp - have "norm H x1 \ h ` (generate G K)" using A Mult by simp - moreover have "norm H x2 \ h ` (generate G K)" using A Mult by simp - ultimately obtain k1 k2 where k1: "k1 \ generate G K" "norm H x1 = h k1" - and k2: "k2 \ generate G K" "norm H x2 = h k2" by blast - hence "norm H (Mult x1 x2) = h (k1 \ k2)" + have "Generated_Groups.norm H x1 \ h ` (generate G K)" using A Mult by simp + moreover have "Generated_Groups.norm H x2 \ h ` (generate G K)" using A Mult by simp + ultimately obtain k1 k2 where k1: "k1 \ generate G K" "Generated_Groups.norm H x1 = h k1" + and k2: "k2 \ generate G K" "Generated_Groups.norm H x2 = h k2" by blast + hence "Generated_Groups.norm H (Mult x1 x2) = h (k1 \ k2)" using G.generate_in_carrier assms by auto thus ?case using k1 k2 by (simp add: generate.eng) qed @@ -208,24 +208,24 @@ show "h ` generate G K \ generate H (h ` K)" proof fix x assume "x \ h ` generate G K" - then obtain r where r: "elts r \ K" "x = h (norm G r)" using G.generate_repr_iff assms by auto - from \elts r \ K\ have "h (norm G r) \ generate H (h ` K)" + then obtain r where r: "elts r \ K" "x = h (Generated_Groups.norm G r)" using G.generate_repr_iff assms by auto + from \elts r \ K\ have "h (Generated_Groups.norm G r) \ generate H (h ` K)" proof (induct r rule: repr.induct) case One thus ?case by (simp add: generate.one) next case (Inv x) hence A: "x \ K" by simp - hence "h (norm G (Inv x)) = inv\<^bsub>H\<^esub> (h x)" using assms by auto + hence "h (Generated_Groups.norm G (Inv x)) = inv\<^bsub>H\<^esub> (h x)" using assms by auto moreover have "h x \ generate H (h ` K)" using A by (simp add: generate.incl) ultimately show ?case by (simp add: A generate.inv) next case (Leaf x) thus ?case by (simp add: generate.incl) next case (Mult x1 x2) hence A: "elts x1 \ elts x2 \ K" by simp - have "norm G x1 \ carrier G" + have "Generated_Groups.norm G x1 \ carrier G" by (meson A G.generateE(1) G.generate_repr_iff Un_subset_iff assms subgroup.mem_carrier) - moreover have "norm G x2 \ carrier G" + moreover have "Generated_Groups.norm G x2 \ carrier G" by (meson A G.generateE(1) G.generate_repr_iff Un_subset_iff assms subgroup.mem_carrier) - ultimately have "h (norm G (Mult x1 x2)) = h (norm G x1) \\<^bsub>H\<^esub> h (norm G x2)" by simp + ultimately have "h (Generated_Groups.norm G (Mult x1 x2)) = h (Generated_Groups.norm G x1) \\<^bsub>H\<^esub> h (Generated_Groups.norm G x2)" by simp thus ?case using Mult A by (simp add: generate.eng) qed thus "x \ generate H (h ` K)" using r by simp