# HG changeset patch
# User eberlm
# Date 1466092629 -7200
# Node ID ca187a9f66daf8bdc20c756e7c744b294479493e
# Parent  3b69758756331faf4c267e4051862fe7f0eef9dc
Various additions to polynomials, FPSs, Gamma function

diff -r 3b6975875633 -r ca187a9f66da src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Binomial.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -672,6 +672,10 @@
   finally show ?case .
 qed simp
 
+lemma fact_double:
+  "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)"
+  using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact)
+
 lemma pochhammer_absorb_comp:
   "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
   (is "?lhs = ?rhs")
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Divides.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -363,6 +363,23 @@
 lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
 by (blast intro: dvd_mod_imp_dvd dvd_mod)
 
+lemma div_div_eq_right:
+  assumes "c dvd b" "b dvd a"
+  shows   "a div (b div c) = a div b * c"
+proof -
+  from assms have "a div b * c = (a * c) div b"
+    by (subst dvd_div_mult) simp_all
+  also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp
+  also have "a * c div (b div c * c) = a div (b div c)"
+    by (cases "c = 0") simp_all
+  finally show ?thesis ..
+qed
+
+lemma div_div_div_same:
+  assumes "d dvd a" "d dvd b" "b dvd a"
+  shows   "(a div d) div (b div d) = a div b"
+  using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
+
 end
 
 class ring_div = comm_ring_1 + semiring_div
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Groups_List.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -369,6 +369,10 @@
   with assms(1) show ?thesis by simp
 qed
 
+lemma listprod_zero_iff: 
+  "listprod xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
+  by (induction xs) simp_all
+
 text \<open>Some syntactic sugar:\<close>
 
 syntax (ASCII)
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -248,6 +248,9 @@
 
 subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
 
+lemma fps_square_nth: "(f^2) $ n = (\<Sum>k\<le>n. f $ k * f $ (n - k))"
+  by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost)
+
 lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)"
   by (simp add: expand_fps_eq)
 
@@ -387,6 +390,10 @@
 lemma fps_numeral_nth_0 [simp]: "numeral n $ 0 = numeral n"
   by (simp add: numeral_fps_const)
 
+lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
+  by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
+
+
 
 subsection \<open>The eXtractor series X\<close>
 
@@ -412,8 +419,18 @@
 qed
 
 lemma X_mult_right_nth[simp]:
-    "((f :: 'a::comm_semiring_1 fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
-  by (metis X_mult_nth mult.commute)
+  "((a::'a::semiring_1 fps) * X) $ n = (if n = 0 then 0 else a $ (n - 1))"
+proof -
+  have "(a * X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
+    by (simp add: fps_times_def X_def)
+  also have "\<dots> = (\<Sum>i = 0..n. if i = n - 1 then if n = 0 then 0 else a $ i else 0)"
+    by (intro setsum.cong) auto
+  also have "\<dots> = (if n = 0 then 0 else a $ (n - 1))" by (simp add: setsum.delta)
+  finally show ?thesis .
+qed
+
+lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X" 
+  by (simp add: fps_eq_iff)
 
 lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then 1::'a::comm_ring_1 else 0)"
 proof (induct k)
@@ -1057,6 +1074,9 @@
     by (auto simp add: expand_fps_eq)
 qed
 
+lemma fps_inverse_eq_0: "f$0 = 0 \<Longrightarrow> inverse (f :: 'a :: division_ring fps) = 0"
+  by simp
+  
 lemma setsum_zero_lemma:
   fixes n::nat
   assumes "0 < n"
@@ -1311,6 +1331,16 @@
   thus "f dvd g" by (simp add: dvd_eq_mod_eq_0)
 qed (simp add: assms dvd_imp_subdegree_le)
 
+lemma fps_shift_altdef:
+  "fps_shift n f = (f :: 'a :: field fps) div X^n"
+  by (simp add: fps_divide_def)
+  
+lemma fps_div_X_power_nth: "((f :: 'a :: field fps) div X^n) $ k = f $ (k + n)"
+  by (simp add: fps_shift_altdef [symmetric])
+
+lemma fps_div_X_nth: "((f :: 'a :: field fps) div X) $ k = f $ Suc k"
+  using fps_div_X_power_nth[of f 1] by simp
+
 lemma fps_const_inverse: "inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
   by (cases "a \<noteq> 0", rule fps_inverse_unique) (auto simp: fps_eq_iff)
 
@@ -1321,6 +1351,18 @@
   "inverse (numeral n :: ('a :: field_char_0) fps) = fps_const (inverse (numeral n))"
   by (intro fps_inverse_unique fps_ext) (simp_all add: fps_numeral_nth)
 
+lemma fps_numeral_divide_divide:
+  "x / numeral b / numeral c = (x / numeral (b * c) :: 'a :: field fps)"
+  by (cases "numeral b = (0::'a)"; cases "numeral c = (0::'a)")
+      (simp_all add: fps_divide_unit fps_inverse_mult [symmetric] numeral_fps_const numeral_mult 
+                del: numeral_mult [symmetric])
+
+lemma fps_numeral_mult_divide:
+  "numeral b * x / numeral c = (numeral b / numeral c * x :: 'a :: field fps)"
+  by (cases "numeral c = (0::'a)") (simp_all add: fps_divide_unit numeral_fps_const)
+
+lemmas fps_numeral_simps = 
+  fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
 
 
 
@@ -1828,6 +1870,12 @@
   shows "f * inverse f = 1"
   by (metis mult.commute inverse_mult_eq_1 f0)
 
