--- 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 "\<And>h. h \<in> generate G H \<Longrightarrow> inv h \<in> generate G H"
using generate_m_inv_closed[OF assms] by blast
show "\<And>h1 h2. \<lbrakk> h1 \<in> generate G H; h2 \<in> generate G H \<rbrakk> \<Longrightarrow> h1 \<otimes> h2 \<in> generate G H"
- by (simp add: generate.eng)
+ by (simp add: generate.eng)
qed
@@ -64,11 +64,11 @@
proof
fix h show "h \<in> generate G H \<Longrightarrow> h \<in> 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) = \<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) \<otimes>\<^bsub>G\<^esub> (norm G h2)"
fun elts :: "'a repr \<Rightarrow> 'a set"
where
"elts (One) = {}"
| "elts (Inv h) = { h }"
- | "elts (Leaf h) = { h }"
+ | "elts (Leaf h) = { h }"
| "elts (Mult h1 h2) = (elts h1) \<union> (elts h2)"
lemma (in group) generate_repr_iff:
@@ -136,7 +136,7 @@
show "h \<in> generate G H \<Longrightarrow> \<exists>r. (elts r) \<subseteq> H \<and> 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) \<subseteq> H \<and> norm G (Leaf h) = h" by simp
@@ -150,7 +150,7 @@
then obtain r1 r2 where r1: "elts r1 \<subseteq> H" "norm G r1 = h1"
and r2: "elts r2 \<subseteq> H" "norm G r2 = h2" by blast
hence "elts (Mult r1 r2) \<subseteq> H \<and> norm G (Mult r1 r2) = h1 \<otimes> h2" by simp
- thus ?case by blast
+ thus ?case by blast
qed
show "\<exists>r. elts r \<subseteq> H \<and> norm G r = h \<Longrightarrow> h \<in> 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 \<in> K" using A by simp
+ case (Inv k) hence "k \<in> K" using A by simp
thus ?case using m_inv_consistent[OF assms(1)] assms(2) by auto
next
- case (Leaf k) hence "k \<in> K" using A by simp
+ case (Leaf k) hence "k \<in> 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 \<otimes> (norm G r) \<otimes> (inv g)) \<in> (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 \<otimes> h \<otimes> (inv g) \<in> 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 "\<exists>r. elts r \<subseteq> H \<and> norm G r = g \<otimes> (inv h) \<otimes> (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 \<otimes> h \<otimes> inv g" H] by simp
@@ -305,16 +305,16 @@
proof
fix h show "h \<in> generate G { a } \<Longrightarrow> h \<in> { a [^] k | k. k \<in> (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 \<lparr> carrier := H \<rparr>)"
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 " ... \<subseteq> (derived G) (carrier G)"
using mono_derived[of "carrier G" "(derived G ^^ n) H" 1] Suc by simp
also have " ... \<subseteq> 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 \<subseteq> 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
--- 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 \<open>Simplification Rules for Polynomials\<close>
@@ -120,7 +121,7 @@
$\sum_{d | n}^n \varphi(d) = n$ holds.
\<close>
-lemma dvd_div_ge_1 :
+lemma dvd_div_ge_1:
fixes a b :: nat
assumes "a \<ge> 1" "b dvd a"
shows "a div b \<ge> 1"
@@ -129,7 +130,7 @@
with \<open>a \<ge> 1\<close> 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 \<and> n \<le> p"
@@ -142,7 +143,7 @@
notation (latex output)
phi' ("\<phi> _")
-lemma phi'_nonzero :
+lemma phi'_nonzero:
assumes "m > 0"
shows "phi' m > 0"
proof -
@@ -207,7 +208,7 @@
@{term "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}"}
(this is our counting argument) the thesis follows.
\<close>
-lemma sum_phi'_factors :
+lemma sum_phi'_factors:
fixes n :: nat
assumes "n > 0"
shows "(\<Sum>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 \<in> 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 \<in> carrier G"
shows "\<exists> d::nat. d \<ge> 1 \<and> x [^] d = \<one>"
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 \<in> carrier G"
shows "inj_on (\<lambda> 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 \<in> carrier G"
shows "inj_on (\<lambda> 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 \<in> carrier G"
shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
proof
@@ -422,6 +423,75 @@
thus "?L \<subseteq> ?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 \<in> carrier G"
+ shows "generate G { a } = { a [^] k | k. k \<in> (UNIV :: nat set) }"
+proof
+ show "{ a [^] k | k. k \<in> (UNIV :: nat set) } \<subseteq> generate G { a }"
+ proof
+ fix b assume "b \<in> { a [^] k | k. k \<in> (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 \<in> generate G { a }"
+ unfolding generate_pow[OF assms(2)] by blast
+ qed
+next
+ show "generate G { a } \<subseteq> { a [^] k | k. k \<in> (UNIV :: nat set) }"
+ proof
+ fix b assume "b \<in> generate G { a }"
+ then obtain k :: int where k: "b = a [^] k"
+ unfolding generate_pow[OF assms(2)] by blast
+ show "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }"
+ proof (cases "k < 0")
+ assume "\<not> 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 \<ge> nat (- k)"
+ by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
+ hence "a [^] (ord a * m) = \<one>"
+ by (metis assms nat_pow_one nat_pow_pow pow_ord_eq_1)
+ then obtain k' :: nat where "(a [^] (nat (- k))) \<otimes> (a [^] k') = \<one>"
+ 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 \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }" by blast
+ qed
+ qed
+qed
+
+lemma generate_pow_card:
+ assumes "finite (carrier G)" and "a \<in> 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 \<in> carrier G"
+ shows "a [^] (order G) = \<one>"
+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 \<in> carrier G" "a [^] k = \<one>"
shows "ord a dvd k"
@@ -514,57 +584,20 @@
shows "ord \<one> = 1"
using assms ord_ge_1 ord_min[of 1 \<one>] 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 \<in> carrier G"
shows "subgroup {a [^] i | i. i \<in> {0 .. ord a - 1}} G"
-proof
- show "{a[^]i | i. i \<in> {0 .. ord a - 1} } \<subseteq> carrier G" by auto
-next
- fix x y
- assume A: "x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" "y \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
- obtain i::nat where i:"x = a[^]i" and i2:"i \<in> UNIV" using A by auto
- obtain j::nat where j:"y = a[^]j" and j2:"j \<in> UNIV" using A by auto
- have "a[^](i+j) \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto
- thus "x \<otimes> y \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
- using i j a ord_elems assms by (auto simp add: nat_pow_mult)
-next
- show "\<one> \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" by force
-next
- fix x assume x: "x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
- hence x_in_carrier: "x \<in> carrier G" by auto
- then obtain d::nat where d:"x [^] d = \<one>" and "d\<ge>1"
- using finite_group_elem_finite_ord by auto
- have inv_1:"x[^](d - 1) \<otimes> x = \<one>" using \<open>d\<ge>1\<close> d nat_pow_Suc[of x "d - 1"] by simp
- have elem:"x [^] (d - 1) \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
- proof -
- obtain i::nat where i:"x = a[^]i" using x by auto
- hence "x[^](d - 1) \<in> {a[^]i | i. i \<in> (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 \<in> {a[^]i | i. i \<in> {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 \<in> carrier G"
- shows "ord a dvd order G"
-proof -
- have card_dvd:"card {a[^]i | i. i \<in> {0 .. ord a - 1}} dvd card (carrier G)"
- using lagrange_dvd element_generates_subgroup unfolding order_def by simp
- have "inj_on (\<lambda> i . a[^]i) {0..ord a - 1}" using ord_inj by simp
- hence cards_eq:"card ( (\<lambda> i . a[^]i) ` {0..ord a - 1}) = card {0..ord a - 1}"
- using card_image[of "\<lambda> i . a[^]i" "{0..ord a - 1}"] by auto
- have "(\<lambda> i . a[^]i) ` {0..ord a - 1} = {a[^]i | i. i \<in> {0..ord a - 1}}" by auto
- hence "card {a[^]i | i. i \<in> {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp
- also have "\<dots> = 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 \<in> 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 :
"\<And>x. x \<in> carrier (mult_of R) \<Longrightarrow> 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)"
--- 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) \<subseteq> h ` generate G K"
proof
fix x assume "x \<in> generate H (h ` K)"
- then obtain r where r: "elts r \<subseteq> (h ` K)" "norm H r = x"
+ then obtain r where r: "elts r \<subseteq> (h ` K)" "Generated_Groups.norm H r = x"
using H.generate_repr_iff img_in_carrier by auto
- from \<open>elts r \<subseteq> (h ` K)\<close> have "norm H r \<in> h ` generate G K"
+ from \<open>elts r \<subseteq> (h ` K)\<close> have "Generated_Groups.norm H r \<in> h ` generate G K"
proof (induct r rule: repr.induct)
case One
have "\<one>\<^bsub>G\<^esub> \<in> 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 \<union> elts x2 \<subseteq> h ` K" by simp
- have "norm H x1 \<in> h ` (generate G K)" using A Mult by simp
- moreover have "norm H x2 \<in> h ` (generate G K)" using A Mult by simp
- ultimately obtain k1 k2 where k1: "k1 \<in> generate G K" "norm H x1 = h k1"
- and k2: "k2 \<in> generate G K" "norm H x2 = h k2" by blast
- hence "norm H (Mult x1 x2) = h (k1 \<otimes> k2)"
+ have "Generated_Groups.norm H x1 \<in> h ` (generate G K)" using A Mult by simp
+ moreover have "Generated_Groups.norm H x2 \<in> h ` (generate G K)" using A Mult by simp
+ ultimately obtain k1 k2 where k1: "k1 \<in> generate G K" "Generated_Groups.norm H x1 = h k1"
+ and k2: "k2 \<in> generate G K" "Generated_Groups.norm H x2 = h k2" by blast
+ hence "Generated_Groups.norm H (Mult x1 x2) = h (k1 \<otimes> 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 \<subseteq> generate H (h ` K)"
proof
fix x assume "x \<in> h ` generate G K"
- then obtain r where r: "elts r \<subseteq> K" "x = h (norm G r)" using G.generate_repr_iff assms by auto
- from \<open>elts r \<subseteq> K\<close> have "h (norm G r) \<in> generate H (h ` K)"
+ then obtain r where r: "elts r \<subseteq> K" "x = h (Generated_Groups.norm G r)" using G.generate_repr_iff assms by auto
+ from \<open>elts r \<subseteq> K\<close> have "h (Generated_Groups.norm G r) \<in> 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 \<in> 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 \<in> 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 \<union> elts x2 \<subseteq> K" by simp
- have "norm G x1 \<in> carrier G"
+ have "Generated_Groups.norm G x1 \<in> carrier G"
by (meson A G.generateE(1) G.generate_repr_iff Un_subset_iff assms subgroup.mem_carrier)
- moreover have "norm G x2 \<in> carrier G"
+ moreover have "Generated_Groups.norm G x2 \<in> 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) \<otimes>\<^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) \<otimes>\<^bsub>H\<^esub> h (Generated_Groups.norm G x2)" by simp
thus ?case using Mult A by (simp add: generate.eng)
qed
thus "x \<in> generate H (h ` K)" using r by simp