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
```