# HG changeset patch # User paulson # Date 1530554330 -3600 # Node ID d40d03487f648d9aeb7e3c055d835ebc4a20dab0 # Parent 2a6e258bfd66186542de71b2cd60790047a2d440 more lemmas from Paulo diff -r 2a6e258bfd66 -r d40d03487f64 src/HOL/Algebra/Multiplicative_Group.thy --- a/src/HOL/Algebra/Multiplicative_Group.thy Mon Jul 02 16:20:03 2018 +0100 +++ b/src/HOL/Algebra/Multiplicative_Group.thy Mon Jul 02 18:58:50 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)"