# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1554214992 -3600
# Node ID 042ae6ca2c408d83aeaf4fea794b548292176f9f
# Parent  b5574e88092be5c213cf6154663f69fb61fa8e72
The order of a group now follows the HOL Light definition, which is more general

diff -r b5574e88092b -r 042ae6ca2c40 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Apr 02 14:01:52 2019 +0100
+++ b/src/HOL/Algebra/Group.thy	Tue Apr 02 15:23:12 2019 +0100
@@ -550,6 +550,22 @@
     by (metis eq inv_mult_group local.nat_pow_Suc nat_pow_closed pow_mult_distrib xy)
 qed
 
+lemma (in group) pow_eq_div2:
+  fixes m n :: nat
+  assumes x_car: "x \<in> carrier G"
+  assumes pow_eq: "x [^] m = x [^] n"
+  shows "x [^] (m - n) = \<one>"
+proof (cases "m < n")
+  case False
+  have "\<one> \<otimes> x [^] m = x [^] m" by (simp add: x_car)
+  also have "\<dots> = x [^] (m - n) \<otimes> x [^] n"
+    using False by (simp add: nat_pow_mult x_car)
+  also have "\<dots> = x [^] (m - n) \<otimes> x [^] m"
+    by (simp add: pow_eq)
+  finally show ?thesis
+    by (metis nat_pow_closed one_closed right_cancel x_car)
+qed simp
+
 subsection \<open>Submonoids\<close>
 
 locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
@@ -1520,12 +1536,9 @@
   then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
 qed
 
-subsection\<open>Jeremy Avigad's \<open>More_Group\<close> material\<close>
+subsection\<open>The units in any monoid give rise to a group\<close>
 
-text \<open>
-  Show that the units in any monoid give rise to a group.
-
-  The file Residues.thy provides some infrastructure to use
+text \<open>Thanks to Jeremy Avigad. The file Residues.thy provides some infrastructure to use
   facts about the unit group within the ring locale.
 \<close>
 
diff -r b5574e88092b -r 042ae6ca2c40 src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Apr 02 14:01:52 2019 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Tue Apr 02 15:23:12 2019 +0100
@@ -269,28 +269,135 @@
 
 context group begin
 
-lemma pow_eq_div2:
-  fixes m n :: nat
-  assumes x_car: "x \<in> carrier G"
-  assumes pow_eq: "x [^] m = x [^] n"
-  shows "x [^] (m - n) = \<one>"
-proof (cases "m < n")
+definition (in group) ord :: "'a \<Rightarrow> nat" where
+  "ord x \<equiv> (@d. \<forall>n::nat. pow G x n = one G \<longleftrightarrow> d dvd n)"
+
+lemma (in group) pow_eq_id:
+  assumes "x \<in> carrier G"
+  shows "pow G x n = one G \<longleftrightarrow> (ord x) dvd n"
+proof (cases "\<forall>n::nat. pow G x n = one G \<longrightarrow> n = 0")
+  case True
+  show ?thesis
+    unfolding ord_def
+    by (rule someI2 [where a=0]) (auto simp: True)
+next
   case False
-  have "\<one> \<otimes> x [^] m = x [^] m" by (simp add: x_car)
-  also have "\<dots> = x [^] (m - n) \<otimes> x [^] n"
-    using False by (simp add: nat_pow_mult x_car)
-  also have "\<dots> = x [^] (m - n) \<otimes> x [^] m"
-    by (simp add: pow_eq)
-  finally show ?thesis by (simp add: x_car)
-qed simp
+  define N where "N \<equiv> LEAST n::nat. x [^] n = \<one> \<and> n > 0"
+  have N: "x [^] N = \<one> \<and> N > 0"
+    using False
+    apply (simp add: N_def)
+    by (metis (mono_tags, lifting) LeastI)
+  have eq0: "n = 0" if "x [^] n = \<one>" "n < N" for n
+    using N_def not_less_Least that by fastforce
+  show ?thesis
+    unfolding ord_def
+  proof (rule someI2 [where a = N], rule allI)
+    fix n :: "nat"
+    show "(x [^] n = \<one>) \<longleftrightarrow> (N dvd n)"
+    proof (cases "n = 0")
+      case False
+      show ?thesis
+        unfolding dvd_def
+      proof safe
+        assume 1: "x [^] n = \<one>"
+        have "x [^] n = x [^] (n mod N + N * (n div N))"
+          by simp
+        also have "\<dots> = x [^] (n mod N) \<otimes> x [^] (N * (n div N))"
+          by (simp add: assms nat_pow_mult)
+        also have "\<dots> = x [^] (n mod N)"
+          by (metis N assms l_cancel_one nat_pow_closed nat_pow_one nat_pow_pow)
+        finally have "x [^] (n mod N) = \<one>"
+          by (simp add: "1")
+        then have "n mod N = 0"
+          using N eq0 mod_less_divisor by blast
+        then show "\<exists>k. n = N * k"
+          by blast
+      next
+        fix k :: "nat"
+        assume "n = N * k"
+        with N show "x [^] (N * k) = \<one>"
+          by (metis assms nat_pow_one nat_pow_pow)
+      qed
+    qed simp
+  qed blast
+qed
+
+lemma (in group) pow_ord_eq_1 [simp]:
+   "x \<in> carrier G \<Longrightarrow> x [^] ord x = \<one>"
+  by (simp add: pow_eq_id)
 
