diff --git a/thys/Berlekamp_Zassenhaus/Finite_Field.thy b/thys/Berlekamp_Zassenhaus/Finite_Field.thy
--- a/thys/Berlekamp_Zassenhaus/Finite_Field.thy
+++ b/thys/Berlekamp_Zassenhaus/Finite_Field.thy
@@ -1,350 +1,350 @@
 (*
     Authors:      Jose Divasón
                   Sebastiaan Joosten
                   René Thiemann
                   Akihisa Yamada
 *)
 section \<open>Finite Rings and Fields\<close>
 
 text \<open>We start by establishing some preliminary results about finite rings and finite fields\<close>
 
 subsection \<open>Finite Rings\<close>
 
 theory Finite_Field
 imports 
   "HOL-Computational_Algebra.Primes"
   "HOL-Number_Theory.Residues"
-  Containers.Set_Impl
+  "HOL-Library.Cardinality"
   Subresultants.Binary_Exponentiation
   Polynomial_Interpolation.Ring_Hom_Poly
 begin
 
 typedef ('a::finite) mod_ring = "{0..<int CARD('a)}" by auto
 
 setup_lifting type_definition_mod_ring
 
 lemma CARD_mod_ring[simp]: "CARD('a mod_ring) = CARD('a::finite)" 
 proof -
   have "card {y. \<exists>x\<in>{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} = card {0..<int CARD('a)}"
   proof (rule bij_betw_same_card)
     have "inj_on Rep_mod_ring {y. \<exists>x\<in>{0..<int CARD('a)}. y = Abs_mod_ring x}"
       by (meson Rep_mod_ring_inject inj_onI)      
     moreover have "Rep_mod_ring ` {y. \<exists>x\<in>{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} = {0..<int CARD('a)}"
     proof (auto simp add: image_def Rep_mod_ring_inject)
       fix xb show "0 \<le> Rep_mod_ring (Abs_mod_ring xb)" 
         using Rep_mod_ring atLeastLessThan_iff by blast 
       assume xb1: "0 \<le> xb" and xb2: "xb < int CARD('a)"
       thus " Rep_mod_ring (Abs_mod_ring xb) < int CARD('a)"
         by (metis Abs_mod_ring_inverse Rep_mod_ring atLeastLessThan_iff le_less_trans linear)
       have xb: "xb \<in> {0..<int CARD('a)}" using xb1 xb2 by simp
       show "\<exists>xa::'a mod_ring. (\<exists>x\<in>{0..<int CARD('a)}. xa = Abs_mod_ring x) \<and> xb = Rep_mod_ring xa"
       by (rule exI[of _ "Abs_mod_ring xb"], auto simp add: xb1 xb2, rule Abs_mod_ring_inverse[OF xb, symmetric])
     qed    
     ultimately show "bij_betw Rep_mod_ring
       {y. \<exists>x\<in>{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} 
       {0..<int CARD('a)}"
       by (simp add: bij_betw_def)
   qed
   thus ?thesis
     unfolding type_definition.univ[OF type_definition_mod_ring]
     unfolding image_def by auto
 qed
 
 instance mod_ring :: (finite) finite 
 proof (intro_classes)
   show "finite (UNIV::'a mod_ring set)" 
     unfolding type_definition.univ[OF type_definition_mod_ring]
     using finite by simp
 qed
 
 
 instantiation mod_ring :: (finite) equal
 begin
 lift_definition equal_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> bool" is "(=)" .
 instance by (intro_classes, transfer, auto)
 end
 
 instantiation mod_ring :: (finite) comm_ring
 begin
 
 lift_definition plus_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> 'a mod_ring" is
   "\<lambda> x y. (x + y) mod int (CARD('a))" by simp
 
 lift_definition uminus_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring" is
   "\<lambda> x. if x = 0 then 0 else int (CARD('a)) - x" by simp
 
 lift_definition minus_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> 'a mod_ring" is
   "\<lambda> x y. (x - y) mod int (CARD('a))" by simp
 
 lift_definition times_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> 'a mod_ring" is
   "\<lambda> x y. (x * y) mod int (CARD('a))" by simp
 
 lift_definition zero_mod_ring :: "'a mod_ring" is 0 by simp
 
 instance
   by standard
     (transfer; auto simp add: mod_simps algebra_simps intro: mod_diff_cong)+
 
 end
 
 lift_definition to_int_mod_ring :: "'a::finite mod_ring \<Rightarrow> int" is "\<lambda> x. x" .
 
 lift_definition of_int_mod_ring :: "int \<Rightarrow> 'a::finite mod_ring" is
   "\<lambda> x. x mod int (CARD('a))" by simp
 
 interpretation to_int_mod_ring_hom: inj_zero_hom to_int_mod_ring
   by (unfold_locales; transfer, auto)
 
 lemma int_nat_card[simp]: "int (nat CARD('a::finite)) = CARD('a)" by auto
 
 interpretation of_int_mod_ring_hom: zero_hom of_int_mod_ring
   by (unfold_locales, transfer, auto)
 
 lemma of_int_mod_ring_to_int_mod_ring[simp]:
   "of_int_mod_ring (to_int_mod_ring x) = x" by (transfer, auto)
 
 lemma to_int_mod_ring_of_int_mod_ring[simp]: "0 \<le> x \<Longrightarrow> x < int CARD('a :: finite) \<Longrightarrow>
   to_int_mod_ring (of_int_mod_ring x :: 'a mod_ring) = x"
   by (transfer, auto)
 
 lemma range_to_int_mod_ring:
   "range (to_int_mod_ring :: ('a :: finite mod_ring \<Rightarrow> int)) = {0 ..< CARD('a)}"
   apply (intro equalityI subsetI)
   apply (elim rangeE, transfer, force)
   by (auto intro!: range_eqI to_int_mod_ring_of_int_mod_ring[symmetric])
 
 subsection \<open>Nontrivial Finite Rings\<close>
 
 class nontriv = assumes nontriv: "CARD('a) > 1"
 
 subclass(in nontriv) finite by(intro_classes,insert nontriv,auto intro:card_ge_0_finite)
 
 instantiation mod_ring :: (nontriv) comm_ring_1
 begin
 
 lift_definition one_mod_ring :: "'a mod_ring" is 1 using nontriv[where ?'a='a] by auto
 
 instance by (intro_classes; transfer, simp)
 
 end
 
 interpretation to_int_mod_ring_hom: inj_one_hom to_int_mod_ring
   by (unfold_locales, transfer, simp)
 
 lemma of_nat_of_int_mod_ring [code_unfold]:
   "of_nat = of_int_mod_ring o int"
 proof (rule ext, unfold o_def)
   show "of_nat n = of_int_mod_ring (int n)" for n
   proof (induct n)
     case (Suc n)
     show ?case
       by (simp only: of_nat_Suc Suc, transfer) (simp add: mod_simps)
   qed simp
 qed
 
 lemma of_nat_card_eq_0[simp]: "(of_nat (CARD('a::nontriv)) :: 'a mod_ring) = 0"
   by (unfold of_nat_of_int_mod_ring, transfer, auto)
 
 lemma of_int_of_int_mod_ring[code_unfold]: "of_int = of_int_mod_ring"
 proof (rule ext)
   fix x :: int
   obtain n1 n2 where x: "x = int n1 - int n2" by (rule int_diff_cases)
   show "of_int x = of_int_mod_ring x"
     unfolding x of_int_diff of_int_of_nat_eq of_nat_of_int_mod_ring o_def
     by (transfer, simp add: mod_diff_right_eq mod_diff_left_eq)
 qed
 
 unbundle lifting_syntax
 
 lemma pcr_mod_ring_to_int_mod_ring: "pcr_mod_ring = (\<lambda>x y. x = to_int_mod_ring y)"
  unfolding mod_ring.pcr_cr_eq unfolding cr_mod_ring_def to_int_mod_ring.rep_eq ..
 
 lemma [transfer_rule]:
   "((=) ===> pcr_mod_ring) (\<lambda> x. int x mod int (CARD('a :: nontriv))) (of_nat :: nat \<Rightarrow> 'a mod_ring)"
   by (intro rel_funI, unfold pcr_mod_ring_to_int_mod_ring of_nat_of_int_mod_ring, transfer, auto)
 
 lemma [transfer_rule]:
   "((=) ===> pcr_mod_ring) (\<lambda> x. x mod int (CARD('a :: nontriv))) (of_int :: int \<Rightarrow> 'a mod_ring)"
   by (intro rel_funI, unfold pcr_mod_ring_to_int_mod_ring of_int_of_int_mod_ring, transfer, auto)
 
 lemma one_mod_card [simp]: "1 mod CARD('a::nontriv) = 1"
   using mod_less nontriv by blast 
 
 lemma Suc_0_mod_card [simp]: "Suc 0 mod CARD('a::nontriv) = 1"
   using one_mod_card by simp
 
 lemma one_mod_card_int [simp]: "1 mod int CARD('a::nontriv) = 1"
 proof -
   from nontriv [where ?'a = 'a] have "int (1 mod CARD('a::nontriv)) = 1"
     by simp
   then show ?thesis
     using of_nat_mod [of 1 "CARD('a)", where ?'a = int] by simp
 qed
 
 lemma pow_mod_ring_transfer[transfer_rule]:
   "(pcr_mod_ring ===> (=) ===> pcr_mod_ring) 
    (\<lambda>a::int. \<lambda>n. a^n mod CARD('a::nontriv)) ((^)::'a mod_ring \<Rightarrow> nat \<Rightarrow> 'a mod_ring)"
 unfolding pcr_mod_ring_to_int_mod_ring
 proof (intro rel_funI,simp)
   fix x::"'a mod_ring" and n
   show "to_int_mod_ring x ^ n mod int CARD('a) = to_int_mod_ring (x ^ n)"
   proof (induct n)
     case 0
     thus ?case by auto
   next
     case (Suc n)
     have "to_int_mod_ring (x ^ Suc n) = to_int_mod_ring (x * x ^ n)" by auto
     also have "... = to_int_mod_ring x * to_int_mod_ring (x ^ n) mod CARD('a)"
       unfolding to_int_mod_ring_def using times_mod_ring.rep_eq by auto
     also have "... = to_int_mod_ring x * (to_int_mod_ring x ^ n mod CARD('a)) mod CARD('a)"
       using Suc.hyps by auto
     also have "... = to_int_mod_ring x ^ Suc n mod int CARD('a)"
       by (simp add: mod_simps)
     finally show ?case ..
   qed
 qed
 
 lemma dvd_mod_ring_transfer[transfer_rule]:
 "((pcr_mod_ring :: int \<Rightarrow> 'a :: nontriv mod_ring \<Rightarrow> bool) ===>
   (pcr_mod_ring :: int \<Rightarrow> 'a mod_ring \<Rightarrow> bool) ===> (=))
   (\<lambda> i j. \<exists>k \<in> {0..<int CARD('a)}. j = i * k mod int CARD('a)) (dvd)"
 proof (unfold pcr_mod_ring_to_int_mod_ring, intro rel_funI iffI)
   fix x y :: "'a mod_ring" and i j
   assume i: "i = to_int_mod_ring x" and j: "j = to_int_mod_ring y"
   { assume "x dvd y"
     then obtain z where "y = x * z" by (elim dvdE, auto)
     then have "j = i * to_int_mod_ring z mod CARD('a)" by (unfold i j, transfer)
     with range_to_int_mod_ring
     show "\<exists>k \<in> {0..<int CARD('a)}. j = i * k mod CARD('a)" by auto
   }
   assume "\<exists>k \<in> {0..<int CARD('a)}. j = i * k mod CARD('a)"
   then obtain k where k: "k \<in> {0..<int CARD('a)}" and dvd: "j = i * k mod CARD('a)" by auto
   from k have "to_int_mod_ring (of_int k :: 'a mod_ring) = k" by (transfer, auto)
   also from dvd have "j = i * ... mod CARD('a)" by auto
   finally have "y = x * (of_int k :: 'a mod_ring)" unfolding i j using k by (transfer, auto)
   then show "x dvd y" by auto
 qed
 
 lemma Rep_mod_ring_mod[simp]: "Rep_mod_ring (a :: 'a :: nontriv mod_ring) mod CARD('a) = Rep_mod_ring a"
   using Rep_mod_ring[where 'a = 'a] by auto
 
 subsection \<open>Finite Fields\<close>
 
 text \<open>When the domain is prime, the ring becomes a field\<close>
 
 class prime_card = assumes prime_card: "prime (CARD('a))"
 begin
 lemma prime_card_int: "prime (int (CARD('a)))" using prime_card by auto
 
 subclass nontriv using prime_card prime_gt_1_nat by (intro_classes,auto)
 end
 
 instantiation mod_ring :: (prime_card) field
 begin
  
 definition inverse_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring" where
   "inverse_mod_ring x = (if x = 0 then 0 else x ^ (nat (CARD('a) - 2)))"
 
 definition divide_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> 'a mod_ring"  where
   "divide_mod_ring x y = x * ((\<lambda>c. if c = 0 then 0 else c ^ (nat (CARD('a) - 2))) y)" 
 
 instance
 proof
   fix a b c::"'a mod_ring"
   show "inverse 0 = (0::'a mod_ring)" by (simp add: inverse_mod_ring_def)
   show "a div b = a * inverse b" 
     unfolding inverse_mod_ring_def by (transfer', simp add: divide_mod_ring_def)
   show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   proof (unfold inverse_mod_ring_def, transfer)
     let ?p="CARD('a)"
     fix x
     assume x: "x \<in> {0..<int CARD('a)}" and x0: "x \<noteq> 0"
     have p0': "0\<le>?p" by auto
     have "\<not> ?p dvd x"
       using x x0 zdvd_imp_le by fastforce
     then have "\<not> CARD('a) dvd nat \<bar>x\<bar>"
       by simp
     with x have "\<not> CARD('a) dvd nat x"
       by simp
     have rw: "x ^ nat (int (?p - 2)) * x = x ^ nat (?p - 1)"
     proof -
       have p2: "0 \<le> int (?p-2)" using x by simp
       have card_rw: "(CARD('a) - Suc 0) = nat (1 + int (CARD('a) - 2))" 
         using nat_eq_iff x x0 by auto
       have "x ^ nat (?p - 2)*x = x ^ (Suc (nat (?p - 2)))" by simp
       also have "... = x ^ (nat (?p - 1))"
         using Suc_nat_eq_nat_zadd1[OF p2] card_rw by auto
       finally show ?thesis .
     qed
     have "[int (nat x ^ (CARD('a) - 1)) = int 1] (mod CARD('a))"
       using fermat_theorem [OF prime_card \<open>\<not> CARD('a) dvd nat x\<close>]
       by (simp only: cong_def cong_def of_nat_mod [symmetric])
     then have *: "[x ^ (CARD('a) - 1) = 1] (mod CARD('a))"
       using x by auto
     have "x ^ (CARD('a) - 2) mod CARD('a) * x mod CARD('a) 
       = (x ^ nat (CARD('a) - 2) * x) mod CARD('a)" by (simp add: mod_simps)
     also have "... =  (x ^ nat (?p - 1) mod ?p)" unfolding rw by simp
     also have "... = (x ^ (nat ?p - 1) mod ?p)" using p0' by (simp add: nat_diff_distrib')
     also have "... = 1"
       using * by (simp add: cong_def)
     finally show "(if x = 0 then 0 else x ^ nat (int (CARD('a) - 2)) mod CARD('a)) * x mod CARD('a) = 1"
       using x0 by auto
   qed
 qed
 end
 
 instantiation mod_ring :: (prime_card) "{normalization_euclidean_semiring, euclidean_ring}"
 begin
 
 definition modulo_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> 'a mod_ring" where "modulo_mod_ring x y = (if y = 0 then x else 0)"
 definition normalize_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring" where "normalize_mod_ring x = (if x = 0 then 0 else 1)" 
 definition unit_factor_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring" where "unit_factor_mod_ring x = x" 
 definition euclidean_size_mod_ring :: "'a mod_ring \<Rightarrow> nat" where "euclidean_size_mod_ring x = (if x = 0 then 0 else 1)" 
 
 instance
 proof (intro_classes)
   fix a :: "'a mod_ring" show "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
     unfolding dvd_def unit_factor_mod_ring_def by (intro exI[of _ "inverse a"], auto)
 qed (auto simp: normalize_mod_ring_def unit_factor_mod_ring_def modulo_mod_ring_def
      euclidean_size_mod_ring_def field_simps)
 end
 
 instantiation mod_ring :: (prime_card) euclidean_ring_gcd
 begin
 
 definition gcd_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> 'a mod_ring" where "gcd_mod_ring = Euclidean_Algorithm.gcd"
 definition lcm_mod_ring :: "'a mod_ring \<Rightarrow> 'a mod_ring \<Rightarrow> 'a mod_ring" where "lcm_mod_ring = Euclidean_Algorithm.lcm"
 definition Gcd_mod_ring :: "'a mod_ring set \<Rightarrow> 'a mod_ring" where "Gcd_mod_ring = Euclidean_Algorithm.Gcd"
 definition Lcm_mod_ring :: "'a mod_ring set \<Rightarrow> 'a mod_ring" where "Lcm_mod_ring = Euclidean_Algorithm.Lcm"
 
 instance by (intro_classes, auto simp: gcd_mod_ring_def lcm_mod_ring_def Gcd_mod_ring_def Lcm_mod_ring_def)
 end
 
 instantiation mod_ring :: (prime_card) unique_euclidean_ring
 begin
 
 definition [simp]: "division_segment_mod_ring (x :: 'a mod_ring) = (1 :: 'a mod_ring)"
 
 instance by intro_classes (auto simp: euclidean_size_mod_ring_def split: if_splits)
 
 end
 
 instance mod_ring :: (prime_card) field_gcd
   by intro_classes auto
 
 
 lemma surj_of_nat_mod_ring: "\<exists> i. i < CARD('a :: prime_card) \<and> (x :: 'a mod_ring) = of_nat i" 
   by (rule exI[of _ "nat (to_int_mod_ring x)"], unfold of_nat_of_int_mod_ring o_def,
   subst nat_0_le, transfer, simp, simp, transfer, auto) 
 
 lemma of_nat_0_mod_ring_dvd: assumes x: "of_nat x = (0 :: 'a ::prime_card mod_ring)"
   shows "CARD('a) dvd x" 
 proof -
   let ?x = "of_nat x :: int" 
   from x have "of_int_mod_ring ?x = (0 :: 'a mod_ring)" by (fold of_int_of_int_mod_ring, simp)
   hence "?x mod CARD('a) = 0" by (transfer, auto)
   hence "x mod CARD('a) = 0" by presburger
   thus ?thesis unfolding mod_eq_0_iff_dvd .
 qed
 
 end