src/HOL/Algebra/poly/LongDiv.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 35849 b5522b51cb1e
child 42768 4db4a8b164c1
permissions -rw-r--r--
more antiquotations;
wenzelm@35849
     1
(*  Author: Clemens Ballarin, started 23 June 1999
wenzelm@35849
     2
wenzelm@35849
     3
Experimental theory: long division of polynomials.
paulson@7998
     4
*)
paulson@7998
     5
wenzelm@35849
     6
theory LongDiv
wenzelm@35849
     7
imports PolyHomo
wenzelm@35849
     8
begin
paulson@7998
     9
wenzelm@21423
    10
definition
wenzelm@21423
    11
  lcoeff :: "'a::ring up => 'a" where
wenzelm@21423
    12
  "lcoeff p = coeff p (deg p)"
paulson@7998
    13
wenzelm@21423
    14
definition
wenzelm@21423
    15
  eucl_size :: "'a::zero up => nat" where
wenzelm@21423
    16
  "eucl_size p = (if p = 0 then 0 else deg p + 1)"
obua@14723
    17
obua@14723
    18
lemma SUM_shrink_below_lemma:
obua@14723
    19
  "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) --> 
obua@14723
    20
  setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
obua@14723
    21
  apply (induct_tac d)
paulson@15481
    22
   apply (induct_tac m)
wenzelm@21423
    23
    apply simp
wenzelm@21423
    24
   apply force
haftmann@22384
    25
  apply (simp add: add_commute [of m]) 
wenzelm@21423
    26
  done
wenzelm@21423
    27
wenzelm@21423
    28
lemma SUM_extend_below: 
wenzelm@21423
    29
  "!! f::(nat=>'a::ring).  
wenzelm@21423
    30
     [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |]  
wenzelm@21423
    31
     ==> P (setsum f {..n})"
wenzelm@21423
    32
  by (simp add: SUM_shrink_below_lemma add_diff_inverse leD)
wenzelm@21423
    33
wenzelm@21423
    34
lemma up_repr2D: 
wenzelm@21423
    35
  "!! p::'a::ring up.  
wenzelm@21423
    36
   [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |]  
wenzelm@21423
    37
     ==> P p"
wenzelm@21423
    38
  by (simp add: up_repr_le)
wenzelm@21423
    39
wenzelm@21423
    40
wenzelm@21423
    41
(* Start of LongDiv *)
wenzelm@21423
    42
wenzelm@21423
    43
lemma deg_lcoeff_cancel: 
wenzelm@21423
    44
  "!!p::('a::ring up).  