-definition ord where "ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"
+lemma (in group) int_pow_eq_id:
+  assumes "x \<in> carrier G"
+  shows "(pow G x i = one G \<longleftrightarrow> int (ord x) dvd i)"
+proof (cases i rule: int_cases2)
+  case (nonneg n)
+  then show ?thesis
+    by (simp add: int_pow_int pow_eq_id assms)
+next
+  case (nonpos n)
+  then have "x [^] i = inv (x [^] n)"
+    by (simp add: assms int_pow_int int_pow_neg)
+  then show ?thesis
+    by (simp add: assms pow_eq_id nonpos)
+qed
+
+lemma (in group) int_pow_eq:
+   "x \<in> carrier G \<Longrightarrow> (x [^] m = x [^] n) \<longleftrightarrow> int (ord x) dvd (n - m)"
+  apply (simp flip: int_pow_eq_id)
+  by (metis int_pow_closed int_pow_diff inv_closed r_inv right_cancel)
+
+lemma (in group) ord_eq_0:
+   "x \<in> carrier G \<Longrightarrow> (ord x = 0 \<longleftrightarrow> (\<forall>n::nat. n \<noteq> 0 \<longrightarrow> x [^] n \<noteq> \<one>))"
+  by (auto simp: pow_eq_id)
+
+lemma (in group) ord_unique:
+   "x \<in> carrier G \<Longrightarrow> ord x = d \<longleftrightarrow> (\<forall>n. pow G x n = one G \<longleftrightarrow> d dvd n)"
+  by (meson dvd_antisym dvd_refl pow_eq_id)
+
+lemma (in group) ord_eq_1:
+   "x \<in> carrier G \<Longrightarrow> (ord x = 1 \<longleftrightarrow> x = \<one>)"
+  by (metis pow_eq_id nat_dvd_1_iff_1 nat_pow_eone)
+
+lemma (in group) ord_id [simp]:
+   "ord (one G) = 1"
+  using ord_eq_1 by blast
+
+lemma (in group) ord_inv [simp]:
+   "x \<in> carrier G
+        \<Longrightarrow> ord (m_inv G x) = ord x"
+  by (simp add: ord_unique pow_eq_id nat_pow_inv)
+
+lemma (in group) ord_pow:
+  assumes "x \<in> carrier G" "k dvd ord x" "k \<noteq> 0"
+  shows "ord (pow G x k) = ord x div k"
+proof -
+  have "(x [^] k) [^] (ord x div k) = \<one>"
+    using assms by (simp add: nat_pow_pow)
+  moreover have "ord x dvd k * ord (x [^] k)"
+    by (metis assms(1) pow_ord_eq_1 pow_eq_id nat_pow_closed nat_pow_pow)
+  ultimately show ?thesis
+    by (metis assms div_dvd_div dvd_antisym dvd_triv_left pow_eq_id nat_pow_closed nonzero_mult_div_cancel_left)
+qed
+
+lemma (in group) ord_mul_divides:
+  assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+  shows "ord (x \<otimes> y) dvd (ord x * ord y)"
+apply (simp add: xy flip: pow_eq_id eq)
+  by (metis dvd_triv_left dvd_triv_right eq pow_eq_id one_closed pow_mult_distrib r_one xy)
+
+lemma (in comm_group) abelian_ord_mul_divides:
+   "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
+        \<Longrightarrow> ord (x \<otimes> y) dvd (ord x * ord y)"
+  by (simp add: ord_mul_divides m_comm)
+
+
+definition old_ord where "old_ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"
 
 lemma
-  assumes finite:"finite (carrier G)"
-  assumes a:"a \<in> carrier G"
-  shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> order G"
-    and pow_ord_eq_1: "a [^] ord a = \<one>"
+  assumes finite: "finite (carrier G)"
+  assumes a: "a \<in> carrier G"
+  shows old_ord_ge_1: "1 \<le> old_ord a" and old_ord_le_group_order: "old_ord a \<le> order G"
+    and pow_old_ord_eq_1: "a [^] old_ord a = \<one>"
 proof -
   have "\<not>inj_on (\<lambda>x. a [^] x) {0 .. order G}"
   proof (rule notI)
