diff --git a/src/HOL/Algebra/Multiplicative_Group.thy b/src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy
+++ b/src/HOL/Algebra/Multiplicative_Group.thy
@@ -1,1061 +1,1061 @@
 (*  Title:      HOL/Algebra/Multiplicative_Group.thy
     Author:     Simon Wimmer
     Author:     Lars Noschinski
 *)
 
 theory Multiplicative_Group
 imports
   Complex_Main
   Group
   Coset
   UnivPoly
   Generated_Groups
   Elementary_Groups
 begin
 
 section \<open>Simplification Rules for Polynomials\<close>
 text_raw \<open>\label{sec:simp-rules}\<close>
 
 lemma (in ring_hom_cring) hom_sub[simp]:
   assumes "x \<in> carrier R" "y \<in> carrier R"
   shows "h (x \<ominus> y) = h x \<ominus>\<^bsub>S\<^esub> h y"
   using assms by (simp add: R.minus_eq S.minus_eq)
 
 context UP_ring begin
 
 lemma deg_nzero_nzero:
   assumes deg_p_nzero: "deg R p \<noteq> 0"
   shows "p \<noteq> \<zero>\<^bsub>P\<^esub>"
   using deg_zero deg_p_nzero by auto
 
 lemma deg_add_eq:
   assumes c: "p \<in> carrier P" "q \<in> carrier P"
   assumes "deg R q \<noteq> deg R p"
   shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
 proof -
   let ?m = "max (deg R p) (deg R q)"
   from assms have "coeff P p ?m = \<zero> \<longleftrightarrow> coeff P q ?m \<noteq> \<zero>"
     by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)
   then have "coeff P (p \<oplus>\<^bsub>P\<^esub> q) ?m \<noteq> \<zero>"
     using assms by auto
   then have "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<ge> ?m"
     using assms by (blast intro: deg_belowI)
   with deg_add[OF c] show ?thesis by arith
 qed
 
 lemma deg_minus_eq:
   assumes "p \<in> carrier P" "q \<in> carrier P" "deg R q \<noteq> deg R p"
   shows "deg R (p \<ominus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
   using assms by (simp add: deg_add_eq a_minus_def)
 
 end
 
 context UP_cring begin
 
 lemma evalRR_add:
   assumes "p \<in> carrier P" "q \<in> carrier P"
   assumes x: "x \<in> carrier R"
   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"
 proof -
   interpret UP_pre_univ_prop R R id by unfold_locales simp
   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
   show ?thesis using assms by simp
 qed
 
 lemma evalRR_sub:
   assumes "p \<in> carrier P" "q \<in> carrier P"
   assumes x: "x \<in> carrier R"
   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"
 proof -
   interpret UP_pre_univ_prop R R id by unfold_locales simp
   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
   show ?thesis using assms by simp
 qed
 
 lemma evalRR_mult:
   assumes "p \<in> carrier P" "q \<in> carrier P"
   assumes x: "x \<in> carrier R"
   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"
 proof -
   interpret UP_pre_univ_prop R R id by unfold_locales simp
   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
   show ?thesis using assms by simp
 qed
 
 lemma evalRR_monom:
   assumes a: "a \<in> carrier R" and x: "x \<in> carrier R"
   shows "eval R R id x (monom P a d) = a \<otimes> x [^] d"
 proof -
   interpret UP_pre_univ_prop R R id by unfold_locales simp
   show ?thesis using assms by (simp add: eval_monom)
 qed
 
 lemma evalRR_one:
   assumes x: "x \<in> carrier R"
   shows "eval R R id x \<one>\<^bsub>P\<^esub> = \<one>"
 proof -
   interpret UP_pre_univ_prop R R id by unfold_locales simp
   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
   show ?thesis using assms by simp
 qed
 
 lemma carrier_evalRR:
   assumes x: "x \<in> carrier R" and "p \<in> carrier P"
   shows "eval R R id x p \<in> carrier R"
 proof -
   interpret UP_pre_univ_prop R R id by unfold_locales simp
   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
   show ?thesis using assms by simp
 qed
 
 lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR
 
 end
 
 
 
 section \<open>Properties of the Euler \<open>\<phi>\<close>-function\<close>
 text_raw \<open>\label{sec:euler-phi}\<close>
 
 text\<open>
   In this section we prove that for every positive natural number the equation
   $\sum_{d | n}^n \varphi(d) = n$ holds.
 \<close>
 
 lemma dvd_div_ge_1:
   fixes a b :: nat
   assumes "a \<ge> 1" "b dvd a"
   shows "a div b \<ge> 1"
 proof -
   from \<open>b dvd a\<close> obtain c where "a = b * c" ..
   with \<open>a \<ge> 1\<close> show ?thesis by simp
 qed
 
 lemma dvd_nat_bounds:
  fixes n p :: nat
  assumes "p > 0" "n dvd p"
  shows "n > 0 \<and> n \<le> p"
  using assms by (simp add: dvd_pos_nat dvd_imp_le)
 
 (* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of
    HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic
    dependency. *)
 definition phi' :: "nat => nat"
   where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
 
 notation (latex output)
   phi' ("\<phi> _")
 
 lemma phi'_nonzero:
   assumes "m > 0"
   shows "phi' m > 0"
 proof -
   have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" using assms by simp
   hence "card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m} > 0" by (auto simp: card_gt_0_iff)
   thus ?thesis unfolding phi'_def by simp
 qed
 
 lemma dvd_div_eq_1:
   fixes a b c :: nat
   assumes "c dvd a" "c dvd b" "a div c = b div c"
   shows "a = b" using assms dvd_mult_div_cancel[OF \<open>c dvd a\<close>] dvd_mult_div_cancel[OF \<open>c dvd b\<close>]
                 by presburger
 
 lemma dvd_div_eq_2:
   fixes a b c :: nat
   assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"
   shows "a = b"
   proof -
   have "a > 0" "a \<le> c" using dvd_nat_bounds[OF assms(1-2)] by auto
   have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
   also have "\<dots> = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
   finally show "a = b" using \<open>c>0\<close> dvd_div_ge_1[OF _ \<open>a dvd c\<close>] by fastforce
 qed
 
 lemma div_mult_mono:
   fixes a b c :: nat
   assumes "a > 0" "a\<le>d"
   shows "a * b div d \<le> b"
 proof -
   have "a*b div d \<le> b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger
   thus ?thesis using assms by force
 qed
 
 text\<open>
   We arrive at the main result of this section:
   For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.
 
   The outline of the proof for this lemma is as follows:
   We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.
   We analyze the reduced form $a/d = m/n$ for any of those fractions.
   We want to know how many fractions $m/n$ have the reduced form denominator $d$.
   The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.
   Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. \<^term>\<open>gcd a d = 1\<close>.
   This number is exactly \<^term>\<open>phi' d\<close>.
 
   Finally, by counting the fractions $m/n$ according to their reduced form denominator,
   we get: @{term [display] "(\<Sum>d | d dvd n . phi' d) = n"}.
   To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$
   \begin{itemize}
     \item the set of reduced form numerators \<^term>\<open>{a. (1::nat) \<le> a \<and> a \<le> d \<and> coprime a d}\<close>
     \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,
       i.e. the set \<^term>\<open>{m \<in> {1::nat .. n}. n div gcd m n = d}\<close>
   \end{itemize}
   We show that \<^term>\<open>\<lambda>a. a*n div d\<close> with the inverse \<^term>\<open>\<lambda>a. a div gcd a n\<close> is
   a bijection between theses sets, thus yielding the equality
   @{term [display] "phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"}
   This gives us
   @{term [display] "(\<Sum>d | d dvd n . phi' d)
           = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"}
   and by showing
   \<^term>\<open>(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}\<close>
   (this is our counting argument) the thesis follows.
 \<close>
 lemma sum_phi'_factors:
  fixes n :: nat
  assumes "n > 0"
  shows "(\<Sum>d | d dvd n. phi' d) = n"
 proof -
   { fix d assume "d dvd n" then obtain q where q: "n = d * q" ..
     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}"
          (is "card ?RF = card ?F")
     proof (rule card_bij_eq)
       { fix a b assume "a * n div d = b * n div d"
         hence "a * (n div d) = b * (n div d)"
           using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
         hence "a = b" using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
           by (simp add: mult.commute nat_mult_eq_cancel1)
       } thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
       { fix a assume a: "a\<in>?RF"
         hence "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp
         hence ge_1: "a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)
         have le_n: "a * n div d \<le> n" using div_mult_mono a by simp
         have "gcd (a * n div d) n = n div d * gcd a d"
           by (simp add: gcd_mult_distrib_nat q ac_simps)
         hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
         hence "a * n div d \<in> ?F"
           using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
       } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
       { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
         hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
         hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
       } thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast
       { fix m assume "m \<in> ?F"
         hence "m div gcd m n \<in> ?RF" using dvd_div_ge_1
           by (fastforce simp add: div_le_mono div_gcd_coprime)
       } thus "(\<lambda>a. a div gcd a n) ` ?F \<subseteq> ?RF" by blast
     qed force+
   } hence phi'_eq: "\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
       unfolding phi'_def by presburger
   have fin: "finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force
   have "(\<Sum>d | d dvd n. phi' d)
                  = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
     using card_UN_disjoint[OF fin, of "(\<lambda>d. {m \<in> {1 .. n}. n div gcd m n = d})"] phi'_eq
     by fastforce
   also have "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")
   proof
     show "?L \<supseteq> ?R"
     proof
       fix m assume m: "m \<in> ?R"
       thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
         by simp
     qed
   qed fastforce
   finally show ?thesis by force
 qed
 
 
 
 section \<open>Order of an Element of a Group\<close>
 text_raw \<open>\label{sec:order-elem}\<close>
 
 
 context group begin
 
 definition (in group) ord :: "'a \<Rightarrow> nat" where
   "ord x \<equiv> (@d. \<forall>n::nat. x [^] n = \<one> \<longleftrightarrow> d dvd n)"
 
 lemma (in group) pow_eq_id:
   assumes "x \<in> carrier G"
   shows "x [^] n = \<one> \<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
   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)
 
 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)
 
 lemma ord_inj:
   assumes a: "a \<in> carrier G"
   shows "inj_on (\<lambda> x . a [^] x) {0 .. ord a - 1}"
 proof -
   let ?M = "Max (ord ` carrier G)"
   have "finite {d \<in> {..?M}. a [^] d = \<one>}" by auto
 
   have *: False if A: "x < y" "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}"
         "a [^] x = a [^] y" for x y
   proof -
     have "y - x < ord a" using that by auto
     moreover have "a [^] (y-x) = \<one>" using a A by (simp add: pow_eq_div2)
     ultimately have "min (y - x) (ord a) = ord a"
       using A(1) a pow_eq_id by auto
     with \<open>y - x < ord a\<close> show False by linarith
   qed
   show ?thesis
     unfolding inj_on_def by (metis nat_neq_iff *)
 qed
 
 lemma ord_inj':
   assumes a: "a \<in> carrier G"
   shows "inj_on (\<lambda> x . a [^] x) {1 .. ord a}"
 proof (rule inj_onI, rule ccontr)
   fix x y :: nat
   assume A: "x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a [^] x = a [^] y" "x\<noteq>y"
   { assume "x < ord a" "y < ord a"
     hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce
   }
   moreover
   { assume "x = ord a" "y < ord a"
     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 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
   }
   ultimately show False using A  by force
 qed
 
 lemma (in group) ord_ge_1: 
   assumes finite: "finite (carrier G)" and a: "a \<in> carrier G"
   shows "ord a \<ge> 1" 
 proof -
   have "((\<lambda>n::nat. a [^] n) ` {0<..}) \<subseteq> carrier G"
     using a by blast
   then have "finite ((\<lambda>n::nat. a [^] n) ` {0<..})"
     using finite_subset finite by auto
   then have "\<not> inj_on (\<lambda>n::nat. a [^] n) {0<..}"
     using finite_imageD infinite_Ioi by blast
   then obtain i j::nat where "i \<noteq> j" "a [^] i = a [^] j"
     by (auto simp: inj_on_def)
   then have "\<exists>n::nat. n>0 \<and> a [^] n = \<one>"
     by (metis a diffs0_imp_equal pow_eq_div2 neq0_conv)
   then have "ord a \<noteq> 0"
     by (simp add: ord_eq_0 [OF a])
   then show ?thesis
     by simp
 qed
 
 lemma ord_elems:
   assumes "finite (carrier G)" "a \<in> carrier G"
   shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
 proof
   show "?R \<subseteq> ?L" by blast
   { fix y assume "y \<in> ?L"
     then obtain x::nat where x: "y = a[^]x" by auto
     define r q where "r = x mod ord a" and "q = x div ord a"
     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 (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)
     hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast
   }
   thus "?L \<subseteq> ?R" by auto
 qed
 
 lemma (in group)
   assumes "x \<in> carrier G"
   shows finite_cyclic_subgroup:
         "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> x [^] n = \<one>)" (is "?fin \<longleftrightarrow> ?nat1")
     and infinite_cyclic_subgroup:
         "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>m n::nat. x [^] m = x [^] n \<longrightarrow> m = n)" (is "\<not> ?fin \<longleftrightarrow> ?nateq")
     and finite_cyclic_subgroup_int:
         "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>i::int. i \<noteq> 0 \<and> x [^] i = \<one>)" (is "?fin \<longleftrightarrow> ?int1")
     and infinite_cyclic_subgroup_int:
         "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>i j::int. x [^] i = x [^] j \<longrightarrow> i = j)" (is "\<not> ?fin \<longleftrightarrow> ?inteq")
 proof -
   have 1: "\<not> ?fin" if ?nateq
   proof -
     have "infinite (range (\<lambda>n::nat. x [^] n))"
       using that range_inj_infinite [of "(\<lambda>n::nat. x [^] n)"] by (auto simp: inj_on_def)
     moreover have "range (\<lambda>n::nat. x [^] n) \<subseteq> range (\<lambda>i::int. x [^] i)"
       apply clarify
       by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI)
     ultimately show ?thesis
       using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto
   qed
   have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat
     using eq [of "int m" "int n"]
     by (simp add: int_pow_int mn)
   have 3: ?nat1 if non: "\<not> ?inteq"
   proof -
     obtain i j::int where eq: "x [^] i = x [^] j" and "i \<noteq> j"
       using non by auto
     show ?thesis
     proof (cases i j rule: linorder_cases)
       case less
       then have [simp]: "x [^] (j - i) = \<one>"
         by (simp add: eq assms int_pow_diff)
       show ?thesis
         using less by (rule_tac x="nat (j-i)" in exI) auto
     next
       case greater
       then have [simp]: "x [^] (i - j) = \<one>"
         by (simp add: eq assms int_pow_diff)
       then show ?thesis
         using greater by (rule_tac x="nat (i-j)" in exI) auto
     qed (use \<open>i \<noteq> j\<close> in auto)
   qed
   have 4: "\<exists>i::int. (i \<noteq> 0) \<and> x [^] i = \<one>" if "n \<noteq> 0" "x [^] n = \<one>" for n::nat
     apply (rule_tac x="int n" in exI)
     by (simp add: int_pow_int that)
   have 5: "finite (carrier (subgroup_generated G {x}))" if "i \<noteq> 0" and 1: "x [^] i = \<one>" for i::int
   proof -
     obtain n::nat where n: "n > 0" "x [^] n = \<one>"
       using "1" "3" \<open>i \<noteq> 0\<close> by fastforce
     have "x [^] a \<in> ([^]) x ` {0..<n}" for a::int
     proof
       show "x [^] a = x [^] nat (a mod int n)"
         using n
         by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
       show "nat (a mod int n) \<in> {0..<n}"
         using n  apply (simp add:  split: split_nat)
         using Euclidean_Division.pos_mod_bound by presburger
     qed
     then have "carrier (subgroup_generated G {x}) \<subseteq> ([^]) x ` {0..<n}"
       using carrier_subgroup_generated_by_singleton [OF assms] by auto
     then show ?thesis
       using finite_surj by blast
   qed
   show "?fin \<longleftrightarrow> ?nat1" "\<not> ?fin \<longleftrightarrow> ?nateq" "?fin \<longleftrightarrow> ?int1" "\<not> ?fin \<longleftrightarrow> ?inteq"
     using 1 2 3 4 5 by meson+
 qed
 
 lemma (in group) finite_cyclic_subgroup_order:
    "x \<in> carrier G \<Longrightarrow> finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x \<noteq> 0"
   by (simp add: finite_cyclic_subgroup ord_eq_0)
 
 lemma (in group) infinite_cyclic_subgroup_order:
    "x \<in> carrier G \<Longrightarrow> infinite (carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x = 0"
   by (simp add: finite_cyclic_subgroup_order)
 
 lemma generate_pow_on_finite_carrier: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "finite (carrier G)" and a: "a \<in> carrier G"
   shows "generate G { a } = { a [^] k | k. k \<in> (UNIV :: nat set) }"
 proof
   show "{ a [^] k | k. k \<in> (UNIV :: nat set) } \<subseteq> generate G { a }"
   proof
     fix b assume "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }"
     then obtain k :: nat where "b = a [^] k" by blast
     hence "b = a [^] (int k)"
       by (simp add: int_pow_int)
     thus "b \<in> generate G { a }"
       unfolding generate_pow[OF a] by blast
   qed
 next
   show "generate G { a } \<subseteq> { a [^] k | k. k \<in> (UNIV :: nat set) }"
   proof
     fix b assume "b \<in> generate G { a }"
     then obtain k :: int where k: "b = a [^] k"
       unfolding generate_pow[OF a] by blast
     show "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }"
     proof (cases "k < 0")
       assume "\<not> k < 0"
       hence "b = a [^] (nat k)"
         by (simp add: k)
       thus ?thesis by blast
     next
       assume "k < 0"
       hence b: "b = inv (a [^] (nat (- k)))"
         using k a by (auto simp: int_pow_neg)
       obtain m where m: "ord a * m \<ge> nat (- k)"
         by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
       hence "a [^] (ord a * m) = \<one>"
         by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
       then obtain k' :: nat where "(a [^] (nat (- k))) \<otimes> (a [^] k') = \<one>"
         using m a nat_le_iff_add nat_pow_mult by auto
       hence "b = a [^] k'"
         using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
       thus "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }" by blast
     qed
   qed
 qed
 
 lemma ord_elems_inf_carrier:
  assumes "a \<in> carrier G" "ord a \<noteq> 0"
  shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
 proof
  show "?R \<subseteq> ?L" by blast
  { fix y assume "y \<in> ?L"
    then obtain x::nat where x: "y = a[^]x" by auto
    define r q where "r = x mod ord a" and "q = x div ord a"
    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 (metis mult.commute nat_pow_mult nat_pow_pow)
    hence "y = a[^]r" using assms by simp
    have "r < ord a" using assms by (simp add: r_def)
    hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
    hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast
  }
  thus "?L \<subseteq> ?R" by auto
 qed
 
 lemma generate_pow_nat:
  assumes a: "a \<in> carrier G" and "ord a \<noteq> 0"
  shows "generate G { a } = { a [^] k | k. k \<in> (UNIV :: nat set) }"
 proof
  show "{ a [^] k | k. k \<in> (UNIV :: nat set) } \<subseteq> generate G { a }"
  proof
    fix b assume "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }"
    then obtain k :: nat where "b = a [^] k" by blast
    hence "b = a [^] (int k)"
      by (simp add: int_pow_int)
    thus "b \<in> generate G { a }"
      unfolding generate_pow[OF a] by blast
  qed
 next
  show "generate G { a } \<subseteq> { a [^] k | k. k \<in> (UNIV :: nat set) }"
  proof
    fix b assume "b \<in> generate G { a }"
    then obtain k :: int where k: "b = a [^] k"
      unfolding generate_pow[OF a] by blast
    show "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }"
    proof (cases "k < 0")
      assume "\<not> k < 0"
      hence "b = a [^] (nat k)"
        by (simp add: k)
      thus ?thesis by blast
    next
      assume "k < 0"
      hence b: "b = inv (a [^] (nat (- k)))"
        using k a by (auto simp: int_pow_neg)
      obtain m where m: "ord a * m \<ge> nat (- k)"
        by (metis assms(2) dvd_imp_le dvd_triv_right le_zero_eq mult_eq_0_iff not_gr_zero)
      hence "a [^] (ord a * m) = \<one>"
        by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
      then obtain k' :: nat where "(a [^] (nat (- k))) \<otimes> (a [^] k') = \<one>"
        using m a nat_le_iff_add nat_pow_mult by auto
      hence "b = a [^] k'"
        using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
      thus "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }" by blast
    qed
  qed
 qed
 
 lemma generate_pow_card:
   assumes a: "a \<in> carrier G"
   shows "ord a = card (generate G { a })"
 proof (cases "ord a = 0")
   case True
   then have "infinite (carrier (subgroup_generated G {a}))"
     using infinite_cyclic_subgroup_order[OF a] by auto
   then have "infinite (generate G {a})"
     unfolding subgroup_generated_def
     using a by simp
   then show ?thesis