wenzelm@21423
    45
     [| deg p <= deg r; deg q <= deg r;  
wenzelm@21423
    46
        coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==>  
wenzelm@21423
    47
     deg (p + q) < deg r"
paulson@24742
    48
  apply (rule le_less_trans [of _ "deg r - 1"])
wenzelm@21423
    49
   prefer 2
wenzelm@21423
    50
   apply arith
wenzelm@21423
    51
  apply (rule deg_aboveI)
wenzelm@21423
    52
  apply (case_tac "deg r = m")
wenzelm@21423
    53
   apply clarify
wenzelm@21423
    54
   apply simp
wenzelm@21423
    55
  (* case "deg q ~= m" *)
wenzelm@21423
    56
   apply (subgoal_tac "deg p < m & deg q < m")
wenzelm@21423
    57
    apply (simp (no_asm_simp) add: deg_aboveD)
wenzelm@21423
    58
  apply arith
wenzelm@21423
    59
  done
wenzelm@21423
    60
wenzelm@21423
    61
lemma deg_lcoeff_cancel2: 
wenzelm@21423
    62
  "!!p::('a::ring up).  
wenzelm@21423
    63
     [| deg p <= deg r; deg q <= deg r;  
wenzelm@21423
    64
        p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==>  
wenzelm@21423
    65
     deg (p + q) < deg r"
wenzelm@21423
    66
  apply (rule deg_lcoeff_cancel)
wenzelm@21423
    67
     apply assumption+
wenzelm@21423
    68
  apply (rule classical)
wenzelm@21423
    69
  apply clarify
wenzelm@21423
    70
  apply (erule notE)
wenzelm@21423
    71
  apply (rule_tac p = p in up_repr2D, assumption)
wenzelm@21423
    72
  apply (rule_tac p = q in up_repr2D, assumption)
wenzelm@21423
    73
  apply (rotate_tac -1)
wenzelm@21423
    74
  apply (simp add: smult_l_minus)
wenzelm@21423
    75
  done
wenzelm@21423
    76
wenzelm@21423
    77
lemma long_div_eucl_size: 
wenzelm@21423
    78
  "!!g::('a::ring up). g ~= 0 ==>  
wenzelm@21423
    79
     Ex (% (q, r, k).  
wenzelm@21423
    80
       (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))"
wenzelm@21423
    81
  apply (rule_tac P = "%f. Ex (% (q, r, k) . (lcoeff g) ^k *s f = q * g + r & (eucl_size r < eucl_size g))" in wf_induct)
wenzelm@21423
    82
  (* TO DO: replace by measure_induct *)
wenzelm@21423
    83
  apply (rule_tac f = eucl_size in wf_measure)
wenzelm@21423
    84
  apply (case_tac "eucl_size x < eucl_size g")
wenzelm@21423
    85
   apply (rule_tac x = "(0, x, 0)" in exI)
wenzelm@21423
    86
   apply (simp (no_asm_simp))
wenzelm@21423
    87
  (* case "eucl_size x >= eucl_size g" *)
wenzelm@21423
    88
  apply (drule_tac x = "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g" in spec)
wenzelm@21423
    89
  apply (erule impE)
wenzelm@21423
    90
   apply (simp (no_asm_use) add: inv_image_def measure_def lcoeff_def)
wenzelm@21423
    91
   apply (case_tac "x = 0")
wenzelm@21423
    92
    apply (rotate_tac -1)
wenzelm@21423
    93
    apply (simp add: eucl_size_def)
wenzelm@21423
    94
    (* case "x ~= 0 *)
wenzelm@21423
    95
    apply (rotate_tac -1)
wenzelm@21423
    96
   apply (simp add: eucl_size_def)
wenzelm@21423
    97
   apply (rule impI)
wenzelm@21423
    98
   apply (rule deg_lcoeff_cancel2)
wenzelm@21423
    99
  (* replace by linear arithmetic??? *)
wenzelm@21423
   100
      apply (rule_tac [2] le_trans)
wenzelm@21423
   101
       apply (rule_tac [2] deg_smult_ring)
wenzelm@21423
   102
      prefer 2
wenzelm@21423
   103
      apply simp
wenzelm@21423
   104
     apply (simp (no_asm))
wenzelm@21423
   105
     apply (rule le_trans)
wenzelm@21423
   106
      apply (rule deg_mult_ring)
wenzelm@21423
   107
     apply (rule le_trans)
wenzelm@21423
   108
(**)
wenzelm@21423
   109
      apply (rule add_le_mono)
wenzelm@21423
   110
       apply (rule le_refl)
wenzelm@21423
   111
    (* term order forces to use this instead of add_le_mono1 *)
wenzelm@21423
   112
      apply (rule deg_monom_ring)
wenzelm@21423
   113
     apply (simp (no_asm_simp))
wenzelm@21423
   114
    apply force
wenzelm@21423
   115
   apply (simp (no_asm))
wenzelm@21423
   116
(**)
wenzelm@21423
   117
   (* This change is probably caused by application of commutativity *)
wenzelm@21423
   118
   apply (rule_tac m = "deg g" and n = "deg x" in SUM_extend)
wenzelm@21423
   119
     apply (simp (no_asm))
wenzelm@21423
   120
    apply (simp (no_asm_simp))
wenzelm@21423
   121
    apply arith
wenzelm@21423
   122
   apply (rule_tac m = "deg g" and n = "deg g" in SUM_extend_below)
wenzelm@21423
   123
     apply (rule le_refl)
wenzelm@21423
   124
    apply (simp (no_asm_simp))
wenzelm@21423
   125
    apply arith
wenzelm@21423
   126
   apply (simp (no_asm))
wenzelm@21423
   127
(**)
wenzelm@21423
   128
(* end of subproof deg f1 < deg f *)
wenzelm@21423
   129
  apply (erule exE)
wenzelm@21423
   130
  apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI)
wenzelm@21423
   131
  apply clarify
wenzelm@21423
   132
  apply (drule sym)
wenzelm@26342
   133
  apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}]