+lemma fps_inverse_minus [simp]: "inverse (-f) = -inverse (f :: 'a :: field fps)"
+  by (cases "f$0 = 0") (auto intro: fps_inverse_unique simp: inverse_mult_eq_1' fps_inverse_eq_0)
+  
+lemma divide_fps_const [simp]: "f / fps_const (c :: 'a :: field) = fps_const (inverse c) * f"
+  by (cases "c = 0") (simp_all add: fps_divide_unit fps_const_inverse)
+
 (* FIXME: The last part of this proof should go through by simp once we have a proper
    theorem collection for simplifying division on rings *)
 lemma fps_divide_deriv:
@@ -1846,6 +1894,18 @@
 lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
   by (simp add: fps_inverse_gp fps_eq_iff X_def)
 
+lemma fps_one_over_one_minus_X_squared:
+  "inverse ((1 - X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))"
+proof -
+  have "inverse ((1 - X)^2 :: 'a fps) = fps_deriv (inverse (1 - X))"
+    by (subst fps_inverse_deriv) (simp_all add: fps_inverse_power)
+  also have "inverse (1 - X :: 'a fps) = Abs_fps (\<lambda>_. 1)"
+    by (subst fps_inverse_gp' [symmetric]) simp
+  also have "fps_deriv \<dots> = Abs_fps (\<lambda>n. of_nat (n + 1))"
+    by (simp add: fps_deriv_def)
+  finally show ?thesis .
+qed
+
 lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)"
   by (cases n) simp_all
 
@@ -2307,6 +2367,157 @@
  finally show ?thesis .
 qed
 
+lemma natpermute_max_card:
+  assumes n0: "n \<noteq> 0"
+  shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
+  unfolding natpermute_contain_maximal
+proof -
+  let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
+  let ?K = "{0 ..k}"
+  have fK: "finite ?K"
+    by simp
+  have fAK: "\<forall>i\<in>?K. finite (?A i)"
+    by auto
+  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
+    {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+  proof clarify
+    fix i j
+    assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j"
+    have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
+    proof -
+      have "(replicate (k+1) 0 [i:=n] ! i) = n"
+        using i by (simp del: replicate.simps)
+      moreover
+      have "(replicate (k+1) 0 [j:=n] ! i) = 0"
+        using i ij by (simp del: replicate.simps)
+      ultimately show ?thesis
+        using eq n0 by (simp del: replicate.simps)
+    qed
+    then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+      by auto
+  qed
+  from card_UN_disjoint[OF fK fAK d]
+  show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1"
+    by simp
+qed
+
+lemma fps_power_Suc_nth:
+  fixes f :: "'a :: comm_ring_1 fps"
+  assumes k: "k > 0"
+  shows "(f ^ Suc m) $ k = 
+           of_nat (Suc m) * (f $ k * (f $ 0) ^ m) +
+           (\<Sum>v\<in>{v\<in>natpermute k (m+1). k \<notin> set v}. \<Prod>j = 0..m. f $ v ! j)"
+proof -
+  define A B 
+    where "A = {v\<in>natpermute k (m+1). k \<in> set v}" 
+      and  "B = {v\<in>natpermute k (m+1). k \<notin> set v}"
+  have [simp]: "finite A" "finite B" "A \<inter> B = {}" by (auto simp: A_def B_def natpermute_finite)
+
+  from natpermute_max_card[of k m] k have card_A: "card A = m + 1" by (simp add: A_def)
+  {
+    fix v assume v: "v \<in> A"
+    from v have [simp]: "length v = Suc m" by (simp add: A_def natpermute_def)
+    from v have "\<exists>j. j \<le> m \<and> v ! j = k" 
+      by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le)
+    then guess j by (elim exE conjE) note j = this
+    
+    from v have "k = listsum v" by (simp add: A_def natpermute_def)
+    also have "\<dots> = (\<Sum>i=0..m. v ! i)"
+      by (simp add: listsum_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
+    also from j have "{0..m} = insert j ({0..m}-{j})" by auto
+    also from j have "(\<Sum>i\<in>\<dots>. v ! i) = k + (\<Sum>i\<in>{0..m}-{j}. v ! i)"
+      by (subst setsum.insert) simp_all
+    finally have "(\<Sum>i\<in>{0..m}-{j}. v ! i) = 0" by simp
+    hence zero: "v ! i = 0" if "i \<in> {0..m}-{j}" for i using that
+      by (subst (asm) setsum_eq_0_iff) auto
+      
+    from j have "{0..m} = insert j ({0..m} - {j})" by auto
+    also from j have "(\<Prod>i\<in>\<dots>. f $ (v ! i)) = f $ k * (\<Prod>i\<in>{0..m} - {j}. f $ (v ! i))"
+      by (subst setprod.insert) auto
+    also have "(\<Prod>i\<in>{0..m} - {j}. f $ (v ! i)) = (\<Prod>i\<in>{0..m} - {j}. f $ 0)"
+      by (intro setprod.cong) (simp_all add: zero)
+    also from j have "\<dots> = (f $ 0) ^ m" by (subst setprod_constant) simp_all
+    finally have "(\<Prod>j = 0..m. f $ (v ! j)) = f $ k * (f $ 0) ^ m" .
+  } note A = this
+  
+  have "(f ^ Suc m) $ k = (\<Sum>v\<in>natpermute k (m + 1). \<Prod>j = 0..m. f $ v ! j)"
+    by (rule fps_power_nth_Suc)
+  also have "natpermute k (m+1) = A \<union> B" unfolding A_def B_def by blast
+  also have "(\<Sum>v\<in>\<dots>. \<Prod>j = 0..m. f $ (v ! j)) = 
+               (\<Sum>v\<in>A. \<Prod>j = 0..m. f $ (v ! j)) + (\<Sum>v\<in>B. \<Prod>j = 0..m. f $ (v ! j))"
+    by (intro setsum.union_disjoint) simp_all   
+  also have "(\<Sum>v\<in>A. \<Prod>j = 0..m. f $ (v ! j)) = of_nat (Suc m) * (f $ k * (f $ 0) ^ m)"
+    by (simp add: A card_A)
+  finally show ?thesis by (simp add: B_def)
+qed 
+  
+lemma fps_power_Suc_eqD:
+  fixes f g :: "'a :: {idom,semiring_char_0} fps"
+  assumes "f ^ Suc m = g ^ Suc m" "f $ 0 = g $ 0" "f $ 0 \<noteq> 0"
+  shows   "f = g"
+proof (rule fps_ext)
+  fix k :: nat
+  show "f $ k = g $ k"
+  proof (induction k rule: less_induct)
+    case (less k)
+    show ?case
+    proof (cases "k = 0")
+      case False
+      let ?h = "\<lambda>f. (\<Sum>v | v \<in> natpermute k (m + 1) \<and> k \<notin> set v. \<Prod>j = 0..m. f $ v ! j)"
+      from False fps_power_Suc_nth[of k f m] fps_power_Suc_nth[of k g m]
+        have "f $ k * (of_nat (Suc m) * (f $ 0) ^ m) + ?h f =
+                g $ k * (of_nat (Suc m) * (f $ 0) ^ m) + ?h g" using assms 
+        by (simp add: mult_ac del: power_Suc of_nat_Suc)
+      also have "v ! i < k" if "v \<in> {v\<in>natpermute k (m+1). k \<notin> set v}" "i \<le> m" for v i
+        using that elem_le_listsum_nat[of i v] unfolding natpermute_def
+        by (auto simp: set_conv_nth dest!: spec[of _ i])
+      hence "?h f = ?h g"
+        by (intro setsum.cong refl setprod.cong less lessI) (auto simp: natpermute_def)
+      finally have "f $ k * (of_nat (Suc m) * (f $ 0) ^ m) = g $ k * (of_nat (Suc m) * (f $ 0) ^ m)"
+        by simp
+      with assms show "f $ k = g $ k" 
+        by (subst (asm) mult_right_cancel) (auto simp del: of_nat_Suc)
+    qed (simp_all add: assms)
+  qed
+qed
+
+lemma fps_power_Suc_eqD':
+  fixes f g :: "'a :: {idom,semiring_char_0} fps"
+  assumes "f ^ Suc m = g ^ Suc m" "f $ subdegree f = g $ subdegree g"
+  shows   "f = g"
+proof (cases "f = 0")
+  case False
+  have "Suc m * subdegree f = subdegree (f ^ Suc m)"
+    by (rule subdegree_power [symmetric])
+  also have "f ^ Suc m = g ^ Suc m" by fact
+  also have "subdegree \<dots> = Suc m * subdegree g" by (rule subdegree_power)
+  finally have [simp]: "subdegree f = subdegree g"
+    by (subst (asm) Suc_mult_cancel1)
+  have "fps_shift (subdegree f) f * X ^ subdegree f = f"
+    by (rule subdegree_decompose [symmetric])
+  also have "\<dots> ^ Suc m = g ^ Suc m" by fact
+  also have "g = fps_shift (subdegree g) g * X ^ subdegree g"
+    by (rule subdegree_decompose)
+  also have "subdegree f = subdegree g" by fact
+  finally have "fps_shift (subdegree g) f ^ Suc m = fps_shift (subdegree g) g ^ Suc m"
+    by (simp add: algebra_simps power_mult_distrib del: power_Suc)
+  hence "fps_shift (subdegree g) f = fps_shift (subdegree g) g"
+    by (rule fps_power_Suc_eqD) (insert assms False, auto)
+  with subdegree_decompose[of f] subdegree_decompose[of g] show ?thesis by simp
+qed (insert assms, simp_all)
+
+lemma fps_power_eqD':
+  fixes f g :: "'a :: {idom,semiring_char_0} fps"
+  assumes "f ^ m = g ^ m" "f $ subdegree f = g $ subdegree g" "m > 0"
+  shows   "f = g"
+  using fps_power_Suc_eqD'[of f "m-1" g] assms by simp
+
+lemma fps_power_eqD:
+  fixes f g :: "'a :: {idom,semiring_char_0} fps"
+  assumes "f ^ m = g ^ m" "f $ 0 = g $ 0" "f $ 0 \<noteq> 0" "m > 0"
+  shows   "f = g"
+  by (rule fps_power_eqD'[of f m g]) (insert assms, simp_all)
+
 lemma fps_compose_inj_right:
   assumes a0: "a$0 = (0::'a::idom)"
     and a1: "a$1 \<noteq> 0"
@@ -2442,40 +2653,6 @@
     using Suc by simp
 qed
 
-lemma natpermute_max_card:
-  assumes n0: "n \<noteq> 0"
-  shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
-  unfolding natpermute_contain_maximal
-proof -
-  let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
-  let ?K = "{0 ..k}"
-  have fK: "finite ?K"
-    by simp
-  have fAK: "\<forall>i\<in>?K. finite (?A i)"
-    by auto
-  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
-    {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
-  proof clarify
-    fix i j
-    assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j"
-    have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
-    proof -
-      have "(replicate (k+1) 0 [i:=n] ! i) = n"
-        using i by (simp del: replicate.simps)
-      moreover
-      have "(replicate (k+1) 0 [j:=n] ! i) = 0"
-        using i ij by (simp del: replicate.simps)
-      ultimately show ?thesis
-        using eq n0 by (simp del: replicate.simps)
-    qed
-    then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
-      by auto
-  qed
-  from card_UN_disjoint[OF fK fAK d]
-  show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1"
-    by simp
-qed
-
 lemma power_radical:
   fixes a:: "'a::field_char_0 fps"
   assumes a0: "a$0 \<noteq> 0"
@@ -3213,6 +3390,21 @@
   apply (simp add: fps_compose_mult_distrib[OF c0])
   done
 
+lemma fps_compose_divide:
+  assumes [simp]: "g dvd f" "h $ 0 = 0"
+  shows   "fps_compose f h = fps_compose (f / g :: 'a :: field fps) h * fps_compose g h"
+proof -
+  have "f = (f / g) * g" by simp
+  also have "fps_compose \<dots> h = fps_compose (f / g) h * fps_compose g h"
+    by (subst fps_compose_mult_distrib) simp_all
+  finally show ?thesis .
+qed
+
+lemma fps_compose_divide_distrib:
+  assumes "g dvd f" "h $ 0 = 0" "fps_compose g h \<noteq> 0"
+  shows   "fps_compose (f / g :: 'a :: field fps) h = fps_compose f h / fps_compose g h"
+  using fps_compose_divide[OF assms(1,2)] assms(3) by simp
+
 lemma fps_compose_power:
   assumes c0: "c$0 = (0::'a::idom)"
   shows "(a oo c)^n = a^n oo c"
@@ -3493,6 +3685,10 @@
     unfolding fps_inv_right[OF a0 a1] by simp
 qed
 
+lemma fps_compose_linear:
+  "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)"
+  by (simp add: fps_eq_iff fps_compose_def power_mult_distrib
+                if_distrib setsum.delta' cong: if_cong)
 
 subsection \<open>Elementary series\<close>
 
@@ -3742,6 +3938,10 @@
   qed
 qed
 
+lemma fps_binomial_ODE_unique':
+  "(fps_deriv a = fps_const c * a / (1 + X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)"
+  by (subst fps_binomial_ODE_unique) auto
+
 lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
 proof -
   let ?a = "fps_binomial c"
@@ -3783,6 +3983,87 @@
   show ?thesis by (simp add: fps_inverse_def)
 qed
 
+lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + X :: 'a :: field_char_0 fps) ^ n"
+proof (cases "n = 0")
+  case [simp]: True
+  have "fps_deriv ((1 + X) ^ n :: 'a fps) = 0" by simp
+  also have "\<dots> = fps_const (of_nat n) * (1 + X) ^ n / (1 + X)" by (simp add: fps_binomial_def)
+  finally show ?thesis by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) simp_all
+next
+  case False
+  have "fps_deriv ((1 + X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + X) ^ (n - 1)"
+    by (simp add: fps_deriv_power)
+  also have "(1 + X :: 'a fps) $ 0 \<noteq> 0" by simp
+  hence "(1 + X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp)
+  with False have "(1 + X :: 'a fps) ^ (n - 1) = (1 + X) ^ n / (1 + X)"
+    by (cases n) (simp_all )
+  also have "fps_const (of_nat n :: 'a) * ((1 + X) ^ n / (1 + X)) =
+               fps_const (of_nat n) * (1 + X) ^ n / (1 + X)"
+    by (simp add: unit_div_mult_swap)
+  finally show ?thesis
+    by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) (simp_all add: fps_power_nth)
+qed
+
+lemma fps_binomial_0 [simp]: "fps_binomial 0 = 1"
+  using fps_binomial_of_nat[of 0] by simp
+  
+lemma fps_binomial_power: "fps_binomial a ^ n = fps_binomial (of_nat n * a)"
+  by (induction n) (simp_all add: fps_binomial_add_mult ring_distribs)
+
+lemma fps_binomial_1: "fps_binomial 1 = 1 + X"
+  using fps_binomial_of_nat[of 1] by simp
+
+lemma fps_binomial_minus_of_nat:
+  "fps_binomial (- of_nat n) = inverse ((1 + X :: 'a :: field_char_0 fps) ^ n)"
+  by (rule sym, rule fps_inverse_unique)
+     (simp add: fps_binomial_of_nat [symmetric] fps_binomial_add_mult [symmetric])
+
+lemma one_minus_const_X_power:
+  "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * X) ^ n =
+     fps_compose (fps_binomial (of_nat n)) (-fps_const c * X)"
+  by (subst fps_binomial_of_nat)
+     (simp add: fps_compose_power [symmetric] fps_compose_add_distrib fps_const_neg [symmetric] 
+           del: fps_const_neg)
+
+lemma one_minus_X_const_neg_power:
+  "inverse ((1 - fps_const c * X) ^ n) = 
+       fps_compose (fps_binomial (-of_nat n)) (-fps_const c * X)"
+proof (cases "c = 0")
+  case False
+  thus ?thesis
+  by (subst fps_binomial_minus_of_nat)
+     (simp add: fps_compose_power [symmetric] fps_inverse_compose fps_compose_add_distrib
+                fps_const_neg [symmetric] del: fps_const_neg)
+qed simp
+
+lemma X_plus_const_power:
+  "c \<noteq> 0 \<Longrightarrow> (X + fps_const c) ^ n =
+     fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * X)"
+  by (subst fps_binomial_of_nat)
+     (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
+                fps_const_power [symmetric] power_mult_distrib [symmetric] 
+                algebra_simps inverse_mult_eq_1' del: fps_const_power)
+
+lemma X_plus_const_neg_power:
+  "c \<noteq> 0 \<Longrightarrow> inverse ((X + fps_const c) ^ n) =
+     fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * X)"
+  by (subst fps_binomial_minus_of_nat)
+     (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
+                fps_const_power [symmetric] power_mult_distrib [symmetric] fps_inverse_compose 
+                algebra_simps fps_const_inverse [symmetric] fps_inverse_mult [symmetric]
+                fps_inverse_power [symmetric] inverse_mult_eq_1'
+           del: fps_const_power)
+
+
+lemma one_minus_const_X_neg_power':
+  "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * X) ^ n) =
+       Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)"
+  apply (rule fps_ext)
+  apply (subst one_minus_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear)
+  apply (simp add: power_mult_distrib [symmetric] mult.assoc [symmetric] 
+                   gbinomial_minus binomial_gbinomial of_nat_diff)
+  done
+
 text \<open>Vandermonde's Identity as a consequence.\<close>
 lemma gbinomial_Vandermonde:
   "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
@@ -4216,6 +4497,10 @@
 lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   by (fact fps_const_sub)
 
+lemma fps_of_int: "fps_const (of_int c) = of_int c"
+  by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
+                             del: fps_const_minus fps_const_neg)
+
 lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
   by (fact numeral_fps_const) (* FIXME: duplicate *)
 
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Library/Library.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -58,6 +58,7 @@
   Permutation
   Permutations
   Polynomial
