Various additions to polynomials, FPSs, Gamma function
authoreberlm
Thu Jun 16 17:57:09 2016 +0200 (2016-06-16)
changeset 63317ca187a9f66da
parent 63305 3b6975875633
child 63318 008db47be9dc
Various additions to polynomials, FPSs, Gamma function
src/HOL/Binomial.thy
src/HOL/Divides.thy
src/HOL/Groups_List.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Library.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Polynomial_FPS.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Gamma.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Binomial.thy	Wed Jun 15 15:52:24 2016 +0100
     1.2 +++ b/src/HOL/Binomial.thy	Thu Jun 16 17:57:09 2016 +0200
     1.3 @@ -672,6 +672,10 @@
     1.4    finally show ?case .
     1.5  qed simp
     1.6  
     1.7 +lemma fact_double:
     1.8 +  "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)"
     1.9 +  using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact)
    1.10 +
    1.11  lemma pochhammer_absorb_comp:
    1.12    "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
    1.13    (is "?lhs = ?rhs")
     2.1 --- a/src/HOL/Divides.thy	Wed Jun 15 15:52:24 2016 +0100
     2.2 +++ b/src/HOL/Divides.thy	Thu Jun 16 17:57:09 2016 +0200
     2.3 @@ -363,6 +363,23 @@
     2.4  lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
     2.5  by (blast intro: dvd_mod_imp_dvd dvd_mod)
     2.6  
     2.7 +lemma div_div_eq_right:
     2.8 +  assumes "c dvd b" "b dvd a"
     2.9 +  shows   "a div (b div c) = a div b * c"
    2.10 +proof -
    2.11 +  from assms have "a div b * c = (a * c) div b"
    2.12 +    by (subst dvd_div_mult) simp_all
    2.13 +  also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp
    2.14 +  also have "a * c div (b div c * c) = a div (b div c)"
    2.15 +    by (cases "c = 0") simp_all
    2.16 +  finally show ?thesis ..
    2.17 +qed
    2.18 +
    2.19 +lemma div_div_div_same:
    2.20 +  assumes "d dvd a" "d dvd b" "b dvd a"
    2.21 +  shows   "(a div d) div (b div d) = a div b"
    2.22 +  using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
    2.23 +
    2.24  end
    2.25  
    2.26  class ring_div = comm_ring_1 + semiring_div
     3.1 --- a/src/HOL/Groups_List.thy	Wed Jun 15 15:52:24 2016 +0100
     3.2 +++ b/src/HOL/Groups_List.thy	Thu Jun 16 17:57:09 2016 +0200
     3.3 @@ -369,6 +369,10 @@
     3.4    with assms(1) show ?thesis by simp
     3.5  qed
     3.6  
     3.7 +lemma listprod_zero_iff: 
     3.8 +  "listprod xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
     3.9 +  by (induction xs) simp_all
    3.10 +
    3.11  text \<open>Some syntactic sugar:\<close>
    3.12  
    3.13  syntax (ASCII)
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Jun 15 15:52:24 2016 +0100
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jun 16 17:57:09 2016 +0200
     4.3 @@ -248,6 +248,9 @@
     4.4  
     4.5  subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
     4.6  
     4.7 +lemma fps_square_nth: "(f^2) $ n = (\<Sum>k\<le>n. f $ k * f $ (n - k))"
     4.8 +  by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost)
     4.9 +
    4.10  lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)"
    4.11    by (simp add: expand_fps_eq)
    4.12  
    4.13 @@ -387,6 +390,10 @@
    4.14  lemma fps_numeral_nth_0 [simp]: "numeral n $ 0 = numeral n"
    4.15    by (simp add: numeral_fps_const)
    4.16  
    4.17 +lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
    4.18 +  by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
    4.19 +
    4.20 +
    4.21  
    4.22  subsection \<open>The eXtractor series X\<close>
    4.23  
    4.24 @@ -412,8 +419,18 @@
    4.25  qed
    4.26  
    4.27  lemma X_mult_right_nth[simp]:
    4.28 -    "((f :: 'a::comm_semiring_1 fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
    4.29 -  by (metis X_mult_nth mult.commute)
    4.30 +  "((a::'a::semiring_1 fps) * X) $ n = (if n = 0 then 0 else a $ (n - 1))"
    4.31 +proof -
    4.32 +  have "(a * X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
    4.33 +    by (simp add: fps_times_def X_def)
    4.34 +  also have "\<dots> = (\<Sum>i = 0..n. if i = n - 1 then if n = 0 then 0 else a $ i else 0)"
    4.35 +    by (intro setsum.cong) auto
    4.36 +  also have "\<dots> = (if n = 0 then 0 else a $ (n - 1))" by (simp add: setsum.delta)
    4.37 +  finally show ?thesis .
    4.38 +qed
    4.39 +
    4.40 +lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X" 
    4.41 +  by (simp add: fps_eq_iff)
    4.42  
    4.43  lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then 1::'a::comm_ring_1 else 0)"
    4.44  proof (induct k)
    4.45 @@ -1057,6 +1074,9 @@
    4.46      by (auto simp add: expand_fps_eq)
    4.47  qed
    4.48  
    4.49 +lemma fps_inverse_eq_0: "f$0 = 0 \<Longrightarrow> inverse (f :: 'a :: division_ring fps) = 0"
    4.50 +  by simp
    4.51 +  
    4.52  lemma setsum_zero_lemma:
    4.53    fixes n::nat
    4.54    assumes "0 < n"
    4.55 @@ -1311,6 +1331,16 @@
    4.56    thus "f dvd g" by (simp add: dvd_eq_mod_eq_0)
    4.57  qed (simp add: assms dvd_imp_subdegree_le)
    4.58  
    4.59 +lemma fps_shift_altdef:
    4.60 +  "fps_shift n f = (f :: 'a :: field fps) div X^n"
    4.61 +  by (simp add: fps_divide_def)
    4.62 +  
    4.63 +lemma fps_div_X_power_nth: "((f :: 'a :: field fps) div X^n) $ k = f $ (k + n)"
    4.64 +  by (simp add: fps_shift_altdef [symmetric])
    4.65 +
    4.66 +lemma fps_div_X_nth: "((f :: 'a :: field fps) div X) $ k = f $ Suc k"
    4.67 +  using fps_div_X_power_nth[of f 1] by simp
    4.68 +
    4.69  lemma fps_const_inverse: "inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
    4.70    by (cases "a \<noteq> 0", rule fps_inverse_unique) (auto simp: fps_eq_iff)
    4.71  
    4.72 @@ -1321,6 +1351,18 @@
    4.73    "inverse (numeral n :: ('a :: field_char_0) fps) = fps_const (inverse (numeral n))"
    4.74    by (intro fps_inverse_unique fps_ext) (simp_all add: fps_numeral_nth)
    4.75  
    4.76 +lemma fps_numeral_divide_divide:
    4.77 +  "x / numeral b / numeral c = (x / numeral (b * c) :: 'a :: field fps)"
    4.78 +  by (cases "numeral b = (0::'a)"; cases "numeral c = (0::'a)")
    4.79 +      (simp_all add: fps_divide_unit fps_inverse_mult [symmetric] numeral_fps_const numeral_mult 
    4.80 +                del: numeral_mult [symmetric])
    4.81 +
    4.82 +lemma fps_numeral_mult_divide:
    4.83 +  "numeral b * x / numeral c = (numeral b / numeral c * x :: 'a :: field fps)"
    4.84 +  by (cases "numeral c = (0::'a)") (simp_all add: fps_divide_unit numeral_fps_const)
    4.85 +
    4.86 +lemmas fps_numeral_simps = 
    4.87 +  fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
    4.88  
    4.89  
    4.90  
    4.91 @@ -1828,6 +1870,12 @@
    4.92    shows "f * inverse f = 1"
    4.93    by (metis mult.commute inverse_mult_eq_1 f0)
    4.94  
    4.95 +lemma fps_inverse_minus [simp]: "inverse (-f) = -inverse (f :: 'a :: field fps)"
    4.96 +  by (cases "f$0 = 0") (auto intro: fps_inverse_unique simp: inverse_mult_eq_1' fps_inverse_eq_0)
    4.97 +  
    4.98 +lemma divide_fps_const [simp]: "f / fps_const (c :: 'a :: field) = fps_const (inverse c) * f"
    4.99 +  by (cases "c = 0") (simp_all add: fps_divide_unit fps_const_inverse)
   4.100 +
   4.101  (* FIXME: The last part of this proof should go through by simp once we have a proper
   4.102     theorem collection for simplifying division on rings *)
   4.103  lemma fps_divide_deriv:
   4.104 @@ -1846,6 +1894,18 @@
   4.105  lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
   4.106    by (simp add: fps_inverse_gp fps_eq_iff X_def)
   4.107  
   4.108 +lemma fps_one_over_one_minus_X_squared:
   4.109 +  "inverse ((1 - X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))"
   4.110 +proof -
   4.111 +  have "inverse ((1 - X)^2 :: 'a fps) = fps_deriv (inverse (1 - X))"
   4.112 +    by (subst fps_inverse_deriv) (simp_all add: fps_inverse_power)
   4.113 +  also have "inverse (1 - X :: 'a fps) = Abs_fps (\<lambda>_. 1)"
   4.114 +    by (subst fps_inverse_gp' [symmetric]) simp
   4.115 +  also have "fps_deriv \<dots> = Abs_fps (\<lambda>n. of_nat (n + 1))"
   4.116 +    by (simp add: fps_deriv_def)
   4.117 +  finally show ?thesis .
   4.118 +qed
   4.119 +
   4.120  lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)"
   4.121    by (cases n) simp_all
   4.122  
   4.123 @@ -2307,6 +2367,157 @@
   4.124   finally show ?thesis .
   4.125  qed
   4.126  
   4.127 +lemma natpermute_max_card:
   4.128 +  assumes n0: "n \<noteq> 0"
   4.129 +  shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
   4.130 +  unfolding natpermute_contain_maximal
   4.131 +proof -
   4.132 +  let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
   4.133 +  let ?K = "{0 ..k}"
   4.134 +  have fK: "finite ?K"
   4.135 +    by simp
   4.136 +  have fAK: "\<forall>i\<in>?K. finite (?A i)"
   4.137 +    by auto
   4.138 +  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
   4.139 +    {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
   4.140 +  proof clarify
   4.141 +    fix i j
   4.142 +    assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j"
   4.143 +    have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
   4.144 +    proof -
   4.145 +      have "(replicate (k+1) 0 [i:=n] ! i) = n"
   4.146 +        using i by (simp del: replicate.simps)
   4.147 +      moreover
   4.148 +      have "(replicate (k+1) 0 [j:=n] ! i) = 0"
   4.149 +        using i ij by (simp del: replicate.simps)
   4.150 +      ultimately show ?thesis
   4.151 +        using eq n0 by (simp del: replicate.simps)
   4.152 +    qed
   4.153 +    then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
   4.154 +      by auto
   4.155 +  qed
   4.156 +  from card_UN_disjoint[OF fK fAK d]
   4.157 +  show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1"
   4.158 +    by simp
   4.159 +qed
   4.160 +
   4.161 +lemma fps_power_Suc_nth:
   4.162 +  fixes f :: "'a :: comm_ring_1 fps"
   4.163 +  assumes k: "k > 0"
   4.164 +  shows "(f ^ Suc m) $ k = 
   4.165 +           of_nat (Suc m) * (f $ k * (f $ 0) ^ m) +
   4.166 +           (\<Sum>v\<in>{v\<in>natpermute k (m+1). k \<notin> set v}. \<Prod>j = 0..m. f $ v ! j)"
   4.167 +proof -
   4.168 +  define A B 
   4.169 +    where "A = {v\<in>natpermute k (m+1). k \<in> set v}" 
   4.170 +      and  "B = {v\<in>natpermute k (m+1). k \<notin> set v}"
   4.171 +  have [simp]: "finite A" "finite B" "A \<inter> B = {}" by (auto simp: A_def B_def natpermute_finite)
   4.172 +
   4.173 +  from natpermute_max_card[of k m] k have card_A: "card A = m + 1" by (simp add: A_def)
   4.174 +  {
   4.175 +    fix v assume v: "v \<in> A"
   4.176 +    from v have [simp]: "length v = Suc m" by (simp add: A_def natpermute_def)
   4.177 +    from v have "\<exists>j. j \<le> m \<and> v ! j = k" 
   4.178 +      by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le)
   4.179 +    then guess j by (elim exE conjE) note j = this
   4.180 +    
   4.181 +    from v have "k = listsum v" by (simp add: A_def natpermute_def)
   4.182 +    also have "\<dots> = (\<Sum>i=0..m. v ! i)"
   4.183 +      by (simp add: listsum_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
   4.184 +    also from j have "{0..m} = insert j ({0..m}-{j})" by auto
   4.185 +    also from j have "(\<Sum>i\<in>\<dots>. v ! i) = k + (\<Sum>i\<in>{0..m}-{j}. v ! i)"
   4.186 +      by (subst setsum.insert) simp_all
   4.187 +    finally have "(\<Sum>i\<in>{0..m}-{j}. v ! i) = 0" by simp
   4.188 +    hence zero: "v ! i = 0" if "i \<in> {0..m}-{j}" for i using that
   4.189 +      by (subst (asm) setsum_eq_0_iff) auto
   4.190 +      
   4.191 +    from j have "{0..m} = insert j ({0..m} - {j})" by auto
   4.192 +    also from j have "(\<Prod>i\<in>\<dots>. f $ (v ! i)) = f $ k * (\<Prod>i\<in>{0..m} - {j}. f $ (v ! i))"
   4.193 +      by (subst setprod.insert) auto
   4.194 +    also have "(\<Prod>i\<in>{0..m} - {j}. f $ (v ! i)) = (\<Prod>i\<in>{0..m} - {j}. f $ 0)"
   4.195 +      by (intro setprod.cong) (simp_all add: zero)
   4.196 +    also from j have "\<dots> = (f $ 0) ^ m" by (subst setprod_constant) simp_all
   4.197 +    finally have "(\<Prod>j = 0..m. f $ (v ! j)) = f $ k * (f $ 0) ^ m" .
   4.198 +  } note A = this
   4.199 +  
   4.200 +  have "(f ^ Suc m) $ k = (\<Sum>v\<in>natpermute k (m + 1). \<Prod>j = 0..m. f $ v ! j)"
   4.201 +    by (rule fps_power_nth_Suc)
   4.202 +  also have "natpermute k (m+1) = A \<union> B" unfolding A_def B_def by blast
   4.203 +  also have "(\<Sum>v\<in>\<dots>. \<Prod>j = 0..m. f $ (v ! j)) = 
   4.204 +               (\<Sum>v\<in>A. \<Prod>j = 0..m. f $ (v ! j)) + (\<Sum>v\<in>B. \<Prod>j = 0..m. f $ (v ! j))"
   4.205 +    by (intro setsum.union_disjoint) simp_all   
   4.206 +  also have "(\<Sum>v\<in>A. \<Prod>j = 0..m. f $ (v ! j)) = of_nat (Suc m) * (f $ k * (f $ 0) ^ m)"
   4.207 +    by (simp add: A card_A)
   4.208 +  finally show ?thesis by (simp add: B_def)
   4.209 +qed 
   4.210 +  
   4.211 +lemma fps_power_Suc_eqD:
   4.212 +  fixes f g :: "'a :: {idom,semiring_char_0} fps"
   4.213 +  assumes "f ^ Suc m = g ^ Suc m" "f $ 0 = g $ 0" "f $ 0 \<noteq> 0"
   4.214 +  shows   "f = g"
   4.215 +proof (rule fps_ext)
   4.216 +  fix k :: nat
   4.217 +  show "f $ k = g $ k"
   4.218 +  proof (induction k rule: less_induct)
   4.219 +    case (less k)
   4.220 +    show ?case
   4.221 +    proof (cases "k = 0")
   4.222 +      case False
   4.223 +      let ?h = "\<lambda>f. (\<Sum>v | v \<in> natpermute k (m + 1) \<and> k \<notin> set v. \<Prod>j = 0..m. f $ v ! j)"
   4.224 +      from False fps_power_Suc_nth[of k f m] fps_power_Suc_nth[of k g m]
   4.225 +        have "f $ k * (of_nat (Suc m) * (f $ 0) ^ m) + ?h f =
   4.226 +                g $ k * (of_nat (Suc m) * (f $ 0) ^ m) + ?h g" using assms 
   4.227 +        by (simp add: mult_ac del: power_Suc of_nat_Suc)
   4.228 +      also have "v ! i < k" if "v \<in> {v\<in>natpermute k (m+1). k \<notin> set v}" "i \<le> m" for v i
   4.229 +        using that elem_le_listsum_nat[of i v] unfolding natpermute_def
   4.230 +        by (auto simp: set_conv_nth dest!: spec[of _ i])
   4.231 +      hence "?h f = ?h g"
   4.232 +        by (intro setsum.cong refl setprod.cong less lessI) (auto simp: natpermute_def)
   4.233 +      finally have "f $ k * (of_nat (Suc m) * (f $ 0) ^ m) = g $ k * (of_nat (Suc m) * (f $ 0) ^ m)"
   4.234 +        by simp
   4.235 +      with assms show "f $ k = g $ k" 
   4.236 +        by (subst (asm) mult_right_cancel) (auto simp del: of_nat_Suc)
   4.237 +    qed (simp_all add: assms)
   4.238 +  qed
   4.239 +qed
   4.240 +
   4.241 +lemma fps_power_Suc_eqD':
   4.242 +  fixes f g :: "'a :: {idom,semiring_char_0} fps"
   4.243 +  assumes "f ^ Suc m = g ^ Suc m" "f $ subdegree f = g $ subdegree g"
   4.244 +  shows   "f = g"
   4.245 +proof (cases "f = 0")
   4.246 +  case False
   4.247 +  have "Suc m * subdegree f = subdegree (f ^ Suc m)"
   4.248 +    by (rule subdegree_power [symmetric])
   4.249 +  also have "f ^ Suc m = g ^ Suc m" by fact
   4.250 +  also have "subdegree \<dots> = Suc m * subdegree g" by (rule subdegree_power)
   4.251 +  finally have [simp]: "subdegree f = subdegree g"
   4.252 +    by (subst (asm) Suc_mult_cancel1)
   4.253 +  have "fps_shift (subdegree f) f * X ^ subdegree f = f"
   4.254 +    by (rule subdegree_decompose [symmetric])
   4.255 +  also have "\<dots> ^ Suc m = g ^ Suc m" by fact
   4.256 +  also have "g = fps_shift (subdegree g) g * X ^ subdegree g"
   4.257 +    by (rule subdegree_decompose)
   4.258 +  also have "subdegree f = subdegree g" by fact
   4.259 +  finally have "fps_shift (subdegree g) f ^ Suc m = fps_shift (subdegree g) g ^ Suc m"
   4.260 +    by (simp add: algebra_simps power_mult_distrib del: power_Suc)
   4.261 +  hence "fps_shift (subdegree g) f = fps_shift (subdegree g) g"
   4.262 +    by (rule fps_power_Suc_eqD) (insert assms False, auto)
   4.263 +  with subdegree_decompose[of f] subdegree_decompose[of g] show ?thesis by simp
   4.264 +qed (insert assms, simp_all)
   4.265 +
   4.266 +lemma fps_power_eqD':
   4.267 +  fixes f g :: "'a :: {idom,semiring_char_0} fps"
   4.268 +  assumes "f ^ m = g ^ m" "f $ subdegree f = g $ subdegree g" "m > 0"
   4.269 +  shows   "f = g"
   4.270 +  using fps_power_Suc_eqD'[of f "m-1" g] assms by simp
   4.271 +
   4.272 +lemma fps_power_eqD:
   4.273 +  fixes f g :: "'a :: {idom,semiring_char_0} fps"
   4.274 +  assumes "f ^ m = g ^ m" "f $ 0 = g $ 0" "f $ 0 \<noteq> 0" "m > 0"
   4.275 +  shows   "f = g"
   4.276 +  by (rule fps_power_eqD'[of f m g]) (insert assms, simp_all)
   4.277 +
   4.278  lemma fps_compose_inj_right:
   4.279    assumes a0: "a$0 = (0::'a::idom)"
   4.280      and a1: "a$1 \<noteq> 0"
   4.281 @@ -2442,40 +2653,6 @@
   4.282      using Suc by simp
   4.283  qed
   4.284  
   4.285 -lemma natpermute_max_card:
   4.286 -  assumes n0: "n \<noteq> 0"
   4.287 -  shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
   4.288 -  unfolding natpermute_contain_maximal
   4.289 -proof -
   4.290 -  let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
   4.291 -  let ?K = "{0 ..k}"
   4.292 -  have fK: "finite ?K"
   4.293 -    by simp
   4.294 -  have fAK: "\<forall>i\<in>?K. finite (?A i)"
   4.295 -    by auto
   4.296 -  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
   4.297 -    {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
   4.298 -  proof clarify
   4.299 -    fix i j
   4.300 -    assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j"
   4.301 -    have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
   4.302 -    proof -
   4.303 -      have "(replicate (k+1) 0 [i:=n] ! i) = n"
   4.304 -        using i by (simp del: replicate.simps)
   4.305 -      moreover
   4.306 -      have "(replicate (k+1) 0 [j:=n] ! i) = 0"
   4.307 -        using i ij by (simp del: replicate.simps)
   4.308 -      ultimately show ?thesis
   4.309 -        using eq n0 by (simp del: replicate.simps)
   4.310 -    qed
   4.311 -    then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
   4.312 -      by auto
   4.313 -  qed
   4.314 -  from card_UN_disjoint[OF fK fAK d]
   4.315 -  show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1"
   4.316 -    by simp
   4.317 -qed
   4.318 -
   4.319  lemma power_radical:
   4.320    fixes a:: "'a::field_char_0 fps"
   4.321    assumes a0: "a$0 \<noteq> 0"
   4.322 @@ -3213,6 +3390,21 @@
   4.323    apply (simp add: fps_compose_mult_distrib[OF c0])
   4.324    done
   4.325  
   4.326 +lemma fps_compose_divide:
   4.327 +  assumes [simp]: "g dvd f" "h $ 0 = 0"
   4.328 +  shows   "fps_compose f h = fps_compose (f / g :: 'a :: field fps) h * fps_compose g h"
   4.329 +proof -
   4.330 +  have "f = (f / g) * g" by simp
   4.331 +  also have "fps_compose \<dots> h = fps_compose (f / g) h * fps_compose g h"
   4.332 +    by (subst fps_compose_mult_distrib) simp_all
   4.333 +  finally show ?thesis .
   4.334 +qed
   4.335 +
   4.336 +lemma fps_compose_divide_distrib:
   4.337 +  assumes "g dvd f" "h $ 0 = 0" "fps_compose g h \<noteq> 0"
   4.338 +  shows   "fps_compose (f / g :: 'a :: field fps) h = fps_compose f h / fps_compose g h"
   4.339 +  using fps_compose_divide[OF assms(1,2)] assms(3) by simp
   4.340 +
   4.341  lemma fps_compose_power:
   4.342    assumes c0: "c$0 = (0::'a::idom)"
   4.343    shows "(a oo c)^n = a^n oo c"
   4.344 @@ -3493,6 +3685,10 @@
   4.345      unfolding fps_inv_right[OF a0 a1] by simp
   4.346  qed
   4.347  
   4.348 +lemma fps_compose_linear:
   4.349 +  "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)"
   4.350 +  by (simp add: fps_eq_iff fps_compose_def power_mult_distrib
   4.351 +                if_distrib setsum.delta' cong: if_cong)
   4.352  
   4.353  subsection \<open>Elementary series\<close>
   4.354  
   4.355 @@ -3742,6 +3938,10 @@
   4.356    qed
   4.357  qed
   4.358  
   4.359 +lemma fps_binomial_ODE_unique':
   4.360 +  "(fps_deriv a = fps_const c * a / (1 + X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)"
   4.361 +  by (subst fps_binomial_ODE_unique) auto
   4.362 +
   4.363  lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
   4.364  proof -
   4.365    let ?a = "fps_binomial c"
   4.366 @@ -3783,6 +3983,87 @@
   4.367    show ?thesis by (simp add: fps_inverse_def)
   4.368  qed
   4.369  
   4.370 +lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + X :: 'a :: field_char_0 fps) ^ n"
   4.371 +proof (cases "n = 0")
   4.372 +  case [simp]: True
   4.373 +  have "fps_deriv ((1 + X) ^ n :: 'a fps) = 0" by simp
   4.374 +  also have "\<dots> = fps_const (of_nat n) * (1 + X) ^ n / (1 + X)" by (simp add: fps_binomial_def)
   4.375 +  finally show ?thesis by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) simp_all
   4.376 +next
   4.377 +  case False
   4.378 +  have "fps_deriv ((1 + X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + X) ^ (n - 1)"
   4.379 +    by (simp add: fps_deriv_power)
   4.380 +  also have "(1 + X :: 'a fps) $ 0 \<noteq> 0" by simp
   4.381 +  hence "(1 + X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp)
   4.382 +  with False have "(1 + X :: 'a fps) ^ (n - 1) = (1 + X) ^ n / (1 + X)"
   4.383 +    by (cases n) (simp_all )
   4.384 +  also have "fps_const (of_nat n :: 'a) * ((1 + X) ^ n / (1 + X)) =
   4.385 +               fps_const (of_nat n) * (1 + X) ^ n / (1 + X)"
   4.386 +    by (simp add: unit_div_mult_swap)
   4.387 +  finally show ?thesis
   4.388 +    by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) (simp_all add: fps_power_nth)
   4.389 +qed
   4.390 +
   4.391 +lemma fps_binomial_0 [simp]: "fps_binomial 0 = 1"
   4.392 +  using fps_binomial_of_nat[of 0] by simp
   4.393 +  
   4.394 +lemma fps_binomial_power: "fps_binomial a ^ n = fps_binomial (of_nat n * a)"
   4.395 +  by (induction n) (simp_all add: fps_binomial_add_mult ring_distribs)
   4.396 +
   4.397 +lemma fps_binomial_1: "fps_binomial 1 = 1 + X"
   4.398 +  using fps_binomial_of_nat[of 1] by simp
   4.399 +
   4.400 +lemma fps_binomial_minus_of_nat:
   4.401 +  "fps_binomial (- of_nat n) = inverse ((1 + X :: 'a :: field_char_0 fps) ^ n)"
   4.402 +  by (rule sym, rule fps_inverse_unique)
   4.403 +     (simp add: fps_binomial_of_nat [symmetric] fps_binomial_add_mult [symmetric])
   4.404 +
   4.405 +lemma one_minus_const_X_power:
   4.406 +  "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * X) ^ n =
   4.407 +     fps_compose (fps_binomial (of_nat n)) (-fps_const c * X)"
   4.408 +  by (subst fps_binomial_of_nat)
   4.409 +     (simp add: fps_compose_power [symmetric] fps_compose_add_distrib fps_const_neg [symmetric] 
   4.410 +           del: fps_const_neg)
   4.411 +
   4.412 +lemma one_minus_X_const_neg_power:
   4.413 +  "inverse ((1 - fps_const c * X) ^ n) = 
   4.414 +       fps_compose (fps_binomial (-of_nat n)) (-fps_const c * X)"
   4.415 +proof (cases "c = 0")
   4.416 +  case False
   4.417 +  thus ?thesis
   4.418 +  by (subst fps_binomial_minus_of_nat)
   4.419 +     (simp add: fps_compose_power [symmetric] fps_inverse_compose fps_compose_add_distrib
   4.420 +                fps_const_neg [symmetric] del: fps_const_neg)
   4.421 +qed simp
   4.422 +
   4.423 +lemma X_plus_const_power:
   4.424 +  "c \<noteq> 0 \<Longrightarrow> (X + fps_const c) ^ n =
   4.425 +     fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * X)"
   4.426 +  by (subst fps_binomial_of_nat)
   4.427 +     (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
   4.428 +                fps_const_power [symmetric] power_mult_distrib [symmetric] 
   4.429 +                algebra_simps inverse_mult_eq_1' del: fps_const_power)
   4.430 +
   4.431 +lemma X_plus_const_neg_power:
   4.432 +  "c \<noteq> 0 \<Longrightarrow> inverse ((X + fps_const c) ^ n) =
   4.433 +     fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * X)"
   4.434 +  by (subst fps_binomial_minus_of_nat)
   4.435 +     (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
   4.436 +                fps_const_power [symmetric] power_mult_distrib [symmetric] fps_inverse_compose 
   4.437 +                algebra_simps fps_const_inverse [symmetric] fps_inverse_mult [symmetric]
   4.438 +                fps_inverse_power [symmetric] inverse_mult_eq_1'
   4.439 +           del: fps_const_power)
   4.440 +
   4.441 +
   4.442 +lemma one_minus_const_X_neg_power':
   4.443 +  "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * X) ^ n) =
   4.444 +       Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)"
   4.445 +  apply (rule fps_ext)
   4.446 +  apply (subst one_minus_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear)
   4.447 +  apply (simp add: power_mult_distrib [symmetric] mult.assoc [symmetric] 
   4.448 +                   gbinomial_minus binomial_gbinomial of_nat_diff)
   4.449 +  done
   4.450 +
   4.451  text \<open>Vandermonde's Identity as a consequence.\<close>
   4.452  lemma gbinomial_Vandermonde:
   4.453    "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
   4.454 @@ -4216,6 +4497,10 @@
   4.455  lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   4.456    by (fact fps_const_sub)
   4.457  
   4.458 +lemma fps_of_int: "fps_const (of_int c) = of_int c"
   4.459 +  by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
   4.460 +                             del: fps_const_minus fps_const_neg)
   4.461 +
   4.462  lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
   4.463    by (fact numeral_fps_const) (* FIXME: duplicate *)
   4.464  
     5.1 --- a/src/HOL/Library/Library.thy	Wed Jun 15 15:52:24 2016 +0100
     5.2 +++ b/src/HOL/Library/Library.thy	Thu Jun 16 17:57:09 2016 +0200
     5.3 @@ -58,6 +58,7 @@
     5.4    Permutation
     5.5    Permutations
     5.6    Polynomial
     5.7 +  Polynomial_FPS
     5.8    Preorder
     5.9    Product_Vector
    5.10    Quadratic_Discriminant
     6.1 --- a/src/HOL/Library/Polynomial.thy	Wed Jun 15 15:52:24 2016 +0100
     6.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Jun 16 17:57:09 2016 +0200
     6.3 @@ -564,8 +564,14 @@
     6.4    fixes a x :: "'a::{comm_semiring_1}"
     6.5    shows "poly (monom a n) x = a * x ^ n"
     6.6    by (cases "a = 0", simp_all)
     6.7 -    (induct n, simp_all add: mult.left_commute poly_def)
     6.8 -
     6.9 +    (induct n, simp_all add: mult.left_commute poly_def)  
    6.10 +
    6.11 +lemma monom_eq_iff': "monom c n = monom d m \<longleftrightarrow>  c = d \<and> (c = 0 \<or> n = m)"
    6.12 +  by (auto simp: poly_eq_iff)
    6.13 +  
    6.14 +lemma monom_eq_const_iff: "monom c n = [:d:] \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = 0)"
    6.15 +  using monom_eq_iff'[of c n d 0] by (simp add: monom_0)
    6.16 +  
    6.17      
    6.18  subsection \<open>Addition and subtraction\<close>
    6.19  
    6.20 @@ -869,6 +875,9 @@
    6.21  lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
    6.22    by (induct n, simp add: monom_0, simp add: monom_Suc)
    6.23  
    6.24 +lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
    6.25 +  by (auto simp add: poly_eq_iff coeff_Poly_eq nth_default_def)
    6.26 +
    6.27  lemma degree_smult_eq [simp]:
    6.28    fixes a :: "'a::idom"
    6.29    shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
    6.30 @@ -878,7 +887,7 @@
    6.31    fixes a :: "'a::idom"
    6.32    shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
    6.33    by (simp add: poly_eq_iff)
    6.34 -
    6.35 +  
    6.36  lemma coeffs_smult [code abstract]:
    6.37    fixes p :: "'a::idom poly"
    6.38    shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
    6.39 @@ -985,6 +994,13 @@
    6.40  lemma monom_eq_1 [simp]:
    6.41    "monom 1 0 = 1"
    6.42    by (simp add: monom_0 one_poly_def)
    6.43 +
    6.44 +lemma monom_eq_1_iff: "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0"
    6.45 +  using monom_eq_const_iff[of c n 1] by (auto simp: one_poly_def)
    6.46 +
    6.47 +lemma monom_altdef:
    6.48 +  "monom c n = smult c ([:0, 1:]^n)"
    6.49 +  by (induction n) (simp_all add: monom_0 monom_Suc one_poly_def)
    6.50    
    6.51  lemma degree_1 [simp]: "degree 1 = 0"
    6.52    unfolding one_poly_def
    6.53 @@ -2854,6 +2870,14 @@
    6.54    shows "pcompose p [: 0, 1 :] = p"
    6.55    by (induct p; simp add: pcompose_pCons)
    6.56  
    6.57 +lemma pcompose_setsum: "pcompose (setsum f A) p = setsum (\<lambda>i. pcompose (f i) p) A"
    6.58 +  by (cases "finite A", induction rule: finite_induct)
    6.59 +     (simp_all add: pcompose_1 pcompose_add)
    6.60 +
    6.61 +lemma pcompose_setprod: "pcompose (setprod f A) p = setprod (\<lambda>i. pcompose (f i) p) A"
    6.62 +  by (cases "finite A", induction rule: finite_induct)
    6.63 +     (simp_all add: pcompose_1 pcompose_mult)
    6.64 +
    6.65  
    6.66  (* The remainder of this section and the next were contributed by Wenda Li *)
    6.67  
    6.68 @@ -2940,6 +2964,12 @@
    6.69  lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
    6.70    unfolding lead_coeff_def by auto
    6.71  
    6.72 +lemma coeff_0_listprod: "coeff (listprod xs) 0 = listprod (map (\<lambda>p. coeff p 0) xs)"
    6.73 +  by (induction xs) (simp_all add: coeff_mult)
    6.74 +
    6.75 +lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
    6.76 +  by (induction n) (simp_all add: coeff_mult)
    6.77 +
    6.78  lemma lead_coeff_mult:
    6.79     fixes p q::"'a ::idom poly"
    6.80     shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
    6.81 @@ -3015,6 +3045,200 @@
    6.82    by (simp add: lead_coeff_def)
    6.83  
    6.84  
    6.85 +subsection \<open>Shifting polynomials\<close>
    6.86 +
    6.87 +definition poly_shift :: "nat \<Rightarrow> ('a::zero) poly \<Rightarrow> 'a poly" where
    6.88 +  "poly_shift n p = Abs_poly (\<lambda>i. coeff p (i + n))"
    6.89 +
    6.90 +lemma nth_default_drop: "nth_default x (drop n xs) m = nth_default x xs (m + n)"
    6.91 +  by (auto simp add: nth_default_def add_ac)
    6.92 +  
    6.93 +lemma nth_default_take: "nth_default x (take n xs) m = (if m < n then nth_default x xs m else x)"
    6.94 +  by (auto simp add: nth_default_def add_ac)
    6.95 +  
    6.96 +  
    6.97 +lemma coeff_poly_shift: "coeff (poly_shift n p) i = coeff p (i + n)"
    6.98 +proof -
    6.99 +  from MOST_coeff_eq_0[of p] obtain m where "\<forall>k>m. coeff p k = 0" by (auto simp: MOST_nat)
   6.100 +  hence "\<forall>k>m. coeff p (k + n) = 0" by auto
   6.101 +  hence "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0" by (auto simp: MOST_nat)
   6.102 +  thus ?thesis by (simp add: poly_shift_def poly.Abs_poly_inverse)
   6.103 +qed
   6.104 +
   6.105 +lemma poly_shift_id [simp]: "poly_shift 0 = (\<lambda>x. x)"
   6.106 +  by (simp add: poly_eq_iff fun_eq_iff coeff_poly_shift)
   6.107 +
   6.108 +lemma poly_shift_0 [simp]: "poly_shift n 0 = 0"
   6.109 +  by (simp add: poly_eq_iff coeff_poly_shift)
   6.110 +  
   6.111 +lemma poly_shift_1: "poly_shift n 1 = (if n = 0 then 1 else 0)"
   6.112 +  by (simp add: poly_eq_iff coeff_poly_shift)
   6.113 +
   6.114 +lemma poly_shift_monom: "poly_shift n (monom c m) = (if m \<ge> n then monom c (m - n) else 0)"
   6.115 +  by (auto simp add: poly_eq_iff coeff_poly_shift)
   6.116 +
   6.117 +lemma coeffs_shift_poly [code abstract]: "coeffs (poly_shift n p) = drop n (coeffs p)"
   6.118 +proof (cases "p = 0")
   6.119 +  case False
   6.120 +  thus ?thesis
   6.121 +    by (intro coeffs_eqI)
   6.122 +       (simp_all add: coeff_poly_shift nth_default_drop last_coeffs_not_0 nth_default_coeffs_eq)
   6.123 +qed simp_all
   6.124 +
   6.125 +
   6.126 +subsection \<open>Truncating polynomials\<close>
   6.127 +
   6.128 +definition poly_cutoff where
   6.129 +  "poly_cutoff n p = Abs_poly (\<lambda>k. if k < n then coeff p k else 0)"
   6.130 +
   6.131 +lemma coeff_poly_cutoff: "coeff (poly_cutoff n p) k = (if k < n then coeff p k else 0)"
   6.132 +  unfolding poly_cutoff_def
   6.133 +  by (subst poly.Abs_poly_inverse) (auto simp: MOST_nat intro: exI[of _ n])
   6.134 +
   6.135 +lemma poly_cutoff_0 [simp]: "poly_cutoff n 0 = 0"
   6.136 +  by (simp add: poly_eq_iff coeff_poly_cutoff)
   6.137 +
   6.138 +lemma poly_cutoff_1 [simp]: "poly_cutoff n 1 = (if n = 0 then 0 else 1)"
   6.139 +  by (simp add: poly_eq_iff coeff_poly_cutoff)
   6.140 +
   6.141 +lemma coeffs_poly_cutoff [code abstract]: 
   6.142 +  "coeffs (poly_cutoff n p) = strip_while (op = 0) (take n (coeffs p))"
   6.143 +proof (cases "strip_while (op = 0) (take n (coeffs p)) = []")
   6.144 +  case True
   6.145 +  hence "coeff (poly_cutoff n p) k = 0" for k
   6.146 +    unfolding coeff_poly_cutoff
   6.147 +    by (auto simp: nth_default_coeffs_eq [symmetric] nth_default_def set_conv_nth)
   6.148 +  hence "poly_cutoff n p = 0" by (simp add: poly_eq_iff)
   6.149 +  thus ?thesis by (subst True) simp_all
   6.150 +next
   6.151 +  case False
   6.152 +  have "no_trailing (op = 0) (strip_while (op = 0) (take n (coeffs p)))" by simp
   6.153 +  with False have "last (strip_while (op = 0) (take n (coeffs p))) \<noteq> 0" 
   6.154 +    unfolding no_trailing_unfold by auto
   6.155 +  thus ?thesis
   6.156 +    by (intro coeffs_eqI)
   6.157 +       (simp_all add: coeff_poly_cutoff last_coeffs_not_0 nth_default_take nth_default_coeffs_eq)
   6.158 +qed
   6.159 +
   6.160 +
   6.161 +subsection \<open>Reflecting polynomials\<close>
   6.162 +
   6.163 +definition reflect_poly where
   6.164 +  "reflect_poly p = Poly (rev (coeffs p))"
   6.165 +  
   6.166 +lemma coeffs_reflect_poly [code abstract]:
   6.167 +    "coeffs (reflect_poly p) = rev (dropWhile (op = 0) (coeffs p))"
   6.168 +  unfolding reflect_poly_def by simp
   6.169 +  
   6.170 +lemma reflect_poly_0 [simp]: "reflect_poly 0 = 0"
   6.171 +  by (simp add: reflect_poly_def)
   6.172 +
   6.173 +lemma reflect_poly_1 [simp]: "reflect_poly 1 = 1"
   6.174 +  by (simp add: reflect_poly_def one_poly_def)
   6.175 +
   6.176 +lemma coeff_reflect_poly:
   6.177 +  "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))"
   6.178 +  by (cases "p = 0") (auto simp add: reflect_poly_def coeff_Poly_eq nth_default_def
   6.179 +                                     rev_nth degree_eq_length_coeffs coeffs_nth not_less
   6.180 +                                dest: le_imp_less_Suc)
   6.181 +
   6.182 +lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
   6.183 +  by (simp add: coeff_reflect_poly)
   6.184 +
   6.185 +lemma reflect_poly_at_0_eq_0_iff [simp]: "poly (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
   6.186 +  by (simp add: coeff_reflect_poly poly_0_coeff_0)
   6.187 +
   6.188 +lemma reflect_poly_pCons':
   6.189 +  "p \<noteq> 0 \<Longrightarrow> reflect_poly (pCons c p) = reflect_poly p + monom c (Suc (degree p))"
   6.190 +  by (intro poly_eqI)
   6.191 +     (auto simp: coeff_reflect_poly coeff_pCons not_less Suc_diff_le split: nat.split)
   6.192 +
   6.193 +lemma reflect_poly_const [simp]: "reflect_poly [:a:] = [:a:]"
   6.194 +  by (cases "a = 0") (simp_all add: reflect_poly_def)
   6.195 +
   6.196 +lemma poly_reflect_poly_nz:
   6.197 +  "(x :: 'a :: field) \<noteq> 0 \<Longrightarrow> poly (reflect_poly p) x = x ^ degree p * poly p (inverse x)"
   6.198 +  by (induction rule: pCons_induct) (simp_all add: field_simps reflect_poly_pCons' poly_monom)
   6.199 +
   6.200 +lemma coeff_0_reflect_poly [simp]: "coeff (reflect_poly p) 0 = lead_coeff p"
   6.201 +  by (simp add: coeff_reflect_poly lead_coeff_def)
   6.202 +
   6.203 +lemma poly_reflect_poly_0 [simp]: "poly (reflect_poly p) 0 = lead_coeff p"
   6.204 +  by (simp add: poly_0_coeff_0)
   6.205 +
   6.206 +lemma reflect_poly_reflect_poly [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> reflect_poly (reflect_poly p) = p"
   6.207 +  by (cases p rule: pCons_cases) (simp add: reflect_poly_def )
   6.208 +
   6.209 +lemma degree_reflect_poly_le: "degree (reflect_poly p) \<le> degree p"
   6.210 +  by (simp add: degree_eq_length_coeffs coeffs_reflect_poly length_dropWhile_le diff_le_mono)
   6.211 +
   6.212 +lemma reflect_poly_pCons:
   6.213 +  "a \<noteq> 0 \<Longrightarrow> reflect_poly (pCons a p) = Poly (rev (a # coeffs p))"
   6.214 +  by (subst coeffs_eq_iff) (simp add: coeffs_reflect_poly)
   6.215 +  
   6.216 +lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
   6.217 +  by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)
   6.218 +  
   6.219 +(* TODO: does this work for non-idom as well? *)
   6.220 +lemma reflect_poly_mult:
   6.221 +  "reflect_poly (p * q) = reflect_poly p * reflect_poly (q :: _ :: idom poly)"
   6.222 +proof (cases "p = 0 \<or> q = 0")
   6.223 +  case False
   6.224 +  hence [simp]: "p \<noteq> 0" "q \<noteq> 0" by auto
   6.225 +  show ?thesis
   6.226 +  proof (rule poly_eqI)
   6.227 +    fix i :: nat
   6.228 +    show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i"
   6.229 +    proof (cases "i \<le> degree (p * q)")
   6.230 +      case True
   6.231 +      def A \<equiv> "{..i} \<inter> {i - degree q..degree p}"
   6.232 +      def B \<equiv> "{..degree p} \<inter> {degree p - i..degree (p*q) - i}"
   6.233 +      let ?f = "\<lambda>j. degree p - j"
   6.234 +
   6.235 +      from True have "coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)"
   6.236 +        by (simp add: coeff_reflect_poly)
   6.237 +      also have "\<dots> = (\<Sum>j\<le>degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))"
   6.238 +        unfolding coeff_mult by simp
   6.239 +      also have "\<dots> = (\<Sum>j\<in>B. coeff p j * coeff q (degree (p * q) - i - j))"
   6.240 +        by (intro setsum.mono_neutral_right) (auto simp: B_def degree_mult_eq not_le coeff_eq_0)
   6.241 +      also from True have "\<dots> = (\<Sum>j\<in>A. coeff p (degree p - j) * coeff q (degree q - (i - j)))"
   6.242 +        by (intro setsum.reindex_bij_witness[of _ ?f ?f])
   6.243 +           (auto simp: A_def B_def degree_mult_eq add_ac)
   6.244 +      also have "\<dots> = (\<Sum>j\<le>i. if j \<in> {i - degree q..degree p} then
   6.245 +                 coeff p (degree p - j) * coeff q (degree q - (i - j)) else 0)"
   6.246 +        by (subst setsum.inter_restrict [symmetric]) (simp_all add: A_def)
   6.247 +       also have "\<dots> = coeff (reflect_poly p * reflect_poly q) i"
   6.248 +          by (fastforce simp: coeff_mult coeff_reflect_poly intro!: setsum.cong)
   6.249 +       finally show ?thesis .
   6.250 +    qed (auto simp: coeff_mult coeff_reflect_poly coeff_eq_0 degree_mult_eq intro!: setsum.neutral)
   6.251 +  qed
   6.252 +qed auto
   6.253 +
   6.254 +lemma reflect_poly_smult: 
   6.255 +  "reflect_poly (Polynomial.smult (c::'a::idom) p) = Polynomial.smult c (reflect_poly p)"
   6.256 +  using reflect_poly_mult[of "[:c:]" p] by simp
   6.257 +
   6.258 +lemma reflect_poly_power:
   6.259 +    "reflect_poly (p ^ n :: 'a :: idom poly) = reflect_poly p ^ n"
   6.260 +  by (induction n) (simp_all add: reflect_poly_mult)
   6.261 +
   6.262 +lemma reflect_poly_setprod:
   6.263 +  "reflect_poly (setprod (f :: _ \<Rightarrow> _ :: idom poly) A) = setprod (\<lambda>x. reflect_poly (f x)) A"
   6.264 +  by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)
   6.265 +
   6.266 +lemma reflect_poly_listprod:
   6.267 +  "reflect_poly (listprod (xs :: _ :: idom poly list)) = listprod (map reflect_poly xs)"
   6.268 +  by (induction xs) (simp_all add: reflect_poly_mult)
   6.269 +
   6.270 +lemma reflect_poly_Poly_nz: 
   6.271 +  "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0 \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
   6.272 +  unfolding reflect_poly_def coeffs_Poly by simp
   6.273 +
   6.274 +lemmas reflect_poly_simps = 
   6.275 +  reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
   6.276 +  reflect_poly_power reflect_poly_setprod reflect_poly_listprod
   6.277 +
   6.278 +
   6.279  subsection \<open>Derivatives of univariate polynomials\<close>
   6.280  
   6.281  function pderiv :: "('a :: semidom) poly \<Rightarrow> 'a poly"
   6.282 @@ -3545,6 +3769,15 @@
   6.283    ultimately show ?case using Suc by auto
   6.284  qed
   6.285  
   6.286 +lemma order_0_monom [simp]:
   6.287 +  assumes "c \<noteq> 0"
   6.288 +  shows   "order 0 (monom c n) = n"
   6.289 +  using assms order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult)
   6.290 +
   6.291 +lemma dvd_imp_order_le:
   6.292 +  "q \<noteq> 0 \<Longrightarrow> p dvd q \<Longrightarrow> Polynomial.order a p \<le> Polynomial.order a q"
   6.293 +  by (auto simp: order_mult elim: dvdE)
   6.294 +
   6.295  text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>
   6.296  
   6.297  lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
   6.298 @@ -3554,6 +3787,11 @@
   6.299  apply (erule power_le_dvd [OF order_1])
   6.300  done
   6.301  
   6.302 +lemma monom_1_dvd_iff:
   6.303 +  assumes "p \<noteq> 0"
   6.304 +  shows   "monom 1 n dvd p \<longleftrightarrow> n \<le> Polynomial.order 0 p"
   6.305 +  using assms order_divides[of 0 n p] by (simp add: monom_altdef)
   6.306 +
   6.307  lemma poly_squarefree_decomp_order:
   6.308    assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
   6.309    and p: "p = q * d"
   6.310 @@ -3639,6 +3877,35 @@
   6.311      by (simp add: rsquarefree_def order_root)
   6.312  qed
   6.313  
   6.314 +lemma coeff_monom_mult: 
   6.315 +  "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
   6.316 +proof -
   6.317 +  have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k - i))"
   6.318 +    by (simp add: coeff_mult)
   6.319 +  also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
   6.320 +    by (intro setsum.cong) simp_all
   6.321 +  also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))" by (simp add: setsum.delta')
   6.322 +  finally show ?thesis .
   6.323 +qed
   6.324 +
   6.325 +lemma monom_1_dvd_iff':
   6.326 +  "monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)"
   6.327 +proof
   6.328 +  assume "monom 1 n dvd p"
   6.329 +  then obtain r where r: "p = monom 1 n * r" by (elim dvdE)
   6.330 +  thus "\<forall>k<n. coeff p k = 0" by (simp add: coeff_mult)
   6.331 +next
   6.332 +  assume zero: "(\<forall>k<n. coeff p k = 0)"
   6.333 +  define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))"
   6.334 +  have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
   6.335 +    by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, 
   6.336 +        subst cofinite_eq_sequentially [symmetric]) transfer
   6.337 +  hence coeff_r [simp]: "coeff r k = coeff p (k + n)" for k unfolding r_def
   6.338 +    by (subst poly.Abs_poly_inverse) simp_all
   6.339 +  have "p = monom 1 n * r"
   6.340 +    by (intro poly_eqI, subst coeff_monom_mult) (insert zero, simp_all)
   6.341 +  thus "monom 1 n dvd p" by simp
   6.342 +qed
   6.343  
   6.344  no_notation cCons (infixr "##" 65)
   6.345  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/Polynomial_FPS.thy	Thu Jun 16 17:57:09 2016 +0200
     7.3 @@ -0,0 +1,313 @@
     7.4 +(*
     7.5 +  File:      Polynomial_FPS.thy
     7.6 +  Author:    Manuel Eberl (TUM)
     7.7 +  
     7.8 +  Converting polynomials to formal power series
     7.9 +*)
    7.10 +
    7.11 +section \<open>Converting polynomials to formal power series\<close>
    7.12 +theory Polynomial_FPS
    7.13 +imports Polynomial Formal_Power_Series
    7.14 +begin
    7.15 +
    7.16 +definition fps_from_poly where
    7.17 +  "fps_from_poly p = Abs_fps (coeff p)"
    7.18 +
    7.19 +lemma fps_from_poly_eq_iff: "fps_from_poly p = fps_from_poly q \<longleftrightarrow> p = q"
    7.20 +  by (simp add: fps_from_poly_def poly_eq_iff fps_eq_iff)
    7.21 +
    7.22 +lemma fps_from_poly_nth [simp]: "fps_from_poly p $ n = coeff p n"
    7.23 +  by (simp add: fps_from_poly_def)
    7.24 +  
    7.25 +lemma fps_from_poly_const: "fps_from_poly [:c:] = fps_const c"
    7.26 +proof (subst fps_eq_iff, clarify)
    7.27 +  fix n :: nat show "fps_from_poly [:c:] $ n = fps_const c $ n"
    7.28 +    by (cases n) (auto simp: fps_from_poly_def)
    7.29 +qed
    7.30 +
    7.31 +lemma fps_from_poly_0 [simp]: "fps_from_poly 0 = 0"
    7.32 +  by (subst fps_const_0_eq_0 [symmetric], subst fps_from_poly_const [symmetric]) simp
    7.33 +
    7.34 +lemma fps_from_poly_1 [simp]: "fps_from_poly 1 = 1"
    7.35 +  by (subst fps_const_1_eq_1 [symmetric], subst fps_from_poly_const [symmetric])
    7.36 +     (simp add: one_poly_def)
    7.37 +
    7.38 +lemma fps_from_poly_1' [simp]: "fps_from_poly [:1:] = 1"
    7.39 +  by (subst fps_const_1_eq_1 [symmetric], subst fps_from_poly_const [symmetric])
    7.40 +     (simp add: one_poly_def)
    7.41 +
    7.42 +lemma fps_from_poly_numeral [simp]: "fps_from_poly (numeral n) = numeral n"
    7.43 +  by (simp add: numeral_fps_const fps_from_poly_const [symmetric] numeral_poly)
    7.44 +
    7.45 +lemma fps_from_poly_numeral' [simp]: "fps_from_poly [:numeral n:] = numeral n"
    7.46 +  by (simp add: numeral_fps_const fps_from_poly_const [symmetric] numeral_poly)
    7.47 +
    7.48 +lemma fps_from_poly_X [simp]: "fps_from_poly [:0, 1:] = X"
    7.49 +  by (auto simp add: fps_from_poly_def fps_eq_iff coeff_pCons split: nat.split)
    7.50 +
    7.51 +lemma fps_from_poly_add: "fps_from_poly (p + q) = fps_from_poly p + fps_from_poly q"
    7.52 +  by (simp add: fps_from_poly_def plus_poly.rep_eq fps_plus_def)
    7.53 +
    7.54 +lemma fps_from_poly_diff: "fps_from_poly (p - q) = fps_from_poly p - fps_from_poly q"
    7.55 +  by (simp add: fps_from_poly_def minus_poly.rep_eq fps_minus_def)
    7.56 +
    7.57 +lemma fps_from_poly_uminus: "fps_from_poly (-p) = -fps_from_poly p"
    7.58 +  by (simp add: fps_from_poly_def uminus_poly.rep_eq fps_uminus_def)
    7.59 +
    7.60 +lemma fps_from_poly_mult: "fps_from_poly (p * q) = fps_from_poly p * fps_from_poly q"
    7.61 +  by (simp add: fps_from_poly_def fps_times_def fps_eq_iff coeff_mult atLeast0AtMost)
    7.62 +
    7.63 +lemma fps_from_poly_smult: 
    7.64 +  "fps_from_poly (smult c p) = fps_const c * fps_from_poly p"
    7.65 +  using fps_from_poly_mult[of "[:c:]" p] by (simp add: fps_from_poly_mult fps_from_poly_const)
    7.66 +  
    7.67 +lemma fps_from_poly_setsum: "fps_from_poly (setsum f A) = setsum (\<lambda>x. fps_from_poly (f x)) A"
    7.68 +  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_from_poly_add)
    7.69 +
    7.70 +lemma fps_from_poly_listsum: "fps_from_poly (listsum xs) = listsum (map fps_from_poly xs)"
    7.71 +  by (induction xs) (simp_all add: fps_from_poly_add)
    7.72 +  
    7.73 +lemma fps_from_poly_setprod: "fps_from_poly (setprod f A) = setprod (\<lambda>x. fps_from_poly (f x)) A"
    7.74 +  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_from_poly_mult)
    7.75 +  
    7.76 +lemma fps_from_poly_listprod: "fps_from_poly (listprod xs) = listprod (map fps_from_poly xs)"
    7.77 +  by (induction xs) (simp_all add: fps_from_poly_mult)
    7.78 +
    7.79 +lemma fps_from_poly_pCons: 
    7.80 +  "fps_from_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_from_poly p * X"
    7.81 +  by (subst fps_mult_X_commute [symmetric], intro fps_ext) 
    7.82 +     (auto simp: fps_from_poly_def coeff_pCons split: nat.split)
    7.83 +  
    7.84 +lemma fps_from_poly_pderiv: "fps_from_poly (pderiv p) = fps_deriv (fps_from_poly p)"
    7.85 +  by (intro fps_ext) (simp add: fps_from_poly_nth coeff_pderiv)
    7.86 +
    7.87 +lemma fps_from_poly_power: "fps_from_poly (p ^ n) = fps_from_poly p ^ n"
    7.88 +  by (induction n) (simp_all add: fps_from_poly_mult)
    7.89 +  
    7.90 +lemma fps_from_poly_monom: "fps_from_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
    7.91 +  by (intro fps_ext) simp_all
    7.92 +
    7.93 +lemma fps_from_poly_monom': "fps_from_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n"
    7.94 +  by (simp add: fps_from_poly_monom)
    7.95 +
    7.96 +lemma fps_from_poly_div:
    7.97 +  assumes "(q :: 'a :: field poly) dvd p"
    7.98 +  shows   "fps_from_poly (p div q) = fps_from_poly p / fps_from_poly q"
    7.99 +proof (cases "q = 0")
   7.100 +  case False
   7.101 +  from False fps_from_poly_eq_iff[of q 0] have nz: "fps_from_poly q \<noteq> 0" by simp 
   7.102 +  from assms have "p = (p div q) * q" by simp
   7.103 +  also have "fps_from_poly \<dots> = fps_from_poly (p div q) * fps_from_poly q" 
   7.104 +    by (simp add: fps_from_poly_mult)
   7.105 +  also from nz have "\<dots> / fps_from_poly q = fps_from_poly (p div q)"
   7.106 +    by (intro div_mult_self2_is_id) (auto simp: fps_from_poly_0)
   7.107 +  finally show ?thesis ..
   7.108 +qed simp
   7.109 +
   7.110 +lemma fps_from_poly_divide_numeral:
   7.111 +  "fps_from_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_from_poly p / numeral c"
   7.112 +proof -
   7.113 +  have "smult (inverse (numeral c)) p = [:inverse (numeral c):] * p" by simp
   7.114 +  also have "fps_from_poly \<dots> = fps_from_poly p / numeral c"
   7.115 +    by (subst fps_from_poly_mult) (simp add: numeral_fps_const fps_from_poly_pCons)
   7.116 +  finally show ?thesis by simp
   7.117 +qed
   7.118 +
   7.119 +
   7.120 +lemma subdegree_fps_from_poly:
   7.121 +  assumes "p \<noteq> 0"
   7.122 +  defines "n \<equiv> Polynomial.order 0 p"
   7.123 +  shows   "subdegree (fps_from_poly p) = n"
   7.124 +proof (rule subdegreeI)
   7.125 +  from assms have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff)
   7.126 +  thus zero: "fps_from_poly p $ i = 0" if "i < n" for i
   7.127 +    using that by (simp add: monom_1_dvd_iff')
   7.128 +    
   7.129 +  from assms have "\<not>monom 1 (Suc n) dvd p"
   7.130 +    by (auto simp: monom_1_dvd_iff simp del: power_Suc)
   7.131 +  then obtain k where "k \<le> n" "fps_from_poly p $ k \<noteq> 0" 
   7.132 +    by (auto simp: monom_1_dvd_iff' less_Suc_eq_le)
   7.133 +  moreover from this and zero[of k] have "k = n" by linarith
   7.134 +  ultimately show "fps_from_poly p $ n \<noteq> 0" by simp
   7.135 +qed
   7.136 +
   7.137 +lemma fps_from_poly_dvd:
   7.138 +  assumes "p dvd q"
   7.139 +  shows   "fps_from_poly (p :: 'a :: field poly) dvd fps_from_poly q"
   7.140 +proof (cases "p = 0 \<or> q = 0")
   7.141 +  case False
   7.142 +  with assms fps_from_poly_eq_iff[of p 0] fps_from_poly_eq_iff[of q 0] show ?thesis
   7.143 +    by (auto simp: fps_dvd_iff subdegree_fps_from_poly dvd_imp_order_le)
   7.144 +qed (insert assms, auto)
   7.145 +
   7.146 +
   7.147 +lemmas fps_from_poly_simps =
   7.148 +  fps_from_poly_0 fps_from_poly_1 fps_from_poly_numeral fps_from_poly_const fps_from_poly_X
   7.149 +  fps_from_poly_add fps_from_poly_diff fps_from_poly_uminus fps_from_poly_mult fps_from_poly_smult
   7.150 +  fps_from_poly_setsum fps_from_poly_listsum fps_from_poly_setprod fps_from_poly_listprod
   7.151 +  fps_from_poly_pCons fps_from_poly_pderiv fps_from_poly_power fps_from_poly_monom
   7.152 +  fps_from_poly_divide_numeral
   7.153 +
   7.154 +lemma fps_from_poly_pcompose:
   7.155 +  assumes "coeff q 0 = (0 :: 'a :: idom)"
   7.156 +  shows   "fps_from_poly (pcompose p q) = fps_compose (fps_from_poly p) (fps_from_poly q)"
   7.157 +  using assms by (induction p rule: pCons_induct)
   7.158 +                 (auto simp: pcompose_pCons fps_from_poly_simps fps_from_poly_pCons 
   7.159 +                             fps_compose_add_distrib fps_compose_mult_distrib)
   7.160 +  
   7.161 +lemmas reify_fps_atom =
   7.162 +  fps_from_poly_0 fps_from_poly_1' fps_from_poly_numeral' fps_from_poly_const fps_from_poly_X
   7.163 +
   7.164 +
   7.165 +text \<open>
   7.166 +  The following simproc can reduce the equality of two polynomial FPSs two equality of the
   7.167 +  respective polynomials. A polynomial FPS is one that only has finitely many non-zero 
   7.168 +  coefficients and can therefore be written as @{term "fps_from_poly p"} for some 
   7.169 +  polynomial @{text "p"}.
   7.170 +  
   7.171 +  This may sound trivial, but it covers a number of annoying side conditions like 
   7.172 +  @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.
   7.173 +\<close>
   7.174 +
   7.175 +ML \<open>
   7.176 +
   7.177 +(* TODO: Support for division *)
   7.178 +signature POLY_FPS = sig
   7.179 +
   7.180 +val reify_conv : conv
   7.181 +val eq_conv : conv
   7.182 +val eq_simproc : cterm -> thm option
   7.183 +
   7.184 +end
   7.185 +
   7.186 +
   7.187 +structure Poly_Fps = struct
   7.188 +
   7.189 +fun const_binop_conv s conv ct =
   7.190 +  case Thm.term_of ct of
   7.191 +    (Const (s', _) $ _ $ _) => 
   7.192 +      if s = s' then 
   7.193 +        Conv.binop_conv conv ct 
   7.194 +      else 
   7.195 +        raise CTERM ("const_binop_conv", [ct])
   7.196 +  | _ => raise CTERM ("const_binop_conv", [ct])
   7.197 +
   7.198 +fun reify_conv ct = 
   7.199 +  let
   7.200 +    val rewr = Conv.rewrs_conv o map (fn thm => thm RS @{thm eq_reflection})
   7.201 +    val un = Conv.arg_conv reify_conv
   7.202 +    val bin = Conv.binop_conv reify_conv
   7.203 +  in
   7.204 +    case Thm.term_of ct of
   7.205 +      (Const (@{const_name "fps_from_poly"}, _) $ _) => ct |> Conv.all_conv
   7.206 +    | (Const (@{const_name "Groups.plus"}, _) $ _ $ _) => ct |> (
   7.207 +        bin then_conv rewr @{thms fps_from_poly_add [symmetric]})
   7.208 +    | (Const (@{const_name "Groups.uminus"}, _) $ _) => ct |> (
   7.209 +        un then_conv rewr @{thms fps_from_poly_uminus [symmetric]})
   7.210 +    | (Const (@{const_name "Groups.minus"}, _) $ _ $ _) => ct |> (
   7.211 +        bin then_conv rewr @{thms fps_from_poly_diff [symmetric]})
   7.212 +    | (Const (@{const_name "Groups.times"}, _) $ _ $ _) => ct |> (
   7.213 +        bin then_conv rewr @{thms fps_from_poly_mult [symmetric]})
   7.214 +    | (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _))
   7.215 +        => ct |> (Conv.fun_conv (Conv.arg_conv reify_conv)
   7.216 +             then_conv rewr @{thms fps_from_poly_divide_numeral [symmetric]})
   7.217 +    | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct |> (
   7.218 +        rewr @{thms fps_from_poly_monom' [symmetric]}) 
   7.219 +    | (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> (
   7.220 +        Conv.fun_conv (Conv.arg_conv reify_conv) 
   7.221 +        then_conv rewr @{thms fps_from_poly_power [symmetric]})
   7.222 +    | _ => ct |> (
   7.223 +        rewr @{thms reify_fps_atom [symmetric]})
   7.224 +  end
   7.225 +    
   7.226 +
   7.227 +fun eq_conv ct =
   7.228 +  case Thm.term_of ct of
   7.229 +    (Const (@{const_name "HOL.eq"}, _) $ _ $ _) => ct |> (
   7.230 +      Conv.binop_conv reify_conv
   7.231 +      then_conv Conv.rewr_conv @{thm fps_from_poly_eq_iff[THEN eq_reflection]})
   7.232 +  | _ => raise CTERM ("poly_fps_eq_conv", [ct])
   7.233 +
   7.234 +val eq_simproc = try eq_conv
   7.235 +
   7.236 +end
   7.237 +\<close> 
   7.238 +
   7.239 +simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close>
   7.240 +
   7.241 +lemma fps_from_poly_linear: "fps_from_poly [:a,1 :: 'a :: field:] = X + fps_const a"
   7.242 +  by simp
   7.243 +
   7.244 +lemma fps_from_poly_linear': "fps_from_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
   7.245 +  by simp
   7.246 +
   7.247 +lemma fps_from_poly_cutoff [simp]: 
   7.248 +  "fps_from_poly (poly_cutoff n p) = fps_cutoff n (fps_from_poly p)"
   7.249 +  by (simp add: fps_eq_iff coeff_poly_cutoff)
   7.250 +
   7.251 +lemma fps_from_poly_shift [simp]: "fps_from_poly (poly_shift n p) = fps_shift n (fps_from_poly p)"
   7.252 +  by (simp add: fps_eq_iff coeff_poly_shift)
   7.253 +
   7.254 +
   7.255 +definition poly_subdegree :: "'a::zero poly \<Rightarrow> nat" where
   7.256 +  "poly_subdegree p = subdegree (fps_from_poly p)"
   7.257 +
   7.258 +lemma coeff_less_poly_subdegree:
   7.259 +  "k < poly_subdegree p \<Longrightarrow> coeff p k = 0"
   7.260 +  unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_from_poly p"] by simp
   7.261 +
   7.262 +(* TODO: Move ? *)
   7.263 +definition prefix_length :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" where
   7.264 +  "prefix_length P xs = length (takeWhile P xs)"
   7.265 +
   7.266 +primrec prefix_length_aux :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat" where
   7.267 +  "prefix_length_aux P acc [] = acc"
   7.268 +| "prefix_length_aux P acc (x#xs) = (if P x then prefix_length_aux P (Suc acc) xs else acc)"
   7.269 +
   7.270 +lemma prefix_length_aux_correct: "prefix_length_aux P acc xs = prefix_length P xs + acc"
   7.271 +  by (induction xs arbitrary: acc) (simp_all add: prefix_length_def)
   7.272 +
   7.273 +lemma prefix_length_code [code]: "prefix_length P xs = prefix_length_aux P 0 xs"
   7.274 +  by (simp add: prefix_length_aux_correct)
   7.275 +
   7.276 +lemma prefix_length_le_length: "prefix_length P xs \<le> length xs"
   7.277 +  by (induction xs) (simp_all add: prefix_length_def)
   7.278 +  
   7.279 +lemma prefix_length_less_length: "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> prefix_length P xs < length xs"
   7.280 +  by (induction xs) (simp_all add: prefix_length_def)
   7.281 +
   7.282 +lemma nth_prefix_length:
   7.283 +  "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> \<not>P (xs ! prefix_length P xs)"
   7.284 +  by (induction xs) (simp_all add: prefix_length_def)
   7.285 +  
   7.286 +lemma nth_less_prefix_length:
   7.287 +  "n < prefix_length P xs \<Longrightarrow> P (xs ! n)"
   7.288 +  by (induction xs arbitrary: n) 
   7.289 +     (auto simp: prefix_length_def nth_Cons split: if_splits nat.splits)
   7.290 +(* END TODO *)
   7.291 +  
   7.292 +lemma poly_subdegree_code [code]: "poly_subdegree p = prefix_length (op = 0) (coeffs p)"
   7.293 +proof (cases "p = 0")
   7.294 +  case False
   7.295 +  note [simp] = this
   7.296 +  define n where "n = prefix_length (op = 0) (coeffs p)"
   7.297 +  from False have "\<exists>k. coeff p k \<noteq> 0" by (auto simp: poly_eq_iff)
   7.298 +  hence ex: "\<exists>x\<in>set (coeffs p). x \<noteq> 0" by (auto simp: coeffs_def)
   7.299 +  hence n_less: "n < length (coeffs p)" and nonzero: "coeffs p ! n \<noteq> 0" 
   7.300 +    unfolding n_def by (auto intro!: prefix_length_less_length nth_prefix_length)
   7.301 +  show ?thesis unfolding poly_subdegree_def
   7.302 +  proof (intro subdegreeI)
   7.303 +    from n_less have "fps_from_poly p $ n = coeffs p ! n"
   7.304 +      by (subst coeffs_nth) (simp_all add: degree_eq_length_coeffs)
   7.305 +    with nonzero show "fps_from_poly p $ prefix_length (op = 0) (coeffs p) \<noteq> 0"
   7.306 +      unfolding n_def by simp
   7.307 +  next
   7.308 +    fix k assume A: "k < prefix_length (op = 0) (coeffs p)"
   7.309 +    also have "\<dots> \<le> length (coeffs p)" by (rule prefix_length_le_length)
   7.310 +    finally show "fps_from_poly p $ k = 0"
   7.311 +      using nth_less_prefix_length[OF A]
   7.312 +      by (simp add: coeffs_nth degree_eq_length_coeffs)
   7.313 +  qed
   7.314 +qed (simp_all add: poly_subdegree_def prefix_length_def)
   7.315 +
   7.316 +end
     8.1 --- a/src/HOL/List.thy	Wed Jun 15 15:52:24 2016 +0100
     8.2 +++ b/src/HOL/List.thy	Thu Jun 16 17:57:09 2016 +0200
     8.3 @@ -3039,6 +3039,9 @@
     8.4  lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
     8.5  by(simp add:upt_conv_Cons)
     8.6  
     8.7 +lemma tl_upt: "tl [m..<n] = [Suc m..<n]"
     8.8 +  by (simp add: upt_rec)
     8.9 +
    8.10  lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
    8.11  by(cases j)(auto simp: upt_Suc_append)
    8.12  
     9.1 --- a/src/HOL/Multivariate_Analysis/Gamma.thy	Wed Jun 15 15:52:24 2016 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Thu Jun 16 17:57:09 2016 +0200
     9.3 @@ -71,6 +71,18 @@
     9.4    with assms(1) show False by contradiction
     9.5  qed
     9.6  
     9.7 +lemma fraction_not_in_nats:
     9.8 +  assumes "\<not>n dvd m" "n \<noteq> 0"
     9.9 +  shows   "of_int m / of_int n \<notin> (\<nat> :: 'a :: {division_ring,ring_char_0} set)"
    9.10 +proof
    9.11 +  assume "of_int m / of_int n \<in> (\<nat> :: 'a set)"
    9.12 +  also note Nats_subset_Ints
    9.13 +  finally have "of_int m / of_int n \<in> (\<int> :: 'a set)" .
    9.14 +  moreover have "of_int m / of_int n \<notin> (\<int> :: 'a set)"
    9.15 +    using assms by (intro fraction_not_in_ints)
    9.16 +  ultimately show False by contradiction
    9.17 +qed
    9.18 +
    9.19  lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \<notin> \<int> \<Longrightarrow> z \<notin> \<int>\<^sub>\<le>\<^sub>0"
    9.20    by (auto simp: Ints_def nonpos_Ints_def)
    9.21  
    10.1 --- a/src/HOL/Set_Interval.thy	Wed Jun 15 15:52:24 2016 +0100
    10.2 +++ b/src/HOL/Set_Interval.thy	Thu Jun 16 17:57:09 2016 +0200
    10.3 @@ -1907,6 +1907,9 @@
    10.4  lemma setprod_lessThan_Suc: "setprod f {..<Suc n} = setprod f {..<n} * f n"
    10.5    by (simp add: lessThan_Suc mult.commute)
    10.6  
    10.7 +lemma setprod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
    10.8 +  by (induction n) (simp_all add: lessThan_Suc mult_ac)
    10.9 +
   10.10  lemma setprod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> setprod f {a..<Suc b} = setprod f {a..<b} * f b"
   10.11    by (simp add: atLeastLessThanSuc mult.commute)
   10.12  
    11.1 --- a/src/HOL/Topological_Spaces.thy	Wed Jun 15 15:52:24 2016 +0100
    11.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Jun 16 17:57:09 2016 +0200
    11.3 @@ -1008,6 +1008,9 @@
    11.4  apply (auto intro: less_trans)
    11.5  done
    11.6  
    11.7 +lemma subseq_add: "subseq (\<lambda>n. n + k)"
    11.8 +  by (auto simp: subseq_Suc_iff)
    11.9 +
   11.10  text\<open>for any sequence, there is a monotonic subsequence\<close>
   11.11  lemma seq_monosub:
   11.12    fixes s :: "nat => 'a::linorder"