author eberlm Thu Jun 16 17:57:09 2016 +0200 (2016-06-16) changeset 63317 ca187a9f66da parent 63305 3b6975875633 child 63318 008db47be9dc
Various additions to polynomials, FPSs, Gamma function
 src/HOL/Binomial.thy file | annotate | diff | revisions src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/Groups_List.thy file | annotate | diff | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | revisions src/HOL/Library/Library.thy file | annotate | diff | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | revisions src/HOL/Library/Polynomial_FPS.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Gamma.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions
```     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.12
4.13 @@ -387,6 +390,10 @@
4.14  lemma fps_numeral_nth_0 [simp]: "numeral n \$ 0 = numeral n"
4.16
4.17 +lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
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.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.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.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.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.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.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.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
```
```     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.19
6.20 @@ -869,6 +875,9 @@
6.21  lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
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.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.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.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.79     fixes p q::"'a ::idom poly"
6.81 @@ -3015,6 +3045,200 @@
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.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.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.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.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.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.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.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.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"
```