+  Polynomial_FPS
   Preorder
   Product_Vector
   Quadratic_Discriminant
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -564,8 +564,14 @@
   fixes a x :: "'a::{comm_semiring_1}"
   shows "poly (monom a n) x = a * x ^ n"
   by (cases "a = 0", simp_all)
-    (induct n, simp_all add: mult.left_commute poly_def)
-
+    (induct n, simp_all add: mult.left_commute poly_def)  
+
+lemma monom_eq_iff': "monom c n = monom d m \<longleftrightarrow>  c = d \<and> (c = 0 \<or> n = m)"
+  by (auto simp: poly_eq_iff)
+  
+lemma monom_eq_const_iff: "monom c n = [:d:] \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = 0)"
+  using monom_eq_iff'[of c n d 0] by (simp add: monom_0)
+  
     
 subsection \<open>Addition and subtraction\<close>
 
@@ -869,6 +875,9 @@
 lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   by (induct n, simp add: monom_0, simp add: monom_Suc)
 
+lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
+  by (auto simp add: poly_eq_iff coeff_Poly_eq nth_default_def)
+
 lemma degree_smult_eq [simp]:
   fixes a :: "'a::idom"
   shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
@@ -878,7 +887,7 @@
   fixes a :: "'a::idom"
   shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
   by (simp add: poly_eq_iff)
