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