src/HOL/Library/Polynomial.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 64861 9e8de30fd859
child 65346 673a7b3379ec
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 39302
diff changeset
     1
(*  Title:      HOL/Library/Polynomial.thy
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
41959
b460124855b8 tuned headers;
wenzelm
parents: 39302
diff changeset
     3
    Author:     Clemens Ballarin
62352
35a9e1cbb5b3 separated potentially conflicting type class instance into separate theory
haftmann
parents: 62351
diff changeset
     4
    Author:     Amine Chaieb
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
     5
    Author:     Florian Haftmann
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
     6
*)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
     7
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
     8
section \<open>Polynomials as type over a ring structure\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
     9
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    10
theory Polynomial
62352
35a9e1cbb5b3 separated potentially conflicting type class instance into separate theory
haftmann
parents: 62351
diff changeset
    11
imports Main "~~/src/HOL/Deriv" "~~/src/HOL/Library/More_List"
35a9e1cbb5b3 separated potentially conflicting type class instance into separate theory
haftmann
parents: 62351
diff changeset
    12
  "~~/src/HOL/Library/Infinite_Set"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    13
begin
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    14
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
    15
subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    16
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    17
definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    18
where
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    19
  "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    20
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    21
lemma cCons_0_Nil_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    22
  "0 ## [] = []"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    23
  by (simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    24
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    25
lemma cCons_Cons_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    26
  "x ## y # ys = x # y # ys"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    27
  by (simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    28
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    29
lemma cCons_append_Cons_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    30
  "x ## xs @ y # ys = x # xs @ y # ys"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    31
  by (simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    32
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    33
lemma cCons_not_0_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    34
  "x \<noteq> 0 \<Longrightarrow> x ## xs = x # xs"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    35
  by (simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    36
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    37
lemma strip_while_not_0_Cons_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    38
  "strip_while (\<lambda>x. x = 0) (x # xs) = x ## strip_while (\<lambda>x. x = 0) xs"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    39
proof (cases "x = 0")
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    40
  case False then show ?thesis by simp
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    41
next
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    42
  case True show ?thesis
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    43
  proof (induct xs rule: rev_induct)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    44
    case Nil with True show ?case by simp
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    45
  next
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    46
    case (snoc y ys) then show ?case
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    47
      by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    48
  qed
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    49
qed
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    50
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    51
lemma tl_cCons [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    52
  "tl (x ## xs) = xs"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    53
  by (simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    54
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61260
diff changeset
    55
subsection \<open>Definition of type \<open>poly\<close>\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    56
61260
e6f03fae14d5 explicit indication of overloaded typedefs;
wenzelm
parents: 60686
diff changeset
    57
typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
63433
wenzelm
parents: 63317
diff changeset
    58
  morphisms coeff Abs_poly
wenzelm
parents: 63317
diff changeset
    59
  by (auto intro!: ALL_MOST)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    60
59487
adaa430fc0f7 default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents: 58881
diff changeset
    61
setup_lifting type_definition_poly
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    62
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    63
lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    64
  by (simp add: coeff_inject [symmetric] fun_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    65
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    66
lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    67
  by (simp add: poly_eq_iff)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    68
59983
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
    69
lemma MOST_coeff_eq_0: "\<forall>\<^sub>\<infinity> n. coeff p n = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    70
  using coeff [of p] by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    71
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    72
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
    73
subsection \<open>Degree of a polynomial\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    74
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    75
definition degree :: "'a::zero poly \<Rightarrow> nat"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    76
where
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    77
  "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    78
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    79
lemma coeff_eq_0:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    80
  assumes "degree p < n"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    81
  shows "coeff p n = 0"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    82
proof -
59983
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
    83
  have "\<exists>n. \<forall>i>n. coeff p i = 0"
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
    84
    using MOST_coeff_eq_0 by (simp add: MOST_nat)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    85
  then have "\<forall>i>degree p. coeff p i = 0"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    86
    unfolding degree_def by (rule LeastI_ex)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
    87
  with assms show ?thesis by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    88
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    89
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    90
lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    91
  by (erule contrapos_np, rule coeff_eq_0, simp)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    92
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    93
lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    94
  unfolding degree_def by (erule Least_le)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    95
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    96
lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    97
  unfolding degree_def by (drule not_less_Least, simp)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    98
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
    99
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   100
subsection \<open>The zero polynomial\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   101
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   102
instantiation poly :: (zero) zero
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   103
begin
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   104
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   105
lift_definition zero_poly :: "'a poly"
59983
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
   106
  is "\<lambda>_. 0" by (rule MOST_I) simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   107
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   108
instance ..
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   109
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   110
end
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   111
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   112
lemma coeff_0 [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   113
  "coeff 0 n = 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   114
  by transfer rule
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   115
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   116
lemma degree_0 [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   117
  "degree 0 = 0"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   118
  by (rule order_antisym [OF degree_le le0]) simp
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   119
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   120
lemma leading_coeff_neq_0:
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   121
  assumes "p \<noteq> 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   122
  shows "coeff p (degree p) \<noteq> 0"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   123
proof (cases "degree p")
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   124
  case 0
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   125
  from \<open>p \<noteq> 0\<close> have "\<exists>n. coeff p n \<noteq> 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   126
    by (simp add: poly_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   127
  then obtain n where "coeff p n \<noteq> 0" ..
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   128
  hence "n \<le> degree p" by (rule le_degree)
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   129
  with \<open>coeff p n \<noteq> 0\<close> and \<open>degree p = 0\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   130
  show "coeff p (degree p) \<noteq> 0" by simp
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   131
next
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   132
  case (Suc n)
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   133
  from \<open>degree p = Suc n\<close> have "n < degree p" by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   134
  hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   135
  then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   136
  from \<open>degree p = Suc n\<close> and \<open>n < i\<close> have "degree p \<le> i" by simp
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   137
  also from \<open>coeff p i \<noteq> 0\<close> have "i \<le> degree p" by (rule le_degree)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   138
  finally have "degree p = i" .
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   139
  with \<open>coeff p i \<noteq> 0\<close> show "coeff p (degree p) \<noteq> 0" by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   140
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   141
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   142
lemma leading_coeff_0_iff [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   143
  "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   144
  by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   145
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   146
lemma eq_zero_or_degree_less:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   147
  assumes "degree p \<le> n" and "coeff p n = 0"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   148
  shows "p = 0 \<or> degree p < n"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   149
proof (cases n)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   150
  case 0
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   151
  with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close>
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   152
  have "coeff p (degree p) = 0" by simp
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   153
  then have "p = 0" by simp
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   154
  then show ?thesis ..
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   155
next
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   156
  case (Suc m)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   157
  have "\<forall>i>n. coeff p i = 0"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   158
    using \<open>degree p \<le> n\<close> by (simp add: coeff_eq_0)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   159
  then have "\<forall>i\<ge>n. coeff p i = 0"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   160
    using \<open>coeff p n = 0\<close> by (simp add: le_less)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   161
  then have "\<forall>i>m. coeff p i = 0"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   162
    using \<open>n = Suc m\<close> by (simp add: less_eq_Suc_le)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   163
  then have "degree p \<le> m"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   164
    by (rule degree_le)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   165
  then have "degree p < n"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   166
    using \<open>n = Suc m\<close> by (simp add: less_Suc_eq_le)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   167
  then show ?thesis ..
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   168
qed
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   169
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   170
lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 \<Longrightarrow> degree rrr \<le> dr \<Longrightarrow> degree rrr \<le> dr - 1"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   171
  using eq_zero_or_degree_less by fastforce
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   172
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   173
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   174
subsection \<open>List-style constructor for polynomials\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   175
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   176
lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
55415
05f5fdb8d093 renamed 'nat_{case,rec}' to '{case,rec}_nat'
blanchet
parents: 54856
diff changeset
   177
  is "\<lambda>a p. case_nat a (coeff p)"
59983
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
   178
  by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   179
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   180
lemmas coeff_pCons = pCons.rep_eq
29455
0139c9a01ca4 add list-style syntax for pCons
huffman
parents: 29454
diff changeset
   181
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   182
lemma coeff_pCons_0 [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   183
  "coeff (pCons a p) 0 = a"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   184
  by transfer simp
29455
0139c9a01ca4 add list-style syntax for pCons
huffman
parents: 29454
diff changeset
   185
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   186
lemma coeff_pCons_Suc [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   187
  "coeff (pCons a p) (Suc n) = coeff p n"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   188
  by (simp add: coeff_pCons)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   189
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   190
lemma degree_pCons_le:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   191
  "degree (pCons a p) \<le> Suc (degree p)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   192
  by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   193
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   194
lemma degree_pCons_eq:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   195
  "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   196
  apply (rule order_antisym [OF degree_pCons_le])
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   197
  apply (rule le_degree, simp)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   198
  done
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   199
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   200
lemma degree_pCons_0:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   201
  "degree (pCons a 0) = 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   202
  apply (rule order_antisym [OF _ le0])
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   203
  apply (rule degree_le, simp add: coeff_pCons split: nat.split)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   204
  done
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   205
29460
ad87e5d1488b new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents: 29457
diff changeset
   206
lemma degree_pCons_eq_if [simp]:
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   207
  "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   208
  apply (cases "p = 0", simp_all)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   209
  apply (rule order_antisym [OF _ le0])
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   210
  apply (rule degree_le, simp add: coeff_pCons split: nat.split)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   211
  apply (rule order_antisym [OF degree_pCons_le])
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   212
  apply (rule le_degree, simp)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   213
  done
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   214
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   215
lemma pCons_0_0 [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   216
  "pCons 0 0 = 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   217
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   218
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   219
lemma pCons_eq_iff [simp]:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   220
  "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   221
proof safe
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   222
  assume "pCons a p = pCons b q"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   223
  then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   224
  then show "a = b" by simp
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   225
next
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   226
  assume "pCons a p = pCons b q"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   227
  then have "\<forall>n. coeff (pCons a p) (Suc n) =
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   228
                 coeff (pCons b q) (Suc n)" by simp
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   229
  then show "p = q" by (simp add: poly_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   230
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   231
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   232
lemma pCons_eq_0_iff [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   233
  "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   234
  using pCons_eq_iff [of a p 0 0] by simp
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   235
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   236
lemma pCons_cases [cases type: poly]:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   237
  obtains (pCons) a q where "p = pCons a q"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   238
proof
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   239
  show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   240
    by transfer
59983
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
   241
       (simp_all add: MOST_inj[where f=Suc and P="\<lambda>n. p n = 0" for p] fun_eq_iff Abs_poly_inverse
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
   242
                 split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   243
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   244
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   245
lemma pCons_induct [case_names 0 pCons, induct type: poly]:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   246
  assumes zero: "P 0"
54856
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   247
  assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   248
  shows "P p"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   249
proof (induct p rule: measure_induct_rule [where f=degree])
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   250
  case (less p)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   251
  obtain a q where "p = pCons a q" by (rule pCons_cases)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   252
  have "P q"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   253
  proof (cases "q = 0")
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   254
    case True
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   255
    then show "P q" by (simp add: zero)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   256
  next
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   257
    case False
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   258
    then have "degree (pCons a q) = Suc (degree q)"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   259
      by (rule degree_pCons_eq)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   260
    then have "degree q < degree p"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   261
      using \<open>p = pCons a q\<close> by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   262
    then show "P q"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   263
      by (rule less.hyps)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   264
  qed
54856
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   265
  have "P (pCons a q)"
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   266
  proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   267
    case True
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   268
    with \<open>P q\<close> show ?thesis by (auto intro: pCons)
54856
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   269
  next
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   270
    case False
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   271
    with zero show ?thesis by simp
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   272
  qed
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   273
  then show ?case
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   274
    using \<open>p = pCons a q\<close> by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   275
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   276
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   277
lemma degree_eq_zeroE:
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   278
  fixes p :: "'a::zero poly"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   279
  assumes "degree p = 0"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   280
  obtains a where "p = pCons a 0"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   281
proof -
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   282
  obtain a q where p: "p = pCons a q" by (cases p)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   283
  with assms have "q = 0" by (cases "q = 0") simp_all
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   284
  with p have "p = pCons a 0" by simp
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   285
  with that show thesis .
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   286
qed
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   287
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   288
62422
4aa35fd6c152 Tuned Euclidean rings
eberlm
parents: 62352
diff changeset
   289
subsection \<open>Quickcheck generator for polynomials\<close>
4aa35fd6c152 Tuned Euclidean rings
eberlm
parents: 62352
diff changeset
   290
4aa35fd6c152 Tuned Euclidean rings
eberlm
parents: 62352
diff changeset
   291
quickcheck_generator poly constructors: "0 :: _ poly", pCons
4aa35fd6c152 Tuned Euclidean rings
eberlm
parents: 62352
diff changeset
   292
4aa35fd6c152 Tuned Euclidean rings
eberlm
parents: 62352
diff changeset
   293
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   294
subsection \<open>List-style syntax for polynomials\<close>
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   295
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   296
syntax
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   297
  "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   298
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   299
translations
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   300
  "[:x, xs:]" == "CONST pCons x [:xs:]"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   301
  "[:x:]" == "CONST pCons x 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   302
  "[:x:]" <= "CONST pCons x (_constrain 0 t)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   303
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   304
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   305
subsection \<open>Representation of polynomials by lists of coefficients\<close>
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   306
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   307
primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   308
where
54855
d700d054d022 convenient printing of polynomial values
haftmann
parents: 54489
diff changeset
   309
  [code_post]: "Poly [] = 0"
d700d054d022 convenient printing of polynomial values
haftmann
parents: 54489
diff changeset
   310
| [code_post]: "Poly (a # as) = pCons a (Poly as)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   311
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   312
lemma Poly_replicate_0 [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   313
  "Poly (replicate n 0) = 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   314
  by (induct n) simp_all
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   315
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   316
lemma Poly_eq_0:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   317
  "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   318
  by (induct as) (auto simp add: Cons_replicate_eq)
63027
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   319
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   320
lemma Poly_append_replicate_zero [simp]:
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   321
  "Poly (as @ replicate n 0) = Poly as"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   322
  by (induct as) simp_all
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   323
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   324
lemma Poly_snoc_zero [simp]:
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   325
  "Poly (as @ [0]) = Poly as"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   326
  using Poly_append_replicate_zero [of as 1] by simp
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   327
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   328
lemma Poly_cCons_eq_pCons_Poly [simp]:
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   329
  "Poly (a ## p) = pCons a (Poly p)"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   330
  by (simp add: cCons_def)
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   331
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   332
lemma Poly_on_rev_starting_with_0 [simp]:
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   333
  assumes "hd as = 0"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   334
  shows "Poly (rev (tl as)) = Poly (rev as)"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   335
  using assms by (cases as) simp_all
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   336
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   337
lemma degree_Poly: "degree (Poly xs) \<le> length xs"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   338
  by (induction xs) simp_all
63027
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   339
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   340
lemma coeff_Poly_eq [simp]:
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   341
  "coeff (Poly xs) = nth_default 0 xs"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   342
  by (induct xs) (simp_all add: fun_eq_iff coeff_pCons split: nat.splits)
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   343
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   344
definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   345
where
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   346
  "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   347
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   348
lemma coeffs_eq_Nil [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   349
  "coeffs p = [] \<longleftrightarrow> p = 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   350
  by (simp add: coeffs_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   351
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   352
lemma not_0_coeffs_not_Nil:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   353
  "p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   354
  by simp
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   355
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   356
lemma coeffs_0_eq_Nil [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   357
  "coeffs 0 = []"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   358
  by simp
29454
b0f586f38dd7 add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents: 29453
diff changeset
   359
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   360
lemma coeffs_pCons_eq_cCons [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   361
  "coeffs (pCons a p) = a ## coeffs p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   362
proof -
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   363
  { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   364
    assume "\<forall>m\<in>set ms. m > 0"
55415
05f5fdb8d093 renamed 'nat_{case,rec}' to '{case,rec}_nat'
blanchet
parents: 54856
diff changeset
   365
    then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
58199
5fbe474b5da8 explicit theory with additional, less commonly used list operations
haftmann
parents: 57862
diff changeset
   366
      by (induct ms) (auto split: nat.split)
5fbe474b5da8 explicit theory with additional, less commonly used list operations
haftmann
parents: 57862
diff changeset
   367
  }
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   368
  note * = this
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   369
  show ?thesis
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   370
    by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   371
qed
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   372
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   373
lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   374
  by (simp add: coeffs_def)
64860
4d56170d97b3 generalized definition
haftmann
parents: 64849
diff changeset
   375
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   376
lemma coeffs_nth:
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   377
  assumes "p \<noteq> 0" "n \<le> degree p"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   378
  shows   "coeffs p ! n = coeff p n"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   379
  using assms unfolding coeffs_def by (auto simp del: upt_Suc)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   380
64860
4d56170d97b3 generalized definition
haftmann
parents: 64849
diff changeset
   381
lemma coeff_in_coeffs:
4d56170d97b3 generalized definition
haftmann
parents: 64849
diff changeset
   382
  "p \<noteq> 0 \<Longrightarrow> n \<le> degree p \<Longrightarrow> coeff p n \<in> set (coeffs p)"
4d56170d97b3 generalized definition
haftmann
parents: 64849
diff changeset
   383
  using coeffs_nth [of p n, symmetric]
4d56170d97b3 generalized definition
haftmann
parents: 64849
diff changeset
   384
  by (simp add: length_coeffs)
4d56170d97b3 generalized definition
haftmann
parents: 64849
diff changeset
   385
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   386
lemma not_0_cCons_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   387
  "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   388
  by (simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   389
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   390
lemma Poly_coeffs [simp, code abstype]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   391
  "Poly (coeffs p) = p"
54856
356b4c0a2061 more general induction rule;
haftmann
parents: 54855
diff changeset
   392
  by (induct p) auto
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   393
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   394
lemma coeffs_Poly [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   395
  "coeffs (Poly as) = strip_while (HOL.eq 0) as"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   396
proof (induct as)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   397
  case Nil then show ?case by simp
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   398
next
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   399
  case (Cons a as)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   400
  have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   401
    using replicate_length_same [of as 0] by (auto dest: sym [of _ as])
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   402
  with Cons show ?case by auto
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   403
qed
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   404
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   405
lemma last_coeffs_not_0:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   406
  "p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   407
  by (induct p) (auto simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   408
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   409
lemma strip_while_coeffs [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   410
  "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   411
  by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   412
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   413
lemma coeffs_eq_iff:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   414
  "p = q \<longleftrightarrow> coeffs p = coeffs q" (is "?P \<longleftrightarrow> ?Q")
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   415
proof
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   416
  assume ?P then show ?Q by simp
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   417
next
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   418
  assume ?Q
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   419
  then have "Poly (coeffs p) = Poly (coeffs q)" by simp
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   420
  then show ?P by simp
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   421
qed
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   422
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   423
lemma nth_default_coeffs_eq:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   424
  "nth_default 0 (coeffs p) = coeff p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   425
  by (simp add: fun_eq_iff coeff_Poly_eq [symmetric])
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   426
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   427
lemma [code]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   428
  "coeff p = nth_default 0 (coeffs p)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   429
  by (simp add: nth_default_coeffs_eq)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   430
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   431
lemma coeffs_eqI:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   432
  assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   433
  assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   434
  shows "coeffs p = xs"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   435
proof -
63027
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   436
  from coeff have "p = Poly xs" by (simp add: poly_eq_iff)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   437
  with zero show ?thesis by simp (cases xs, simp_all)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   438
qed
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   439
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   440
lemma degree_eq_length_coeffs [code]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   441
  "degree p = length (coeffs p) - 1"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   442
  by (simp add: coeffs_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   443
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   444
lemma length_coeffs_degree:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   445
  "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   446
  by (induct p) (auto simp add: cCons_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   447
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   448
lemma [code abstract]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   449
  "coeffs 0 = []"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   450
  by (fact coeffs_0_eq_Nil)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   451
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   452
lemma [code abstract]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   453
  "coeffs (pCons a p) = a ## coeffs p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   454
  by (fact coeffs_pCons_eq_cCons)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   455
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   456
instantiation poly :: ("{zero, equal}") equal
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   457
begin
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   458
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   459
definition
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   460
  [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   461
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   462
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   463
  by standard (simp add: equal equal_poly_def coeffs_eq_iff)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   464
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   465
end
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   466
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   467
lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   468
  by (fact equal_refl)
29454
b0f586f38dd7 add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents: 29453
diff changeset
   469
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   470
definition is_zero :: "'a::zero poly \<Rightarrow> bool"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   471
where
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   472
  [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   473
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   474
lemma is_zero_null [code_abbrev]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   475
  "is_zero p \<longleftrightarrow> p = 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   476
  by (simp add: is_zero_def null_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   477
63027
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   478
subsubsection \<open>Reconstructing the polynomial from the list\<close>
63145
703edebd1d92 isabelle update_cartouches -c -t;
wenzelm
parents: 63060
diff changeset
   479
  \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
63027
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   480
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   481
definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   482
where
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   483
  [simp]: "poly_of_list = Poly"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   484
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   485
lemma poly_of_list_impl [code abstract]:
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   486
  "coeffs (poly_of_list as) = strip_while (HOL.eq 0) as"
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   487
  by simp
8de0ebee3f1c several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents: 62422
diff changeset
   488
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   489
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   490
subsection \<open>Fold combinator for polynomials\<close>
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   491
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   492
definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   493
where
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   494
  "fold_coeffs f p = foldr f (coeffs p)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   495
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   496
lemma fold_coeffs_0_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   497
  "fold_coeffs f 0 = id"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   498
  by (simp add: fold_coeffs_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   499
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   500
lemma fold_coeffs_pCons_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   501
  "f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   502
  by (simp add: fold_coeffs_def cCons_def fun_eq_iff)
29454
b0f586f38dd7 add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents: 29453
diff changeset
   503
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   504
lemma fold_coeffs_pCons_0_0_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   505
  "fold_coeffs f (pCons 0 0) = id"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   506
  by (simp add: fold_coeffs_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   507
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   508
lemma fold_coeffs_pCons_coeff_not_0_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   509
  "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   510
  by (simp add: fold_coeffs_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   511
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   512
lemma fold_coeffs_pCons_not_0_0_eq [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   513
  "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   514
  by (simp add: fold_coeffs_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   515
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   516
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   517
subsection \<open>Canonical morphism on polynomials -- evaluation\<close>
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   518
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   519
definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   520
where
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61260
diff changeset
   521
  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close>
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   522
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   523
lemma poly_0 [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   524
  "poly 0 x = 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   525
  by (simp add: poly_def)
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   526
  
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   527
lemma poly_pCons [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   528
  "poly (pCons a p) x = a + x * poly p x"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   529
  by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
29454
b0f586f38dd7 add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents: 29453
diff changeset
   530
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   531
lemma poly_altdef: 
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   532
  "poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   533
proof (induction p rule: pCons_induct)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   534
  case (pCons a p)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   535
    show ?case
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   536
    proof (cases "p = 0")
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   537
      case False
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   538
      let ?p' = "pCons a p"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   539
      note poly_pCons[of a p x]
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   540
      also note pCons.IH
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   541
      also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   542
                 coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   543
          by (simp add: field_simps sum_distrib_left coeff_pCons)
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   544
      also note sum_atMost_Suc_shift[symmetric]
62072
bf3d9f113474 isabelle update_cartouches -c -t;
wenzelm
parents: 62067
diff changeset
   545
      also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   546
      finally show ?thesis .
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   547
   qed simp
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   548
qed simp
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   549
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   550
lemma poly_0_coeff_0: "poly p 0 = coeff p 0"
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   551
  by (cases p) (auto simp: poly_altdef)
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   552
29454
b0f586f38dd7 add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents: 29453
diff changeset
   553
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   554
subsection \<open>Monomials\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   555
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   556
lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   557
  is "\<lambda>a m n. if m = n then a else 0"
59983
cd2efd7d06bd replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents: 59815
diff changeset
   558
  by (simp add: MOST_iff_cofinite)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   559
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   560
lemma coeff_monom [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   561
  "coeff (monom a m) n = (if m = n then a else 0)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   562
  by transfer rule
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   563
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   564
lemma monom_0:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   565
  "monom a 0 = pCons a 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   566
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   567
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   568
lemma monom_Suc:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   569
  "monom a (Suc n) = pCons 0 (monom a n)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   570
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   571
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   572
lemma monom_eq_0 [simp]: "monom 0 n = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   573
  by (rule poly_eqI) simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   574
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   575
lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   576
  by (simp add: poly_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   577
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   578
lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   579
  by (simp add: poly_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   580
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   581
lemma degree_monom_le: "degree (monom a n) \<le> n"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   582
  by (rule degree_le, simp)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   583
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   584
lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   585
  apply (rule order_antisym [OF degree_monom_le])
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   586
  apply (rule le_degree, simp)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   587
  done
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   588
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   589
lemma coeffs_monom [code abstract]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   590
  "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   591
  by (induct n) (simp_all add: monom_0 monom_Suc)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   592
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   593
lemma fold_coeffs_monom [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   594
  "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   595
  by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   596
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   597
lemma poly_monom:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   598
  fixes a x :: "'a::{comm_semiring_1}"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   599
  shows "poly (monom a n) x = a * x ^ n"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   600
  by (cases "a = 0", simp_all)
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   601
    (induct n, simp_all add: mult.left_commute poly_def)  
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   602
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   603
lemma monom_eq_iff': "monom c n = monom d m \<longleftrightarrow>  c = d \<and> (c = 0 \<or> n = m)"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   604
  by (auto simp: poly_eq_iff)
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   605
  
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   606
lemma monom_eq_const_iff: "monom c n = [:d:] \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = 0)"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   607
  using monom_eq_iff'[of c n d 0] by (simp add: monom_0)
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   608
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   609
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   610
subsection \<open>Leading coefficient\<close>
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   611
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   612
abbreviation lead_coeff:: "'a::zero poly \<Rightarrow> 'a"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   613
  where "lead_coeff p \<equiv> coeff p (degree p)"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   614
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   615
lemma lead_coeff_pCons[simp]:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   616
  "p \<noteq> 0 \<Longrightarrow> lead_coeff (pCons a p) = lead_coeff p"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   617
  "p = 0 \<Longrightarrow> lead_coeff (pCons a p) = a"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   618
  by auto
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   619
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   620
lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   621
  by (cases "c = 0") (simp_all add: degree_monom_eq)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   622
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   623
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   624
subsection \<open>Addition and subtraction\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   625
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   626
instantiation poly :: (comm_monoid_add) comm_monoid_add
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   627
begin
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   628
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   629
lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   630
  is "\<lambda>p q n. coeff p n + coeff q n"
60040
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   631
proof -
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   632
  fix q p :: "'a poly"
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   633
  show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
60040
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   634
    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   635
qed
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   636
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   637
lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   638
  by (simp add: plus_poly.rep_eq)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   639
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   640
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   641
proof
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   642
  fix p q r :: "'a poly"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   643
  show "(p + q) + r = p + (q + r)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57482
diff changeset
   644
    by (simp add: poly_eq_iff add.assoc)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   645
  show "p + q = q + p"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57482
diff changeset
   646
    by (simp add: poly_eq_iff add.commute)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   647
  show "0 + p = p"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   648
    by (simp add: poly_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   649
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   650
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   651
end
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   652
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   653
instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   654
begin
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   655
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   656
lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   657
  is "\<lambda>p q n. coeff p n - coeff q n"
60040
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   658
proof -
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   659
  fix q p :: "'a poly"
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   660
  show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
60040
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   661
    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   662
qed
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   663
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   664
lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   665
  by (simp add: minus_poly.rep_eq)
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   666
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   667
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   668
proof
29540
8858d197a9b6 more instance declarations for poly
huffman
parents: 29539
diff changeset
   669
  fix p q r :: "'a poly"
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   670
  show "p + q - p = q"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   671
    by (simp add: poly_eq_iff)
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   672
  show "p - q - r = p - (q + r)"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   673
    by (simp add: poly_eq_iff diff_diff_eq)
29540
8858d197a9b6 more instance declarations for poly
huffman
parents: 29539
diff changeset
   674
qed
8858d197a9b6 more instance declarations for poly
huffman
parents: 29539
diff changeset
   675
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   676
end
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   677
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   678
instantiation poly :: (ab_group_add) ab_group_add
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   679
begin
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   680
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   681
lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   682
  is "\<lambda>p n. - coeff p n"
60040
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   683
proof -
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   684
  fix p :: "'a poly"
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   685
  show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
60040
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   686
    using MOST_coeff_eq_0 by simp
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   687
qed
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   688
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   689
lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   690
  by (simp add: uminus_poly.rep_eq)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   691
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   692
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   693
proof
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   694
  fix p q :: "'a poly"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   695
  show "- p + p = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   696
    by (simp add: poly_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   697
  show "p - q = p + - q"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 52380
diff changeset
   698
    by (simp add: poly_eq_iff)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   699
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   700
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   701
end
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   702
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   703
lemma add_pCons [simp]:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   704
  "pCons a p + pCons b q = pCons (a + b) (p + q)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   705
  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   706
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   707
lemma minus_pCons [simp]:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   708
  "- pCons a p = pCons (- a) (- p)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   709
  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   710
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   711
lemma diff_pCons [simp]:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   712
  "pCons a p - pCons b q = pCons (a - b) (p - q)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   713
  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   714
29539
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   715
lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   716
  by (rule degree_le, auto simp add: coeff_eq_0)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   717
29539
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   718
lemma degree_add_le:
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   719
  "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p + q) \<le> n"
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   720
  by (auto intro: order_trans degree_add_le_max)
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   721
29453
de4f26f59135 add lemmas degree_{add,diff}_less
huffman
parents: 29451
diff changeset
   722
lemma degree_add_less:
de4f26f59135 add lemmas degree_{add,diff}_less
huffman
parents: 29451
diff changeset
   723
  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
29539
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   724
  by (auto intro: le_less_trans degree_add_le_max)
29453
de4f26f59135 add lemmas degree_{add,diff}_less
huffman
parents: 29451
diff changeset
   725
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   726
lemma degree_add_eq_right:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   727
  "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   728
  apply (cases "q = 0", simp)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   729
  apply (rule order_antisym)
29539
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   730
  apply (simp add: degree_add_le)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   731
  apply (rule le_degree)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   732
  apply (simp add: coeff_eq_0)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   733
  done
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   734
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   735
lemma degree_add_eq_left:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   736
  "degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   737
  using degree_add_eq_right [of q p]
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57482
diff changeset
   738
  by (simp add: add.commute)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   739
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   740
lemma degree_minus [simp]:
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   741
  "degree (- p) = degree p"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   742
  unfolding degree_def by simp
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   743
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   744
lemma lead_coeff_add_le:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   745
  assumes "degree p < degree q"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   746
  shows "lead_coeff (p + q) = lead_coeff q" 
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   747
  using assms
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   748
  by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   749
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   750
lemma lead_coeff_minus:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   751
  "lead_coeff (- p) = - lead_coeff p"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   752
  by (metis coeff_minus degree_minus)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   753
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   754
lemma degree_diff_le_max:
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   755
  fixes p q :: "'a :: ab_group_add poly"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   756
  shows "degree (p - q) \<le> max (degree p) (degree q)"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   757
  using degree_add_le [where p=p and q="-q"]
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 52380
diff changeset
   758
  by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   759
29539
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   760
lemma degree_diff_le:
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   761
  fixes p q :: "'a :: ab_group_add poly"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   762
  assumes "degree p \<le> n" and "degree q \<le> n"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   763
  shows "degree (p - q) \<le> n"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   764
  using assms degree_add_le [of p n "- q"] by simp
29539
abfe2af6883e add lemmas about degree
huffman
parents: 29537
diff changeset
   765
29453
de4f26f59135 add lemmas degree_{add,diff}_less
huffman
parents: 29451
diff changeset
   766
lemma degree_diff_less:
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   767
  fixes p q :: "'a :: ab_group_add poly"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   768
  assumes "degree p < n" and "degree q < n"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   769
  shows "degree (p - q) < n"
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59557
diff changeset
   770
  using assms degree_add_less [of p n "- q"] by simp
29453
de4f26f59135 add lemmas degree_{add,diff}_less
huffman
parents: 29451
diff changeset
   771
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   772
lemma add_monom: "monom a n + monom b n = monom (a + b) n"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   773
  by (rule poly_eqI) simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   774
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   775
lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   776
  by (rule poly_eqI) simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   777
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   778
lemma minus_monom: "- monom a n = monom (-a) n"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   779
  by (rule poly_eqI) simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   780
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   781
lemma coeff_sum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   782
  by (cases "finite A", induct set: finite, simp_all)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   783
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   784
lemma monom_sum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   785
  by (rule poly_eqI) (simp add: coeff_sum)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   786
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   787
fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   788
where
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   789
  "plus_coeffs xs [] = xs"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   790
| "plus_coeffs [] ys = ys"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   791
| "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   792
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   793
lemma coeffs_plus_eq_plus_coeffs [code abstract]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   794
  "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   795
proof -
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   796
  { fix xs ys :: "'a list" and n
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   797
    have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   798
    proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   799
      case (3 x xs y ys n)
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   800
      then show ?case by (cases n) (auto simp add: cCons_def)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   801
    qed simp_all }
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   802
  note * = this
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   803
  { fix xs ys :: "'a list"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   804
    assume "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   805
    moreover assume "plus_coeffs xs ys \<noteq> []"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   806
    ultimately have "last (plus_coeffs xs ys) \<noteq> 0"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   807
    proof (induct xs ys rule: plus_coeffs.induct)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   808
      case (3 x xs y ys) then show ?case by (auto simp add: cCons_def) metis
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   809
    qed simp_all }
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   810
  note ** = this
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   811
  show ?thesis
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   812
    apply (rule coeffs_eqI)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   813
    apply (simp add: * nth_default_coeffs_eq)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   814
    apply (rule **)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   815
    apply (auto dest: last_coeffs_not_0)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   816
    done
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   817
qed
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   818
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   819
lemma coeffs_uminus [code abstract]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   820
  "coeffs (- p) = map (\<lambda>a. - a) (coeffs p)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   821
  by (rule coeffs_eqI)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   822
    (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   823
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   824
lemma [code]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   825
  fixes p q :: "'a::ab_group_add poly"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   826
  shows "p - q = p + - q"
59557
ebd8ecacfba6 establish unique preferred fact names
haftmann
parents: 59487
diff changeset
   827
  by (fact diff_conv_add_uminus)
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   828
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   829
lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   830
  apply (induct p arbitrary: q, simp)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   831
  apply (case_tac q, simp, simp add: algebra_simps)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   832
  done
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   833
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   834
lemma poly_minus [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   835
  fixes x :: "'a::comm_ring"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   836
  shows "poly (- p) x = - poly p x"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   837
  by (induct p) simp_all
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   838
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   839
lemma poly_diff [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   840
  fixes x :: "'a::comm_ring"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   841
  shows "poly (p - q) x = poly p x - poly q x"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 52380
diff changeset
   842
  using poly_add [of p "- q" x] by simp
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   843
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   844
lemma poly_sum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   845
  by (induct A rule: infinite_finite_induct) simp_all
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   846
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   847
lemma degree_sum_le: "finite S \<Longrightarrow> (\<And> p . p \<in> S \<Longrightarrow> degree (f p) \<le> n)
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   848
  \<Longrightarrow> degree (sum f S) \<le> n"
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   849
proof (induct S rule: finite_induct)
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   850
  case (insert p S)
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   851
  hence "degree (sum f S) \<le> n" "degree (f p) \<le> n" by auto
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   852
  thus ?case unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le)
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   853
qed simp
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   854
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   855
lemma poly_as_sum_of_monoms': 
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   856
  assumes n: "degree p \<le> n" 
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   857
  shows "(\<Sum>i\<le>n. monom (coeff p i) i) = p"
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   858
proof -
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   859
  have eq: "\<And>i. {..n} \<inter> {i} = (if i \<le> n then {i} else {})"
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   860
    by auto
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   861
  show ?thesis
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
   862
    using n by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq 
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   863
                  if_distrib[where f="\<lambda>x. x * a" for a])
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   864
qed
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   865
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   866
lemma poly_as_sum_of_monoms: "(\<Sum>i\<le>degree p. monom (coeff p i) i) = p"
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   867
  by (intro poly_as_sum_of_monoms' order_refl)
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
   868
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   869
lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   870
  by (induction xs) (simp_all add: monom_0 monom_Suc)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
   871
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   872
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   873
subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   874
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   875
lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   876
  is "\<lambda>a p n. a * coeff p n"
60040
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   877
proof -
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   878
  fix a :: 'a and p :: "'a poly" show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
1fa1023b13b9 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents: 59983
diff changeset
   879
    using MOST_coeff_eq_0[of p] by eventually_elim simp
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   880
qed
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   881
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   882
lemma coeff_smult [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   883
  "coeff (smult a p) n = a * coeff p n"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   884
  by (simp add: smult.rep_eq)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   885
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   886
lemma degree_smult_le: "degree (smult a p) \<le> degree p"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   887
  by (rule degree_le, simp add: coeff_eq_0)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   888
29472
a63a2e46cec9 declare smult rules [simp]
huffman
parents: 29471
diff changeset
   889
lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57482
diff changeset
   890
  by (rule poly_eqI, simp add: mult.assoc)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   891
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   892
lemma smult_0_right [simp]: "smult a 0 = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   893
  by (rule poly_eqI, simp)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   894
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   895
lemma smult_0_left [simp]: "smult 0 p = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   896
  by (rule poly_eqI, simp)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   897
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   898
lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   899
  by (rule poly_eqI, simp)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   900
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   901
lemma smult_add_right:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   902
  "smult a (p + q) = smult a p + smult a q"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   903
  by (rule poly_eqI, simp add: algebra_simps)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   904
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   905
lemma smult_add_left:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   906
  "smult (a + b) p = smult a p + smult b p"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   907
  by (rule poly_eqI, simp add: algebra_simps)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   908
29457
2eadbc24de8c correctness and uniqueness of synthetic division
huffman
parents: 29456
diff changeset
   909
lemma smult_minus_right [simp]:
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   910
  "smult (a::'a::comm_ring) (- p) = - smult a p"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   911
  by (rule poly_eqI, simp)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   912
29457
2eadbc24de8c correctness and uniqueness of synthetic division
huffman
parents: 29456
diff changeset
   913
lemma smult_minus_left [simp]:
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   914
  "smult (- a::'a::comm_ring) p = - smult a p"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   915
  by (rule poly_eqI, simp)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   916
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   917
lemma smult_diff_right:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   918
  "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   919
  by (rule poly_eqI, simp add: algebra_simps)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   920
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   921
lemma smult_diff_left:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   922
  "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   923
  by (rule poly_eqI, simp add: algebra_simps)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   924
29472
a63a2e46cec9 declare smult rules [simp]
huffman
parents: 29471
diff changeset
   925
lemmas smult_distribs =
a63a2e46cec9 declare smult rules [simp]
huffman
parents: 29471
diff changeset
   926
  smult_add_left smult_add_right
a63a2e46cec9 declare smult rules [simp]
huffman
parents: 29471
diff changeset
   927
  smult_diff_left smult_diff_right
a63a2e46cec9 declare smult rules [simp]
huffman
parents: 29471
diff changeset
   928
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   929
lemma smult_pCons [simp]:
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   930
  "smult a (pCons b p) = pCons (a * b) (smult a p)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   931
  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   932
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   933
lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   934
  by (induct n, simp add: monom_0, simp add: monom_Suc)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   935
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   936
lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
   937
  by (auto simp add: poly_eq_iff nth_default_def)
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   938
29659
f8d2c03ecfd8 add lemmas about smult
huffman
parents: 29540
diff changeset
   939
lemma degree_smult_eq [simp]:
63498
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
   940
  fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
29659
f8d2c03ecfd8 add lemmas about smult
huffman
parents: 29540
diff changeset
   941
  shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
f8d2c03ecfd8 add lemmas about smult
huffman
parents: 29540
diff changeset
   942
  by (cases "a = 0", simp, simp add: degree_def)
f8d2c03ecfd8 add lemmas about smult
huffman
parents: 29540
diff changeset
   943
f8d2c03ecfd8 add lemmas about smult
huffman
parents: 29540
diff changeset
   944
lemma smult_eq_0_iff [simp]:
63498
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
   945
  fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
29659
f8d2c03ecfd8 add lemmas about smult
huffman
parents: 29540
diff changeset
   946
  shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   947
  by (simp add: poly_eq_iff)
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
   948
  
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   949
lemma coeffs_smult [code abstract]:
63498
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
   950
  fixes p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   951
  shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   952
  by (rule coeffs_eqI)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   953
    (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   954
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   955
lemma smult_eq_iff:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   956
  assumes "(b :: 'a :: field) \<noteq> 0"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   957
  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   958
proof
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   959
  assume "smult a p = smult b q"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   960
  also from assms have "smult (inverse b) \<dots> = q" by simp
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   961
  finally show "smult (a / b) p = q" by (simp add: field_simps)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   962
qed (insert assms, auto)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
   963
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   964
instantiation poly :: (comm_semiring_0) comm_semiring_0
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   965
begin
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   966
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   967
definition
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   968
  "p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0"
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   969
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   970
lemma mult_poly_0_left: "(0::'a poly) * q = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   971
  by (simp add: times_poly_def)
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   972
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   973
lemma mult_pCons_left [simp]:
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   974
  "pCons a p * q = smult a q + pCons 0 (p * q)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   975
  by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def)
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   976
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   977
lemma mult_poly_0_right: "p * (0::'a poly) = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   978
  by (induct p) (simp add: mult_poly_0_left, simp)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   979
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   980
lemma mult_pCons_right [simp]:
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   981
  "p * pCons a q = smult a p + pCons 0 (p * q)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   982
  by (induct p) (simp add: mult_poly_0_left, simp add: algebra_simps)
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   983
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   984
lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   985
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   986
lemma mult_smult_left [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   987
  "smult a p * q = smult a (p * q)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   988
  by (induct p) (simp add: mult_poly_0, simp add: smult_add_right)
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   989
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   990
lemma mult_smult_right [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   991
  "p * smult a q = smult a (p * q)"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   992
  by (induct q) (simp add: mult_poly_0, simp add: smult_add_right)
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   993
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   994
lemma mult_poly_add_left:
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   995
  fixes p q r :: "'a poly"
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
   996
  shows "(p + q) * r = p * r + q * r"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
   997
  by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
   998
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
   999
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
  1000
proof
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1001
  fix p q r :: "'a poly"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1002
  show 0: "0 * p = 0"
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1003
    by (rule mult_poly_0_left)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1004
  show "p * 0 = 0"
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1005
    by (rule mult_poly_0_right)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1006
  show "(p + q) * r = p * r + q * r"
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1007
    by (rule mult_poly_add_left)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1008
  show "(p * q) * r = p * (q * r)"
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1009
    by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1010
  show "p * q = q * p"
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1011
    by (induct p, simp add: mult_poly_0, simp)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1012
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1013
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1014
end
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1015
63498
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1016
lemma coeff_mult_degree_sum:
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1017
  "coeff (p * q) (degree p + degree q) =
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1018
   coeff p (degree p) * coeff q (degree q)"
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1019
  by (induct p, simp, simp add: coeff_eq_0)
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1020
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1021
instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1022
proof
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1023
  fix p q :: "'a poly"
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1024
  assume "p \<noteq> 0" and "q \<noteq> 0"
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1025
  have "coeff (p * q) (degree p + degree q) =
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1026
        coeff p (degree p) * coeff q (degree q)"
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1027
    by (rule coeff_mult_degree_sum)
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1028
  also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1029
    using \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> by simp
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1030
  finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1031
  thus "p * q \<noteq> 0" by (simp add: poly_eq_iff)
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1032
qed
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1033
29540
8858d197a9b6 more instance declarations for poly
huffman
parents: 29539
diff changeset
  1034
instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
8858d197a9b6 more instance declarations for poly
huffman
parents: 29539
diff changeset
  1035
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1036
lemma coeff_mult:
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1037
  "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1038
proof (induct p arbitrary: n)
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1039
  case 0 show ?case by simp
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1040
next
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1041
  case (pCons a p n) thus ?case
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
  1042
    by (cases n, simp, simp add: sum_atMost_Suc_shift
b9a1486e79be setsum -> sum
nipkow
parents: 63950
diff changeset
  1043
                            del: sum_atMost_Suc)
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1044
qed
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1045
29474
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1046
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1047
apply (rule degree_le)
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1048
apply (induct p)
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1049
apply simp
674a21226c5a define polynomial multiplication using poly_rec
huffman
parents: 29472
diff changeset
  1050
apply (simp add: coeff_eq_0 coeff_pCons split: nat.split)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1051
done
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1052
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1053
lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
  1054
  by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1055
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1056
instantiation poly :: (comm_semiring_1) comm_semiring_1
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1057
begin
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1058
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
  1059
definition one_poly_def: "1 = pCons 1 0"
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1060
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
  1061
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
  1062
proof
ade12ef2773c tuned proofs;
wenzelm
parents: 60570
diff changeset
  1063
  show "1 * p = p" for p :: "'a poly"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1064
    unfolding one_poly_def by simp
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1065
  show "0 \<noteq> (1::'a poly)"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1066
    unfolding one_poly_def by simp
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1067
qed
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1068
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1069
end
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1070
63498
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1071
instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors ..
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1072
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1073
instance poly :: (comm_ring) comm_ring ..
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1074
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1075
instance poly :: (comm_ring_1) comm_ring_1 ..
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1076
63498
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1077
instance poly :: (comm_ring_1) comm_semiring_1_cancel ..
a3fe3250d05d Reformed factorial rings
eberlm <eberlm@in.tum.de>
parents: 63433
diff changeset
  1078
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1079
lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1080
  unfolding one_poly_def
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1081
  by (simp add: coeff_pCons split: nat.split)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1082
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1083
lemma monom_eq_1 [simp]:
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1084
  "monom 1 0 = 1"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1085
  by (simp add: monom_0 one_poly_def)
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
  1086
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
  1087
lemma monom_eq_1_iff: "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
  1088
  using monom_eq_const_iff[of c n 1] by (auto simp: one_poly_def)
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
  1089
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
  1090
lemma monom_altdef:
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
  1091
  "monom c n = smult c ([:0, 1:]^n)"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63145
diff changeset
  1092
  by (induction n) (simp_all add: monom_0 monom_Suc one_poly_def)
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1093
  
29451
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1094
lemma degree_1 [simp]: "degree 1 = 0"
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1095
  unfolding one_poly_def
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1096
  by (rule degree_pCons_0)
5f0cb3fa530d new theory of polynomials
huffman
parents:
diff changeset
  1097
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1098
lemma coeffs_1_eq [simp, code abstract]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1099
  "coeffs 1 = [1]"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1100
  by (simp add: one_poly_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1101
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1102
lemma degree_power_le:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1103
  "degree (p ^ n) \<le> degree p * n"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1104
  by (induct n) (auto intro: order_trans degree_mult_le)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1105
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1106
lemma coeff_0_power:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1107
  "coeff (p ^ n) 0 = coeff p 0 ^ n"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1108
  by (induction n) (simp_all add: coeff_mult)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1109
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1110
lemma poly_smult [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1111
  "poly (smult a p) x = a * poly p x"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1112
  by (induct p, simp, simp add: algebra_simps)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1113
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1114
lemma poly_mult [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1115
  "poly (p * q) x = poly p x * poly q x"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1116
  by (induct p, simp_all, simp add: algebra_simps)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1117
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1118
lemma poly_1 [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1119
  "poly 1 x = 1"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1120
  by (simp add: one_poly_def)
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1121
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1122
lemma poly_power [simp]:
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1123
  fixes p :: "'a::{comm_semiring_1} poly"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1124
  shows "poly (p ^ n) x = poly p x ^ n"
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1125
  by (induct n) simp_all
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 49962
diff changeset
  1126
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
  1127
lemma poly_prod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
  1128
  by (induct A rule: infinite_finite_induct) simp_all
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
  1129
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
  1130
lemma degree_prod_sum_le: "finite S \<Longrightarrow> degree (prod f S) \<le> sum (degree o f) S"
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
  1131
proof (induct S rule: finite_induct)
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
  1132
  case (insert a S)
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
  1133
  show ?case unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
  1134
    by (rule le_trans[OF degree_mult_le], insert insert, auto)
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
  1135
qed simp
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 62072
diff changeset
  1136
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1137
lemma coeff_0_prod_list:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1138
  "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1139
  by (induction xs) (simp_all add: coeff_mult)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1140
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1141
lemma coeff_monom_mult: 
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1142
  "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1143
proof -
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1144
  have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k - i))"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1145
    by (simp add: coeff_mult)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1146
  also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1147
    by (intro sum.cong) simp_all
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1148
  also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))" by (simp add: sum.delta')
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1149
  finally show ?thesis .
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1150
qed
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1151
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1152
lemma monom_1_dvd_iff':
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1153
  "monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1154
proof
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1155
  assume "monom 1 n dvd p"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1156
  then obtain r where r: "p = monom 1 n * r" by (elim dvdE)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1157
  thus "\<forall>k<n. coeff p k = 0" by (simp add: coeff_mult)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1158
next
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1159
  assume zero: "(\<forall>k<n. coeff p k = 0)"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1160
  define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1161
  have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1162
    by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, 
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1163
        subst cofinite_eq_sequentially [symmetric]) transfer
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1164
  hence coeff_r [simp]: "coeff r k = coeff p (k + n)" for k unfolding r_def
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1165
    by (subst poly.Abs_poly_inverse) simp_all
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1166
  have "p = monom 1 n * r"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1167
    by (intro poly_eqI, subst coeff_monom_mult) (insert zero, simp_all)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1168
  thus "monom 1 n dvd p" by simp
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1169
qed
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1170
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1171
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1172
subsection \<open>Mapping polynomials\<close>
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1173
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1174
definition map_poly 
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1175
     :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1176
  "map_poly f p = Poly (map f (coeffs p))"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1177
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1178
lemma map_poly_0 [simp]: "map_poly f 0 = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1179
  by (simp add: map_poly_def)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1180
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1181
lemma map_poly_1: "map_poly f 1 = [:f 1:]"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1182
  by (simp add: map_poly_def)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1183
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1184
lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1185
  by (simp add: map_poly_def one_poly_def)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1186
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1187
lemma coeff_map_poly:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1188
  assumes "f 0 = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1189
  shows   "coeff (map_poly f p) n = f (coeff p n)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1190
  by (auto simp: map_poly_def nth_default_def coeffs_def assms
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1191
        not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1192
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1193
lemma coeffs_map_poly [code abstract]: 
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1194
    "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1195
  by (simp add: map_poly_def)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1196
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1197
lemma set_coeffs_map_poly:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1198
  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1199
  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1200
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1201
lemma coeffs_map_poly': 
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1202
  assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1203
  shows   "coeffs (map_poly f p) = map f (coeffs p)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1204
  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1205
                           intro!: strip_while_not_last split: if_splits)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1206
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1207
lemma degree_map_poly:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1208
  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1209
  shows   "degree (map_poly f p) = degree p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1210
  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1211
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1212
lemma map_poly_eq_0_iff:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1213
  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1214
  shows   "map_poly f p = 0 \<longleftrightarrow> p = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1215
proof -
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1216
  {
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1217
    fix n :: nat
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1218
    have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1219
    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1220
    proof (cases "n < length (coeffs p)")
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1221
      case True
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1222
      hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1223
      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1224
    qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1225
    finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1226
  }
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1227
  thus ?thesis by (auto simp: poly_eq_iff)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1228
qed
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1229
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1230
lemma map_poly_smult:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1231
  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1232
  shows   "map_poly f (smult c p) = smult (f c) (map_poly f p)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1233
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1234
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1235
lemma map_poly_pCons:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1236
  assumes "f 0 = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1237
  shows   "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1238
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1239
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1240
lemma map_poly_map_poly:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1241
  assumes "f 0 = 0" "g 0 = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1242
  shows   "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1243
  by (intro poly_eqI) (simp add: coeff_map_poly assms)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1244
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1245
lemma map_poly_id [simp]: "map_poly id p = p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1246
  by (simp add: map_poly_def)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1247
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1248
lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1249
  by (simp add: map_poly_def)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1250
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1251
lemma map_poly_cong: 
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1252
  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1253
  shows   "map_poly f p = map_poly g p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1254
proof -
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1255
  from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1256
  thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1257
qed
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1258
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1259
lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1260
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1261
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1262
lemma map_poly_idI:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1263
  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1264
  shows   "map_poly f p = p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1265
  using map_poly_cong[OF assms, of _ id] by simp
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1266
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1267
lemma map_poly_idI':
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1268
  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1269
  shows   "p = map_poly f p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1270
  using map_poly_cong[OF assms, of _ id] by simp
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1271
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1272
lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1273
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1274
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64272
diff changeset
  1275
64793
3df00fb1ce0b more lemmas;
haftmann
parents: 64635
diff changeset
  1276
subsection \<open>Conversions from @{typ nat} and @{typ int} numbers\<close>
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1277
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1278
lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1279
proof (induction n)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1280
  case (Suc n)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1281
  hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" 
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1282
    by simp
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1283
  also have "(of_nat n :: 'a poly) = [: of_nat n :]" 
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1284
    by (subst Suc) (rule refl)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1285
  also have "1 = [:1:]" by (simp add: one_poly_def)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1286
  finally show ?case by (subst (asm) add_pCons) simp
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1287
qed simp
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1288
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1289
lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1290
  by (simp add: of_nat_poly)
1546a042e87b Added some facts about polynomials
eberlm
parents: 61945
diff changeset
  1291
64795
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1292
lemma lead_coeff_of_nat [simp]:
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1293
  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1294
  by (simp add: of_nat_poly)
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1295
8e7db8df16a0 tuned structure
haftmann
parents: 64794
diff changeset
  1296
lemma of_int_poly: "of_int k = [:of_int k :: 'a :: comm_ring_1:]"
64793
3df00fb1ce0b more lemmas;
haftmann
parents: 64635
diff changeset
  1297
  by (simp only: of_int_of_nat of_nat_poly) simp
3df00fb1ce0b more lemmas;
haftmann
parents: 64635
diff changeset
  1298
64795
8e7db8df16a0 tuned structure
haftman