-    using `ord a = 0` by auto
+    using \<open>ord a = 0\<close> by auto
 next
   case False
   note finite_subgroup = this
   then have "generate G { a } = (([^]) a) ` {0..ord a - 1}"
     using generate_pow_nat ord_elems_inf_carrier a by auto
   hence "card (generate G {a}) = card {0..ord a - 1}"
     using ord_inj[OF a] card_image by metis
   also have "... = ord a" using finite_subgroup by auto
   finally show ?thesis.. 
 qed
 
 lemma (in group) cyclic_order_is_ord:
  assumes "g \<in> carrier G"
  shows "ord g = order (subgroup_generated G {g})"
  unfolding order_def subgroup_generated_def
  using assms generate_pow_card by simp
 
 lemma ord_dvd_group_order:
   assumes "a \<in> carrier G" shows "(ord a) dvd (order G)"
   using lagrange[OF generate_is_subgroup[of "{a}"]] assms
   unfolding generate_pow_card[OF assms]
   by (metis dvd_triv_right empty_subsetI insert_subset)
 
 lemma (in group) pow_order_eq_1:
   assumes "a \<in> carrier G" shows "a [^] order G = \<one>"
   using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)
 
 lemma dvd_gcd:
   fixes a b :: nat
   obtains q where "a * (b div gcd a b) = b*q"
 proof
   have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add:  div_mult_swap dvd_div_mult)
   also have "\<dots> = b * (a div gcd a b)" by simp
   finally show "a * (b div gcd a b) = b * (a div gcd a b) " .
 qed
 
 lemma (in group) ord_le_group_order:
   assumes finite: "finite (carrier G)" and a: "a \<in> carrier G"
   shows "ord a \<le> order G"
   by (simp add: a dvd_imp_le local.finite ord_dvd_group_order order_gt_0_iff_finite)
 
 lemma (in group) ord_pow_gen:
   assumes "x \<in> carrier G"
   shows "ord (pow G x k) = (if k = 0 then 1 else ord x div gcd (ord x) k)"
 proof -
   have "ord (x [^] k) = ord x div gcd (ord x) k"
     if "0 < k"
   proof -
     have "(d dvd k * n) = (d div gcd (d) k dvd n)" for d n
       using that by (simp add: div_dvd_iff_mult gcd_mult_distrib_nat mult.commute)
     then show ?thesis
       using that by (auto simp add: assms ord_unique nat_pow_pow pow_eq_id)
   qed
   then show ?thesis by auto
 qed
 
 lemma (in group)
   assumes finite': "finite (carrier G)" "a \<in> carrier G"
   shows pow_ord_eq_ord_iff: "group.ord G (a [^] k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
     using assms ord_ge_1 [OF assms]
     by (auto simp: div_eq_dividend_iff ord_pow_gen coprime_iff_gcd_eq_1 gcd.commute split: if_split_asm)
 
 lemma element_generates_subgroup:
   assumes finite[simp]: "finite (carrier G)"
   assumes a[simp]: "a \<in> carrier G"
   shows "subgroup {a [^] i | i. i \<in> {0 .. ord a - 1}} G"
   using generate_is_subgroup[of "{ a }"] assms(2)
         generate_pow_on_finite_carrier[OF assms]
   unfolding ord_elems[OF assms] by auto
 
 end
 
 
 section \<open>Number of Roots of a Polynomial\<close>
 text_raw \<open>\label{sec:number-roots}\<close>
 
 
 definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
   "mult_of R \<equiv> \<lparr> carrier = carrier R - {\<zero>\<^bsub>R\<^esub>}, mult = mult R, one = \<one>\<^bsub>R\<^esub>\<rparr>"
 
 lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"
   by (simp add: mult_of_def)
 
 lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
  by (simp add: mult_of_def)
 
 lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
   by (simp add: mult_of_def fun_eq_iff nat_pow_def)
 
 lemma one_mult_of [simp]: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
   by (simp add: mult_of_def)
 
 lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
 
 context field
 begin
 
 lemma mult_of_is_Units: "mult_of R = units_of R"
   unfolding mult_of_def units_of_def using field_Units by auto
 
 lemma m_inv_mult_of:
 "\<And>x. x \<in> carrier (mult_of R) \<Longrightarrow> m_inv (mult_of R) x = m_inv R x"
   using mult_of_is_Units units_of_inv unfolding units_of_def
   by simp
 
 lemma (in field) field_mult_group: "group (mult_of R)"
   proof (rule groupI)
   show "\<exists>y\<in>carrier (mult_of R). y \<otimes>\<^bsub>mult_of R\<^esub> x = \<one>\<^bsub>mult_of R\<^esub>"
     if "x \<in> carrier (mult_of R)" for x
     using group.l_inv_ex mult_of_is_Units that units_group by fastforce
 qed (auto simp: m_assoc dest: integral)
 
 lemma finite_mult_of: "finite (carrier R) \<Longrightarrow> finite (carrier (mult_of R))"
   by simp
 
 lemma order_mult_of: "finite (carrier R) \<Longrightarrow> order (mult_of R) = order R - 1"
   unfolding order_def carrier_mult_of by (simp add: card.remove)
 
 end
 
 
 
 lemma (in monoid) Units_pow_closed :
   fixes d :: nat
   assumes "x \<in> Units G"
   shows "x [^] d \<in> Units G"
     by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)
 
 lemma (in ring) r_right_minus_eq[simp]:
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "a \<ominus> b = \<zero> \<longleftrightarrow> a = b"
   using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)
 
 context UP_cring begin
 
 lemma is_UP_cring: "UP_cring R" by (unfold_locales)
 lemma is_UP_ring:
   shows "UP_ring R" by (unfold_locales)
 
 end
 
 context UP_domain begin
 
 
 lemma roots_bound:
   assumes f [simp]: "f \<in> carrier P"
   assumes f_not_zero: "f \<noteq> \<zero>\<^bsub>P\<^esub>"
   assumes finite: "finite (carrier R)"
   shows "finite {a \<in> carrier R . eval R R id a f = \<zero>} \<and>
          card {a \<in> carrier R . eval R R id a f = \<zero>} \<le> deg R f" using f f_not_zero
 proof (induction "deg R f" arbitrary: f)
   case 0
   have "\<And>x. eval R R id x f \<noteq> \<zero>"
   proof -
     fix x
     have "(\<Oplus>i\<in>{..deg R f}. id (coeff P f i) \<otimes> x [^] i) \<noteq> \<zero>"
       using 0 lcoeff_nonzero_nonzero[where p = f] by simp
     thus "eval R R id x f \<noteq> \<zero>" using 0 unfolding eval_def P_def by simp
   qed
   then have *: "{a \<in> carrier R. eval R R (\<lambda>a. a) a f = \<zero>} = {}"
     by (auto simp: id_def)
   show ?case by (simp add: *)
 next
   case (Suc x)
   show ?case
   proof (cases "\<exists> a \<in> carrier R . eval R R id a f = \<zero>")
     case True
     then obtain a where a_carrier[simp]: "a \<in> carrier R" and a_root: "eval R R id a f = \<zero>" by blast
     have R_not_triv: "carrier R \<noteq> {\<zero>}"
       by (metis R.one_zeroI R.zero_not_one)
     obtain q  where q: "(q \<in> carrier P)" and
       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"
      using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto
     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)
     have deg: "deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) = 1"
       using a_carrier by (simp add: deg_minus_eq)
     hence mon_not_zero: "(monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<noteq> \<zero>\<^bsub>P\<^esub>"
       by (fastforce simp del: r_right_minus_eq)
     have q_not_zero: "q \<noteq> \<zero>\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac)
     hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]
       by (simp add : lin_fac)
     hence q_IH: "finite {a \<in> carrier R . eval R R id a q = \<zero>}
                 \<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast
     have subs: "{a \<in> carrier R . eval R R id a f = \<zero>}
                 \<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")
       using a_carrier \<open>q \<in> _\<close>
       by (auto simp: evalRR_simps lin_fac R.integral_iff)
     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>}"
      using subs by auto
     hence "card {a \<in> carrier R . eval R R id a f = \<zero>} \<le>
            card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)
     also have "\<dots> \<le> deg R f" using q_IH \<open>Suc x = _\<close>
       by (simp add: card_insert_if)
     finally show ?thesis using q_IH \<open>Suc x = _\<close> using finite by force
   next
     case False
     hence "card {a \<in> carrier R. eval R R id a f = \<zero>} = 0" using finite by auto
     also have "\<dots> \<le>  deg R f" by simp
     finally show ?thesis using finite by auto
   qed
 qed
 
 end
 
 lemma (in domain) num_roots_le_deg :
   fixes p d :: nat
   assumes finite: "finite (carrier R)"
   assumes d_neq_zero: "d \<noteq> 0"
   shows "card {x \<in> carrier R. x [^] d = \<one>} \<le> d"
 proof -
   let ?f = "monom (UP R) \<one>\<^bsub>R\<^esub> d \<ominus>\<^bsub> (UP R)\<^esub> monom (UP R) \<one>\<^bsub>R\<^esub> 0"
   have one_in_carrier: "\<one> \<in> carrier R" by simp
   interpret R: UP_domain R "UP R" by (unfold_locales)
   have "deg R ?f = d"
     using d_neq_zero by (simp add: R.deg_minus_eq)
   hence f_not_zero: "?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using  d_neq_zero by (auto simp add : R.deg_nzero_nzero)
   have roots_bound: "finite {a \<in> carrier R . eval R R id a ?f = \<zero>} \<and>
                     card {a \<in> carrier R . eval R R id a ?f = \<zero>} \<le> deg R ?f"
                     using finite by (intro R.roots_bound[OF _ f_not_zero]) simp
   have subs: "{x \<in> carrier R. x [^] d = \<one>} \<subseteq> {a \<in> carrier R . eval R R id a ?f = \<zero>}"
     by (auto simp: R.evalRR_simps)
   then have "card {x \<in> carrier R. x [^] d = \<one>} \<le>
         card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
   thus ?thesis using \<open>deg R ?f = d\<close> roots_bound by linarith
 qed
 
 
 
 section \<open>The Multiplicative Group of a Field\<close>
 text_raw \<open>\label{sec:mult-group}\<close>
 
 
 text \<open>
   In this section we show that the multiplicative group of a finite field
   is generated by a single element, i.e. it is cyclic. The proof is inspired
   by the first proof given in the survey~@{cite "conrad-cyclicity"}.
 \<close>
 
 context field begin
 
 lemma num_elems_of_ord_eq_phi':
   assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"
       and exists: "\<exists>a\<in>carrier (mult_of R). group.ord (mult_of R) a = d"
   shows "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"
 proof -
   note mult_of_simps[simp]
   have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
 
   interpret G:group "mult_of R" rewrites "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
     by (rule field_mult_group) simp_all
 
   from exists
   obtain a where a: "a \<in> carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"
     by (auto simp add: card_gt_0_iff)
 
   have set_eq1: "{a[^]n| n. n \<in> {1 .. d}} = {x \<in> carrier (mult_of R). x [^] d = \<one>}"
   proof (rule card_seteq)
     show "finite {x \<in> carrier (mult_of R). x [^] d = \<one>}" using finite by auto
 
     show "{a[^]n| n. n \<in> {1 ..d}} \<subseteq> {x \<in> carrier (mult_of R). x[^]d = \<one>}"
     proof
       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 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
 
     show "card {x \<in> carrier (mult_of R). x [^] d = \<one>} \<le> card {a[^]n | n. n \<in> {1 .. d}}"
     proof -
       have *: "{a[^]n | n. n \<in> {1 .. d }} = ((\<lambda> n. a[^]n) ` {1 .. d})" by auto
       have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]
         using card_mono[OF finite, of "{\<zero>, \<one>}"] by (simp add: order_def)
       have "card {x \<in> carrier (mult_of R). x [^] d = \<one>} \<le> card {x \<in> carrier R. x [^] d = \<one>}"
         using finite by (auto intro: card_mono)
       also have "\<dots> \<le> d" using \<open>0 < order (mult_of R)\<close> num_roots_le_deg[OF finite, of d]
         by (simp add : dvd_pos_nat[OF _ \<open>d dvd order (mult_of R)\<close>])
       finally show ?thesis using G.ord_inj'[OF a] ord_a * by (simp add: card_image)
     qed
   qed
 
   have set_eq2: "{x \<in> carrier (mult_of R) . group.ord (mult_of R) x = d}
                 = (\<lambda> n . a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")
   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 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
     show "?R \<subseteq> ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
   qed
   have "inj_on (\<lambda> n . a[^]n) {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"
     using G.ord_inj'[OF a, unfolded ord_a] unfolding inj_on_def by fast
   hence "card ((\<lambda>n. a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d})
          = card {k \<in> {1 .. d}. group.ord (mult_of R) (a[^]k) = d}"
          using card_image by blast
   thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \<open>a \<in> _\<close>, unfolded ord_a]
     by (simp add: phi'_def)
 qed
 
 end
 
 
 theorem (in field) finite_field_mult_group_has_gen :
   assumes finite: "finite (carrier R)"
   shows "\<exists> a \<in> carrier (mult_of R) . carrier (mult_of R) = {a[^]i | i::nat . i \<in> UNIV}"
 proof -
   note mult_of_simps[simp]
   have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
 
   interpret G: group "mult_of R" rewrites
       "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
     by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)
 
   let ?N = "\<lambda> x . card {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = x}"
   have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\<zero>, \<one>}"] by simp
   then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)
   have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force
 
   have "(\<Sum>d | d dvd order (mult_of R). ?N d)
       = card (UN d:{d . d dvd order (mult_of R) }. {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = d})"
       (is "_ = card ?U")
     using fin finite by (subst card_UN_disjoint) auto
   also have "?U = carrier (mult_of R)"
   proof
     { fix x assume x: "x \<in> carrier (mult_of R)"
       hence x': "x\<in>carrier (mult_of R)" by simp
       then have "group.ord (mult_of R) x dvd order (mult_of R)"
         using G.ord_dvd_group_order by blast
       hence "x \<in> ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
     } thus "carrier (mult_of R) \<subseteq> ?U" by blast
   qed auto
   also have "card ... = order (mult_of R)"
     using order_mult_of finite' by (simp add: order_def)
   finally have sum_Ns_eq: "(\<Sum>d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .
 
   { fix d assume d: "d dvd order (mult_of R)"
     have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"
     proof cases
       assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger
       next
       assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<noteq> 0"
       hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
       thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
     qed
   }
   hence all_le: "\<And>i. i \<in> {d. d dvd order (mult_of R) }
         \<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
   hence le: "(\<Sum>i | i dvd order (mult_of R). ?N i)
             \<le> (\<Sum>i | i dvd order (mult_of R). phi' i)"
             using sum_mono[of "{d .  d dvd order (mult_of R)}"
                   "\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger
   have "order (mult_of R) = (\<Sum>d | d dvd order (mult_of R). phi' d)" using *
     by (simp add: sum_phi'_factors)
   hence eq: "(\<Sum>i | i dvd order (mult_of R). ?N i)
           = (\<Sum>i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger
   have "\<And>i. i \<in> {d. d dvd order (mult_of R) } \<Longrightarrow> ?N i = (\<lambda>i. phi' i) i"
   proof (rule ccontr)
     fix i
     assume i1: "i \<in> {d. d dvd order (mult_of R)}" and "?N i \<noteq> phi' i"
     hence "?N i = 0"
       using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)
     moreover  have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])
     ultimately have "?N i < phi' i" using phi'_nonzero by presburger
     hence "(\<Sum>i | i dvd order (mult_of R). ?N i)
          < (\<Sum>i | i dvd order (mult_of R). phi' i)"
       using sum_strict_mono_ex1[OF fin, of "?N" "\<lambda> i . phi' i"]
             i1 all_le by auto
     thus False using eq by force
   qed
   hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)
   then obtain a where a: "a \<in> carrier (mult_of R)" and a_ord: "group.ord (mult_of R) a = order (mult_of R)"
     by (auto simp add: card_gt_0_iff)
   hence set_eq: "{a[^]i | i::nat. i \<in> UNIV} = (\<lambda>x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}"
     using G.ord_elems[OF finite'] by auto
   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}"
     by (intro card_image G.ord_inj finite' a)
   hence "card ((\<lambda> x . a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
     using assms by (simp add: card_eq a_ord)
   hence card_R_minus_1: "card {a[^]i | i::nat. i \<in> UNIV} =  order (mult_of R)"
     using * by (subst set_eq) auto
   have **: "{a[^]i | i::nat. i \<in> UNIV} \<subseteq> carrier (mult_of R)"
     using G.nat_pow_closed[OF a] by auto
   with _ have "carrier (mult_of R) = {a[^]i|i::nat. i \<in> UNIV}"
     by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)
   thus ?thesis using a by blast
 qed
 
 end
diff --git a/src/HOL/Lattices_Big.thy b/src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy
+++ b/src/HOL/Lattices_Big.thy
@@ -1,1060 +1,1060 @@
 (*  Title:      HOL/Lattices_Big.thy
     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
                 with contributions by Jeremy Avigad
 *)
 
 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
 
 theory Lattices_Big
   imports Option
 begin
 
 subsection \<open>Generic lattice operations over a set\<close>
 
 subsubsection \<open>Without neutral element\<close>
 
 locale semilattice_set = semilattice
 begin
 
 interpretation comp_fun_idem f
   by standard (simp_all add: fun_eq_iff left_commute)
 
 definition F :: "'a set \<Rightarrow> 'a"
 where
   eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
 
 lemma eq_fold:
   assumes "finite A"
   shows "F (insert x A) = Finite_Set.fold f x A"
 proof (rule sym)
   let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
   interpret comp_fun_idem "?f"
     by standard (simp_all add: fun_eq_iff commute left_commute split: option.split)
   from assms show "Finite_Set.fold f x A = F (insert x A)"
   proof induct
     case empty then show ?case by (simp add: eq_fold')
   next
     case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
   qed
 qed
 
 lemma singleton [simp]:
   "F {x} = x"
   by (simp add: eq_fold)
 
 lemma insert_not_elem:
   assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
   shows "F (insert x A) = x \<^bold>* F A"
 proof -
   from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
   with \<open>finite A\<close> and \<open>x \<notin> A\<close>
     have "finite (insert x B)" and "b \<notin> insert x B" by auto
   then have "F (insert b (insert x B)) = x \<^bold>* F (insert b B)"
     by (simp add: eq_fold)
   then show ?thesis by (simp add: * insert_commute)
 qed
 
 lemma in_idem:
   assumes "finite A" and "x \<in> A"
   shows "x \<^bold>* F A = F A"
 proof -
   from assms have "A \<noteq> {}" by auto
   with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
 qed
 
 lemma insert [simp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "F (insert x A) = x \<^bold>* F A"
   using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
 
 lemma union:
   assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
   shows "F (A \<union> B) = F A \<^bold>* F B"
   using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
 
 lemma remove:
   assumes "finite A" and "x \<in> A"
   shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
 proof -
   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   with assms show ?thesis by simp
 qed
 
 lemma insert_remove:
   assumes "finite A"
   shows "F (insert x A) = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
 
 lemma subset:
   assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
   shows "F B \<^bold>* F A = F A"
 proof -
   from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
 qed
 
 lemma closed:
   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
   shows "F A \<in> A"
 using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
   case singleton then show ?case by simp
 next
   case insert with elem show ?case by force
 qed
 
 lemma hom_commute:
   assumes hom: "\<And>x y. h (x \<^bold>* y) = h x \<^bold>* h y"
   and N: "finite N" "N \<noteq> {}"
   shows "h (F N) = F (h ` N)"
 using N proof (induct rule: finite_ne_induct)
   case singleton thus ?case by simp
 next
   case (insert n N)
   then have "h (F (insert n N)) = h (n \<^bold>* F N)" by simp
   also have "\<dots> = h n \<^bold>* h (F N)" by (rule hom)
   also have "h (F N) = F (h ` N)" by (rule insert)
   also have "h n \<^bold>* \<dots> = F (insert (h n) (h ` N))"
     using insert by simp
   also have "insert (h n) (h ` N) = h ` insert n N" by simp
   finally show ?case .
 qed
 
 lemma infinite: "\<not> finite A \<Longrightarrow> F A = the None"
   unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite)
 
 end
 
 locale semilattice_order_set = binary?: semilattice_order + semilattice_set
 begin
 
 lemma bounded_iff:
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
   using assms by (induct rule: finite_ne_induct) simp_all
 
 lemma boundedI:
   assumes "finite A"
   assumes "A \<noteq> {}"
   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   shows "x \<^bold>\<le> F A"
   using assms by (simp add: bounded_iff)
 
 lemma boundedE:
   assumes "finite A" and "A \<noteq> {}" and "x \<^bold>\<le> F A"
   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   using assms by (simp add: bounded_iff)
 
 lemma coboundedI:
   assumes "finite A"
     and "a \<in> A"
   shows "F A \<^bold>\<le> a"
 proof -
   from assms have "A \<noteq> {}" by auto
   from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
   proof (induct rule: finite_ne_induct)
     case singleton thus ?case by (simp add: refl)
   next
     case (insert x B)
     from insert have "a = x \<or> a \<in> B" by simp
     then show ?case using insert by (auto intro: coboundedI2)
   qed
 qed
 
 lemma subset_imp:
   assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
   shows "F B \<^bold>\<le> F A"
 proof (cases "A = B")
   case True then show ?thesis by (simp add: refl)
 next
   case False
   have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
   then have "F B = F (A \<union> (B - A))" by simp
   also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   also have "\<dots> \<^bold>\<le> F A" by simp
   finally show ?thesis .
 qed
 
 end
 
 
 subsubsection \<open>With neutral element\<close>
 
 locale semilattice_neutr_set = semilattice_neutr
 begin
 
 interpretation comp_fun_idem f
   by standard (simp_all add: fun_eq_iff left_commute)
 
 definition F :: "'a set \<Rightarrow> 'a"
 where
   eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"
 
 lemma infinite [simp]:
   "\<not> finite A \<Longrightarrow> F A = \<^bold>1"
   by (simp add: eq_fold)
 
 lemma empty [simp]:
   "F {} = \<^bold>1"
   by (simp add: eq_fold)
 
 lemma insert [simp]:
   assumes "finite A"
   shows "F (insert x A) = x \<^bold>* F A"
   using assms by (simp add: eq_fold)
 
 lemma in_idem:
   assumes "finite A" and "x \<in> A"
   shows "x \<^bold>* F A = F A"
 proof -
   from assms have "A \<noteq> {}" by auto
   with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
 qed
 
 lemma union:
   assumes "finite A" and "finite B"
   shows "F (A \<union> B) = F A \<^bold>* F B"
   using assms by (induct A) (simp_all add: ac_simps)
 
 lemma remove:
   assumes "finite A" and "x \<in> A"
   shows "F A = x \<^bold>* F (A - {x})"
 proof -
   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   with assms show ?thesis by simp
 qed
 
 lemma insert_remove:
   assumes "finite A"
   shows "F (insert x A) = x \<^bold>* F (A - {x})"
   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
 
 lemma subset:
   assumes "finite A" and "B \<subseteq> A"
   shows "F B \<^bold>* F A = F A"
 proof -
   from assms have "finite B" by (auto dest: finite_subset)
   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
 qed
 
 lemma closed:
   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
   shows "F A \<in> A"
 using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
   case singleton then show ?case by simp
 next
   case insert with elem show ?case by force
 qed
 
 end
 
 locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
 begin
 
 lemma bounded_iff:
   assumes "finite A"
   shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
   using assms by (induct A) simp_all
 
 lemma boundedI:
   assumes "finite A"
   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   shows "x \<^bold>\<le> F A"
   using assms by (simp add: bounded_iff)
 
 lemma boundedE:
   assumes "finite A" and "x \<^bold>\<le> F A"
   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   using assms by (simp add: bounded_iff)
 
 lemma coboundedI:
   assumes "finite A"
     and "a \<in> A"
   shows "F A \<^bold>\<le> a"
 proof -
   from assms have "A \<noteq> {}" by auto
   from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
   proof (induct rule: finite_ne_induct)
     case singleton thus ?case by (simp add: refl)
   next
     case (insert x B)
     from insert have "a = x \<or> a \<in> B" by simp
     then show ?case using insert by (auto intro: coboundedI2)
   qed
 qed
 
 lemma subset_imp:
   assumes "A \<subseteq> B" and "finite B"
   shows "F B \<^bold>\<le> F A"
 proof (cases "A = B")
   case True then show ?thesis by (simp add: refl)
 next
   case False
   have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
   then have "F B = F (A \<union> (B - A))" by simp
   also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   also have "\<dots> \<^bold>\<le> F A" by simp
   finally show ?thesis .
 qed
 
 end
 
 
 subsection \<open>Lattice operations on finite sets\<close>
 
 context semilattice_inf
 begin
 
 sublocale Inf_fin: semilattice_order_set inf less_eq less
 defines
   Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Inf_fin.F ..
 
 end
 
 context semilattice_sup
 begin
 
 sublocale Sup_fin: semilattice_order_set sup greater_eq greater
 defines
   Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Sup_fin.F ..
 
 end
 
 
 subsection \<open>Infimum and Supremum over non-empty sets\<close>
 
 context lattice
 begin
 
 lemma Inf_fin_le_Sup_fin [simp]: 
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
 proof -
   from \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" by blast
   with \<open>finite A\<close> have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
   moreover from \<open>finite A\<close> \<open>a \<in> A\<close> have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
   ultimately show ?thesis by (rule order_trans)
 qed
 
 lemma sup_Inf_absorb [simp]:
   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
   by (rule sup_absorb2) (rule Inf_fin.coboundedI)
 
 lemma inf_Sup_absorb [simp]:
   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
   by (rule inf_absorb1) (rule Sup_fin.coboundedI)
 
 end
 
 context distrib_lattice
 begin
 
 lemma sup_Inf1_distrib:
   assumes "finite A"
     and "A \<noteq> {}"
   shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
   (rule arg_cong [where f="Inf_fin"], blast)
 
 lemma sup_Inf2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton then show ?case
     by (simp add: sup_Inf1_distrib [OF B])
 next
   case (insert x A)
   have finB: "finite {sup x b |b. b \<in> B}"
     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   proof -
     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (\<Union>a\<in>A. \<Union>b\<in>B. {sup a b})"
       by blast
     thus ?thesis by(simp add: insert(1) B(1))
   qed
   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)"
     using insert by simp
   also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
   also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:sup_Inf1_distrib[OF B])
   also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
     (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
     using B insert
     by (simp add: Inf_fin.union [OF finB _ finAB ne])
   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
     by blast
   finally show ?case .
 qed
 
 lemma inf_Sup1_distrib:
   assumes "finite A" and "A \<noteq> {}"
   shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
   (rule arg_cong [where f="Sup_fin"], blast)
 
 lemma inf_Sup2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
     by(simp add: inf_Sup1_distrib [OF B])
 next
   case (insert x A)
   have finB: "finite {inf x b |b. b \<in> B}"
     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   proof -
     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (\<Union>a\<in>A. \<Union>b\<in>B. {inf a b})"
       by blast
     thus ?thesis by(simp add: insert(1) B(1))
   qed
   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)"
     using insert by simp
   also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
   also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:inf_Sup1_distrib[OF B])
   also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
     (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
     using B insert
     by (simp add: Sup_fin.union [OF finB _ finAB ne])
   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
     by blast
   finally show ?case .
 qed
 
 end
 
 context complete_lattice
 begin
 
 lemma Inf_fin_Inf:
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A"
 proof -
   from assms obtain b B where "A = insert b B" and "finite B" by auto
   then show ?thesis
     by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
 qed
 
 lemma Sup_fin_Sup:
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A"
 proof -
   from assms obtain b B where "A = insert b B" and "finite B" by auto
   then show ?thesis
     by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
 qed
 
 end
 
 
 subsection \<open>Minimum and Maximum over non-empty sets\<close>
 
 context linorder
 begin
 
 sublocale Min: semilattice_order_set min less_eq less
   + Max: semilattice_order_set max greater_eq greater
 defines
   Min = Min.F and Max = Max.F ..
 
 end
 
 syntax
   "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
   "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _\<in>_./ _)" [0, 0, 10] 10)
   "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
   "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
 
 translations
   "MIN x y. f"   \<rightleftharpoons> "MIN x. MIN y. f"
   "MIN x. f"     \<rightleftharpoons> "CONST Min (CONST range (\<lambda>x. f))"
   "MIN x\<in>A. f"   \<rightleftharpoons> "CONST Min ((\<lambda>x. f) ` A)"
   "MAX x y. f"   \<rightleftharpoons> "MAX x. MAX y. f"
   "MAX x. f"     \<rightleftharpoons> "CONST Max (CONST range (\<lambda>x. f))"
   "MAX x\<in>A. f"   \<rightleftharpoons> "CONST Max ((\<lambda>x. f) ` A)"
 
 text \<open>An aside: \<^const>\<open>Min\<close>/\<^const>\<open>Max\<close> on linear orders as special case of \<^const>\<open>Inf_fin\<close>/\<^const>\<open>Sup_fin\<close>\<close>
 
 lemma Inf_fin_Min:
   "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
   by (simp add: Inf_fin_def Min_def inf_min)
 
 lemma Sup_fin_Max:
   "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
   by (simp add: Sup_fin_def Max_def sup_max)
 
 context linorder
 begin
 
 lemma dual_min:
   "ord.min greater_eq = max"
   by (auto simp add: ord.min_def max_def fun_eq_iff)
 
 lemma dual_max:
   "ord.max greater_eq = min"
   by (auto simp add: ord.max_def min_def fun_eq_iff)
 
 lemma dual_Min:
   "linorder.Min greater_eq = Max"
 proof -
   interpret dual: linorder greater_eq greater by (fact dual_linorder)
   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
 qed
 
 lemma dual_Max:
   "linorder.Max greater_eq = Min"
 proof -
   interpret dual: linorder greater_eq greater by (fact dual_linorder)
   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
 qed
 
 lemmas Min_singleton = Min.singleton
 lemmas Max_singleton = Max.singleton
 lemmas Min_insert = Min.insert
 lemmas Max_insert = Max.insert
 lemmas Min_Un = Min.union
 lemmas Max_Un = Max.union
 lemmas hom_Min_commute = Min.hom_commute
 lemmas hom_Max_commute = Max.hom_commute
 
 lemma Min_in [simp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<in> A"
   using assms by (auto simp add: min_def Min.closed)
 
 lemma Max_in [simp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<in> A"
   using assms by (auto simp add: max_def Max.closed)
 
 lemma Min_insert2:
   assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
   shows "Min (insert a A) = a"
 proof (cases "A = {}")
   case True
   then show ?thesis by simp
 next
   case False
   with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
     by simp
   moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
   ultimately show ?thesis by (simp add: min.absorb1)
 qed
 
 lemma Max_insert2:
   assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
   shows "Max (insert a A) = a"
 proof (cases "A = {}")
   case True
   then show ?thesis by simp
 next
   case False
   with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
     by simp
   moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
   ultimately show ?thesis by (simp add: max.absorb1)
 qed
 
 lemma Min_le [simp]:
   assumes "finite A" and "x \<in> A"
   shows "Min A \<le> x"
   using assms by (fact Min.coboundedI)
 
 lemma Max_ge [simp]:
   assumes "finite A" and "x \<in> A"
   shows "x \<le> Max A"
   using assms by (fact Max.coboundedI)
 
 lemma Min_eqI:
   assumes "finite A"
   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
     and "x \<in> A"
   shows "Min A = x"
 proof (rule antisym)
   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
   with assms show "Min A \<ge> x" by simp
 next
   from assms show "x \<ge> Min A" by simp
 qed
 
 lemma Max_eqI:
   assumes "finite A"
   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
     and "x \<in> A"
   shows "Max A = x"
 proof (rule antisym)
   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
   with assms show "Max A \<le> x" by simp
 next
   from assms show "x \<le> Max A" by simp
 qed
 
 lemma eq_Min_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
 by (meson Min_in Min_le antisym)
 
 lemma Min_eq_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
 by (meson Min_in Min_le antisym)
 
 lemma eq_Max_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
 by (meson Max_in Max_ge antisym)
 
 lemma Max_eq_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
 by (meson Max_in Max_ge antisym)
 
 context
   fixes A :: "'a set"
   assumes fin_nonempty: "finite A" "A \<noteq> {}"
 begin
 
 lemma Min_ge_iff [simp]:
   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   using fin_nonempty by (fact Min.bounded_iff)
 
 lemma Max_le_iff [simp]:
   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   using fin_nonempty by (fact Max.bounded_iff)
 
 lemma Min_gr_iff [simp]:
   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
 
 lemma Max_less_iff [simp]:
   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
 
 lemma Min_le_iff:
   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
 
 lemma Max_ge_iff:
   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
 
 lemma Min_less_iff:
   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
 
 lemma Max_gr_iff:
   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
 
 end
 
 lemma Max_eq_if:
   assumes "finite A"  "finite B"  "\<forall>a\<in>A. \<exists>b\<in>B. a \<le> b"  "\<forall>b\<in>B. \<exists>a\<in>A. b \<le> a"
   shows "Max A = Max B"
 proof cases
   assume "A = {}" thus ?thesis using assms by simp
 next
   assume "A \<noteq> {}" thus ?thesis using assms
     by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
 qed
 
 lemma Min_antimono:
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Min N \<le> Min M"
   using assms by (fact Min.subset_imp)
 
 lemma Max_mono:
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Max M \<le> Max N"
   using assms by (fact Max.subset_imp)
 
 end
 
 context linorder  (* FIXME *)
 begin
 
 lemma mono_Min_commute:
   assumes "mono f"
   assumes "finite A" and "A \<noteq> {}"
   shows "f (Min A) = Min (f ` A)"
 proof (rule linorder_class.Min_eqI [symmetric])
   from \<open>finite A\<close> show "finite (f ` A)" by simp
   from assms show "f (Min A) \<in> f ` A" by simp
   fix x
   assume "x \<in> f ` A"
   then obtain y where "y \<in> A" and "x = f y" ..
   with assms have "Min A \<le> y" by auto
   with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE)
   with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp
 qed
 
 lemma mono_Max_commute:
   assumes "mono f"
   assumes "finite A" and "A \<noteq> {}"
   shows "f (Max A) = Max (f ` A)"
 proof (rule linorder_class.Max_eqI [symmetric])
   from \<open>finite A\<close> show "finite (f ` A)" by simp
   from assms show "f (Max A) \<in> f ` A" by simp
   fix x
   assume "x \<in> f ` A"
   then obtain y where "y \<in> A" and "x = f y" ..
   with assms have "y \<le> Max A" by auto
   with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE)
   with \<open>x = f y\<close> show "x \<le> f (Max A)" by simp
 qed
 
 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
   assumes fin: "finite A"
   and empty: "P {}" 
   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
   shows "P A"
 using fin empty insert
 proof (induct rule: finite_psubset_induct)
   case (psubset A)
   have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
   have fin: "finite A" by fact 
   have empty: "P {}" by fact
   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
   show "P A"
   proof (cases "A = {}")
     assume "A = {}" 
     then show "P A" using \<open>P {}\<close> by simp
   next
     let ?B = "A - {Max A}" 
     let ?A = "insert (Max A) ?B"
     have "finite ?B" using \<open>finite A\<close> by simp
     assume "A \<noteq> {}"
     with \<open>finite A\<close> have "Max A \<in> A" by auto
     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
     then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast
     moreover 
     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF \<open>finite A\<close>] by fastforce
     ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce
   qed
 qed
 
 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
   "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
 
 lemma finite_ranking_induct[consumes 1, case_names empty insert]:
   fixes f :: "'b \<Rightarrow> 'a"
   assumes "finite S"
   assumes "P {}" 
   assumes "\<And>x S. finite S \<Longrightarrow> (\<And>y. y \<in> S \<Longrightarrow> f y \<le> f x) \<Longrightarrow> P S \<Longrightarrow> P (insert x S)"
   shows "P S"