wenzelm@21423
   134
    delsimprocs [ring_simproc]) 1 *})
wenzelm@26342
   135
  apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
wenzelm@39159
   136
  apply (tactic {* simp_tac (@{simpset} addsimps [@{thm minus_def}, @{thm smult_r_distr},
wenzelm@39159
   137
    @{thm smult_r_minus}, @{thm monom_mult_smult}, @{thm smult_assoc2}]
wenzelm@21423
   138
    delsimprocs [ring_simproc]) 1 *})
haftmann@30968
   139
  apply (simp add: smult_assoc1 [symmetric])
wenzelm@21423
   140
  done
wenzelm@21423
   141
wenzelm@27214
   142
ML {*
wenzelm@27214
   143
 bind_thm ("long_div_ring_aux",
wenzelm@27214
   144
    simplify (@{simpset} addsimps [@{thm eucl_size_def}]
wenzelm@27214
   145
    delsimprocs [ring_simproc]) (@{thm long_div_eucl_size}))
wenzelm@27214
   146
*}
wenzelm@21423
   147
wenzelm@21423
   148
lemma long_div_ring: 
wenzelm@21423
   149
  "!!g::('a::ring up). g ~= 0 ==>  
wenzelm@21423
   150
     Ex (% (q, r, k).  
wenzelm@21423
   151
       (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
wenzelm@27214
   152
  apply (frule_tac f = f in long_div_ring_aux)
wenzelm@26342
   153
  apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *})
wenzelm@21423
   154
  apply (case_tac "aa = 0")
wenzelm@21423
   155
   apply blast
wenzelm@21423
   156
  (* case "aa ~= 0 *)
wenzelm@21423
   157
  apply (rotate_tac -1)
wenzelm@21423
   158
  apply auto
wenzelm@21423
   159
  done
wenzelm@21423
   160
wenzelm@21423
   161
(* Next one fails *)
wenzelm@21423
   162
lemma long_div_unit: 
wenzelm@21423
   163
  "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==>  
wenzelm@21423
   164
     Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
wenzelm@21423
   165
  apply (frule_tac f = "f" in long_div_ring)
wenzelm@21423
   166
  apply (erule exE)
wenzelm@21423
   167
  apply (rule_tac x = "((% (q,r,k) . (inverse (lcoeff g ^k) *s q)) x, (% (q,r,k) . inverse (lcoeff g ^k) *s r) x) " in exI)
wenzelm@21423
   168
  apply clarify
wenzelm@21423
   169
  apply (rule conjI)
wenzelm@21423
   170
   apply (drule sym)
wenzelm@21423
   171
   apply (tactic {* asm_simp_tac
wenzelm@39159
   172
     (@{simpset} addsimps [@{thm smult_r_distr} RS sym, @{thm smult_assoc2}]
wenzelm@21423
   173
     delsimprocs [ring_simproc]) 1 *})
wenzelm@21423
   174
   apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
wenzelm@21423
   175
  (* degree property *)
wenzelm@21423
   176
   apply (erule disjE)
wenzelm@21423
   177
    apply (simp (no_asm_simp))
wenzelm@21423
   178
  apply (rule disjI2)
wenzelm@21423
   179
  apply (rule le_less_trans)
wenzelm@21423
   180
   apply (rule deg_smult_ring)
wenzelm@21423
   181
  apply (simp (no_asm_simp))
wenzelm@21423
   182
  done
wenzelm@21423
   183
wenzelm@21423
   184
lemma long_div_theorem: 
wenzelm@21423
   185
  "!!g::('a::field up). g ~= 0 ==>  
wenzelm@21423
   186
     Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
wenzelm@21423
   187
  apply (rule long_div_unit)
wenzelm@21423
   188
   apply assumption
wenzelm@21423
   189
  apply (simp (no_asm_simp) add: lcoeff_def lcoeff_nonzero field_ax)
wenzelm@21423
   190
  done
wenzelm@21423
   191
wenzelm@21423
   192
lemma uminus_zero: "- (0::'a::ring) = 0"
wenzelm@21423
   193
  by simp
wenzelm@21423
   194
wenzelm@21423
   195
lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b"
wenzelm@21423
   196
  apply (rule_tac s = "a - (a - b) " in trans)
wenzelm@26342
   197
   apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
wenzelm@21423
   198
   apply simp
wenzelm@21423
   199
  apply (simp (no_asm))
wenzelm@21423
   200
  done
wenzelm@21423
   201
wenzelm@21423
   202
lemma eq_imp_diff_zero: "!!a::'a::ring. a = b ==> a + (-b) = 0"
wenzelm@21423
   203
  by simp
wenzelm@21423
   204
wenzelm@21423
   205
lemma long_div_quo_unique: 
wenzelm@21423
   206
  "!!g::('a::field up). [| g ~= 0;  
wenzelm@21423
   207
     f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);  