@@ -315,25 +422,25 @@
     assume "\<not>y < x" with x_y show ?thesis
       by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a])
   qed
-  hence "ord a \<in> {d \<in> {1 .. order G} . a [^] d = \<one>}"
-    unfolding ord_def using Min_in[of "{d \<in> {1 .. order G} . a [^] d = \<one>}"]
+  hence "old_ord a \<in> {d \<in> {1 .. order G} . a [^] d = \<one>}"
+    unfolding old_ord_def using Min_in[of "{d \<in> {1 .. order G} . a [^] d = \<one>}"]
     by fastforce
-  then show "1 \<le> ord a" and "ord a \<le> order G" and "a [^] ord a = \<one>"
+  then show "1 \<le> old_ord a" and "old_ord a \<le> order G" and "a [^] old_ord a = \<one>"
     by (auto simp: order_def)
 qed
 
 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
+  using assms old_ord_ge_1 pow_old_ord_eq_1 by auto
 
-lemma ord_min:
-  assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a [^] d = \<one>" shows "ord a \<le> d"
+lemma old_ord_min:
+  assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a [^] d = \<one>" shows "old_ord a \<le> d"
 proof -
   define Ord where "Ord = {d \<in> {1..order G}. a [^] d = \<one>}"
   have fin: "finite Ord" by (auto simp: Ord_def)
-  have in_ord: "ord a \<in> Ord"
-    using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
+  have in_ord: "old_ord a \<in> Ord"
+    using assms pow_old_ord_eq_1 old_ord_ge_1 old_ord_le_group_order by (auto simp: Ord_def)
   then have "Ord \<noteq> {}" by auto
 
   show ?thesis
@@ -341,13 +448,49 @@
     case True
     then have "d \<in> Ord" using assms by (auto simp: Ord_def)
     with fin in_ord show ?thesis
-      unfolding ord_def Ord_def[symmetric] by simp
+      unfolding old_ord_def Ord_def[symmetric] by simp
   next
     case False
     then show ?thesis using in_ord by (simp add: Ord_def)
   qed
 qed
 
+lemma old_ord_dvd_pow_eq_1 :
+  assumes "finite (carrier G)" "a \<in> carrier G" "a [^] k = \<one>"
+  shows "old_ord a dvd k"
+proof -
+  define r where "r = k mod old_ord a"
+
+  define r q where "r = k mod old_ord a" and "q = k div old_ord a"
+  then have q: "k = q * old_ord a + r"
+    by (simp add: div_mult_mod_eq)
+  hence "a[^]k = (a[^]old_ord a)[^]q \<otimes> a[^]r"
+      using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
+  hence "a[^]k = a[^]r" using assms by (simp add: pow_old_ord_eq_1)
+  hence "a[^]r = \<one>" using assms(3) by simp
+  have "r < old_ord a" using old_ord_ge_1[OF assms(1-2)] by (simp add: r_def)
+  hence "r = 0" using \<open>a[^]r = \<one>\<close> old_ord_def[of a] old_ord_min[of r a] assms(1-2) by linarith
+  thus ?thesis using q by simp
+qed
+
+lemma (in group) ord_iff_old_ord:
+  assumes finite: "finite (carrier G)"
+  assumes a: "a \<in> carrier G"
+  shows  "ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"
+proof -
+  have "a [^] ord a = \<one>"
+    using a pow_ord_eq_1 by blast
+  then show ?thesis
+    by (metis a dvd_antisym local.finite old_ord_def old_ord_dvd_pow_eq_1 pow_eq_id pow_old_ord_eq_1)
+qed
+
+lemma
+  assumes finite: "finite (carrier G)"
+  assumes a: "a \<in> carrier G"
+  shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> 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)
+
 lemma ord_inj:
   assumes finite: "finite (carrier G)"
   assumes a: "a \<in> carrier G"
@@ -366,7 +509,8 @@
 
     hence y_x:"y - x \<in> {d \<in> {1.. order G}. a [^] d = \<one>}" using y_x_range by blast
     have "min (y - x) (ord a) = ord a"
-      using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a [^] d = \<one>}\<close> y_x] ord_def by auto
+      using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a [^] d = \<one>}\<close> y_x]
+      by (simp add: a group.ord_iff_old_ord is_group local.finite) 
     with \<open>y - x < ord a\<close> have False by linarith
   }
   note X = this
