more approproiate placement of theories MiscAlgebra and Multiplicate_Group
authorhaftmann
Thu Apr 06 08:33:37 2017 +0200 (2017-04-06)
changeset 65416f707dbcf11e3
parent 65415 8cd54b18b68b
child 65417 fc41a5650fb1
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
src/HOL/Algebra/More_Finite_Product.thy
src/HOL/Algebra/More_Group.thy
src/HOL/Algebra/More_Ring.thy
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/More_Finite_Product.thy	Thu Apr 06 08:33:37 2017 +0200
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Title:      HOL/Algebra/More_Finite_Product.thy
     1.5 +    Author:     Jeremy Avigad
     1.6 +*)
     1.7 +
     1.8 +section \<open>More on finite products\<close>
     1.9 +
    1.10 +theory More_Finite_Product
    1.11 +imports
    1.12 +  More_Group
    1.13 +begin
    1.14 +
    1.15 +lemma (in comm_monoid) finprod_UN_disjoint:
    1.16 +  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
    1.17 +     (A i) Int (A j) = {}) \<longrightarrow>
    1.18 +      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
    1.19 +        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
    1.20 +  apply (induct set: finite)
    1.21 +  apply force
    1.22 +  apply clarsimp
    1.23 +  apply (subst finprod_Un_disjoint)
    1.24 +  apply blast
    1.25 +  apply (erule finite_UN_I)
    1.26 +  apply blast
    1.27 +  apply (fastforce)
    1.28 +  apply (auto intro!: funcsetI finprod_closed)
    1.29 +  done
    1.30 +
    1.31 +lemma (in comm_monoid) finprod_Union_disjoint:
    1.32 +  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
    1.33 +      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
    1.34 +   ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
    1.35 +  apply (frule finprod_UN_disjoint [of C id f])
    1.36 +  apply auto
    1.37 +  done
    1.38 +
    1.39 +lemma (in comm_monoid) finprod_one:
    1.40 +    "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
    1.41 +  by (induct set: finite) auto
    1.42 +
    1.43 +
    1.44 +(* need better simplification rules for rings *)
    1.45 +(* the next one holds more generally for abelian groups *)
    1.46 +
    1.47 +lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
    1.48 +  by (metis minus_equality)
    1.49 +
    1.50 +lemma (in domain) square_eq_one:
    1.51 +  fixes x
    1.52 +  assumes [simp]: "x : carrier R"
    1.53 +    and "x \<otimes> x = \<one>"
    1.54 +  shows "x = \<one> | x = \<ominus>\<one>"
    1.55 +proof -
    1.56 +  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
    1.57 +    by (simp add: ring_simprules)
    1.58 +  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
    1.59 +    by (simp add: ring_simprules)
    1.60 +  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
    1.61 +  then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
    1.62 +    by (intro integral, auto)
    1.63 +  then show ?thesis
    1.64 +    apply auto
    1.65 +    apply (erule notE)
    1.66 +    apply (rule sum_zero_eq_neg)
    1.67 +    apply auto
    1.68 +    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
    1.69 +    apply (simp add: ring_simprules)
    1.70 +    apply (rule sum_zero_eq_neg)
    1.71 +    apply auto
    1.72 +    done
    1.73 +qed
    1.74 +
    1.75 +lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
    1.76 +  by (metis Units_closed Units_l_inv square_eq_one)
    1.77 +
    1.78 +
    1.79 +text \<open>
    1.80 +  The following translates theorems about groups to the facts about
    1.81 +  the units of a ring. (The list should be expanded as more things are
    1.82 +  needed.)
    1.83 +\<close>
    1.84 +
    1.85 +lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
    1.86 +  by (rule finite_subset) auto
    1.87 +
    1.88 +lemma (in monoid) units_of_pow:
    1.89 +  fixes n :: nat
    1.90 +  shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n"
    1.91 +  apply (induct n)
    1.92 +  apply (auto simp add: units_group group.is_monoid
    1.93 +    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
    1.94 +  done
    1.95 +
    1.96 +lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
    1.97 +    \<Longrightarrow> a (^) card(Units R) = \<one>"
    1.98 +  apply (subst units_of_carrier [symmetric])
    1.99 +  apply (subst units_of_one [symmetric])
   1.100 +  apply (subst units_of_pow [symmetric])
   1.101 +  apply assumption
   1.102 +  apply (rule comm_group.power_order_eq_one)
   1.103 +  apply (rule units_comm_group)
   1.104 +  apply (unfold units_of_def, auto)
   1.105 +  done
   1.106 +
   1.107 +end
   1.108 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Algebra/More_Group.thy	Thu Apr 06 08:33:37 2017 +0200
     2.3 @@ -0,0 +1,136 @@
     2.4 +(*  Title:      HOL/Algebra/More_Group.thy
     2.5 +    Author:     Jeremy Avigad
     2.6 +*)
     2.7 +
     2.8 +section \<open>More on groups\<close>
     2.9 +
    2.10 +theory More_Group
    2.11 +imports
    2.12 +  Ring
    2.13 +begin
    2.14 +
    2.15 +text \<open>
    2.16 +  Show that the units in any monoid give rise to a group.
    2.17 +
    2.18 +  The file Residues.thy provides some infrastructure to use
    2.19 +  facts about the unit group within the ring locale.
    2.20 +\<close>
    2.21 +
    2.22 +definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
    2.23 +  "units_of G == (| carrier = Units G,
    2.24 +     Group.monoid.mult = Group.monoid.mult G,
    2.25 +     one  = one G |)"
    2.26 +
    2.27 +lemma (in monoid) units_group: "group(units_of G)"
    2.28 +  apply (unfold units_of_def)
    2.29 +  apply (rule groupI)
    2.30 +  apply auto
    2.31 +  apply (subst m_assoc)
    2.32 +  apply auto
    2.33 +  apply (rule_tac x = "inv x" in bexI)
    2.34 +  apply auto
    2.35 +  done
    2.36 +
    2.37 +lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
    2.38 +  apply (rule group.group_comm_groupI)
    2.39 +  apply (rule units_group)
    2.40 +  apply (insert comm_monoid_axioms)
    2.41 +  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    2.42 +  apply auto
    2.43 +  done
    2.44 +
    2.45 +lemma units_of_carrier: "carrier (units_of G) = Units G"
    2.46 +  unfolding units_of_def by auto
    2.47 +
    2.48 +lemma units_of_mult: "mult(units_of G) = mult G"
    2.49 +  unfolding units_of_def by auto
    2.50 +
    2.51 +lemma units_of_one: "one(units_of G) = one G"
    2.52 +  unfolding units_of_def by auto
    2.53 +
    2.54 +lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
    2.55 +  apply (rule sym)
    2.56 +  apply (subst m_inv_def)
    2.57 +  apply (rule the1_equality)
    2.58 +  apply (rule ex_ex1I)
    2.59 +  apply (subst (asm) Units_def)
    2.60 +  apply auto
    2.61 +  apply (erule inv_unique)
    2.62 +  apply auto
    2.63 +  apply (rule Units_closed)
    2.64 +  apply (simp_all only: units_of_carrier [symmetric])
    2.65 +  apply (insert units_group)
    2.66 +  apply auto
    2.67 +  apply (subst units_of_mult [symmetric])
    2.68 +  apply (subst units_of_one [symmetric])
    2.69 +  apply (erule group.r_inv, assumption)
    2.70 +  apply (subst units_of_mult [symmetric])
    2.71 +  apply (subst units_of_one [symmetric])
    2.72 +  apply (erule group.l_inv, assumption)
    2.73 +  done
    2.74 +
    2.75 +lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
    2.76 +  unfolding inj_on_def by auto
    2.77 +
    2.78 +lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
    2.79 +  apply (auto simp add: image_def)
    2.80 +  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
    2.81 +  apply auto
    2.82 +(* auto should get this. I suppose we need "comm_monoid_simprules"
    2.83 +   for ac_simps rewriting. *)
    2.84 +  apply (subst m_assoc [symmetric])
    2.85 +  apply auto
    2.86 +  done
    2.87 +
    2.88 +lemma (in group) l_cancel_one [simp]:
    2.89 +    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
    2.90 +  apply auto
    2.91 +  apply (subst l_cancel [symmetric])
    2.92 +  prefer 4
    2.93 +  apply (erule ssubst)
    2.94 +  apply auto
    2.95 +  done
    2.96 +
    2.97 +lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
    2.98 +    (a \<otimes> x = x) = (a = one G)"
    2.99 +  apply auto
   2.100 +  apply (subst r_cancel [symmetric])
   2.101 +  prefer 4
   2.102 +  apply (erule ssubst)
   2.103 +  apply auto
   2.104 +  done
   2.105 +
   2.106 +(* Is there a better way to do this? *)
   2.107 +lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   2.108 +    (x = x \<otimes> a) = (a = one G)"
   2.109 +  apply (subst eq_commute)
   2.110 +  apply simp
   2.111 +  done
   2.112 +
   2.113 +lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   2.114 +    (x = a \<otimes> x) = (a = one G)"
   2.115 +  apply (subst eq_commute)
   2.116 +  apply simp
   2.117 +  done
   2.118 +
   2.119 +(* This should be generalized to arbitrary groups, not just commutative
   2.120 +   ones, using Lagrange's theorem. *)
   2.121 +
   2.122 +lemma (in comm_group) power_order_eq_one:
   2.123 +  assumes fin [simp]: "finite (carrier G)"
   2.124 +    and a [simp]: "a : carrier G"
   2.125 +  shows "a (^) card(carrier G) = one G"
   2.126 +proof -
   2.127 +  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
   2.128 +    by (subst (2) finprod_reindex [symmetric],
   2.129 +      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   2.130 +  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
   2.131 +    by (auto simp add: finprod_multf Pi_def)
   2.132 +  also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
   2.133 +    by (auto simp add: finprod_const)
   2.134 +  finally show ?thesis
   2.135 +(* uses the preceeding lemma *)
   2.136 +    by auto
   2.137 +qed
   2.138 +
   2.139 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Algebra/More_Ring.thy	Thu Apr 06 08:33:37 2017 +0200
     3.3 @@ -0,0 +1,77 @@
     3.4 +(*  Title:      HOL/Algebra/More_Group.thy
     3.5 +    Author:     Jeremy Avigad
     3.6 +*)
     3.7 +
     3.8 +section \<open>More on rings etc.\<close>
     3.9 +
    3.10 +theory More_Ring
    3.11 +imports
    3.12 +  Ring
    3.13 +begin
    3.14 +
    3.15 +lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
    3.16 +  apply (unfold_locales)
    3.17 +  apply (insert cring_axioms, auto)
    3.18 +  apply (rule trans)
    3.19 +  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
    3.20 +  apply assumption
    3.21 +  apply (subst m_assoc)
    3.22 +  apply auto
    3.23 +  apply (unfold Units_def)
    3.24 +  apply auto
    3.25 +  done
    3.26 +
    3.27 +lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
    3.28 +    x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
    3.29 +  apply (subgoal_tac "x : Units G")
    3.30 +  apply (subgoal_tac "y = inv x \<otimes> \<one>")
    3.31 +  apply simp
    3.32 +  apply (erule subst)
    3.33 +  apply (subst m_assoc [symmetric])
    3.34 +  apply auto
    3.35 +  apply (unfold Units_def)
    3.36 +  apply auto
    3.37 +  done
    3.38 +
    3.39 +lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
    3.40 +  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
    3.41 +  apply (rule inv_char)
    3.42 +  apply auto
    3.43 +  apply (subst m_comm, auto)
    3.44 +  done
    3.45 +
    3.46 +lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
    3.47 +  apply (rule inv_char)
    3.48 +  apply (auto simp add: l_minus r_minus)
    3.49 +  done
    3.50 +
    3.51 +lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
    3.52 +    inv x = inv y \<Longrightarrow> x = y"
    3.53 +  apply (subgoal_tac "inv(inv x) = inv(inv y)")
    3.54 +  apply (subst (asm) Units_inv_inv)+
    3.55 +  apply auto
    3.56 +  done
    3.57 +
    3.58 +lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
    3.59 +  apply (unfold Units_def)
    3.60 +  apply auto
    3.61 +  apply (rule_tac x = "\<ominus> \<one>" in bexI)
    3.62 +  apply auto
    3.63 +  apply (simp add: l_minus r_minus)
    3.64 +  done
    3.65 +
    3.66 +lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
    3.67 +  apply (rule inv_char)
    3.68 +  apply auto
    3.69 +  done
    3.70 +
    3.71 +lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
    3.72 +  apply auto
    3.73 +  apply (subst Units_inv_inv [symmetric])
    3.74 +  apply auto
    3.75 +  done
    3.76 +
    3.77 +lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
    3.78 +  by (metis Units_inv_inv inv_one)
    3.79 +
    3.80 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Thu Apr 06 08:33:37 2017 +0200
     4.3 @@ -0,0 +1,904 @@
     4.4 +(*  Title:      HOL/Algebra/Multiplicative_Group.thy
     4.5 +    Author:     Simon Wimmer
     4.6 +    Author:     Lars Noschinski
     4.7 +*)
     4.8 +
     4.9 +theory Multiplicative_Group
    4.10 +imports
    4.11 +  Complex_Main
    4.12 +  Group
    4.13 +  More_Group
    4.14 +  More_Finite_Product
    4.15 +  Coset
    4.16 +  UnivPoly
    4.17 +begin
    4.18 +
    4.19 +section {* Simplification Rules for Polynomials *}
    4.20 +text_raw {* \label{sec:simp-rules} *}
    4.21 +
    4.22 +lemma (in ring_hom_cring) hom_sub[simp]:
    4.23 +  assumes "x \<in> carrier R" "y \<in> carrier R"
    4.24 +  shows "h (x \<ominus> y) = h x \<ominus>\<^bsub>S\<^esub> h y"
    4.25 +  using assms by (simp add: R.minus_eq S.minus_eq)
    4.26 +
    4.27 +context UP_ring begin
    4.28 +
    4.29 +lemma deg_nzero_nzero:
    4.30 +  assumes deg_p_nzero: "deg R p \<noteq> 0"
    4.31 +  shows "p \<noteq> \<zero>\<^bsub>P\<^esub>"
    4.32 +  using deg_zero deg_p_nzero by auto
    4.33 +
    4.34 +lemma deg_add_eq:
    4.35 +  assumes c: "p \<in> carrier P" "q \<in> carrier P"
    4.36 +  assumes "deg R q \<noteq> deg R p"
    4.37 +  shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
    4.38 +proof -
    4.39 +  let ?m = "max (deg R p) (deg R q)"
    4.40 +  from assms have "coeff P p ?m = \<zero> \<longleftrightarrow> coeff P q ?m \<noteq> \<zero>"
    4.41 +    by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)
    4.42 +  then have "coeff P (p \<oplus>\<^bsub>P\<^esub> q) ?m \<noteq> \<zero>"
    4.43 +    using assms by auto
    4.44 +  then have "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<ge> ?m"
    4.45 +    using assms by (blast intro: deg_belowI)
    4.46 +  with deg_add[OF c] show ?thesis by arith
    4.47 +qed
    4.48 +
    4.49 +lemma deg_minus_eq:
    4.50 +  assumes "p \<in> carrier P" "q \<in> carrier P" "deg R q \<noteq> deg R p"
    4.51 +  shows "deg R (p \<ominus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
    4.52 +  using assms by (simp add: deg_add_eq a_minus_def)
    4.53 +
    4.54 +end
    4.55 +
    4.56 +context UP_cring begin
    4.57 +
    4.58 +lemma evalRR_add:
    4.59 +  assumes "p \<in> carrier P" "q \<in> carrier P"
    4.60 +  assumes x:"x \<in> carrier R"
    4.61 +  shows "eval R R id x (p \<oplus>\<^bsub>P\<^esub> q) = eval R R id x p \<oplus> eval R R id x q"
    4.62 +proof -
    4.63 +  interpret UP_pre_univ_prop R R id by unfold_locales simp
    4.64 +  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
    4.65 +  show ?thesis using assms by simp
    4.66 +qed
    4.67 +
    4.68 +lemma evalRR_sub:
    4.69 +  assumes "p \<in> carrier P" "q \<in> carrier P"
    4.70 +  assumes x:"x \<in> carrier R"
    4.71 +  shows "eval R R id x (p \<ominus>\<^bsub>P\<^esub> q) = eval R R id x p \<ominus> eval R R id x q"
    4.72 +proof -
    4.73 +  interpret UP_pre_univ_prop R R id by unfold_locales simp
    4.74 +  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
    4.75 +  show ?thesis using assms by simp
    4.76 +qed
    4.77 +
    4.78 +lemma evalRR_mult:
    4.79 +  assumes "p \<in> carrier P" "q \<in> carrier P"
    4.80 +  assumes x:"x \<in> carrier R"
    4.81 +  shows "eval R R id x (p \<otimes>\<^bsub>P\<^esub> q) = eval R R id x p \<otimes> eval R R id x q"
    4.82 +proof -
    4.83 +  interpret UP_pre_univ_prop R R id by unfold_locales simp
    4.84 +  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
    4.85 +  show ?thesis using assms by simp
    4.86 +qed
    4.87 +
    4.88 +lemma evalRR_monom:
    4.89 +  assumes a: "a \<in> carrier R" and x: "x \<in> carrier R"
    4.90 +  shows "eval R R id x (monom P a d) = a \<otimes> x (^) d"
    4.91 +proof -
    4.92 +  interpret UP_pre_univ_prop R R id by unfold_locales simp
    4.93 +  show ?thesis using assms by (simp add: eval_monom)
    4.94 +qed
    4.95 +
    4.96 +lemma evalRR_one:
    4.97 +  assumes x: "x \<in> carrier R"
    4.98 +  shows "eval R R id x \<one>\<^bsub>P\<^esub> = \<one>"
    4.99 +proof -
   4.100 +  interpret UP_pre_univ_prop R R id by unfold_locales simp
   4.101 +  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
   4.102 +  show ?thesis using assms by simp
   4.103 +qed
   4.104 +
   4.105 +lemma carrier_evalRR:
   4.106 +  assumes x: "x \<in> carrier R" and "p \<in> carrier P"
   4.107 +  shows "eval R R id x p \<in> carrier R"
   4.108 +proof -
   4.109 +  interpret UP_pre_univ_prop R R id by unfold_locales simp
   4.110 +  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
   4.111 +  show ?thesis using assms by simp
   4.112 +qed
   4.113 +
   4.114 +lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR
   4.115 +
   4.116 +end
   4.117 +
   4.118 +
   4.119 +
   4.120 +section {* Properties of the Euler @{text \<phi>}-function *}
   4.121 +text_raw {* \label{sec:euler-phi} *}
   4.122 +
   4.123 +text{*
   4.124 +  In this section we prove that for every positive natural number the equation
   4.125 +  $\sum_{d | n}^n \varphi(d) = n$ holds.
   4.126 +*}
   4.127 +
   4.128 +lemma dvd_div_ge_1 :
   4.129 +  fixes a b :: nat
   4.130 +  assumes "a \<ge> 1" "b dvd a"
   4.131 +  shows "a div b \<ge> 1"
   4.132 +proof -
   4.133 +  from \<open>b dvd a\<close> obtain c where "a = b * c" ..
   4.134 +  with \<open>a \<ge> 1\<close> show ?thesis by simp
   4.135 +qed
   4.136 +
   4.137 +lemma dvd_nat_bounds :
   4.138 + fixes n p :: nat
   4.139 + assumes "p > 0" "n dvd p"
   4.140 + shows "n > 0 \<and> n \<le> p"
   4.141 + using assms by (simp add: dvd_pos_nat dvd_imp_le)
   4.142 +
   4.143 +(* Deviates from the definition given in the library in number theory *)
   4.144 +definition phi' :: "nat => nat"
   4.145 +  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
   4.146 +
   4.147 +notation (latex_output)
   4.148 +  phi' ("\<phi> _")
   4.149 +
   4.150 +lemma phi'_nonzero :
   4.151 +  assumes "m > 0"
   4.152 +  shows "phi' m > 0"
   4.153 +proof -
   4.154 +  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" using assms by simp
   4.155 +  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)
   4.156 +  thus ?thesis unfolding phi'_def by simp
   4.157 +qed
   4.158 +
   4.159 +lemma dvd_div_eq_1:
   4.160 +  fixes a b c :: nat
   4.161 +  assumes "c dvd a" "c dvd b" "a div c = b div c"
   4.162 +  shows "a = b" using assms dvd_mult_div_cancel[OF `c dvd a`] dvd_mult_div_cancel[OF `c dvd b`]
   4.163 +                by presburger
   4.164 +
   4.165 +lemma dvd_div_eq_2:
   4.166 +  fixes a b c :: nat
   4.167 +  assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"
   4.168 +  shows "a = b"
   4.169 +  proof -
   4.170 +  have "a > 0" "a \<le> c" using dvd_nat_bounds[OF assms(1-2)] by auto
   4.171 +  have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
   4.172 +  also have "\<dots> = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
   4.173 +  finally show "a = b" using `c>0` dvd_div_ge_1[OF _ `a dvd c`] by fastforce
   4.174 +qed
   4.175 +
   4.176 +lemma div_mult_mono:
   4.177 +  fixes a b c :: nat
   4.178 +  assumes "a > 0" "a\<le>d"
   4.179 +  shows "a * b div d \<le> b"
   4.180 +proof -
   4.181 +  have "a*b div d \<le> b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger
   4.182 +  thus ?thesis using assms by force
   4.183 +qed
   4.184 +
   4.185 +text{*
   4.186 +  We arrive at the main result of this section:
   4.187 +  For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.
   4.188 +
   4.189 +  The outline of the proof for this lemma is as follows:
   4.190 +  We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.
   4.191 +  We analyze the reduced form $a/d = m/n$ for any of those fractions.
   4.192 +  We want to know how many fractions $m/n$ have the reduced form denominator $d$.
   4.193 +  The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.
   4.194 +  Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. @{term "gcd a d = 1"}.
   4.195 +  This number is exactly @{term "phi' d"}.
   4.196 +
   4.197 +  Finally, by counting the fractions $m/n$ according to their reduced form denominator,
   4.198 +  we get: @{term [display] "(\<Sum>d | d dvd n . phi' d) = n"}.
   4.199 +  To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$
   4.200 +  \begin{itemize}
   4.201 +    \item the set of reduced form numerators @{term "{a. (1::nat) \<le> a \<and> a \<le> d \<and> coprime a d}"}
   4.202 +    \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,
   4.203 +      i.e. the set @{term "{m \<in> {1::nat .. n}. n div gcd m n = d}"}
   4.204 +  \end{itemize}
   4.205 +  We show that @{term "\<lambda>a. a*n div d"} with the inverse @{term "\<lambda>a. a div gcd a n"} is
   4.206 +  a bijection between theses sets, thus yielding the equality
   4.207 +  @{term [display] "phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"}
   4.208 +  This gives us
   4.209 +  @{term [display] "(\<Sum>d | d dvd n . phi' d)
   4.210 +          = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"}
   4.211 +  and by showing
   4.212 +  @{term "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}"}
   4.213 +  (this is our counting argument) the thesis follows.
   4.214 +*}
   4.215 +lemma sum_phi'_factors :
   4.216 + fixes n :: nat
   4.217 + assumes "n > 0"
   4.218 + shows "(\<Sum>d | d dvd n. phi' d) = n"
   4.219 +proof -
   4.220 +  { fix d assume "d dvd n" then obtain q where q: "n = d * q" ..
   4.221 +    have "card {a. 1 \<le> a \<and> a \<le> d \<and> coprime a d} = card {m \<in> {1 .. n}.  n div gcd m n = d}"
   4.222 +         (is "card ?RF = card ?F")
   4.223 +    proof (rule card_bij_eq)
   4.224 +      { fix a b assume "a * n div d = b * n div d"
   4.225 +        hence "a * (n div d) = b * (n div d)"
   4.226 +          using dvd_div_mult[OF `d dvd n`] by (fastforce simp add: mult.commute)
   4.227 +        hence "a = b" using dvd_div_ge_1[OF _ `d dvd n`] `n>0`
   4.228 +          by (simp add: mult.commute nat_mult_eq_cancel1)
   4.229 +      } thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
   4.230 +      { fix a assume a:"a\<in>?RF"
   4.231 +        hence "a * (n div d) \<ge> 1" using `n>0` dvd_div_ge_1[OF _ `d dvd n`] by simp
   4.232 +        hence ge_1:"a * n div d \<ge> 1" by (simp add: `d dvd n` div_mult_swap)
   4.233 +        have le_n:"a * n div d \<le> n" using div_mult_mono a by simp
   4.234 +        have "gcd (a * n div d) n = n div d * gcd a d"
   4.235 +          by (simp add: gcd_mult_distrib_nat q ac_simps)
   4.236 +        hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
   4.237 +        hence "a * n div d \<in> ?F"
   4.238 +          using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel)
   4.239 +      } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
   4.240 +      { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
   4.241 +        hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
   4.242 +        hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
   4.243 +      } thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast
   4.244 +      { fix m assume "m \<in> ?F"
   4.245 +        hence "m div gcd m n \<in> ?RF" using dvd_div_ge_1
   4.246 +          by (fastforce simp add: div_le_mono div_gcd_coprime)
   4.247 +      } thus "(\<lambda>a. a div gcd a n) ` ?F \<subseteq> ?RF" by blast
   4.248 +    qed force+
   4.249 +  } hence phi'_eq:"\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
   4.250 +      unfolding phi'_def by presburger
   4.251 +  have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF `n>0`] by force
   4.252 +  have "(\<Sum>d | d dvd n. phi' d)
   4.253 +                 = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
   4.254 +    using card_UN_disjoint[OF fin, of "(\<lambda>d. {m \<in> {1 .. n}. n div gcd m n = d})"] phi'_eq
   4.255 +    by fastforce
   4.256 +  also have "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")
   4.257 +  proof
   4.258 +    show "?L \<supseteq> ?R"
   4.259 +    proof
   4.260 +      fix m assume m: "m \<in> ?R"
   4.261 +      thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
   4.262 +        by (simp add: dvd_mult_div_cancel)
   4.263 +    qed
   4.264 +  qed fastforce
   4.265 +  finally show ?thesis by force
   4.266 +qed
   4.267 +
   4.268 +section {* Order of an Element of a Group *}
   4.269 +text_raw {* \label{sec:order-elem} *}
   4.270 +
   4.271 +
   4.272 +context group begin
   4.273 +
   4.274 +lemma pow_eq_div2 :
   4.275 +  fixes m n :: nat
   4.276 +  assumes x_car: "x \<in> carrier G"
   4.277 +  assumes pow_eq: "x (^) m = x (^) n"
   4.278 +  shows "x (^) (m - n) = \<one>"
   4.279 +proof (cases "m < n")
   4.280 +  case False
   4.281 +  have "\<one> \<otimes> x (^) m = x (^) m" by (simp add: x_car)
   4.282 +  also have "\<dots> = x (^) (m - n) \<otimes> x (^) n"
   4.283 +    using False by (simp add: nat_pow_mult x_car)
   4.284 +  also have "\<dots> = x (^) (m - n) \<otimes> x (^) m"
   4.285 +    by (simp add: pow_eq)
   4.286 +  finally show ?thesis by (simp add: x_car)
   4.287 +qed simp
   4.288 +
   4.289 +definition ord where "ord a = Min {d \<in> {1 .. order G} . a (^) d = \<one>}"
   4.290 +
   4.291 +lemma
   4.292 +  assumes finite:"finite (carrier G)"
   4.293 +  assumes a:"a \<in> carrier G"
   4.294 +  shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> order G"
   4.295 +    and pow_ord_eq_1: "a (^) ord a = \<one>"
   4.296 +proof -
   4.297 +  have "\<not>inj_on (\<lambda>x. a (^) x) {0 .. order G}"
   4.298 +  proof (rule notI)
   4.299 +    assume A: "inj_on (\<lambda>x. a (^) x) {0 .. order G}"
   4.300 +    have "order G + 1 = card {0 .. order G}" by simp
   4.301 +    also have "\<dots> = card ((\<lambda>x. a (^) x) ` {0 .. order G})" (is "_ = card ?S")
   4.302 +      using A by (simp add: card_image)
   4.303 +    also have "?S = {a (^) x | x. x \<in> {0 .. order G}}" by blast
   4.304 +    also have "\<dots> \<subseteq> carrier G" (is "?S \<subseteq> _") using a by blast
   4.305 +    then have "card ?S \<le> order G" unfolding order_def
   4.306 +      by (rule card_mono[OF finite])
   4.307 +    finally show False by arith
   4.308 +  qed
   4.309 +
   4.310 +  then obtain x y where x_y:"x \<noteq> y" "x \<in> {0 .. order G}" "y \<in> {0 .. order G}"
   4.311 +                        "a (^) x = a (^) y" unfolding inj_on_def by blast
   4.312 +  obtain d where "1 \<le> d" "a (^) d = \<one>" "d \<le> order G"
   4.313 +  proof cases
   4.314 +    assume "y < x" with x_y show ?thesis
   4.315 +      by (intro that[where d="x - y"]) (auto simp add: pow_eq_div2[OF a])
   4.316 +  next
   4.317 +    assume "\<not>y < x" with x_y show ?thesis
   4.318 +      by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a])
   4.319 +  qed
   4.320 +  hence "ord a \<in> {d \<in> {1 .. order G} . a (^) d = \<one>}"
   4.321 +    unfolding ord_def using Min_in[of "{d \<in> {1 .. order G} . a (^) d = \<one>}"]
   4.322 +    by fastforce
   4.323 +  then show "1 \<le> ord a" and "ord a \<le> order G" and "a (^) ord a = \<one>"
   4.324 +    by (auto simp: order_def)
   4.325 +qed
   4.326 +
   4.327 +lemma finite_group_elem_finite_ord :
   4.328 +  assumes "finite (carrier G)" "x \<in> carrier G"
   4.329 +  shows "\<exists> d::nat. d \<ge> 1 \<and> x (^) d = \<one>"
   4.330 +  using assms ord_ge_1 pow_ord_eq_1 by auto
   4.331 +
   4.332 +lemma ord_min:
   4.333 +  assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
   4.334 +proof -
   4.335 +  def Ord \<equiv> "{d \<in> {1..order G}. a (^) d = \<one>}"
   4.336 +  have fin: "finite Ord" by (auto simp: Ord_def)
   4.337 +  have in_ord: "ord a \<in> Ord"
   4.338 +    using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
   4.339 +  then have "Ord \<noteq> {}" by auto
   4.340 +
   4.341 +  show ?thesis
   4.342 +  proof (cases "d \<le> order G")
   4.343 +    case True
   4.344 +    then have "d \<in> Ord" using assms by (auto simp: Ord_def)
   4.345 +    with fin in_ord show ?thesis
   4.346 +      unfolding ord_def Ord_def[symmetric] by simp
   4.347 +  next
   4.348 +    case False
   4.349 +    then show ?thesis using in_ord by (simp add: Ord_def)
   4.350 +  qed
   4.351 +qed
   4.352 +
   4.353 +lemma ord_inj :
   4.354 +  assumes finite: "finite (carrier G)"
   4.355 +  assumes a: "a \<in> carrier G"
   4.356 +  shows "inj_on (\<lambda> x . a (^) x) {0 .. ord a - 1}"
   4.357 +proof (rule inj_onI, rule ccontr)
   4.358 +  fix x y assume A: "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}" "a (^) x= a (^) y" "x \<noteq> y"
   4.359 +
   4.360 +  have "finite {d \<in> {1..order G}. a (^) d = \<one>}" by auto
   4.361 +
   4.362 +  { fix x y assume A: "x < y" "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}"
   4.363 +        "a (^) x = a (^) y"
   4.364 +    hence "y - x < ord a" by auto
   4.365 +    also have "\<dots> \<le> order G" using assms by (simp add: ord_le_group_order)
   4.366 +    finally have y_x_range:"y - x \<in> {1 .. order G}" using A by force
   4.367 +    have "a (^) (y-x) = \<one>" using a A by (simp add: pow_eq_div2)
   4.368 +
   4.369 +    hence y_x:"y - x \<in> {d \<in> {1.. order G}. a (^) d = \<one>}" using y_x_range by blast
   4.370 +    have "min (y - x) (ord a) = ord a"
   4.371 +      using Min.in_idem[OF `finite {d \<in> {1 .. order G} . a (^) d = \<one>}` y_x] ord_def by auto
   4.372 +    with `y - x < ord a` have False by linarith
   4.373 +  }
   4.374 +  note X = this
   4.375 +
   4.376 +  { assume "x < y" with A X have False by blast }
   4.377 +  moreover
   4.378 +  { assume "x > y" with A X  have False by metis }
   4.379 +  moreover
   4.380 +  { assume "x = y" then have False using A by auto}
   4.381 +  ultimately
   4.382 +  show False by fastforce
   4.383 +qed
   4.384 +
   4.385 +lemma ord_inj' :
   4.386 +  assumes finite: "finite (carrier G)"
   4.387 +  assumes a: "a \<in> carrier G"
   4.388 +  shows "inj_on (\<lambda> x . a (^) x) {1 .. ord a}"
   4.389 +proof (rule inj_onI, rule ccontr)
   4.390 +  fix x y :: nat
   4.391 +  assume A:"x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a (^) x = a (^) y" "x\<noteq>y"
   4.392 +  { assume "x < ord a" "y < ord a"
   4.393 +    hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce
   4.394 +  }
   4.395 +  moreover
   4.396 +  { assume "x = ord a" "y < ord a"
   4.397 +    hence "a (^) y = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   4.398 +    hence "y=0" using ord_inj[OF assms] `y < ord a` unfolding inj_on_def by force
   4.399 +    hence False using A by fastforce
   4.400 +  }
   4.401 +  moreover
   4.402 +  { assume "y = ord a" "x < ord a"
   4.403 +    hence "a (^) x = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   4.404 +    hence "x=0" using ord_inj[OF assms] `x < ord a` unfolding inj_on_def by force
   4.405 +    hence False using A by fastforce
   4.406 +  }
   4.407 +  ultimately show False using A  by force
   4.408 +qed
   4.409 +
   4.410 +lemma ord_elems :
   4.411 +  assumes "finite (carrier G)" "a \<in> carrier G"
   4.412 +  shows "{a(^)x | x. x \<in> (UNIV :: nat set)} = {a(^)x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
   4.413 +proof
   4.414 +  show "?R \<subseteq> ?L" by blast
   4.415 +  { fix y assume "y \<in> ?L"
   4.416 +    then obtain x::nat where x:"y = a(^)x" by auto
   4.417 +    def r \<equiv> "x mod ord a"
   4.418 +    then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
   4.419 +    hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
   4.420 +      using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
   4.421 +    hence "y = a(^)r" using assms by (simp add: pow_ord_eq_1)
   4.422 +    have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
   4.423 +    hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
   4.424 +    hence "y \<in> {a(^)x | x. x \<in> {0 .. ord a - 1}}" using `y=a(^)r` by blast
   4.425 +  }
   4.426 +  thus "?L \<subseteq> ?R" by auto
   4.427 +qed
   4.428 +
   4.429 +lemma ord_dvd_pow_eq_1 :
   4.430 +  assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
   4.431 +  shows "ord a dvd k"
   4.432 +proof -
   4.433 +  def r \<equiv> "k mod ord a"
   4.434 +  then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
   4.435 +  hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
   4.436 +      using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
   4.437 +  hence "a(^)k = a(^)r" using assms by (simp add: pow_ord_eq_1)
   4.438 +  hence "a(^)r = \<one>" using assms(3) by simp
   4.439 +  have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)
   4.440 +  hence "r = 0" using `a(^)r = \<one>` ord_def[of a] ord_min[of r a] assms(1-2) by linarith
   4.441 +  thus ?thesis using q by simp
   4.442 +qed
   4.443 +
   4.444 +lemma dvd_gcd :
   4.445 +  fixes a b :: nat
   4.446 +  obtains q where "a * (b div gcd a b) = b*q"
   4.447 +proof
   4.448 +  have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add:  div_mult_swap dvd_div_mult)
   4.449 +  also have "\<dots> = b * (a div gcd a b)" by simp
   4.450 +  finally show "a * (b div gcd a b) = b * (a div gcd a b) " .
   4.451 +qed
   4.452 +
   4.453 +lemma ord_pow_dvd_ord_elem :
   4.454 +  assumes finite[simp]: "finite (carrier G)"
   4.455 +  assumes a[simp]:"a \<in> carrier G"
   4.456 +  shows "ord (a(^)n) = ord a div gcd n (ord a)"
   4.457 +proof -
   4.458 +  have "(a(^)n) (^) ord a = (a (^) ord a) (^) n"
   4.459 +    by (simp add: mult.commute nat_pow_pow)
   4.460 +  hence "(a(^)n) (^) ord a = \<one>" by (simp add: pow_ord_eq_1)
   4.461 +  obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd)
   4.462 +  hence "(a(^)n) (^) (ord a div gcd n (ord a)) = (a (^) ord a)(^)q"  by (simp add : nat_pow_pow)
   4.463 +  hence pow_eq_1: "(a(^)n) (^) (ord a div gcd n (ord a)) = \<one>"
   4.464 +     by (auto simp add : pow_ord_eq_1[of a])
   4.465 +  have "ord a \<ge> 1" using ord_ge_1 by simp
   4.466 +  have ge_1:"ord a div gcd n (ord a) \<ge> 1"
   4.467 +  proof -
   4.468 +    have "gcd n (ord a) dvd ord a" by blast
   4.469 +    thus ?thesis by (rule dvd_div_ge_1[OF `ord a \<ge> 1`])
   4.470 +  qed
   4.471 +  have "ord a \<le> order G" by (simp add: ord_le_group_order)
   4.472 +  have "ord a div gcd n (ord a) \<le> order G"
   4.473 +  proof -
   4.474 +    have "ord a div gcd n (ord a) \<le> ord a" by simp
   4.475 +    thus ?thesis using `ord a \<le> order G` by linarith
   4.476 +  qed
   4.477 +  hence ord_gcd_elem:"ord a div gcd n (ord a) \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
   4.478 +    using ge_1 pow_eq_1 by force
   4.479 +  { fix d :: nat
   4.480 +    assume d_elem:"d \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
   4.481 +    assume d_lt:"d < ord a div gcd n (ord a)"
   4.482 +    hence pow_nd:"a(^)(n*d)  = \<one>" using d_elem
   4.483 +      by (simp add : nat_pow_pow)
   4.484 +    hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1)
   4.485 +    then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel)
   4.486 +    hence prod_eq:"(ord a div gcd n (ord a)) * q = (n div gcd n (ord a)) * d"
   4.487 +      by (simp add: dvd_div_mult)
   4.488 +    have cp:"coprime (ord a div gcd n (ord a)) (n div gcd n (ord a))"
   4.489 +    proof -
   4.490 +      have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"
   4.491 +        using div_gcd_coprime[of n "ord a"] ge_1 by fastforce
   4.492 +      thus ?thesis by (simp add: gcd.commute)
   4.493 +    qed
   4.494 +    have dvd_d:"(ord a div gcd n (ord a)) dvd d"
   4.495 +    proof -
   4.496 +      have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq
   4.497 +        by (metis dvd_triv_right mult.commute)
   4.498 +      hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"
   4.499 +        by (simp add:  mult.commute)
   4.500 +      thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce
   4.501 +    qed
   4.502 +    have "d > 0" using d_elem by simp
   4.503 +    hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
   4.504 +    hence False using d_lt by simp
   4.505 +  } hence ord_gcd_min: "\<And> d . d \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}
   4.506 +                        \<Longrightarrow> d\<ge>ord a div gcd n (ord a)" by fastforce
   4.507 +  have fin:"finite {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}" by auto
   4.508 +  thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem]
   4.509 +    unfolding ord_def by simp
   4.510 +qed
   4.511 +
   4.512 +lemma ord_1_eq_1 :
   4.513 +  assumes "finite (carrier G)"
   4.514 +  shows "ord \<one> = 1"
   4.515 + using assms ord_ge_1 ord_min[of 1 \<one>] by force
   4.516 +
   4.517 +theorem lagrange_dvd:
   4.518 + assumes "finite(carrier G)" "subgroup H G" shows "(card H) dvd (order G)"
   4.519 + using assms by (simp add: lagrange[symmetric])
   4.520 +
   4.521 +lemma element_generates_subgroup:
   4.522 +  assumes finite[simp]: "finite (carrier G)"
   4.523 +  assumes a[simp]: "a \<in> carrier G"
   4.524 +  shows "subgroup {a (^) i | i. i \<in> {0 .. ord a - 1}} G"
   4.525 +proof
   4.526 +  show "{a(^)i | i. i \<in> {0 .. ord a - 1} } \<subseteq> carrier G" by auto
   4.527 +next
   4.528 +  fix x y
   4.529 +  assume A: "x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" "y \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   4.530 +  obtain i::nat where i:"x = a(^)i" and i2:"i \<in> UNIV" using A by auto
   4.531 +  obtain j::nat where j:"y = a(^)j" and j2:"j \<in> UNIV" using A by auto
   4.532 +  have "a(^)(i+j) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto
   4.533 +  thus "x \<otimes> y \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   4.534 +    using i j a ord_elems assms by (auto simp add: nat_pow_mult)
   4.535 +next
   4.536 +  show "\<one> \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" by force
   4.537 +next
   4.538 +  fix x assume x: "x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   4.539 +  hence x_in_carrier: "x \<in> carrier G" by auto
   4.540 +  then obtain d::nat where d:"x (^) d = \<one>" and "d\<ge>1"
   4.541 +    using finite_group_elem_finite_ord by auto
   4.542 +  have inv_1:"x(^)(d - 1) \<otimes> x = \<one>" using `d\<ge>1` d nat_pow_Suc[of x "d - 1"] by simp
   4.543 +  have elem:"x (^) (d - 1) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   4.544 +  proof -
   4.545 +    obtain i::nat where i:"x = a(^)i" using x by auto
   4.546 +    hence "x(^)(d - 1) \<in> {a(^)i | i. i \<in> (UNIV::nat set)}" by (auto simp add: nat_pow_pow)
   4.547 +    thus ?thesis using ord_elems[of a] by auto
   4.548 +  qed
   4.549 +  have inv:"inv x = x(^)(d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast
   4.550 +  thus "inv x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" using elem inv by auto
   4.551 +qed
   4.552 +
   4.553 +lemma ord_dvd_group_order :
   4.554 +  assumes finite[simp]: "finite (carrier G)"
   4.555 +  assumes a[simp]: "a \<in> carrier G"
   4.556 +  shows "ord a dvd order G"
   4.557 +proof -
   4.558 +  have card_dvd:"card {a(^)i | i. i \<in> {0 .. ord a - 1}} dvd card (carrier G)"
   4.559 +    using lagrange_dvd element_generates_subgroup unfolding order_def by simp
   4.560 +  have "inj_on (\<lambda> i . a(^)i) {0..ord a - 1}" using ord_inj by simp
   4.561 +  hence cards_eq:"card ( (\<lambda> i . a(^)i) ` {0..ord a - 1}) = card {0..ord a - 1}"
   4.562 +    using card_image[of "\<lambda> i . a(^)i" "{0..ord a - 1}"] by auto
   4.563 +  have "(\<lambda> i . a(^)i) ` {0..ord a - 1} = {a(^)i | i. i \<in> {0..ord a - 1}}" by auto
   4.564 +  hence "card {a(^)i | i. i \<in> {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp
   4.565 +  also have "\<dots> = ord a" using ord_ge_1[of a] by simp
   4.566 +  finally show ?thesis using card_dvd by (simp add: order_def)
   4.567 +qed
   4.568 +
   4.569 +end
   4.570 +
   4.571 +
   4.572 +section {* Number of Roots of a Polynomial *}
   4.573 +text_raw {* \label{sec:number-roots} *}
   4.574 +
   4.575 +
   4.576 +definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
   4.577 +  "mult_of R \<equiv> \<lparr> carrier = carrier R - {\<zero>\<^bsub>R\<^esub>}, mult = mult R, one = \<one>\<^bsub>R\<^esub>\<rparr>"
   4.578 +
   4.579 +lemma carrier_mult_of: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"
   4.580 +  by (simp add: mult_of_def)
   4.581 +
   4.582 +lemma mult_mult_of: "mult (mult_of R) = mult R"
   4.583 + by (simp add: mult_of_def)
   4.584 +
   4.585 +lemma nat_pow_mult_of: "op (^)\<^bsub>mult_of R\<^esub> = (op (^)\<^bsub>R\<^esub> :: _ \<Rightarrow> nat \<Rightarrow> _)"
   4.586 +  by (simp add: mult_of_def fun_eq_iff nat_pow_def)
   4.587 +
   4.588 +lemma one_mult_of: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
   4.589 +  by (simp add: mult_of_def)
   4.590 +
   4.591 +lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
   4.592 +
   4.593 +context field begin
   4.594 +
   4.595 +lemma field_mult_group :
   4.596 +  shows "group (mult_of R)"
   4.597 +  apply (rule groupI)
   4.598 +  apply (auto simp: mult_of_simps m_assoc dest: integral)
   4.599 +  by (metis Diff_iff Units_inv_Units Units_l_inv field_Units singletonE)
   4.600 +
   4.601 +lemma finite_mult_of: "finite (carrier R) \<Longrightarrow> finite (carrier (mult_of R))"
   4.602 +  by (auto simp: mult_of_simps)
   4.603 +
   4.604 +lemma order_mult_of: "finite (carrier R) \<Longrightarrow> order (mult_of R) = order R - 1"
   4.605 +  unfolding order_def carrier_mult_of by (simp add: card.remove)
   4.606 +
   4.607 +end
   4.608 +
   4.609 +
   4.610 +
   4.611 +lemma (in monoid) Units_pow_closed :
   4.612 +  fixes d :: nat
   4.613 +  assumes "x \<in> Units G"
   4.614 +  shows "x (^) d \<in> Units G"
   4.615 +    by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)
   4.616 +
   4.617 +lemma (in comm_monoid) is_monoid:
   4.618 +  shows "monoid G" by unfold_locales
   4.619 +
   4.620 +declare comm_monoid.is_monoid[intro?]
   4.621 +
   4.622 +lemma (in ring) r_right_minus_eq[simp]:
   4.623 +  assumes "a \<in> carrier R" "b \<in> carrier R"
   4.624 +  shows "a \<ominus> b = \<zero> \<longleftrightarrow> a = b"
   4.625 +  using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)
   4.626 +
   4.627 +context UP_cring begin
   4.628 +
   4.629 +lemma is_UP_cring:"UP_cring R" by (unfold_locales)
   4.630 +lemma is_UP_ring :
   4.631 +  shows "UP_ring R" by (unfold_locales)
   4.632 +
   4.633 +end
   4.634 +
   4.635 +context UP_domain begin
   4.636 +
   4.637 +
   4.638 +lemma roots_bound:
   4.639 +  assumes f [simp]: "f \<in> carrier P"
   4.640 +  assumes f_not_zero: "f \<noteq> \<zero>\<^bsub>P\<^esub>"
   4.641 +  assumes finite: "finite (carrier R)"
   4.642 +  shows "finite {a \<in> carrier R . eval R R id a f = \<zero>} \<and>
   4.643 +         card {a \<in> carrier R . eval R R id a f = \<zero>} \<le> deg R f" using f f_not_zero
   4.644 +proof (induction "deg R f" arbitrary: f)
   4.645 +  case 0
   4.646 +  have "\<And>x. eval R R id x f \<noteq> \<zero>"
   4.647 +  proof -
   4.648 +    fix x
   4.649 +    have "(\<Oplus>i\<in>{..deg R f}. id (coeff P f i) \<otimes> x (^) i) \<noteq> \<zero>"
   4.650 +      using 0 lcoeff_nonzero_nonzero[where p = f] by simp
   4.651 +    thus "eval R R id x f \<noteq> \<zero>" using 0 unfolding eval_def P_def by simp
   4.652 +  qed
   4.653 +  then have *: "{a \<in> carrier R. eval R R (\<lambda>a. a) a f = \<zero>} = {}"
   4.654 +    by (auto simp: id_def)
   4.655 +  show ?case by (simp add: *)
   4.656 +next
   4.657 +  case (Suc x)
   4.658 +  show ?case
   4.659 +  proof (cases "\<exists> a \<in> carrier R . eval R R id a f = \<zero>")
   4.660 +    case True
   4.661 +    then obtain a where a_carrier[simp]: "a \<in> carrier R" and a_root:"eval R R id a f = \<zero>" by blast
   4.662 +    have R_not_triv: "carrier R \<noteq> {\<zero>}"
   4.663 +      by (metis R.one_zeroI R.zero_not_one)
   4.664 +    obtain q  where q:"(q \<in> carrier P)" and
   4.665 +      f:"f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> monom P (eval R R id a f) 0"
   4.666 +     using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto
   4.667 +    hence lin_fac: "f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q" using q by (simp add: a_root)
   4.668 +    have deg:"deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) = 1"
   4.669 +      using a_carrier by (simp add: deg_minus_eq)
   4.670 +    hence mon_not_zero:"(monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<noteq> \<zero>\<^bsub>P\<^esub>"
   4.671 +      by (fastforce simp del: r_right_minus_eq)
   4.672 +    have q_not_zero:"q \<noteq> \<zero>\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac)
   4.673 +    hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]
   4.674 +      by (simp add : lin_fac)
   4.675 +    hence q_IH:"finite {a \<in> carrier R . eval R R id a q = \<zero>}
   4.676 +                \<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast
   4.677 +    have subs:"{a \<in> carrier R . eval R R id a f = \<zero>}
   4.678 +                \<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")
   4.679 +      using a_carrier `q \<in> _`
   4.680 +      by (auto simp: evalRR_simps lin_fac R.integral_iff)
   4.681 +    have "{a \<in> carrier R . eval R R id a f = \<zero>} \<subseteq> insert a {a \<in> carrier R . eval R R id a q = \<zero>}"
   4.682 +     using subs by auto
   4.683 +    hence "card {a \<in> carrier R . eval R R id a f = \<zero>} \<le>
   4.684 +           card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)
   4.685 +    also have "\<dots> \<le> deg R f" using q_IH `Suc x = _`
   4.686 +      by (simp add: card_insert_if)
   4.687 +    finally show ?thesis using q_IH `Suc x = _` using finite by force
   4.688 +  next
   4.689 +    case False
   4.690 +    hence "card {a \<in> carrier R. eval R R id a f = \<zero>} = 0" using finite by auto
   4.691 +    also have "\<dots> \<le>  deg R f" by simp
   4.692 +    finally show ?thesis using finite by auto
   4.693 +  qed
   4.694 +qed
   4.695 +
   4.696 +end
   4.697 +
   4.698 +lemma (in domain) num_roots_le_deg :
   4.699 +  fixes p d :: nat
   4.700 +  assumes finite:"finite (carrier R)"
   4.701 +  assumes d_neq_zero : "d \<noteq> 0"
   4.702 +  shows "card {x \<in> carrier R. x (^) d = \<one>} \<le> d"
   4.703 +proof -
   4.704 +  let ?f = "monom (UP R) \<one>\<^bsub>R\<^esub> d \<ominus>\<^bsub> (UP R)\<^esub> monom (UP R) \<one>\<^bsub>R\<^esub> 0"
   4.705 +  have one_in_carrier:"\<one> \<in> carrier R" by simp
   4.706 +  interpret R: UP_domain R "UP R" by (unfold_locales)
   4.707 +  have "deg R ?f = d"
   4.708 +    using d_neq_zero by (simp add: R.deg_minus_eq)
   4.709 +  hence f_not_zero:"?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using  d_neq_zero by (auto simp add : R.deg_nzero_nzero)
   4.710 +  have roots_bound:"finite {a \<in> carrier R . eval R R id a ?f = \<zero>} \<and>
   4.711 +                    card {a \<in> carrier R . eval R R id a ?f = \<zero>} \<le> deg R ?f"
   4.712 +                    using finite by (intro R.roots_bound[OF _ f_not_zero]) simp
   4.713 +  have subs:"{x \<in> carrier R. x (^) d = \<one>} \<subseteq> {a \<in> carrier R . eval R R id a ?f = \<zero>}"
   4.714 +    by (auto simp: R.evalRR_simps)
   4.715 +  then have "card {x \<in> carrier R. x (^) d = \<one>} \<le>
   4.716 +        card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
   4.717 +  thus ?thesis using `deg R ?f = d` roots_bound by linarith
   4.718 +qed
   4.719 +
   4.720 +
   4.721 +
   4.722 +section {* The Multiplicative Group of a Field *}
   4.723 +text_raw {* \label{sec:mult-group} *}
   4.724 +
   4.725 +
   4.726 +text {*
   4.727 +  In this section we show that the multiplicative group of a finite field
   4.728 +  is generated by a single element, i.e. it is cyclic. The proof is inspired
   4.729 +  by the first proof given in the survey~\cite{conrad-cyclicity}.
   4.730 +*}
   4.731 +
   4.732 +lemma (in group) pow_order_eq_1:
   4.733 +  assumes "finite (carrier G)" "x \<in> carrier G" shows "x (^) order G = \<one>"
   4.734 +  using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)
   4.735 +
   4.736 +(* XXX remove in AFP devel, replaced by div_eq_dividend_iff *)
   4.737 +lemma nat_div_eq: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
   4.738 +  apply rule
   4.739 +  apply (cases "b = 0")
   4.740 +  apply simp_all
   4.741 +  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
   4.742 +  done
   4.743 +
   4.744 +lemma (in group)
   4.745 +  assumes finite': "finite (carrier G)"
   4.746 +  assumes "a \<in> carrier G"
   4.747 +  shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
   4.748 +proof
   4.749 +  assume A: ?L then show ?R
   4.750 +    using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)
   4.751 +next
   4.752 +  assume ?R then show ?L
   4.753 +    using ord_pow_dvd_ord_elem[OF assms, of k] by auto
   4.754 +qed
   4.755 +
   4.756 +context field begin
   4.757 +
   4.758 +lemma num_elems_of_ord_eq_phi':
   4.759 +  assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"
   4.760 +      and exists: "\<exists>a\<in>carrier (mult_of R). group.ord (mult_of R) a = d"
   4.761 +  shows "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"
   4.762 +proof -
   4.763 +  note mult_of_simps[simp]
   4.764 +  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
   4.765 +
   4.766 +  interpret G:group "mult_of R" rewrites "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
   4.767 +    by (rule field_mult_group) simp_all
   4.768 +
   4.769 +  from exists
   4.770 +  obtain a where a:"a \<in> carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"
   4.771 +    by (auto simp add: card_gt_0_iff)
   4.772 +
   4.773 +  have set_eq1:"{a(^)n| n. n \<in> {1 .. d}} = {x \<in> carrier (mult_of R). x (^) d = \<one>}"
   4.774 +  proof (rule card_seteq)
   4.775 +    show "finite {x \<in> carrier (mult_of R). x (^) d = \<one>}" using finite by auto
   4.776 +
   4.777 +    show "{a(^)n| n. n \<in> {1 ..d}} \<subseteq> {x \<in> carrier (mult_of R). x(^)d = \<one>}"
   4.778 +    proof
   4.779 +      fix x assume "x \<in> {a(^)n | n. n \<in> {1 .. d}}"
   4.780 +      then obtain n where n:"x = a(^)n \<and> n \<in> {1 .. d}" by auto
   4.781 +      have "x(^)d =(a(^)d)(^)n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
   4.782 +      hence "x(^)d = \<one>" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce
   4.783 +      thus "x \<in> {x \<in> carrier (mult_of R). x(^)d = \<one>}" using G.nat_pow_closed[OF a] n by blast
   4.784 +    qed
   4.785 +
   4.786 +    show "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {a(^)n | n. n \<in> {1 .. d}}"
   4.787 +    proof -
   4.788 +      have *:"{a(^)n | n. n \<in> {1 .. d }} = ((\<lambda> n. a(^)n) ` {1 .. d})" by auto
   4.789 +      have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]
   4.790 +        using card_mono[OF finite, of "{\<zero>, \<one>}"] by (simp add: order_def)
   4.791 +      have "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {x \<in> carrier R. x (^) d = \<one>}"
   4.792 +        using finite by (auto intro: card_mono)
   4.793 +      also have "\<dots> \<le> d" using `0 < order (mult_of R)` num_roots_le_deg[OF finite, of d]
   4.794 +        by (simp add : dvd_pos_nat[OF _ `d dvd order (mult_of R)`])
   4.795 +      finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image)
   4.796 +    qed
   4.797 +  qed
   4.798 +
   4.799 +  have set_eq2:"{x \<in> carrier (mult_of R) . group.ord (mult_of R) x = d}
   4.800 +                = (\<lambda> n . a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d}" (is "?L = ?R")
   4.801 +  proof
   4.802 +    { fix x assume x:"x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"
   4.803 +      hence "x \<in> {x \<in> carrier (mult_of R). x (^) d = \<one>}"
   4.804 +        by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric])
   4.805 +      then obtain n where n:"x = a(^)n \<and> n \<in> {1 .. d}" using set_eq1 by blast
   4.806 +      hence "x \<in> ?R" using x by fast
   4.807 +    } thus "?L \<subseteq> ?R" by blast
   4.808 +    show "?R \<subseteq> ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
   4.809 +  qed
   4.810 +  have "inj_on (\<lambda> n . a(^)n) {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d}"
   4.811 +    using G.ord_inj'[OF finite' a, unfolded ord_a] unfolding inj_on_def by fast
   4.812 +  hence "card ((\<lambda>n. a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d})
   4.813 +         = card {k \<in> {1 .. d}. group.ord (mult_of R) (a(^)k) = d}"
   4.814 +         using card_image by blast
   4.815 +  thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' `a \<in> _`, unfolded ord_a]
   4.816 +    by (simp add: phi'_def)
   4.817 +qed
   4.818 +
   4.819 +end
   4.820 +
   4.821 +
   4.822 +theorem (in field) finite_field_mult_group_has_gen :
   4.823 +  assumes finite:"finite (carrier R)"
   4.824 +  shows "\<exists> a \<in> carrier (mult_of R) . carrier (mult_of R) = {a(^)i | i::nat . i \<in> UNIV}"
   4.825 +proof -
   4.826 +  note mult_of_simps[simp]
   4.827 +  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
   4.828 +
   4.829 +  interpret G: group "mult_of R" rewrites
   4.830 +      "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
   4.831 +    by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)
   4.832 +
   4.833 +  let ?N = "\<lambda> x . card {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = x}"
   4.834 +  have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\<zero>, \<one>}"] by simp
   4.835 +  then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)
   4.836 +  have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force
   4.837 +
   4.838 +  have "(\<Sum>d | d dvd order (mult_of R). ?N d)
   4.839 +      = card (UN d:{d . d dvd order (mult_of R) }. {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = d})"
   4.840 +      (is "_ = card ?U")
   4.841 +    using fin finite by (subst card_UN_disjoint) auto
   4.842 +  also have "?U = carrier (mult_of R)"
   4.843 +  proof
   4.844 +    { fix x assume x:"x \<in> carrier (mult_of R)"
   4.845 +      hence x':"x\<in>carrier (mult_of R)" by simp
   4.846 +      then have "group.ord (mult_of R) x dvd order (mult_of R)"
   4.847 +          using finite' G.ord_dvd_group_order[OF _ x'] by (simp add: order_mult_of)
   4.848 +      hence "x \<in> ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
   4.849 +    } thus "carrier (mult_of R) \<subseteq> ?U" by blast
   4.850 +  qed auto
   4.851 +  also have "card ... = order (mult_of R)"
   4.852 +    using order_mult_of finite' by (simp add: order_def)
   4.853 +  finally have sum_Ns_eq: "(\<Sum>d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .
   4.854 +
   4.855 +  { fix d assume d:"d dvd order (mult_of R)"
   4.856 +    have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"
   4.857 +    proof cases
   4.858 +      assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger
   4.859 +      next
   4.860 +      assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<noteq> 0"
   4.861 +      hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
   4.862 +      thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
   4.863 +    qed
   4.864 +  }
   4.865 +  hence all_le:"\<And>i. i \<in> {d. d dvd order (mult_of R) }
   4.866 +        \<Longrightarrow> (\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}) i \<le> (\<lambda>i. phi' i) i" by fast
   4.867 +  hence le:"(\<Sum>i | i dvd order (mult_of R). ?N i)
   4.868 +            \<le> (\<Sum>i | i dvd order (mult_of R). phi' i)"
   4.869 +            using sum_mono[of "{d .  d dvd order (mult_of R)}"
   4.870 +                  "\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger
   4.871 +  have "order (mult_of R) = (\<Sum>d | d dvd order (mult_of R). phi' d)" using *
   4.872 +    by (simp add: sum_phi'_factors)
   4.873 +  hence eq:"(\<Sum>i | i dvd order (mult_of R). ?N i)
   4.874 +          = (\<Sum>i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger
   4.875 +  have "\<And>i. i \<in> {d. d dvd order (mult_of R) } \<Longrightarrow> ?N i = (\<lambda>i. phi' i) i"
   4.876 +  proof (rule ccontr)
   4.877 +    fix i
   4.878 +    assume i1:"i \<in> {d. d dvd order (mult_of R)}" and "?N i \<noteq> phi' i"
   4.879 +    hence "?N i = 0"
   4.880 +      using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)
   4.881 +    moreover  have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])
   4.882 +    ultimately have "?N i < phi' i" using phi'_nonzero by presburger
   4.883 +    hence "(\<Sum>i | i dvd order (mult_of R). ?N i)
   4.884 +         < (\<Sum>i | i dvd order (mult_of R). phi' i)"
   4.885 +      using sum_strict_mono_ex1[OF fin, of "?N" "\<lambda> i . phi' i"]
   4.886 +            i1 all_le by auto
   4.887 +    thus False using eq by force
   4.888 +  qed
   4.889 +  hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)
   4.890 +  then obtain a where a:"a \<in> carrier (mult_of R)" and a_ord:"group.ord (mult_of R) a = order (mult_of R)"
   4.891 +    by (auto simp add: card_gt_0_iff)
   4.892 +  hence set_eq:"{a(^)i | i::nat. i \<in> UNIV} = (\<lambda>x. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}"
   4.893 +    using G.ord_elems[OF finite'] by auto
   4.894 +  have card_eq:"card ((\<lambda>x. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"
   4.895 +    by (intro card_image G.ord_inj finite' a)
   4.896 +  hence "card ((\<lambda> x . a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
   4.897 +    using assms by (simp add: card_eq a_ord)
   4.898 +  hence card_R_minus_1:"card {a(^)i | i::nat. i \<in> UNIV} =  order (mult_of R)"
   4.899 +    using * by (subst set_eq) auto
   4.900 +  have **:"{a(^)i | i::nat. i \<in> UNIV} \<subseteq> carrier (mult_of R)"
   4.901 +    using G.nat_pow_closed[OF a] by auto
   4.902 +  with _ have "carrier (mult_of R) = {a(^)i|i::nat. i \<in> UNIV}"
   4.903 +    by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)
   4.904 +  thus ?thesis using a by blast
   4.905 +qed
   4.906 +
   4.907 +end
     5.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Apr 06 22:04:30 2017 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,333 +0,0 @@
     5.4 -(*  Title:      HOL/Number_Theory/MiscAlgebra.thy
     5.5 -    Author:     Jeremy Avigad
     5.6 -*)
     5.7 -
     5.8 -section \<open>Things that can be added to the Algebra library\<close>
     5.9 -
    5.10 -theory MiscAlgebra
    5.11 -imports
    5.12 -  "~~/src/HOL/Algebra/Ring"
    5.13 -  "~~/src/HOL/Algebra/FiniteProduct"
    5.14 -begin
    5.15 -
    5.16 -subsection \<open>Finiteness stuff\<close>
    5.17 -
    5.18 -lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
    5.19 -  apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
    5.20 -  apply (erule finite_subset)
    5.21 -  apply auto
    5.22 -  done
    5.23 -
    5.24 -
    5.25 -subsection \<open>The rest is for the algebra libraries\<close>
    5.26 -
    5.27 -subsubsection \<open>These go in Group.thy\<close>
    5.28 -
    5.29 -text \<open>
    5.30 -  Show that the units in any monoid give rise to a group.
    5.31 -
    5.32 -  The file Residues.thy provides some infrastructure to use
    5.33 -  facts about the unit group within the ring locale.
    5.34 -\<close>
    5.35 -
    5.36 -definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
    5.37 -  "units_of G == (| carrier = Units G,
    5.38 -     Group.monoid.mult = Group.monoid.mult G,
    5.39 -     one  = one G |)"
    5.40 -
    5.41 -(*
    5.42 -
    5.43 -lemma (in monoid) Units_mult_closed [intro]:
    5.44 -  "x : Units G ==> y : Units G ==> x \<otimes> y : Units G"
    5.45 -  apply (unfold Units_def)
    5.46 -  apply (clarsimp)
    5.47 -  apply (rule_tac x = "xaa \<otimes> xa" in bexI)
    5.48 -  apply auto
    5.49 -  apply (subst m_assoc)
    5.50 -  apply auto
    5.51 -  apply (subst (2) m_assoc [symmetric])
    5.52 -  apply auto
    5.53 -  apply (subst m_assoc)
    5.54 -  apply auto
    5.55 -  apply (subst (2) m_assoc [symmetric])
    5.56 -  apply auto
    5.57 -done
    5.58 -
    5.59 -*)
    5.60 -
    5.61 -lemma (in monoid) units_group: "group(units_of G)"
    5.62 -  apply (unfold units_of_def)
    5.63 -  apply (rule groupI)
    5.64 -  apply auto
    5.65 -  apply (subst m_assoc)
    5.66 -  apply auto
    5.67 -  apply (rule_tac x = "inv x" in bexI)
    5.68 -  apply auto
    5.69 -  done
    5.70 -
    5.71 -lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
    5.72 -  apply (rule group.group_comm_groupI)
    5.73 -  apply (rule units_group)
    5.74 -  apply (insert comm_monoid_axioms)
    5.75 -  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    5.76 -  apply auto
    5.77 -  done
    5.78 -
    5.79 -lemma units_of_carrier: "carrier (units_of G) = Units G"
    5.80 -  unfolding units_of_def by auto
    5.81 -
    5.82 -lemma units_of_mult: "mult(units_of G) = mult G"
    5.83 -  unfolding units_of_def by auto
    5.84 -
    5.85 -lemma units_of_one: "one(units_of G) = one G"
    5.86 -  unfolding units_of_def by auto
    5.87 -
    5.88 -lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
    5.89 -  apply (rule sym)
    5.90 -  apply (subst m_inv_def)
    5.91 -  apply (rule the1_equality)
    5.92 -  apply (rule ex_ex1I)
    5.93 -  apply (subst (asm) Units_def)
    5.94 -  apply auto
    5.95 -  apply (erule inv_unique)
    5.96 -  apply auto
    5.97 -  apply (rule Units_closed)
    5.98 -  apply (simp_all only: units_of_carrier [symmetric])
    5.99 -  apply (insert units_group)
   5.100 -  apply auto
   5.101 -  apply (subst units_of_mult [symmetric])
   5.102 -  apply (subst units_of_one [symmetric])
   5.103 -  apply (erule group.r_inv, assumption)
   5.104 -  apply (subst units_of_mult [symmetric])
   5.105 -  apply (subst units_of_one [symmetric])
   5.106 -  apply (erule group.l_inv, assumption)
   5.107 -  done
   5.108 -
   5.109 -lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
   5.110 -  unfolding inj_on_def by auto
   5.111 -
   5.112 -lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
   5.113 -  apply (auto simp add: image_def)
   5.114 -  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   5.115 -  apply auto
   5.116 -(* auto should get this. I suppose we need "comm_monoid_simprules"
   5.117 -   for ac_simps rewriting. *)
   5.118 -  apply (subst m_assoc [symmetric])
   5.119 -  apply auto
   5.120 -  done
   5.121 -
   5.122 -lemma (in group) l_cancel_one [simp]:
   5.123 -    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
   5.124 -  apply auto
   5.125 -  apply (subst l_cancel [symmetric])
   5.126 -  prefer 4
   5.127 -  apply (erule ssubst)
   5.128 -  apply auto
   5.129 -  done
   5.130 -
   5.131 -lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   5.132 -    (a \<otimes> x = x) = (a = one G)"
   5.133 -  apply auto
   5.134 -  apply (subst r_cancel [symmetric])
   5.135 -  prefer 4
   5.136 -  apply (erule ssubst)
   5.137 -  apply auto
   5.138 -  done
   5.139 -
   5.140 -(* Is there a better way to do this? *)
   5.141 -lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   5.142 -    (x = x \<otimes> a) = (a = one G)"
   5.143 -  apply (subst eq_commute)
   5.144 -  apply simp
   5.145 -  done
   5.146 -
   5.147 -lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   5.148 -    (x = a \<otimes> x) = (a = one G)"
   5.149 -  apply (subst eq_commute)
   5.150 -  apply simp
   5.151 -  done
   5.152 -
   5.153 -(* This should be generalized to arbitrary groups, not just commutative
   5.154 -   ones, using Lagrange's theorem. *)
   5.155 -
   5.156 -lemma (in comm_group) power_order_eq_one:
   5.157 -  assumes fin [simp]: "finite (carrier G)"
   5.158 -    and a [simp]: "a : carrier G"
   5.159 -  shows "a (^) card(carrier G) = one G"
   5.160 -proof -
   5.161 -  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
   5.162 -    by (subst (2) finprod_reindex [symmetric],
   5.163 -      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   5.164 -  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
   5.165 -    by (auto simp add: finprod_multf Pi_def)
   5.166 -  also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
   5.167 -    by (auto simp add: finprod_const)
   5.168 -  finally show ?thesis
   5.169 -(* uses the preceeding lemma *)
   5.170 -    by auto
   5.171 -qed
   5.172 -
   5.173 -
   5.174 -subsubsection \<open>Miscellaneous\<close>
   5.175 -
   5.176 -lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
   5.177 -  apply (unfold_locales)
   5.178 -  apply (insert cring_axioms, auto)
   5.179 -  apply (rule trans)
   5.180 -  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
   5.181 -  apply assumption
   5.182 -  apply (subst m_assoc)
   5.183 -  apply auto
   5.184 -  apply (unfold Units_def)
   5.185 -  apply auto
   5.186 -  done
   5.187 -
   5.188 -lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   5.189 -    x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
   5.190 -  apply (subgoal_tac "x : Units G")
   5.191 -  apply (subgoal_tac "y = inv x \<otimes> \<one>")
   5.192 -  apply simp
   5.193 -  apply (erule subst)
   5.194 -  apply (subst m_assoc [symmetric])
   5.195 -  apply auto
   5.196 -  apply (unfold Units_def)
   5.197 -  apply auto
   5.198 -  done
   5.199 -
   5.200 -lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   5.201 -  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
   5.202 -  apply (rule inv_char)
   5.203 -  apply auto
   5.204 -  apply (subst m_comm, auto)
   5.205 -  done
   5.206 -
   5.207 -lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
   5.208 -  apply (rule inv_char)
   5.209 -  apply (auto simp add: l_minus r_minus)
   5.210 -  done
   5.211 -
   5.212 -lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
   5.213 -    inv x = inv y \<Longrightarrow> x = y"
   5.214 -  apply (subgoal_tac "inv(inv x) = inv(inv y)")
   5.215 -  apply (subst (asm) Units_inv_inv)+
   5.216 -  apply auto
   5.217 -  done
   5.218 -
   5.219 -lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
   5.220 -  apply (unfold Units_def)
   5.221 -  apply auto
   5.222 -  apply (rule_tac x = "\<ominus> \<one>" in bexI)
   5.223 -  apply auto
   5.224 -  apply (simp add: l_minus r_minus)
   5.225 -  done
   5.226 -
   5.227 -lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
   5.228 -  apply (rule inv_char)
   5.229 -  apply auto
   5.230 -  done
   5.231 -
   5.232 -lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
   5.233 -  apply auto
   5.234 -  apply (subst Units_inv_inv [symmetric])
   5.235 -  apply auto
   5.236 -  done
   5.237 -
   5.238 -lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
   5.239 -  by (metis Units_inv_inv inv_one)
   5.240 -
   5.241 -
   5.242 -subsubsection \<open>This goes in FiniteProduct\<close>
   5.243 -
   5.244 -lemma (in comm_monoid) finprod_UN_disjoint:
   5.245 -  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
   5.246 -     (A i) Int (A j) = {}) \<longrightarrow>
   5.247 -      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
   5.248 -        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
   5.249 -  apply (induct set: finite)
   5.250 -  apply force
   5.251 -  apply clarsimp
   5.252 -  apply (subst finprod_Un_disjoint)
   5.253 -  apply blast
   5.254 -  apply (erule finite_UN_I)
   5.255 -  apply blast
   5.256 -  apply (fastforce)
   5.257 -  apply (auto intro!: funcsetI finprod_closed)
   5.258 -  done
   5.259 -
   5.260 -lemma (in comm_monoid) finprod_Union_disjoint:
   5.261 -  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
   5.262 -      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
   5.263 -   ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
   5.264 -  apply (frule finprod_UN_disjoint [of C id f])
   5.265 -  apply auto
   5.266 -  done
   5.267 -
   5.268 -lemma (in comm_monoid) finprod_one:
   5.269 -    "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
   5.270 -  by (induct set: finite) auto
   5.271 -
   5.272 -
   5.273 -(* need better simplification rules for rings *)
   5.274 -(* the next one holds more generally for abelian groups *)
   5.275 -
   5.276 -lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
   5.277 -  by (metis minus_equality)
   5.278 -
   5.279 -lemma (in domain) square_eq_one:
   5.280 -  fixes x
   5.281 -  assumes [simp]: "x : carrier R"
   5.282 -    and "x \<otimes> x = \<one>"
   5.283 -  shows "x = \<one> | x = \<ominus>\<one>"
   5.284 -proof -
   5.285 -  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
   5.286 -    by (simp add: ring_simprules)
   5.287 -  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
   5.288 -    by (simp add: ring_simprules)
   5.289 -  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
   5.290 -  then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
   5.291 -    by (intro integral, auto)
   5.292 -  then show ?thesis
   5.293 -    apply auto
   5.294 -    apply (erule notE)
   5.295 -    apply (rule sum_zero_eq_neg)
   5.296 -    apply auto
   5.297 -    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
   5.298 -    apply (simp add: ring_simprules)
   5.299 -    apply (rule sum_zero_eq_neg)
   5.300 -    apply auto
   5.301 -    done
   5.302 -qed
   5.303 -
   5.304 -lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
   5.305 -  by (metis Units_closed Units_l_inv square_eq_one)
   5.306 -
   5.307 -
   5.308 -text \<open>
   5.309 -  The following translates theorems about groups to the facts about
   5.310 -  the units of a ring. (The list should be expanded as more things are
   5.311 -  needed.)
   5.312 -\<close>
   5.313 -
   5.314 -lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
   5.315 -  by (rule finite_subset) auto
   5.316 -
   5.317 -lemma (in monoid) units_of_pow:
   5.318 -  fixes n :: nat
   5.319 -  shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n"
   5.320 -  apply (induct n)
   5.321 -  apply (auto simp add: units_group group.is_monoid
   5.322 -    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
   5.323 -  done
   5.324 -
   5.325 -lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
   5.326 -    \<Longrightarrow> a (^) card(Units R) = \<one>"
   5.327 -  apply (subst units_of_carrier [symmetric])
   5.328 -  apply (subst units_of_one [symmetric])
   5.329 -  apply (subst units_of_pow [symmetric])
   5.330 -  apply assumption
   5.331 -  apply (rule comm_group.power_order_eq_one)
   5.332 -  apply (rule units_comm_group)
   5.333 -  apply (unfold units_of_def, auto)
   5.334 -  done
   5.335 -
   5.336 -end
     6.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Thu Apr 06 22:04:30 2017 +0200
     6.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Apr 06 08:33:37 2017 +0200
     6.3 @@ -131,14 +131,18 @@
     6.4  lemma phi_lowerbound_1: assumes n: "n \<ge> 2"
     6.5    shows "phi n \<ge> 1"
     6.6  proof -
     6.7 -  have "1 \<le> card {0::int <.. 1}"
     6.8 -    by auto
     6.9 -  also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
    6.10 -    apply (rule card_mono) using assms
    6.11 -    by auto (metis dual_order.antisym gcd_1_int gcd.commute int_one_le_iff_zero_less)
    6.12 +  have "finite {x. 0 < x \<and> x < n}"
    6.13 +    by simp
    6.14 +  then have "finite {x. 0 < x \<and> x < n \<and> coprime x n}"
    6.15 +    by (auto intro: rev_finite_subset)
    6.16 +  moreover have "{0::int <.. 1} \<subseteq> {x. 0 < x \<and> x < n \<and> coprime x n}"
    6.17 +    using n by (auto simp add: antisym_conv) 
    6.18 +  ultimately have "card {0::int <.. 1} \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
    6.19 +    by (rule card_mono)
    6.20    also have "... = phi n"
    6.21      by (simp add: phi_def)
    6.22 -  finally show ?thesis .
    6.23 +  finally show ?thesis
    6.24 +    by simp
    6.25  qed
    6.26  
    6.27  lemma phi_lowerbound_1_nat: assumes n: "n \<ge> 2"
     7.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Thu Apr 06 22:04:30 2017 +0200
     7.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Thu Apr 06 08:33:37 2017 +0200
     7.3 @@ -178,6 +178,7 @@
     7.4    where "g_1 res = (THE x. P_1 res x)"
     7.5  
     7.6  lemma P_1_lemma:
     7.7 +  fixes res :: "int \<times> int"
     7.8    assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
     7.9    shows "\<exists>!x. P_1 res x"
    7.10  proof -
    7.11 @@ -204,12 +205,35 @@
    7.12  qed
    7.13  
    7.14  lemma g_1_lemma:
    7.15 +  fixes res :: "int \<times> int"
    7.16    assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
    7.17    shows "P_1 res (g_1 res)"
    7.18 -  using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger
    7.19 +  using assms P_1_lemma [of res] theI' [of "P_1 res"] g_1_def
    7.20 +  by auto
    7.21  
    7.22  definition "BuC = Sets_pq Res_ge_0 Res_h Res_l"
    7.23  
    7.24 +lemma finite_BuC [simp]:
    7.25 +  "finite BuC"
    7.26 +proof -
    7.27 +  {
    7.28 +    fix p q :: nat
    7.29 +    have "finite {x. 0 < x \<and> x < int p * int q}"
    7.30 +      by simp
    7.31 +    then have "finite {x.
    7.32 +      0 < x \<and>
    7.33 +      x < int p * int q \<and>
    7.34 +      (int p - 1) div 2
    7.35 +      < x mod int p \<and>
    7.36 +      x mod int p < int p \<and>
    7.37 +      0 < x mod int q \<and>
    7.38 +      x mod int q \<le> (int q - 1) div 2}"
    7.39 +      by (auto intro: rev_finite_subset)
    7.40 +  }
    7.41 +  then show ?thesis
    7.42 +    by (simp add: BuC_def)
    7.43 +qed
    7.44 +
    7.45  lemma QR_lemma_04: "card BuC = card (Res_h p \<times> Res_l q)"
    7.46    using card_bij_eq[of f_1 "BuC" "Res_h p \<times> Res_l q" g_1]
    7.47  proof
    7.48 @@ -245,7 +269,7 @@
    7.49      with x show "y \<in> BuC"
    7.50        unfolding P_1_def BuC_def mem_Collect_eq using SigmaE prod.sel by fastforce
    7.51    qed
    7.52 -qed (auto simp: BuC_def finite_subset f_1_def)
    7.53 +qed (auto simp: finite_subset f_1_def, simp_all add: BuC_def)
    7.54  
    7.55  lemma QR_lemma_05: "card (Res_h p \<times> Res_l q) = r"
    7.56  proof -
     8.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Apr 06 22:04:30 2017 +0200
     8.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Apr 06 08:33:37 2017 +0200
     8.3 @@ -8,7 +8,12 @@
     8.4  section \<open>Residue rings\<close>
     8.5  
     8.6  theory Residues
     8.7 -imports Cong MiscAlgebra
     8.8 +imports
     8.9 +  Cong
    8.10 +  "~~/src/HOL/Algebra/More_Group"
    8.11 +  "~~/src/HOL/Algebra/More_Ring"
    8.12 +  "~~/src/HOL/Algebra/More_Finite_Product"
    8.13 +  "~~/src/HOL/Algebra/Multiplicative_Group"
    8.14  begin
    8.15  
    8.16  definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
    8.17 @@ -117,10 +122,10 @@
    8.18    done
    8.19  
    8.20  lemma finite [iff]: "finite (carrier R)"
    8.21 -  by (subst res_carrier_eq) auto
    8.22 +  by (simp add: res_carrier_eq)
    8.23  
    8.24  lemma finite_Units [iff]: "finite (Units R)"
    8.25 -  by (subst res_units_eq) auto
    8.26 +  by (simp add: finite_ring_finite_units)
    8.27  
    8.28  text \<open>
    8.29    The function \<open>a \<mapsto> a mod m\<close> maps the integers to the
    8.30 @@ -286,6 +291,28 @@
    8.31  lemma phi_one [simp]: "phi 1 = 0"
    8.32    by (auto simp add: phi_def card_eq_0_iff)
    8.33  
    8.34 +lemma phi_leq: "phi x \<le> nat x - 1"
    8.35 +proof -
    8.36 +  have "phi x \<le> card {1..x - 1}"
    8.37 +    unfolding phi_def by (rule card_mono) auto
    8.38 +  then show ?thesis by simp
    8.39 +qed
    8.40 +
    8.41 +lemma phi_nonzero:
    8.42 +  "phi x > 0" if "2 \<le> x"
    8.43 +proof -
    8.44 +  have "finite {y. 0 < y \<and> y < x}"
    8.45 +    by simp
    8.46 +  then have "finite {y. 0 < y \<and> y < x \<and> coprime y x}"
    8.47 +    by (auto intro: rev_finite_subset)
    8.48 +  moreover have "1 \<in> {y. 0 < y \<and> y < x \<and> coprime y x}"
    8.49 +    using that by simp
    8.50 +  ultimately have "card {y. 0 < y \<and> y < x \<and> coprime y x} \<noteq> 0"
    8.51 +    by auto
    8.52 +  then show ?thesis
    8.53 +    by (simp add: phi_def)
    8.54 +qed
    8.55 +
    8.56  lemma (in residues) phi_eq: "phi m = card (Units R)"
    8.57    by (simp add: phi_def res_units_eq)
    8.58  
    8.59 @@ -413,4 +440,60 @@
    8.60      by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
    8.61  qed
    8.62  
    8.63 +text {*
    8.64 +  This result can be transferred to the multiplicative group of
    8.65 +  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *}
    8.66 +
    8.67 +lemma mod_nat_int_pow_eq:
    8.68 +  fixes n :: nat and p a :: int
    8.69 +  assumes "a \<ge> 0" "p \<ge> 0"
    8.70 +  shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
    8.71 +  using assms
    8.72 +  by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
    8.73 +
    8.74 +theorem residue_prime_mult_group_has_gen :
    8.75 + fixes p :: nat
    8.76 + assumes prime_p : "prime p"
    8.77 + shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
    8.78 +proof -
    8.79 +  have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp
    8.80 +  interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def
    8.81 +    by (simp add: prime_p)
    8.82 +  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} =  {1 .. int p - 1}"
    8.83 +    by (auto simp add: R.zero_cong R.res_carrier_eq)
    8.84 +  obtain a where a:"a \<in> {1 .. int p - 1}"
    8.85 +         and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
    8.86 +    apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field]
    8.87 +    by (auto simp add: car[symmetric] carrier_mult_of)
    8.88 +  { fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}"
    8.89 +    hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
    8.90 +  note * = this
    8.91 +  have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
    8.92 +  proof
    8.93 +    { fix n assume n: "n \<in> ?L"
    8.94 +      then have "n \<in> ?R" using `p\<ge>2` by force
    8.95 +    } thus "?L \<subseteq> ?R" by blast
    8.96 +    { fix n assume n: "n \<in> ?R"
    8.97 +      then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce
    8.98 +    } thus "?R \<subseteq> ?L" by blast
    8.99 +  qed
   8.100 +  have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
   8.101 +  proof
   8.102 +    { fix x assume x: "x \<in> ?L"
   8.103 +      then obtain i where i:"x = nat (a^i mod (int p))" by blast
   8.104 +      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
   8.105 +      hence "x \<in> ?R" using i by blast
   8.106 +    } thus "?L \<subseteq> ?R" by blast
   8.107 +    { fix x assume x: "x \<in> ?R"
   8.108 +      then obtain i where i:"x = nat a^i mod p" by blast
   8.109 +      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
   8.110 +    } thus "?R \<subseteq> ?L" by blast
   8.111 +  qed
   8.112 +  hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
   8.113 +    using * a a_gen ** by presburger
   8.114 +  moreover
   8.115 +  have "nat a \<in> {1 .. p - 1}" using a by force
   8.116 +  ultimately show ?thesis ..
   8.117 +qed
   8.118 +
   8.119  end
     9.1 --- a/src/HOL/ROOT	Thu Apr 06 22:04:30 2017 +0200
     9.2 +++ b/src/HOL/ROOT	Thu Apr 06 08:33:37 2017 +0200
     9.3 @@ -311,11 +311,15 @@
     9.4      FiniteProduct        (* Product operator for commutative groups *)
     9.5      Sylow                (* Sylow's theorem *)
     9.6      Bij                  (* Automorphism Groups *)
     9.7 +    More_Group
     9.8 +    More_Finite_Product
     9.9 +    Multiplicative_Group
    9.10  
    9.11      (* Rings *)
    9.12      Divisibility         (* Rings *)
    9.13      IntRing              (* Ideals and residue classes *)
    9.14      UnivPoly             (* Polynomials *)
    9.15 +    More_Ring
    9.16    document_files "root.bib" "root.tex"
    9.17  
    9.18  session "HOL-Auth" (timing) in Auth = HOL +