src/HOL/Algebra/poly/UnivPoly2.thy
author wenzelm
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 35849 b5522b51cb1e
child 41959 b460124855b8
permissions -rw-r--r--
clarified example settings for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35849
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     1
(*  Title:      Univariate Polynomials
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     2
    Author:     Clemens Ballarin, started 9 December 1996
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     3
    Copyright:  Clemens Ballarin
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     4
*)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     5
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     6
header {* Univariate Polynomials *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     7
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15045
diff changeset
     8
theory UnivPoly2
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15045
diff changeset
     9
imports "../abstract/Abstract"
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15045
diff changeset
    10
begin
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    11
16640
03bdf544a552 Removed setsubgoaler hack (thanks to strong_setsum_cong).
berghofe
parents: 16052
diff changeset
    12
(* With this variant of setsum_cong, assumptions
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    13
   like i:{m..n} get simplified (to m <= i & i <= n). *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    14
16640
03bdf544a552 Removed setsubgoaler hack (thanks to strong_setsum_cong).
berghofe
parents: 16052
diff changeset
    15
declare strong_setsum_cong [cong]
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    16
35849
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
    17
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    18
section {* Definition of type up *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    19
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    20
definition
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    21
  bound :: "[nat, nat => 'a::zero] => bool" where
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    22
  "bound n f = (ALL i. n < i --> f i = 0)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    23
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    24
lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    25
  unfolding bound_def by blast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    26
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    27
lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    28
  unfolding bound_def by blast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    29
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    30
lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    31
  unfolding bound_def by blast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    32
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    33
lemma bound_below:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    34
  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    35
proof (rule classical)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    36
  assume "~ ?thesis"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    37
  then have "m < n" by arith
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    38
  with bound have "f n = 0" ..
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    39
  with nonzero show ?thesis by contradiction
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    40
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    41
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    42
typedef (UP)
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    43
    ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    44
  by (rule+)   (* Question: what does trace_rule show??? *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    45
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    46
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    47
section {* Constants *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    48
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    49
definition
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
    50
  coeff :: "['a up, nat] => ('a::zero)"
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
    51
  where "coeff p n = Rep_UP p n"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    52
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    53
definition
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
    54
  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70)
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
    55
  where "monom a n = Abs_UP (%i. if i=n then a else 0)"
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    56
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    57
definition
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
    58
  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70)
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
    59
  where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    60
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    61
lemma coeff_bound_ex: "EX n. bound n (coeff p)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    62
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    63
  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    64
  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    65
  then show ?thesis ..
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    66
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    67
  
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    68
lemma bound_coeff_obtain:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    69
  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    70
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    71
  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    72
  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    73
  with prem show P .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    74
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    75
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
    76
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    77
text {* Ring operations *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    78
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    79
instantiation up :: (zero) zero
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    80
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    81
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    82
definition
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    83
  up_zero_def: "0 = monom 0 0"
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    84
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    85
instance ..
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    86
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    87
end
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    88
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    89
instantiation up :: ("{one, zero}") one
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    90
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    91
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    92
definition
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    93
  up_one_def: "1 = monom 1 0"
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    94
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    95
instance ..
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    96
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    97
end
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    98
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
    99
instantiation up :: ("{plus, zero}") plus
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   100
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   101
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   102
definition
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   103
  up_add_def: "p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   104
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   105
instance ..
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   106
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   107
end
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   108
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   109
instantiation up :: ("{one, times, uminus, zero}") uminus
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   110
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   111
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   112
definition
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   113
  (* note: - 1 is different from -1; latter is of class number *)
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   114
  up_uminus_def:"- p = (- 1) *s p"
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   115
  (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   116
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   117
instance ..
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   118
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   119
end
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   120
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   121
instantiation up :: ("{one, plus, times, minus, uminus, zero}") minus
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   122
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   123
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   124
definition
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   125
  up_minus_def: "(a :: 'a up) - b = a + (-b)"
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   126
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   127
instance ..
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   128
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   129
end
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   130
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   131
instantiation up :: ("{times, comm_monoid_add}") times
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   132
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   133
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   134
definition
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
   135
  up_mult_def: "p * q = Abs_UP (%n::nat. setsum
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   136
                     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   137
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   138
instance ..
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   139
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   140
end
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   141
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 33657
diff changeset
   142
instance up :: ("{times, comm_monoid_add}") Rings.dvd ..
26563
420567ad8125 explicit dummy instantiation for div
haftmann
parents: 26480
diff changeset
   143
420567ad8125 explicit dummy instantiation for div
haftmann
parents: 26480
diff changeset
   144
instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   145
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   146
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   147
definition
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   148
  up_inverse_def: "inverse (a :: 'a up) = (if a dvd 1 then
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   149
                     THE x. a * x = 1 else 0)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   150
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   151
definition
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
   152
  up_divide_def: "(a :: 'a up) / b = a * inverse b"
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   153
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   154
instance ..
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   155
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 24993
diff changeset
   156
end
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   157
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   158
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   159
subsection {* Effect of operations on coefficients *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   160
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   161
lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   162
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   163
  have "(%n. if n = m then a else 0) : UP"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   164
    using UP_def by force
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   165
  from this show ?thesis
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   166
    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   167
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   168
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   169
lemma coeff_zero [simp]: "coeff 0 n = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   170
proof (unfold up_zero_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   171
qed simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   172
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   173
lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   174
proof (unfold up_one_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   175
qed simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   176
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   177
(* term order
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   178
lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   179
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   180
  have "!!f. f : UP ==> (%n. a * f n) : UP"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 27651
diff changeset
   181
    by (unfold UP_def) (force simp add: algebra_simps)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   182
*)      (* this force step is slow *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   183
(*  then show ?thesis
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   184
    apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   185
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   186
*)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   187
lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   188
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   189
  have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 27651
diff changeset
   190
    by (unfold UP_def) (force simp add: algebra_simps)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   191
      (* this force step is slow *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   192
  then show ?thesis
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   193
    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   194
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   195
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   196
lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   197
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   198
  {
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   199
    fix f g
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   200
    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   201
    have "(%i. f i + g i) : UP"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   202
    proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   203
      from fup obtain n where boundn: "bound n f"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   204
        by (unfold UP_def) fast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   205
      from gup obtain m where boundm: "bound m g"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   206
        by (unfold UP_def) fast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   207
      have "bound (max n m) (%i. (f i + g i))"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   208
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   209
        fix i
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   210
        assume "max n m < i"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   211
        with boundn and boundm show "f i + g i = 0"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 27651
diff changeset
   212
          by (fastsimp simp add: algebra_simps)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   213
      qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   214
      then show "(%i. (f i + g i)) : UP"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   215
        by (unfold UP_def) fast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   216
    qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   217
  }
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   218
  then show ?thesis
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   219
    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   220
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   221
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   222
lemma coeff_mult [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   223
  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   224
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   225
  {
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   226
    fix f g
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   227
    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   228
    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   229
    proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   230
      from fup obtain n where "bound n f"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   231
        by (unfold UP_def) fast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   232
      from gup obtain m where "bound m g"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   233
        by (unfold UP_def) fast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   234
      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   235
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   236
        fix k
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   237
        assume bound: "n + m < k"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   238
        {
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   239
          fix i
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   240
          have "f i * g (k-i) = 0"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   241
          proof cases
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   242
            assume "n < i"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   243
            with `bound n f` show ?thesis by (auto simp add: algebra_simps)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   244
          next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   245
            assume "~ (n < i)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   246
            with bound have "m < k-i" by arith
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   247
            with `bound m g` show ?thesis by (auto simp add: algebra_simps)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   248
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   249
        }
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   250
        then show "setsum (%i. f i * g (k-i)) {..k} = 0"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   251
          by (simp add: algebra_simps)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   252
      qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   253
      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   254
        by (unfold UP_def) fast
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   255
    qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   256
  }
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   257
  then show ?thesis
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   258
    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   259
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   260
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   261
lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 27651
diff changeset
   262
by (unfold up_uminus_def) (simp add: algebra_simps)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   263
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   264
(* Other lemmas *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   265
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   266
lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   267
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   268
  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   269
  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   270
  also have "... = q" by (simp add: Rep_UP_inverse)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   271
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   272
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   273
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 25762
diff changeset
   274
(* ML {* Addsimprocs [ring_simproc] *} *)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   275
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   276
instance up :: (ring) ring
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   277
proof
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   278
  fix p q r :: "'a::ring up"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   279
  show "(p + q) + r = p + (q + r)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   280
    by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   281
  show "0 + p = p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   282
    by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   283
  show "(-p) + p = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   284
    by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   285
  show "p + q = q + p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   286
    by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   287
  show "(p * q) * r = p * (q * r)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   288
  proof (rule up_eqI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   289
    fix n 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   290
    {
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   291
      fix k and a b c :: "nat=>'a::ring"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   292
      have "k <= n ==> 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   293
        setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   294
        setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   295
        (is "_ ==> ?eq k")
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   296
      proof (induct k)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   297
        case 0 show ?case by simp
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   298
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   299
        case (Suc k)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   300
        then have "k <= n" by arith
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   301
        then have "?eq k" by (rule Suc)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   302
        then show ?case
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   303
          by (simp add: Suc_diff_le natsum_ldistr)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   304
      qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   305
    }
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   306
    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   307
      by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   308
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   309
  show "1 * p = p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   310
  proof (rule up_eqI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   311
    fix n
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   312
    show "coeff (1 * p) n = coeff p n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   313
    proof (cases n)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   314
      case 0 then show ?thesis by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   315
    next
16052
880b0e786c1b tuned setsum rewrites
nipkow
parents: 15596
diff changeset
   316
      case Suc then show ?thesis by (simp del: setsum_atMost_Suc add: natsum_Suc2)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   317
    qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   318
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   319
  show "(p + q) * r = p * r + q * r"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   320
    by (rule up_eqI) simp
30968
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30012
diff changeset
   321
  show "\<And>q. p * q = q * p"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   322
  proof (rule up_eqI)
30968
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30012
diff changeset
   323
    fix q
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   324
    fix n 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   325
    {
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   326
      fix k
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   327
      fix a b :: "nat=>'a::ring"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   328
      have "k <= n ==> 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   329
        setsum (%i. a i * b (n-i)) {..k} =
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   330
        setsum (%i. a (k-i) * b (i+n-k)) {..k}"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   331
        (is "_ ==> ?eq k")
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   332
      proof (induct k)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   333
        case 0 show ?case by simp
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   334
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   335
        case (Suc k) then show ?case by (subst natsum_Suc2) simp
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   336
      qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   337
    }
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   338
    then show "coeff (p * q) n = coeff (q * p) n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   339
      by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   340
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   341
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   342
  show "p - q = p + (-q)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   343
    by (simp add: up_minus_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   344
  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   345
    by (simp add: up_inverse_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   346
  show "p / q = p * inverse q"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   347
    by (simp add: up_divide_def)
27540
dc38e79f5a1c separate class dvd for divisibility predicate
haftmann
parents: 26563
diff changeset
   348
qed
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   349
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   350
(* Further properties of monom *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   351
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   352
lemma monom_zero [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   353
  "monom 0 n = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   354
  by (simp add: monom_def up_zero_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   355
(* term order: application of coeff_mult goes wrong: rule not symmetric
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   356
lemma monom_mult_is_smult:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   357
  "monom (a::'a::ring) 0 * p = a *s p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   358
proof (rule up_eqI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   359
  fix k
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   360
  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   361
  proof (cases k)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   362
    case 0 then show ?thesis by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   363
  next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   364
    case Suc then show ?thesis by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   365
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   366
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   367
*)
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 25762
diff changeset
   368
ML {* Delsimprocs [ring_simproc] *}
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   369
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   370
lemma monom_mult_is_smult:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   371
  "monom (a::'a::ring) 0 * p = a *s p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   372
proof (rule up_eqI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   373
  fix k
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   374
  have "coeff (p * monom a 0) k = coeff (a *s p) k"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   375
  proof (cases k)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   376
    case 0 then show ?thesis by simp ring
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   377
  next
30012
a717c3dffe4f fixed spurious proof failure
haftmann
parents: 29667
diff changeset
   378
    case Suc then show ?thesis by simp (ring, simp)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   379
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   380
  then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   381
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   382
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 25762
diff changeset
   383
ML {* Addsimprocs [ring_simproc] *}
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   384
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   385
lemma monom_add [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   386
  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   387
by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   388
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   389
lemma monom_mult_smult:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   390
  "monom (a * b) n = a *s monom (b::'a::ring) n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   391
by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   392
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   393
lemma monom_uminus [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   394
  "monom (-a) n = - monom (a::'a::ring) n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   395
by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   396
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   397
lemma monom_one [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   398
  "monom 1 0 = 1"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   399
by (simp add: up_one_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   400
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   401
lemma monom_inj:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   402
  "(monom a n = monom b n) = (a = b)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   403
proof
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   404
  assume "monom a n = monom b n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   405
  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   406
  then show "a = b" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   407
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   408
  assume "a = b" then show "monom a n = monom b n" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   409
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   410
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   411
(* Properties of *s:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   412
   Polynomials form a module *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   413
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   414
lemma smult_l_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   415
  "(a + b::'a::ring) *s p = a *s p + b *s p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   416
by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   417
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   418
lemma smult_r_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   419
  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   420
by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   421
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   422
lemma smult_assoc1:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   423
  "(a * b::'a::ring) *s p = a *s (b *s p)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   424
by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   425
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   426
lemma smult_one [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   427
  "(1::'a::ring) *s p = p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   428
by (rule up_eqI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   429
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   430
(* Polynomials form an algebra *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   431
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 25762
diff changeset
   432
ML {* Delsimprocs [ring_simproc] *}
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   433
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   434
lemma smult_assoc2:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   435
  "(a *s p) * q = (a::'a::ring) *s (p * q)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   436
by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   437
(* Simproc fails. *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   438
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 25762
diff changeset
   439
ML {* Addsimprocs [ring_simproc] *}
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   440
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   441
(* the following can be derived from the above ones,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   442
   for generality reasons, it is therefore done *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   443
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   444
lemma smult_l_null [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   445
  "(0::'a::ring) *s p = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   446
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   447
  fix a
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   448
  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   449
  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   450
  also have "... = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   451
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   452
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   453
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   454
lemma smult_r_null [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   455
  "(a::'a::ring) *s 0 = 0";
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   456
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   457
  fix p
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   458
  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   459
  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   460
  also have "... = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   461
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   462
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   463
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   464
lemma smult_l_minus:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   465
  "(-a::'a::ring) *s p = - (a *s p)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   466
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   467
  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   468
  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   469
  also have "... = -(a *s p)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   470
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   471
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   472
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   473
lemma smult_r_minus:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   474
  "(a::'a::ring) *s (-p) = - (a *s p)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   475
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   476
  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   477
  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   478
  also have "... = -(a *s p)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   479
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   480
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   481
35849
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
   482
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   483
section {* The degree function *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   484
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   485
definition
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
   486
  deg :: "('a::zero) up => nat"
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35050
diff changeset
   487
  where "deg p = (LEAST n. bound n (coeff p))"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   488
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   489
lemma deg_aboveI:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   490
  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   491
by (unfold deg_def) (fast intro: Least_le)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   492
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   493
lemma deg_aboveD:
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22931
diff changeset
   494
  assumes "deg p < m" shows "coeff p m = 0"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   495
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   496
  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   497
  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22931
diff changeset
   498
  then show "coeff p m = 0" using `deg p < m` by (rule boundD)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   499
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   500
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   501
lemma deg_belowI:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   502
  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   503
(* logically, this is a slightly stronger version of deg_aboveD *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   504
proof (cases "n=0")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   505
  case True then show ?thesis by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   506
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   507
  case False then have "coeff p n ~= 0" by (rule prem)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   508
  then have "~ deg p < n" by (fast dest: deg_aboveD)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   509
  then show ?thesis by arith
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   510
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   511
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   512
lemma lcoeff_nonzero_deg:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   513
  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   514
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   515
  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   516
  proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   517
    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   518
      by arith (* make public?, why does proof not work with "1" *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   519
    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   520
      by (unfold deg_def) arith
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   521
    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   522
    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   523
      by (unfold bound_def) fast
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   524
    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 22931
diff changeset
   525
    then show ?thesis by (auto intro: that)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   526
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   527
  with deg_belowI have "deg p = m" by fastsimp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   528
  with m_coeff show ?thesis by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   529
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   530
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   531
lemma lcoeff_nonzero_nonzero:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   532
  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   533
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   534
  have "EX m. coeff p m ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   535
  proof (rule classical)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   536
    assume "~ ?thesis"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   537
    then have "p = 0" by (auto intro: up_eqI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   538
    with nonzero show ?thesis by contradiction
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   539
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   540
  then obtain m where coeff: "coeff p m ~= 0" ..
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   541
  then have "m <= deg p" by (rule deg_belowI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   542
  then have "m = 0" by (simp add: deg)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   543
  with coeff show ?thesis by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   544
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   545
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   546
lemma lcoeff_nonzero:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   547
  "p ~= 0 ==> coeff p (deg p) ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   548
proof (cases "deg p = 0")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   549
  case True
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   550
  assume "p ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   551
  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   552
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   553
  case False
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   554
  assume "p ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   555
  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   556
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   557
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   558
lemma deg_eqI:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   559
  "[| !!m. n < m ==> coeff p m = 0;
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   560
      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   561
by (fast intro: le_antisym deg_aboveI deg_belowI)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   562
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   563
(* Degree and polynomial operations *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   564
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   565
lemma deg_add [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   566
  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
32436
10cd49e0c067 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents: 31021
diff changeset
   567
by (rule deg_aboveI) (simp add: deg_aboveD)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   568
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   569
lemma deg_monom_ring:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   570
  "deg (monom a n::'a::ring up) <= n"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   571
by (rule deg_aboveI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   572
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   573
lemma deg_monom [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   574
  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   575
by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   576
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   577
lemma deg_const [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   578
  "deg (monom (a::'a::ring) 0) = 0"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   579
proof (rule le_antisym)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   580
  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   581
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   582
  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   583
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   584
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   585
lemma deg_zero [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   586
  "deg 0 = 0"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   587
proof (rule le_antisym)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   588
  show "deg 0 <= 0" by (rule deg_aboveI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   589
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   590
  show "0 <= deg 0" by (rule deg_belowI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   591
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   592
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   593
lemma deg_one [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   594
  "deg 1 = 0"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   595
proof (rule le_antisym)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   596
  show "deg 1 <= 0" by (rule deg_aboveI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   597
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   598
  show "0 <= deg 1" by (rule deg_belowI) simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   599
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   600
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   601
lemma uminus_monom:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   602
  "!!a::'a::ring. (-a = 0) = (a = 0)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   603
proof
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   604
  fix a::"'a::ring"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   605
  assume "a = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   606
  then show "-a = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   607
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   608
  fix a::"'a::ring"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   609
  assume "- a = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   610
  then have "-(- a) = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   611
  then show "a = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   612
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   613
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   614
lemma deg_uminus [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   615
  "deg (-p::('a::ring) up) = deg p"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   616
proof (rule le_antisym)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   617
  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   618
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   619
  show "deg p <= deg (- p)" 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   620
  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   621
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   622
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   623
lemma deg_smult_ring:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   624
  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   625
proof (cases "a = 0")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   626
qed (simp add: deg_aboveI deg_aboveD)+
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   627
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   628
lemma deg_smult [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   629
  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   630
proof (rule le_antisym)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   631
  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   632
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   633
  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   634
  proof (cases "a = 0")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   635
  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   636
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   637
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   638
lemma deg_mult_ring:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   639
  "deg (p * q::'a::ring up) <= deg p + deg q"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   640
proof (rule deg_aboveI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   641
  fix m
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   642
  assume boundm: "deg p + deg q < m"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   643
  {
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   644
    fix k i
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   645
    assume boundk: "deg p + deg q < k"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   646
    then have "coeff p i * coeff q (k - i) = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   647
    proof (cases "deg p < i")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   648
      case True then show ?thesis by (simp add: deg_aboveD)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   649
    next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   650
      case False with boundk have "deg q < k - i" by arith
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   651
      then show ?thesis by (simp add: deg_aboveD)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   652
    qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   653
  }
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   654
      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   655
         proofs. *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   656
  with boundm show "coeff (p * q) m = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   657
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   658
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   659
lemma deg_mult [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   660
  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
33657
a4179bf442d1 renamed lemmas "anti_sym" -> "antisym"
nipkow
parents: 32960
diff changeset
   661
proof (rule le_antisym)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   662
  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   663
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   664
  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   665
  assume nz: "p ~= 0" "q ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   666
  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   667
  show "deg p + deg q <= deg (p * q)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   668
  proof (rule deg_belowI, simp)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   669
    have "setsum ?s {.. deg p + deg q}
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 14590
diff changeset
   670
      = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   671
      by (simp only: ivl_disj_un_one)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   672
    also have "... = setsum ?s {deg p .. deg p + deg q}"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   673
      by (simp add: setsum_Un_disjoint ivl_disj_int_one
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   674
        setsum_0 deg_aboveD less_add_diff)
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 14590
diff changeset
   675
    also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   676
      by (simp only: ivl_disj_un_singleton)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   677
    also have "... = coeff p (deg p) * coeff q (deg q)" 
32456
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   678
      by (simp add: setsum_Un_disjoint setsum_0 deg_aboveD)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   679
    finally have "setsum ?s {.. deg p + deg q} 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   680
      = coeff p (deg p) * coeff q (deg q)" .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   681
    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   682
      by (simp add: integral_iff lcoeff_nonzero)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   683
    qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   684
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   685
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   686
lemma coeff_natsum:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   687
  "((coeff (setsum p A) k)::'a::ring) = 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   688
   setsum (%i. coeff (p i) k) A"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   689
proof (cases "finite A")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   690
  case True then show ?thesis by induct auto
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   691
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   692
  case False then show ?thesis by (simp add: setsum_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   693
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   694
(* Instance of a more general result!!! *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   695
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   696
(*
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   697
lemma coeff_natsum:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   698
  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   699
   setsum (%i. coeff (p i) k) {..n}"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   700
by (induct n) auto
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   701
*)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   702
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   703
lemma up_repr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   704
  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   705
proof (rule up_eqI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   706
  let ?s = "(%i. monom (coeff p i) i)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   707
  fix k
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   708
  show "coeff (setsum ?s {..deg p}) k = coeff p k"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   709
  proof (cases "k <= deg p")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   710
    case True
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   711
    hence "coeff (setsum ?s {..deg p}) k = 
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 14590
diff changeset
   712
          coeff (setsum ?s ({..k} Un {k<..deg p})) k"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   713
      by (simp only: ivl_disj_un_one)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   714
    also from True
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   715
    have "... = coeff (setsum ?s {..k}) k"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   716
      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   717
        setsum_0 coeff_natsum )
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   718
    also
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 14590
diff changeset
   719
    have "... = coeff (setsum ?s ({..<k} Un {k})) k"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   720
      by (simp only: ivl_disj_un_singleton)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   721
    also have "... = coeff p k"
32456
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   722
      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   723
    finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   724
  next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   725
    case False
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   726
    hence "coeff (setsum ?s {..deg p}) k = 
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 14590
diff changeset
   727
          coeff (setsum ?s ({..<deg p} Un {deg p})) k"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   728
      by (simp only: ivl_disj_un_singleton)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   729
    also from False have "... = coeff p k"
32456
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   730
      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   731
    finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   732
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   733
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   734
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   735
lemma up_repr_le:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   736
  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   737
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   738
  let ?s = "(%i. monom (coeff p i) i)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   739
  assume "deg p <= n"
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 14590
diff changeset
   740
  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   741
    by (simp only: ivl_disj_un_one)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   742
  also have "... = setsum ?s {..deg p}"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   743
    by (simp add: setsum_Un_disjoint ivl_disj_int_one
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   744
      setsum_0 deg_aboveD)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   745
  also have "... = p" by (rule up_repr)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   746
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   747
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   748
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   749
instance up :: ("domain") "domain"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   750
proof
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   751
  show "1 ~= (0::'a up)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   752
  proof (* notI is applied here *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   753
    assume "1 = (0::'a up)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   754
    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   755
    hence "1 = (0::'a)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   756
    with one_not_zero show "False" by contradiction
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   757
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   758
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   759
  fix p q :: "'a::domain up"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   760
  assume pq: "p * q = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   761
  show "p = 0 | q = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   762
  proof (rule classical)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   763
    assume c: "~ (p = 0 | q = 0)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   764
    then have "deg p + deg q = deg (p * q)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   765
    also from pq have "... = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   766
    finally have "deg p + deg q = 0" .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   767
    then have f1: "deg p = 0 & deg q = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   768
    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   769
      by (simp only: up_repr_le)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   770
    also have "... = monom (coeff p 0) 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   771
    finally have p: "p = monom (coeff p 0) 0" .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   772
    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   773
      by (simp only: up_repr_le)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   774
    also have "... = monom (coeff q 0) 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   775
    finally have q: "q = monom (coeff q 0) 0" .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   776
    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   777
    also from pq have "... = 0" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   778
    finally have "coeff p 0 * coeff q 0 = 0" .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   779
    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   780
    with p q show "p = 0 | q = 0" by fastsimp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   781
  qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   782
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   783
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   784
lemma monom_inj_zero:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   785
  "(monom a n = 0) = (a = 0)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   786
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   787
  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   788
  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   789
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   790
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   791
(* term order: makes this simpler!!!
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   792
lemma smult_integral:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   793
  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   794
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   795
*)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   796
lemma smult_integral:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   797
  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   798
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   799
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   800
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   801
(* Divisibility and degree *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   802
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   803
lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   804
  apply (unfold dvd_def)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   805
  apply (erule exE)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   806
  apply hypsubst
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   807
  apply (case_tac "p = 0")
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   808
   apply (case_tac [2] "k = 0")
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   809
    apply auto
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   810
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 20432
diff changeset
   811
14590
276ef51cedbf simplified ML code for setsubgoaler;
wenzelm
parents: 13936
diff changeset
   812
end