@@ -392,13 +536,13 @@
   }
   moreover
   { assume "x = ord a" "y < ord a"
-    hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto
+    hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
     hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
     hence False using A by fastforce
   }
   moreover
   { assume "y = ord a" "x < ord a"
-    hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto
+    hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
     hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
     hence False using A by fastforce
   }
@@ -416,7 +560,7 @@
     then have "x = q * ord a + r"
       by (simp add: div_mult_mod_eq)
     hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
-      using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
+      using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
     hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
     have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
     hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
@@ -489,25 +633,7 @@
     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"
-proof -
-  define r where "r = k mod ord a"
-
-  define r q where "r = k mod ord a" and "q = k div ord a"
-  then have q: "k = q * ord a + r"
-    by (simp add: div_mult_mod_eq)
-  hence "a[^]k = (a[^]ord a)[^]q \<otimes> a[^]r"
-      using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
-  hence "a[^]k = a[^]r" using assms by (simp add: pow_ord_eq_1)
-  hence "a[^]r = \<one>" using assms(3) by simp
-  have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)
-  hence "r = 0" using \<open>a[^]r = \<one>\<close> ord_def[of a] ord_min[of r a] assms(1-2) by linarith
-  thus ?thesis using q by simp
+    using assms(2) pow_ord_eq_1 by (metis nat_pow_one nat_pow_pow)
 qed
 
 lemma dvd_gcd :
@@ -525,10 +651,11 @@
   shows "ord (a[^]n) = ord a div gcd n (ord a)"
 proof -
   have "(a[^]n) [^] ord a = (a [^] ord a) [^] n"
-    by (simp add: mult.commute nat_pow_pow)
+    by (simp add: nat_pow_pow pow_eq_id)
   hence "(a[^]n) [^] ord a = \<one>" by (simp add: pow_ord_eq_1)
   obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd)
-  hence "(a[^]n) [^] (ord a div gcd n (ord a)) = (a [^] ord a)[^]q"  by (simp add : nat_pow_pow)
+  hence "(a[^]n) [^] (ord a div gcd n (ord a)) = (a [^] ord a)[^]q"
+    using a nat_pow_pow by presburger
   hence pow_eq_1: "(a[^]n) [^] (ord a div gcd n (ord a)) = \<one>"
      by (auto simp add : pow_ord_eq_1[of a])
   have "ord a \<ge> 1" using ord_ge_1 by simp
@@ -550,7 +677,7 @@
     assume d_lt:"d < ord a div gcd n (ord a)"
     hence pow_nd:"a[^](n*d)  = \<one>" using d_elem
       by (simp add : nat_pow_pow)
-    hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1)
+    hence "ord a dvd n*d" using assms pow_eq_id by blast
     then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel)
     hence prod_eq:"(ord a div gcd n (ord a)) * q = (n div gcd n (ord a)) * d"
       by (simp add: dvd_div_mult)
@@ -576,14 +703,9 @@
                         \<Longrightarrow> d\<ge>ord a div gcd n (ord a)" by fastforce
   have fin:"finite {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}" by auto
   thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem]
-    unfolding ord_def by simp
+    by (simp add: group.ord_iff_old_ord is_group)
 qed
 
-lemma ord_1_eq_1 :
-  assumes "finite (carrier G)"
-  shows "ord \<one> = 1"
- using assms ord_ge_1 ord_min[of 1 \<one>] by force
-
 lemma element_generates_subgroup:
   assumes finite[simp]: "finite (carrier G)"
   assumes a[simp]: "a \<in> carrier G"
@@ -592,7 +714,7 @@
         generate_pow_on_finite_carrier[OF assms]
   unfolding ord_elems[OF assms] by auto
 
-lemma ord_dvd_group_order: (* <- DELETE *)
+lemma ord_dvd_group_order: 
   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)
@@ -822,7 +944,7 @@
       fix x assume "x \<in> {a[^]n | n. n \<in> {1 .. d}}"
       then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" by auto
       have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
-      hence "x[^]d = \<one>" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce
+      hence "x[^]d = \<one>" using ord_a G.pow_ord_eq_1[OF a] by fastforce
       thus "x \<in> {x \<in> carrier (mult_of R). x[^]d = \<one>}" using G.nat_pow_closed[OF a] n by blast
     qed
 
@@ -844,7 +966,7 @@
   proof
     { fix x assume x:"x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"
       hence "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"
-        by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric])
+        by (simp add: G.pow_ord_eq_1[of x, symmetric])
       then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" using set_eq1 by blast
       hence "x \<in> ?R" using x by fast
     } thus "?L \<subseteq> ?R" by blast