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