-  using `finite S` 
+  using \<open>finite S\<close> 
 proof (induction rule: finite_psubset_induct)
   case (psubset A)
   {
     assume "A \<noteq> {}"
     hence "f ` A \<noteq> {}" and "finite (f ` A)"
       using psubset finite_image_iff by simp+ 
     then obtain a where "f a = Max (f ` A)" and "a \<in> A"
       by (metis Max_in[of "f ` A"] imageE)
     then have "P (A - {a})"
       using psubset member_remove by blast 
     moreover 
     have "\<And>y. y \<in> A \<Longrightarrow> f y \<le> f a"
       using \<open>f a = Max (f ` A)\<close> \<open>finite (f ` A)\<close> by simp
     ultimately
     have ?case
       by (metis \<open>a \<in> A\<close> DiffD1 insert_Diff assms(3) finite_Diff psubset.hyps)
   }
   thus ?case
     using assms(2) by blast
 qed
 
 lemma Least_Min:
   assumes "finite {a. P a}" and "\<exists>a. P a"
   shows "(LEAST a. P a) = Min {a. P a}"
 proof -
   { fix A :: "'a set"
     assume A: "finite A" "A \<noteq> {}"
     have "(LEAST a. a \<in> A) = Min A"
     using A proof (induct A rule: finite_ne_induct)
       case singleton show ?case by (rule Least_equality) simp_all
     next
       case (insert a A)
       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
       with insert show ?case by simp
     qed
   } from this [of "{a. P a}"] assms show ?thesis by simp
 qed
 
 lemma infinite_growing:
   assumes "X \<noteq> {}"
   assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
   shows "\<not> finite X"
 proof
   assume "finite X"
   with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
     by auto
   with *[of "Max X"] show False
     by auto
 qed
 
 end
 
 context linordered_ab_semigroup_add
 begin
 
 lemma Min_add_commute:
   fixes k
   assumes "finite S" and "S \<noteq> {}"
   shows "Min ((\<lambda>x. f x + k) ` S) = Min(f ` S) + k"
 proof -
   have m: "\<And>x y. min x y + k = min (x+k) (y+k)"
     by(simp add: min_def antisym add_right_mono)
   have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto
   also have "Min \<dots> = Min (f ` S) + k"
     using assms hom_Min_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp
   finally show ?thesis by simp
 qed
 
 lemma Max_add_commute:
   fixes k
   assumes "finite S" and "S \<noteq> {}"
   shows "Max ((\<lambda>x. f x + k) ` S) = Max(f ` S) + k"
 proof -
   have m: "\<And>x y. max x y + k = max (x+k) (y+k)"
     by(simp add: max_def antisym add_right_mono)
   have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto
   also have "Max \<dots> = Max (f ` S) + k"
     using assms hom_Max_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp
   finally show ?thesis by simp
 qed
 
 end
 
 context linordered_ab_group_add
 begin
 
 lemma minus_Max_eq_Min [simp]:
   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
 
 lemma minus_Min_eq_Max [simp]:
   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
 
 end
 
 context complete_linorder
 begin
 
 lemma Min_Inf:
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A = Inf A"
 proof -
   from assms obtain b B where "A = insert b B" and "finite B" by auto
   then show ?thesis
     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
 qed
 
 lemma Max_Sup:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A = Sup A"
 proof -
   from assms obtain b B where "A = insert b B" and "finite B" by auto
   then show ?thesis
     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
 qed
 
 end
 
 
 subsection \<open>Arg Min\<close>
 
 context ord
 begin
 
 definition is_arg_min :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
 "is_arg_min f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y < f x))"
 
 definition arg_min :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b" where
 "arg_min f P = (SOME x. is_arg_min f P x)"
 
 definition arg_min_on :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b" where
 "arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)"
 
 end
 
 syntax
   "_arg_min" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'b"
     ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10)
 translations
   "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"
 
 lemma is_arg_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
 shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))"
 by(auto simp add: is_arg_min_def)
 
 lemma is_arg_min_antimono: fixes f :: "'a \<Rightarrow> ('b::order)"
 shows "\<lbrakk> is_arg_min f P x; f y \<le> f x; P y \<rbrakk> \<Longrightarrow> is_arg_min f P y"
 by (simp add: order.order_iff_strict is_arg_min_def)
 
 lemma arg_minI:
   "\<lbrakk> P x;
     \<And>y. P y \<Longrightarrow> \<not> f y < f x;
     \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
   \<Longrightarrow> Q (arg_min f P)"
 apply (simp add: arg_min_def is_arg_min_def)
 apply (rule someI2_ex)
  apply blast
 apply blast
 done
 
 lemma arg_min_equality:
   "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k"
   for f :: "_ \<Rightarrow> 'a::order"
 apply (rule arg_minI)
   apply assumption
  apply (simp add: less_le_not_le)
 by (metis le_less)
 
 lemma wf_linord_ex_has_least:
   "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk>
    \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
 apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
 apply (drule_tac x = "m ` Collect P" in spec)
 by force
 
 lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
   for m :: "'a \<Rightarrow> nat"
 apply (simp only: pred_nat_trancl_eq_le [symmetric])
 apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
  apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
 by assumption
 
 lemma arg_min_nat_lemma:
   "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)"
   for m :: "'a \<Rightarrow> nat"
 apply (simp add: arg_min_def is_arg_min_linorder)
 apply (rule someI_ex)
 apply (erule ex_has_least_nat)
 done
 
 lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1]
 
 lemma is_arg_min_arg_min_nat: fixes m :: "'a \<Rightarrow> nat"
 shows "P x \<Longrightarrow> is_arg_min m P (arg_min m P)"
 by (metis arg_min_nat_lemma is_arg_min_linorder)
 
 lemma arg_min_nat_le: "P x \<Longrightarrow> m (arg_min m P) \<le> m x"
   for m :: "'a \<Rightarrow> nat"
 by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
 
 lemma ex_min_if_finite:
   "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>m\<in>S. \<not>(\<exists>x\<in>S. x < (m::'a::order))"
 by(induction rule: finite.induct) (auto intro: order.strict_trans)
 
 lemma ex_is_arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
 shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x"
 unfolding is_arg_min_def
 using ex_min_if_finite[of "f ` S"]
 by auto
 
 lemma arg_min_SOME_Min:
   "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
 unfolding arg_min_on_def arg_min_def is_arg_min_linorder
 apply(rule arg_cong[where f = Eps])
 apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
 done
 
 lemma arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
 assumes "finite S" "S \<noteq> {}"
 shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
 using ex_is_arg_min_if_finite[OF assms, of f]
 unfolding arg_min_on_def arg_min_def is_arg_min_def
 by(auto dest!: someI_ex)
 
 lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
 shows "\<lbrakk> finite S;  S \<noteq> {};  y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y"
 by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)
 
 lemma arg_min_inj_eq: fixes f :: "'a \<Rightarrow> 'b :: order"
 shows "\<lbrakk> inj_on f {x. P x}; P a; \<forall>y. P y \<longrightarrow> f a \<le> f y \<rbrakk> \<Longrightarrow> arg_min f P = a"
 apply(simp add: arg_min_def is_arg_min_def)
 apply(rule someI2[of _ a])
  apply (simp add: less_le_not_le)
 by (metis inj_on_eq_iff less_le mem_Collect_eq)
 
 
 subsection \<open>Arg Max\<close>
 
 context ord
 begin
 
 definition is_arg_max :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
 "is_arg_max f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y > f x))"
 
 definition arg_max :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b" where
 "arg_max f P = (SOME x. is_arg_max f P x)"
 
 definition arg_max_on :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b" where
 "arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)"
 
 end
 
 syntax
   "_arg_max" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
     ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10)
 translations
   "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"
 
 lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
 shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))"
 by(auto simp add: is_arg_max_def)
 
 lemma arg_maxI:
   "P x \<Longrightarrow>
     (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow>
     (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow>
     Q (arg_max f P)"
 apply (simp add: arg_max_def is_arg_max_def)
 apply (rule someI2_ex)
  apply blast
 apply blast
 done
 
 lemma arg_max_equality:
   "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k"
   for f :: "_ \<Rightarrow> 'a::order"
 apply (rule arg_maxI [where f = f])
   apply assumption
  apply (simp add: less_le_not_le)
 by (metis le_less)
 
 lemma ex_has_greatest_nat_lemma:
   "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> f y \<le> f x) \<Longrightarrow> \<exists>y. P y \<and> \<not> f y < f k + n"
   for f :: "'a \<Rightarrow> nat"
 by (induct n) (force simp: le_Suc_eq)+
 
 lemma ex_has_greatest_nat:
   "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f x)"
   for f :: "'a \<Rightarrow> nat"
 apply (rule ccontr)
 apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma)
   apply (subgoal_tac [3] "f k \<le> b")
    apply auto
 done
 
 lemma arg_max_nat_lemma:
   "\<lbrakk> P k;  \<forall>y. P y \<longrightarrow> f y < b \<rbrakk>
   \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))"
   for f :: "'a \<Rightarrow> nat"
 apply (simp add: arg_max_def is_arg_max_linorder)
 apply (rule someI_ex)
 apply (erule (1) ex_has_greatest_nat)
 done
 
 lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1]
 
 lemma arg_max_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)"
   for f :: "'a \<Rightarrow> nat"
 by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
 
 end