-
+  
 lemma coeffs_smult [code abstract]:
   fixes p :: "'a::idom poly"
   shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
@@ -985,6 +994,13 @@
 lemma monom_eq_1 [simp]:
   "monom 1 0 = 1"
   by (simp add: monom_0 one_poly_def)
+
+lemma monom_eq_1_iff: "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0"
+  using monom_eq_const_iff[of c n 1] by (auto simp: one_poly_def)
+
+lemma monom_altdef:
+  "monom c n = smult c ([:0, 1:]^n)"
+  by (induction n) (simp_all add: monom_0 monom_Suc one_poly_def)
   
 lemma degree_1 [simp]: "degree 1 = 0"
   unfolding one_poly_def
@@ -2854,6 +2870,14 @@
   shows "pcompose p [: 0, 1 :] = p"
   by (induct p; simp add: pcompose_pCons)
 
+lemma pcompose_setsum: "pcompose (setsum f A) p = setsum (\<lambda>i. pcompose (f i) p) A"
+  by (cases "finite A", induction rule: finite_induct)
+     (simp_all add: pcompose_1 pcompose_add)
+
+lemma pcompose_setprod: "pcompose (setprod f A) p = setprod (\<lambda>i. pcompose (f i) p) A"
+  by (cases "finite A", induction rule: finite_induct)
+     (simp_all add: pcompose_1 pcompose_mult)
+
 
 (* The remainder of this section and the next were contributed by Wenda Li *)
 
@@ -2940,6 +2964,12 @@
 lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
   unfolding lead_coeff_def by auto
 
+lemma coeff_0_listprod: "coeff (listprod xs) 0 = listprod (map (\<lambda>p. coeff p 0) xs)"
+  by (induction xs) (simp_all add: coeff_mult)
+
+lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
+  by (induction n) (simp_all add: coeff_mult)
+
 lemma lead_coeff_mult:
    fixes p q::"'a ::idom poly"
    shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
@@ -3015,6 +3045,200 @@
   by (simp add: lead_coeff_def)
 
 
