src/HOL/Algebra/poly/PolyHomo.thy
author haftmann
Wed Jan 02 15:14:02 2008 +0100 (2008-01-02)
changeset 25762 c03e9d04b3e4
parent 21423 6cdd0589aa73
child 35849 b5522b51cb1e
permissions -rw-r--r--
splitted class uminus from class minus
paulson@7998
     1
(*
paulson@7998
     2
    Universal property and evaluation homomorphism of univariate polynomials
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 15 April 1997
paulson@7998
     5
*)
paulson@7998
     6
wenzelm@17479
     7
theory PolyHomo imports UnivPoly2 begin
paulson@7998
     8
wenzelm@21423
     9
definition
wenzelm@21423
    10
  EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
wenzelm@21423
    11
  "EVAL2 phi a p = setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
wenzelm@21423
    12
wenzelm@21423
    13
definition
wenzelm@21423
    14
  EVAL :: "['a::ring, 'a up] => 'a" where
wenzelm@21423
    15
  "EVAL = EVAL2 (%x. x)"
wenzelm@21423
    16
wenzelm@21423
    17
lemma SUM_shrink_lemma:
wenzelm@21423
    18
  "!! f::(nat=>'a::ring).
wenzelm@21423
    19
     m <= n & (ALL i. m < i & i <= n --> f i = 0) -->
wenzelm@21423
    20
     setsum f {..m} = setsum f {..n}"
wenzelm@21423
    21
  apply (induct_tac n)
wenzelm@21423
    22
  (* Base case *)
wenzelm@21423
    23
   apply (simp (no_asm))
wenzelm@21423
    24
  (* Induction step *)
wenzelm@21423
    25
  apply (case_tac "m <= n")
wenzelm@21423
    26
   apply auto
wenzelm@21423
    27
  apply (subgoal_tac "m = Suc n")
wenzelm@21423
    28
   apply (simp (no_asm_simp))
wenzelm@21423
    29
  apply arith
wenzelm@21423
    30
  done
wenzelm@21423
    31
wenzelm@21423
    32
lemma SUM_shrink:
wenzelm@21423
    33
  "!! f::(nat=>'a::ring).
wenzelm@21423
    34
     [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |]
wenzelm@21423
    35
   ==> P (setsum f {..m})"
wenzelm@21423
    36
  apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
wenzelm@21423
    37
  apply simp
wenzelm@21423
    38
  done
wenzelm@21423
    39
wenzelm@21423
    40
lemma SUM_extend:
wenzelm@21423
    41
  "!! f::(nat=>'a::ring).
wenzelm@21423
    42
     [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |]
wenzelm@21423
    43
     ==> P (setsum f {..n})"
wenzelm@21423
    44
  apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
wenzelm@21423
    45
  apply simp
wenzelm@21423
    46
  done
wenzelm@21423
    47
wenzelm@21423
    48
lemma DiagSum_lemma:
wenzelm@21423
    49
  "!!f::nat=>'a::ring. j <= n + m -->
wenzelm@21423
    50
     setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} =
wenzelm@21423
    51
     setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"
wenzelm@21423
    52
  apply (induct_tac j)
wenzelm@21423
    53
  (* Base case *)
wenzelm@21423
    54
   apply (simp (no_asm))
wenzelm@21423
    55
  (* Induction step *)
wenzelm@21423
    56
  apply (simp (no_asm) add: Suc_diff_le natsum_add)
wenzelm@21423
    57
  apply (simp (no_asm_simp))
wenzelm@21423
    58
  done
wenzelm@21423
    59
wenzelm@21423
    60
lemma DiagSum:
wenzelm@21423
    61
  "!!f::nat=>'a::ring.
wenzelm@21423
    62
     setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} =
wenzelm@21423
    63
     setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"
wenzelm@21423
    64
  apply (rule DiagSum_lemma [THEN mp])
wenzelm@21423
    65
  apply (rule le_refl)
wenzelm@21423
    66
  done
wenzelm@21423
    67
wenzelm@21423
    68
lemma CauchySum:
wenzelm@21423
    69
  "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==>
wenzelm@21423
    70
     setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} =
wenzelm@21423
    71
     setsum f {..n} * setsum g {..m}"
wenzelm@21423
    72
  apply (simp (no_asm) add: natsum_ldistr DiagSum)
wenzelm@21423
    73
  (* SUM_rdistr must be applied after SUM_ldistr ! *)
wenzelm@21423
    74
  apply (simp (no_asm) add: natsum_rdistr)
wenzelm@21423
    75
  apply (rule_tac m = n and n = "n + m" in SUM_extend)
wenzelm@21423
    76
  apply (rule le_add1)
wenzelm@21423
    77
   apply force
wenzelm@21423
    78
  apply (rule natsum_cong)
wenzelm@21423
    79
   apply (rule refl)
wenzelm@21423
    80
  apply (rule_tac m = m and n = "n +m - i" in SUM_shrink)
wenzelm@21423
    81
    apply (simp (no_asm_simp) add: le_add_diff)
wenzelm@21423
    82
   apply auto
wenzelm@21423
    83
  done
wenzelm@21423
    84
wenzelm@21423
    85
(* Evaluation homomorphism *)
paulson@7998
    86
wenzelm@21423
    87
lemma EVAL2_homo:
wenzelm@21423
    88
    "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"
wenzelm@21423
    89
  apply (rule homoI)
wenzelm@21423
    90
    apply (unfold EVAL2_def)
wenzelm@21423
    91
  (* + commutes *)
wenzelm@21423
    92
  (* degree estimations:
wenzelm@21423
    93
    bound of all sums can be extended to max (deg aa) (deg b) *)
wenzelm@21423
    94
    apply (rule_tac m = "deg (aa + b) " and n = "max (deg aa) (deg b)" in SUM_shrink)
wenzelm@21423
    95
      apply (rule deg_add)
wenzelm@21423
    96
     apply (simp (no_asm_simp) del: coeff_add add: deg_aboveD)
wenzelm@21423
    97
    apply (rule_tac m = "deg aa" and n = "max (deg aa) (deg b)" in SUM_shrink)
wenzelm@21423
    98
     apply (rule le_maxI1)
wenzelm@21423
    99
    apply (simp (no_asm_simp) add: deg_aboveD)
wenzelm@21423
   100
   apply (rule_tac m = "deg b" and n = "max (deg aa) (deg b) " in SUM_shrink)
wenzelm@21423
   101
     apply (rule le_maxI2)
wenzelm@21423
   102
    apply (simp (no_asm_simp) add: deg_aboveD)
wenzelm@21423
   103
  (* actual homom property + *)
wenzelm@21423
   104
    apply (simp (no_asm_simp) add: l_distr natsum_add)
wenzelm@21423
   105
wenzelm@21423
   106
  (* * commutes *)
wenzelm@21423
   107
   apply (rule_tac m = "deg (aa * b) " and n = "deg aa + deg b" in SUM_shrink)
wenzelm@21423
   108
    apply (rule deg_mult_ring)
wenzelm@21423
   109
    apply (simp (no_asm_simp) del: coeff_mult add: deg_aboveD)
wenzelm@21423
   110
   apply (rule trans)
wenzelm@21423
   111
    apply (rule_tac [2] CauchySum)
wenzelm@21423
   112
     prefer 2
wenzelm@21423
   113
     apply (simp add: boundI deg_aboveD)
wenzelm@21423
   114
    prefer 2
wenzelm@21423
   115
    apply (simp add: boundI deg_aboveD)
wenzelm@21423
   116
  (* getting a^i and a^(k-i) together is difficult, so we do it manually *)
wenzelm@21423
   117
  apply (rule_tac s = "setsum (%k. setsum (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * (a ^ i * a ^ (k - i)))) {..k}) {..deg aa + deg b}" in trans)
wenzelm@21423
   118
    apply (simp (no_asm_simp) add: power_mult leD [THEN add_diff_inverse] natsum_ldistr)
wenzelm@21423
   119
   apply (simp (no_asm))
wenzelm@21423
   120
  (* 1 commutes *)
wenzelm@21423
   121
  apply (simp (no_asm_simp))
wenzelm@21423
   122
  done
wenzelm@21423
   123
wenzelm@21423
   124
lemma EVAL2_const:
wenzelm@21423
   125
    "!!phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"
wenzelm@21423
   126
  by (simp add: EVAL2_def)
wenzelm@21423
   127
wenzelm@21423
   128
lemma EVAL2_monom1:
wenzelm@21423
   129
    "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"
wenzelm@21423
   130
  by (simp add: EVAL2_def)
wenzelm@21423
   131
  (* Must be able to distinguish 0 from 1, hence 'a::domain *)
wenzelm@21423
   132
wenzelm@21423
   133
lemma EVAL2_monom:
wenzelm@21423
   134
  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"
wenzelm@21423
   135
  apply (unfold EVAL2_def)
wenzelm@21423
   136
  apply (simp (no_asm))
wenzelm@21423
   137
  apply (case_tac n)
wenzelm@21423
   138
   apply auto
wenzelm@21423
   139
  done
wenzelm@21423
   140
wenzelm@21423
   141
lemma EVAL2_smult:
wenzelm@21423
   142
  "!!phi::'a::ring=>'b::ring.
wenzelm@21423
   143
     homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"
wenzelm@21423
   144
  by (simp (no_asm_simp) add: monom_mult_is_smult [symmetric] EVAL2_homo EVAL2_const)
wenzelm@21423
   145
wenzelm@21423
   146
lemma monom_decomp: "monom (a::'a::ring) n = monom a 0 * monom 1 n"
wenzelm@21423
   147
  apply (simp (no_asm) add: monom_mult_is_smult)
wenzelm@21423
   148
  apply (rule up_eqI)
wenzelm@21423
   149
  apply (simp (no_asm))
wenzelm@21423
   150
  done
wenzelm@21423
   151
wenzelm@21423
   152
lemma EVAL2_monom_n:
wenzelm@21423
   153
  "!! phi::'a::domain=>'b::ring.
wenzelm@21423
   154
     homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"
wenzelm@21423
   155
  apply (subst monom_decomp)
wenzelm@21423
   156
  apply (simp (no_asm_simp) add: EVAL2_homo EVAL2_const EVAL2_monom)
wenzelm@21423
   157
  done
wenzelm@21423
   158
wenzelm@21423
   159
lemma EVAL_homo: "!!a::'a::ring. homo (EVAL a)"
wenzelm@21423
   160
  by (simp add: EVAL_def EVAL2_homo)
wenzelm@21423
   161
wenzelm@21423
   162
lemma EVAL_const: "!!a::'a::ring. EVAL a (monom b 0) = b"
wenzelm@21423
   163
  by (simp add: EVAL_def EVAL2_const)
wenzelm@21423
   164
wenzelm@21423
   165
lemma EVAL_monom: "!!a::'a::domain. EVAL a (monom 1 n) = a ^ n"
wenzelm@21423
   166
  by (simp add: EVAL_def EVAL2_monom)
wenzelm@21423
   167
wenzelm@21423
   168
lemma EVAL_smult: "!!a::'a::ring. EVAL a (b *s p) = b * EVAL a p"
wenzelm@21423
   169
  by (simp add: EVAL_def EVAL2_smult)
wenzelm@21423
   170
wenzelm@21423
   171
lemma EVAL_monom_n: "!!a::'a::domain. EVAL a (monom b n) = b * a ^ n"
wenzelm@21423
   172
  by (simp add: EVAL_def EVAL2_monom_n)
wenzelm@21423
   173
wenzelm@21423
   174
wenzelm@21423
   175
(* Examples *)
wenzelm@21423
   176
wenzelm@21423
   177
lemma "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"
wenzelm@21423
   178
  by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n)
wenzelm@21423
   179
wenzelm@21423
   180
lemma
wenzelm@21423
   181
  "EVAL (y::'a::domain)
wenzelm@21423
   182
    (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
wenzelm@21423
   183
   x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
haftmann@25762
   184
  by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
paulson@7998
   185
paulson@7998
   186
end