wenzelm@21423
   208
     f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2"
wenzelm@21423
   209
  apply (subgoal_tac "(q1 - q2) * g = r2 - r1") (* 1 *)
wenzelm@21423
   210
   apply (erule_tac V = "f = ?x" in thin_rl)
wenzelm@21423
   211
  apply (erule_tac V = "f = ?x" in thin_rl)
wenzelm@21423
   212
  apply (rule diff_zero_imp_eq)
wenzelm@21423
   213
  apply (rule classical)
wenzelm@21423
   214
  apply (erule disjE)
wenzelm@21423
   215
  (* r1 = 0 *)
wenzelm@21423
   216
    apply (erule disjE)
wenzelm@21423
   217
  (* r2 = 0 *)
wenzelm@26342
   218
     apply (tactic {* asm_full_simp_tac (@{simpset}
wenzelm@39159
   219
       addsimps [@{thm integral_iff}, @{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}]
wenzelm@21423
   220
       delsimprocs [ring_simproc]) 1 *})
wenzelm@21423
   221
  (* r2 ~= 0 *)
wenzelm@21423
   222
    apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
wenzelm@26342
   223
    apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
wenzelm@39159
   224
      [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *})
wenzelm@21423
   225
  (* r1 ~=0 *)
wenzelm@21423
   226
   apply (erule disjE)
wenzelm@21423
   227
  (* r2 = 0 *)
wenzelm@21423
   228
    apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
wenzelm@26342
   229
    apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
wenzelm@39159
   230
      [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *})
wenzelm@21423
   231
  (* r2 ~= 0 *)
wenzelm@21423
   232
   apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
wenzelm@39159
   233
   apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [@{thm minus_def}]
wenzelm@21423
   234
     delsimprocs [ring_simproc]) 1 *})
wenzelm@21423
   235
   apply (drule order_eq_refl [THEN add_leD2])
wenzelm@21423
   236
   apply (drule leD)
wenzelm@21423
   237
   apply (erule notE, rule deg_add [THEN le_less_trans])
wenzelm@21423
   238
   apply (simp (no_asm_simp))
wenzelm@21423
   239
  (* proof of 1 *)
wenzelm@21423
   240
   apply (rule diff_zero_imp_eq)
wenzelm@21423
   241
  apply hypsubst
wenzelm@21423
   242
  apply (drule_tac a = "?x+?y" in eq_imp_diff_zero)
wenzelm@21423
   243
  apply simp
wenzelm@21423
   244
  done
wenzelm@21423
   245
wenzelm@21423
   246
lemma long_div_rem_unique: 
wenzelm@21423
   247
  "!!g::('a::field up). [| g ~= 0;  
wenzelm@21423
   248
     f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);  
wenzelm@21423
   249
     f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"
wenzelm@21423
   250
  apply (subgoal_tac "q1 = q2")
paulson@24742
   251
   apply (metis a_comm a_lcancel m_comm)
paulson@24742
   252
  apply (metis a_comm l_zero long_div_quo_unique m_comm conc)
obua@14723
   253
  done
paulson@7998
   254
paulson@7998
   255
end