diff --git a/metadata/entries/Perfect_Fields.toml b/metadata/entries/Perfect_Fields.toml
--- a/metadata/entries/Perfect_Fields.toml
+++ b/metadata/entries/Perfect_Fields.toml
@@ -1,45 +1,45 @@
title = "Perfect Fields"
date = 2023-11-06
topics = [
"Mathematics/Algebra",
]
abstract = """
This entry provides a type class for perfect fields.
A perfect field K can be characterized by one of the following equivalent conditions:
- Any irreducible polynomial p is separable, i.e. gcd(p,p') = 1, or, equivalently, p' non-zero.
- Either the characteristic of K is 0 or p > 0 and the Frobenius endomorphism is surjective (i.e. every element of K has a p-th root).
We define perfect fields using the second characterization and show the equivalence to the first characterization.
The implication ``2 => 1'' is relatively straightforward using the injectivity of the Frobenius homomorphism.
Examples for perfect fields are:
- any field of characteristic 0 (e.g. the reals or complex numbers)
- any finite field (i.e. Fq for q=pn, n > 0 and p prime)
-- any algebraically closed field (for example the formal Puiseux series over finite fields)
+- any algebraically closed field
"""
license = "bsd"
note = ""
[authors]
[authors.eberl]
email = "eberl_email"
[authors.kreuzer]
email = "kreuzer_email"
[contributors]
[notify]
eberl = "eberl_email"
kreuzer = "kreuzer_email"
[history]
[extra]
[related]
dois = []
pubs = []
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,353 +1,429 @@
(*
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..Finite Fields\
text \When the domain is prime, the ring becomes a field\
class prime_card = assumes prime_card: "prime (CARD('a))"
begin
lemma prime_card_int: "prime (int (CARD('a)))" using prime_card by auto
subclass nontriv using prime_card prime_gt_1_nat by (intro_classes,auto)
end
instance bool :: prime_card
by standard auto
instantiation mod_ring :: (prime_card) field
begin
definition inverse_mod_ring :: "'a mod_ring \ '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
+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
+
+
+text \
+ The following Material was contributed by Manuel Eberl
+\
+instance mod_ring :: (prime_card) finite_field
+ by standard simp_all
+
+instantiation mod_ring :: (prime_card) enum_finite_field
+begin
+
+definition enum_finite_field_mod_ring :: "nat \ 'a mod_ring" where
+ "enum_finite_field_mod_ring n = of_int_mod_ring (int n)"
+
+instance proof
+ interpret type_definition "Rep_mod_ring :: 'a mod_ring \ int" Abs_mod_ring "{0.. = (Abs_mod_ring ` \ :: 'a mod_ring set)"
+ by (intro image_cong refl) (auto simp: of_int_mod_ring_def)
+ also have "\ = (UNIV :: 'a mod_ring set)"
+ using Abs_image by simp
+ finally show "enum_finite_field ` {.. nat" Abs_ring_char ?A
+ by (rule type_definition_ring_char)
+ from card show ?thesis
+ by auto
+qed
+
+instance ring_char :: (semiring_prime_char) nontriv
+proof
+ show "CARD('a ring_char) > 1"
+ using prime_nat_iff by auto
+qed
+
+instance ring_char :: (semiring_prime_char) prime_card
+proof
+ from CARD_ring_char show "prime CARD('a ring_char)"
+ by auto
+qed
+
+lemma to_int_mod_ring_add:
+ "to_int_mod_ring (x + y :: 'a :: finite mod_ring) = (to_int_mod_ring x + to_int_mod_ring y) mod CARD('a)"
+ by transfer auto
+
+lemma to_int_mod_ring_mult:
+ "to_int_mod_ring (x * y :: 'a :: finite mod_ring) = (to_int_mod_ring x * to_int_mod_ring y) mod CARD('a)"
+ by transfer auto
+
+lemma of_nat_mod_CHAR [simp]: "of_nat (x mod CHAR('a :: semiring_1)) = (of_nat x :: 'a)"
+ by (metis (no_types, opaque_lifting) comm_monoid_add_class.add_0 div_mod_decomp
+ mult_zero_right of_nat_CHAR of_nat_add of_nat_mult)
+
+lemma of_int_mod_CHAR [simp]: "of_int (x mod int CHAR('a :: ring_1)) = (of_int x :: 'a)"
+ by (simp add: of_int_eq_iff_cong_CHAR)
+
+end
diff --git a/thys/Formal_Puiseux_Series/Formal_Puiseux_Series.thy b/thys/Formal_Puiseux_Series/Formal_Puiseux_Series.thy
--- a/thys/Formal_Puiseux_Series/Formal_Puiseux_Series.thy
+++ b/thys/Formal_Puiseux_Series/Formal_Puiseux_Series.thy
@@ -1,1824 +1,1841 @@
(*
File: Formal_Puiseux_Series.thy
Author: Manuel Eberl, TU München
*)
section \Formal Puiseux Series\
theory Formal_Puiseux_Series
imports FPS_Hensel
begin
subsection \Auxiliary facts and definitions\
lemma div_dvd_self:
fixes a b :: "'a :: {semidom_divide}"
shows "b dvd a \ a div b dvd a"
by (elim dvdE; cases "b = 0") simp_all
lemma quotient_of_int [simp]: "quotient_of (of_int n) = (n, 1)"
using Rat.of_int_def quotient_of_int by auto
lemma of_int_div_of_int_in_Ints_iff:
"(of_int n / of_int m :: 'a :: field_char_0) \ \ \ m = 0 \ m dvd n"
proof
assume *: "(of_int n / of_int m :: 'a) \ \"
{
assume "m \ 0"
from * obtain k where k: "(of_int n / of_int m :: 'a) = of_int k"
by (auto elim!: Ints_cases)
hence "of_int n = (of_int k * of_int m :: 'a)"
using \m \ 0\ by (simp add: field_simps)
also have "\ = of_int (k * m)"
by simp
finally have "n = k * m"
by (subst (asm) of_int_eq_iff)
hence "m dvd n" by auto
}
thus "m = 0 \ m dvd n" by blast
qed auto
lemma rat_eq_quotientD:
assumes "r = rat_of_int a / rat_of_int b" "b \ 0"
shows "fst (quotient_of r) dvd a" "snd (quotient_of r) dvd b"
proof -
define a' b' where "a' = fst (quotient_of r)" and "b' = snd (quotient_of r)"
define d where "d = gcd a b"
have "b' > 0"
by (auto simp: b'_def quotient_of_denom_pos')
have "coprime a' b'"
by (rule quotient_of_coprime[of r]) (simp add: a'_def b'_def)
have r: "r = rat_of_int a' / rat_of_int b'"
by (simp add: a'_def b'_def quotient_of_div)
from assms \b' > 0\ have "rat_of_int (a' * b) = rat_of_int (a * b')"
unfolding of_int_mult by (simp add: field_simps r)
hence eq: "a' * b = a * b'"
by (subst (asm) of_int_eq_iff)
have "a' dvd a * b'"
by (simp flip: eq)
hence "a' dvd a"
by (subst (asm) coprime_dvd_mult_left_iff) fact
moreover have "b' dvd a' * b"
by (simp add: eq)
hence "b' dvd b"
by (subst (asm) coprime_dvd_mult_right_iff) (use \coprime a' b'\ in \simp add: coprime_commute\)
ultimately show "fst (quotient_of r) dvd a" "snd (quotient_of r) dvd b"
unfolding a'_def b'_def by blast+
qed
lemma quotient_of_denom_add_dvd:
"snd (quotient_of (x + y)) dvd snd (quotient_of x) * snd (quotient_of y)"
proof -
define a b where "a = fst (quotient_of x)" and "b = snd (quotient_of x)"
define c d where "c = fst (quotient_of y)" and "d = snd (quotient_of y)"
have "b > 0" "d > 0"
by (auto simp: b_def d_def quotient_of_denom_pos')
have xy: "x = rat_of_int a / rat_of_int b" "y = rat_of_int c / rat_of_int d"
unfolding a_def b_def c_def d_def by (simp_all add: quotient_of_div)
show "snd (quotient_of (x + y)) dvd b * d"
proof (rule rat_eq_quotientD)
show "x + y = rat_of_int (a * d + c * b) / rat_of_int (b * d)"
using \b > 0\ \d > 0\ by (simp add: field_simps xy)
qed (use \b > 0\ \d > 0\ in auto)
qed
lemma quotient_of_denom_diff_dvd:
"snd (quotient_of (x - y)) dvd snd (quotient_of x) * snd (quotient_of y)"
using quotient_of_denom_add_dvd[of x "-y"]
by (simp add: rat_uminus_code Let_def case_prod_unfold)
definition supp :: "('a \ ('b :: zero)) \ 'a set" where
"supp f = f -` (-{0})"
lemma supp_0 [simp]: "supp (\_. 0) = {}"
and supp_const: "supp (\_. c) = (if c = 0 then {} else UNIV)"
and supp_singleton [simp]: "c \ 0 \ supp (\x. if x = d then c else 0) = {d}"
by (auto simp: supp_def)
lemma supp_uminus [simp]: "supp (\x. -f x :: 'a :: group_add) = supp f"
by (auto simp: supp_def)
subsection \Definition\
text \
Similarly to formal power series $R[[X]]$ and formal Laurent series $R((X))$, we define the ring
of formal Puiseux series $R\{\{X\}\}$ as functions from the rationals into a ring such that
\<^enum> the support is bounded from below, and
\<^enum> the denominators of the numbers in the support have a common multiple other than 0
One can also think of a formal Puiseux series in the paramter $X$ as a formal Laurent series
in the parameter $X^{1/d}$ for some positive integer $d$. This is often written in the
following suggestive notation:
\[ R\{\{X\}\} = \bigcup_{d\geq 1} R((X^{1/d})) \]
Many operations will be defined in terms of this correspondence between Puiseux and Laurent
series, and many of the simple properties proven that way.
\
definition is_fpxs :: "(rat \ 'a :: zero) \ bool" where
"is_fpxs f \ bdd_below (supp f) \ (LCM r\supp f. snd (quotient_of r)) \ 0"
typedef (overloaded) 'a fpxs = "{f::rat \ 'a :: zero. is_fpxs f}"
morphisms fpxs_nth Abs_fpxs
by (rule exI[of _ "\_. 0"]) (auto simp: is_fpxs_def supp_def)
setup_lifting type_definition_fpxs
lemma fpxs_ext: "(\r. fpxs_nth f r = fpxs_nth g r) \ f = g"
by transfer auto
lemma fpxs_eq_iff: "f = g \ (\r. fpxs_nth f r = fpxs_nth g r)"
by transfer auto
lift_definition fpxs_supp :: "'a :: zero fpxs \ rat set" is supp .
lemma fpxs_supp_altdef: "fpxs_supp f = {x. fpxs_nth f x \ 0}"
by transfer (auto simp: supp_def)
text \
The following gives us the ``root order'' of \f\i, i.e. the smallest positive integer \d\
such that \f\ is in $R((X^{1/p}))$.
\
lift_definition fpxs_root_order :: "'a :: zero fpxs \ nat" is
"\f. nat (LCM r\supp f. snd (quotient_of r))" .
lemma fpxs_root_order_pos [simp]: "fpxs_root_order f > 0"
proof transfer
fix f :: "rat \ 'a" assume f: "is_fpxs f"
hence "(LCM r\supp f. snd (quotient_of r)) \ 0"
by (auto simp: is_fpxs_def)
moreover have "(LCM r\supp f. snd (quotient_of r)) \ 0"
by simp
ultimately show "nat (LCM r\supp f. snd (quotient_of r)) > 0"
by linarith
qed
lemma fpxs_root_order_nonzero [simp]: "fpxs_root_order f \ 0"
using fpxs_root_order_pos[of f] by linarith
text \
Let \d\ denote the root order of a Puiseux series \f\, i.e. the smallest number \d\ such that
all monomials with non-zero coefficients can be written in the form $X^{n/d}$ for some \n\.
Then \f\ can be written as a Laurent series in \X^{1/d}\. The following operation gives us
this Laurent series.
\
lift_definition fls_of_fpxs :: "'a :: zero fpxs \ 'a fls" is
"\f n. f (of_int n / of_int (LCM r\supp f. snd (quotient_of r)))"
proof -
fix f :: "rat \ 'a"
assume f: "is_fpxs f"
hence "bdd_below (supp f)"
by (auto simp: is_fpxs_def)
then obtain r0 where "\x\supp f. r0 \ x"
by (auto simp: bdd_below_def)
hence r0: "f x = 0" if "x < r0" for x
using that by (auto simp: supp_def vimage_def)
define d :: int where "d = (LCM r\supp f. snd (quotient_of r))"
have "d \ 0" by (simp add: d_def)
moreover have "d \ 0"
using f by (auto simp: d_def is_fpxs_def)
ultimately have "d > 0" by linarith
have *: "f (of_int n / of_int d) = 0" if "n < \r0 * of_int d\" for n
proof -
have "rat_of_int n < r0 * rat_of_int d"
using that by linarith
thus ?thesis
using \d > 0\ by (intro r0) (auto simp: field_simps)
qed
have "eventually (\n. n > -\r0 * of_int d\) at_top"
by (rule eventually_gt_at_top)
hence "eventually (\n. f (of_int (-n) / of_int d) = 0) at_top"
by (eventually_elim) (rule *, auto)
hence "eventually (\n. f (of_int (-int n) / of_int d) = 0) at_top"
by (rule eventually_compose_filterlim) (rule filterlim_int_sequentially)
thus "eventually (\n. f (of_int (-int n) / of_int d) = 0) cofinite"
by (simp add: cofinite_eq_sequentially)
qed
lemma fls_nth_of_fpxs:
"fls_nth (fls_of_fpxs f) n = fpxs_nth f (of_int n / of_nat (fpxs_root_order f))"
by transfer simp
subsection \Basic algebraic typeclass instances\
instantiation fpxs :: (zero) zero
begin
lift_definition zero_fpxs :: "'a fpxs" is "\r::rat. 0 :: 'a"
by (auto simp: is_fpxs_def supp_def)
instance ..
end
instantiation fpxs :: ("{one, zero}") one
begin
lift_definition one_fpxs :: "'a fpxs" is "\r::rat. if r = 0 then 1 else 0 :: 'a"
by (cases "(1 :: 'a) = 0") (auto simp: is_fpxs_def cong: if_cong)
instance ..
end
lemma fls_of_fpxs_0 [simp]: "fls_of_fpxs 0 = 0"
by transfer auto
lemma fpxs_nth_0 [simp]: "fpxs_nth 0 r = 0"
by transfer auto
lemma fpxs_nth_1: "fpxs_nth 1 r = (if r = 0 then 1 else 0)"
by transfer auto
lemma fpxs_nth_1': "fpxs_nth 1 0 = 1" "r \ 0 \ fpxs_nth 1 r = 0"
by (auto simp: fpxs_nth_1)
instantiation fpxs :: (monoid_add) monoid_add
begin
lift_definition plus_fpxs :: "'a fpxs \ 'a fpxs \ 'a fpxs" is
"\f g x. f x + g x"
proof -
fix f g :: "rat \ 'a"
assume fg: "is_fpxs f" "is_fpxs g"
show "is_fpxs (\x. f x + g x)"
unfolding is_fpxs_def
proof
have supp: "supp (\x. f x + g x) \ supp f \ supp g"
by (auto simp: supp_def)
show "bdd_below (supp (\x. f x + g x))"
by (rule bdd_below_mono[OF _ supp]) (use fg in \auto simp: is_fpxs_def\)
have "(LCM r\supp (\x. f x + g x). snd (quotient_of r)) dvd
(LCM r\supp f \ supp g. snd (quotient_of r))"
by (intro Lcm_subset image_mono supp)
also have "\ = lcm (LCM r\supp f. snd (quotient_of r)) (LCM r\supp g. snd (quotient_of r))"
unfolding image_Un Lcm_Un ..
finally have "(LCM r\supp (\x. f x + g x). snd (quotient_of r)) dvd
lcm (LCM r\supp f. snd (quotient_of r)) (LCM r\supp g. snd (quotient_of r))" .
moreover have "lcm (LCM r\supp f. snd (quotient_of r)) (LCM r\supp g. snd (quotient_of r)) \ 0"
using fg by (auto simp: is_fpxs_def)
ultimately show "(LCM r\supp (\