diff --git a/thys/Formal_Puiseux_Series/FPS_Hensel.thy b/thys/Formal_Puiseux_Series/FPS_Hensel.thy new file mode 100644 --- /dev/null +++ b/thys/Formal_Puiseux_Series/FPS_Hensel.thy @@ -0,0 +1,442 @@ +(* + File: FPS_Hensel.thy + Author: Manuel Eberl, TU München +*) +section \Hensel's lemma for formal power series\ +theory FPS_Hensel + imports "HOL-Computational_Algebra.Computational_Algebra" Puiseux_Polynomial_Library +begin + +text \ + The following proof of Hensel's lemma for formal power series follows the book + ``Algebraic Geometry for Scientists and Engineers'' by Abhyankar~\cite[p.~90--92]{abhyankar1990}. +\ + +definition fps_poly_swap1 :: "'a :: zero fps poly \ 'a poly fps" where + "fps_poly_swap1 p = Abs_fps (\m. Abs_poly (\n. fps_nth (coeff p n) m))" + +lemma coeff_fps_nth_fps_poly_swap1 [simp]: + "coeff (fps_nth (fps_poly_swap1 p) m) n = fps_nth (coeff p n) m" +proof - + have "\\<^sub>\n. poly.coeff p n = 0" + using MOST_coeff_eq_0 by blast + hence "\\<^sub>\n. poly.coeff p n $ m = 0" + by eventually_elim auto + thus ?thesis + by (simp add: fps_poly_swap1_def poly.Abs_poly_inverse) +qed + +definition fps_poly_swap2 :: "'a :: zero poly fps \ 'a fps poly" where + "fps_poly_swap2 p = Abs_poly (\m. Abs_fps (\n. coeff (fps_nth p n) m))" + +lemma fps_nth_coeff_fps_poly_swap2: + assumes "\n. degree (fps_nth p n) \ d" + shows "fps_nth (coeff (fps_poly_swap2 p) m) n = coeff (fps_nth p n) m" +proof - + have "\\<^sub>\n. n > d" + using MOST_nat by blast + hence "\\<^sub>\n. (\m. poly.coeff (p $ m) n) = (\_. 0)" + by eventually_elim (auto simp: fun_eq_iff intro!: coeff_eq_0 le_less_trans[OF assms(1)]) + hence ev: "\\<^sub>\n. Abs_fps (\m. poly.coeff (p $ m) n) = 0" + by eventually_elim (simp add: fps_zero_def) + + have "fps_nth (coeff (fps_poly_swap2 p) m) n = + poly.coeff (Abs_poly (\m. Abs_fps (\n. poly.coeff (p $ n) m))) m $ n" + by (simp add: fps_poly_swap2_def) + also have "\ = Abs_fps (\n. poly.coeff (p $ n) m) $ n" + using ev by (subst poly.Abs_poly_inverse) auto + finally show "fps_nth (coeff (fps_poly_swap2 p) m) n = coeff (fps_nth p n) m" + by simp +qed + +lemma degree_fps_poly_swap2_le: + assumes "\n. degree (fps_nth p n) \ d" + shows "degree (fps_poly_swap2 p) \ d" +proof (safe intro!: degree_le) + fix n assume "n > d" + show "poly.coeff (fps_poly_swap2 p) n = 0" + proof (rule fps_ext) + fix m + have "poly.coeff (fps_poly_swap2 p) n $ m = poly.coeff (p $ m) n" + by (subst fps_nth_coeff_fps_poly_swap2[OF assms]) auto + also have "\ = 0" + by (intro coeff_eq_0 le_less_trans[OF assms \n > d\]) + finally show "poly.coeff (fps_poly_swap2 p) n $ m = 0 $ m" + by simp + qed +qed + +lemma degree_fps_poly_swap2_eq: + assumes "\n. degree (fps_nth p n) \ d" + assumes "d > 0 \ fps_nth p n \ 0" + assumes "degree (fps_nth p n) = d" + shows "degree (fps_poly_swap2 p) = d" +proof (rule antisym) + have "fps_nth (coeff (fps_poly_swap2 p) d) n = poly.coeff (fps_nth p n) d" + by (subst fps_nth_coeff_fps_poly_swap2[OF assms(1)]) auto + also have "\ \ 0" + using assms(2,3) by force + finally have "coeff (fps_poly_swap2 p) d \ 0" + by force + thus "degree (fps_poly_swap2 p) \ d" + using le_degree by blast +next + show "degree (fps_poly_swap2 p) \ d" + by (intro degree_fps_poly_swap2_le) fact +qed + +definition reduce_fps_poly :: "'a :: zero fps poly \ 'a poly" where + "reduce_fps_poly F = fps_nth (fps_poly_swap1 F) 0" + +lemma + fixes F :: "'a :: field fps poly" + assumes "lead_coeff F = 1" + shows degree_reduce_fps_poly_monic: "degree (reduce_fps_poly F) = degree F" + and reduce_fps_poly_monic: "lead_coeff (reduce_fps_poly F) = 1" +proof - + have eq1: "coeff (reduce_fps_poly F) (degree F) = 1" + unfolding reduce_fps_poly_def by (simp add: assms) + have eq2: "coeff (reduce_fps_poly F) n = 0" if "n > degree F" for n + unfolding reduce_fps_poly_def using that by (simp add: coeff_eq_0) + + have "degree (reduce_fps_poly F) \ degree F" + by (rule degree_le) (auto simp: eq2) + moreover have "degree (reduce_fps_poly F) \ degree F" + by (rule le_degree) (simp add: eq1) + from eq1 eq2 show "degree (reduce_fps_poly F) = degree F" + by (intro antisym le_degree degree_le) auto + with eq1 show "lead_coeff (reduce_fps_poly F) = 1" + by simp +qed + +locale fps_hensel_aux = + fixes F :: "'a :: field_gcd poly fps" + fixes g h :: "'a poly" + assumes coprime: "coprime g h" and deg_g: "degree g > 0" and deg_h: "degree h > 0" +begin + +context + fixes g' h' :: "'a poly" + defines "h' \ fst (bezout_coefficients g h)" and "g' \ snd (bezout_coefficients g h)" +begin + +fun hensel_fpxs_aux :: "nat \ 'a poly \ 'a poly" where + "hensel_fpxs_aux n = (if n = 0 then (g, h) else + (let + U = fps_nth F n - + (\(i,j) | i < n \ j < n \ i + j = n. fst (hensel_fpxs_aux i) * snd (hensel_fpxs_aux j)) + in (U * g' + g * ((U * h') div h), (U * h') mod h)))" + +lemmas [simp del] = hensel_fpxs_aux.simps + +lemma hensel_fpxs_aux_0 [simp]: "hensel_fpxs_aux 0 = (g, h)" + by (subst hensel_fpxs_aux.simps) auto + +definition hensel_fpxs1 :: "'a poly fps" + where "hensel_fpxs1 = Abs_fps (fst \ hensel_fpxs_aux)" + +definition hensel_fpxs2 :: "'a poly fps" + where "hensel_fpxs2 = Abs_fps (snd \ hensel_fpxs_aux)" + +lemma hensel_fpxs1_0 [simp]: "hensel_fpxs1 $ 0 = g" + by (simp add: hensel_fpxs1_def) + +lemma hensel_fpxs2_0 [simp]: "hensel_fpxs2 $ 0 = h" + by (simp add: hensel_fpxs2_def) + +theorem fps_hensel_aux: + defines "f \ fps_nth F 0" + assumes "f = g * h" + assumes "\n>0. degree (fps_nth F n) < degree f" + defines "G \ hensel_fpxs1" and "H \ hensel_fpxs2" + shows "F = G * H" "fps_nth G 0 = g" "fps_nth H 0 = h" + "\n>0. degree (fps_nth G n) < degree g" + "\n>0. degree (fps_nth H n) < degree h" +proof - + show "fps_nth G 0 = g" "fps_nth H 0 = h" + by (simp_all add: G_def H_def hensel_fpxs1_def hensel_fpxs2_def) + + have deg_f: "degree f = degree g + degree h" + unfolding \f = g * h\ using assms by (intro degree_mult_eq) auto + + have deg_H: "degree (fps_nth H n) < degree h" if \n > 0\ for n + proof (cases "snd (hensel_fpxs_aux n) = 0") + case False + thus ?thesis + using deg_h \n > 0\ + by (auto simp: hensel_fpxs_aux.simps[of n] hensel_fpxs2_def H_def intro: degree_mod_less') + qed (use assms deg_h in \auto simp: hensel_fpxs2_def\) + thus "\n>0. degree (fps_nth H n) < degree h" + by blast + + have *: "fps_nth F n = fps_nth (G * H) n \ (n > 0 \ degree (fps_nth G n) < degree g)" for n + proof (induction n rule: less_induct) + case (less n) + have fin: "finite {p. fst p < n \ snd p < n \ fst p + snd p = n}" + by (rule finite_subset[of _ "{..n} \ {..n}"]) auto + show ?case + proof (cases "n = 0") + case True + thus ?thesis using assms + by (auto simp: hensel_fpxs1_def hensel_fpxs2_def) + next + case False + define U where "U = fps_nth F n - + (\(i,j) | i < n \ j < n \ i + j = n. fst (hensel_fpxs_aux i) * snd (hensel_fpxs_aux j))" + define g'' h'' where "g'' = U * g'" and "h'' = U * h'" + + have "fps_nth (G * H) n = + (\i=0..n. fst (hensel_fpxs_aux i) * snd (hensel_fpxs_aux (n - i)))" + using assms by (auto simp: hensel_fpxs1_def hensel_fpxs2_def fps_mult_nth) + also have "\ = (\(i,j) | i + j = n. fst (hensel_fpxs_aux i) * snd (hensel_fpxs_aux j))" + by (rule sum.reindex_bij_witness[of _ fst "\i. (i, n - i)"]) auto + also have "{(i,j). i + j = n} = {(i,j). i < n \ j < n \ i + j = n} \ {(n,0), (0,n)}" + by auto + also have "(\(i,j)\\. fst (hensel_fpxs_aux i) * snd (hensel_fpxs_aux j)) = + fps_nth F n - U + (fst (hensel_fpxs_aux n) * h + g * snd (hensel_fpxs_aux n))" + using False fin by (subst sum.union_disjoint) (auto simp: case_prod_unfold U_def) + also have eq: "fst (hensel_fpxs_aux n) * h + g * snd (hensel_fpxs_aux n) = U" + proof - + have "fst (hensel_fpxs_aux n) * h + g * snd (hensel_fpxs_aux n) = + (g'' + g * (h'' div h)) * h + g * (h'' mod h)" + using False by (simp add: hensel_fpxs_aux.simps[of n] U_def g''_def h''_def) + also have "h'' mod h = h'' - (h'' div h) * h" + by (simp add: minus_div_mult_eq_mod) + also have "(g'' + g * (h'' div h)) * h + g * (h'' - h'' div h * h) = g * h'' + g'' * h" + by (simp add: algebra_simps) + also have "\ = U * (h' * g + g' * h)" + by (simp add: algebra_simps g''_def h''_def) + also have "h' * g + g' * h = gcd g h" + unfolding g'_def h'_def by (rule bezout_coefficients_fst_snd) + also have "gcd g h = 1" + using coprime by simp + finally show ?thesis by simp + qed + finally have "fps_nth F n = fps_nth (G * H) n" by simp + + have "degree (G $ n) < degree g" + proof (cases "G $ n = 0") + case False + have "degree (G $ n) + degree h = degree (G $ n * h)" + using False assms by (intro degree_mult_eq [symmetric]) auto + also from eq have "fps_nth G n * h = U - g * snd (hensel_fpxs_aux n)" + by (simp add: algebra_simps G_def hensel_fpxs1_def) + hence "degree (fps_nth G n * h) = degree (U - g * snd (hensel_fpxs_aux n))" + by (simp only: ) + also have "\ < degree f" + proof (intro degree_diff_less) + have "degree (g * snd (local.hensel_fpxs_aux n)) \ + degree g + degree (snd (local.hensel_fpxs_aux n))" + by (intro degree_mult_le) + also have "degree (snd (local.hensel_fpxs_aux n)) < degree h" + using deg_H[of n] \n \ 0\ by (auto simp: H_def hensel_fpxs2_def) + also have "degree g + degree h = degree f" + by (subst deg_f) auto + finally show "degree (g * snd (local.hensel_fpxs_aux n)) < degree f" + by simp + next + show "degree U < degree f" + unfolding U_def + proof (intro degree_diff_less degree_sum_less) + show "degree (F $ n) < degree f" + using \n \ 0\ assms by auto + next + show "degree f > 0" + unfolding deg_f using deg_g by simp + next + fix z assume z: "z \ {(i, j). i < n \ j < n \ i + j = n}" + have "degree (case z of (i, j) \ fst (hensel_fpxs_aux i) * snd (hensel_fpxs_aux j)) = + degree (fps_nth G (fst z) * fps_nth H (snd z))" (is "?lhs = _") + by (simp add: case_prod_unfold G_def H_def hensel_fpxs1_def hensel_fpxs2_def) + also have "\ \ degree (fps_nth G (fst z)) + degree (fps_nth H (snd z))" + by (intro degree_mult_le) + also have "\ < degree g + degree h" + using z less.IH[of "fst z"] + by (intro add_strict_mono deg_H) (simp_all add: case_prod_unfold) + finally show "?lhs < degree f" + by (simp add: deg_f) + qed + qed + finally show ?thesis + by (simp add: deg_f) + qed (use deg_g in auto) + + with \fps_nth F n = fps_nth (G * H) n\ show ?thesis + by blast + qed + qed + + from * show "F = G * H" and "\n>0. degree (fps_nth G n) < degree g" + by (auto simp: fps_eq_iff) +qed + +end + +end + + +locale fps_hensel = + fixes F :: "'a :: field_gcd fps poly" and f g h :: "'a poly" + assumes monic: "lead_coeff F = 1" + defines "f \ reduce_fps_poly F" + assumes f_splits: "f = g * h" + assumes coprime: "coprime g h" and deg_g: "degree g > 0" and deg_h: "degree h > 0" +begin + +definition F' where "F' = fps_poly_swap1 F" + +sublocale fps_hensel_aux F' g h + by unfold_locales (fact deg_g deg_h coprime)+ + + +definition G where + "G = fps_poly_swap2 hensel_fpxs1" + +definition H where + "H = fps_poly_swap2 hensel_fpxs2" + +lemma deg_f: "degree f = degree F" +proof (intro antisym) + have "coeff f (degree F) \ 0" + using monic by (simp add: f_def reduce_fps_poly_def) + thus "degree f \ (degree F)" + by (rule le_degree) +next + have "coeff f n = 0" if "n > degree F" for n + using that by (simp add: f_def reduce_fps_poly_def coeff_eq_0) + thus "degree f \ degree F" + using degree_le by blast +qed + +lemma + F_splits: "F = G * H" and + reduce_G: "reduce_fps_poly G = g" and + reduce_H: "reduce_fps_poly H = h" and + deg_G: "degree G = degree g" and + deg_H: "degree H = degree h" and + lead_coeff_G: "lead_coeff G = fps_const (lead_coeff g)" and + lead_coeff_H: "lead_coeff H = fps_const (lead_coeff h)" +proof - + from deg_g deg_h have [simp]: "g \ 0" "h \ 0" + by auto + define N where "N = degree F" + + have deg_f: "degree f = N" + proof (intro antisym) + have "coeff f N \ 0" + using monic by (simp add: f_def reduce_fps_poly_def N_def) + thus "degree f \ N" + by (rule le_degree) + next + have "coeff f n = 0" if "n > N" for n + using that by (simp add: f_def reduce_fps_poly_def N_def coeff_eq_0) + thus "degree f \ N" + using degree_le by blast + qed + + have "F' $ 0 = f" + unfolding F'_def f_def reduce_fps_poly_def .. + have F'0: "F' $ 0 = g * h" + using f_splits by (simp add: F'_def f_def reduce_fps_poly_def) + + have "\n>0. degree (F' $ n) < N" + proof (subst F'_def, intro allI impI degree_lessI) + fix n :: nat + assume n: "n > 0" + show "fps_poly_swap1 F $ n \ 0 \ 0 < N" + using n deg_g deg_h f_splits deg_f by (auto simp: F'0 degree_mult_eq) + fix k + assume k: "k \ N" + have "coeff (F' $ n) k = coeff F k $ n" + unfolding F'_def by simp + also have "\= 0" + using monic \n > 0\ k by (cases "k > N") (auto simp: N_def coeff_eq_0) + finally show "coeff (fps_poly_swap1 F $ n) k = 0" + by (simp add: F'_def) + qed + hence degs_less: "\n>0. degree (F' $ n) < degree (F' $ 0)" + by (simp add: \F' $ 0 = f\ deg_f) + note hensel = fps_hensel_aux[OF F'0 degs_less] + + have deg_less1: "degree (hensel_fpxs1 $ n) < degree g" if "n > 0" for n + using hensel(4) that by (simp add: F'_def) + have deg_le1: "degree (hensel_fpxs1 $ n) \ degree g" for n + proof (cases "n = 0") + case True + hence "hensel_fpxs1 $ n = g" + by (simp add: hensel_fpxs1_def) + thus ?thesis by simp + qed (auto intro: less_imp_le deg_less1 simp: f_def) + + have deg_less2: "degree (hensel_fpxs2 $ n) < degree h" if "n > 0" for n + using hensel(5) that by (simp add: F'_def) + have deg_le2: "degree (hensel_fpxs2 $ n) \ degree h" for n + proof (cases "n = 0") + case True + hence "hensel_fpxs2 $ n = h" + by (simp add: hensel_fpxs2_def) + thus ?thesis by simp + qed (auto intro: less_imp_le deg_less2 simp: f_def) + + show "F = G * H" + unfolding poly_eq_iff fps_eq_iff + proof safe + fix n k + have "poly.coeff F n $ k = poly.coeff (F' $ k) n" + unfolding F'_def by simp + also have "F' = hensel_fpxs1 * hensel_fpxs2" + by (rule hensel) + also have "\ $ k = (\i=0..k. hensel_fpxs1 $ i * hensel_fpxs2 $ (k - i))" + unfolding fps_mult_nth .. + also have "poly.coeff \ n = + (\i=0..k. \j\n. coeff (hensel_fpxs1 $ i) j * coeff (hensel_fpxs2 $ (k - i)) (n - j))" + by (simp add: coeff_sum coeff_mult) + also have "(\i j. coeff (hensel_fpxs1 $ i) j) = (\i j. coeff G j $ i)" + unfolding G_def + by (subst fps_nth_coeff_fps_poly_swap2[OF deg_le1]) (auto simp: F'_def) + also have "(\i j. coeff (hensel_fpxs2 $ i) j) = (\i j. coeff H j $ i)" + unfolding H_def + by (subst fps_nth_coeff_fps_poly_swap2[OF deg_le2]) (auto simp: F'_def) + also have "(\i=0..k. \j\n. poly.coeff G j $ i * poly.coeff H (n - j) $ (k - i)) = + (\j\n. \i=0..k. poly.coeff G j $ i * poly.coeff H (n - j) $ (k - i))" + by (rule sum.swap) + also have "\ = poly.coeff (G * H) n $ k" + by (simp add: coeff_mult fps_mult_nth fps_sum_nth) + finally show "poly.coeff F n $ k = poly.coeff (G * H) n $ k" . + qed + + show "reduce_fps_poly G = g" unfolding G_def reduce_fps_poly_def poly_eq_iff + by (auto simp: fps_nth_coeff_fps_poly_swap2[OF deg_le1]) + show "reduce_fps_poly H = h" unfolding H_def reduce_fps_poly_def poly_eq_iff + by (auto simp: fps_nth_coeff_fps_poly_swap2[OF deg_le2]) + show "degree G = degree g" unfolding G_def + by (rule degree_fps_poly_swap2_eq[where n = 0] deg_le1 disjI1 deg_g deg_le2)+ simp_all + show "degree H = degree h" unfolding H_def + by (rule degree_fps_poly_swap2_eq[where n = 0] deg_le1 disjI1 deg_h deg_le2)+ simp_all + + show "lead_coeff G = fps_const (lead_coeff g)" + proof (rule fps_ext) + fix n ::nat + have "lead_coeff G $ n = coeff (hensel_fpxs1 $ n) (degree G)" + by (subst G_def, subst fps_nth_coeff_fps_poly_swap2[OF deg_le1]) auto + also have "\ = (if n = 0 then lead_coeff g else 0)" + by (auto simp: \degree G = degree g\ intro: coeff_eq_0 deg_less1) + finally show "lead_coeff G $ n = fps_const (lead_coeff g) $ n" + by simp + qed + + show "lead_coeff H = fps_const (lead_coeff h)" + proof (rule fps_ext) + fix n ::nat + have "lead_coeff H $ n = coeff (hensel_fpxs2 $ n) (degree H)" + by (subst H_def, subst fps_nth_coeff_fps_poly_swap2[OF deg_le2]) auto + also have "\ = (if n = 0 then lead_coeff h else 0)" + by (auto simp: \degree H = degree h\ intro: coeff_eq_0 deg_less2) + finally show "lead_coeff H $ n = fps_const (lead_coeff h) $ n" + by simp + qed +qed + +end + +end \ No newline at end of file diff --git a/thys/Formal_Puiseux_Series/Formal_Puiseux_Series.thy b/thys/Formal_Puiseux_Series/Formal_Puiseux_Series.thy new file mode 100644 --- /dev/null +++ b/thys/Formal_Puiseux_Series/Formal_Puiseux_Series.thy @@ -0,0 +1,1824 @@ +(* + File: Formal_Puiseux_Series.thy + Author: Manuel Eberl, TU München +*) +section \Formal Puiseux Series\ +theory Formal_Puiseux_Series + imports Puiseux_Laurent_Library 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 (\x. f x + g x). snd (quotient_of r)) \ 0" + by auto + qed +qed + +instance + by standard (transfer; simp add: algebra_simps fun_eq_iff)+ + +end + +instance fpxs :: (comm_monoid_add) comm_monoid_add +proof + fix f g :: "'a fpxs" + show "f + g = g + f" + by transfer (auto simp: add_ac) +qed simp_all + +lemma fpxs_nth_add [simp]: "fpxs_nth (f + g) r = fpxs_nth f r + fpxs_nth g r" + by transfer auto + +lift_definition fpxs_of_fls :: "'a :: zero fls \ 'a fpxs" is + "\f r. if r \ \ then f \r\ else 0" +proof - + fix f :: "int \ 'a" + assume "eventually (\n. f (-int n) = 0) cofinite" + hence "eventually (\n. f (-int n) = 0) at_top" + by (simp add: cofinite_eq_sequentially) + then obtain N where N: "f (-int n) = 0" if "n \ N" for n + by (auto simp: eventually_at_top_linorder) + + show "is_fpxs (\r. if r \ \ then f \r\ else 0)" + unfolding is_fpxs_def + proof + have "bdd_below {-(of_nat N::rat)..}" + by simp + moreover have "supp (\r::rat. if r \ \ then f \r\ else 0) \ {-of_nat N..}" + proof + fix r :: rat assume "r \ supp (\r. if r \ \ then f \r\ else 0)" + then obtain m where [simp]: "r = of_int m" "f m \ 0" + by (auto simp: supp_def elim!: Ints_cases split: if_splits) + have "m \ -int N" + using N[of "nat (-m)"] by (cases "m \ 0"; cases "-int N \ m") (auto simp: le_nat_iff) + thus "r \ {-of_nat N..}" by simp + qed + ultimately show "bdd_below (supp (\r::rat. if r \ \ then f \r\ else 0))" + by (rule bdd_below_mono) + next + have "(LCM r\supp (\r. if r \ \ then f \r\ else 0). snd (quotient_of r)) dvd 1" + by (intro Lcm_least) (auto simp: supp_def elim!: Ints_cases split: if_splits) + thus "(LCM r\supp (\r. if r \ \ then f \r\ else 0). snd (quotient_of r)) \ 0" + by (intro notI) simp + qed +qed + +instantiation fpxs :: (group_add) group_add +begin + +lift_definition uminus_fpxs :: "'a fpxs \ 'a fpxs" is "\f x. -f x" + by (auto simp: is_fpxs_def) + +definition minus_fpxs :: "'a fpxs \ 'a fpxs \ 'a fpxs" where + "minus_fpxs f g = f + (-g)" + +instance proof + fix f :: "'a fpxs" + show "-f + f = 0" + by transfer auto +qed (auto simp: minus_fpxs_def) + +end + +lemma fpxs_nth_uminus [simp]: "fpxs_nth (-f) r = -fpxs_nth f r" + by transfer auto + +lemma fpxs_nth_minus [simp]: "fpxs_nth (f - g) r = fpxs_nth f r - fpxs_nth g r" + unfolding minus_fpxs_def fpxs_nth_add fpxs_nth_uminus by simp + +lemma fpxs_of_fls_eq_iff [simp]: "fpxs_of_fls f = fpxs_of_fls g \ f = g" + by transfer (force simp: fun_eq_iff Ints_def) + +lemma fpxs_of_fls_0 [simp]: "fpxs_of_fls 0 = 0" + by transfer auto + +lemma fpxs_of_fls_1 [simp]: "fpxs_of_fls 1 = 1" + by transfer (auto simp: fun_eq_iff elim!: Ints_cases) + +lemma fpxs_of_fls_add [simp]: "fpxs_of_fls (f + g) = fpxs_of_fls f + fpxs_of_fls g" + by transfer (auto simp: fun_eq_iff elim!: Ints_cases) + +lemma fps_to_fls_sum [simp]: "fps_to_fls (sum f A) = (\x\A. fps_to_fls (f x))" + by (induction A rule: infinite_finite_induct) auto + +lemma fpxs_of_fls_sum [simp]: "fpxs_of_fls (sum f A) = (\x\A. fpxs_of_fls (f x))" + by (induction A rule: infinite_finite_induct) auto + +lemma fpxs_nth_of_fls: + "fpxs_nth (fpxs_of_fls f) r = (if r \ \ then fls_nth f \r\ else 0)" + by transfer auto + +lemma fpxs_of_fls_eq_0_iff [simp]: "fpxs_of_fls f = 0 \ f = 0" + using fpxs_of_fls_eq_iff[of f 0] by (simp del: fpxs_of_fls_eq_iff) + +lemma fpxs_of_fls_eq_1_iff [simp]: "fpxs_of_fls f = 1 \ f = 1" + using fpxs_of_fls_eq_iff[of f 1] by (simp del: fpxs_of_fls_eq_iff) + +lemma fpxs_root_order_of_fls [simp]: "fpxs_root_order (fpxs_of_fls f) = 1" +proof (transfer, goal_cases) + case (1 f) + have "supp (\r. if r \ \ then f \r\ else 0) = rat_of_int ` {n. f n \ 0}" + by (force simp: supp_def Ints_def) + also have "(LCM r\\. snd (quotient_of r)) = nat (LCM x\{n. f n \ 0}. 1)" + by (simp add: image_image) + also have "\ = 1" + by simp + also have "nat 1 = 1" + by simp + finally show ?case . +qed + + + +subsection \The substitution $X \mapsto X^r$\ + +text \ + This operation turns a formal Puiseux series $f(X)$ into $f(X^r)$, where + $r$ can be any positive rational number: +\ +lift_definition fpxs_compose_power :: "'a :: zero fpxs \ rat \ 'a fpxs" is + "\f r x. if r > 0 then f (x / r) else 0" +proof - + fix f :: "rat \ 'a" and r :: rat + assume f: "is_fpxs f" + have "is_fpxs (\x. f (x / r))" if "r > 0" + unfolding is_fpxs_def + proof + define r' where "r' = inverse r" + have "r' > 0" + using \r > 0\ by (auto simp: r'_def) + have "(\x. x / r') ` supp f = supp (\x. f (x * r'))" + using \r' > 0\ by (auto simp: supp_def image_iff vimage_def field_simps) + hence eq: "(\x. x * r) ` supp f = supp (\x. f (x / r))" + using \r > 0\ by (simp add: r'_def field_simps) + + from f have "bdd_below (supp f)" + by (auto simp: is_fpxs_def) + hence "bdd_below ((\x. x * r) ` supp f)" + using \r > 0\ by (intro bdd_below_image_mono) (auto simp: mono_def divide_right_mono) + also note eq + finally show "bdd_below (supp (\x. f (x / r)))" . + + define a b where "a = fst (quotient_of r)" and "b = snd (quotient_of r)" + have "b > 0" by (simp add: b_def quotient_of_denom_pos') + have [simp]: "quotient_of r = (a, b)" + by (simp add: a_def b_def) + have "r = of_int a / of_int b" + by (simp add: quotient_of_div) + with \r > 0\ and \b > 0\ have \a > 0\ + by (simp add: field_simps) + + have "(LCM r\supp (\x. f (x / r)). snd (quotient_of r)) = + (LCM x\supp f. snd (quotient_of (x * r)))" + by (simp add: eq [symmetric] image_image) + also have "\ dvd (LCM x\supp f. snd (quotient_of x) * b)" + using \a > 0\ \b > 0\ + by (intro Lcm_mono) + (simp add: rat_times_code case_prod_unfold Let_def Rat.normalize_def + quotient_of_denom_pos' div_dvd_self) + also have "\ dvd normalize (b * (LCM x\supp f. snd (quotient_of x)))" + proof (cases "supp f = {}") + case False + thus ?thesis using Lcm_mult[of "(\x. snd (quotient_of x)) ` supp f" b] + by (simp add: mult_ac image_image) + qed auto + hence "(LCM x\supp f. snd (quotient_of x) * b) dvd + b * (LCM x\supp f. snd (quotient_of x))" by simp + finally show "(LCM r\supp (\x. f (x / r)). snd (quotient_of r)) \ 0" + using \b > 0\ f by (auto simp: is_fpxs_def) + qed + thus "is_fpxs (\x. if r > 0 then f (x / r) else 0)" + by (cases "r > 0") (auto simp: is_fpxs_def supp_def) +qed + +lemma fpxs_as_fls: + "fpxs_compose_power (fpxs_of_fls (fls_of_fpxs f)) (1 / of_nat (fpxs_root_order f)) = f" +proof (transfer, goal_cases) + case (1 f) + define d where "d = (LCM r\supp f. snd (quotient_of r))" + have "d \ 0" by (simp add: d_def) + moreover have "d \ 0" using 1 by (simp add: is_fpxs_def d_def) + ultimately have "d > 0" by linarith + + have "(if rat_of_int d * x \ \ then f (rat_of_int \rat_of_int d * x\ / rat_of_int d) else 0) = f x" for x + proof (cases "rat_of_int d * x \ \") + case True + then obtain n where n: "rat_of_int d * x = of_int n" + by (auto elim!: Ints_cases) + have "f (rat_of_int \rat_of_int d * x\ / rat_of_int d) = f (rat_of_int n / rat_of_int d)" + by (simp add: n) + also have "rat_of_int n / rat_of_int d = x" + using n \d > 0\ by (simp add: field_simps) + finally show ?thesis + using True by simp + next + case False + have "x \ supp f" + proof + assume "x \ supp f" + hence "snd (quotient_of x) dvd d" + by (simp add: d_def) + hence "rat_of_int (fst (quotient_of x) * d) / rat_of_int (snd (quotient_of x)) \ \" + by (intro of_int_divide_in_Ints) auto + also have "rat_of_int (fst (quotient_of x) * d) / rat_of_int (snd (quotient_of x)) = + rat_of_int d * (rat_of_int (fst (quotient_of x)) / rat_of_int (snd (quotient_of x)))" + by (simp only: of_int_mult mult_ac times_divide_eq_right) + also have "\ = rat_of_int d * x" + by (metis Fract_of_int_quotient Rat_cases normalize_stable prod.sel(1) prod.sel(2) quotient_of_Fract) + finally have "rat_of_int d * x \ \" . + with False show False by contradiction + qed + thus ?thesis using False by (simp add: supp_def) + qed + thus ?case + using \d > 0\ by (simp add: is_fpxs_def d_def mult_ac fun_eq_iff cong: if_cong) +qed + +lemma fpxs_compose_power_0 [simp]: "fpxs_compose_power 0 r = 0" + by transfer simp + +lemma fpxs_compose_power_1 [simp]: "r > 0 \ fpxs_compose_power 1 r = 1" + by transfer (auto simp: fun_eq_iff) + +lemma fls_of_fpxs_eq_0_iff [simp]: "fls_of_fpxs x = 0 \ x = 0" + by (metis fls_of_fpxs_0 fpxs_as_fls fpxs_compose_power_0 fpxs_of_fls_0) + +lemma fpxs_of_fls_compose_power [simp]: + "fpxs_of_fls (fls_compose_power f d) = fpxs_compose_power (fpxs_of_fls f) (of_nat d)" +proof (transfer, goal_cases) + case (1 f d) + show ?case + proof (cases "d = 0") + case False + show ?thesis + proof (intro ext, goal_cases) + case (1 r) + show ?case + proof (cases "r \ \") + case True + then obtain n where [simp]: "r = of_int n" + by (cases r rule: Ints_cases) + show ?thesis + proof (cases "d dvd n") + case True + thus ?thesis by (auto elim!: Ints_cases) + next + case False + hence "rat_of_int n / rat_of_int (int d) \ \" + using \d \ 0\ by (subst of_int_div_of_int_in_Ints_iff) auto + thus ?thesis using False by auto + qed + next + case False + hence "r / rat_of_nat d \ \" + using \d \ 0\ by (auto elim!: Ints_cases simp: field_simps) + thus ?thesis using False by auto + qed + qed + qed auto +qed + +lemma fpxs_compose_power_add [simp]: + "fpxs_compose_power (f + g) r = fpxs_compose_power f r + fpxs_compose_power g r" + by transfer (auto simp: fun_eq_iff) + +lemma fpxs_compose_power_distrib: + "r1 > 0 \ r2 > 0 \ + fpxs_compose_power (fpxs_compose_power f r1) r2 = fpxs_compose_power f (r1 * r2)" + by transfer (auto simp: fun_eq_iff algebra_simps zero_less_mult_iff) + +lemma fpxs_compose_power_divide_right: + "r1 > 0 \ r2 > 0 \ + fpxs_compose_power f (r1 / r2) = fpxs_compose_power (fpxs_compose_power f r1) (inverse r2)" + by (simp add: fpxs_compose_power_distrib field_simps) + +lemma fpxs_compose_power_1_right [simp]: "fpxs_compose_power f 1 = f" + by transfer auto + +lemma fpxs_compose_power_eq_iff [simp]: + assumes "r > 0" + shows "fpxs_compose_power f r = fpxs_compose_power g r \ f = g" + using assms +proof (transfer, goal_cases) + case (1 r f g) + have "f x = g x" if "\x. f (x / r) = g (x / r)" for x + using that[of "x * r"] \r > 0\ by auto + thus ?case using \r > 0\ by (auto simp: fun_eq_iff) +qed + +lemma fpxs_compose_power_eq_1_iff [simp]: + assumes "l > 0" + shows "fpxs_compose_power p l = 1 \ p = 1" +proof - + have "fpxs_compose_power p l = 1 \ fpxs_compose_power p l = fpxs_compose_power 1 l" + by (subst fpxs_compose_power_1) (use assms in auto) + also have "\ \ p = 1" + using assms by (subst fpxs_compose_power_eq_iff) auto + finally show ?thesis . +qed + +lemma fpxs_compose_power_eq_0_iff [simp]: + assumes "r > 0" + shows "fpxs_compose_power f r = 0 \ f = 0" + using fpxs_compose_power_eq_iff[of r f 0] assms by (simp del: fpxs_compose_power_eq_iff) + +lemma fls_of_fpxs_of_fls [simp]: "fls_of_fpxs (fpxs_of_fls f) = f" + using fpxs_as_fls[of "fpxs_of_fls f"] by simp + +lemma fpxs_as_fls': + assumes "fpxs_root_order f dvd d" "d > 0" + obtains f' where "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)" +proof - + define D where "D = fpxs_root_order f" + have "D > 0" + by (auto simp: D_def) + define f' where "f' = fls_of_fpxs f" + from assms obtain d' where d': "d = D * d'" + by (auto simp: D_def) + have "d' > 0" + using assms by (auto intro!: Nat.gr0I simp: d') + define f'' where "f'' = fls_compose_power f' d'" + have "fpxs_compose_power (fpxs_of_fls f'') (1 / of_nat d) = f" + using \D > 0\ \d' > 0\ + by (simp add: d' D_def f''_def f'_def fpxs_as_fls fpxs_compose_power_distrib) + thus ?thesis using that[of f''] by blast +qed + + +subsection \Mutiplication and ring properties\ + +instantiation fpxs :: (comm_semiring_1) comm_semiring_1 +begin + +lift_definition times_fpxs :: "'a fpxs \ 'a fpxs \ 'a fpxs" is + "\f g x. (\(y,z) | y \ supp f \ z \ supp g \ x = y + z. f y * g z)" +proof - + fix f g :: "rat \ 'a" + assume fg: "is_fpxs f" "is_fpxs g" + show "is_fpxs (\x. \(y,z) | y \ supp f \ z \ supp g \ x = y + z. f y * g z)" + (is "is_fpxs ?h") unfolding is_fpxs_def + proof + from fg obtain bnd1 bnd2 where bnds: "\x\supp f. x \ bnd1" "\x\supp g. x \ bnd2" + by (auto simp: is_fpxs_def bdd_below_def) + have "supp ?h \ (\(x,y). x + y) ` (supp f \ supp g)" + proof + fix x :: rat + assume "x \ supp ?h" + have "{(y,z). y \ supp f \ z \ supp g \ x = y + z} \ {}" + proof + assume eq: "{(y,z). y \ supp f \ z \ supp g \ x = y + z} = {}" + hence "?h x = 0" + by (simp only:) auto + with \x \ supp ?h\ show False by (auto simp: supp_def) + qed + thus "x \ (\(x,y). x + y) ` (supp f \ supp g)" + by auto + qed + also have "\ \ {bnd1 + bnd2..}" + using bnds by (auto intro: add_mono) + finally show "bdd_below (supp ?h)" + by auto + next + define d1 where "d1 = (LCM r\supp f. snd (quotient_of r))" + define d2 where "d2 = (LCM r\supp g. snd (quotient_of r))" + have "(LCM r\supp ?h. snd (quotient_of r)) dvd (d1 * d2)" + proof (intro Lcm_least, safe) + fix r :: rat + assume "r \ supp ?h" + hence "(\(y, z) | y \ supp f \ z \ supp g \ r = y + z. f y * g z) \ 0" + by (auto simp: supp_def) + hence "{(y, z). y \ supp f \ z \ supp g \ r = y + z} \ {}" + by (intro notI) simp_all + then obtain y z where yz: "y \ supp f" "z \ supp g" "r = y + z" + by auto + have "snd (quotient_of r) = snd (quotient_of y) * snd (quotient_of z) div + gcd (fst (quotient_of y) * snd (quotient_of z) + + fst (quotient_of z) * snd (quotient_of y)) + (snd (quotient_of y) * snd (quotient_of z))" + by (simp add: \r = _\ rat_plus_code case_prod_unfold Let_def + Rat.normalize_def quotient_of_denom_pos') + also have "\ dvd snd (quotient_of y) * snd (quotient_of z)" + by (metis dvd_def dvd_div_mult_self gcd_dvd2) + also have "\ dvd d1 * d2" + using yz by (auto simp: d1_def d2_def intro!: mult_dvd_mono) + finally show "snd (quotient_of r) dvd d1 * d2" + by (simp add: d1_def d2_def) + qed + moreover have "d1 * d2 \ 0" + using fg by (auto simp: d1_def d2_def is_fpxs_def) + ultimately show "(LCM r\supp ?h. snd (quotient_of r)) \ 0" + by auto + qed +qed + +lemma fpxs_nth_mult: + "fpxs_nth (f * g) r = + (\(y,z) | y \ fpxs_supp f \ z \ fpxs_supp g \ r = y + z. fpxs_nth f y * fpxs_nth g z)" + by transfer simp + +lemma fpxs_compose_power_mult [simp]: + "fpxs_compose_power (f * g) r = fpxs_compose_power f r * fpxs_compose_power g r" +proof (transfer, rule ext, goal_cases) + case (1 f g r x) + show ?case + proof (cases "r > 0") + case True + have "(\x\{(y, z). y \ supp f \ z \ supp g \ x / r = y + z}. + case x of (y, z) \ f y * g z) = + (\x\{(y, z). y \ supp (\x. f (x / r)) \ z \ supp (\x. g (x / r)) \ x = y + z}. + case x of (y, z) \ f (y / r) * g (z / r))" + by (rule sum.reindex_bij_witness[of _ "\(x,y). (x/r,y/r)" "\(x,y). (x*r,y*r)"]) + (use \r > 0\ in \auto simp: supp_def field_simps\) + thus ?thesis + by (auto simp: fun_eq_iff) + qed auto +qed + +lemma fpxs_supp_of_fls: "fpxs_supp (fpxs_of_fls f) = of_int ` supp (fls_nth f)" + by (force simp: fpxs_supp_def fpxs_nth_of_fls supp_def elim!: Ints_cases) + +lemma fpxs_of_fls_mult [simp]: "fpxs_of_fls (f * g) = fpxs_of_fls f * fpxs_of_fls g" +proof (rule fpxs_ext) + fix r :: rat + show "fpxs_nth (fpxs_of_fls (f * g)) r = fpxs_nth (fpxs_of_fls f * fpxs_of_fls g) r" + proof (cases "r \ \") + case True + define h1 where "h1 = (\(x, y). (\x::rat\, \y::rat\))" + define h2 where "h2 = (\(x, y). (of_int x :: rat, of_int y :: rat))" + define df dg where [simp]: "df = fls_subdegree f" "dg = fls_subdegree g" + from True obtain n where [simp]: "r = of_int n" + by (cases rule: Ints_cases) + have "fpxs_nth (fpxs_of_fls f * fpxs_of_fls g) r = + (\(y,z) | y \ fpxs_supp (fpxs_of_fls f) \ z \ fpxs_supp (fpxs_of_fls g) \ rat_of_int n = y + z. + (if y \ \ then fls_nth f \y\ else 0) * (if z \ \ then fls_nth g \z\ else 0))" + by (auto simp: fpxs_nth_mult fpxs_nth_of_fls) + also have "\ = (\(y,z) | y \ supp (fls_nth f) \ z \ supp (fls_nth g) \ n = y + z. + fls_nth f y * fls_nth g z)" + by (rule sum.reindex_bij_witness[of _ h2 h1]) (auto simp: h1_def h2_def fpxs_supp_of_fls) + also have "\ = (\y | y - fls_subdegree g \ supp (fls_nth f) \ fls_subdegree g + n - y \ supp (fls_nth g). + fls_nth f (y - fls_subdegree g) * fls_nth g (fls_subdegree g + n - y))" + by (rule sum.reindex_bij_witness[of _ "\y. (y - fls_subdegree g, fls_subdegree g + n - y)" "\z. fst z + fls_subdegree g"]) + auto + also have "\ = (\i = fls_subdegree f + fls_subdegree g..n. + fls_nth f (i - fls_subdegree g) * fls_nth g (fls_subdegree g + n - i))" + using fls_subdegree_leI[of f] fls_subdegree_leI [of g] + by (intro sum.mono_neutral_left; force simp: supp_def) + also have "\ = fpxs_nth (fpxs_of_fls (f * g)) r" + by (auto simp: fls_times_nth fpxs_nth_of_fls) + finally show ?thesis .. + next + case False + have "fpxs_nth (fpxs_of_fls f * fpxs_of_fls g) r = + (\(y,z) | y \ fpxs_supp (fpxs_of_fls f) \ z \ fpxs_supp (fpxs_of_fls g) \ r = y + z. + (if y \ \ then fls_nth f \y\ else 0) * (if z \ \ then fls_nth g \z\ else 0))" + by (simp add: fpxs_nth_mult fpxs_nth_of_fls) + also have "\ = 0" + using False by (intro sum.neutral ballI) auto + also have "0 = fpxs_nth (fpxs_of_fls (f * g)) r" + using False by (simp add: fpxs_nth_of_fls) + finally show ?thesis .. + qed +qed + +instance proof + show "0 \ (1 :: 'a fpxs)" + by transfer (auto simp: fun_eq_iff) +next + fix f :: "'a fpxs" + show "1 * f = f" + proof (transfer, goal_cases) + case (1 f) + have "{(y, z). y \ supp (\r. if r = 0 then (1::'a) else 0) \ z \ supp f \ x = y + z} = + (if x \ supp f then {(0, x)} else {})" for x + by (auto simp: supp_def split: if_splits) + thus ?case + by (auto simp: fun_eq_iff supp_def) + qed +next + fix f :: "'a fpxs" + show "0 * f = 0" + by transfer (auto simp: fun_eq_iff supp_def) + show "f * 0 = 0" + by transfer (auto simp: fun_eq_iff supp_def) +next + fix f g :: "'a fpxs" + show "f * g = g * f" + proof (transfer, rule ext, goal_cases) + case (1 f g x) + show "(\(y, z)\{(y, z). y \ supp f \ z \ supp g \ x = y + z}. f y * g z) = + (\(y, z)\{(y, z). y \ supp g \ z \ supp f \ x = y + z}. g y * f z)" + by (rule sum.reindex_bij_witness[of _ "\(x,y). (y,x)" "\(x,y). (y,x)"]) + (auto simp: mult_ac) + qed +next + fix f g h :: "'a fpxs" + define d where "d = (LCM F\{f,g,h}. fpxs_root_order F)" + have "d > 0" + by (auto simp: d_def intro!: Nat.gr0I) + obtain f' where f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)" + using fpxs_as_fls'[of f d] \d > 0\ by (auto simp: d_def) + obtain g' where g: "g = fpxs_compose_power (fpxs_of_fls g') (1 / of_nat d)" + using fpxs_as_fls'[of g d] \d > 0\ by (auto simp: d_def) + obtain h' where h: "h = fpxs_compose_power (fpxs_of_fls h') (1 / of_nat d)" + using fpxs_as_fls'[of h d] \d > 0\ by (auto simp: d_def) + show "(f * g) * h = f * (g * h)" + by (simp add: f g h mult_ac + flip: fpxs_compose_power_mult fpxs_compose_power_add fpxs_of_fls_mult) + show "(f + g) * h = f * h + g * h" + by (simp add: f g h ring_distribs + flip: fpxs_compose_power_mult fpxs_compose_power_add fpxs_of_fls_mult fpxs_of_fls_add) +qed + +end + +instance fpxs :: (comm_ring_1) comm_ring_1 + by intro_classes auto + +instance fpxs :: ("{comm_semiring_1,semiring_no_zero_divisors}") semiring_no_zero_divisors +proof + fix f g :: "'a fpxs" + assume fg: "f \ 0" "g \ 0" + define d where "d = lcm (fpxs_root_order f) (fpxs_root_order g)" + have "d > 0" + by (auto simp: d_def intro!: lcm_pos_nat) + obtain f' where f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)" + using fpxs_as_fls'[of f d] \d > 0\ by (auto simp: d_def) + obtain g' where g: "g = fpxs_compose_power (fpxs_of_fls g') (1 / of_nat d)" + using fpxs_as_fls'[of g d] \d > 0\ by (auto simp: d_def) + show "f * g \ 0" + using \d > 0\ fg + by (simp add: f g flip: fpxs_compose_power_mult fpxs_of_fls_mult) +qed + +lemma fpxs_of_fls_power [simp]: "fpxs_of_fls (f ^ n) = fpxs_of_fls f ^ n" + by (induction n) auto + +lemma fpxs_compose_power_power [simp]: + "r > 0 \ fpxs_compose_power (f ^ n) r = fpxs_compose_power f r ^ n" + by (induction n) simp_all + + +subsection \Constant Puiseux series and the series \X\\ + +lift_definition fpxs_const :: "'a :: zero \ 'a fpxs" is + "\c n. if n = 0 then c else 0" +proof - + fix c :: 'a + have "supp (\n::rat. if n = 0 then c else 0) = (if c = 0 then {} else {0})" + by auto + thus "is_fpxs (\n::rat. if n = 0 then c else 0)" + unfolding is_fpxs_def by auto +qed + +lemma fpxs_const_0 [simp]: "fpxs_const 0 = 0" + by transfer auto + +lemma fpxs_const_1 [simp]: "fpxs_const 1 = 1" + by transfer auto + +lemma fpxs_of_fls_const [simp]: "fpxs_of_fls (fls_const c) = fpxs_const c" + by transfer (auto simp: fun_eq_iff Ints_def) + +lemma fls_of_fpxs_const [simp]: "fls_of_fpxs (fpxs_const c) = fls_const c" + by (metis fls_of_fpxs_of_fls fpxs_of_fls_const) + +lemma fls_of_fpxs_1 [simp]: "fls_of_fpxs 1 = 1" + using fls_of_fpxs_const[of 1] by (simp del: fls_of_fpxs_const) + +lift_definition fpxs_X :: "'a :: {one, zero} fpxs" is + "\x. if x = 1 then (1::'a) else 0" + by (cases "1 = (0 :: 'a)") (auto simp: is_fpxs_def cong: if_cong) + +lemma fpxs_const_altdef: "fpxs_const x = fpxs_of_fls (fls_const x)" + by transfer auto + +lemma fpxs_const_add [simp]: "fpxs_const (x + y) = fpxs_const x + fpxs_const y" + by transfer auto + +lemma fpxs_const_mult [simp]: + fixes x y :: "'a::{comm_semiring_1}" + shows "fpxs_const (x * y) = fpxs_const x * fpxs_const y" + unfolding fpxs_const_altdef fls_const_mult_const[symmetric] fpxs_of_fls_mult .. + +lemma fpxs_const_eq_iff [simp]: + "fpxs_const x = fpxs_const y \ x = y" + by transfer (auto simp: fun_eq_iff) + +lemma of_nat_fpxs_eq: "of_nat n = fpxs_const (of_nat n)" + by (induction n) auto + +lemma fpxs_const_uminus [simp]: "fpxs_const (-x) = -fpxs_const x" + by transfer auto + +lemma fpxs_const_diff [simp]: "fpxs_const (x - y) = fpxs_const x - fpxs_const y" + unfolding minus_fpxs_def by transfer auto + +lemma of_int_fpxs_eq: "of_int n = fpxs_const (of_int n)" + by (induction n) (auto simp: of_nat_fpxs_eq) + + +subsection \More algebraic typeclass instances\ + +instance fpxs :: ("{comm_semiring_1,semiring_char_0}") semiring_char_0 +proof + show "inj (of_nat :: nat \ 'a fpxs)" + by (intro injI) (auto simp: of_nat_fpxs_eq) +qed + +instance fpxs :: ("{comm_ring_1,ring_char_0}") ring_char_0 .. + +instance fpxs :: (idom) idom .. + +instantiation fpxs :: (field) field +begin + +definition inverse_fpxs :: "'a fpxs \ 'a fpxs" where + "inverse_fpxs f = + fpxs_compose_power (fpxs_of_fls (inverse (fls_of_fpxs f))) (1 / of_nat (fpxs_root_order f))" + +definition divide_fpxs :: "'a fpxs \ 'a fpxs \ 'a fpxs" where + "divide_fpxs f g = f * inverse g" + +instance proof + fix f :: "'a fpxs" + assume "f \ 0" + define f' where "f' = fls_of_fpxs f" + define d where "d = fpxs_root_order f" + have "d > 0" by (auto simp: d_def) + have f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)" + by (simp add: f'_def d_def fpxs_as_fls) + + have "inverse f * f = fpxs_compose_power (fpxs_of_fls (inverse f')) (1 / of_nat d) * f" + by (simp add: inverse_fpxs_def f'_def d_def) + also have "fpxs_compose_power (fpxs_of_fls (inverse f')) (1 / of_nat d) * f = + fpxs_compose_power (fpxs_of_fls (inverse f' * f')) (1 / of_nat d)" + by (simp add: f) + also have "inverse f' * f' = 1" + using \f \ 0\ \d > 0\ by (simp add: f field_simps) + finally show "inverse f * f = 1" + using \d > 0\ by simp +qed (auto simp: divide_fpxs_def inverse_fpxs_def) + +end + +instance fpxs :: (field_char_0) field_char_0 .. + + +subsection \Valuation\ + +definition fpxs_val :: "'a :: zero fpxs \ rat" where + "fpxs_val f = + of_int (fls_subdegree (fls_of_fpxs f)) / rat_of_nat (fpxs_root_order f)" + +lemma fpxs_val_of_fls [simp]: "fpxs_val (fpxs_of_fls f) = of_int (fls_subdegree f)" + by (simp add: fpxs_val_def) + +lemma fpxs_nth_compose_power [simp]: + assumes "r > 0" + shows "fpxs_nth (fpxs_compose_power f r) n = fpxs_nth f (n / r)" + using assms by transfer auto + +lemma fls_of_fpxs_uminus [simp]: "fls_of_fpxs (-f) = -fls_of_fpxs f" + by transfer auto + +lemma fpxs_root_order_uminus [simp]: "fpxs_root_order (-f) = fpxs_root_order f" + by transfer auto + +lemma fpxs_val_uminus [simp]: "fpxs_val (-f) = fpxs_val f" + unfolding fpxs_val_def by simp + +lemma fpxs_val_minus_commute: "fpxs_val (f - g) = fpxs_val (g - f)" + by (subst fpxs_val_uminus [symmetric]) (simp del: fpxs_val_uminus) + +lemma fpxs_val_const [simp]: "fpxs_val (fpxs_const c) = 0" + by (simp add: fpxs_val_def) + +lemma fpxs_val_1 [simp]: "fpxs_val 1 = 0" + by (simp add: fpxs_val_def) + +lemma of_int_fls_subdegree_of_fpxs: + "rat_of_int (fls_subdegree (fls_of_fpxs f)) = fpxs_val f * of_nat (fpxs_root_order f)" + by (simp add: fpxs_val_def) + +lemma fpxs_nth_val_nonzero: + assumes "f \ 0" + shows "fpxs_nth f (fpxs_val f) \ 0" +proof - + define N where "N = fpxs_root_order f" + define f' where "f' = fls_of_fpxs f" + define M where "M = fls_subdegree f'" + have val: "fpxs_val f = of_int M / of_nat N" + by (simp add: M_def fpxs_val_def N_def f'_def) + have *: "f = fpxs_compose_power (fpxs_of_fls f') (1 / rat_of_nat N)" + by (simp add: fpxs_as_fls N_def f'_def) + also have "fpxs_nth \ (fpxs_val f) = + fpxs_nth (fpxs_of_fls f') (fpxs_val f * rat_of_nat (fpxs_root_order f))" + by (subst fpxs_nth_compose_power) (auto simp: N_def) + also have "\ = fls_nth f' M" + by (subst fpxs_nth_of_fls) (auto simp: val N_def) + also have "f' \ 0" + using * assms by auto + hence "fls_nth f' M \ 0" + unfolding M_def by simp + finally show "fpxs_nth f (fpxs_val f) \ 0" . +qed + +lemma fpxs_nth_below_val: + assumes n: "n < fpxs_val f" + shows "fpxs_nth f n = 0" +proof (cases "f = 0") + case False + define N where "N = fpxs_root_order f" + define f' where "f' = fls_of_fpxs f" + define M where "M = fls_subdegree f'" + have val: "fpxs_val f = of_int M / of_nat N" + by (simp add: M_def fpxs_val_def N_def f'_def) + have *: "f = fpxs_compose_power (fpxs_of_fls f') (1 / rat_of_nat N)" + by (simp add: fpxs_as_fls N_def f'_def) + have "fpxs_nth f n = fpxs_nth (fpxs_of_fls f') (n * rat_of_nat N)" + by (subst *, subst fpxs_nth_compose_power) (auto simp: N_def) + also have "\ = 0" + proof (cases "rat_of_nat N * n \ \") + case True + then obtain n' where n': "of_int n' = rat_of_nat N * n" + by (elim Ints_cases) auto + have "of_int n' < rat_of_nat N * fpxs_val f" + unfolding n' using n by (intro mult_strict_left_mono) (auto simp: N_def) + also have "\ = of_int M" + by (simp add: val N_def) + finally have "n' < M" by linarith + + have "fpxs_nth (fpxs_of_fls f') (rat_of_nat N * n) = fls_nth f' n'" + unfolding n'[symmetric] by (subst fpxs_nth_of_fls) (auto simp: N_def) + also from \n' < M\ have "\ = 0" + unfolding M_def by simp + finally show ?thesis by (simp add: mult_ac) + qed (auto simp: fpxs_nth_of_fls mult_ac) + finally show "fpxs_nth f n = 0" . +qed auto + +lemma fpxs_val_leI: "fpxs_nth f r \ 0 \ fpxs_val f \ r" + using fpxs_nth_below_val[of r f] + by (cases "f = 0"; cases "fpxs_val f" r rule: linorder_cases) auto + +lemma fpxs_val_0 [simp]: "fpxs_val 0 = 0" + by (simp add: fpxs_val_def) + +lemma fpxs_val_geI: + assumes "f \ 0" "\r. r < r' \ fpxs_nth f r = 0" + shows "fpxs_val f \ r'" + using fpxs_nth_val_nonzero[of f] assms by force + +lemma fpxs_val_compose_power [simp]: + assumes "r > 0" + shows "fpxs_val (fpxs_compose_power f r) = fpxs_val f * r" +proof (cases "f = 0") + case [simp]: False + show ?thesis + proof (intro antisym) + show "fpxs_val (fpxs_compose_power f r) \ fpxs_val f * r" + using assms by (intro fpxs_val_leI) (simp add: fpxs_nth_val_nonzero) + next + show "fpxs_val f * r \ fpxs_val (fpxs_compose_power f r)" + proof (intro fpxs_val_geI) + show "fpxs_nth (fpxs_compose_power f r) r' = 0" if "r' < fpxs_val f * r" for r' + unfolding fpxs_nth_compose_power[OF assms] + by (rule fpxs_nth_below_val) (use that assms in \auto simp: field_simps\) + qed (use assms in auto) + qed +qed auto + +lemma fpxs_val_add_ge: + assumes "f + g \ 0" + shows "fpxs_val (f + g) \ min (fpxs_val f) (fpxs_val g)" +proof (rule ccontr) + assume "\(fpxs_val (f + g) \ min (fpxs_val f) (fpxs_val g))" (is "\(?n \ _)") + hence "?n < fpxs_val f" "?n < fpxs_val g" + by auto + hence "fpxs_nth f ?n = 0" "fpxs_nth g ?n = 0" + by (intro fpxs_nth_below_val; simp; fail)+ + hence "fpxs_nth (f + g) ?n = 0" + by simp + moreover have "fpxs_nth (f + g) ?n \ 0" + by (intro fpxs_nth_val_nonzero assms) + ultimately show False by contradiction +qed + +lemma fpxs_val_diff_ge: + assumes "f \ g" + shows "fpxs_val (f - g) \ min (fpxs_val f) (fpxs_val g)" + using fpxs_val_add_ge[of f "-g"] assms by simp + +lemma fpxs_nth_mult_val: + "fpxs_nth (f * g) (fpxs_val f + fpxs_val g) = fpxs_nth f (fpxs_val f) * fpxs_nth g (fpxs_val g)" +proof (cases "f = 0 \ g = 0") + case False + have "{(y, z). y \ fpxs_supp f \ z \ fpxs_supp g \ fpxs_val f + fpxs_val g = y + z} \ + {(fpxs_val f, fpxs_val g)}" + using False fpxs_val_leI[of f] fpxs_val_leI[of g] by (force simp: fpxs_supp_def supp_def) + hence "fpxs_nth (f * g) (fpxs_val f + fpxs_val g) = + (\(y, z)\{(fpxs_val f, fpxs_val g)}. fpxs_nth f y * fpxs_nth g z)" + unfolding fpxs_nth_mult + by (intro sum.mono_neutral_left) (auto simp: fpxs_supp_def supp_def) + thus ?thesis by simp +qed auto + +lemma fpxs_val_mult [simp]: + fixes f g :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs" + assumes "f \ 0" "g \ 0" + shows "fpxs_val (f * g) = fpxs_val f + fpxs_val g" +proof (intro antisym fpxs_val_leI fpxs_val_geI) + fix r :: rat + assume r: "r < fpxs_val f + fpxs_val g" + show "fpxs_nth (f * g) r = 0" + unfolding fpxs_nth_mult using assms fpxs_val_leI[of f] fpxs_val_leI[of g] r + by (intro sum.neutral; force) +qed (use assms in \auto simp: fpxs_nth_mult_val fpxs_nth_val_nonzero\) + +lemma fpxs_val_power [simp]: + fixes f :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs" + assumes "f \ 0 \ n > 0" + shows "fpxs_val (f ^ n) = of_nat n * fpxs_val f" +proof (cases "f = 0") + case False + have [simp]: "f ^ n \ 0" for n + using False by (induction n) auto + thus ?thesis using False + by (induction n) (auto simp: algebra_simps) +qed (use assms in \auto simp: power_0_left\) + +lemma fpxs_nth_power_val [simp]: + fixes f :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs" + shows "fpxs_nth (f ^ r) (rat_of_nat r * fpxs_val f) = fpxs_nth f (fpxs_val f) ^ r" +proof (cases "f \ 0") + case True + show ?thesis + proof (induction r) + case (Suc r) + have "fpxs_nth (f ^ Suc r) (rat_of_nat (Suc r) * fpxs_val f) = + fpxs_nth (f * f ^ r) (fpxs_val f + fpxs_val (f ^ r))" + using True by (simp add: fpxs_nth_mult_val ring_distribs) + also have "\ = fpxs_nth f (fpxs_val f) ^ Suc r" + using Suc True by (subst fpxs_nth_mult_val) auto + finally show ?case . + qed (auto simp: fpxs_nth_1') +next + case False + thus ?thesis + by (cases r) (auto simp: fpxs_nth_1') +qed + + +subsection \Powers of \X\ and shifting\ + +lift_definition fpxs_X_power :: "rat \ 'a :: {zero, one} fpxs" is + "\r n :: rat. if n = r then 1 else (0 :: 'a)" +proof - + fix r :: rat + have "supp (\n. if n = r then 1 else (0 :: 'a)) = (if (1 :: 'a) = 0 then {} else {r})" + by (auto simp: supp_def) + thus "is_fpxs (\n. if n = r then 1 else (0 :: 'a))" + using quotient_of_denom_pos'[of r] by (auto simp: is_fpxs_def) +qed + +lemma fpxs_X_power_0 [simp]: "fpxs_X_power 0 = 1" + by transfer auto + +lemma fpxs_X_power_add: "fpxs_X_power (a + b) = fpxs_X_power a * fpxs_X_power b" +proof (transfer, goal_cases) + case (1 a b) + have *: "{(y,z). y \ supp (\n. if n=a then (1::'a) else 0) \ + z \ supp (\n. if n=b then (1::'a) else 0) \ x=y+z} = + (if x = a + b then {(a, b)} else {})" for x + by (auto simp: supp_def fun_eq_iff) + show ?case + unfolding * by (auto simp: fun_eq_iff case_prod_unfold) +qed + +lemma fpxs_X_power_mult: "fpxs_X_power (rat_of_nat n * m) = fpxs_X_power m ^ n" + by (induction n) (auto simp: ring_distribs fpxs_X_power_add) + +lemma fpxs_of_fls_X_power [simp]: "fpxs_of_fls (fls_shift n 1) = fpxs_X_power (-rat_of_int n)" + by transfer (auto simp: fun_eq_iff Ints_def simp flip: of_int_minus) + +lemma fpxs_X_power_neq_0 [simp]: "fpxs_X_power r \ (0 :: 'a :: zero_neq_one fpxs)" + by transfer (auto simp: fun_eq_iff) + +lemma fpxs_X_power_eq_1_iff [simp]: "fpxs_X_power r = (1 :: 'a :: zero_neq_one fpxs) \ r = 0" + by transfer (auto simp: fun_eq_iff) + + +lift_definition fpxs_shift :: "rat \ 'a :: zero fpxs \ 'a fpxs" is + "\r f n. f (n + r)" +proof - + fix r :: rat and f :: "rat \ 'a" + assume f: "is_fpxs f" + have subset: "supp (\n. f (n + r)) \ (\n. n + r) -` supp f" + by (auto simp: supp_def) + have eq: "(\n. n + r) -` supp f = (\n. n - r) ` supp f" + by (auto simp: image_iff algebra_simps) + + show "is_fpxs (\n. f (n + r))" + unfolding is_fpxs_def + proof + have "bdd_below ((\n. n + r) -` supp f)" + unfolding eq by (rule bdd_below_image_mono) (use f in \auto simp: is_fpxs_def mono_def\) + thus "bdd_below (supp (\n. f (n + r)))" + by (rule bdd_below_mono[OF _ subset]) + next + have "(LCM r\supp (\n. f (n + r)). snd (quotient_of r)) dvd + (LCM r\(\n. n + r) -` supp f. snd (quotient_of r))" + by (intro Lcm_subset image_mono subset) + also have "\ = (LCM x\supp f. snd (quotient_of (x - r)))" + by (simp only: eq image_image o_def) + also have "\ dvd (LCM x\supp f. snd (quotient_of r) * snd (quotient_of x))" + by (subst mult.commute, intro Lcm_mono quotient_of_denom_diff_dvd) + also have "\ = Lcm ((\x. snd (quotient_of r) * x) ` (\x. snd (quotient_of x)) ` supp f)" + by (simp add: image_image o_def) + also have "\ dvd normalize (snd (quotient_of r) * (LCM x\supp f. snd (quotient_of x)))" + proof (cases "supp f = {}") + case False + thus ?thesis by (subst Lcm_mult) auto + qed auto + finally show "(LCM r\supp (\n. f (n + r)). snd (quotient_of r)) \ 0" + using quotient_of_denom_pos'[of r] f by (auto simp: is_fpxs_def) + qed +qed + +lemma fpxs_nth_shift [simp]: "fpxs_nth (fpxs_shift r f) n = fpxs_nth f (n + r)" + by transfer simp_all + +lemma fpxs_shift_0_left [simp]: "fpxs_shift 0 f = f" + by transfer auto + +lemma fpxs_shift_add_left: "fpxs_shift (m + n) f = fpxs_shift m (fpxs_shift n f)" + by transfer (simp_all add: add_ac) + +lemma fpxs_shift_diff_left: "fpxs_shift (m - n) f = fpxs_shift m (fpxs_shift (-n) f)" + by (subst fpxs_shift_add_left [symmetric]) auto + +lemma fpxs_shift_0 [simp]: "fpxs_shift r 0 = 0" + by transfer simp_all + +lemma fpxs_shift_add [simp]: "fpxs_shift r (f + g) = fpxs_shift r f + fpxs_shift r g" + by transfer auto + +lemma fpxs_shift_uminus [simp]: "fpxs_shift r (-f) = -fpxs_shift r f" + by transfer auto + +lemma fpxs_shift_shift_uminus [simp]: "fpxs_shift r (fpxs_shift (-r) f) = f" + by (simp flip: fpxs_shift_add_left) + +lemma fpxs_shift_shift_uminus' [simp]: "fpxs_shift (-r) (fpxs_shift r f) = f" + by (simp flip: fpxs_shift_add_left) + +lemma fpxs_shift_diff [simp]: "fpxs_shift r (f - g) = fpxs_shift r f - fpxs_shift r g" + unfolding minus_fpxs_def by (subst fpxs_shift_add) auto + +lemma fpxs_shift_compose_power [simp]: + "fpxs_shift r (fpxs_compose_power f s) = fpxs_compose_power (fpxs_shift (r / s) f) s" + by transfer (simp_all add: add_divide_distrib add_ac cong: if_cong) + +lemma rat_of_int_div_dvd: "d dvd n \ rat_of_int (n div d) = rat_of_int n / rat_of_int d" + by auto + +lemma fpxs_of_fls_shift [simp]: + "fpxs_of_fls (fls_shift n f) = fpxs_shift (of_int n) (fpxs_of_fls f)" +proof (transfer, goal_cases) + case (1 n f) + show ?case + proof + fix r :: rat + have eq: "r + rat_of_int n \ \ \ r \ \" + by (metis Ints_add Ints_diff Ints_of_int add_diff_cancel_right') + show "(if r \ \ then f (\r\ + n) else 0) = + (if r + rat_of_int n \ \ then f \r + rat_of_int n\ else 0)" + unfolding eq by auto + qed +qed + +lemma fpxs_shift_mult: "f * fpxs_shift r g = fpxs_shift r (f * g)" + "fpxs_shift r f * g = fpxs_shift r (f * g)" +proof - + obtain a b where ab: "r = of_int a / of_nat b" and "b > 0" + by (metis Fract_of_int_quotient of_int_of_nat_eq quotient_of_unique zero_less_imp_eq_int) + + define s where "s = lcm b (lcm (fpxs_root_order f) (fpxs_root_order g))" + have "s > 0" using \b > 0\ + by (auto simp: s_def intro!: Nat.gr0I) + obtain f' where f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / rat_of_nat s)" + using fpxs_as_fls'[of f s] \s > 0\ by (auto simp: s_def) + obtain g' where g: "g = fpxs_compose_power (fpxs_of_fls g') (1 / rat_of_nat s)" + using fpxs_as_fls'[of g s] \s > 0\ by (auto simp: s_def) + + define n where "n = (a * s) div b" + have "b dvd s" + by (auto simp: s_def) + have sr_eq: "r * rat_of_nat s = rat_of_int n" + using \b > 0\ \b dvd s\ + by (simp add: ab field_simps of_rat_divide of_rat_mult n_def rat_of_int_div_dvd) + + show "f * fpxs_shift r g = fpxs_shift r (f * g)" "fpxs_shift r f * g = fpxs_shift r (f * g)" + unfolding f g using \s > 0\ + by (simp_all flip: fpxs_compose_power_mult fpxs_of_fls_mult fpxs_of_fls_shift + add: sr_eq fls_shifted_times_simps mult_ac) +qed + +lemma fpxs_shift_1: "fpxs_shift r 1 = fpxs_X_power (-r)" + by transfer (auto simp: fun_eq_iff) + +lemma fpxs_X_power_conv_shift: "fpxs_X_power r = fpxs_shift (-r) 1" + by (simp add: fpxs_shift_1) + +lemma fpxs_shift_power [simp]: "fpxs_shift n x ^ m = fpxs_shift (of_nat m * n) (x ^ m)" + by (induction m) (simp_all add: algebra_simps fpxs_shift_mult flip: fpxs_shift_add_left) + +lemma fpxs_compose_power_X_power [simp]: + "s > 0 \ fpxs_compose_power (fpxs_X_power r) s = fpxs_X_power (r * s)" + by transfer (simp add: field_simps) + + +subsection \The \n\-th root of a Puiseux series\ + +text \ + In this section, we define the formal root of a Puiseux series. This is done using the + same concept for formal power series. There is still one interesting theorems that is missing + here, e.g.\ the uniqueness (which could probably be lifted over from FPSs) somehow. +\ + +definition fpxs_radical :: "(nat \ 'a :: field_char_0 \ 'a) \ nat \ 'a fpxs \ 'a fpxs" where + "fpxs_radical rt r f = (if f = 0 then 0 else + (let f' = fls_base_factor_to_fps (fls_of_fpxs f); + f'' = fpxs_of_fls (fps_to_fls (fps_radical rt r f')) + in fpxs_shift (-fpxs_val f / rat_of_nat r) + (fpxs_compose_power f'' (1 / rat_of_nat (fpxs_root_order f)))))" + +lemma fpxs_radical_0 [simp]: "fpxs_radical rt r 0 = 0" + by (simp add: fpxs_radical_def) + +lemma + fixes r :: nat + assumes r: "r > 0" + shows fpxs_power_radical: + "rt r (fpxs_nth f (fpxs_val f)) ^ r = fpxs_nth f (fpxs_val f) \ fpxs_radical rt r f ^ r = f" + and fpxs_radical_lead_coeff: + "f \ 0 \ fpxs_nth (fpxs_radical rt r f) (fpxs_val f / rat_of_nat r) = + rt r (fpxs_nth f (fpxs_val f))" +proof - + define q where "q = fpxs_root_order f" + define f' where "f' = fls_base_factor_to_fps (fls_of_fpxs f)" + have [simp]: "fps_nth f' 0 = fpxs_nth f (fpxs_val f)" + by (simp add: f'_def fls_nth_of_fpxs of_int_fls_subdegree_of_fpxs) + define f'' where "f'' = fpxs_of_fls (fps_to_fls (fps_radical rt r f'))" + have eq1: "fls_of_fpxs f = fls_shift (-fls_subdegree (fls_of_fpxs f)) (fps_to_fls f')" + by (subst fls_conv_base_factor_to_fps_shift_subdegree) (simp add: f'_def) + have eq2: "fpxs_compose_power (fpxs_of_fls (fls_of_fpxs f)) (1 / of_nat q) = f" + unfolding q_def by (rule fpxs_as_fls) + also note eq1 + also have "fpxs_of_fls (fls_shift (- fls_subdegree (fls_of_fpxs f)) (fps_to_fls f')) = + fpxs_shift (- (fpxs_val f * rat_of_nat q)) (fpxs_of_fls (fps_to_fls f'))" + by (simp add: of_int_fls_subdegree_of_fpxs q_def) + finally have eq3: "fpxs_compose_power (fpxs_shift (- (fpxs_val f * rat_of_nat q)) + (fpxs_of_fls (fps_to_fls f'))) (1 / rat_of_nat q) = f" . + + { + assume rt: "rt r (fpxs_nth f (fpxs_val f)) ^ r = fpxs_nth f (fpxs_val f)" + show "fpxs_radical rt r f ^ r = f" + proof (cases "f = 0") + case [simp]: False + have "f'' ^ r = fpxs_of_fls (fps_to_fls (fps_radical rt r f' ^ r))" + by (simp add: fps_to_fls_power f''_def) + also have "fps_radical rt r f' ^ r = f'" + using power_radical[of f' rt "r - 1"] r rt by (simp add: fpxs_nth_val_nonzero) + finally have "f'' ^ r = fpxs_of_fls (fps_to_fls f')" . + + have "fpxs_shift (-fpxs_val f / rat_of_nat r) (fpxs_compose_power f'' (1 / of_nat q)) ^ r = + fpxs_shift (-fpxs_val f) (fpxs_compose_power (f'' ^ r) (1 / of_nat q))" + unfolding q_def using r + by (subst fpxs_shift_power, subst fpxs_compose_power_power [symmetric]) simp_all + also have "f'' ^ r = fpxs_of_fls (fps_to_fls f')" + by fact + also have "fpxs_shift (-fpxs_val f) (fpxs_compose_power + (fpxs_of_fls (fps_to_fls f')) (1 / of_nat q)) = f" + using r eq3 by simp + finally show "fpxs_radical rt r f ^ r = f" + by (simp add: fpxs_radical_def f'_def f''_def q_def) + qed (use r in auto) + } + + assume [simp]: "f \ 0" + have "fpxs_nth (fpxs_shift (-fpxs_val f / of_nat r) (fpxs_compose_power f'' (1 / of_nat q))) + (fpxs_val f / of_nat r) = fpxs_nth f'' 0" + using r by (simp add: q_def) + also have "fpxs_shift (-fpxs_val f / of_nat r) (fpxs_compose_power f'' (1 / of_nat q)) = + fpxs_radical rt r f" + by (simp add: fpxs_radical_def q_def f'_def f''_def) + also have "fpxs_nth f'' 0 = rt r (fpxs_nth f (fpxs_val f))" + using r by (simp add: f''_def fpxs_nth_of_fls) + finally show "fpxs_nth (fpxs_radical rt r f) (fpxs_val f / rat_of_nat r) = + rt r (fpxs_nth f (fpxs_val f))" . +qed + +lemma fls_base_factor_power: + fixes f :: "'a::{semiring_1, semiring_no_zero_divisors} fls" + shows "fls_base_factor (f ^ n) = fls_base_factor f ^ n" +proof (cases "f = 0") + case False + have [simp]: "f ^ n \ 0" for n + by (induction n) (use False in auto) + show ?thesis using False + by (induction n) (auto simp: fls_base_factor_mult simp flip: fls_times_both_shifted_simp) +qed (cases n; simp) + +(* TODO: Uniqueness of radical. Also: composition and composition inverse *) + +hide_const (open) supp + + +subsection \Algebraic closedness\ + +text \ + We will now show that the field of formal Puiseux series over an algebraically closed field of + characteristic 0 is again algebraically closed. + + The typeclass constraint \<^class>\field_gcd\ is a technical constraint that mandates that + the field has a (trivial) GCD operation defined on it. It comes from some peculiarities of + Isabelle's typeclass system and can be considered unimportant, since any concrete type of + class \<^class>\field\ can easily be made an instance of \<^class>\field_gcd\. + + It would be possible to get rid of this constraint entirely here, but it is not worth + the effort. + + The proof is a fairly standard one that uses Hensel's lemma. Some preliminary tricks are + required to be able to use it, however, namely a number of non-obvious changes of variables + to turn the polynomial with Puiseux coefficients into one with formal power series coefficients. + The overall approach was taken from an article by Nowak~\cite{nowak2000}. + + Basically, what we need to show is this: Let + \[p(X,Z) = a_n(Z) X^n + a_{n-1}(Z) X^{n-1} + \ldots + a_0(Z)\] + be a polynomial in \X\ of degree at least 2 + with coefficients that are formal Puiseux series in \Z\. Then \p\ is reducible, i.e. it splits + into two non-constant factors. + + Due to work we have already done elsewhere, we may assume here that $a_n = 1$, $a_{n-1} = 0$, and + $a_0 \neq 0$, all of which will come in very useful. +\ + +instance fpxs :: ("{alg_closed_field, field_char_0, field_gcd}") alg_closed_field +proof (rule alg_closedI_reducible_coeff_deg_minus_one_eq_0) + fix p :: "'a fpxs poly" + assume deg_p: "degree p > 1" and lc_p: "lead_coeff p = 1" + assume coeff_deg_minus_1: "coeff p (degree p - 1) = 0" + assume "coeff p 0 \ 0" + define N where "N = degree p" + + text \ + Let $a_0, \ldots, a_n$ be the coefficients of \p\ with $a_n = 1$. Now let \r\ be the maximum of + $-\frac{\text{val}(a_i)}{n-i}$ ranging over all $i < n$ such that $a_i \neq 0$. + \ + define r :: rat + where "r = (MAX i\{i\{.. 0}. + -fpxs_val (poly.coeff p i) / (rat_of_nat N - rat_of_nat i))" + + text \ + We write $r = a / b$ such that all the $a_i$ can be written as Laurent series in + $X^{1/b}$, i.e. the root orders of all the $a_i$ divide $b$: + \ + obtain a b where ab: "b > 0" "r = of_int a / of_nat b" "\i\N. fpxs_root_order (coeff p i) dvd b" + proof - + define b where "b = lcm (nat (snd (quotient_of r))) (LCM i\{..N}. fpxs_root_order (coeff p i))" + define x where "x = b div nat (snd (quotient_of r))" + define a where "a = fst (quotient_of r) * int x" + + show ?thesis + proof (rule that) + show "b > 0" + using quotient_of_denom_pos'[of r] by (auto simp: b_def intro!: Nat.gr0I) + have b_eq: "b = nat (snd (quotient_of r)) * x" + by (simp add: x_def b_def) + have "x > 0" + using b_eq \b > 0\ by (auto intro!: Nat.gr0I) + have "r = rat_of_int (fst (quotient_of r)) / rat_of_int (int (nat (snd (quotient_of r))))" + using quotient_of_denom_pos'[of r] quotient_of_div[of r] by simp + also have "\ = rat_of_int a / rat_of_nat b" + using \x > 0\ by (simp add: a_def b_eq) + finally show "r = rat_of_int a / rat_of_nat b" . + show "\i\N. fpxs_root_order (poly.coeff p i) dvd b" + by (auto simp: b_def) + qed + qed + + text \ + We write all the coefficients of \p\ as Laurent series in $X^{1/b}$: + \ + have "\c. coeff p i = fpxs_compose_power (fpxs_of_fls c) (1 / rat_of_nat b)" if i: "i \ N" for i + proof - + have "fpxs_root_order (coeff p i) dvd b" + using ab(3) i by auto + from fpxs_as_fls'[OF this \b > 0\] show ?thesis by metis + qed + then obtain c_aux where c_aux: + "coeff p i = fpxs_compose_power (fpxs_of_fls (c_aux i)) (1 / rat_of_nat b)" if "i \ N" for i + by metis + define c where "c = (\i. if i \ N then c_aux i else 0)" + have c: "coeff p i = fpxs_compose_power (fpxs_of_fls (c i)) (1 / rat_of_nat b)" for i + using c_aux[of i] by (auto simp: c_def N_def coeff_eq_0) + have c_eq_0 [simp]: "c i = 0" if "i > N" for i + using that by (auto simp: c_def) + have c_eq: "fpxs_of_fls (c i) = fpxs_compose_power (coeff p i) (rat_of_nat b)" for i + using c[of i] \b > 0\ by (simp add: fpxs_compose_power_distrib) + + text \ + We perform another change of variables and multiply with a suitable power of \X\ to turn our + Laurent coefficients into FPS coefficients: + \ + define c' where "c' = (\i. fls_X_intpow ((int N - int i) * a) * c i)" + have "c' N = 1" + using c[of N] \lead_coeff p = 1\ \b > 0\ by (simp add: c'_def N_def) + + have subdegree_c: "of_int (fls_subdegree (c i)) = fpxs_val (coeff p i) * rat_of_nat b" + if i: "i \ N" for i + proof - + have "rat_of_int (fls_subdegree (c i)) = fpxs_val (fpxs_of_fls (c i))" + by simp + also have "fpxs_of_fls (c i) = fpxs_compose_power (poly.coeff p i) (rat_of_nat b)" + by (subst c_eq) auto + also have "fpxs_val \ = fpxs_val (coeff p i) * rat_of_nat b" + using \b > 0\ by simp + finally show ?thesis . + qed + + text \ + We now write all the coefficients as FPSs: + \ + have "\c''. c' i = fps_to_fls c''" if "i \ N" for i + proof (cases "i = N") + case True + hence "c' i = fps_to_fls 1" + using \c' N = 1\ by simp + thus ?thesis by metis + next + case i: False + show ?thesis + proof (cases "c i = 0") + case True + hence "c' i = 0" by (auto simp: c'_def) + thus ?thesis by auto + next + case False + hence "coeff p i \ 0" + using c_eq[of i] by auto + hence r_ge: "r \ -fpxs_val (poly.coeff p i) / (rat_of_nat N - rat_of_nat i)" + unfolding r_def using i that False by (intro Max.coboundedI) auto + + have "fls_subdegree (c' i) = fls_subdegree (c i) + (int N - int i) * a" + using i that False by (simp add: c'_def fls_X_intpow_times_conv_shift subdegree_c) + also have "rat_of_int \ = + fpxs_val (poly.coeff p i) * of_nat b + (of_nat N - of_nat i) * of_int a" + using i that False by (simp add: subdegree_c) + also have "\ = of_nat b * (of_nat N - of_nat i) * + (fpxs_val (poly.coeff p i) / (of_nat N - of_nat i) + r)" + using \b > 0\ i by (auto simp: field_simps ab(2)) + also have "\ \ 0" + using r_ge that by (intro mult_nonneg_nonneg) auto + finally have "fls_subdegree (c' i) \ 0" by simp + hence "\c''. c' i = fls_shift 0 (fps_to_fls c'')" + by (intro fls_as_fps') (auto simp: algebra_simps) + thus ?thesis by simp + qed + qed + then obtain c''_aux where c''_aux: "c' i = fps_to_fls (c''_aux i)" if "i \ N" for i + by metis + define c'' where "c'' = (\i. if i \ N then c''_aux i else 0)" + have c': "c' i = fps_to_fls (c'' i)" for i + proof (cases "i \ N") + case False + thus ?thesis by (auto simp: c'_def c''_def) + qed (auto simp: c''_def c''_aux) + have c''_eq: "fps_to_fls (c'' i) = c' i" for i + using c'[of i] by simp + + define p' where "p' = Abs_poly c''" + have coeff_p': "coeff p' = c''" + unfolding p'_def + proof (rule coeff_Abs_poly) + fix i assume "i > N" + hence "coeff p i = 0" + by (simp add: N_def coeff_eq_0) + thus "c'' i = 0" using c'[of i] c[of i] \b > 0\ + by (auto simp: c'_def fls_shift_eq0_iff) + qed + + text \ + We set up some homomorphisms to convert between the two polynomials: + \ + interpret comppow: map_poly_inj_idom_hom "(\x::'a fpxs. fpxs_compose_power x (1/rat_of_nat b))" + by unfold_locales (use \b > 0\ in simp_all) + define lift_poly :: "'a fps poly \ 'a fpxs poly" where + "lift_poly = (\p. pcompose p [:0, fpxs_X_power r:]) \ + (map_poly ((\x. fpxs_compose_power x (1/rat_of_nat b)) \ fpxs_of_fls \ fps_to_fls))" + have [simp]: "degree (lift_poly q) = degree q" for q + unfolding lift_poly_def by (simp add: degree_map_poly) + + interpret fps_to_fls: map_poly_inj_idom_hom fps_to_fls + by unfold_locales (simp_all add: fls_times_fps_to_fls) + interpret fpxs_of_fls: map_poly_inj_idom_hom fpxs_of_fls + by unfold_locales simp_all + interpret lift_poly: inj_idom_hom lift_poly + unfolding lift_poly_def + by (intro inj_idom_hom_compose inj_idom_hom_pcompose inj_idom_hom.inj_idom_hom_map_poly + fps_to_fls.base.inj_idom_hom_axioms fpxs_of_fls.base.inj_idom_hom_axioms + comppow.base.inj_idom_hom_axioms) simp_all + interpret lift_poly: map_poly_inj_idom_hom lift_poly + by unfold_locales + + define C :: "'a fpxs" where "C = fpxs_X_power (- (rat_of_nat N * r))" + have [simp]: "C \ 0" + by (auto simp: C_def) + + text \ + Now, finally: the original polynomial and the new polynomial are related through the + \<^term>\lift_poly\ homomorphism: + \ + have p_eq: "p = smult C (lift_poly p')" + using \b > 0\ + by (intro poly_eqI) + (simp_all add: coeff_map_poly coeff_pcompose_linear coeff_p' c c''_eq c'_def C_def + ring_distribs fpxs_X_power_conv_shift fpxs_shift_mult lift_poly_def ab(2) + flip: fpxs_X_power_add fpxs_X_power_mult fpxs_shift_add_left) + have [simp]: "degree p' = N" + unfolding N_def using \b > 0\ by (simp add: p_eq) + have lc_p': "lead_coeff p' = 1" + using c''_eq[of N] by (simp add: coeff_p' \c' N = 1\) + have "coeff p' (N - 1) = 0" + using coeff_deg_minus_1 \b > 0\ unfolding N_def [symmetric] + by (simp add: p_eq lift_poly_def coeff_map_poly coeff_pcompose_linear) + + text \ + We reduce $p'(X,Z)$ to $p'(X,0)$: + \ + define p'_proj where "p'_proj = reduce_fps_poly p'" + have [simp]: "degree p'_proj = N" + unfolding p'_proj_def using lc_p' by (subst degree_reduce_fps_poly_monic) simp_all + have lc_p'_proj: "lead_coeff p'_proj = 1" + unfolding p'_proj_def using lc_p' by (subst reduce_fps_poly_monic) simp_all + hence [simp]: "p'_proj \ 0" + by auto + have "coeff p'_proj (N - 1) = 0" + using \coeff p' (N - 1) = 0\ by (simp add: p'_proj_def reduce_fps_poly_def) + + text \ + We now show that \<^term>\p'_proj\ splits into non-trivial coprime factors. To do this, we + have to show that it has two distinct roots, i.e. that it is not of the form $(X - c)^n$. + \ + obtain g h where gh: "degree g > 0" "degree h > 0" "coprime g h" "p'_proj = g * h" + proof - + have "degree p'_proj > 1" + using deg_p by (auto simp: N_def) + text \Let \x\ be an arbitrary root of \<^term>\p'_proj\:\ + then obtain x where x: "poly p'_proj x = 0" + using alg_closed_imp_poly_has_root[of p'_proj] by force + + text \Assume for the sake of contradiction that \<^term>\p'_proj\ were equal to $(1-x)^n$:\ + have not_only_one_root: "p'_proj \ [:-x, 1:] ^ N" + proof safe + assume *: "p'_proj = [:-x, 1:] ^ N" + + text \ + If \x\ were non-zero, all the coefficients of \p'_proj\ would also be non-zero by the + Binomial Theorem. Since we know that the coefficient of \n - 1\ \<^emph>\is\ zero, this means + that \x\ must be zero: + \ + have "coeff p'_proj (N - 1) = 0" by fact + hence "x = 0" + by (subst (asm) *, subst (asm) coeff_linear_poly_power) auto + + text \ + However, by our choice of \r\, we know that there is an index \i\ such that \c' i\ has + is non-zero and has valuation (i.e. subdegree) 0, which means that the \i\-th coefficient + of \<^term>\p'_proj\ must also be non-zero. + \ + have "0 < N \ coeff p 0 \ 0" + using deg_p \coeff p 0 \ 0\ by (auto simp: N_def) + hence "{i\{.. 0} \ {}" + by blast + hence "r \ (\i. -fpxs_val (poly.coeff p i) / (rat_of_nat N - rat_of_nat i)) ` + {i\{.. 0}" + unfolding r_def using deg_p by (intro Max_in) (auto simp: N_def) + then obtain i where i: "i < N" "coeff p i \ 0" + "-fpxs_val (coeff p i) / (rat_of_nat N - rat_of_nat i) = r" + by blast + hence [simp]: "c' i \ 0" + using i c[of i] by (auto simp: c'_def) + have "fpxs_val (poly.coeff p i) = rat_of_int (fls_subdegree (c i)) / rat_of_nat b" + using subdegree_c[of i] i \b > 0\ by (simp add: field_simps) + also have "fpxs_val (coeff p i) = -r * (rat_of_nat N - rat_of_nat i)" + using i by (simp add: field_simps) + finally have "rat_of_int (fls_subdegree (c i)) = - r * (of_nat N - of_nat i) * of_nat b" + using \b > 0\ by (simp add: field_simps) + also have "c i = fls_shift ((int N - int i) * a) (c' i)" + using i by (simp add: c'_def ring_distribs fls_X_intpow_times_conv_shift + flip: fls_shifted_times_simps(2)) + also have "fls_subdegree \ = fls_subdegree (c' i) - (int N - int i) * a" + by (subst fls_shift_subdegree) auto + finally have "fls_subdegree (c' i) = 0" + using \b > 0\ by (simp add: ab(2)) + hence "subdegree (coeff p' i) = 0" + by (simp flip: c''_eq add: fls_subdegree_fls_to_fps coeff_p') + moreover have "coeff p' i \ 0" + using \c' i \ 0\ c' coeff_p' by auto + ultimately have "coeff p' i $ 0 \ 0" + using subdegree_eq_0_iff by blast + + also have "coeff p' i $ 0 = coeff p'_proj i" + by (simp add: p'_proj_def reduce_fps_poly_def) + also have "\ = 0" + by (subst *, subst coeff_linear_poly_power) (use i \x = 0\ in auto) + finally show False by simp + qed + + text \ + We can thus obtain our second root \y\ from the factorisation: + \ + have "\y. x \ y \ poly p'_proj y = 0" + proof (rule ccontr) + assume *: "\(\y. x \ y \ poly p'_proj y = 0)" + have "p'_proj \ 0" by simp + then obtain A where A: "size A = degree p'_proj" + "p'_proj = smult (lead_coeff p'_proj) (\x\#A. [:-x, 1:])" + using alg_closed_imp_factorization[of p'_proj] by blast + have "set_mset A = {x. poly p'_proj x = 0}" + using lc_p'_proj by (subst A) (auto simp: poly_prod_mset) + also have "\ = {x}" + using x * by auto + finally have "A = replicate_mset N x" + using set_mset_subset_singletonD[of A x] A(1) by simp + with A(2) have "p'_proj = [:- x, 1:] ^ N" + using lc_p'_proj by simp + with not_only_one_root show False + by contradiction + qed + then obtain y where "x \ y" "poly p'_proj y = 0" + by blast + + text \ + It now follows easily that \<^term>\p'_proj\ splits into non-trivial and coprime factors: + \ + show ?thesis + proof (rule alg_closed_imp_poly_splits_coprime) + show "degree p'_proj > 1" + using deg_p by (simp add: N_def) + show "x \ y" "poly p'_proj x = 0" "poly p'_proj y = 0" + by fact+ + qed (use that in metis) + qed + + text \ + By Hensel's lemma, these factors give rise to corresponding factors of \p'\: + \ + interpret hensel: fps_hensel p' p'_proj g h + proof unfold_locales + show "lead_coeff p' = 1" + using lc_p' by simp + qed (use gh \coprime g h\ in \simp_all add: p'_proj_def\) + + text \All that remains now is to undo the variable substitutions we did above:\ + have "p = [:C:] * lift_poly hensel.G * lift_poly hensel.H" + unfolding p_eq by (subst hensel.F_splits) (simp add: hom_distribs) + thus "\irreducible p" + by (rule reducible_polyI) (use hensel.deg_G hensel.deg_H gh in simp_all) +qed + +text \ + We do not actually show that this is the algebraic closure since this cannot be stated + idiomatically in the typeclass setting and is probably not very useful either, but it can + be motivated like this: + + Suppose we have an algebraically closed extension $L$ of the field of Laurent series. Clearly, + $X^{a/b}\in L$ for any integer \a\ and any positive integer \b\ since + $(X^{a/b})^b - X^a = 0$. But any Puiseux series $F(X)$ with root order \b\ can + be written as + \[F(X) = \sum_{k=0}^{b-1} X^{k/b} F_k(X)\] + where the Laurent series $F_k(X)$ are defined as follows: + \[F_k(X) := \sum_{n = n_{0,k}}^\infty [X^{n + k/b}] F(X) X^n\] + Thus, $F(X)$ can be written as a finite sum of products of elements in $L$ and must therefore + also be in $L$. Thus, the Puiseux series are all contained in $L$. +\ + + +subsection \Metric and topology\ + +text \ + Formal Puiseux series form a metric space with the usual metric for formal series: + Two series are ``close'' to one another if they have many initial coefficients in common. +\ + +instantiation fpxs :: (zero) norm +begin + +definition norm_fpxs :: "'a fpxs \ real" where + "norm f = (if f = 0 then 0 else 2 powr (-of_rat (fpxs_val f)))" + +instance .. + +end + + +instantiation fpxs :: (group_add) dist +begin + +definition dist_fpxs :: "'a fpxs \ 'a fpxs \ real" where + "dist f g = (if f = g then 0 else 2 powr (-of_rat (fpxs_val (f - g))))" + +instance .. + +end + + +instantiation fpxs :: (group_add) metric_space +begin + +definition uniformity_fpxs_def [code del]: + "(uniformity :: ('a fpxs \ 'a fpxs) filter) = (INF e\{0 <..}. principal {(x, y). dist x y < e})" + +definition open_fpxs_def [code del]: + "open (U :: 'a fpxs set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)" + +instance proof + fix f g h :: "'a fpxs" + show "dist f g \ dist f h + dist g h" + proof (cases "f \ g \ f \ h \ g \ h") + case True + have "dist f g \ 2 powr -real_of_rat (min (fpxs_val (f - h)) (fpxs_val (g - h)))" + using fpxs_val_add_ge[of "f - h" "h - g"] True + by (auto simp: algebra_simps fpxs_val_minus_commute dist_fpxs_def of_rat_less_eq) + also have "\ \ dist f h + dist g h" + using True by (simp add: dist_fpxs_def min_def) + finally show ?thesis . + qed (auto simp: dist_fpxs_def fpxs_val_minus_commute) +qed (simp_all add: uniformity_fpxs_def open_fpxs_def dist_fpxs_def) + +end + + +instance fpxs :: (group_add) dist_norm + by standard (auto simp: dist_fpxs_def norm_fpxs_def) + +end \ No newline at end of file diff --git a/thys/Formal_Puiseux_Series/Puiseux_Laurent_Library.thy b/thys/Formal_Puiseux_Series/Puiseux_Laurent_Library.thy new file mode 100644 --- /dev/null +++ b/thys/Formal_Puiseux_Series/Puiseux_Laurent_Library.thy @@ -0,0 +1,212 @@ +(* + File: Puiseux_Laurent_Library.thy + Author: Manuel Eberl, TU München +*) +subsection \Facts about Laurent series\ +theory Puiseux_Laurent_Library + imports "HOL-Computational_Algebra.Computational_Algebra" +begin + +lemma filterlim_at_top_div_const_nat: + assumes "c > 0" + shows "filterlim (\x::nat. x div c) at_top at_top" + unfolding filterlim_at_top +proof + fix C :: nat + have *: "n div c \ C" if "n \ C * c" for n + using assms that by (metis div_le_mono div_mult_self_is_m) + have "eventually (\n. n \ C * c) at_top" + by (rule eventually_ge_at_top) + thus "eventually (\n. n div c \ C) at_top" + by eventually_elim (use * in auto) +qed + +lemma fls_eq_iff: "f = g \ (\n. fls_nth f n = fls_nth g n)" + by transfer auto + +lemma fls_shift_eq_1_iff: "fls_shift n f = 1 \ f = fls_shift (-n) 1" +proof - + have "fls_shift n f = 1 \ fls_shift n f = fls_shift n (fls_shift (-n) 1)" + by (simp del: fls_shift_eq_iff) + also have "\ \ f = fls_shift (-n) 1" + by (subst fls_shift_eq_iff) auto + finally show ?thesis . +qed + +lemma fps_to_fls_eq_iff [simp]: "fps_to_fls f = fps_to_fls g \ f = g" +proof safe + assume "fps_to_fls f = fps_to_fls g" + hence *: "n < 0 \ f $ nat n = g $ nat n" for n + by (force simp: fls_eq_iff split: if_splits) + have "f $ n = g $ n" for n + using *[of "int n"] by auto + thus "f = g" + by (auto simp: fps_eq_iff) +qed + +lemma fps_to_fls_eq_0_iff [simp]: "fps_to_fls f = 0 \ f = 0" + using fps_to_fls_eq_iff[of f 0] by (simp del: fps_to_fls_eq_iff) + +lemma fps_to_fls_eq_1_iff [simp]: "fps_to_fls f = 1 \ f = 1" + using fps_to_fls_eq_iff[of f 1] by (simp del: fps_to_fls_eq_iff) + +lemma fps_to_fls_power: "fps_to_fls (f ^ n) = fps_to_fls f ^ n" + by (induction n) (auto simp: fls_times_fps_to_fls) + +lemma fls_as_fps: + fixes f :: "'a :: zero fls" and n :: int + assumes n: "n \ -fls_subdegree f" + obtains f' where "f = fls_shift n (fps_to_fls f')" +proof - + have "fls_subdegree (fls_shift (- n) f) \ 0" + by (rule fls_shift_nonneg_subdegree) (use n in simp) + hence "f = fls_shift n (fps_to_fls (fls_regpart (fls_shift (-n) f)))" + by (subst fls_regpart_to_fls_trivial) simp_all + thus ?thesis + by (rule that) +qed + +lemma fls_as_fps': + fixes f :: "'a :: zero fls" and n :: int + assumes n: "n \ -fls_subdegree f" + shows "\f'. f = fls_shift n (fps_to_fls f')" + using fls_as_fps[OF assms] by metis + + +definition fls_compose_fps :: "'a :: field fls \ 'a fps \ 'a fls" where + "fls_compose_fps f g = + (if f = 0 then 0 + else if fls_subdegree f \ 0 then fps_to_fls (fps_compose (fls_regpart f) g) + else fps_to_fls (fps_compose (fls_base_factor_to_fps f) g) / + fps_to_fls g ^ nat (-fls_subdegree f))" + +lemma fls_compose_fps_fps [simp]: + "fls_compose_fps (fps_to_fls f) g = fps_to_fls (fps_compose f g)" + by (auto simp: fls_compose_fps_def fls_subdegree_fls_to_fps) + +lemma fls_const_transfer [transfer_rule]: + "rel_fun (=) (pcr_fls (=)) + (\c n. if n = 0 then c else 0) fls_const" + by (auto simp: fls_const_def rel_fun_def pcr_fls_def OO_def cr_fls_def) + +lemma fls_shift_transfer [transfer_rule]: + "rel_fun (=) (rel_fun (pcr_fls (=)) (pcr_fls (=))) + (\n f k. f (k+n)) fls_shift" + by (auto simp: fls_const_def rel_fun_def pcr_fls_def OO_def cr_fls_def) + +lift_definition fls_compose_power :: "'a :: zero fls \ nat \ 'a fls" is + "\f d n. if d > 0 \ int d dvd n then f (n div int d) else 0" +proof - + fix f :: "int \ 'a" and d :: nat + assume *: "eventually (\n. f (-int n) = 0) cofinite" + show "eventually (\n. (if d > 0 \ int d dvd -int n then f (-int n div int d) else 0) = 0) cofinite" + proof (cases "d = 0") + case False + from * have "eventually (\n. f (-int n) = 0) at_top" + by (simp add: cofinite_eq_sequentially) + hence "eventually (\n. f (-int (n div d)) = 0) at_top" + by (rule eventually_compose_filterlim[OF _ filterlim_at_top_div_const_nat]) (use False in auto) + hence "eventually (\n. (if d > 0 \ int d dvd -int n then f (-int n div int d) else 0) = 0) at_top" + by eventually_elim (auto simp: zdiv_int dvd_neg_div) + thus ?thesis + by (simp add: cofinite_eq_sequentially) + qed auto +qed + +lemma fls_nth_compose_power: + assumes "d > 0" + shows "fls_nth (fls_compose_power f d) n = (if int d dvd n then fls_nth f (n div int d) else 0)" + using assms by transfer auto + + +lemma fls_compose_power_0_left [simp]: "fls_compose_power 0 d = 0" + by transfer auto + +lemma fls_compose_power_1_left [simp]: "d > 0 \ fls_compose_power 1 d = 1" + by transfer (auto simp: fun_eq_iff) + +lemma fls_compose_power_const_left [simp]: + "d > 0 \ fls_compose_power (fls_const c) d = fls_const c" + by transfer (auto simp: fun_eq_iff) + +lemma fls_compose_power_shift [simp]: + "d > 0 \ fls_compose_power (fls_shift n f) d = fls_shift (d * n) (fls_compose_power f d)" + by transfer (auto simp: fun_eq_iff add_ac mult_ac) + +lemma fls_compose_power_X_intpow [simp]: + "d > 0 \ fls_compose_power (fls_X_intpow n) d = fls_X_intpow (int d * n)" + by simp + +lemma fls_compose_power_X [simp]: + "d > 0 \ fls_compose_power fls_X d = fls_X_intpow (int d)" + by transfer (auto simp: fun_eq_iff) + +lemma fls_compose_power_X_inv [simp]: + "d > 0 \ fls_compose_power fls_X_inv d = fls_X_intpow (-int d)" + by (simp add: fls_X_inv_conv_shift_1) + +lemma fls_compose_power_0_right [simp]: "fls_compose_power f 0 = 0" + by transfer auto + +lemma fls_compose_power_add [simp]: + "fls_compose_power (f + g) d = fls_compose_power f d + fls_compose_power g d" + by transfer auto + +lemma fls_compose_power_diff [simp]: + "fls_compose_power (f - g) d = fls_compose_power f d - fls_compose_power g d" + by transfer auto + +lemma fls_compose_power_uminus [simp]: + "fls_compose_power (-f) d = -fls_compose_power f d" + by transfer auto + +lemma fps_nth_compose_X_power: + "fps_nth (f oo (fps_X ^ d)) n = (if d dvd n then fps_nth f (n div d) else 0)" +proof - + have "fps_nth (f oo (fps_X ^ d)) n = (\i = 0..n. f $ i * (fps_X ^ (d * i)) $ n)" + unfolding fps_compose_def by (simp add: power_mult) + also have "\ = (\i\(if d dvd n then {n div d} else {}). f $ i * (fps_X ^ (d * i)) $ n)" + by (intro sum.mono_neutral_right) auto + also have "\ = (if d dvd n then fps_nth f (n div d) else 0)" + by auto + finally show ?thesis . +qed + +lemma fls_compose_power_fps_to_fls: + assumes "d > 0" + shows "fls_compose_power (fps_to_fls f) d = fps_to_fls (fps_compose f (fps_X ^ d))" + using assms + by (intro fls_eqI) (auto simp: fls_nth_compose_power fps_nth_compose_X_power + pos_imp_zdiv_neg_iff div_neg_pos_less0 nat_div_distrib + simp flip: int_dvd_int_iff) + +lemma fls_compose_power_mult [simp]: + "fls_compose_power (f * g :: 'a :: idom fls) d = fls_compose_power f d * fls_compose_power g d" +proof (cases "d > 0") + case True + define n where "n = nat (max 0 (max (- fls_subdegree f) (- fls_subdegree g)))" + have n_ge: "-fls_subdegree f \ int n" "-fls_subdegree g \ int n" + unfolding n_def by auto + obtain f' where f': "f = fls_shift n (fps_to_fls f')" + using fls_as_fps[OF n_ge(1)] by (auto simp: n_def) + obtain g' where g': "g = fls_shift n (fps_to_fls g')" + using fls_as_fps[OF n_ge(2)] by (auto simp: n_def) + show ?thesis using \d > 0\ + by (simp add: f' g' fls_shifted_times_simps mult_ac fls_compose_power_fps_to_fls + fps_compose_mult_distrib flip: fls_times_fps_to_fls) +qed auto + +lemma fls_compose_power_power [simp]: + assumes "d > 0 \ n > 0" + shows "fls_compose_power (f ^ n :: 'a :: idom fls) d = fls_compose_power f d ^ n" +proof (cases "d > 0") + case True + thus ?thesis by (induction n) auto +qed (use assms in auto) + +lemma fls_nth_compose_power' [simp]: + "d = 0 \ \d dvd n \ fls_nth (fls_compose_power f d) n = 0" + "d dvd n \ d > 0 \ fls_nth (fls_compose_power f d) n = fls_nth f (n div d)" + by (transfer; force; fail)+ + +end \ No newline at end of file diff --git a/thys/Formal_Puiseux_Series/Puiseux_Polynomial_Library.thy b/thys/Formal_Puiseux_Series/Puiseux_Polynomial_Library.thy new file mode 100644 --- /dev/null +++ b/thys/Formal_Puiseux_Series/Puiseux_Polynomial_Library.thy @@ -0,0 +1,497 @@ +(* + File: Puiseux_Polynomial_Library.thy + Author: Manuel Eberl, TU München +*) +section \Auxiliary material\ +subsection \Facts about polynomials\ +theory Puiseux_Polynomial_Library + imports "HOL-Computational_Algebra.Computational_Algebra" "Polynomial_Interpolation.Ring_Hom_Poly" +begin + +(* TODO: move a lot of this *) + +lemma poly_sum_mset: "poly (\x\#A. p x) y = (\x\#A. poly (p x) y)" + by (induction A) auto + +lemma poly_prod_mset: "poly (\x\#A. p x) y = (\x\#A. poly (p x) y)" + by (induction A) auto + +lemma set_mset_subset_singletonD: + assumes "set_mset A \ {x}" + shows "A = replicate_mset (size A) x" + using assms by (induction A) auto + +lemma inj_idom_hom_compose [intro]: + assumes "inj_idom_hom f" "inj_idom_hom g" + shows "inj_idom_hom (f \ g)" +proof - + interpret f: inj_idom_hom f by fact + interpret g: inj_idom_hom g by fact + show ?thesis + by unfold_locales (auto simp: f.hom_add g.hom_add f.hom_mult g.hom_mult) +qed + +lemma coeff_pcompose_linear: + "coeff (pcompose p [:0, a :: 'a :: comm_semiring_1:]) i = a ^ i * coeff p i" + by (induction p arbitrary: i) (auto simp: pcompose_pCons coeff_pCons mult_ac split: nat.splits) + +lemma degree_cong: + assumes "\i. coeff p i = 0 \ coeff q i = 0" + shows "degree p = degree q" +proof - + have "(\n. \i>n. poly.coeff p i = 0) = (\n. \i>n. poly.coeff q i = 0)" + using assms by (auto simp: fun_eq_iff) + thus ?thesis + by (simp only: degree_def) +qed + +lemma coeff_Abs_poly_If_le: + "coeff (Abs_poly (\i. if i \ n then f i else 0)) = (\i. if i \ n then f i else 0)" +proof (rule Abs_poly_inverse, clarify) + have "eventually (\i. i > n) cofinite" + by (auto simp: MOST_nat) + thus "eventually (\i. (if i \ n then f i else 0) = 0) cofinite" + by eventually_elim auto +qed + +lemma coeff_Abs_poly: + assumes "\i. i > n \ f i = 0" + shows "coeff (Abs_poly f) = f" +proof (rule Abs_poly_inverse, clarify) + have "eventually (\i. i > n) cofinite" + by (auto simp: MOST_nat) + thus "eventually (\i. f i = 0) cofinite" + by eventually_elim (use assms in auto) +qed + +lemma (in inj_idom_hom) inj_idom_hom_map_poly [intro]: "inj_idom_hom (map_poly hom)" +proof - + interpret map_poly_inj_idom_hom hom by unfold_locales + show ?thesis + by (simp add: inj_idom_hom_axioms) +qed + +lemma inj_idom_hom_pcompose [intro]: + assumes [simp]: "degree (p :: 'a :: idom poly) \ 0" + shows "inj_idom_hom (\q. pcompose q p)" + by unfold_locales (simp_all add: pcompose_eq_0) + +lemma degree_sum_less: + assumes "\x. x \ A \ degree (f x) < n" "n > 0" + shows "degree (sum f A) < n" + using assms by (induction rule: infinite_finite_induct) (auto intro!: degree_add_less) + +lemma degree_lessI: + assumes "p \ 0 \ n > 0" "\k\n. coeff p k = 0" + shows "degree p < n" +proof (cases "p = 0") + case False + show ?thesis + proof (rule ccontr) + assume *: "\(degree p < n)" + define d where "d = degree p" + from \p \ 0\ have "coeff p d \ 0" + by (auto simp: d_def) + moreover have "coeff p d = 0" + using assms(2) * by (auto simp: not_less) + ultimately show False by contradiction + qed +qed (use assms in auto) + +lemma coeff_linear_poly_power: + fixes c :: "'a :: semiring_1" + assumes "i \ n" + shows "coeff ([:a, b:] ^ n) i = of_nat (n choose i) * b ^ i * a ^ (n - i)" +proof - + have "[:a, b:] = monom b 1 + [:a:]" + by (simp add: monom_altdef) + also have "coeff (\ ^ n) i = (\k\n. a^(n-k) * of_nat (n choose k) * (if k = i then b ^ k else 0))" + by (subst binomial_ring) (simp add: coeff_sum of_nat_poly monom_power poly_const_pow mult_ac) + also have "\ = (\k\{i}. a ^ (n - i) * b ^ i * of_nat (n choose k))" + using assms by (intro sum.mono_neutral_cong_right) (auto simp: mult_ac) + finally show *: ?thesis by (simp add: mult_ac) +qed + +lemma pcompose_altdef: "pcompose p q = poly (map_poly (\x. [:x:]) p) q" + by (induction p) simp_all + +lemma coeff_mult_0: "coeff (p * q) 0 = coeff p 0 * coeff q 0" + by (simp add: coeff_mult) + +lemma coeff_pcompose_0 [simp]: + "coeff (pcompose p q) 0 = poly p (coeff q 0)" + by (induction p) (simp_all add: coeff_mult_0) + +lemma reducible_polyI: + fixes p :: "'a :: field poly" + assumes "p = q * r" "degree q > 0" "degree r > 0" + shows "\irreducible p" + using assms by (auto simp: irreducible_def) + +lemma root_imp_reducible_poly: + fixes x :: "'a :: field" + assumes "poly p x = 0" and "degree p > 1" + shows "\irreducible p" +proof - + from assms have "p \ 0" + by auto + define q where "q = [:-x, 1:]" + have "q dvd p" + using assms by (simp add: poly_eq_0_iff_dvd q_def) + then obtain r where p_eq: "p = q * r" + by (elim dvdE) + have [simp]: "q \ 0" "r \ 0" + using \p \ 0\ by (auto simp: p_eq) + have "degree p = Suc (degree r)" + unfolding p_eq by (subst degree_mult_eq) (auto simp: q_def) + with assms(2) have "degree r > 0" + by auto + hence "\is_unit r" + by auto + moreover have "\is_unit q" + by (auto simp: q_def) + ultimately show ?thesis using p_eq + by (auto simp: irreducible_def) +qed + + +subsection \A typeclass for algebraically closed fields\ + +(* TODO: Move! *) + +text \ + Since the required sort constraints are not available inside the class, we have to resort + to a somewhat awkward way of writing the definition of algebraically closed fields: +\ +class alg_closed_field = field + + assumes alg_closed: "n > 0 \ f n \ 0 \ \x. (\k\n. f k * x ^ k) = 0" + +text \ + We can then however easily show the equivalence to the proper definition: +\ +lemma alg_closed_imp_poly_has_root: + assumes "degree (p :: 'a :: alg_closed_field poly) > 0" + shows "\x. poly p x = 0" +proof - + have "\x. (\k\degree p. coeff p k * x ^ k) = 0" + using assms by (intro alg_closed) auto + thus ?thesis + by (simp add: poly_altdef) +qed + +lemma alg_closedI [Pure.intro]: + assumes "\p :: 'a poly. degree p > 0 \ lead_coeff p = 1 \ \x. poly p x = 0" + shows "OFCLASS('a :: field, alg_closed_field_class)" +proof + fix n :: nat and f :: "nat \ 'a" + assume n: "n > 0" "f n \ 0" + define p where "p = Abs_poly (\k. if k \ n then f k else 0)" + have coeff_p: "coeff p k = (if k \ n then f k else 0)" for k + proof - + have "eventually (\k. k > n) cofinite" + by (auto simp: MOST_nat) + hence "eventually (\k. (if k \ n then f k else 0) = 0) cofinite" + by eventually_elim auto + thus ?thesis + unfolding p_def by (subst Abs_poly_inverse) auto + qed + + from n have "degree p \ n" + by (intro le_degree) (auto simp: coeff_p) + moreover have "degree p \ n" + by (intro degree_le) (auto simp: coeff_p) + ultimately have deg_p: "degree p = n" + by linarith + from deg_p and n have [simp]: "p \ 0" + by auto + + define p' where "p' = smult (inverse (lead_coeff p)) p" + have deg_p': "degree p' = degree p" + by (auto simp: p'_def) + have lead_coeff_p' [simp]: "lead_coeff p' = 1" + by (auto simp: p'_def) + + from deg_p and deg_p' and n have "degree p' > 0" + by simp + from assms[OF this] obtain x where "poly p' x = 0" + by auto + hence "poly p x = 0" + by (simp add: p'_def) + also have "poly p x = (\k\n. f k * x ^ k)" + unfolding poly_altdef by (intro sum.cong) (auto simp: deg_p coeff_p) + finally show "\x. (\k\n. f k * x ^ k) = 0" .. +qed + + +text \ + We can now prove by induction that every polynomial of degree \n\ splits into a product of + \n\ linear factors: +\ +lemma alg_closed_imp_factorization: + fixes p :: "'a :: alg_closed_field poly" + assumes "p \ 0" + shows "\A. size A = degree p \ p = smult (lead_coeff p) (\x\#A. [:-x, 1:])" + using assms +proof (induction "degree p" arbitrary: p rule: less_induct) + case (less p) + show ?case + proof (cases "degree p = 0") + case True + thus ?thesis + by (intro exI[of _ "{#}"]) (auto elim!: degree_eq_zeroE) + next + case False + then obtain x where x: "poly p x = 0" + using alg_closed_imp_poly_has_root by blast + hence "[:-x, 1:] dvd p" + using poly_eq_0_iff_dvd by blast + then obtain q where p_eq: "p = [:-x, 1:] * q" + by (elim dvdE) + have "q \ 0" + using less.prems p_eq by auto + moreover from this have deg: "degree p = Suc (degree q)" + unfolding p_eq by (subst degree_mult_eq) auto + ultimately obtain A where A: "size A = degree q" "q = smult (lead_coeff q) (\x\#A. [:-x, 1:])" + using less.hyps[of q] by auto + have "smult (lead_coeff p) (\y\#add_mset x A. [:- y, 1:]) = + [:- x, 1:] * smult (lead_coeff q) (\y\#A. [:- y, 1:])" + unfolding p_eq lead_coeff_mult by simp + also note A(2) [symmetric] + also note p_eq [symmetric] + finally show ?thesis using A(1) + by (intro exI[of _ "add_mset x A"]) (auto simp: deg) + qed +qed + +text \ + As an alternative characterisation of algebraic closure, one can also say that any + polynomial of degree at least 2 splits into non-constant factors: +\ +lemma alg_closed_imp_reducible: + assumes "degree (p :: 'a :: alg_closed_field poly) > 1" + shows "\irreducible p" +proof - + have "degree p > 0" + using assms by auto + then obtain z where z: "poly p z = 0" + using alg_closed_imp_poly_has_root[of p] by blast + then have dvd: "[:-z, 1:] dvd p" + by (subst dvd_iff_poly_eq_0) auto + then obtain q where q: "p = [:-z, 1:] * q" + by (erule dvdE) + have [simp]: "q \ 0" + using assms q by auto + + show ?thesis + proof (rule reducible_polyI) + show "p = [:-z, 1:] * q" + by fact + next + have "degree p = degree ([:-z, 1:] * q)" + by (simp only: q) + also have "\ = degree q + 1" + by (subst degree_mult_eq) auto + finally show "degree q > 0" + using assms by linarith + qed auto +qed + +text \ + When proving algebraic closure through reducibility, we can assume w.l.o.g. that the polynomial + is monic and has a non-zero constant coefficient: +\ +lemma alg_closedI_reducible: + assumes "\p :: 'a poly. degree p > 1 \ lead_coeff p = 1 \ coeff p 0 \ 0 \ + \irreducible p" + shows "OFCLASS('a :: field, alg_closed_field_class)" +proof + fix p :: "'a poly" assume p: "degree p > 0" "lead_coeff p = 1" + show "\x. poly p x = 0" + proof (cases "coeff p 0 = 0") + case True + hence "poly p 0 = 0" + by (simp add: poly_0_coeff_0) + thus ?thesis by blast + next + case False + from p and this show ?thesis + proof (induction "degree p" arbitrary: p rule: less_induct) + case (less p) + show ?case + proof (cases "degree p = 1") + case True + then obtain a b where p: "p = [:a, b:]" + by (cases p) (auto split: if_splits elim!: degree_eq_zeroE) + from True have [simp]: "b \ 0" + by (auto simp: p) + have "poly p (-a/b) = 0" + by (auto simp: p) + thus ?thesis by blast + next + case False + hence "degree p > 1" + using less.prems by auto + from assms[OF \degree p > 1\ \lead_coeff p = 1\ \coeff p 0 \ 0\] + have "\irreducible p" by auto + then obtain r s where rs: "degree r > 0" "degree s > 0" "p = r * s" + using less.prems by (auto simp: irreducible_def) + hence "coeff r 0 \ 0" + using \coeff p 0 \ 0\ by (auto simp: coeff_mult_0) + + define r' where "r' = smult (inverse (lead_coeff r)) r" + have [simp]: "degree r' = degree r" + by (simp add: r'_def) + have lc: "lead_coeff r' = 1" + using rs by (auto simp: r'_def) + have nz: "coeff r' 0 \ 0" + using \coeff r 0 \ 0\ by (auto simp: r'_def) + + have "degree r < degree r + degree s" + using rs by linarith + also have "\ = degree (r * s)" + using rs(3) less.prems by (subst degree_mult_eq) auto + also have "r * s = p" + using rs(3) by simp + finally have "\x. poly r' x = 0" + by (intro less) (use lc rs nz in auto) + thus ?thesis + using rs(3) by (auto simp: r'_def) + qed + qed + qed +qed + +text \ + Using a clever Tschirnhausen transformation mentioned e.g. in the article by + Nowak~\cite{nowak2000}, we can also assume w.l.o.g. that the coefficient $a_{n-1}$ is zero. +\ +lemma alg_closedI_reducible_coeff_deg_minus_one_eq_0: + assumes "\p :: 'a poly. degree p > 1 \ lead_coeff p = 1 \ coeff p (degree p - 1) = 0 \ + coeff p 0 \ 0 \ \irreducible p" + shows "OFCLASS('a :: field_char_0, alg_closed_field_class)" +proof (rule alg_closedI_reducible, goal_cases) + case (1 p) + define n where [simp]: "n = degree p" + define a where "a = coeff p (n - 1)" + define r where "r = [: -a / of_nat n, 1 :]" + define s where "s = [: a / of_nat n, 1 :]" + define q where "q = pcompose p r" + + have "n > 0" + using 1 by simp + have r_altdef: "r = monom 1 1 + [:-a / of_nat n:]" + by (simp add: r_def monom_altdef) + have deg_q: "degree q = n" + by (simp add: q_def r_def) + have lc_q: "lead_coeff q = 1" + unfolding q_def using 1 by (subst lead_coeff_comp) (simp_all add: r_def) + have "q \ 0" + using 1 deg_q by auto + + have "coeff q (n - 1) = + (\i\n. \k\i. coeff p i * (of_nat (i choose k) * + ((-a / of_nat n) ^ (i - k) * (if k = n - 1 then 1 else 0))))" + unfolding q_def pcompose_altdef poly_altdef r_altdef + by (simp_all add: degree_map_poly coeff_map_poly coeff_sum binomial_ring sum_distrib_left poly_const_pow + sum_distrib_right mult_ac monom_power coeff_monom_mult of_nat_poly cong: if_cong) + also have "\ = (\i\n. \k\(if i \ n - 1 then {n-1} else {}). + coeff p i * (of_nat (i choose k) * (-a / of_nat n) ^ (i - k)))" + by (rule sum.cong [OF refl], rule sum.mono_neutral_cong_right) (auto split: if_splits) + also have "\ = (\i\{n-1,n}. \k\(if i \ n - 1 then {n-1} else {}). + coeff p i * (of_nat (i choose k) * (-a / of_nat n) ^ (i - k)))" + by (rule sum.mono_neutral_right) auto + also have "\ = a - of_nat (n choose (n - 1)) * a / of_nat n" + using 1 by (simp add: a_def) + also have "n choose (n - 1) = n" + using \n > 0\ by (subst binomial_symmetric) auto + also have "a - of_nat n * a / of_nat n = 0" + using \n > 0\ by simp + finally have "coeff q (n - 1) = 0" . + + show ?case + proof (cases "coeff q 0 = 0") + case True + hence "poly p (- (a / of_nat (degree p))) = 0" + by (auto simp: q_def r_def) + thus ?thesis + by (rule root_imp_reducible_poly) (use 1 in auto) + next + case False + hence "\irreducible q" + using assms[of q] and lc_q and 1 and \coeff q (n - 1) = 0\ + by (auto simp: deg_q) + then obtain u v where uv: "degree u > 0" "degree v > 0" "q = u * v" + using \q \ 0\ 1 deg_q by (auto simp: irreducible_def) + + have "p = pcompose q s" + by (simp add: q_def r_def s_def flip: pcompose_assoc) + also have "q = u * v" + by fact + finally have "p = pcompose u s * pcompose v s" + by (simp add: pcompose_mult) + moreover have "degree (pcompose u s) > 0" "degree (pcompose v s) > 0" + using uv by (simp_all add: s_def) + ultimately show "\irreducible p" + using 1 by (intro reducible_polyI) + qed +qed + +text \ + As a consequence of the full factorisation lemma proven above, we can also show that any + polynomial with at least two different roots splits into two non-constant coprime factors: +\ +lemma alg_closed_imp_poly_splits_coprime: + assumes "degree (p :: 'a :: {alg_closed_field} poly) > 1" + assumes "poly p x = 0" "poly p y = 0" "x \ y" + obtains r s where "degree r > 0" "degree s > 0" "coprime r s" "p = r * s" +proof - + define n where "n = order x p" + have "n > 0" + using assms by (metis degree_0 gr0I n_def not_one_less_zero order_root) + have "[:-x, 1:] ^ n dvd p" + unfolding n_def by (simp add: order_1) + then obtain q where p_eq: "p = [:-x, 1:] ^ n * q" + by (elim dvdE) + from assms have [simp]: "q \ 0" + by (auto simp: p_eq) + have "order x p = n + Polynomial.order x q" + unfolding p_eq by (subst order_mult) (auto simp: order_power_n_n) + hence "Polynomial.order x q = 0" + by (simp add: n_def) + hence "poly q x \ 0" + by (simp add: order_root) + + show ?thesis + proof (rule that) + show "coprime ([:-x, 1:] ^ n) q" + proof (rule coprimeI) + fix d + assume d: "d dvd [:-x, 1:] ^ n" "d dvd q" + have "degree d = 0" + proof (rule ccontr) + assume "\(degree d = 0)" + then obtain z where z: "poly d z = 0" + using alg_closed_imp_poly_has_root by blast + moreover from this and d(1) have "poly ([:-x, 1:] ^ n) z = 0" + using dvd_trans poly_eq_0_iff_dvd by blast + ultimately have "poly d x = 0" + by auto + with d(2) have "poly q x = 0" + using dvd_trans poly_eq_0_iff_dvd by blast + with \poly q x \ 0\ show False by contradiction + qed + thus "is_unit d" using d + by auto + qed + next + have "poly q y = 0" + using \poly p y = 0\ \x \ y\ by (auto simp: p_eq) + with \q \ 0\ show "degree q > 0" + using poly_zero by blast + qed (use \n > 0\ in \simp_all add: p_eq degree_power_eq\) +qed + +instance complex :: alg_closed_field + by standard (use constant_degree fundamental_theorem_of_algebra neq0_conv in blast) + +end \ No newline at end of file diff --git a/thys/Formal_Puiseux_Series/ROOT b/thys/Formal_Puiseux_Series/ROOT new file mode 100644 --- /dev/null +++ b/thys/Formal_Puiseux_Series/ROOT @@ -0,0 +1,15 @@ +chapter AFP + +session Formal_Puiseux_Series (AFP) = "HOL-Computational_Algebra" + + options [timeout = 1200] + sessions + Polynomial_Interpolation + theories + Puiseux_Polynomial_Library + Puiseux_Laurent_Library + FPS_Hensel + Formal_Puiseux_Series + document_files + "root.tex" + "root.bib" + diff --git a/thys/Formal_Puiseux_Series/document/root.bib b/thys/Formal_Puiseux_Series/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Formal_Puiseux_Series/document/root.bib @@ -0,0 +1,17 @@ +@article{nowak2000, + title={Some elementary proofs of {P}uiseux’s theorems}, + author={Nowak, Krzysztof Jan}, + journal={Univ. Iagel. Acta Math}, + volume={38}, + pages={279--282}, + year={2000} +} + +@book{abhyankar1990, + title={Algebraic Geometry for Scientists and Engineers}, + author={Shreeram Shankar Abhyankar}, + isbn={9780821815359}, + series={Mathematical surveys and monographs}, + year={1990}, + publisher={American Mathematical Society} +} diff --git a/thys/Formal_Puiseux_Series/document/root.tex b/thys/Formal_Puiseux_Series/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Formal_Puiseux_Series/document/root.tex @@ -0,0 +1,43 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} +\usepackage{amsfonts, amsmath, amssymb} +\usepackage{pgfplots} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Formal Puiseux Series} +\author{Manuel Eberl} +\maketitle + +\begin{abstract} +Formal Puiseux series are generalisations of formal power series and formal Laurent series that also allow for fractional exponents. They have the following general form: +\[\sum_{i=N}^\infty a_{i/d} X^{i/d}\] +where $N$ is an integer and $d$ is a positive integer. + +This entry defines these series including their basic algebraic properties. Furthermore, it proves the Newton--Puiseux Theorem, namely that the Puiseux series over an algebraically closed field of characteristic 0 are also algebraically closed. +\end{abstract} + +\newpage +\tableofcontents +\newpage +\parindent 0pt\parskip 0.5ex + +\input{session} + +\nocite{corless96} +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,584 +1,585 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BNF_CC BNF_Operations Banach_Steinhaus Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties CSP_RefTK DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DOM_Components DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing +Formal_Puiseux_Series Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpreter_Optimizations Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaGeoCoq Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knuth_Bendix_Order Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mersenne_Primes MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PCF PLM POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Projective_Geometry Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Shadow_DOM Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL