# HG changeset patch # User paulson # Date 1555018682 -3600 # Node ID 4ce88d646767d22c5012fb55e710d95cf45c2fe1 # Parent c7866e763e9fb175d2b2af24578849f37aa8bdd5# Parent c6e1a4806f49ccff9b03504fa53ed50495c2f8ce merged diff -r c7866e763e9f -r 4ce88d646767 src/HOL/Algebra/Multiplicative_Group.thy --- a/src/HOL/Algebra/Multiplicative_Group.thy Thu Apr 11 21:33:21 2019 +0200 +++ b/src/HOL/Algebra/Multiplicative_Group.thy Thu Apr 11 22:38:02 2019 +0100 @@ -270,11 +270,11 @@ context group begin definition (in group) ord :: "'a \ nat" where - "ord x \ (@d. \n::nat. pow G x n = one G \ d dvd n)" + "ord x \ (@d. \n::nat. x [^] n = \ \ d dvd n)" lemma (in group) pow_eq_id: assumes "x \ carrier G" - shows "pow G x n = one G \ (ord x) dvd n" + shows "x [^] n = \ \ (ord x) dvd n" proof (cases "\n::nat. pow G x n = one G \ n = 0") case True show ?thesis @@ -429,11 +429,6 @@ by (auto simp: order_def) qed -lemma finite_group_elem_finite_ord: - assumes "finite (carrier G)" "x \ carrier G" - shows "\ d::nat. d \ 1 \ x [^] d = \" - using assms old_ord_ge_1 pow_old_ord_eq_1 by auto - lemma old_ord_min: assumes "finite (carrier G)" "1 \ d" "a \ carrier G" "a [^] d = \" shows "old_ord a \ d" proof - @@ -455,7 +450,7 @@ qed qed -lemma old_ord_dvd_pow_eq_1 : +lemma old_ord_dvd_pow_eq_1: assumes "finite (carrier G)" "a \ carrier G" "a [^] k = \" shows "old_ord a dvd k" proof - @@ -487,45 +482,30 @@ lemma assumes finite: "finite (carrier G)" assumes a: "a \ carrier G" - shows ord_ge_1: "1 \ ord a" and ord_le_group_order: "ord a \ order G" - using a group.old_ord_ge_1 group.pow_eq_id group.pow_old_ord_eq_1 is_group local.finite apply fastforce - by (metis a dvd_antisym group.pow_eq_id is_group local.finite old_ord_dvd_pow_eq_1 old_ord_le_group_order pow_ord_eq_1 pow_old_ord_eq_1) + shows ord_ge_1: "1 \ ord a" + using a group.old_ord_ge_1 group.pow_eq_id group.pow_old_ord_eq_1 is_group local.finite by fastforce lemma ord_inj: - assumes finite: "finite (carrier G)" assumes a: "a \ carrier G" shows "inj_on (\ x . a [^] x) {0 .. ord a - 1}" -proof (rule inj_onI, rule ccontr) - fix x y assume A: "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}" "a [^] x= a [^] y" "x \ y" - - have "finite {d \ {1..order G}. a [^] d = \}" by auto - - { fix x y assume A: "x < y" "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}" - "a [^] x = a [^] y" - hence "y - x < ord a" by auto - also have "\ \ order G" using assms by (simp add: ord_le_group_order) - finally have y_x_range:"y - x \ {1 .. order G}" using A by force - have "a [^] (y-x) = \" using a A by (simp add: pow_eq_div2) +proof - + let ?M = "Max (ord ` carrier G)" + have "finite {d \ {..?M}. a [^] d = \}" by auto - hence y_x:"y - x \ {d \ {1.. order G}. a [^] d = \}" using y_x_range by blast - have "min (y - x) (ord a) = ord a" - using Min.in_idem[OF \finite {d \ {1 .. order G} . a [^] d = \}\ y_x] - by (simp add: a group.ord_iff_old_ord is_group local.finite) - with \y - x < ord a\ have False by linarith - } - note X = this - - { assume "x < y" with A X have False by blast } - moreover - { assume "x > y" with A X have False by metis } - moreover - { assume "x = y" then have False using A by auto} - ultimately - show False by fastforce + have *: False if A: "x < y" "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}" + "a [^] x = a [^] y" for x y + proof - + have "y - x < ord a" using that by auto + moreover have "a [^] (y-x) = \" using a A by (simp add: pow_eq_div2) + ultimately have "min (y - x) (ord a) = ord a" + using A(1) a pow_eq_id by auto + with \y - x < ord a\ show False by linarith + qed + show ?thesis + unfolding inj_on_def by (metis nat_neq_iff *) qed lemma ord_inj': - assumes finite: "finite (carrier G)" assumes a: "a \ carrier G" shows "inj_on (\ x . a [^] x) {1 .. ord a}" proof (rule inj_onI, rule ccontr) @@ -612,31 +592,23 @@ qed lemma generate_pow_card: \<^marker>\contributor \Paulo Emílio de Vilhena\\ - assumes "finite (carrier G)" and "a \ carrier G" + assumes "finite (carrier G)" and a: "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) + using ord_inj[OF a] 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: \<^marker>\contributor \Paulo Emílio de Vilhena\\ +lemma ord_dvd_group_order: 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 by (metis nat_pow_one nat_pow_pow) -qed + 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) -lemma dvd_gcd : +lemma dvd_gcd: fixes a b :: nat obtains q where "a * (b div gcd a b) = b*q" proof @@ -645,9 +617,14 @@ finally show "a * (b div gcd a b) = b * (a div gcd a b) " . qed -lemma ord_pow_dvd_ord_elem : +lemma (in group) ord_le_group_order: + assumes finite: "finite (carrier G)" and a: "a \ carrier G" + shows "ord a \ order G" + by (simp add: finite order_gt_0_iff_finite dvd_imp_le [OF ord_dvd_group_order [OF assms]]) + +lemma ord_pow_dvd_ord_elem: assumes finite[simp]: "finite (carrier G)" - assumes a[simp]:"a \ carrier G" + assumes a[simp]: "a \ carrier G" shows "ord (a[^]n) = ord a div gcd n (ord a)" proof - have "(a[^]n) [^] ord a = (a [^] ord a) [^] n" @@ -714,13 +691,6 @@ generate_pow_on_finite_carrier[OF assms] unfolding ord_elems[OF assms] by auto -lemma ord_dvd_group_order: - 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 @@ -751,12 +721,12 @@ 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 : +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 -lemma field_mult_group : +lemma field_mult_group: shows "group (mult_of R)" apply (rule groupI) apply (auto simp: mult_of_simps m_assoc dest: integral) @@ -791,7 +761,7 @@ context UP_cring begin lemma is_UP_cring:"UP_cring R" by (unfold_locales) -lemma is_UP_ring : +lemma is_UP_ring: shows "UP_ring R" by (unfold_locales) end @@ -893,18 +863,6 @@ by the first proof given in the survey~@{cite "conrad-cyclicity"}. \ -lemma (in group) pow_order_eq_1: - assumes "finite (carrier G)" "x \ carrier G" shows "x [^] order G = \" - using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one) - -(* XXX remove in AFP devel, replaced by div_eq_dividend_iff *) -lemma nat_div_eq: "a \ 0 \ (a :: nat) div b = a \ b = 1" - apply rule - apply (cases "b = 0") - apply simp_all - apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3) - done - lemma (in group) assumes finite': "finite (carrier G)" assumes "a \ carrier G" @@ -912,7 +870,7 @@ proof assume A: ?L then show ?R using assms ord_ge_1 [OF assms] - by (auto simp: nat_div_eq ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1) + by (auto simp: div_eq_dividend_iff ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1) next assume ?R then show ?L using ord_pow_dvd_ord_elem[OF assms, of k] by auto @@ -957,7 +915,7 @@ using finite by (auto intro: card_mono) also have "\ \ d" using \0 < order (mult_of R)\ num_roots_le_deg[OF finite, of d] by (simp add : dvd_pos_nat[OF _ \d dvd order (mult_of R)\]) - finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image) + finally show ?thesis using G.ord_inj'[OF a] ord_a * by (simp add: card_image) qed qed @@ -973,7 +931,7 @@ show "?R \ ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of) qed have "inj_on (\ n . a[^]n) {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" - using G.ord_inj'[OF finite' a, unfolded ord_a] unfolding inj_on_def by fast + using G.ord_inj'[OF a, unfolded ord_a] unfolding inj_on_def by fast hence "card ((\n. a[^]n) ` {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}) = card {k \ {1 .. d}. group.ord (mult_of R) (a[^]k) = d}" using card_image by blast