+subsection \<open>Shifting polynomials\<close>
+
+definition poly_shift :: "nat \<Rightarrow> ('a::zero) poly \<Rightarrow> 'a poly" where
+  "poly_shift n p = Abs_poly (\<lambda>i. coeff p (i + n))"
+
+lemma nth_default_drop: "nth_default x (drop n xs) m = nth_default x xs (m + n)"
+  by (auto simp add: nth_default_def add_ac)
+  
+lemma nth_default_take: "nth_default x (take n xs) m = (if m < n then nth_default x xs m else x)"
+  by (auto simp add: nth_default_def add_ac)
+  
+  
+lemma coeff_poly_shift: "coeff (poly_shift n p) i = coeff p (i + n)"
+proof -
+  from MOST_coeff_eq_0[of p] obtain m where "\<forall>k>m. coeff p k = 0" by (auto simp: MOST_nat)
+  hence "\<forall>k>m. coeff p (k + n) = 0" by auto
+  hence "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0" by (auto simp: MOST_nat)
+  thus ?thesis by (simp add: poly_shift_def poly.Abs_poly_inverse)
+qed
+
+lemma poly_shift_id [simp]: "poly_shift 0 = (\<lambda>x. x)"
+  by (simp add: poly_eq_iff fun_eq_iff coeff_poly_shift)
+
+lemma poly_shift_0 [simp]: "poly_shift n 0 = 0"
+  by (simp add: poly_eq_iff coeff_poly_shift)
+  
+lemma poly_shift_1: "poly_shift n 1 = (if n = 0 then 1 else 0)"
+  by (simp add: poly_eq_iff coeff_poly_shift)
+
+lemma poly_shift_monom: "poly_shift n (monom c m) = (if m \<ge> n then monom c (m - n) else 0)"
+  by (auto simp add: poly_eq_iff coeff_poly_shift)
+
+lemma coeffs_shift_poly [code abstract]: "coeffs (poly_shift n p) = drop n (coeffs p)"
+proof (cases "p = 0")
+  case False
+  thus ?thesis
+    by (intro coeffs_eqI)
+       (simp_all add: coeff_poly_shift nth_default_drop last_coeffs_not_0 nth_default_coeffs_eq)
+qed simp_all
+
+
+subsection \<open>Truncating polynomials\<close>
+
+definition poly_cutoff where
+  "poly_cutoff n p = Abs_poly (\<lambda>k. if k < n then coeff p k else 0)"
+
+lemma coeff_poly_cutoff: "coeff (poly_cutoff n p) k = (if k < n then coeff p k else 0)"
+  unfolding poly_cutoff_def
+  by (subst poly.Abs_poly_inverse) (auto simp: MOST_nat intro: exI[of _ n])
+
+lemma poly_cutoff_0 [simp]: "poly_cutoff n 0 = 0"
+  by (simp add: poly_eq_iff coeff_poly_cutoff)
+
+lemma poly_cutoff_1 [simp]: "poly_cutoff n 1 = (if n = 0 then 0 else 1)"
+  by (simp add: poly_eq_iff coeff_poly_cutoff)
+
+lemma coeffs_poly_cutoff [code abstract]: 
+  "coeffs (poly_cutoff n p) = strip_while (op = 0) (take n (coeffs p))"
+proof (cases "strip_while (op = 0) (take n (coeffs p)) = []")
+  case True
+  hence "coeff (poly_cutoff n p) k = 0" for k
+    unfolding coeff_poly_cutoff
+    by (auto simp: nth_default_coeffs_eq [symmetric] nth_default_def set_conv_nth)
+  hence "poly_cutoff n p = 0" by (simp add: poly_eq_iff)
+  thus ?thesis by (subst True) simp_all
+next
+  case False
+  have "no_trailing (op = 0) (strip_while (op = 0) (take n (coeffs p)))" by simp
+  with False have "last (strip_while (op = 0) (take n (coeffs p))) \<noteq> 0" 
+    unfolding no_trailing_unfold by auto
+  thus ?thesis
+    by (intro coeffs_eqI)
+       (simp_all add: coeff_poly_cutoff last_coeffs_not_0 nth_default_take nth_default_coeffs_eq)
+qed
+
+
+subsection \<open>Reflecting polynomials\<close>
+
+definition reflect_poly where
+  "reflect_poly p = Poly (rev (coeffs p))"
+  
+lemma coeffs_reflect_poly [code abstract]:
+    "coeffs (reflect_poly p) = rev (dropWhile (op = 0) (coeffs p))"
+  unfolding reflect_poly_def by simp
+  
+lemma reflect_poly_0 [simp]: "reflect_poly 0 = 0"
+  by (simp add: reflect_poly_def)
+
+lemma reflect_poly_1 [simp]: "reflect_poly 1 = 1"
+  by (simp add: reflect_poly_def one_poly_def)
+
+lemma coeff_reflect_poly:
+  "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))"
+  by (cases "p = 0") (auto simp add: reflect_poly_def coeff_Poly_eq nth_default_def
+                                     rev_nth degree_eq_length_coeffs coeffs_nth not_less
+                                dest: le_imp_less_Suc)
+
+lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
+  by (simp add: coeff_reflect_poly)
+
+lemma reflect_poly_at_0_eq_0_iff [simp]: "poly (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
+  by (simp add: coeff_reflect_poly poly_0_coeff_0)
+
+lemma reflect_poly_pCons':
+  "p \<noteq> 0 \<Longrightarrow> reflect_poly (pCons c p) = reflect_poly p + monom c (Suc (degree p))"
+  by (intro poly_eqI)
+     (auto simp: coeff_reflect_poly coeff_pCons not_less Suc_diff_le split: nat.split)
+
+lemma reflect_poly_const [simp]: "reflect_poly [:a:] = [:a:]"
+  by (cases "a = 0") (simp_all add: reflect_poly_def)
+
+lemma poly_reflect_poly_nz:
+  "(x :: 'a :: field) \<noteq> 0 \<Longrightarrow> poly (reflect_poly p) x = x ^ degree p * poly p (inverse x)"
+  by (induction rule: pCons_induct) (simp_all add: field_simps reflect_poly_pCons' poly_monom)
+
+lemma coeff_0_reflect_poly [simp]: "coeff (reflect_poly p) 0 = lead_coeff p"
+  by (simp add: coeff_reflect_poly lead_coeff_def)
+
+lemma poly_reflect_poly_0 [simp]: "poly (reflect_poly p) 0 = lead_coeff p"
+  by (simp add: poly_0_coeff_0)
+
+lemma reflect_poly_reflect_poly [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> reflect_poly (reflect_poly p) = p"
+  by (cases p rule: pCons_cases) (simp add: reflect_poly_def )
+
+lemma degree_reflect_poly_le: "degree (reflect_poly p) \<le> degree p"
+  by (simp add: degree_eq_length_coeffs coeffs_reflect_poly length_dropWhile_le diff_le_mono)
+
+lemma reflect_poly_pCons:
+  "a \<noteq> 0 \<Longrightarrow> reflect_poly (pCons a p) = Poly (rev (a # coeffs p))"
+  by (subst coeffs_eq_iff) (simp add: coeffs_reflect_poly)
+  
+lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
+  by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)
+  
+(* TODO: does this work for non-idom as well? *)
+lemma reflect_poly_mult:
+  "reflect_poly (p * q) = reflect_poly p * reflect_poly (q :: _ :: idom poly)"
+proof (cases "p = 0 \<or> q = 0")
+  case False
+  hence [simp]: "p \<noteq> 0" "q \<noteq> 0" by auto
+  show ?thesis
+  proof (rule poly_eqI)
+    fix i :: nat
+    show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i"
+    proof (cases "i \<le> degree (p * q)")
+      case True
+      def A \<equiv> "{..i} \<inter> {i - degree q..degree p}"
+      def B \<equiv> "{..degree p} \<inter> {degree p - i..degree (p*q) - i}"
+      let ?f = "\<lambda>j. degree p - j"
+
+      from True have "coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)"
+        by (simp add: coeff_reflect_poly)
+      also have "\<dots> = (\<Sum>j\<le>degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))"
+        unfolding coeff_mult by simp
+      also have "\<dots> = (\<Sum>j\<in>B. coeff p j * coeff q (degree (p * q) - i - j))"
+        by (intro setsum.mono_neutral_right) (auto simp: B_def degree_mult_eq not_le coeff_eq_0)
+      also from True have "\<dots> = (\<Sum>j\<in>A. coeff p (degree p - j) * coeff q (degree q - (i - j)))"
+        by (intro setsum.reindex_bij_witness[of _ ?f ?f])
+           (auto simp: A_def B_def degree_mult_eq add_ac)
+      also have "\<dots> = (\<Sum>j\<le>i. if j \<in> {i - degree q..degree p} then
+                 coeff p (degree p - j) * coeff q (degree q - (i - j)) else 0)"
+        by (subst setsum.inter_restrict [symmetric]) (simp_all add: A_def)
+       also have "\<dots> = coeff (reflect_poly p * reflect_poly q) i"
+          by (fastforce simp: coeff_mult coeff_reflect_poly intro!: setsum.cong)
+       finally show ?thesis .
+    qed (auto simp: coeff_mult coeff_reflect_poly coeff_eq_0 degree_mult_eq intro!: setsum.neutral)
+  qed
+qed auto
+
+lemma reflect_poly_smult: 
+  "reflect_poly (Polynomial.smult (c::'a::idom) p) = Polynomial.smult c (reflect_poly p)"
+  using reflect_poly_mult[of "[:c:]" p] by simp
+
+lemma reflect_poly_power:
+    "reflect_poly (p ^ n :: 'a :: idom poly) = reflect_poly p ^ n"
+  by (induction n) (simp_all add: reflect_poly_mult)
+
+lemma reflect_poly_setprod:
+  "reflect_poly (setprod (f :: _ \<Rightarrow> _ :: idom poly) A) = setprod (\<lambda>x. reflect_poly (f x)) A"
+  by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)
+
+lemma reflect_poly_listprod:
+  "reflect_poly (listprod (xs :: _ :: idom poly list)) = listprod (map reflect_poly xs)"
+  by (induction xs) (simp_all add: reflect_poly_mult)
+
+lemma reflect_poly_Poly_nz: 
+  "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0 \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
+  unfolding reflect_poly_def coeffs_Poly by simp
+
+lemmas reflect_poly_simps = 
+  reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
+  reflect_poly_power reflect_poly_setprod reflect_poly_listprod
+
+
 subsection \<open>Derivatives of univariate polynomials\<close>
 
 function pderiv :: "('a :: semidom) poly \<Rightarrow> 'a poly"
