Theory Finite_Field_Factorization_Record_Based

    Authors:      Jose Divasón
                  Sebastiaan Joosten
                  René Thiemann
                  Akihisa Yamada
subsection ‹Record Based Version›
theory Finite_Field_Factorization_Record_Based

hide_const(open) monom coeff

text ‹Whereas @{thm finite_field_factorization} provides a result for a polynomials over GF(p),
  we now develop a theorem which speaks about integer polynomials modulo p.›
lemma (in poly_mod_prime_type) finite_field_factorization_modulo_ring:
  assumes g: "(g :: 'a mod_ring poly) = of_int_poly f"
  and sf: "square_free_m f"
  and fact: "finite_field_factorization g = (d,gs)"
  and c: "c = to_int_mod_ring d"
  and fs: "fs = map to_int_poly gs"
  shows "unique_factorization_m f (c, mset fs)"
proof -
  have [transfer_rule]: "MP_Rel f g" unfolding g MP_Rel_def by (simp add: Mp_f_representative)
  have sg: "square_free g" by (transfer, rule sf)
  have [transfer_rule]: "M_Rel c d" unfolding M_Rel_def c by (rule M_to_int_mod_ring)
  have fs_gs[transfer_rule]: "list_all2 MP_Rel fs gs"
    unfolding fs list_all2_map1 MP_Rel_def[abs_def] Mp_to_int_poly by (simp add: list.rel_refl)
  have [transfer_rule]: "rel_mset MP_Rel (mset fs) (mset gs)"
    using fs_gs using rel_mset_def by blast
  have [transfer_rule]: "MF_Rel (c,mset fs) (d,mset gs)" unfolding MF_Rel_def by transfer_prover
  from finite_field_factorization[OF sg fact]
  have uf: "unique_factorization Irr_Mon g (d,mset gs)" by auto
  from uf[untransferred] show "unique_factorization_m f (c, mset fs)" .

text ‹We now have to implement @{const finite_field_factorization}.›  
  fixes p :: int
  and ff_ops :: "'i arith_ops_record"  (* finite-fields *)

fun power_poly_f_mod_i :: "('i list  'i list)  'i list  nat  'i list" where
  "power_poly_f_mod_i modulus a n = (if n = 0 then modulus (one_poly_i ff_ops)
    else let (d,r) = Euclidean_Rings.divmod_nat n 2; 
       rec = power_poly_f_mod_i modulus (modulus (times_poly_i ff_ops a a)) d in 
    if r = 0 then rec else modulus (times_poly_i ff_ops rec a))"

declare power_poly_f_mod_i.simps[simp del]

fun power_polys_i :: "'i list  'i list  'i list  nat  'i list list" where
  "power_polys_i mul_p u curr_p (Suc i) = curr_p # 
      power_polys_i mul_p u (mod_field_poly_i ff_ops (times_poly_i ff_ops curr_p mul_p) u) i"
| "power_polys_i mul_p u curr_p 0 = []"

lemma length_power_polys_i[simp]: "length (power_polys_i x y z n) = n" 
  by (induct n arbitrary: x y z, auto)

definition berlekamp_mat_i :: "'i list  'i mat" where
  "berlekamp_mat_i u = (let n = degree_i u; 
    ze = ff_ops; on = ff_ops;
    mul_p = power_poly_f_mod_i (λ v. mod_field_poly_i ff_ops v u) 
      [ze, on] (nat p);
    xks = power_polys_i mul_p u [on] n
   in mat_of_rows_list n (map (λ cs. cs @ replicate (n - length cs) ze) xks))"

definition berlekamp_resulting_mat_i :: "'i list  'i mat" where
"berlekamp_resulting_mat_i u = (let Q = berlekamp_mat_i u;
    n = dim_row Q;
    QI = mat n n (λ (i,j). if i = j then arith_ops_record.minus ff_ops (Q $$ (i,j)) ( ff_ops) else Q $$ (i,j))
    in (gauss_jordan_single_i ff_ops (transpose_mat QI)))"

definition berlekamp_basis_i :: "'i list  'i list list" where
  "berlekamp_basis_i u = (map (poly_of_list_i ff_ops o list_of_vec) 
    (find_base_vectors_i ff_ops (berlekamp_resulting_mat_i u)))"

