This instance will be upgraded to Heptapod 0.31.0rc on 2022-05-19 at 11:00 UTC+2 (a few minutes of down time)

Commit c05ee65b authored by Manuel Eberl's avatar Manuel Eberl
Browse files

adapted to isabelle-dev/e0237f2eb49d

parent 8b6582b73697
......@@ -535,7 +535,7 @@ proof (cases "p=0")
qed auto
lemma degree_of_gcd: "degree (gcd q r) \<noteq> 0 \<longleftrightarrow>
degree (gcd (of_int_poly q :: 'a :: {field_char_0,euclidean_ring_gcd} poly) (of_int_poly r)) \<noteq> 0"
degree (gcd (of_int_poly q :: 'a :: {field_char_0, field_gcd} poly) (of_int_poly r)) \<noteq> 0"
proof -
let ?r = "of_rat :: rat \<Rightarrow> 'a"
interpret rpoly: field_hom' ?r
......@@ -598,7 +598,7 @@ end
lemma factors_of_int_poly:
defines "rp \<equiv> ipoly :: int poly \<Rightarrow> 'a :: {euclidean_ring_gcd,field_char_0} \<Rightarrow> 'a"
defines "rp \<equiv> ipoly :: int poly \<Rightarrow> 'a :: {field_gcd,field_char_0} \<Rightarrow> 'a"
assumes "factors_of_int_poly p = qs"
shows "\<And> q. q \<in> set qs \<Longrightarrow> irreducible q \<and> lead_coeff q > 0 \<and> degree q \<le> degree p \<and> degree q \<noteq> 0"
"p \<noteq> 0 \<Longrightarrow> rp p x = 0 \<longleftrightarrow> (\<exists> q \<in> set qs. rp q x = 0)"
......@@ -696,7 +696,7 @@ proof -
qed
lemma factors_int_poly_represents:
fixes x :: "'a :: {field_char_0,euclidean_ring_gcd}"
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes p: "p represents x"
shows "\<exists> q \<in> set (factors_of_int_poly p).
q represents x \<and> irreducible q \<and> lead_coeff q > 0 \<and> degree q \<le> degree p"
......@@ -803,7 +803,7 @@ proof -
then show ?thesis by (auto intro: exI[of _ ?p] simp: cf_pos_def)
qed
lemma gcd_of_int_poly: "gcd (of_int_poly f) (of_int_poly g :: 'a :: {field_char_0,euclidean_ring_gcd} poly) =
lemma gcd_of_int_poly: "gcd (of_int_poly f) (of_int_poly g :: 'a :: {field_char_0,field_gcd} poly) =
smult (inverse (of_int (lead_coeff (gcd f g)))) (of_int_poly (gcd f g))"
proof -
let ?ia = "of_int_poly :: _ \<Rightarrow> 'a poly"
......@@ -817,7 +817,7 @@ proof -
qed
lemma algebraic_imp_represents_unique:
fixes x :: "'a :: {field_char_0,euclidean_ring_gcd}"
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes "algebraic x"
shows "\<exists>! p. p represents x \<and> irreducible p \<and> lead_coeff p > 0" (is "Ex1 ?p")
proof -
......@@ -852,7 +852,7 @@ proof -
qed
corollary irreducible_represents_imp_degree:
fixes x :: "'a :: {field_char_0,euclidean_ring_gcd}"
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes "irreducible f" and "f represents x" and "g represents x"
shows "degree f \<le> degree g"
proof -
......@@ -1236,7 +1236,7 @@ lemma sgn_ipoly_add_rat[simp]:
lemma irreducible_preservation:
fixes x :: "'a :: {field_char_0,euclidean_ring_gcd}"
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes irr: "irreducible p"
and x: "p represents x"
and y: "q represents y"
......@@ -1307,7 +1307,7 @@ proof-
qed
lemma reflect_poly_irreducible:
fixes x :: "'a :: {field_char_0,euclidean_ring_gcd}"
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes p: "irreducible p" and x: "p represents x" and x0: "x \<noteq> 0"
shows "irreducible (reflect_poly p)"
proof -
......
......@@ -137,7 +137,7 @@ lemma of_rat_of_int_poly: "map_poly of_rat (of_int_poly p) = of_int_poly p"
by (subst map_poly_map_poly, auto simp: o_def)
lemma square_free_of_int_poly: assumes "square_free p"
shows "square_free (of_int_poly p :: 'a :: {euclidean_ring_gcd, field_char_0} poly)"
shows "square_free (of_int_poly p :: 'a :: {field_gcd, field_char_0} poly)"
proof -
have "square_free (map_poly of_rat (of_int_poly p) :: 'a poly)"
unfolding of_rat_hom.square_free_map_poly by (rule square_free_int_rat[OF assms])
......
......@@ -194,7 +194,7 @@ lemma euclid_ext_i [transfer_rule]:
end
locale field_ops = idom_divide_ops ops R + euclidean_semiring_ops ops R for ops :: "'i arith_ops_record" and
R :: "'i \<Rightarrow> 'a :: {field, normalization_euclidean_semiring, euclidean_ring, factorial_ring_gcd} \<Rightarrow> bool" +
R :: "'i \<Rightarrow> 'a :: {field_gcd} \<Rightarrow> bool" +
assumes inverse[transfer_rule]: "(R ===> R) inverse Fields.inverse"
......
......@@ -315,16 +315,16 @@ next
from p_dvd_q obtain k where q: "q = k * p" unfolding dvd_def by (auto simp: ac_simps)
with q0 have "k \<noteq> 0" by auto
then have "degree k = 0"
using associatedD2 n p0 q
by (metis (no_types, lifting) mult_cancel_right1 normalize_eq_0_iff normalize_mult poly_dvd_1)
using degree_eq degree_mult_eq p0 q by fastforce
then obtain c where k: "k = [: c :]" by (metis degree_0_id)
with \<open>k \<noteq> 0\<close> have "c \<noteq> 0" by auto
have "q = smult c p" unfolding q k by simp
with \<open>c \<noteq> 0\<close> show ?thesis by auto
qed
lemma prod_list_normalize: "normalize (prod_list P) = prod_list (map normalize P)"
lemma prod_list_normalize:
fixes P :: "'b :: {idom_divide,normalization_semidom_multiplicative} poly list"
shows "normalize (prod_list P) = prod_list (map normalize P)"
proof (induct P)
case Nil
show ?case by auto
......@@ -361,7 +361,7 @@ end
lemma gcd_monic_constant:
"gcd f g \<in> {1, f}" if "monic f" and "degree g = 0"
for f g :: "'a :: {field,euclidean_ring_gcd} poly"
for f g :: "'a :: {field_gcd} poly"
proof (cases "g = 0")
case True
moreover from \<open>monic f\<close> have "normalize f = f"
......@@ -415,7 +415,7 @@ lemma power_poly_f_mod_binary: "power_poly_f_mod m a n = (if n = 0 then 1 mod m
else let (d, r) = Divides.divmod_nat n 2;
rec = power_poly_f_mod m ((a * a) mod m) d in
if r = 0 then rec else (rec * a) mod m)"
for m a :: "'a :: {factorial_ring_gcd, field} poly"
for m a :: "'a :: {field_gcd} poly"
proof -
note d = power_poly_f_mod_def
show ?thesis
......@@ -706,7 +706,7 @@ proof -
qed
lemma monic_prod_gcd:
assumes f: "finite A" and f0: "(f :: 'b :: {field,factorial_ring_gcd} poly) \<noteq> 0"
assumes f: "finite A" and f0: "(f :: 'b :: {field_gcd} poly) \<noteq> 0"
shows "monic (\<Prod>c\<in>A. gcd f (h - [:c:]))"
using f
proof (induct A)
......@@ -754,7 +754,7 @@ qed auto
lemma coprime_polynomial_factorization:
fixes a1 :: "'b :: {field,factorial_ring_gcd} poly"
fixes a1 :: "'b :: {field_gcd} poly"
assumes irr: "as \<subseteq> {q. irreducible q \<and> monic q}"
and "finite as" and a1: "a1 \<in> as" and a2: "a2 \<in> as" and a1_not_a2: "a1 \<noteq> a2"
shows "coprime a1 a2"
......@@ -1589,7 +1589,7 @@ by (rule exI[of _ 0], rule exI[of _ 1], auto)
lemma coprime_cong_mult_factorization_poly:
fixes f::"'b::{field} poly"
and a b p :: "'c :: {factorial_ring_gcd,field} poly"
and a b p :: "'c :: {field_gcd} poly"
assumes finite_P: "finite P"
and P: "P \<subseteq> {q. irreducible q}"
and p: "\<forall>p\<in>P. [a=b] (mod p)"
......@@ -2723,7 +2723,8 @@ qed
end
lemma not_irreducible_factor_yields_prime_factors:
assumes uf: "u dvd (f :: 'b :: {field,euclidean_ring_gcd} poly)" and fin: "finite P" and fP: "f = \<Prod>P" and P: "P \<subseteq> {q. irreducible q \<and> monic q}"
assumes uf: "u dvd (f :: 'b :: {field_gcd} poly)" and fin: "finite P"
and fP: "f = \<Prod>P" and P: "P \<subseteq> {q. irreducible q \<and> monic q}"
and u: "degree u > 0" "\<not> irreducible u"
shows "\<exists> pi pj. pi \<in> P \<and> pj \<in> P \<and> pi \<noteq> pj \<and> pi dvd u \<and> pj dvd u"
proof -
......
......@@ -16,28 +16,28 @@ imports
begin
lemma cong_add_poly:
"[(a::'b::{factorial_ring_gcd,field} poly) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
"[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
by (fact cong_add)
lemma cong_mult_poly:
"[(a::'b::{field, factorial_ring_gcd} poly) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
"[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
by (fact cong_mult)
lemma cong_mult_self_poly: "[(a::'b::{factorial_ring_gcd,field} poly) * m = 0] (mod m)"
lemma cong_mult_self_poly: "[(a::'b::{field_gcd} poly) * m = 0] (mod m)"
by (fact cong_mult_self_right)
lemma cong_scalar2_poly: "[(a::'b::{field, factorial_ring_gcd} poly)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
lemma cong_scalar2_poly: "[(a::'b::{field_gcd} poly)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
by (fact cong_scalar_left)
lemma cong_sum_poly:
"(\<And>x. x \<in> A \<Longrightarrow> [((f x)::'b::{factorial_ring_gcd,field} poly) = g x] (mod m)) \<Longrightarrow>
"(\<And>x. x \<in> A \<Longrightarrow> [((f x)::'b::{field_gcd} poly) = g x] (mod m)) \<Longrightarrow>
[(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
by (rule cong_sum)
lemma cong_iff_lin_poly: "([(a::'b::{factorial_ring_gcd,field} poly) = b] (mod m)) = (\<exists>k. b = a + m * k)"
lemma cong_iff_lin_poly: "([(a::'b::{field_gcd} poly) = b] (mod m)) = (\<exists>k. b = a + m * k)"
using cong_diff_iff_cong_0 [of b a m] by (auto simp add: cong_0_iff dvd_def algebra_simps dest: cong_sym)
lemma cong_solve_poly: "(a::'b::{normalization_euclidean_semiring, factorial_ring_gcd,field} poly) \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)"
lemma cong_solve_poly: "(a::'b::{field_gcd} poly) \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)"
proof (cases "n = 0")
case True
note n0=True
......@@ -63,7 +63,7 @@ qed
lemma cong_solve_coprime_poly:
assumes coprime_an:"coprime (a::'b::{normalization_euclidean_semiring, factorial_ring_gcd,field} poly) n"
assumes coprime_an:"coprime (a::'b::{field_gcd} poly) n"
shows "\<exists>x. [a * x = 1] (mod n)"
proof (cases "a = 0")
case True
......@@ -78,12 +78,12 @@ next
qed
lemma cong_dvd_modulus_poly:
"[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" for x y :: "'b::{factorial_ring_gcd,field} poly"
"[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" for x y :: "'b::{field_gcd} poly"
by (auto simp add: cong_iff_lin_poly elim!: dvdE)
lemma chinese_remainder_aux_poly:
fixes A :: "'a set"
and m :: "'a \<Rightarrow> 'b::{normalization_euclidean_semiring,factorial_ring_gcd,field} poly"
and m :: "'a \<Rightarrow> 'b::{field_gcd} poly"
assumes fin: "finite A"
and cop: "\<forall>i \<in> A. (\<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
shows "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
......@@ -108,7 +108,7 @@ qed
(*The Chinese Remainder Theorem for polynomials: *)
lemma chinese_remainder_poly:
fixes A :: "'a set"
and m :: "'a \<Rightarrow> 'b::{normalization_euclidean_semiring,factorial_ring_gcd,field} poly"
and m :: "'a \<Rightarrow> 'b::{field_gcd} poly"
and u :: "'a \<Rightarrow> 'b poly"
assumes fin: "finite A"
and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
......@@ -157,27 +157,27 @@ qed
(*********************** Now we try to prove the uniqueness **********************)
lemma cong_trans_poly:
"[(a::'b::{factorial_ring_gcd,field} poly) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
"[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
by (fact cong_trans)
lemma cong_mod_poly: "(n::'b::{factorial_ring_gcd,field} poly) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
lemma cong_mod_poly: "(n::'b::{field_gcd} poly) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
by auto
lemma cong_sym_poly: "[(a::'b::{factorial_ring_gcd,field} poly) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
lemma cong_sym_poly: "[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
by (fact cong_sym)
lemma cong_1_poly: "[(a::'b::{factorial_ring_gcd,field} poly) = b] (mod 1)"
lemma cong_1_poly: "[(a::'b::{field_gcd} poly) = b] (mod 1)"
by (fact cong_1)
lemma coprime_cong_mult_poly:
assumes "[(a::'b::{factorial_ring_gcd,field} poly) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
assumes "[(a::'b::{field_gcd} poly) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
shows "[a = b] (mod m * n)"
using divides_mult assms
by (metis (no_types, hide_lams) cong_dvd_modulus_poly cong_iff_lin_poly dvd_mult2 dvd_refl minus_add_cancel mult.right_neutral)
lemma coprime_cong_prod_poly:
"(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<Longrightarrow>
(\<forall>i\<in>A. [(x::'b::{factorial_ring_gcd,field} poly) = y] (mod m i)) \<Longrightarrow>
(\<forall>i\<in>A. [(x::'b::{field_gcd} poly) = y] (mod m i)) \<Longrightarrow>
[x = y] (mod (\<Prod>i\<in>A. m i))"
apply (induct A rule: infinite_finite_induct)
apply auto
......@@ -185,13 +185,13 @@ lemma coprime_cong_prod_poly:
done
lemma cong_less_modulus_unique_poly:
"[(x::'b::{factorial_ring_gcd,field} poly) = y] (mod m) \<Longrightarrow> degree x < degree m \<Longrightarrow> degree y < degree m \<Longrightarrow> x = y"
"[(x::'b::{field_gcd} poly) = y] (mod m) \<Longrightarrow> degree x < degree m \<Longrightarrow> degree y < degree m \<Longrightarrow> x = y"
by (simp add: cong_def mod_poly_less)
lemma chinese_remainder_unique_poly:
fixes A :: "'a set"
and m :: "'a \<Rightarrow> 'b::{normalization_euclidean_semiring,factorial_ring_gcd,field} poly"
and m :: "'a \<Rightarrow> 'b::{field_gcd} poly"
and u :: "'a \<Rightarrow> 'b poly"
assumes nz: "\<forall>i\<in>A. (m i) \<noteq> 0"
and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
......
......@@ -19,7 +19,8 @@ declare [[code abort: dummy_Gcd]]
lemma dummy_Gcd_Lcm: "Gcd x = dummy_Gcd x" "Lcm x = dummy_Lcm x"
unfolding dummy_Gcd_def dummy_Lcm_def by auto
lemmas dummy_Gcd_Lcm_poly [code] = dummy_Gcd_Lcm [where ?'a = "'a :: factorial_ring_gcd poly"]
lemmas dummy_Gcd_Lcm_poly [code] = dummy_Gcd_Lcm
[where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"]
lemmas dummy_Gcd_Lcm_int [code] = dummy_Gcd_Lcm [where ?'a = int]
lemmas dummy_Gcd_Lcm_nat [code] = dummy_Gcd_Lcm [where ?'a = nat]
......
......@@ -224,7 +224,7 @@ proof (intro allI conjI impI notI)
from sf[OF _ this] 0 nzq show False by simp
qed
lemma gcd_reflect_poly: fixes f :: "'a :: factorial_ring_gcd poly"
lemma gcd_reflect_poly: fixes f :: "'a :: {factorial_ring_gcd, semiring_gcd_mult_normalize} poly"
assumes nz: "coeff f 0 \<noteq> 0" "coeff g 0 \<noteq> 0"
shows "gcd (reflect_poly f) (reflect_poly g) = normalize (reflect_poly (gcd f g))"
proof (rule sym, rule gcdI)
......
......@@ -14,7 +14,8 @@ imports
begin
(*TODO: Move*)
interpretation content_hom: monoid_mult_hom "content::'a::factorial_semiring_gcd poly \<Rightarrow> _"
interpretation content_hom: monoid_mult_hom
"content::'a::{factorial_semiring, semiring_gcd, normalization_semidom_multiplicative} poly \<Rightarrow> _"
by (unfold_locales, auto simp: content_mult)
lemma prod_dvd_1_imp_all_dvd_1:
......
......@@ -320,6 +320,19 @@ definition Lcm_mod_ring :: "'a mod_ring set \<Rightarrow> 'a mod_ring" where "Lc
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)
......
......@@ -25,7 +25,7 @@ begin
lemma uniqueness_poly_equality:
fixes f g :: "'a :: factorial_ring_gcd poly"
fixes f g :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
assumes cop: "coprime f g"
and deg: "B = 0 \<or> degree B < degree f" "B' = 0 \<or> degree B' < degree f"
and f: "f \<noteq> 0" and eq: "A * f + B * g = A' * f + B' * g"
......@@ -89,7 +89,7 @@ proof -
show "B = 0 \<or> degree B < degree D" using deg unfolding B .
qed
lemma dupe_monic_unique: fixes D :: "'a :: factorial_ring_gcd poly"
lemma dupe_monic_unique: fixes D :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
assumes 1: "D*S + H*T = 1"
and mon: "monic D"
and dupe: "dupe_monic D H S T U = (A,B)"
......
......@@ -91,7 +91,7 @@ lemma yun_wrel_minus: assumes "yun_wrel F c f" "yun_wrel G c g"
using assms unfolding yun_wrel_def by (auto simp: smult_diff_right hom_distribs)
lemma gcd_smult_left: assumes "c \<noteq> 0"
shows "gcd (smult c f) g = gcd f (g :: 'b :: {field, factorial_ring_gcd} poly)"
shows "gcd (smult c f) g = gcd f (g :: 'b :: {field_gcd} poly)"
proof -
from assms have "normalize c = 1"
by (meson dvd_field_iff is_unit_normalize)
......@@ -99,7 +99,7 @@ proof -
by (metis (no_types) Polynomial.normalize_smult gcd.commute gcd.left_commute gcd_left_idem gcd_self smult_1_left)
qed
lemma gcd_smult_right: "c \<noteq> 0 \<Longrightarrow> gcd f (smult c g) = gcd f (g :: 'b :: {field, factorial_ring_gcd} poly)"
lemma gcd_smult_right: "c \<noteq> 0 \<Longrightarrow> gcd f (smult c g) = gcd f (g :: 'b :: {field_gcd} poly)"
using gcd_smult_left[of c g f] by (simp add: gcd.commute)
lemma gcd_rat_to_gcd_int: "gcd (of_int_poly f :: rat poly) (of_int_poly g) =
......
......@@ -911,18 +911,22 @@ sublocale as_ufd: ufd
proof(unfold_locales, goal_cases)
case (1 x)
from prime_factorization_exists[OF \<open>x \<noteq> 0\<close>]
obtain F where f: "\<And>f. f \<in># F \<Longrightarrow> prime_elem f" and Fx: "prod_mset F = normalize x" by auto
from Fx have x: "x = unit_factor x * prod_mset F" by auto
obtain F where f: "\<And>f. f \<in># F \<Longrightarrow> prime_elem f"
and Fx: "normalize (prod_mset F) = normalize x" by auto
from associatedE2[OF Fx] obtain u where u: "is_unit u" "x = u * prod_mset F"
by blast
from \<open>\<not> is_unit x\<close> Fx have "F \<noteq> {#}" by auto
then obtain g G where F: "F = add_mset g G" by (cases F, auto)
then have "g \<in># F" by auto
with f[OF this]prime_elem_iff_irreducible
irreducible_mult_unit_left[OF unit_factor_is_unit[OF \<open>x \<noteq> 0\<close>]]
have g: "irreducible (unit_factor x * g)" by auto
have g: "irreducible (u * g)" using u(1)
by (subst irreducible_mult_unit_left) simp_all
show ?case
proof (intro exI conjI mset_factorsI)
from x show "prod_mset (add_mset (unit_factor x * g) G) = x" by (simp add: F ac_simps)
fix f assume "f \<in># add_mset (unit_factor x * g) G"
show "prod_mset (add_mset (u * g) G) = x"
using \<open>x \<noteq> 0\<close> by (simp add: F ac_simps u)
fix f assume "f \<in># add_mset (u * g) G"
with f[unfolded F] g prime_elem_iff_irreducible
show "irreducible f" by auto
qed auto
......@@ -933,17 +937,21 @@ next
have "list_all2 (ddvd) fs (map normalize fs)" by (intro list_all2_all_nthI, auto)
then have FH: "rel_mset (ddvd) F (image_mset normalize F)" by (unfold rel_mset_def F, force)
also
have FG: "image_mset normalize F = image_mset normalize G"
proof (intro prime_factorization_unique')
from 2 have xF: "x = prod_mset F" and xG: "x = prod_mset G" by auto
from xF have "normalize x = prod_mset (image_mset normalize F)" by (simp add: local.normalize_prod_mset)
with xG have nFG: "\<dots> = prod_mset (image_mset normalize G)" by (simp_all add: local.normalize_prod_mset)
then show "(\<Prod>i\<in>#image_mset normalize F. i) = (\<Prod>i\<in>#image_mset normalize G. i)" by auto
from 2 prime_elem_iff_irreducible have "f \<in># F \<Longrightarrow> prime_elem f" "g \<in># G \<Longrightarrow> prime_elem g" for f g
by (auto intro: prime_elemI)
then show " Multiset.Ball (image_mset normalize F) prime"
"Multiset.Ball (image_mset normalize G) prime" by auto
qed
have FG: "image_mset normalize F = image_mset normalize G"
proof (intro prime_factorization_unique'')
from 2 have xF: "x = prod_mset F" and xG: "x = prod_mset G" by auto
from xF have "normalize x = normalize (prod_mset (image_mset normalize F))"
by (simp add: normalize_prod_mset_normalize)
with xG have nFG: "\<dots> = normalize (prod_mset (image_mset normalize G))"
by (simp_all add: normalize_prod_mset_normalize)
then show "normalize (\<Prod>i\<in>#image_mset normalize F. i) =
normalize (\<Prod>i\<in>#image_mset normalize G. i)" by auto
next
from 2 prime_elem_iff_irreducible have "f \<in># F \<Longrightarrow> prime_elem f" "g \<in># G \<Longrightarrow> prime_elem g" for f g
by (auto intro: prime_elemI)
then show " Multiset.Ball (image_mset normalize F) prime"
"Multiset.Ball (image_mset normalize G) prime" by auto
qed
also
obtain gs where G: "G = mset gs" by (metis ex_mset)
have "list_all2 ((ddvd)\<inverse>\<inverse>) gs (map normalize gs)" by (intro list_all2_all_nthI, auto)
......
......@@ -46,6 +46,18 @@ instance
by (standard, simp_all add: gcd_fract_def lcm_fract_def Gcd_fract_def Lcm_fract_def)
end
(*field + unique_euclidean_ring + euclidean_ring_gcd + normalization_semidom_multiplicative*)
instantiation fract :: (idom) unique_euclidean_ring
begin
definition [simp]: "division_segment_fract (x :: 'a fract) = (1 :: 'a fract)"
instance by standard (auto split: if_splits)
end
instance fract :: (idom) field_gcd by standard auto
definition divides_ff :: "'a::idom fract \<Rightarrow> 'a fract \<Rightarrow> bool"
where "divides_ff x y \<equiv> \<exists> r. y = x * to_fract r"
......
......@@ -69,7 +69,7 @@ proof (rule poly_eqI)
qed
lemma lead_coeff_gcd_field:
fixes p q::"'a::{field,semidom_divide_unit_factor,factorial_ring_gcd} poly"
fixes p q::"'a::field_gcd poly"
assumes "p\<noteq>0 \<or> q\<noteq>0"
shows "lead_coeff (gcd p q) = 1"
using assms by (metis gcd.normalize_idem gcd_eq_0_iff lead_coeff_normalize_field)
......@@ -363,7 +363,7 @@ lemma proots_within_times:
unfolding proots_within_def by auto
lemma proots_within_gcd:
fixes s::"'a::factorial_ring_gcd set"
fixes s::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize} set"
shows "proots_within (gcd p q) s= proots_within p s \<inter> proots_within q s"
unfolding proots_within_def
by (auto simp add: poly_eq_0_iff_dvd)
......
......@@ -234,7 +234,7 @@ next
qed
lemma rsquarefree_gcd_pderiv:
fixes p::"'a::{factorial_ring_gcd,semiring_char_0} poly"
fixes p::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize,semiring_char_0} poly"
assumes "p\<noteq>0"
shows "rsquarefree (p div (gcd p (pderiv p)))"
proof (cases "pderiv p = 0")
......@@ -276,7 +276,7 @@ next
qed
lemma poly_gcd_pderiv_iff:
fixes p::"'a::{semiring_char_0,factorial_ring_gcd} poly"
fixes p::"'a::{semiring_char_0,factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
shows "poly (p div (gcd p (pderiv p))) x =0 \<longleftrightarrow> poly p x=0"
proof (cases "pderiv p=0")
case True
......
......@@ -262,7 +262,7 @@ proof
with A normalize_eq_0_iff[of a] normalize_eq_0_iff[of b] have "a = 0" "b = 0" by auto
thus ?thesis by (auto intro!: exI[of _ 1] simp: Units_def)
qed
qed (auto simp: normalize_Units normalize_mult)
qed (auto simp: normalize_Units Units_def)
end
......@@ -347,10 +347,15 @@ lemma ass_function_0:
lemma ass_function_0':
assumes r: "ass_function ass"
shows "(ass x div x = 0) = (x=0)"
using assms unfolding ass_function_def pairwise_def
by (metis ass_function_0 associatedD2 div_self div_by_0 dvd_normalize_div
normalize_0 normalize_1 one_neq_zero r)
proof safe
assume *: "ass x div x = 0"
from r have **: "normalize (ass x) = normalize x"
by (simp add: ass_function_def)
from associatedD2[OF this] have "x dvd ass x"
by simp
with * ** show "x = 0"
by (auto simp: dvd_div_eq_0_iff)
qed auto
lemma res_function_Complete_set_residues:
assumes f: "res_function f"
......
......@@ -953,7 +953,7 @@ definition det_int :: "int mat \<Rightarrow> int" where
lemma det_int[simp]: "det_int = det"
by (intro ext, auto simp: det_int_def)
definition det_field_poly :: "'a :: {field,euclidean_ring_gcd} poly mat \<Rightarrow> 'a poly" where
definition det_field_poly :: "'a :: {field,field_gcd} poly mat \<Rightarrow> 'a poly" where
"det_field_poly A = det_code (select_min degree) gcd_mute_fun A"
lemma det_field_poly[simp]: "det_field_poly = det"
......
......@@ -766,7 +766,7 @@ proof -
qed
lemma primitive_part_neg [simp]:
fixes a::"'a :: factorial_ring_gcd poly"
fixes a::"'a :: {factorial_ring_gcd,factorial_semiring_multiplicative} poly"
shows "primitive_part (-a) = - primitive_part a"
proof -
have "primitive_part (-a) = primitive_part (smult (-1) a)" by auto
......
......@@ -150,7 +150,7 @@ proof (induction A rule: infinite_finite_induct)
qed auto
lemma is_factorization_of_order:
fixes p :: "'a :: {field,factorial_ring_gcd} poly"
fixes p :: "'a :: field_gcd poly"
assumes "p \<noteq> 0"
assumes "is_factorization_of (a, fctrs) p"
assumes "(c, n) \<in> set fctrs"
......
......@@ -268,7 +268,7 @@ definition
in ratfps_of_poly p / ratfps_of_poly q)"
lemma lhr_fps_correct:
fixes f :: "nat \<Rightarrow> 'a :: {field_char_0,factorial_ring_gcd}"
fixes f :: "nat \<Rightarrow> 'a :: {field_char_0,field_gcd}"
assumes "linear_homogenous_recurrence f cs fs"
shows "fps_of_ratfps (lhr_fps cs fs) = Abs_fps f"
proof -
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment