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,353 @@ (* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) section \Finite Rings and Fields\ text \We start by establishing some preliminary results about finite rings and finite fields\ subsection \Finite Rings\ theory Finite_Field imports "HOL-Computational_Algebra.Primes" "HOL-Number_Theory.Residues" "HOL-Library.Cardinality" Subresultants.Binary_Exponentiation Polynomial_Interpolation.Ring_Hom_Poly begin typedef ('a::finite) mod_ring = "{0..x\{0..x\{0..x\{0.. Rep_mod_ring (Abs_mod_ring xb)" using Rep_mod_ring atLeastLessThan_iff by blast assume xb1: "0 \ 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 \ {0..xa::'a mod_ring. (\x\{0.. 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. \x\{0.. 'a mod_ring \ bool" is "(=)" . instance by (intro_classes, transfer, auto) end instantiation mod_ring :: (finite) comm_ring begin lift_definition plus_mod_ring :: "'a mod_ring \ 'a mod_ring \ 'a mod_ring" is "\ x y. (x + y) mod int (CARD('a))" by simp lift_definition uminus_mod_ring :: "'a mod_ring \ 'a mod_ring" is "\ x. if x = 0 then 0 else int (CARD('a)) - x" by simp lift_definition minus_mod_ring :: "'a mod_ring \ 'a mod_ring \ 'a mod_ring" is "\ x y. (x - y) mod int (CARD('a))" by simp lift_definition times_mod_ring :: "'a mod_ring \ 'a mod_ring \ 'a mod_ring" is "\ 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 \ int" is "\ x. x" . lift_definition of_int_mod_ring :: "int \ 'a::finite mod_ring" is "\ 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 \ x \ x < int CARD('a :: finite) \ 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 \ 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 \Nontrivial Finite Rings\ 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 = (\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) (\ x. int x mod int (CARD('a :: nontriv))) (of_nat :: nat \ '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) (\ x. x mod int (CARD('a :: nontriv))) (of_int :: int \ '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) (\a::int. \n. a^n mod CARD('a::nontriv)) ((^)::'a mod_ring \ nat \ '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 \ 'a :: nontriv mod_ring \ bool) ===> (pcr_mod_ring :: int \ 'a mod_ring \ bool) ===> (=)) (\ i j. \k \ {0..k \ {0..k \ {0.. {0.. '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 \ 'a mod_ring \ 'a mod_ring" where "divide_mod_ring x y = x * ((\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 \ 0 \ inverse a * a = 1" proof (unfold inverse_mod_ring_def, transfer) let ?p="CARD('a)" fix x assume x: "x \ {0.. 0" have p0': "0\?p" by auto have "\ ?p dvd x" using x x0 zdvd_imp_le by fastforce then have "\ CARD('a) dvd nat \x\" by simp with x have "\ CARD('a) dvd nat x" by simp have rw: "x ^ nat (int (?p - 2)) * x = x ^ nat (?p - 1)" proof - have p2: "0 \ 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 \\ CARD('a) dvd nat x\] 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 \ 'a mod_ring \ 'a mod_ring" where "modulo_mod_ring x y = (if y = 0 then x else 0)" definition normalize_mod_ring :: "'a mod_ring \ 'a mod_ring" where "normalize_mod_ring x = (if x = 0 then 0 else 1)" definition unit_factor_mod_ring :: "'a mod_ring \ 'a mod_ring" where "unit_factor_mod_ring x = x" definition euclidean_size_mod_ring :: "'a mod_ring \ 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 \ 0 \ 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 \ 'a mod_ring \ 'a mod_ring" where "gcd_mod_ring = Euclidean_Algorithm.gcd" definition lcm_mod_ring :: "'a mod_ring \ 'a mod_ring \ 'a mod_ring" where "lcm_mod_ring = Euclidean_Algorithm.lcm" definition Gcd_mod_ring :: "'a mod_ring set \ 'a mod_ring" where "Gcd_mod_ring = Euclidean_Algorithm.Gcd" definition Lcm_mod_ring :: "'a mod_ring set \ '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: "\ i. i < CARD('a :: prime_card) \ (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 diff --git a/thys/LLL_Basis_Reduction/LLL_Certification.thy b/thys/LLL_Basis_Reduction/LLL_Certification.thy --- a/thys/LLL_Basis_Reduction/LLL_Certification.thy +++ b/thys/LLL_Basis_Reduction/LLL_Certification.thy @@ -1,656 +1,653 @@ (* Authors: René Thiemann BSD *) section \Certification of External LLL Invocations\ text \Instead of using a fully verified algorithm, we also provide a technique to invoke an external LLL solver. In order to check its result, we not only need the reduced basic, but also the matrices which translate between the input basis and the reduced basis. Then we can easily check whether the resulting lattices are indeed identical and just have to start the verified algorithm on the already reduced basis. This invocation will then usually just require one computation of Gram--Schmidt in order to check that the basis is already reduced. Alternatively, one could also throw an error message in case the basis is not reduced.\ subsection \Checking Results of External LLL Solvers\ theory LLL_Certification imports LLL_Impl Jordan_Normal_Form.Show_Matrix begin definition "gauss_jordan_integer_inverse n A B I = (case gauss_jordan A B of (C,D) \ C = I \ list_all is_int_rat (concat (mat_to_list D)))" definition "integer_equivalent n fs gs = (let fs' = map_mat rat_of_int (mat_of_cols n fs); gs' = map_mat rat_of_int (mat_of_cols n gs); I = 1\<^sub>m n in gauss_jordan_integer_inverse n fs' gs' I \ gauss_jordan_integer_inverse n gs' fs' I)" context vec_module begin lemma mat_mult_sub_lattice: assumes fs: "set fs \ carrier_vec n" and gs: "set gs \ carrier_vec n" and A: "A \ carrier_mat (length fs) (length gs)" and prod: "mat_of_rows n fs = map_mat of_int A * mat_of_rows n gs" shows "lattice_of fs \ lattice_of gs" proof let ?m = "length fs" let ?m' = "length gs" let ?i = "of_int :: int \ 'a" let ?I = "map_mat ?i" let ?A = "?I A" have gsC: "mat_of_rows n gs \ carrier_mat ?m' n" by auto from A have A: "?A \ carrier_mat ?m ?m'" by auto from fs have fsi[simp]: "\ i. i < ?m \ fs ! i \ carrier_vec n" by auto hence fsi'[simp]: "\ i. i < ?m \ dim_vec (fs ! i) = n" by simp from gs have fsi[simp]: "\ i. i < ?m' \ gs ! i \ carrier_vec n" by auto hence gsi'[simp]: "\ i. i < ?m' \ dim_vec (gs ! i) = n" by simp fix v assume "v \ lattice_of fs" from in_latticeE[OF this] obtain c where v: "v = M.sumlist (map (\i. ?i (c i) \\<^sub>v fs ! i) [0.. i. ?i (c i))" let ?d = "A\<^sup>T *\<^sub>v vec ?m c" note v also have "\ = mat_of_cols n fs *\<^sub>v ?c" by (rule eq_vecI, auto intro!: dim_sumlist sum.cong simp: sumlist_nth scalar_prod_def mat_of_cols_def) also have "mat_of_cols n fs = (mat_of_rows n fs)\<^sup>T" by (simp add: transpose_mat_of_rows) also have "\ = (?A * mat_of_rows n gs)\<^sup>T" unfolding prod .. also have "\ = (mat_of_rows n gs)\<^sup>T * ?A\<^sup>T" by (rule transpose_mult[OF A gsC]) also have "(mat_of_rows n gs)\<^sup>T = mat_of_cols n gs" by (simp add: transpose_mat_of_rows) finally have "v = (mat_of_cols n gs * ?A\<^sup>T) *\<^sub>v ?c" . also have "\ = mat_of_cols n gs *\<^sub>v (?A\<^sup>T *\<^sub>v ?c)" by (rule assoc_mult_mat_vec, insert A, auto) also have "?A\<^sup>T = ?I (A\<^sup>T)" by fastforce also have "?c = map_vec ?i (vec ?m c)" by auto also have "?I (A\<^sup>T) *\<^sub>v \ = map_vec ?i ?d" using A by (simp add: of_int_hom.mult_mat_vec_hom) finally have "v = mat_of_cols n gs *\<^sub>v map_vec ?i ?d" . define d where "d = ?d" have d: "d \ carrier_vec ?m'" unfolding d_def using A by auto have "v = mat_of_cols n gs *\<^sub>v map_vec ?i d" unfolding d_def by fact also have "\ = M.sumlist (map (\i. ?i (d $ i) \\<^sub>v gs ! i) [0.. lattice_of gs" by (intro in_latticeI, auto) qed end context LLL_with_assms begin lemma mult_left_identity: defines "B \ (map_mat rat_of_int (mat_of_rows n fs_init))" assumes P_carrier[simp]: "P \ carrier_mat m m" and PB: "P * B = B" shows "P = 1\<^sub>m m" proof - let ?set_rows = "set (rows B)" let ?hom = "of_int_hom.vec_hom :: int vec \ rat vec" have set_rows_carrier: "?set_rows \ (carrier_vec n)" by (auto simp add: rows_def B_def) have set_rows_eq: "?set_rows = set (map of_int_hom.vec_hom fs_init)" proof - have "x \ of_int_hom.vec_hom ` set fs_init" if x: "x \ set (rows B)" for x using x unfolding B_def by (metis cof_vec_space.lin_indpt_list_def fs_init image_set lin_dep mat_of_rows_map rows_mat_of_rows) moreover have "of_int_hom.vec_hom xa \ set (rows B)" if xa: "xa \ set fs_init" for xa proof - obtain i where xa: "xa = fs_init ! i" and i: "i y" have 1: "?hom (fs_init ! x) = row B x" unfolding B_def by (metis fs_init index_map_mat(2) len local.set_rows_carrier mat_of_rows_carrier(2) mat_of_rows_map nth_map nth_rows rows_mat_of_rows set_rows_eq that(1)) moreover have 2: "?hom (fs_init ! y) = row B y" unfolding B_def by (metis fs_init index_map_mat(2) len local.set_rows_carrier mat_of_rows_carrier(2) mat_of_rows_map nth_map nth_rows rows_mat_of_rows set_rows_eq that(2)) ultimately have "?hom (fs_init ! x) = ?hom (fs_init ! y)" using row_xy by auto thus False using lin_dep x y row_xy unfolding gs.lin_indpt_list_def using xy x y len unfolding distinct_conv_nth by auto qed thus ?thesis unfolding inj_on_def by auto qed have the_x: "(THE k. k < m \ row B x = row B k) = x" if x: "x < m" for x proof (rule theI2) show "x < m \ row B x = row B x" using x by auto fix xa assume xa: "xa < m \ row B x = row B xa" show "xa = x" using xa inj_on_rowB x unfolding inj_on_def by auto thus "xa = x" . qed let ?h= "row B" show ?thesis proof (rule eq_matI, unfold one_mat_def, auto) fix j assume j: "j < m" let ?f = "(\v. P $$ (j, THE k. k < m \ v = row B k))" let ?g = "\v. if v = row B j then (?f v) - 1 else ?f v" have finsum_closed[simp]: "finsum_vec TYPE(rat) n (\k. P $$ (j, k) \\<^sub>v row B k) {0.. carrier_vec n" by (rule finsum_vec_closed, insert len B_def, auto) have B_carrier[simp]: "B \ carrier_mat m n" using len fs_init B_def by auto define v where "v \ row B j" have v_set_rows: "v \ set (rows B)" using nth_rows j unfolding v_def by (metis B_carrier carrier_matD(1) length_rows nth_mem) have [simp]: "mat_of_rows n fs_init \ carrier_mat m n" using len fs_init by auto have "B = P*B" using PB by auto also have "... = mat\<^sub>r m n (\i. finsum_vec TYPE(rat) n (\k. P $$ (i, k) \\<^sub>v row B k) {0..k. P $$ (j, k) \\<^sub>v row B k) {0..v. ?f v \\<^sub>v v) ?set_rows" (is "?lhs = ?rhs") proof (rule eq_vecI) have rhs_carrier: "?rhs \ carrier_vec n" by (rule finsum_vec_closed, insert set_rows_carrier, auto) have "dim_vec ?lhs = n" using vec_space.finsum_dim by simp also have dim_rhs: "... = dim_vec ?rhs" using rhs_carrier by auto finally show "dim_vec ?lhs = dim_vec ?rhs" . fix i assume i: "i < dim_vec ?rhs" have i_n: "i < n" using i dim_rhs by auto let ?g = "\v. (?f v \\<^sub>v v) $ i" have image_h: "?h `{0..k\{0..\<^sub>v row B k) $ i)" by (rule index_finsum_vec[OF _ i_n], auto) also have "... = sum (?g \ ?h) {0..v. (?f v \\<^sub>v v) $ i) (?h `{0..v\?set_rows. (?f v \\<^sub>v v) $ i)" using image_h by auto also have "... = ?rhs $ i" by (rule index_finsum_vec[symmetric, OF _ i_n], insert set_rows_carrier, auto) finally show "?lhs $ i = ?rhs $ i" by auto qed also have "... = (\\<^bsub>gs.V\<^esub>v\?set_rows. ?f v \\<^sub>v v)" unfolding vec_space.finsum_vec .. also have "... = gs.lincomb ?f ?set_rows" unfolding gs.lincomb_def by auto finally have lincomb_rowBj: "gs.lincomb ?f ?set_rows = row B j" .. have lincomb_0: "gs.lincomb ?g (?set_rows) = 0\<^sub>v n" proof - have v_closed[simp]: "v \ Rn" unfolding v_def using j by auto have lincomb_f_closed[simp]: "gs.lincomb ?f (?set_rows-{v}) \ Rn" by (rule gs.lincomb_closed, insert set_rows_carrier, auto) have fv_v_closed[simp]: "?f v \\<^sub>v v \ Rn" by auto have lincomb_f: "gs.lincomb ?f ?set_rows = ?f v \\<^sub>v v + gs.lincomb ?f (?set_rows-{v})" by (rule gs.lincomb_del2, insert set_rows_carrier v_set_rows, auto) have fvv_gvv: "?f v \\<^sub>v v - v = ?g v \\<^sub>v v" unfolding v_def by (rule eq_vecI, auto, simp add: left_diff_distrib) have lincomb_fg: "gs.lincomb ?f (?set_rows-{v}) = gs.lincomb ?g (?set_rows-{v})" (is "?lhs = ?rhs") proof (rule eq_vecI) show dim_vec_eq: "dim_vec ?lhs = dim_vec ?rhs" by (smt DiffE carrier_vecD gs.lincomb_closed local.set_rows_carrier subsetCE subsetI) fix i assume i: "ix\(?set_rows-{v}). ?f x * x $ i)" by (rule gs.lincomb_index[OF i_n], insert set_rows_carrier, auto) also have "... = (\x\(?set_rows-{v}). ?g x * x $ i)" by (rule sum.cong, auto simp add: v_def) also have "... = ?rhs $ i" by (rule gs.lincomb_index[symmetric, OF i_n], insert set_rows_carrier, auto) finally show "?lhs $ i = ?rhs $ i" . qed have "0\<^sub>v n = gs.lincomb ?f ?set_rows - v" using lincomb_rowBj unfolding v_def B_def by auto also have "... = ?f v \\<^sub>v v + gs.lincomb ?f (?set_rows-{v}) - v" using lincomb_f by auto also have "... = (gs.lincomb ?f (?set_rows-{v}) + ?f v \\<^sub>v v) + - v" unfolding gs.M.a_comm[OF lincomb_f_closed fv_v_closed] by auto also have "... = gs.lincomb ?f (?set_rows-{v}) + (?f v \\<^sub>v v + - v)" by (rule gs.M.a_assoc, auto) also have "... = gs.lincomb ?f (?set_rows-{v}) + (?f v \\<^sub>v v - v)" by auto also have "... = gs.lincomb ?g (?set_rows-{v}) + (?g v \\<^sub>v v)" unfolding lincomb_fg fvv_gvv by auto also have "... = (?g v \\<^sub>v v) + gs.lincomb ?g (?set_rows-{v})" by (rule gs.M.a_comm, auto, rule gs.lincomb_closed, insert set_rows_carrier, auto) also have "... = gs.lincomb ?g (?set_rows)" by (rule gs.lincomb_del2[symmetric], insert v_set_rows set_rows_carrier, auto) finally show ?thesis .. qed have g0: "?g \ ?set_rows \ {0}" by (rule gs.not_lindepD[of ?set_rows, OF ind_set_rows _ _ _ lincomb_0], auto) hence "?g (row B j) = 0" using v_set_rows unfolding v_def Pi_def by blast hence "?f (row B j) - 1 = 0" by auto hence "P $$ (j,j) - 1 = 0" using the_x j by auto thus "P$$(j,j) = 1" by auto fix i assume i: "i < m" and ji: "j \ i" have row_ij: "row B i \ row B j" using inj_on_rowB ji i j unfolding inj_on_def by fastforce have "row B i \ ?set_rows" using nth_rows i by (metis B_carrier carrier_matD(1) length_rows nth_mem) hence "?g (row B i) = 0" using g0 unfolding Pi_def by blast hence "?f (row B i) = 0" using row_ij by auto thus "P $$ (j, i) = 0" using the_x i by auto next show "dim_row P = m" and "dim_col P = m" using P_carrier unfolding carrier_mat_def by auto qed qed text \This is the key lemma. It permits to change from the initial basis @{term fs_init} to an arbitrary @{term gs} that has been computed by some external tool. Here, two change-of-basis matrices U1 and U2 are required to certify the change via the conditions prod1 and prod2.\ lemma LLL_change_basis: assumes gs: "set gs \ carrier_vec n" and len': "length gs = m" and U1: "U1 \ carrier_mat m m" and U2: "U2 \ carrier_mat m m" and prod1: "mat_of_rows n fs_init = U1 * mat_of_rows n gs" and prod2: "mat_of_rows n gs = U2 * mat_of_rows n fs_init" shows "lattice_of gs = lattice_of fs_init" "LLL_with_assms n m gs \" proof - let ?i = "of_int :: int \ int" have "U1 = map_mat ?i U1" by (intro eq_matI, auto) with prod1 have prod1: "mat_of_rows n fs_init = map_mat ?i U1 * mat_of_rows n gs" by simp have "U2 = map_mat ?i U2" by (intro eq_matI, auto) with prod2 have prod2: "mat_of_rows n gs = map_mat ?i U2 * mat_of_rows n fs_init" by simp have "lattice_of gs \ lattice_of fs_init" by (rule mat_mult_sub_lattice[OF gs fs_init _ prod2], auto simp: U2 len len') moreover have "lattice_of gs \ lattice_of fs_init" by (rule mat_mult_sub_lattice[OF fs_init gs _ prod1], auto simp: U1 len len') ultimately show "lattice_of gs = lattice_of fs_init" by blast show "LLL_with_assms n m gs \" proof show "4/3 \ \" by (rule \) show "length gs = m" by fact show "lin_indep gs" proof - let ?fs = "map_mat rat_of_int (mat_of_rows n fs_init)" let ?gs = "map_mat rat_of_int (mat_of_rows n gs)" let ?U1 = "map_mat rat_of_int U1" let ?U2 = "map_mat rat_of_int U2" let ?P = "?U1 * ?U2" have rows_gs_eq: "rows ?gs = map of_int_hom.vec_hom gs" proof (rule nth_equalityI) fix i assume i: "i < length (rows ?gs)" have "rows ?gs ! i = row ?gs i" by (rule nth_rows, insert i, auto) also have "... = of_int_hom.vec_hom (gs ! i)" by (metis (mono_tags, lifting) gs i index_map_mat(2) length_map length_rows map_carrier_vec mat_of_rows_map mat_of_rows_row nth_map nth_mem rows_mat_of_rows subset_code(1)) also have "... = map of_int_hom.vec_hom gs ! i" by (rule nth_map[symmetric], insert i, auto) finally show "rows ?gs ! i = map of_int_hom.vec_hom gs ! i" . qed (simp) have fs_hom: "?fs \ carrier_mat m n" unfolding carrier_mat_def using len by auto have gs_hom: "?gs \ carrier_mat m n" unfolding carrier_mat_def using len' by auto have U1U2: "U1 * U2 \ carrier_mat m m" by (meson assms(3) assms(4) mult_carrier_mat) have U1_hom: "?U1 \ carrier_mat m m" by (simp add: U1) have U2_hom: "?U2 \ carrier_mat m m" by (simp add: U2) have U1U2_hom: "?U1 * ?U2 \ carrier_mat m m" using U1 U2 by auto have Gs_U2Fs: "?gs = ?U2 * ?fs" using prod2 by (metis U2 assms(6) len mat_of_rows_carrier(1) of_int_hom.mat_hom_mult) have fs_hom_eq: "?fs = ?P * ?fs" by (smt U1 U1U2 U2 assms(5) assms(6) assoc_mult_mat fs_hom map_carrier_mat of_int_hom.mat_hom_mult) have P_id: "?P = 1\<^sub>m m" by (rule mult_left_identity[OF U1U2_hom fs_hom_eq[symmetric]]) hence "det (?U1) * det (?U2) = 1" by (smt U1_hom U2_hom det_mult det_one of_int_hom.hom_det) hence det_U2: "det ?U2 \ 0" and det_U1: "det ?U1 \ 0" by auto from det_non_zero_imp_unit[OF U2_hom det_U2, unfolded Units_def, of "()"] have inv_U2: "invertible_mat ?U2" using U1_hom U2_hom unfolding invertible_mat_def inverts_mat_def by (auto simp: ring_mat_def) interpret Rs: vectorspace class_ring "(gs.vs (gs.row_space ?gs))" by (rule gs.vector_space_row_space[OF gs_hom]) interpret RS_fs: vectorspace class_ring "(gs.vs (gs.row_space (?fs)))" by (rule gs.vector_space_row_space[OF fs_hom]) have submoduleGS: "submodule class_ring (gs.row_space ?gs) gs.V" and submoduleFS: "submodule class_ring (gs.row_space ?fs) gs.V" by (metis gs.row_space_def gs.span_is_submodule index_map_mat(3) mat_of_rows_carrier(3) rows_carrier)+ have set_rows_fs_in: "set (rows ?fs) \ gs.row_space ?fs" and rows_gs_row_space: "set (rows ?gs) \ gs.row_space ?gs" unfolding gs.row_space_def by (metis gs.in_own_span index_map_mat(3) mat_of_rows_carrier(3) rows_carrier)+ have Rs_fs_dim: "RS_fs.dim = m" proof - have "RS_fs.dim = card (set (rows ?fs))" proof (rule RS_fs.dim_basis) have "RS_fs.span (set (rows ?fs)) = gs.span (set (rows ?fs))" by (rule gs.span_li_not_depend[OF _ submoduleFS], simp add: set_rows_fs_in) also have "... = carrier (gs.vs (gs.row_space ?fs))" unfolding gs.row_space_def unfolding gs.carrier_vs_is_self by auto finally have "RS_fs.gen_set (set (rows ?fs))" by auto moreover have "RS_fs.lin_indpt (set (rows ?fs))" proof - have "module.lin_dep class_ring (gs.vs (gs.row_space ?fs)) (set (rows ?fs)) = gs.lin_dep (set (rows ?fs))" by (rule gs.span_li_not_depend[OF _ submoduleFS], simp add: set_rows_fs_in) thus ?thesis using lin_dep unfolding gs.lin_indpt_list_def by (metis fs_init mat_of_rows_map rows_mat_of_rows) qed moreover have "set (rows ?fs) \ carrier (gs.vs (gs.row_space ?fs))" by (simp add: set_rows_fs_in) ultimately show "RS_fs.basis (set (rows ?fs))" unfolding RS_fs.basis_def by simp qed (simp) also have "... = m" by (metis cof_vec_space.lin_indpt_list_def distinct_card fs_init len length_map lin_dep mat_of_rows_map rows_mat_of_rows) finally show ?thesis . qed have "gs.row_space ?fs = gs.row_space (?U2*?fs)" by (rule gs.row_space_is_preserved[symmetric, OF inv_U2 U2_hom fs_hom]) also have "... = gs.row_space ?gs" using Gs_U2Fs by auto finally have "gs.row_space ?fs = gs.row_space ?gs" by auto hence "vectorspace.dim class_ring (gs.vs (gs.row_space ?gs)) = m" using Rs_fs_dim fs_hom_eq by auto hence Rs_dim_is_m: "Rs.dim = m" by blast have card_set_rows: "card (set (rows ?gs)) \ m" by (metis assms(2) card_length length_map rows_gs_eq) have Rs_basis: "Rs.basis (set (rows ?gs))" proof (rule Rs.dim_gen_is_basis) show "card (set (rows ?gs)) \ Rs.dim" using card_set_rows Rs_dim_is_m by auto have "Rs.span (set (rows ?gs)) = gs.span (set (rows ?gs))" by (rule gs.span_li_not_depend[OF rows_gs_row_space submoduleGS]) also have "... = carrier (gs.vs (gs.row_space ?gs))" unfolding gs.row_space_def unfolding gs.carrier_vs_is_self by auto finally show "Rs.gen_set (set (rows ?gs))" by auto show "set (rows ?gs) \ carrier (gs.vs (gs.row_space ?gs))" using rows_gs_row_space by auto qed (simp) hence indpt_Rs: "Rs.lin_indpt (set (rows ?gs))" unfolding Rs.basis_def by auto have gs_lin_indpt_rows: "gs.lin_indpt (set (rows ?gs))" (*Is there any automatic way to prove this?*) (*TODO: via gs.span_li_not_depend*) proof define N where "N \ (gs.row_space ?gs)" assume "gs.lin_dep (set (rows ?gs))" from this obtain A f v where A1: "finite A" and A2: "A \ set (rows ?gs)" and lc_gs: "gs.lincomb f A = 0\<^sub>v n" and v: "v \ A" and fv: "f v \ 0" unfolding gs.lin_dep_def by blast have "gs.lincomb f A = module.lincomb (gs.vs N) f A" by (rule gs.lincomb_not_depend, insert submoduleGS A1 A2 gs.row_space_def rows_gs_row_space, auto simp add: N_def gs.row_space_def) also have "... = Rs.lincomb f A" using N_def by blast finally have "Rs.lin_dep (set (rows ?gs))" unfolding Rs.lin_dep_def using A1 A2 v fv lc_gs by auto thus False using indpt_Rs by auto qed have "card (set (rows ?gs)) \ Rs.dim" by (rule Rs.gen_ge_dim, insert rows_gs_row_space Rs_basis, auto simp add: Rs.basis_def) hence card_m: "card (set (rows ?gs)) = m" using card_set_rows Rs_dim_is_m by auto have "distinct (map (of_int_hom.vec_hom::int vec \ rat vec) gs)" using rows_gs_eq assms(2) card_m card_distinct by force moreover have "set (map of_int_hom.vec_hom gs) \ Rn" using gs by auto ultimately show "gs.lin_indpt_list (map of_int_hom.vec_hom gs)" using gs_lin_indpt_rows unfolding rows_gs_eq gs.lin_indpt_list_def by auto qed qed qed lemma gauss_jordan_integer_inverse: fixes fs gs :: "int vec list" assumes gs: "set gs \ carrier_vec n" and len_gs: "length gs = n" and fs: "set fs \ carrier_vec n" and len_fs: "length fs = n" and gauss: "gauss_jordan_integer_inverse n (map_mat rat_of_int (mat_of_cols n fs)) (map_mat rat_of_int (mat_of_cols n gs)) (1\<^sub>m n)" (is "gauss_jordan_integer_inverse _ ?fs ?gs _") shows "\ U. U \ carrier_mat n n \ mat_of_rows n gs = U * mat_of_rows n fs" proof - have fs': "?fs \ carrier_mat n n" using fs len_fs by auto have gs': "?gs \ carrier_mat n n" using gs len_gs by auto note gauss = gauss[unfolded gauss_jordan_integer_inverse_def] from gauss obtain A where gauss: "gauss_jordan ?fs ?gs = (1\<^sub>m n, A)" and int: "list_all is_int_rat (concat (mat_to_list A))" by auto note gauss = gauss_jordan[OF fs' gs' gauss] note A = gauss(4) let ?A = "map_mat int_of_rat A" from gauss(2)[OF A] A have id: "?fs * A = ?gs" by auto let ?U = "(map_mat int_of_rat A)\<^sup>T" from A have U: "?U \ carrier_mat n n" by auto have "A = map_mat of_int ?A" using int[unfolded list_all_iff] A by (intro eq_matI, auto simp: mat_to_list_def) with id have "?gs = ?fs * map_mat of_int ?A" by auto also have "\ = map_mat of_int (mat_of_cols n fs * ?A)" by (rule of_int_hom.mat_hom_mult[symmetric], insert fs' A, auto) finally have "mat_of_cols n fs * ?A = mat_of_cols n gs" using of_int_hom.mat_hom_inj by fastforce hence "(mat_of_cols n gs)\<^sup>T = (mat_of_cols n fs * ?A)\<^sup>T" by simp also have "\ = ?U * (mat_of_cols n fs)\<^sup>T" by (rule transpose_mult, insert fs' A, auto) also have "(mat_of_cols n fs)\<^sup>T = mat_of_rows n fs" using fs len_fs unfolding mat_of_rows_def mat_of_cols_def by (intro eq_matI, auto) also have "(mat_of_cols n gs)\<^sup>T = mat_of_rows n gs" using gs len_gs unfolding mat_of_rows_def mat_of_cols_def by (intro eq_matI, auto) finally show ?thesis using U by blast qed lemma LLL_change_basis_mat_inverse: assumes gs: "set gs \ carrier_vec n" and len': "length gs = n" and "m = n" and eq: "integer_equivalent n fs_init gs" shows "lattice_of gs = lattice_of fs_init" "LLL_with_assms n m gs \" proof - from eq[unfolded integer_equivalent_def Let_def] have 1: "gauss_jordan_integer_inverse n (of_int_hom.mat_hom (mat_of_cols n fs_init)) (of_int_hom.mat_hom (mat_of_cols n gs)) (1\<^sub>m n)" and 2: "gauss_jordan_integer_inverse n (of_int_hom.mat_hom (mat_of_cols n gs)) (of_int_hom.mat_hom (mat_of_cols n fs_init)) (1\<^sub>m n)" by auto note len = len[unfolded \m = n\] from gauss_jordan_integer_inverse[OF gs len' fs_init len 1] \m = n\ obtain U where U: "U \ carrier_mat m m" "mat_of_rows n gs = U * mat_of_rows n fs_init" by auto from gauss_jordan_integer_inverse[OF fs_init len gs len' 2] \m = n\ obtain V where V: "V \ carrier_mat m m" "mat_of_rows n fs_init = V * mat_of_rows n gs" by auto from LLL_change_basis[OF gs len'[folded \m = n\] V(1) U(1) V(2) U(2)] show "lattice_of gs = lattice_of fs_init" "LLL_with_assms n m gs \" by blast+ qed end text \External solvers must deliver a reduced basis and optionally two matrices to convert between the input and the reduced basis. These two matrices are mandatory if the input matrix is not a square matrix.\ consts external_lll_solver :: "integer \ integer \ integer list list \ integer list list \ (integer list list \ integer list list)option" definition reduce_basis_external :: "rat \ int vec list \ int vec list" where "reduce_basis_external \ fs = (case fs of Nil \ [] | Cons f _ \ (let rb = reduce_basis \; fsi = map (map integer_of_int o list_of_vec) fs; n = dim_vec f; m = length fs in case external_lll_solver (map_prod integer_of_int integer_of_int (quotient_of \)) fsi of (gsi, co) \ let gs = (map (vec_of_list o map int_of_integer) gsi) in if \ (length gs = m \ (\ gi \ set gs. dim_vec gi = n)) then Code.abort (STR ''error in external LLL invocation: dimensions of reduced basis do not fit\input to external solver: '' + String.implode (show fs) + STR ''\\'') (\ _. rb fs) else case co of Some (u1i, u2i) \ (let u1 = mat_of_rows_list m (map (map int_of_integer) u1i); u2 = mat_of_rows_list m (map (map int_of_integer) u2i); gs = (map (vec_of_list o map int_of_integer) gsi); Fs = mat_of_rows n fs; Gs = mat_of_rows n gs in if (dim_row u1 = m \ dim_col u1 = m \ dim_row u2 = m \ dim_col u2 = m \ Fs = u1 * Gs \ Gs = u2 * Fs) then rb gs else Code.abort (STR ''error in external lll invocation\f,g,u1,u2 are as follows\'' + String.implode (show Fs) + STR ''\\'' + String.implode (show Gs) + STR ''\\'' + String.implode (show u1) + STR ''\\'' + String.implode (show u2) + STR ''\\'' ) (\ _. rb fs)) | None \ (if (n = m \ integer_equivalent n fs gs) then rb gs else Code.abort (STR ''error in external LLL invocation:\'' + (if n = m then STR ''reduced matrix does not span same lattice'' else STR ''no certificate only allowed for square matrices'')) (\ _. rb fs)) ))" definition short_vector_external :: "rat \ int vec list \ int vec" where "short_vector_external \ fs = (hd (reduce_basis_external \ fs))" -instance bool :: prime_card - by (standard, auto) - context LLL_with_assms begin lemma reduce_basis_external: assumes res: "reduce_basis_external \ fs_init = fs" shows "reduced fs m" "LLL_invariant True m fs" (* "lattice_of fs = lattice_of fs_init" is part of LLL_invariant *) proof (atomize(full), goal_cases) case 1 show ?case proof (cases "LLL_Impl.reduce_basis \ fs_init = fs") case True from reduce_basis[OF this] show ?thesis by simp next case False show ?thesis proof (cases fs_init) case Nil with res have "fs = []" unfolding reduce_basis_external_def by auto with False Nil have False by (simp add: LLL_Impl.reduce_basis_def) thus ?thesis .. next case (Cons f rest) from Cons fs_init len have dim_fs_n: "dim_vec f = n" by auto let ?ext = "external_lll_solver (map_prod integer_of_int integer_of_int (quotient_of \)) (map (map integer_of_int \ list_of_vec) fs_init)" note res = res[unfolded reduce_basis_external_def Cons Let_def list.case Code.abort_def dim_fs_n, folded Cons] from res False obtain gsi co where ext: "?ext = (gsi, co)" by (cases ?ext, auto) define gs where "gs = map (vec_of_list o map int_of_integer) gsi" note res = res[unfolded ext option.simps split len dim_fs_n, folded gs_def] from res False have not: "(\ (length gs = m \ (\gi\set gs. dim_vec gi = n))) = False" by (auto split: if_splits) note res = res[unfolded this if_False] from not have gs: "set gs \ carrier_vec n" and len_gs: "length gs = m" by auto have "lattice_of gs = lattice_of fs_init \ LLL_with_assms n m gs \ \ LLL_Impl.reduce_basis \ gs = fs" proof (cases co) case (Some pair) from res Some obtain u1i u2i where co: "co = Some (u1i, u2i)" by (cases co, auto) define u1 where "u1 = mat_of_rows_list m (map (map int_of_integer) u1i)" define u2 where "u2 = mat_of_rows_list m (map (map int_of_integer) u2i)" note res = res[unfolded co option.simps split len dim_fs_n, folded u1_def u2_def gs_def] from res False have u1: "u1 \ carrier_mat m m" and u2: "u2 \ carrier_mat m m" and prod1: "mat_of_rows n fs_init = u1 * mat_of_rows n gs" and prod2: "mat_of_rows n gs = u2 * mat_of_rows n fs_init" and gs_v: "LLL_Impl.reduce_basis \ gs = fs" by (auto split: if_splits) from LLL_change_basis[OF gs len_gs u1 u2 prod1 prod2] gs_v show ?thesis by auto next case None from res[unfolded None option.simps] False have id: "fs = LLL_Impl.reduce_basis \ gs" and nm: "n = m" and equiv: "integer_equivalent n fs_init gs" by (auto split: if_splits) from LLL_change_basis_mat_inverse[OF gs len_gs[folded nm] nm[symmetric] equiv] id show ?thesis by auto qed hence id: "lattice_of gs = lattice_of fs_init" and assms: "LLL_with_assms n m gs \" and gs_fs: "LLL_Impl.reduce_basis \ gs = fs" by auto from LLL_with_assms.reduce_basis[OF assms gs_fs] have red: "reduced fs m" and inv: "LLL.LLL_invariant n m gs \ True m fs" by auto from inv[unfolded LLL.LLL_invariant_def LLL.L_def id] have lattice: "lattice_of fs = lattice_of fs_init" by auto show ?thesis proof (intro conjI red lattice) show "LLL_invariant True m fs" using inv unfolding LLL.LLL_invariant_def LLL.L_def id . qed qed qed qed lemma short_vector_external: assumes res: "short_vector_external \ fs_init = v" and m0: "m \ 0" shows "v \ carrier_vec n" "v \ L - {0\<^sub>v n}" "h \ L - {0\<^sub>v n} \ rat_of_int (sq_norm v) \ \ ^ (m - 1) * rat_of_int (sq_norm h)" "v \ 0\<^sub>v j" proof (atomize(full), goal_cases) case 1 obtain fs where red: "reduce_basis_external \ fs_init = fs" by blast from res[unfolded short_vector_external_def red] have v: "v = hd fs" by auto from reduce_basis_external[OF red] have red: "reduced fs m" and inv: "LLL_invariant True m fs" by blast+ from basis_reduction_short_vector[OF inv v m0] show ?case by blast qed end text \Unspecified constant to easily enable/disable external lll solver in generated code\ consts enable_external_lll_solver :: bool definition short_vector_hybrid :: "rat \ int vec list \ int vec" where "short_vector_hybrid = (if enable_external_lll_solver then short_vector_external else short_vector)" definition reduce_basis_hybrid :: "rat \ int vec list \ int vec list" where "reduce_basis_hybrid = (if enable_external_lll_solver then reduce_basis_external else reduce_basis)" context LLL_with_assms begin lemma short_vector_hybrid: assumes res: "short_vector_hybrid \ fs_init = v" and m0: "m \ 0" shows "v \ carrier_vec n" "v \ L - {0\<^sub>v n}" "h \ L - {0\<^sub>v n} \ rat_of_int (sq_norm v) \ \ ^ (m - 1) * rat_of_int (sq_norm h)" "v \ 0\<^sub>v j" using short_vector[of v, OF _ m0] short_vector_external[of v, OF _ m0] res[unfolded short_vector_hybrid_def] by (auto split: if_splits) lemma reduce_basis_hybrid: assumes res: "reduce_basis_hybrid \ fs_init = fs" shows "reduced fs m" "LLL_invariant True m fs" using reduce_basis_external[of fs] reduce_basis[of fs] res[unfolded reduce_basis_hybrid_def] by (auto split: if_splits) end lemma lll_oracle_default_code[code]: "external_lll_solver x = Code.abort (STR ''no implementation of external_lll_solver specified'') (\ _. external_lll_solver x)" by simp text \By default, external solvers are disabled. For enabling an external solver, load it via a separate theory like \<^file>\FPLLL_Solver.thy\\ overloading enable_external_lll_solver \ enable_external_lll_solver begin definition enable_external_lll_solver where "enable_external_lll_solver = False" end definition "short_vector_test_hybrid xs = (let ys = map (vec_of_list o map int_of_integer) xs in integer_of_int (sq_norm (short_vector_hybrid (3/2) ys)))" (* export_code short_vector_test_hybrid in Haskell module_name LLL *) end diff --git a/thys/Perfect_Fields/Perfect_Field_Library.thy b/thys/Perfect_Fields/Perfect_Field_Library.thy --- a/thys/Perfect_Fields/Perfect_Field_Library.thy +++ b/thys/Perfect_Fields/Perfect_Field_Library.thy @@ -1,341 +1,268 @@ (* File: Perfect_Fields/Perfect_Field_Library.thy Authors: Katharina Kreuzer (TU München) Manuel Eberl (University of Innsbruck) A few auxiliary results, most of which should probably be moved to the distribution. *) theory Perfect_Field_Library imports "HOL-Computational_Algebra.Computational_Algebra" "Berlekamp_Zassenhaus.Finite_Field" begin -(* TODO: Orphan instance! Move! *) -instance bool :: prime_card - by standard auto - -(* TODO: replace in library *) -theorem (in comm_semiring_1) binomial_ring: - "(a + b :: 'a)^n = (\k\n. (of_nat (n choose k)) * a^k * b^(n-k))" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - have decomp: "{0..n+1} = {0} \ {n + 1} \ {1..n}" - by auto - have decomp2: "{0..n} = {0} \ {1..n}" - by auto - have "(a + b)^(n+1) = (a + b) * (\k\n. of_nat (n choose k) * a^k * b^(n - k))" - using Suc.hyps by simp - also have "\ = a * (\k\n. of_nat (n choose k) * a^k * b^(n-k)) + - b * (\k\n. of_nat (n choose k) * a^k * b^(n-k))" - by (rule distrib_right) - also have "\ = (\k\n. of_nat (n choose k) * a^(k+1) * b^(n-k)) + - (\k\n. of_nat (n choose k) * a^k * b^(n - k + 1))" - by (auto simp add: sum_distrib_left ac_simps) - also have "\ = (\k\n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + - (\k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))" - by (simp add: atMost_atLeast0 sum.shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum.cl_ivl_Suc) - also have "\ = b^(n + 1) + - (\k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + (a^(n + 1) + - (\k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)))" - using sum.nat_ivl_Suc' [of 1 n "\k. of_nat (n choose (k-1)) * a ^ k * b ^ (n + 1 - k)"] - by (simp add: sum.atLeast_Suc_atMost atMost_atLeast0) - also have "\ = a^(n + 1) + b^(n + 1) + - (\k=1..n. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))" - by (auto simp add: field_simps sum.distrib [symmetric] choose_reduce_nat) - also have "\ = (\k\n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))" - using decomp by (simp add: atMost_atLeast0 field_simps) - finally show ?case - by simp -qed - -(* taken from Berlekamp_Zassenhaus *) -lemma prime_not_dvd_fact: -assumes kn: "k < n" and prime_n: "prime n" -shows "\ n dvd fact k" - using kn leD prime_dvd_fact_iff prime_n by auto - -(* taken from Berlekamp_Zassenhaus *) -lemma dvd_choose_prime: -assumes kn: "k < n" and k: "k \ 0" and n: "n \ 0" and prime_n: "prime n" -shows "n dvd (n choose k)" -proof - - have "n dvd (fact n)" by (simp add: fact_num_eq_if n) - moreover have "\ n dvd (fact k * fact (n-k))" - proof (rule ccontr, safe) - assume "n dvd fact k * fact (n - k)" - hence "n dvd fact k \ n dvd fact (n - k)" using prime_dvd_mult_eq_nat[OF prime_n] by simp - moreover have "\ n dvd (fact k)" by (rule prime_not_dvd_fact[OF kn prime_n]) - moreover have "\ n dvd fact (n - k)" using prime_not_dvd_fact[OF _ prime_n] kn k by simp - ultimately show False by simp - qed - moreover have "(fact n::nat) = fact k * fact (n-k) * (n choose k)" - using binomial_fact_lemma kn by auto - ultimately show ?thesis using prime_n - by (auto simp add: prime_dvd_mult_iff) -qed - -lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \ Suc 0" - by (metis One_nat_def of_nat_1 of_nat_CHAR zero_neq_one) - -lemma (in idom) CHAR_not_1' [simp]: "CHAR('a) \ Suc 0" - using local.of_nat_CHAR by fastforce - lemma semiring_char_mod_ring [simp]: "CHAR('n :: nontriv mod_ring) = CARD('n)" proof (rule CHAR_eq_posI) fix x assume "x > 0" "x < CARD('n)" thus "of_nat x \ (0 :: 'n mod_ring)" by transfer auto qed auto lemma of_nat_eq_iff_cong_CHAR: "of_nat x = (of_nat y :: 'a :: semiring_1_cancel) \ [x = y] (mod CHAR('a))" proof (induction x y rule: linorder_wlog) case (le x y) define z where "z = y - x" have [simp]: "y = x + z" using le by (auto simp: z_def) have "(CHAR('a) dvd z) = [x = x + z] (mod CHAR('a))" by (metis \y = x + z\ cong_def le mod_eq_dvd_iff_nat z_def) thus ?case by (simp add: of_nat_eq_0_iff_char_dvd) qed (simp add: eq_commute cong_sym_eq) lemma (in ring_1) of_int_eq_0_iff_char_dvd: "(of_int n = (0 :: 'a)) = (int CHAR('a) dvd n)" proof (cases "n \ 0") case True hence "(of_int n = (0 :: 'a)) \ (of_nat (nat n)) = (0 :: 'a)" by auto also have "\ \ CHAR('a) dvd nat n" by (subst of_nat_eq_0_iff_char_dvd) auto also have "\ \ int CHAR('a) dvd n" using True by presburger finally show ?thesis . next case False hence "(of_int n = (0 :: 'a)) \ -(of_nat (nat (-n))) = (0 :: 'a)" by auto also have "\ \ CHAR('a) dvd nat (-n)" by (auto simp: of_nat_eq_0_iff_char_dvd) also have "\ \ int CHAR('a) dvd n" using False dvd_nat_abs_iff[of "CHAR('a)" n] by simp finally show ?thesis . qed lemma (in ring_1) of_int_eq_iff_cong_CHAR: "of_int x = (of_int y :: 'a) \ [x = y] (mod int CHAR('a))" proof - have "of_int x = (of_int y :: 'a) \ of_int (x - y) = (0 :: 'a)" by auto also have "\ \ (int CHAR('a) dvd x - y)" by (rule of_int_eq_0_iff_char_dvd) also have "\ \ [x = y] (mod int CHAR('a))" by (simp add: cong_iff_dvd_diff) finally show ?thesis . qed lemma finite_imp_CHAR_pos: assumes "finite (UNIV :: 'a set)" shows "CHAR('a :: semiring_1_cancel) > 0" proof - have "\n\UNIV. infinite {m \ UNIV. of_nat m = (of_nat n :: 'a)}" proof (rule pigeonhole_infinite) show "infinite (UNIV :: nat set)" by simp show "finite (range (of_nat :: nat \ 'a))" by (rule finite_subset[OF _ assms]) auto qed then obtain n :: nat where "infinite {m \ UNIV. of_nat m = (of_nat n :: 'a)}" by blast hence "\({m \ UNIV. of_nat m = (of_nat n :: 'a)} \ {n})" by (intro notI) (use finite_subset in blast) then obtain m where "m \ n" "of_nat m = (of_nat n :: 'a)" by blast hence "[m = n] (mod CHAR('a))" by (simp add: of_nat_eq_iff_cong_CHAR) hence "CHAR('a) \ 0" using \m \ n\ by (intro notI) auto thus ?thesis by simp qed lemma CHAR_dvd_CARD: "CHAR('a :: ring_1) dvd CARD('a)" proof (cases "CARD('a) = 0") case False hence [intro]: "CHAR('a) > 0" by (simp add: card_eq_0_iff finite_imp_CHAR_pos) define G where "G = \ carrier = (UNIV :: 'a set), monoid.mult = (+), one = (0 :: 'a) \" define H where "H = (of_nat ` {.. carrier G" show "\y\carrier G. y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>" by (intro bexI[of _ "-x"]) (auto simp: G_def) qed (auto simp: G_def add_ac) interpret subgroup H G proof show "\\<^bsub>G\<^esub> \ H" using False unfolding G_def H_def by (intro image_eqI[of _ _ 0]) auto next fix x y :: 'a assume "x \ H" "y \ H" then obtain x' y' where [simp]: "x = of_nat x'" "y = of_nat y'" by (auto simp: H_def) have "x + y = of_nat ((x' + y') mod CHAR('a))" by (auto simp flip: of_nat_add simp: of_nat_eq_iff_cong_CHAR) moreover have "(x' + y') mod CHAR('a) < CHAR('a)" using H_def \y \ H\ by fastforce ultimately show "x \\<^bsub>G\<^esub> y \ H" by (auto simp: H_def G_def intro!: imageI) next fix x :: 'a assume x: "x \ H" then obtain x' where [simp]: "x = of_nat x'" and x': "x' < CHAR('a)" by (auto simp: H_def) have "CHAR('a) dvd x' + (CHAR('a) - x') mod CHAR('a)" by (metis x' dvd_eq_mod_eq_0 le_add_diff_inverse mod_add_right_eq mod_self order_less_imp_le) hence "x + of_nat ((CHAR('a) - x') mod CHAR('a)) = 0" by (auto simp flip: of_nat_add simp: of_nat_eq_0_iff_char_dvd) moreover from this have "inv\<^bsub>G\<^esub> x = of_nat ((CHAR('a) - x') mod CHAR('a))" by (intro inv_equality) (auto simp: G_def add_ac) moreover have "of_nat ((CHAR('a) - x') mod CHAR('a)) \ H" unfolding H_def using \CHAR('a) > 0\ by (intro imageI) auto ultimately show "inv\<^bsub>G\<^esub> x \ H" by force qed (auto simp: G_def H_def) have "card H dvd card (rcosets\<^bsub>G\<^esub> H) * card H" by simp also have "card (rcosets\<^bsub>G\<^esub> H) * card H = Coset.order G" proof (rule lagrange_finite) show "finite (carrier G)" using False card_ge_0_finite by (auto simp: G_def) qed (fact is_subgroup) finally have "card H dvd CARD('a)" by (simp add: Coset.order_def G_def) also have "card H = card {.. 0" shows "prime CHAR('a)" proof - have False if ab: "a \ 1" "b \ 1" "CHAR('a) = a * b" for a b proof - from assms ab have "a > 0" "b > 0" by (auto intro!: Nat.gr0I) have "of_nat (a * b) = (0 :: 'a)" using ab by (metis of_nat_CHAR) also have "of_nat (a * b) = (of_nat a :: 'a) * of_nat b" by simp finally have "of_nat a * of_nat b = (0 :: 'a)" . moreover have "of_nat a * of_nat b \ (0 :: 'a)" using ab \a > 0\ \b > 0\ by (intro no_zero_divisors) (auto simp: of_nat_eq_0_iff_char_dvd) ultimately show False by contradiction qed moreover have "CHAR('a) > 1" using assms CHAR_not_1' by linarith ultimately have "prime_elem CHAR('a)" by (intro irreducible_imp_prime_elem) (auto simp: Factorial_Ring.irreducible_def) thus ?thesis by auto qed text \ Characteristics are preserved by typical functors (polynomials, power series, Laurent series): \ lemma semiring_char_poly [simp]: "CHAR('a :: comm_semiring_1 poly) = CHAR('a)" by (rule CHAR_eqI) (auto simp: of_nat_poly of_nat_eq_0_iff_char_dvd) lemma semiring_char_fps [simp]: "CHAR('a :: comm_semiring_1 fps) = CHAR('a)" by (rule CHAR_eqI) (auto simp flip: fps_of_nat simp: of_nat_eq_0_iff_char_dvd) (* TODO Move *) lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 \ c = 0" using fls_const_0 fls_const_nonzero by blast lemma semiring_char_fls [simp]: "CHAR('a :: comm_semiring_1 fls) = CHAR('a)" by (rule CHAR_eqI) (auto simp: fls_of_nat of_nat_eq_0_iff_char_dvd fls_const_nonzero) lemma irreducible_power_iff [simp]: "irreducible (p ^ n) \ irreducible p \ n = 1" proof assume *: "irreducible (p ^ n)" have [simp]: "\p dvd 1" proof assume "p dvd 1" hence "p ^ n dvd 1" by (metis dvd_power_same power_one) with * show False by auto qed consider "n = 0" | "n = 1" | "n > 1" by linarith thus "irreducible p \ n = 1" proof cases assume "n > 1" hence "p ^ n = p * p ^ (n - 1)" by (cases n) auto with * \\ p dvd 1\ have "p ^ (n - 1) dvd 1" using irreducible_multD by blast with \\p dvd 1\ and \n > 1\ have False by (meson dvd_power dvd_trans zero_less_diff) thus ?thesis .. qed (use * in auto) qed auto lemma pderiv_monom: "pderiv (Polynomial.monom c n) = of_nat n * Polynomial.monom c (n - 1)" proof (cases n) case (Suc n) show ?thesis unfolding monom_altdef Suc pderiv_smult pderiv_power_Suc pderiv_pCons by (simp add: of_nat_poly) qed (auto simp: monom_altdef) lemma uminus_CHAR_2 [simp]: assumes "CHAR('a :: ring_1) = 2" shows "-(x :: 'a) = x" proof - have "x + x = 2 * x" by (simp add: mult_2) also have "2 = (0 :: 'a)" using assms by (metis of_nat_CHAR of_nat_numeral) finally show ?thesis by (simp add: add_eq_0_iff2) qed lemma minus_CHAR_2 [simp]: assumes "CHAR('a :: ring_1) = 2" shows "(x - y :: 'a) = x + y" using uminus_CHAR_2[of y] assms by simp lemma minus_power_prime_CHAR: assumes "p = CHAR('a :: {ring_1})" "prime p" shows "(-x :: 'a) ^ p = -(x ^ p)" proof (cases "p = 2") case False have "prime p" using assms by blast with False have "odd p" using primes_dvd_imp_eq two_is_prime_nat by blast thus ?thesis by simp qed (use assms in auto) end \ No newline at end of file