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