@@ -3545,6 +3769,15 @@
   ultimately show ?case using Suc by auto
 qed
 
+lemma order_0_monom [simp]:
+  assumes "c \<noteq> 0"
+  shows   "order 0 (monom c n) = n"
+  using assms order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult)
+
+lemma dvd_imp_order_le:
+  "q \<noteq> 0 \<Longrightarrow> p dvd q \<Longrightarrow> Polynomial.order a p \<le> Polynomial.order a q"
+  by (auto simp: order_mult elim: dvdE)
+
 text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>
 
 lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
@@ -3554,6 +3787,11 @@
 apply (erule power_le_dvd [OF order_1])
 done
 
+lemma monom_1_dvd_iff:
+  assumes "p \<noteq> 0"
+  shows   "monom 1 n dvd p \<longleftrightarrow> n \<le> Polynomial.order 0 p"
+  using assms order_divides[of 0 n p] by (simp add: monom_altdef)
+
 lemma poly_squarefree_decomp_order:
   assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
   and p: "p = q * d"
@@ -3639,6 +3877,35 @@
     by (simp add: rsquarefree_def order_root)
 qed
 
+lemma coeff_monom_mult: 
+  "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
+proof -
+  have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k - i))"
+    by (simp add: coeff_mult)
+  also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
+    by (intro setsum.cong) simp_all
+  also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))" by (simp add: setsum.delta')
+  finally show ?thesis .
+qed
+
+lemma monom_1_dvd_iff':
+  "monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)"
+proof
+  assume "monom 1 n dvd p"
+  then obtain r where r: "p = monom 1 n * r" by (elim dvdE)
+  thus "\<forall>k<n. coeff p k = 0" by (simp add: coeff_mult)
+next
+  assume zero: "(\<forall>k<n. coeff p k = 0)"
+  define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))"
+  have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
+    by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, 
+        subst cofinite_eq_sequentially [symmetric]) transfer
+  hence coeff_r [simp]: "coeff r k = coeff p (k + n)" for k unfolding r_def
+    by (subst poly.Abs_poly_inverse) simp_all
+  have "p = monom 1 n * r"
+    by (intro poly_eqI, subst coeff_monom_mult) (insert zero, simp_all)
+  thus "monom 1 n dvd p" by simp
+qed
 
 no_notation cCons (infixr "##" 65)
 
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Library/Polynomial_FPS.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Polynomial_FPS.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -0,0 +1,313 @@
+(*
+  File:      Polynomial_FPS.thy
+  Author:    Manuel Eberl (TUM)
+  
+  Converting polynomials to formal power series
+*)
+
+section \<open>Converting polynomials to formal power series\<close>
+theory Polynomial_FPS
+imports Polynomial Formal_Power_Series
+begin
+
+definition fps_from_poly where
+  "fps_from_poly p = Abs_fps (coeff p)"
+
+lemma fps_from_poly_eq_iff: "fps_from_poly p = fps_from_poly q \<longleftrightarrow> p = q"
+  by (simp add: fps_from_poly_def poly_eq_iff fps_eq_iff)
+
+lemma fps_from_poly_nth [simp]: "fps_from_poly p $ n = coeff p n"
+  by (simp add: fps_from_poly_def)
+  
+lemma fps_from_poly_const: "fps_from_poly [:c:] = fps_const c"
+proof (subst fps_eq_iff, clarify)
+  fix n :: nat show "fps_from_poly [:c:] $ n = fps_const c $ n"
+    by (cases n) (auto simp: fps_from_poly_def)
+qed
+
+lemma fps_from_poly_0 [simp]: "fps_from_poly 0 = 0"
+  by (subst fps_const_0_eq_0 [symmetric], subst fps_from_poly_const [symmetric]) simp
+
+lemma fps_from_poly_1 [simp]: "fps_from_poly 1 = 1"
+  by (subst fps_const_1_eq_1 [symmetric], subst fps_from_poly_const [symmetric])
+     (simp add: one_poly_def)
+
+lemma fps_from_poly_1' [simp]: "fps_from_poly [:1:] = 1"
+  by (subst fps_const_1_eq_1 [symmetric], subst fps_from_poly_const [symmetric])
+     (simp add: one_poly_def)
+
+lemma fps_from_poly_numeral [simp]: "fps_from_poly (numeral n) = numeral n"
+  by (simp add: numeral_fps_const fps_from_poly_const [symmetric] numeral_poly)
+
+lemma fps_from_poly_numeral' [simp]: "fps_from_poly [:numeral n:] = numeral n"
+  by (simp add: numeral_fps_const fps_from_poly_const [symmetric] numeral_poly)
+
+lemma fps_from_poly_X [simp]: "fps_from_poly [:0, 1:] = X"
+  by (auto simp add: fps_from_poly_def fps_eq_iff coeff_pCons split: nat.split)
+
+lemma fps_from_poly_add: "fps_from_poly (p + q) = fps_from_poly p + fps_from_poly q"
+  by (simp add: fps_from_poly_def plus_poly.rep_eq fps_plus_def)
+
+lemma fps_from_poly_diff: "fps_from_poly (p - q) = fps_from_poly p - fps_from_poly q"
+  by (simp add: fps_from_poly_def minus_poly.rep_eq fps_minus_def)
+
+lemma fps_from_poly_uminus: "fps_from_poly (-p) = -fps_from_poly p"
+  by (simp add: fps_from_poly_def uminus_poly.rep_eq fps_uminus_def)
+
+lemma fps_from_poly_mult: "fps_from_poly (p * q) = fps_from_poly p * fps_from_poly q"
+  by (simp add: fps_from_poly_def fps_times_def fps_eq_iff coeff_mult atLeast0AtMost)
+
+lemma fps_from_poly_smult: 
+  "fps_from_poly (smult c p) = fps_const c * fps_from_poly p"
+  using fps_from_poly_mult[of "[:c:]" p] by (simp add: fps_from_poly_mult fps_from_poly_const)
+  
+lemma fps_from_poly_setsum: "fps_from_poly (setsum f A) = setsum (\<lambda>x. fps_from_poly (f x)) A"
+  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_from_poly_add)
+
+lemma fps_from_poly_listsum: "fps_from_poly (listsum xs) = listsum (map fps_from_poly xs)"
+  by (induction xs) (simp_all add: fps_from_poly_add)
+  
+lemma fps_from_poly_setprod: "fps_from_poly (setprod f A) = setprod (\<lambda>x. fps_from_poly (f x)) A"
+  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_from_poly_mult)
+  
+lemma fps_from_poly_listprod: "fps_from_poly (listprod xs) = listprod (map fps_from_poly xs)"
+  by (induction xs) (simp_all add: fps_from_poly_mult)
+
+lemma fps_from_poly_pCons: 
+  "fps_from_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_from_poly p * X"
+  by (subst fps_mult_X_commute [symmetric], intro fps_ext) 
+     (auto simp: fps_from_poly_def coeff_pCons split: nat.split)
+  
+lemma fps_from_poly_pderiv: "fps_from_poly (pderiv p) = fps_deriv (fps_from_poly p)"
+  by (intro fps_ext) (simp add: fps_from_poly_nth coeff_pderiv)
+
+lemma fps_from_poly_power: "fps_from_poly (p ^ n) = fps_from_poly p ^ n"
+  by (induction n) (simp_all add: fps_from_poly_mult)
+  
+lemma fps_from_poly_monom: "fps_from_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
+  by (intro fps_ext) simp_all
+
+lemma fps_from_poly_monom': "fps_from_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n"
+  by (simp add: fps_from_poly_monom)
+
+lemma fps_from_poly_div:
+  assumes "(q :: 'a :: field poly) dvd p"
+  shows   "fps_from_poly (p div q) = fps_from_poly p / fps_from_poly q"
+proof (cases "q = 0")
+  case False
+  from False fps_from_poly_eq_iff[of q 0] have nz: "fps_from_poly q \<noteq> 0" by simp 
+  from assms have "p = (p div q) * q" by simp
+  also have "fps_from_poly \<dots> = fps_from_poly (p div q) * fps_from_poly q" 
+    by (simp add: fps_from_poly_mult)
+  also from nz have "\<dots> / fps_from_poly q = fps_from_poly (p div q)"
+    by (intro div_mult_self2_is_id) (auto simp: fps_from_poly_0)
+  finally show ?thesis ..
+qed simp
+
+lemma fps_from_poly_divide_numeral:
+  "fps_from_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_from_poly p / numeral c"
+proof -
+  have "smult (inverse (numeral c)) p = [:inverse (numeral c):] * p" by simp
+  also have "fps_from_poly \<dots> = fps_from_poly p / numeral c"
+    by (subst fps_from_poly_mult) (simp add: numeral_fps_const fps_from_poly_pCons)
+  finally show ?thesis by simp
+qed
+
+
+lemma subdegree_fps_from_poly:
+  assumes "p \<noteq> 0"
+  defines "n \<equiv> Polynomial.order 0 p"
+  shows   "subdegree (fps_from_poly p) = n"
+proof (rule subdegreeI)
+  from assms have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff)
+  thus zero: "fps_from_poly p $ i = 0" if "i < n" for i
+    using that by (simp add: monom_1_dvd_iff')
+    
+  from assms have "\<not>monom 1 (Suc n) dvd p"
+    by (auto simp: monom_1_dvd_iff simp del: power_Suc)
+  then obtain k where "k \<le> n" "fps_from_poly p $ k \<noteq> 0" 
+    by (auto simp: monom_1_dvd_iff' less_Suc_eq_le)
+  moreover from this and zero[of k] have "k = n" by linarith
+  ultimately show "fps_from_poly p $ n \<noteq> 0" by simp
+qed
+
+lemma fps_from_poly_dvd:
+  assumes "p dvd q"
+  shows   "fps_from_poly (p :: 'a :: field poly) dvd fps_from_poly q"
+proof (cases "p = 0 \<or> q = 0")
+  case False
+  with assms fps_from_poly_eq_iff[of p 0] fps_from_poly_eq_iff[of q 0] show ?thesis
+    by (auto simp: fps_dvd_iff subdegree_fps_from_poly dvd_imp_order_le)
+qed (insert assms, auto)
+
+
+lemmas fps_from_poly_simps =
+  fps_from_poly_0 fps_from_poly_1 fps_from_poly_numeral fps_from_poly_const fps_from_poly_X
+  fps_from_poly_add fps_from_poly_diff fps_from_poly_uminus fps_from_poly_mult fps_from_poly_smult
+  fps_from_poly_setsum fps_from_poly_listsum fps_from_poly_setprod fps_from_poly_listprod
+  fps_from_poly_pCons fps_from_poly_pderiv fps_from_poly_power fps_from_poly_monom
+  fps_from_poly_divide_numeral
+
+lemma fps_from_poly_pcompose:
+  assumes "coeff q 0 = (0 :: 'a :: idom)"
+  shows   "fps_from_poly (pcompose p q) = fps_compose (fps_from_poly p) (fps_from_poly q)"
+  using assms by (induction p rule: pCons_induct)
+                 (auto simp: pcompose_pCons fps_from_poly_simps fps_from_poly_pCons 
+                             fps_compose_add_distrib fps_compose_mult_distrib)
+  
+lemmas reify_fps_atom =
+  fps_from_poly_0 fps_from_poly_1' fps_from_poly_numeral' fps_from_poly_const fps_from_poly_X
+
+
+text \<open>
+  The following simproc can reduce the equality of two polynomial FPSs two equality of the
+  respective polynomials. A polynomial FPS is one that only has finitely many non-zero 
+  coefficients and can therefore be written as @{term "fps_from_poly p"} for some 
+  polynomial @{text "p"}.
+  
+  This may sound trivial, but it covers a number of annoying side conditions like 
+  @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.
+\<close>
+
+ML \<open>
+
+(* TODO: Support for division *)
+signature POLY_FPS = sig
+
+val reify_conv : conv
+val eq_conv : conv
+val eq_simproc : cterm -> thm option
+
+end
+
+
+structure Poly_Fps = struct
+
+fun const_binop_conv s conv ct =
+  case Thm.term_of ct of
+    (Const (s', _) $ _ $ _) => 
+      if s = s' then 
+        Conv.binop_conv conv ct 
+      else 
+        raise CTERM ("const_binop_conv", [ct])
+  | _ => raise CTERM ("const_binop_conv", [ct])
+
+fun reify_conv ct = 
+  let
+    val rewr = Conv.rewrs_conv o map (fn thm => thm RS @{thm eq_reflection})
+    val un = Conv.arg_conv reify_conv
+    val bin = Conv.binop_conv reify_conv
+  in
+    case Thm.term_of ct of
+      (Const (@{const_name "fps_from_poly"}, _) $ _) => ct |> Conv.all_conv
+    | (Const (@{const_name "Groups.plus"}, _) $ _ $ _) => ct |> (
+        bin then_conv rewr @{thms fps_from_poly_add [symmetric]})
+    | (Const (@{const_name "Groups.uminus"}, _) $ _) => ct |> (
+        un then_conv rewr @{thms fps_from_poly_uminus [symmetric]})
+    | (Const (@{const_name "Groups.minus"}, _) $ _ $ _) => ct |> (
+        bin then_conv rewr @{thms fps_from_poly_diff [symmetric]})
+    | (Const (@{const_name "Groups.times"}, _) $ _ $ _) => ct |> (
+        bin then_conv rewr @{thms fps_from_poly_mult [symmetric]})
+    | (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _))
+        => ct |> (Conv.fun_conv (Conv.arg_conv reify_conv)
+             then_conv rewr @{thms fps_from_poly_divide_numeral [symmetric]})
+    | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct |> (
+        rewr @{thms fps_from_poly_monom' [symmetric]}) 
+    | (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> (
+        Conv.fun_conv (Conv.arg_conv reify_conv) 
+        then_conv rewr @{thms fps_from_poly_power [symmetric]})
+    | _ => ct |> (
+        rewr @{thms reify_fps_atom [symmetric]})
+  end
+    
+
+fun eq_conv ct =
+  case Thm.term_of ct of
+    (Const (@{const_name "HOL.eq"}, _) $ _ $ _) => ct |> (
+      Conv.binop_conv reify_conv
+      then_conv Conv.rewr_conv @{thm fps_from_poly_eq_iff[THEN eq_reflection]})
+  | _ => raise CTERM ("poly_fps_eq_conv", [ct])
+
+val eq_simproc = try eq_conv
+
+end
+\<close> 
+
+simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close>
+
+lemma fps_from_poly_linear: "fps_from_poly [:a,1 :: 'a :: field:] = X + fps_const a"
+  by simp
+
+lemma fps_from_poly_linear': "fps_from_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
+  by simp
+
+lemma fps_from_poly_cutoff [simp]: 
+  "fps_from_poly (poly_cutoff n p) = fps_cutoff n (fps_from_poly p)"
+  by (simp add: fps_eq_iff coeff_poly_cutoff)
+
+lemma fps_from_poly_shift [simp]: "fps_from_poly (poly_shift n p) = fps_shift n (fps_from_poly p)"
+  by (simp add: fps_eq_iff coeff_poly_shift)
+
+
+definition poly_subdegree :: "'a::zero poly \<Rightarrow> nat" where
+  "poly_subdegree p = subdegree (fps_from_poly p)"
+
+lemma coeff_less_poly_subdegree:
+  "k < poly_subdegree p \<Longrightarrow> coeff p k = 0"
+  unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_from_poly p"] by simp
+
+(* TODO: Move ? *)
+definition prefix_length :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" where
+  "prefix_length P xs = length (takeWhile P xs)"
+
+primrec prefix_length_aux :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+  "prefix_length_aux P acc [] = acc"
+| "prefix_length_aux P acc (x#xs) = (if P x then prefix_length_aux P (Suc acc) xs else acc)"
+
+lemma prefix_length_aux_correct: "prefix_length_aux P acc xs = prefix_length P xs + acc"
+  by (induction xs arbitrary: acc) (simp_all add: prefix_length_def)
+
+lemma prefix_length_code [code]: "prefix_length P xs = prefix_length_aux P 0 xs"
+  by (simp add: prefix_length_aux_correct)
+
+lemma prefix_length_le_length: "prefix_length P xs \<le> length xs"
+  by (induction xs) (simp_all add: prefix_length_def)
+  
+lemma prefix_length_less_length: "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> prefix_length P xs < length xs"
+  by (induction xs) (simp_all add: prefix_length_def)
+
+lemma nth_prefix_length:
+  "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> \<not>P (xs ! prefix_length P xs)"
+  by (induction xs) (simp_all add: prefix_length_def)
+  
+lemma nth_less_prefix_length:
+  "n < prefix_length P xs \<Longrightarrow> P (xs ! n)"
+  by (induction xs arbitrary: n) 
+     (auto simp: prefix_length_def nth_Cons split: if_splits nat.splits)
+(* END TODO *)
+  
+lemma poly_subdegree_code [code]: "poly_subdegree p = prefix_length (op = 0) (coeffs p)"
+proof (cases "p = 0")
+  case False
+  note [simp] = this
+  define n where "n = prefix_length (op = 0) (coeffs p)"
+  from False have "\<exists>k. coeff p k \<noteq> 0" by (auto simp: poly_eq_iff)
+  hence ex: "\<exists>x\<in>set (coeffs p). x \<noteq> 0" by (auto simp: coeffs_def)
+  hence n_less: "n < length (coeffs p)" and nonzero: "coeffs p ! n \<noteq> 0" 
+    unfolding n_def by (auto intro!: prefix_length_less_length nth_prefix_length)
+  show ?thesis unfolding poly_subdegree_def
+  proof (intro subdegreeI)
+    from n_less have "fps_from_poly p $ n = coeffs p ! n"
+      by (subst coeffs_nth) (simp_all add: degree_eq_length_coeffs)
+    with nonzero show "fps_from_poly p $ prefix_length (op = 0) (coeffs p) \<noteq> 0"
+      unfolding n_def by simp
+  next
+    fix k assume A: "k < prefix_length (op = 0) (coeffs p)"
+    also have "\<dots> \<le> length (coeffs p)" by (rule prefix_length_le_length)
+    finally show "fps_from_poly p $ k = 0"
+      using nth_less_prefix_length[OF A]
+      by (simp add: coeffs_nth degree_eq_length_coeffs)
+  qed
+qed (simp_all add: poly_subdegree_def prefix_length_def)
+
+end
diff -r 3b6975875633 -r ca187a9f66da src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/List.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -3039,6 +3039,9 @@
 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
 by(simp add:upt_conv_Cons)
 
+lemma tl_upt: "tl [m..<n] = [Suc m..<n]"
+  by (simp add: upt_rec)
+
 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
 by(cases j)(auto simp: upt_Suc_append)
 
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -71,6 +71,18 @@
   with assms(1) show False by contradiction
 qed
 
+lemma fraction_not_in_nats:
+  assumes "\<not>n dvd m" "n \<noteq> 0"
+  shows   "of_int m / of_int n \<notin> (\<nat> :: 'a :: {division_ring,ring_char_0} set)"
+proof
+  assume "of_int m / of_int n \<in> (\<nat> :: 'a set)"
+  also note Nats_subset_Ints
+  finally have "of_int m / of_int n \<in> (\<int> :: 'a set)" .
+  moreover have "of_int m / of_int n \<notin> (\<int> :: 'a set)"
+    using assms by (intro fraction_not_in_ints)
+  ultimately show False by contradiction
+qed
+
 lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \<notin> \<int> \<Longrightarrow> z \<notin> \<int>\<^sub>\<le>\<^sub>0"
   by (auto simp: Ints_def nonpos_Ints_def)
 
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -1907,6 +1907,9 @@
 lemma setprod_lessThan_Suc: "setprod f {..<Suc n} = setprod f {..<n} * f n"
   by (simp add: lessThan_Suc mult.commute)
 
+lemma setprod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
+  by (induction n) (simp_all add: lessThan_Suc mult_ac)
+
 lemma setprod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> setprod f {a..<Suc b} = setprod f {a..<b} * f b"
   by (simp add: atLeastLessThanSuc mult.commute)
 
diff -r 3b6975875633 -r ca187a9f66da src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -1008,6 +1008,9 @@
 apply (auto intro: less_trans)
 done
 
+lemma subseq_add: "subseq (\<lambda>n. n + k)"
+  by (auto simp: subseq_Suc_iff)
+
 text\<open>for any sequence, there is a monotonic subsequence\<close>
 lemma seq_monosub:
   fixes s :: "nat => 'a::linorder"