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