primrec berlekamp_factorization_main_i :: "'i  'i  nat  'i list list  'i list list  nat  'i list list" where
  "berlekamp_factorization_main_i ze on d divs (v # vs) n = (
    if v = [on] then berlekamp_factorization_main_i ze on d divs vs n else
    if length divs = n then divs else
    let of_int = arith_ops_record.of_int ff_ops;
        facts = filter (λ w. w  [on]) 
          [ gcd_poly_i ff_ops u (minus_poly_i ff_ops v (if s = 0 then [] else [of_int (int s)])) . 
            u  divs, s  [0 ..< nat p]];
      (lin,nonlin) = List.partition (λ q. degree_i q = d) facts 
      in lin @ berlekamp_factorization_main_i ze on d nonlin vs (n - length lin))"
| "berlekamp_factorization_main_i ze on d divs [] n = divs"

definition berlekamp_monic_factorization_i :: "nat  'i list  'i list list" where
  "berlekamp_monic_factorization_i d f = (let
     vs = berlekamp_basis_i f
    in berlekamp_factorization_main_i ( ff_ops) ( ff_ops) d [f] vs (length vs))"         

partial_function (tailrec) dist_degree_factorize_main_i :: 
  "'i  'i  nat  'i list  'i list  nat  (nat × 'i list) list 
   (nat × 'i list) list" where
  [code]: "dist_degree_factorize_main_i ze on dv v w d res = (if v = [on] then res else if d + d > dv 
    then (dv, v) # res else let
      w = power_poly_f_mod_i (λ f. mod_field_poly_i ff_ops f v) w (nat p);
      d = Suc d;
      gd = gcd_poly_i ff_ops (minus_poly_i ff_ops w [ze,on]) v
      in if gd = [on] then dist_degree_factorize_main_i ze on dv v w d res else 
      let v' = div_field_poly_i ff_ops v gd
      in dist_degree_factorize_main_i ze on (degree_i v') v' (mod_field_poly_i ff_ops w v') d ((d,gd) # res))" 

definition distinct_degree_factorization_i
  :: "'i list  (nat × 'i list) list" where
  "distinct_degree_factorization_i f = (let ze = ff_ops;
     on = ff_ops in if degree_i f = 1 then [(1,f)] else 
     dist_degree_factorize_main_i ze on (degree_i f) f [ze,on] 0 [])"

definition finite_field_factorization_i :: "'i list  'i × 'i list list" where
  "finite_field_factorization_i f = (if degree_i f = 0 then (lead_coeff_i ff_ops f,[]) else let
     a = lead_coeff_i ff_ops f;
     u = smult_i ff_ops (arith_ops_record.inverse ff_ops a) f;
     gs = (if use_distinct_degree_factorization then distinct_degree_factorization_i u else [(1,u)]);
     (irr,hs) = List.partition (λ (i,f). degree_i f = i) gs
     in (a,map snd irr @ concat (map (λ (i,g). berlekamp_monic_factorization_i i g) hs)))"

context prime_field_gen

lemma power_polys_i: assumes i: "i < n" and [transfer_rule]: "poly_rel f f'" "poly_rel g g'" 
  and h: "poly_rel h h'"
  shows "poly_rel (power_polys_i ff_ops g f h n ! i) (power_polys g' f' h' n ! i)"
  using i h
proof (induct n arbitrary: h h' i)
  case (Suc n h h' i) note * = this
  note [transfer_rule] = *(3)
  show ?case 
  proof (cases i)
    case 0
    with Suc show ?thesis by auto
    case (Suc j)
    with *(2-) have "j < n" by auto
    note IH = *(1)[OF this]
    show ?thesis unfolding Suc by (simp, rule IH, transfer_prover)
qed simp

lemma power_poly_f_mod_i: assumes m: "(poly_rel ===> poly_rel) m (λ x'. x' mod m')"
  shows "poly_rel f f'  poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)"
proof -
  from m have m: " x x'. poly_rel x x'  poly_rel (m x) (x' mod m')" 
    unfolding rel_fun_def by auto
  show "poly_rel f f'  poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)"
  proof (induct n arbitrary: f f' rule: less_induct)
    case (less n f f')
    note f[transfer_rule] = less(2)
    show ?case
    proof (cases "n = 0")
      case True
      show ?thesis 
        by (simp add: True power_poly_f_mod_i.simps power_poly_f_mod_binary, 
          rule m[OF poly_rel_one])
      case False
      hence n: "(n = 0) = False" by simp
      obtain q r where div: "Euclidean_Rings.divmod_nat n 2 = (q,r)" by force
      from this[unfolded Euclidean_Rings.divmod_nat_def] n have "q < n" by auto
      note IH = less(1)[OF this]
      have rec: "poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) 
        (power_poly_f_mod m' (f' * f' mod m') q)" 
        by (rule IH, rule m, transfer_prover)
      have other: "poly_rel 
        (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f))
        (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')" 
        by (rule m, rule poly_rel_times[unfolded rel_fun_def, rule_format, OF rec f])
      show ?thesis unfolding power_poly_f_mod_i.simps[of _ _ _ n] Let_def 
        power_poly_f_mod_binary[of _ _ n] div split n if_False using rec other by auto
lemma berlekamp_mat_i[transfer_rule]: "(poly_rel ===> mat_rel R) 
  (berlekamp_mat_i p ff_ops) berlekamp_mat"
proof (intro rel_funI)
  fix f f' 
  let ?ze = " ff_ops" 
  let ?on = " ff_ops"
  assume f[transfer_rule]: "poly_rel f f'"
  have deg: "degree_i f = degree f'" by transfer_prover
    fix i j
    assume i: "i < degree f'" and j: "j < degree f'" 
    define cs where "cs = (λcs :: 'i list. cs @ replicate (degree f' - length cs) ?ze)"
    define cs' where "cs' = (λcs :: 'a mod_ring poly. coeffs cs @ replicate (degree f' - length (coeffs cs)) 0)"
    define poly where "poly = power_polys_i ff_ops
         (power_poly_f_mod_i ff_ops (λv. mod_field_poly_i ff_ops v f) [?ze, ?on] (nat p)) f [?on]
         (degree f')"
    define poly' where "poly' = (power_polys (power_poly_f_mod f' [:0, 1:] (nat p)) f' 1 (degree f'))"
    have *: "poly_rel (power_poly_f_mod_i ff_ops (λv. mod_field_poly_i ff_ops v f) [?ze, ?on] (nat p))
      (power_poly_f_mod f' [:0, 1:] (nat p))" 
      by (rule power_poly_f_mod_i, transfer_prover, simp add: poly_rel_def one zero)
    have [transfer_rule]: "poly_rel (poly ! i) (poly' ! i)" 
      unfolding poly_def poly'_def 
      by (rule power_polys_i[OF i f *], simp add: poly_rel_def one)
    have *: "list_all2 R (cs (poly ! i)) (cs' (poly' ! i))"
      unfolding cs_def cs'_def by transfer_prover
    from list_all2_nthD[OF *[unfolded poly_rel_def], of j] j
    have "R (cs (poly ! i) ! j) (cs' (poly' ! i) ! j)" unfolding cs_def by auto
    hence "R
            (mat_of_rows_list (degree f')
              (map (λcs. cs @ replicate (degree f' - length cs) ?ze)
                (power_polys_i ff_ops
                  (power_poly_f_mod_i ff_ops (λv. mod_field_poly_i ff_ops v f) [?ze, ?on] (nat p)) f [?on]
                  (degree f'))) $$
             (i, j))
            (mat_of_rows_list (degree f')
              (map (λcs. coeffs cs @ replicate (degree f' - length (coeffs cs)) 0)
                (power_polys (power_poly_f_mod f' [:0, 1:] (nat p)) f' 1 (degree f'))) $$
             (i, j))"           
        unfolding mat_of_rows_list_def length_map length_power_polys_i power_polys_works
          length_power_polys index_mat[OF i j] split
        unfolding poly_def cs_def poly'_def cs'_def using i
        by auto
  } note main = this
  show "mat_rel R (berlekamp_mat_i p ff_ops f) (berlekamp_mat f')"
    unfolding berlekamp_mat_i_def berlekamp_mat_def Let_def nat_p[symmetric] deg
    unfolding mat_rel_def
    by (intro conjI allI impI, insert main, auto)

lemma berlekamp_resulting_mat_i[transfer_rule]: "(poly_rel ===> mat_rel R) 
  (berlekamp_resulting_mat_i p ff_ops) berlekamp_resulting_mat"
proof (intro rel_funI)
  fix f f'
  assume "poly_rel f f'"
  from berlekamp_mat_i[unfolded rel_fun_def, rule_format, OF this]
  have bmi: "mat_rel R (berlekamp_mat_i p ff_ops f) (berlekamp_mat f')" .
  show "mat_rel R (berlekamp_resulting_mat_i p ff_ops f) (berlekamp_resulting_mat f')"
    unfolding berlekamp_resulting_mat_def Let_def berlekamp_resulting_mat_i_def
    by (rule gauss_jordan_i[unfolded rel_fun_def, rule_format],
    insert bmi, auto simp: mat_rel_def one intro!: minus[unfolded rel_fun_def, rule_format])

lemma berlekamp_basis_i[transfer_rule]: "(poly_rel ===> list_all2 poly_rel) 
  (berlekamp_basis_i p ff_ops) berlekamp_basis"
  unfolding berlekamp_basis_i_def[abs_def] berlekamp_basis_code[abs_def] o_def
  by transfer_prover

lemma berlekamp_factorization_main_i[transfer_rule]: 
  "((=) ===> list_all2 poly_rel ===> list_all2 poly_rel ===> (=) ===> list_all2 poly_rel) 
     (berlekamp_factorization_main_i p ff_ops ( ff_ops) 
       ( ff_ops)) 
proof (intro rel_funI, clarify, goal_cases)
  case (1 _ d xs xs' ys ys' _ n)
  let ?ze = " ff_ops" 
  let ?on = " ff_ops"
  let ?of_int = "arith_ops_record.of_int ff_ops"
  from 1(2) 1(1) show ?case
  proof (induct ys ys' arbitrary: xs xs' n rule: list_all2_induct)   
    case (Cons y ys y' ys' xs xs' n)
    note trans[transfer_rule] = Cons(1,2,4)
    obtain clar0 clar1 clar2 where clarify: " s u. gcd_poly_i ff_ops u
                         (minus_poly_i ff_ops y
                        (if s = 0 then [] else [?of_int (int s)])) = clar0 s u" 
        "[0..<nat p] = clar1"
        "[?on] = clar2" by auto
    define facts where "facts = concat (map (λu. concat
                        (map (λs. if gcd_poly_i ff_ops u
                                      (minus_poly_i ff_ops y (if s = 0 then [] else [?of_int (int s)])) 
                                  then [gcd_poly_i ff_ops u
                                         (minus_poly_i ff_ops y (if s = 0 then [] else [?of_int (int s)]))]
                                  else [])
                          [0..<nat p])) xs)"
    define Facts where "Facts = [wconcat
                          (map (λu. map (λs. gcd_poly_i ff_ops u
                                              (minus_poly_i ff_ops y
                                                (if s = 0 then [] else [?of_int (int s)])))
                                     [0..<nat p])
                            xs) .  w  [?on]]"
    have Facts: "Facts = facts"
      unfolding Facts_def facts_def clarify
    proof (induct xs)
      case (Cons x xs)
      show ?case by (simp add: Cons, induct clar1, auto)
    qed simp
    define facts' where "facts' = concat
             (map (λu. concat
                        (map (λx. if gcd u (y' - [:of_nat x:])  1
                                  then [gcd u (y' - [:of_int (int x):])] else [])
                          [0..<nat p]))
    have id: " x. of_int (int x) = of_nat x" "[?on] = one_poly_i ff_ops" 
      by (auto simp: one_poly_i_def) 
    have facts[transfer_rule]: "list_all2 poly_rel facts facts'"
      unfolding facts_def facts'_def
    apply (rule concat_transfer[unfolded rel_fun_def, rule_format])
    apply (rule list.map_transfer[unfolded rel_fun_def, rule_format, OF _ trans(3)])
    apply (rule concat_transfer[unfolded rel_fun_def, rule_format])
    apply (rule list_all2_map_map)
    proof (unfold id)
      fix f f' x
      assume [transfer_rule]: "poly_rel f f'" and x: "x  set [0..<nat p]"
      hence *: "0  int x" "int x < p" by auto
      from of_int[OF this] have rel[transfer_rule]: "R (?of_int (int x)) (of_nat x)" by auto
        assume "0 < x" 
        with * have *: "0 < int x" "int x < p" by auto
        have "(of_nat x :: 'a mod_ring) = of_int (int x)" by simp
        also have "  0" unfolding of_int_of_int_mod_ring using * unfolding p
          by (transfer', auto)
      with rel have [transfer_rule]: "poly_rel (if x = 0 then [] else [?of_int (int x)]) [:of_nat x:]"
        unfolding poly_rel_def by (auto simp add: cCons_def p)
      show "list_all2 poly_rel
          (if gcd_poly_i ff_ops f (minus_poly_i ff_ops y (if x = 0 then [] else [?of_int (int x)]))  one_poly_i ff_ops
           then [gcd_poly_i ff_ops f (minus_poly_i ff_ops y (if x = 0 then [] else [?of_int (int x)]))]
           else [])
          (if gcd f' (y' - [:of_nat x:])  1 then [gcd f' (y' - [:of_nat x:])] else [])"
        by transfer_prover
    have id1: "berlekamp_factorization_main_i p ff_ops ?ze ?on d xs (y # ys) n = (
      if y = [?on] then berlekamp_factorization_main_i p ff_ops ?ze ?on d xs ys n else
      if length xs = n then xs else
      (let fac = facts;
          (lin, nonlin) = List.partition (λq. degree_i q = d) fac
             in lin @ berlekamp_factorization_main_i p ff_ops ?ze ?on d nonlin ys (n - length lin)))" 
      unfolding berlekamp_factorization_main_i.simps Facts[symmetric]
      by (simp add: o_def Facts_def Let_def)
    have id2: "berlekamp_factorization_main d xs' (y' # ys') n = (
      if y' = 1 then berlekamp_factorization_main d xs' ys' n
      else if length xs' = n then xs' else
      (let fac = facts';
          (lin, nonlin) = List.partition (λq. degree q = d) fac
              in lin @ berlekamp_factorization_main d nonlin ys' (n - length lin)))"
      by (simp add: o_def facts'_def nat_p)
    have len: "length xs = length xs'" by transfer_prover
    have id3: "(y = [?on]) = (y' = 1)" 
      by (transfer_prover_start, transfer_step+, simp add: one_poly_i_def finite_field_ops_int_def)
    show ?case
    proof (cases "y' = 1")
      case True
      hence id4: "(y' = 1) = True" by simp
      show ?thesis unfolding id1 id2 id3 id4 if_True
        by (rule Cons(3), transfer_prover)
      case False
      hence id4: "(y' = 1) = False" by simp
      note id1 = id1[unfolded id3 id4 if_False]
      note id2 = id2[unfolded id4 if_False]
      show ?thesis
      proof (cases "length xs' = n")
        case True
        thus ?thesis unfolding id1 id2 Let_def len using trans by simp
        case False
        hence id: "(length xs' = n) = False" by simp
        have id': "length [qfacts . degree_i q = d] = length [qfacts'. degree q = d]" 
          by transfer_prover   
        have [transfer_rule]: "list_all2 poly_rel (berlekamp_factorization_main_i p ff_ops ?ze ?on d [xfacts . degree_i x  d] ys
         (n - length [qfacts . degree_i q = d])) 
         (berlekamp_factorization_main d [xfacts' . degree x  d] ys'
         (n - length [qfacts' . degree q = d]))"
          unfolding id'
          by (rule Cons(3), transfer_prover)
        show ?thesis unfolding id1 id2 Let_def len id if_False
          unfolding partition_filter_conv o_def split by transfer_prover
  qed simp
lemma berlekamp_monic_factorization_i[transfer_rule]: 
  "((=) ===> poly_rel ===> list_all2 poly_rel) 
     (berlekamp_monic_factorization_i p ff_ops) berlekamp_monic_factorization" 
  unfolding berlekamp_monic_factorization_i_def[abs_def] berlekamp_monic_factorization_def[abs_def] Let_def
  by transfer_prover

lemma dist_degree_factorize_main_i: 
  "poly_rel F f  poly_rel G g  list_all2 (rel_prod (=) poly_rel) Res res 
    list_all2 (rel_prod (=) poly_rel) 
      (dist_degree_factorize_main_i p ff_ops 
         ( ff_ops) ( ff_ops) (degree_i F) F G d Res)
      (dist_degree_factorize_main f g d res)" 
proof (induct f g d res arbitrary: F G Res rule: dist_degree_factorize_main.induct)
  case (1 v w d res V W Res)
  let ?ze = " ff_ops" 
  let ?on = " ff_ops"
  note simp = dist_degree_factorize_main.simps[of v w d] 
    dist_degree_factorize_main_i.simps[of p ff_ops ?ze ?on "degree_i V" V W d]
  have v[transfer_rule]: "poly_rel V v" by (rule 1)
  have w[transfer_rule]: "poly_rel W w" by (rule 1)
  have res[transfer_rule]: "list_all2 (rel_prod (=) poly_rel) Res res" by (rule 1)
  have [transfer_rule]: "poly_rel [?on] 1"
    by (simp add: one poly_rel_def)
  have id1: "(V = [?on]) = (v = 1)" unfolding finite_field_ops_int_def by transfer_prover
  have id2: "degree_i V = degree v" by transfer_prover
  note simp = simp[unfolded id1 id2]
  note IH = 1(1,2)
  show ?case 
  proof (cases "v = 1")
    case True
    with res show ?thesis unfolding id2 simp by simp
    case False
    with id1 have "(v = 1) = False" by auto
    note simp = simp[unfolded this if_False]
    note IH = IH[OF False]
    show ?thesis
    proof (cases "degree v < d + d")
      case True
      thus ?thesis unfolding id2 simp using res v by auto
      case False
      hence "(degree v < d + d) = False" by auto
      note simp = simp[unfolded this if_False]
      let ?P = "power_poly_f_mod_i ff_ops (λf. mod_field_poly_i ff_ops f V) W (nat p)" 
      let ?G = "gcd_poly_i ff_ops (minus_poly_i ff_ops ?P [?ze, ?on]) V" 
      let ?g = "gcd (w ^ CARD('a) mod v - monom 1 1) v" 
      define G where "G = ?G" 
      define g where "g = ?g"
      note simp = simp[unfolded Let_def, folded G_def g_def]
      note IH = IH[OF False refl refl refl]
      have [transfer_rule]: "poly_rel [?ze,?on] (monom 1 1)" unfolding poly_rel_def
        by (auto simp: coeffs_monom one zero)
      have id: "w ^ CARD('a) mod v = power_poly_f_mod v w (nat p)"
        unfolding power_poly_f_mod_def by (simp add: p)
      have P[transfer_rule]: "poly_rel ?P (w ^ CARD('a) mod v)" unfolding id
        by (rule power_poly_f_mod_i[OF _ w], transfer_prover)
      have g[transfer_rule]: "poly_rel G g" unfolding G_def g_def by transfer_prover
      have id3: "(G = [?on]) = (g = 1)" by transfer_prover
      note simp = simp[unfolded id3]
      show ?thesis
      proof (cases "g = 1")
        case True
        from IH(1)[OF this[unfolded g_def] v P res] True
        show ?thesis unfolding id2 simp by simp
        case False
        have vg: "poly_rel (div_field_poly_i ff_ops V G) (v div g)" by transfer_prover
        have "poly_rel (mod_field_poly_i ff_ops ?P
          (div_field_poly_i ff_ops V G)) (w ^ CARD('a) mod v mod (v div g))" by transfer_prover        
        note IH = IH(2)[OF False[unfolded g_def] refl vg[unfolded G_def g_def] this[unfolded G_def g_def],
            folded g_def G_def]
        have "list_all2 (rel_prod (=) poly_rel) ((Suc d, G) # Res) ((Suc d, g) # res)" 
          using g res by auto
        note IH = IH[OF this]
        from False have "(g = 1) = False" by simp
        note simp = simp[unfolded this if_False]
        show ?thesis unfolding id2 simp using IH by simp
lemma distinct_degree_factorization_i[transfer_rule]: "(poly_rel ===> list_all2 (rel_prod (=) poly_rel)) 
  (distinct_degree_factorization_i p ff_ops) distinct_degree_factorization"
  fix F f
  assume f[transfer_rule]: "poly_rel F f" 
  have id: "(degree_i F = 1) = (degree f = 1)" by transfer_prover
  note d = distinct_degree_factorization_i_def distinct_degree_factorization_def
  let ?ze = " ff_ops" 
  let ?on = " ff_ops"
  show "list_all2 (rel_prod (=) poly_rel) (distinct_degree_factorization_i p ff_ops F)
            (distinct_degree_factorization f)" 
  proof (cases "degree f = 1")
    case True
    with id f show ?thesis unfolding d by auto
    case False
    from False id have "?thesis = (list_all2 (rel_prod (=) poly_rel) 
      (dist_degree_factorize_main_i p ff_ops ?ze ?on (degree_i F) F [?ze, ?on] 0 [])
      (dist_degree_factorize_main f (monom 1 1) 0 []))" unfolding d Let_def by simp    
    also have 
      by (rule dist_degree_factorize_main_i[OF f], auto simp: poly_rel_def
        coeffs_monom one zero)
    finally show ?thesis .

lemma finite_field_factorization_i[transfer_rule]: 
  "(poly_rel ===> rel_prod R (list_all2 poly_rel))
     (finite_field_factorization_i p ff_ops) finite_field_factorization" 
  unfolding finite_field_factorization_i_def finite_field_factorization_def Let_def lead_coeff_i_def'
  by transfer_prover

text ‹Since the implementation is sound, we can now combine it with the soundness result
  of the finite field factorization.›

lemma finite_field_i_sound: 
  assumes f': "f' = of_int_poly_i ff_ops (Mp f)" 
  and berl_i: "finite_field_factorization_i p ff_ops f' = (c',fs')"
  and sq: "square_free_m f" 
  and fs: "fs = map (to_int_poly_i ff_ops) fs'"
  and c: "c = arith_ops_record.to_int ff_ops c'" 
  shows "unique_factorization_m f (c, mset fs)
     c  {0 ..< p} 
     ( fi  set fs. set (coeffs fi)  {0 ..< p})" 
proof -
  define f'' :: "'a mod_ring poly" where "f'' = of_int_poly (Mp f)"
  have rel_f[transfer_rule]: "poly_rel f' f''" 
    by (rule poly_rel_of_int_poly[OF f'], simp add: f''_def)
  interpret pff: idom_ops "poly_ops ff_ops" poly_rel 
    by (rule idom_ops_poly)
  obtain c'' fs'' where berl: "finite_field_factorization f'' = (c'',fs'')" by force
  from rel_funD[OF finite_field_factorization_i rel_f, unfolded rel_prod_conv assms(2) split berl]
  have rel[transfer_rule]: "R c' c''" "list_all2 poly_rel fs' fs''" by auto  
  from to_int[OF rel(1)] have cc': "c = to_int_mod_ring c''" unfolding c by simp
  have c: "c  {0 ..< p}" unfolding cc'
    by (metis Divides.pos_mod_bound Divides.pos_mod_sign M_to_int_mod_ring atLeastLessThan_iff 
      gr_implies_not_zero nat_le_0 nat_p not_le poly_mod.M_def zero_less_card_finite)
    fix f
    assume "f  set fs'" 
    with rel(2) obtain f' where "poly_rel f f'"  unfolding list_all2_conv_all_nth set_conv_nth
      by auto
    hence "is_poly ff_ops f" using fun_cong[OF Domainp_is_poly, of f]
      unfolding Domainp_iff[abs_def] by auto
  hence fs': "Ball (set fs') (is_poly ff_ops)" by auto
  define mon :: "'a mod_ring poly  bool" where "mon = monic"
  have [transfer_rule]: "(poly_rel ===> (=)) (monic_i ff_ops) mon" unfolding mon_def 
    by (rule poly_rel_monic)
  have len: "length fs' = length fs''" by transfer_prover
  have fs': "fs = map to_int_poly fs''" unfolding fs 
  proof (rule nth_map_conv[OF len], intro allI impI)
    fix i
    assume i: "i < length fs'" 
    obtain f g where id: "fs' ! i = f" "fs'' ! i = g" by auto
    from i rel(2)[unfolded list_all2_conv_all_nth[of _ fs' fs'']] id
    have "poly_rel f g" by auto
    from to_int_poly_i[OF this] have "to_int_poly_i ff_ops f = to_int_poly g" .
    thus "to_int_poly_i ff_ops (fs' ! i) = to_int_poly (fs'' ! i)" unfolding id .
  have f: "f'' = of_int_poly f" unfolding poly_eq_iff f''_def
    by (simp add: to_int_mod_ring_hom.injectivity to_int_mod_ring_of_int_M Mp_coeff)
  have *: "unique_factorization_m f (c, mset fs)" 
    using finite_field_factorization_modulo_ring[OF f sq berl cc' fs'] by auto
  have fs': "(fiset fs. set (coeffs fi)  {0..<p})" unfolding fs' 
    using range_to_int_mod_ring[where 'a = 'a]
    by (auto simp: coeffs_to_int_poly p)
  with c fs *
  show ?thesis by blast

definition finite_field_factorization_main :: "int  'i arith_ops_record  int poly  int × int poly list" where
  "finite_field_factorization_main p f_ops f  
    let (c',fs') = finite_field_factorization_i p f_ops (of_int_poly_i f_ops (poly_mod.Mp p f))
      in (arith_ops_record.to_int f_ops c', map (to_int_poly_i f_ops) fs')"

lemma(in prime_field_gen) finite_field_factorization_main: 
  assumes res: "finite_field_factorization_main p ff_ops f = (c,fs)"
  and sq: "square_free_m f" 
  shows "unique_factorization_m f (c, mset fs)
     c  {0 ..< p} 
     ( fi  set fs. set (coeffs fi)  {0 ..< p})"
proof -
  obtain c' fs' where 
    res': "finite_field_factorization_i p ff_ops (of_int_poly_i ff_ops (Mp f)) = (c', fs')"  by force
  show ?thesis  
    by (rule finite_field_i_sound[OF refl res' sq], 
      insert res[unfolded finite_field_factorization_main_def res'], auto)

definition finite_field_factorization_int :: "int  int poly  int × int poly list" where
  "finite_field_factorization_int p = (  
    if p  65535 
    then finite_field_factorization_main p (finite_field_ops32 (uint32_of_int p))
    else if p  4294967295
    then finite_field_factorization_main p (finite_field_ops64 (uint64_of_int p))
    else finite_field_factorization_main p (finite_field_ops_integer (integer_of_int p)))"

context poly_mod_prime begin
lemmas finite_field_factorization_main_integer = prime_field_gen.finite_field_factorization_main
  [OF prime_field.prime_field_finite_field_ops_integer, unfolded prime_field_def mod_ring_locale_def,
  unfolded poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty]

lemmas finite_field_factorization_main_uint32 = prime_field_gen.finite_field_factorization_main
  [OF prime_field.prime_field_finite_field_ops32, unfolded prime_field_def mod_ring_locale_def,
  unfolded poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty]

lemmas finite_field_factorization_main_uint64 = prime_field_gen.finite_field_factorization_main
  [OF prime_field.prime_field_finite_field_ops64, unfolded prime_field_def mod_ring_locale_def,
  unfolded poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty]

lemma finite_field_factorization_int:
  assumes sq: "poly_mod.square_free_m p f" 
  and result: "finite_field_factorization_int p f = (c,fs)"
  shows "poly_mod.unique_factorization_m p f (c, mset fs)
     c  {0 ..< p} 
     ( fi  set fs. set (coeffs fi)  {0 ..< p})" 
  using finite_field_factorization_main_integer[OF  _ sq, of c fs]
    finite_field_factorization_main_uint32[OF _ _ sq, of c fs]
    finite_field_factorization_main_uint64[OF _ _ sq, of c fs]
    result[unfolded finite_field_factorization_int_def]
  by (auto split: if_splits)