src/HOL/Decision_Procs/Polynomial_List.thy
 author chaieb Sun Oct 25 08:57:36 2009 +0100 (2009-10-25) changeset 33153 92080294beb8 child 33268 02de0317f66f permissions -rw-r--r--
A theory of polynomials based on lists
 chaieb@33153 ` 1` ```(* Title: HOL/Decision_Procs/Polynomial_List.thy ``` chaieb@33153 ` 2` ``` Author: Amine Chaieb ``` chaieb@33153 ` 3` ```*) ``` chaieb@33153 ` 4` chaieb@33153 ` 5` ```header{*Univariate Polynomials as Lists *} ``` chaieb@33153 ` 6` chaieb@33153 ` 7` ```theory Polynomial_List ``` chaieb@33153 ` 8` ```imports Main ``` chaieb@33153 ` 9` ```begin ``` chaieb@33153 ` 10` chaieb@33153 ` 11` ```text{* Application of polynomial as a real function. *} ``` chaieb@33153 ` 12` chaieb@33153 ` 13` ```consts poly :: "'a list => 'a => ('a::{comm_ring})" ``` chaieb@33153 ` 14` ```primrec ``` chaieb@33153 ` 15` ``` poly_Nil: "poly [] x = 0" ``` chaieb@33153 ` 16` ``` poly_Cons: "poly (h#t) x = h + x * poly t x" ``` chaieb@33153 ` 17` chaieb@33153 ` 18` chaieb@33153 ` 19` ```subsection{*Arithmetic Operations on Polynomials*} ``` chaieb@33153 ` 20` chaieb@33153 ` 21` ```text{*addition*} ``` chaieb@33153 ` 22` ```consts padd :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "+++" 65) ``` chaieb@33153 ` 23` ```primrec ``` chaieb@33153 ` 24` ``` padd_Nil: "[] +++ l2 = l2" ``` chaieb@33153 ` 25` ``` padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t ``` chaieb@33153 ` 26` ``` else (h + hd l2)#(t +++ tl l2))" ``` chaieb@33153 ` 27` chaieb@33153 ` 28` ```text{*Multiplication by a constant*} ``` chaieb@33153 ` 29` ```consts cmult :: "['a :: comm_ring_1, 'a list] => 'a list" (infixl "%*" 70) ``` chaieb@33153 ` 30` ```primrec ``` chaieb@33153 ` 31` ``` cmult_Nil: "c %* [] = []" ``` chaieb@33153 ` 32` ``` cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)" ``` chaieb@33153 ` 33` chaieb@33153 ` 34` ```text{*Multiplication by a polynomial*} ``` chaieb@33153 ` 35` ```consts pmult :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "***" 70) ``` chaieb@33153 ` 36` ```primrec ``` chaieb@33153 ` 37` ``` pmult_Nil: "[] *** l2 = []" ``` chaieb@33153 ` 38` ``` pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2 ``` chaieb@33153 ` 39` ``` else (h %* l2) +++ ((0) # (t *** l2)))" ``` chaieb@33153 ` 40` chaieb@33153 ` 41` ```text{*Repeated multiplication by a polynomial*} ``` chaieb@33153 ` 42` ```consts mulexp :: "[nat, 'a list, 'a list] => ('a ::comm_ring_1) list" ``` chaieb@33153 ` 43` ```primrec ``` chaieb@33153 ` 44` ``` mulexp_zero: "mulexp 0 p q = q" ``` chaieb@33153 ` 45` ``` mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q" ``` chaieb@33153 ` 46` chaieb@33153 ` 47` ```text{*Exponential*} ``` chaieb@33153 ` 48` ```consts pexp :: "['a list, nat] => ('a::comm_ring_1) list" (infixl "%^" 80) ``` chaieb@33153 ` 49` ```primrec ``` chaieb@33153 ` 50` ``` pexp_0: "p %^ 0 = [1]" ``` chaieb@33153 ` 51` ``` pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)" ``` chaieb@33153 ` 52` chaieb@33153 ` 53` ```text{*Quotient related value of dividing a polynomial by x + a*} ``` chaieb@33153 ` 54` ```(* Useful for divisor properties in inductive proofs *) ``` chaieb@33153 ` 55` ```consts "pquot" :: "['a list, 'a::field] => 'a list" ``` chaieb@33153 ` 56` ```primrec ``` chaieb@33153 ` 57` ``` pquot_Nil: "pquot [] a= []" ``` chaieb@33153 ` 58` ``` pquot_Cons: "pquot (h#t) a = (if t = [] then [h] ``` chaieb@33153 ` 59` ``` else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))" ``` chaieb@33153 ` 60` chaieb@33153 ` 61` chaieb@33153 ` 62` ```text{*normalization of polynomials (remove extra 0 coeff)*} ``` chaieb@33153 ` 63` ```consts pnormalize :: "('a::comm_ring_1) list => 'a list" ``` chaieb@33153 ` 64` ```primrec ``` chaieb@33153 ` 65` ``` pnormalize_Nil: "pnormalize [] = []" ``` chaieb@33153 ` 66` ``` pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = []) ``` chaieb@33153 ` 67` ``` then (if (h = 0) then [] else [h]) ``` chaieb@33153 ` 68` ``` else (h#(pnormalize p)))" ``` chaieb@33153 ` 69` chaieb@33153 ` 70` ```definition "pnormal p = ((pnormalize p = p) \ p \ [])" ``` chaieb@33153 ` 71` ```definition "nonconstant p = (pnormal p \ (\x. p \ [x]))" ``` chaieb@33153 ` 72` ```text{*Other definitions*} ``` chaieb@33153 ` 73` chaieb@33153 ` 74` ```definition ``` chaieb@33153 ` 75` ``` poly_minus :: "'a list => ('a :: comm_ring_1) list" ("-- _" [80] 80) where ``` chaieb@33153 ` 76` ``` "-- p = (- 1) %* p" ``` chaieb@33153 ` 77` chaieb@33153 ` 78` ```definition ``` chaieb@33153 ` 79` ``` divides :: "[('a::comm_ring_1) list, 'a list] => bool" (infixl "divides" 70) where ``` chaieb@33153 ` 80` ``` "p1 divides p2 = (\q. poly p2 = poly(p1 *** q))" ``` chaieb@33153 ` 81` chaieb@33153 ` 82` ```definition ``` chaieb@33153 ` 83` ``` order :: "('a::comm_ring_1) => 'a list => nat" where ``` chaieb@33153 ` 84` ``` --{*order of a polynomial*} ``` chaieb@33153 ` 85` ``` "order a p = (SOME n. ([-a, 1] %^ n) divides p & ``` chaieb@33153 ` 86` ``` ~ (([-a, 1] %^ (Suc n)) divides p))" ``` chaieb@33153 ` 87` chaieb@33153 ` 88` ```definition ``` chaieb@33153 ` 89` ``` degree :: "('a::comm_ring_1) list => nat" where ``` chaieb@33153 ` 90` ``` --{*degree of a polynomial*} ``` chaieb@33153 ` 91` ``` "degree p = length (pnormalize p) - 1" ``` chaieb@33153 ` 92` chaieb@33153 ` 93` ```definition ``` chaieb@33153 ` 94` ``` rsquarefree :: "('a::comm_ring_1) list => bool" where ``` chaieb@33153 ` 95` ``` --{*squarefree polynomials --- NB with respect to real roots only.*} ``` chaieb@33153 ` 96` ``` "rsquarefree p = (poly p \ poly [] & ``` chaieb@33153 ` 97` ``` (\a. (order a p = 0) | (order a p = 1)))" ``` chaieb@33153 ` 98` chaieb@33153 ` 99` ```lemma padd_Nil2: "p +++ [] = p" ``` chaieb@33153 ` 100` ```by (induct p) auto ``` chaieb@33153 ` 101` ```declare padd_Nil2 [simp] ``` chaieb@33153 ` 102` chaieb@33153 ` 103` ```lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)" ``` chaieb@33153 ` 104` ```by auto ``` chaieb@33153 ` 105` chaieb@33153 ` 106` ```lemma pminus_Nil: "-- [] = []" ``` chaieb@33153 ` 107` ```by (simp add: poly_minus_def) ``` chaieb@33153 ` 108` ```declare pminus_Nil [simp] ``` chaieb@33153 ` 109` chaieb@33153 ` 110` ```lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" ``` chaieb@33153 ` 111` ```by simp ``` chaieb@33153 ` 112` chaieb@33153 ` 113` ```lemma poly_ident_mult: "1 %* t = t" ``` chaieb@33153 ` 114` ```by (induct "t", auto) ``` chaieb@33153 ` 115` ```declare poly_ident_mult [simp] ``` chaieb@33153 ` 116` chaieb@33153 ` 117` ```lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)" ``` chaieb@33153 ` 118` ```by simp ``` chaieb@33153 ` 119` ```declare poly_simple_add_Cons [simp] ``` chaieb@33153 ` 120` chaieb@33153 ` 121` ```text{*Handy general properties*} ``` chaieb@33153 ` 122` chaieb@33153 ` 123` ```lemma padd_commut: "b +++ a = a +++ b" ``` chaieb@33153 ` 124` ```apply (subgoal_tac "\a. b +++ a = a +++ b") ``` chaieb@33153 ` 125` ```apply (induct_tac [2] "b", auto) ``` chaieb@33153 ` 126` ```apply (rule padd_Cons [THEN ssubst]) ``` chaieb@33153 ` 127` ```apply (case_tac "aa", auto) ``` chaieb@33153 ` 128` ```done ``` chaieb@33153 ` 129` chaieb@33153 ` 130` ```lemma padd_assoc [rule_format]: "\b c. (a +++ b) +++ c = a +++ (b +++ c)" ``` chaieb@33153 ` 131` ```apply (induct "a", simp, clarify) ``` chaieb@33153 ` 132` ```apply (case_tac b, simp_all) ``` chaieb@33153 ` 133` ```done ``` chaieb@33153 ` 134` chaieb@33153 ` 135` ```lemma poly_cmult_distr [rule_format]: ``` chaieb@33153 ` 136` ``` "\q. a %* ( p +++ q) = (a %* p +++ a %* q)" ``` chaieb@33153 ` 137` ```apply (induct "p", simp, clarify) ``` chaieb@33153 ` 138` ```apply (case_tac "q") ``` chaieb@33153 ` 139` ```apply (simp_all add: right_distrib) ``` chaieb@33153 ` 140` ```done ``` chaieb@33153 ` 141` chaieb@33153 ` 142` ```lemma pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)" ``` chaieb@33153 ` 143` ```apply (induct "t", simp) ``` chaieb@33153 ` 144` ```by (auto simp add: mult_zero_left poly_ident_mult padd_commut) ``` chaieb@33153 ` 145` chaieb@33153 ` 146` chaieb@33153 ` 147` ```text{*properties of evaluation of polynomials.*} ``` chaieb@33153 ` 148` chaieb@33153 ` 149` ```lemma poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x" ``` chaieb@33153 ` 150` ```apply (subgoal_tac "\p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x") ``` chaieb@33153 ` 151` ```apply (induct_tac [2] "p1", auto) ``` chaieb@33153 ` 152` ```apply (case_tac "p2") ``` chaieb@33153 ` 153` ```apply (auto simp add: right_distrib) ``` chaieb@33153 ` 154` ```done ``` chaieb@33153 ` 155` chaieb@33153 ` 156` ```lemma poly_cmult: "poly (c %* p) x = c * poly p x" ``` chaieb@33153 ` 157` ```apply (induct "p") ``` chaieb@33153 ` 158` ```apply (case_tac [2] "x=0") ``` chaieb@33153 ` 159` ```apply (auto simp add: right_distrib mult_ac) ``` chaieb@33153 ` 160` ```done ``` chaieb@33153 ` 161` chaieb@33153 ` 162` ```lemma poly_minus: "poly (-- p) x = - (poly p x)" ``` chaieb@33153 ` 163` ```apply (simp add: poly_minus_def) ``` chaieb@33153 ` 164` ```apply (auto simp add: poly_cmult) ``` chaieb@33153 ` 165` ```done ``` chaieb@33153 ` 166` chaieb@33153 ` 167` ```lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x" ``` chaieb@33153 ` 168` ```apply (subgoal_tac "\p2. poly (p1 *** p2) x = poly p1 x * poly p2 x") ``` chaieb@33153 ` 169` ```apply (simp (no_asm_simp)) ``` chaieb@33153 ` 170` ```apply (induct "p1") ``` chaieb@33153 ` 171` ```apply (auto simp add: poly_cmult) ``` chaieb@33153 ` 172` ```apply (case_tac p1) ``` chaieb@33153 ` 173` ```apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac) ``` chaieb@33153 ` 174` ```done ``` chaieb@33153 ` 175` chaieb@33153 ` 176` ```lemma poly_exp: "poly (p %^ n) (x::'a::comm_ring_1) = (poly p x) ^ n" ``` chaieb@33153 ` 177` ```apply (induct "n") ``` chaieb@33153 ` 178` ```apply (auto simp add: poly_cmult poly_mult power_Suc) ``` chaieb@33153 ` 179` ```done ``` chaieb@33153 ` 180` chaieb@33153 ` 181` ```text{*More Polynomial Evaluation Lemmas*} ``` chaieb@33153 ` 182` chaieb@33153 ` 183` ```lemma poly_add_rzero: "poly (a +++ []) x = poly a x" ``` chaieb@33153 ` 184` ```by simp ``` chaieb@33153 ` 185` ```declare poly_add_rzero [simp] ``` chaieb@33153 ` 186` chaieb@33153 ` 187` ```lemma poly_mult_assoc: "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x" ``` chaieb@33153 ` 188` ``` by (simp add: poly_mult mult_assoc) ``` chaieb@33153 ` 189` chaieb@33153 ` 190` ```lemma poly_mult_Nil2: "poly (p *** []) x = 0" ``` chaieb@33153 ` 191` ```by (induct "p", auto) ``` chaieb@33153 ` 192` ```declare poly_mult_Nil2 [simp] ``` chaieb@33153 ` 193` chaieb@33153 ` 194` ```lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x" ``` chaieb@33153 ` 195` ```apply (induct "n") ``` chaieb@33153 ` 196` ```apply (auto simp add: poly_mult mult_assoc) ``` chaieb@33153 ` 197` ```done ``` chaieb@33153 ` 198` chaieb@33153 ` 199` ```subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides ``` chaieb@33153 ` 200` ``` @{term "p(x)"} *} ``` chaieb@33153 ` 201` chaieb@33153 ` 202` ```lemma lemma_poly_linear_rem: "\h. \q r. h#t = [r] +++ [-a, 1] *** q" ``` chaieb@33153 ` 203` ```apply (induct "t", safe) ``` chaieb@33153 ` 204` ```apply (rule_tac x = "[]" in exI) ``` chaieb@33153 ` 205` ```apply (rule_tac x = h in exI, simp) ``` chaieb@33153 ` 206` ```apply (drule_tac x = aa in spec, safe) ``` chaieb@33153 ` 207` ```apply (rule_tac x = "r#q" in exI) ``` chaieb@33153 ` 208` ```apply (rule_tac x = "a*r + h" in exI) ``` chaieb@33153 ` 209` ```apply (case_tac "q", auto) ``` chaieb@33153 ` 210` ```done ``` chaieb@33153 ` 211` chaieb@33153 ` 212` ```lemma poly_linear_rem: "\q r. h#t = [r] +++ [-a, 1] *** q" ``` chaieb@33153 ` 213` ```by (cut_tac t = t and a = a in lemma_poly_linear_rem, auto) ``` chaieb@33153 ` 214` chaieb@33153 ` 215` chaieb@33153 ` 216` ```lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\q. p = [-a, 1] *** q))" ``` chaieb@33153 ` 217` ```apply (auto simp add: poly_add poly_cmult right_distrib) ``` chaieb@33153 ` 218` ```apply (case_tac "p", simp) ``` chaieb@33153 ` 219` ```apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe) ``` chaieb@33153 ` 220` ```apply (case_tac "q", auto) ``` chaieb@33153 ` 221` ```apply (drule_tac x = "[]" in spec, simp) ``` chaieb@33153 ` 222` ```apply (auto simp add: poly_add poly_cmult add_assoc) ``` chaieb@33153 ` 223` ```apply (drule_tac x = "aa#lista" in spec, auto) ``` chaieb@33153 ` 224` ```done ``` chaieb@33153 ` 225` chaieb@33153 ` 226` ```lemma lemma_poly_length_mult: "\h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)" ``` chaieb@33153 ` 227` ```by (induct "p", auto) ``` chaieb@33153 ` 228` ```declare lemma_poly_length_mult [simp] ``` chaieb@33153 ` 229` chaieb@33153 ` 230` ```lemma lemma_poly_length_mult2: "\h k. length (k %* p +++ (h # p)) = Suc (length p)" ``` chaieb@33153 ` 231` ```by (induct "p", auto) ``` chaieb@33153 ` 232` ```declare lemma_poly_length_mult2 [simp] ``` chaieb@33153 ` 233` chaieb@33153 ` 234` ```lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)" ``` chaieb@33153 ` 235` ```by auto ``` chaieb@33153 ` 236` ```declare poly_length_mult [simp] ``` chaieb@33153 ` 237` chaieb@33153 ` 238` chaieb@33153 ` 239` ```subsection{*Polynomial length*} ``` chaieb@33153 ` 240` chaieb@33153 ` 241` ```lemma poly_cmult_length: "length (a %* p) = length p" ``` chaieb@33153 ` 242` ```by (induct "p", auto) ``` chaieb@33153 ` 243` ```declare poly_cmult_length [simp] ``` chaieb@33153 ` 244` chaieb@33153 ` 245` ```lemma poly_add_length [rule_format]: ``` chaieb@33153 ` 246` ``` "\p2. length (p1 +++ p2) = ``` chaieb@33153 ` 247` ``` (if (length p1 < length p2) then length p2 else length p1)" ``` chaieb@33153 ` 248` ```apply (induct "p1", simp_all) ``` chaieb@33153 ` 249` ```apply arith ``` chaieb@33153 ` 250` ```done ``` chaieb@33153 ` 251` chaieb@33153 ` 252` ```lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)" ``` chaieb@33153 ` 253` ```by (simp add: poly_cmult_length poly_add_length) ``` chaieb@33153 ` 254` ```declare poly_root_mult_length [simp] ``` chaieb@33153 ` 255` chaieb@33153 ` 256` ```lemma poly_mult_not_eq_poly_Nil: "(poly (p *** q) x \ poly [] x) = ``` chaieb@33153 ` 257` ``` (poly p x \ poly [] x & poly q x \ poly [] (x::'a::idom))" ``` chaieb@33153 ` 258` ```apply (auto simp add: poly_mult) ``` chaieb@33153 ` 259` ```done ``` chaieb@33153 ` 260` ```declare poly_mult_not_eq_poly_Nil [simp] ``` chaieb@33153 ` 261` chaieb@33153 ` 262` ```lemma poly_mult_eq_zero_disj: "(poly (p *** q) (x::'a::idom) = 0) = (poly p x = 0 | poly q x = 0)" ``` chaieb@33153 ` 263` ```by (auto simp add: poly_mult) ``` chaieb@33153 ` 264` chaieb@33153 ` 265` ```text{*Normalisation Properties*} ``` chaieb@33153 ` 266` chaieb@33153 ` 267` ```lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)" ``` chaieb@33153 ` 268` ```by (induct "p", auto) ``` chaieb@33153 ` 269` chaieb@33153 ` 270` ```text{*A nontrivial polynomial of degree n has no more than n roots*} ``` chaieb@33153 ` 271` chaieb@33153 ` 272` ```lemma poly_roots_index_lemma0 [rule_format]: ``` chaieb@33153 ` 273` ``` "\p x. poly p x \ poly [] x & length p = n ``` chaieb@33153 ` 274` ``` --> (\i. \x. (poly p x = (0::'a::idom)) --> (\m. (m \ n & x = i m)))" ``` chaieb@33153 ` 275` ```apply (induct "n", safe) ``` chaieb@33153 ` 276` ```apply (rule ccontr) ``` chaieb@33153 ` 277` ```apply (subgoal_tac "\a. poly p a = 0", safe) ``` chaieb@33153 ` 278` ```apply (drule poly_linear_divides [THEN iffD1], safe) ``` chaieb@33153 ` 279` ```apply (drule_tac x = q in spec) ``` chaieb@33153 ` 280` ```apply (drule_tac x = x in spec) ``` chaieb@33153 ` 281` ```apply (simp del: poly_Nil pmult_Cons) ``` chaieb@33153 ` 282` ```apply (erule exE) ``` chaieb@33153 ` 283` ```apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe) ``` chaieb@33153 ` 284` ```apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe) ``` chaieb@33153 ` 285` ```apply (drule_tac x = "Suc (length q)" in spec) ``` chaieb@33153 ` 286` ```apply (auto simp add: ring_simps) ``` chaieb@33153 ` 287` ```apply (drule_tac x = xa in spec) ``` chaieb@33153 ` 288` ```apply (clarsimp simp add: ring_simps) ``` chaieb@33153 ` 289` ```apply (drule_tac x = m in spec) ``` chaieb@33153 ` 290` ```apply (auto simp add:ring_simps) ``` chaieb@33153 ` 291` ```done ``` chaieb@33153 ` 292` ```lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0, standard] ``` chaieb@33153 ` 293` chaieb@33153 ` 294` ```lemma poly_roots_index_length0: "poly p (x::'a::idom) \ poly [] x ==> ``` chaieb@33153 ` 295` ``` \i. \x. (poly p x = 0) --> (\n. n \ length p & x = i n)" ``` chaieb@33153 ` 296` ```by (blast intro: poly_roots_index_lemma1) ``` chaieb@33153 ` 297` chaieb@33153 ` 298` ```lemma poly_roots_finite_lemma: "poly p (x::'a::idom) \ poly [] x ==> ``` chaieb@33153 ` 299` ``` \N i. \x. (poly p x = 0) --> (\n. (n::nat) < N & x = i n)" ``` chaieb@33153 ` 300` ```apply (drule poly_roots_index_length0, safe) ``` chaieb@33153 ` 301` ```apply (rule_tac x = "Suc (length p)" in exI) ``` chaieb@33153 ` 302` ```apply (rule_tac x = i in exI) ``` chaieb@33153 ` 303` ```apply (simp add: less_Suc_eq_le) ``` chaieb@33153 ` 304` ```done ``` chaieb@33153 ` 305` chaieb@33153 ` 306` chaieb@33153 ` 307` ```lemma real_finite_lemma: ``` chaieb@33153 ` 308` ``` assumes P: "\x. P x --> (\n. n < length j & x = j!n)" ``` chaieb@33153 ` 309` ``` shows "finite {(x::'a::idom). P x}" ``` chaieb@33153 ` 310` ```proof- ``` chaieb@33153 ` 311` ``` let ?M = "{x. P x}" ``` chaieb@33153 ` 312` ``` let ?N = "set j" ``` chaieb@33153 ` 313` ``` have "?M \ ?N" using P by auto ``` chaieb@33153 ` 314` ``` thus ?thesis using finite_subset by auto ``` chaieb@33153 ` 315` ```qed ``` chaieb@33153 ` 316` chaieb@33153 ` 317` ```lemma poly_roots_index_lemma [rule_format]: ``` chaieb@33153 ` 318` ``` "\p x. poly p x \ poly [] x & length p = n ``` chaieb@33153 ` 319` ``` --> (\i. \x. (poly p x = (0::'a::{idom})) --> x \ set i)" ``` chaieb@33153 ` 320` ```apply (induct "n", safe) ``` chaieb@33153 ` 321` ```apply (rule ccontr) ``` chaieb@33153 ` 322` ```apply (subgoal_tac "\a. poly p a = 0", safe) ``` chaieb@33153 ` 323` ```apply (drule poly_linear_divides [THEN iffD1], safe) ``` chaieb@33153 ` 324` ```apply (drule_tac x = q in spec) ``` chaieb@33153 ` 325` ```apply (drule_tac x = x in spec) ``` chaieb@33153 ` 326` ```apply (auto simp del: poly_Nil pmult_Cons) ``` chaieb@33153 ` 327` ```apply (drule_tac x = "a#i" in spec) ``` chaieb@33153 ` 328` ```apply (auto simp only: poly_mult List.list.size) ``` chaieb@33153 ` 329` ```apply (drule_tac x = xa in spec) ``` chaieb@33153 ` 330` ```apply (clarsimp simp add: ring_simps) ``` chaieb@33153 ` 331` ```done ``` chaieb@33153 ` 332` chaieb@33153 ` 333` ```lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard] ``` chaieb@33153 ` 334` chaieb@33153 ` 335` ```lemma poly_roots_index_length: "poly p (x::'a::idom) \ poly [] x ==> ``` chaieb@33153 ` 336` ``` \i. \x. (poly p x = 0) --> x \ set i" ``` chaieb@33153 ` 337` ```by (blast intro: poly_roots_index_lemma2) ``` chaieb@33153 ` 338` chaieb@33153 ` 339` ```lemma poly_roots_finite_lemma': "poly p (x::'a::idom) \ poly [] x ==> ``` chaieb@33153 ` 340` ``` \i. \x. (poly p x = 0) --> x \ set i" ``` chaieb@33153 ` 341` ```by (drule poly_roots_index_length, safe) ``` chaieb@33153 ` 342` chaieb@33153 ` 343` ```lemma UNIV_nat_infinite: "\ finite (UNIV :: nat set)" ``` chaieb@33153 ` 344` ``` unfolding finite_conv_nat_seg_image ``` chaieb@33153 ` 345` ```proof(auto simp add: expand_set_eq image_iff) ``` chaieb@33153 ` 346` ``` fix n::nat and f:: "nat \ nat" ``` chaieb@33153 ` 347` ``` let ?N = "{i. i < n}" ``` chaieb@33153 ` 348` ``` let ?fN = "f ` ?N" ``` chaieb@33153 ` 349` ``` let ?y = "Max ?fN + 1" ``` chaieb@33153 ` 350` ``` from nat_seg_image_imp_finite[of "?fN" "f" n] ``` chaieb@33153 ` 351` ``` have thfN: "finite ?fN" by simp ``` chaieb@33153 ` 352` ``` {assume "n =0" hence "\x. \xa f xa" by auto} ``` chaieb@33153 ` 353` ``` moreover ``` chaieb@33153 ` 354` ``` {assume nz: "n \ 0" ``` chaieb@33153 ` 355` ``` hence thne: "?fN \ {}" by (auto simp add: neq0_conv) ``` chaieb@33153 ` 356` ``` have "\x\ ?fN. Max ?fN \ x" using nz Max_ge_iff[OF thfN thne] by auto ``` chaieb@33153 ` 357` ``` hence "\x\ ?fN. ?y > x" by (auto simp add: less_Suc_eq_le) ``` chaieb@33153 ` 358` ``` hence "?y \ ?fN" by auto ``` chaieb@33153 ` 359` ``` hence "\x. \xa f xa" by auto } ``` chaieb@33153 ` 360` ``` ultimately show "\x. \xa f xa" by blast ``` chaieb@33153 ` 361` ```qed ``` chaieb@33153 ` 362` chaieb@33153 ` 363` ```lemma UNIV_ring_char_0_infinte: "\ finite (UNIV:: ('a::ring_char_0) set)" ``` chaieb@33153 ` 364` ```proof ``` chaieb@33153 ` 365` ``` assume F: "finite (UNIV :: 'a set)" ``` chaieb@33153 ` 366` ``` have th0: "of_nat ` UNIV \ (UNIV:: 'a set)" by simp ``` chaieb@33153 ` 367` ``` from finite_subset[OF th0 F] have th: "finite (of_nat ` UNIV :: 'a set)" . ``` chaieb@33153 ` 368` ``` have th': "inj_on (of_nat::nat \ 'a) (UNIV)" ``` chaieb@33153 ` 369` ``` unfolding inj_on_def by auto ``` chaieb@33153 ` 370` ``` from finite_imageD[OF th th'] UNIV_nat_infinite ``` chaieb@33153 ` 371` ``` show False by blast ``` chaieb@33153 ` 372` ```qed ``` chaieb@33153 ` 373` chaieb@33153 ` 374` ```lemma poly_roots_finite: "(poly p \ poly []) = ``` chaieb@33153 ` 375` ``` finite {x. poly p x = (0::'a::{idom, ring_char_0})}" ``` chaieb@33153 ` 376` ```proof ``` chaieb@33153 ` 377` ``` assume H: "poly p \ poly []" ``` chaieb@33153 ` 378` ``` show "finite {x. poly p x = (0::'a)}" ``` chaieb@33153 ` 379` ``` using H ``` chaieb@33153 ` 380` ``` apply - ``` chaieb@33153 ` 381` ``` apply (erule contrapos_np, rule ext) ``` chaieb@33153 ` 382` ``` apply (rule ccontr) ``` chaieb@33153 ` 383` ``` apply (clarify dest!: poly_roots_finite_lemma') ``` chaieb@33153 ` 384` ``` using finite_subset ``` chaieb@33153 ` 385` ``` proof- ``` chaieb@33153 ` 386` ``` fix x i ``` chaieb@33153 ` 387` ``` assume F: "\ finite {x. poly p x = (0\'a)}" ``` chaieb@33153 ` 388` ``` and P: "\x. poly p x = (0\'a) \ x \ set i" ``` chaieb@33153 ` 389` ``` let ?M= "{x. poly p x = (0\'a)}" ``` chaieb@33153 ` 390` ``` from P have "?M \ set i" by auto ``` chaieb@33153 ` 391` ``` with finite_subset F show False by auto ``` chaieb@33153 ` 392` ``` qed ``` chaieb@33153 ` 393` ```next ``` chaieb@33153 ` 394` ``` assume F: "finite {x. poly p x = (0\'a)}" ``` chaieb@33153 ` 395` ``` show "poly p \ poly []" using F UNIV_ring_char_0_infinte by auto ``` chaieb@33153 ` 396` ```qed ``` chaieb@33153 ` 397` chaieb@33153 ` 398` ```text{*Entirety and Cancellation for polynomials*} ``` chaieb@33153 ` 399` chaieb@33153 ` 400` ```lemma poly_entire_lemma: "[| poly (p:: ('a::{idom,ring_char_0}) list) \ poly [] ; poly q \ poly [] |] ``` chaieb@33153 ` 401` ``` ==> poly (p *** q) \ poly []" ``` chaieb@33153 ` 402` ```by (auto simp add: poly_roots_finite poly_mult Collect_disj_eq) ``` chaieb@33153 ` 403` chaieb@33153 ` 404` ```lemma poly_entire: "(poly (p *** q) = poly ([]::('a::{idom,ring_char_0}) list)) = ((poly p = poly []) | (poly q = poly []))" ``` chaieb@33153 ` 405` ```apply (auto intro: ext dest: fun_cong simp add: poly_entire_lemma poly_mult) ``` chaieb@33153 ` 406` ```apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst]) ``` chaieb@33153 ` 407` ```done ``` chaieb@33153 ` 408` chaieb@33153 ` 409` ```lemma poly_entire_neg: "(poly (p *** q) \ poly ([]::('a::{idom,ring_char_0}) list)) = ((poly p \ poly []) & (poly q \ poly []))" ``` chaieb@33153 ` 410` ```by (simp add: poly_entire) ``` chaieb@33153 ` 411` chaieb@33153 ` 412` ```lemma fun_eq: " (f = g) = (\x. f x = g x)" ``` chaieb@33153 ` 413` ```by (auto intro!: ext) ``` chaieb@33153 ` 414` chaieb@33153 ` 415` ```lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)" ``` chaieb@33153 ` 416` ```by (auto simp add: ring_simps poly_add poly_minus_def fun_eq poly_cmult) ``` chaieb@33153 ` 417` chaieb@33153 ` 418` ```lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))" ``` chaieb@33153 ` 419` ```by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib) ``` chaieb@33153 ` 420` chaieb@33153 ` 421` ```lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly ([]::('a::{idom, ring_char_0}) list) | poly q = poly r)" ``` chaieb@33153 ` 422` ```apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst]) ``` chaieb@33153 ` 423` ```apply (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff) ``` chaieb@33153 ` 424` ```done ``` chaieb@33153 ` 425` chaieb@33153 ` 426` ```lemma poly_exp_eq_zero: ``` chaieb@33153 ` 427` ``` "(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \ 0)" ``` chaieb@33153 ` 428` ```apply (simp only: fun_eq add: all_simps [symmetric]) ``` chaieb@33153 ` 429` ```apply (rule arg_cong [where f = All]) ``` chaieb@33153 ` 430` ```apply (rule ext) ``` chaieb@33153 ` 431` ```apply (induct_tac "n") ``` chaieb@33153 ` 432` ```apply (auto simp add: poly_mult) ``` chaieb@33153 ` 433` ```done ``` chaieb@33153 ` 434` ```declare poly_exp_eq_zero [simp] ``` chaieb@33153 ` 435` chaieb@33153 ` 436` ```lemma poly_prime_eq_zero: "poly [a,(1::'a::comm_ring_1)] \ poly []" ``` chaieb@33153 ` 437` ```apply (simp add: fun_eq) ``` chaieb@33153 ` 438` ```apply (rule_tac x = "1 - a" in exI, simp) ``` chaieb@33153 ` 439` ```done ``` chaieb@33153 ` 440` ```declare poly_prime_eq_zero [simp] ``` chaieb@33153 ` 441` chaieb@33153 ` 442` ```lemma poly_exp_prime_eq_zero: "(poly ([a, (1::'a::idom)] %^ n) \ poly [])" ``` chaieb@33153 ` 443` ```by auto ``` chaieb@33153 ` 444` ```declare poly_exp_prime_eq_zero [simp] ``` chaieb@33153 ` 445` chaieb@33153 ` 446` ```text{*A more constructive notion of polynomials being trivial*} ``` chaieb@33153 ` 447` chaieb@33153 ` 448` ```lemma poly_zero_lemma': "poly (h # t) = poly [] ==> h = (0::'a::{idom,ring_char_0}) & poly t = poly []" ``` chaieb@33153 ` 449` ```apply(simp add: fun_eq) ``` chaieb@33153 ` 450` ```apply (case_tac "h = 0") ``` chaieb@33153 ` 451` ```apply (drule_tac [2] x = 0 in spec, auto) ``` chaieb@33153 ` 452` ```apply (case_tac "poly t = poly []", simp) ``` chaieb@33153 ` 453` ```proof- ``` chaieb@33153 ` 454` ``` fix x ``` chaieb@33153 ` 455` ``` assume H: "\x. x = (0\'a) \ poly t x = (0\'a)" and pnz: "poly t \ poly []" ``` chaieb@33153 ` 456` ``` let ?S = "{x. poly t x = 0}" ``` chaieb@33153 ` 457` ``` from H have "\x. x \0 \ poly t x = 0" by blast ``` chaieb@33153 ` 458` ``` hence th: "?S \ UNIV - {0}" by auto ``` chaieb@33153 ` 459` ``` from poly_roots_finite pnz have th': "finite ?S" by blast ``` chaieb@33153 ` 460` ``` from finite_subset[OF th th'] UNIV_ring_char_0_infinte[where ?'a = 'a] ``` chaieb@33153 ` 461` ``` show "poly t x = (0\'a)" by simp ``` chaieb@33153 ` 462` ``` qed ``` chaieb@33153 ` 463` chaieb@33153 ` 464` ```lemma poly_zero: "(poly p = poly []) = list_all (%c. c = (0::'a::{idom,ring_char_0})) p" ``` chaieb@33153 ` 465` ```apply (induct "p", simp) ``` chaieb@33153 ` 466` ```apply (rule iffI) ``` chaieb@33153 ` 467` ```apply (drule poly_zero_lemma', auto) ``` chaieb@33153 ` 468` ```done ``` chaieb@33153 ` 469` chaieb@33153 ` 470` chaieb@33153 ` 471` chaieb@33153 ` 472` ```text{*Basics of divisibility.*} ``` chaieb@33153 ` 473` chaieb@33153 ` 474` ```lemma poly_primes: "([a, (1::'a::idom)] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)" ``` chaieb@33153 ` 475` ```apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric]) ``` chaieb@33153 ` 476` ```apply (drule_tac x = "-a" in spec) ``` chaieb@33153 ` 477` ```apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric]) ``` chaieb@33153 ` 478` ```apply (rule_tac x = "qa *** q" in exI) ``` chaieb@33153 ` 479` ```apply (rule_tac [2] x = "p *** qa" in exI) ``` chaieb@33153 ` 480` ```apply (auto simp add: poly_add poly_mult poly_cmult mult_ac) ``` chaieb@33153 ` 481` ```done ``` chaieb@33153 ` 482` chaieb@33153 ` 483` ```lemma poly_divides_refl: "p divides p" ``` chaieb@33153 ` 484` ```apply (simp add: divides_def) ``` chaieb@33153 ` 485` ```apply (rule_tac x = "[1]" in exI) ``` chaieb@33153 ` 486` ```apply (auto simp add: poly_mult fun_eq) ``` chaieb@33153 ` 487` ```done ``` chaieb@33153 ` 488` ```declare poly_divides_refl [simp] ``` chaieb@33153 ` 489` chaieb@33153 ` 490` ```lemma poly_divides_trans: "[| p divides q; q divides r |] ==> p divides r" ``` chaieb@33153 ` 491` ```apply (simp add: divides_def, safe) ``` chaieb@33153 ` 492` ```apply (rule_tac x = "qa *** qaa" in exI) ``` chaieb@33153 ` 493` ```apply (auto simp add: poly_mult fun_eq mult_assoc) ``` chaieb@33153 ` 494` ```done ``` chaieb@33153 ` 495` chaieb@33153 ` 496` ```lemma poly_divides_exp: "m \ n ==> (p %^ m) divides (p %^ n)" ``` chaieb@33153 ` 497` ```apply (auto simp add: le_iff_add) ``` chaieb@33153 ` 498` ```apply (induct_tac k) ``` chaieb@33153 ` 499` ```apply (rule_tac [2] poly_divides_trans) ``` chaieb@33153 ` 500` ```apply (auto simp add: divides_def) ``` chaieb@33153 ` 501` ```apply (rule_tac x = p in exI) ``` chaieb@33153 ` 502` ```apply (auto simp add: poly_mult fun_eq mult_ac) ``` chaieb@33153 ` 503` ```done ``` chaieb@33153 ` 504` chaieb@33153 ` 505` ```lemma poly_exp_divides: "[| (p %^ n) divides q; m\n |] ==> (p %^ m) divides q" ``` chaieb@33153 ` 506` ```by (blast intro: poly_divides_exp poly_divides_trans) ``` chaieb@33153 ` 507` chaieb@33153 ` 508` ```lemma poly_divides_add: ``` chaieb@33153 ` 509` ``` "[| p divides q; p divides r |] ==> p divides (q +++ r)" ``` chaieb@33153 ` 510` ```apply (simp add: divides_def, auto) ``` chaieb@33153 ` 511` ```apply (rule_tac x = "qa +++ qaa" in exI) ``` chaieb@33153 ` 512` ```apply (auto simp add: poly_add fun_eq poly_mult right_distrib) ``` chaieb@33153 ` 513` ```done ``` chaieb@33153 ` 514` chaieb@33153 ` 515` ```lemma poly_divides_diff: ``` chaieb@33153 ` 516` ``` "[| p divides q; p divides (q +++ r) |] ==> p divides r" ``` chaieb@33153 ` 517` ```apply (simp add: divides_def, auto) ``` chaieb@33153 ` 518` ```apply (rule_tac x = "qaa +++ -- qa" in exI) ``` chaieb@33153 ` 519` ```apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib algebra_simps) ``` chaieb@33153 ` 520` ```done ``` chaieb@33153 ` 521` chaieb@33153 ` 522` ```lemma poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q" ``` chaieb@33153 ` 523` ```apply (erule poly_divides_diff) ``` chaieb@33153 ` 524` ```apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac) ``` chaieb@33153 ` 525` ```done ``` chaieb@33153 ` 526` chaieb@33153 ` 527` ```lemma poly_divides_zero: "poly p = poly [] ==> q divides p" ``` chaieb@33153 ` 528` ```apply (simp add: divides_def) ``` chaieb@33153 ` 529` ```apply (rule exI[where x="[]"]) ``` chaieb@33153 ` 530` ```apply (auto simp add: fun_eq poly_mult) ``` chaieb@33153 ` 531` ```done ``` chaieb@33153 ` 532` chaieb@33153 ` 533` ```lemma poly_divides_zero2: "q divides []" ``` chaieb@33153 ` 534` ```apply (simp add: divides_def) ``` chaieb@33153 ` 535` ```apply (rule_tac x = "[]" in exI) ``` chaieb@33153 ` 536` ```apply (auto simp add: fun_eq) ``` chaieb@33153 ` 537` ```done ``` chaieb@33153 ` 538` ```declare poly_divides_zero2 [simp] ``` chaieb@33153 ` 539` chaieb@33153 ` 540` ```text{*At last, we can consider the order of a root.*} ``` chaieb@33153 ` 541` chaieb@33153 ` 542` chaieb@33153 ` 543` ```lemma poly_order_exists_lemma [rule_format]: ``` chaieb@33153 ` 544` ``` "\p. length p = d --> poly p \ poly [] ``` chaieb@33153 ` 545` ``` --> (\n q. p = mulexp n [-a, (1::'a::{idom,ring_char_0})] q & poly q a \ 0)" ``` chaieb@33153 ` 546` ```apply (induct "d") ``` chaieb@33153 ` 547` ```apply (simp add: fun_eq, safe) ``` chaieb@33153 ` 548` ```apply (case_tac "poly p a = 0") ``` chaieb@33153 ` 549` ```apply (drule_tac poly_linear_divides [THEN iffD1], safe) ``` chaieb@33153 ` 550` ```apply (drule_tac x = q in spec) ``` chaieb@33153 ` 551` ```apply (drule_tac poly_entire_neg [THEN iffD1], safe, force) ``` chaieb@33153 ` 552` ```apply (rule_tac x = "Suc n" in exI) ``` chaieb@33153 ` 553` ```apply (rule_tac x = qa in exI) ``` chaieb@33153 ` 554` ```apply (simp del: pmult_Cons) ``` chaieb@33153 ` 555` ```apply (rule_tac x = 0 in exI, force) ``` chaieb@33153 ` 556` ```done ``` chaieb@33153 ` 557` chaieb@33153 ` 558` ```(* FIXME: Tidy up *) ``` chaieb@33153 ` 559` ```lemma poly_order_exists: ``` chaieb@33153 ` 560` ``` "[| length p = d; poly p \ poly [] |] ``` chaieb@33153 ` 561` ``` ==> \n. ([-a, 1] %^ n) divides p & ``` chaieb@33153 ` 562` ``` ~(([-a, (1::'a::{idom,ring_char_0})] %^ (Suc n)) divides p)" ``` chaieb@33153 ` 563` ```apply (drule poly_order_exists_lemma [where a=a], assumption, clarify) ``` chaieb@33153 ` 564` ```apply (rule_tac x = n in exI, safe) ``` chaieb@33153 ` 565` ```apply (unfold divides_def) ``` chaieb@33153 ` 566` ```apply (rule_tac x = q in exI) ``` chaieb@33153 ` 567` ```apply (induct_tac "n", simp) ``` chaieb@33153 ` 568` ```apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac) ``` chaieb@33153 ` 569` ```apply safe ``` chaieb@33153 ` 570` ```apply (subgoal_tac "poly (mulexp n [- a, 1] q) \ poly ([- a, 1] %^ Suc n *** qa)") ``` chaieb@33153 ` 571` ```apply simp ``` chaieb@33153 ` 572` ```apply (induct_tac "n") ``` chaieb@33153 ` 573` ```apply (simp del: pmult_Cons pexp_Suc) ``` chaieb@33153 ` 574` ```apply (erule_tac Q = "poly q a = 0" in contrapos_np) ``` chaieb@33153 ` 575` ```apply (simp add: poly_add poly_cmult) ``` chaieb@33153 ` 576` ```apply (rule pexp_Suc [THEN ssubst]) ``` chaieb@33153 ` 577` ```apply (rule ccontr) ``` chaieb@33153 ` 578` ```apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc) ``` chaieb@33153 ` 579` ```done ``` chaieb@33153 ` 580` chaieb@33153 ` 581` ```lemma poly_one_divides: "[1] divides p" ``` chaieb@33153 ` 582` ```by (simp add: divides_def, auto) ``` chaieb@33153 ` 583` ```declare poly_one_divides [simp] ``` chaieb@33153 ` 584` chaieb@33153 ` 585` ```lemma poly_order: "poly p \ poly [] ``` chaieb@33153 ` 586` ``` ==> EX! n. ([-a, (1::'a::{idom,ring_char_0})] %^ n) divides p & ``` chaieb@33153 ` 587` ``` ~(([-a, 1] %^ (Suc n)) divides p)" ``` chaieb@33153 ` 588` ```apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc) ``` chaieb@33153 ` 589` ```apply (cut_tac x = y and y = n in less_linear) ``` chaieb@33153 ` 590` ```apply (drule_tac m = n in poly_exp_divides) ``` chaieb@33153 ` 591` ```apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides] ``` chaieb@33153 ` 592` ``` simp del: pmult_Cons pexp_Suc) ``` chaieb@33153 ` 593` ```done ``` chaieb@33153 ` 594` chaieb@33153 ` 595` ```text{*Order*} ``` chaieb@33153 ` 596` chaieb@33153 ` 597` ```lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n" ``` chaieb@33153 ` 598` ```by (blast intro: someI2) ``` chaieb@33153 ` 599` chaieb@33153 ` 600` ```lemma order: ``` chaieb@33153 ` 601` ``` "(([-a, (1::'a::{idom,ring_char_0})] %^ n) divides p & ``` chaieb@33153 ` 602` ``` ~(([-a, 1] %^ (Suc n)) divides p)) = ``` chaieb@33153 ` 603` ``` ((n = order a p) & ~(poly p = poly []))" ``` chaieb@33153 ` 604` ```apply (unfold order_def) ``` chaieb@33153 ` 605` ```apply (rule iffI) ``` chaieb@33153 ` 606` ```apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order) ``` chaieb@33153 ` 607` ```apply (blast intro!: poly_order [THEN [2] some1_equalityD]) ``` chaieb@33153 ` 608` ```done ``` chaieb@33153 ` 609` chaieb@33153 ` 610` ```lemma order2: "[| poly p \ poly [] |] ``` chaieb@33153 ` 611` ``` ==> ([-a, (1::'a::{idom,ring_char_0})] %^ (order a p)) divides p & ``` chaieb@33153 ` 612` ``` ~(([-a, 1] %^ (Suc(order a p))) divides p)" ``` chaieb@33153 ` 613` ```by (simp add: order del: pexp_Suc) ``` chaieb@33153 ` 614` chaieb@33153 ` 615` ```lemma order_unique: "[| poly p \ poly []; ([-a, 1] %^ n) divides p; ``` chaieb@33153 ` 616` ``` ~(([-a, (1::'a::{idom,ring_char_0})] %^ (Suc n)) divides p) ``` chaieb@33153 ` 617` ``` |] ==> (n = order a p)" ``` chaieb@33153 ` 618` ```by (insert order [of a n p], auto) ``` chaieb@33153 ` 619` chaieb@33153 ` 620` ```lemma order_unique_lemma: "(poly p \ poly [] & ([-a, 1] %^ n) divides p & ``` chaieb@33153 ` 621` ``` ~(([-a, (1::'a::{idom,ring_char_0})] %^ (Suc n)) divides p)) ``` chaieb@33153 ` 622` ``` ==> (n = order a p)" ``` chaieb@33153 ` 623` ```by (blast intro: order_unique) ``` chaieb@33153 ` 624` chaieb@33153 ` 625` ```lemma order_poly: "poly p = poly q ==> order a p = order a q" ``` chaieb@33153 ` 626` ```by (auto simp add: fun_eq divides_def poly_mult order_def) ``` chaieb@33153 ` 627` chaieb@33153 ` 628` ```lemma pexp_one: "p %^ (Suc 0) = p" ``` chaieb@33153 ` 629` ```apply (induct "p") ``` chaieb@33153 ` 630` ```apply (auto simp add: numeral_1_eq_1) ``` chaieb@33153 ` 631` ```done ``` chaieb@33153 ` 632` ```declare pexp_one [simp] ``` chaieb@33153 ` 633` chaieb@33153 ` 634` ```lemma lemma_order_root [rule_format]: ``` chaieb@33153 ` 635` ``` "\p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p ``` chaieb@33153 ` 636` ``` --> poly p a = 0" ``` chaieb@33153 ` 637` ```apply (induct "n", blast) ``` chaieb@33153 ` 638` ```apply (auto simp add: divides_def poly_mult simp del: pmult_Cons) ``` chaieb@33153 ` 639` ```done ``` chaieb@33153 ` 640` chaieb@33153 ` 641` ```lemma order_root: "(poly p a = (0::'a::{idom,ring_char_0})) = ((poly p = poly []) | order a p \ 0)" ``` chaieb@33153 ` 642` ```apply (case_tac "poly p = poly []", auto) ``` chaieb@33153 ` 643` ```apply (simp add: poly_linear_divides del: pmult_Cons, safe) ``` chaieb@33153 ` 644` ```apply (drule_tac [!] a = a in order2) ``` chaieb@33153 ` 645` ```apply (rule ccontr) ``` chaieb@33153 ` 646` ```apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast) ``` chaieb@33153 ` 647` ```using neq0_conv ``` chaieb@33153 ` 648` ```apply (blast intro: lemma_order_root) ``` chaieb@33153 ` 649` ```done ``` chaieb@33153 ` 650` chaieb@33153 ` 651` ```lemma order_divides: "(([-a, 1::'a::{idom,ring_char_0}] %^ n) divides p) = ((poly p = poly []) | n \ order a p)" ``` chaieb@33153 ` 652` ```apply (case_tac "poly p = poly []", auto) ``` chaieb@33153 ` 653` ```apply (simp add: divides_def fun_eq poly_mult) ``` chaieb@33153 ` 654` ```apply (rule_tac x = "[]" in exI) ``` chaieb@33153 ` 655` ```apply (auto dest!: order2 [where a=a] ``` chaieb@33153 ` 656` ``` intro: poly_exp_divides simp del: pexp_Suc) ``` chaieb@33153 ` 657` ```done ``` chaieb@33153 ` 658` chaieb@33153 ` 659` ```lemma order_decomp: ``` chaieb@33153 ` 660` ``` "poly p \ poly [] ``` chaieb@33153 ` 661` ``` ==> \q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) & ``` chaieb@33153 ` 662` ``` ~([-a, 1::'a::{idom,ring_char_0}] divides q)" ``` chaieb@33153 ` 663` ```apply (unfold divides_def) ``` chaieb@33153 ` 664` ```apply (drule order2 [where a = a]) ``` chaieb@33153 ` 665` ```apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe) ``` chaieb@33153 ` 666` ```apply (rule_tac x = q in exI, safe) ``` chaieb@33153 ` 667` ```apply (drule_tac x = qa in spec) ``` chaieb@33153 ` 668` ```apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons) ``` chaieb@33153 ` 669` ```done ``` chaieb@33153 ` 670` chaieb@33153 ` 671` ```text{*Important composition properties of orders.*} ``` chaieb@33153 ` 672` chaieb@33153 ` 673` ```lemma order_mult: "poly (p *** q) \ poly [] ``` chaieb@33153 ` 674` ``` ==> order a (p *** q) = order a p + order (a::'a::{idom,ring_char_0}) q" ``` chaieb@33153 ` 675` ```apply (cut_tac a = a and p = "p***q" and n = "order a p + order a q" in order) ``` chaieb@33153 ` 676` ```apply (auto simp add: poly_entire simp del: pmult_Cons) ``` chaieb@33153 ` 677` ```apply (drule_tac a = a in order2)+ ``` chaieb@33153 ` 678` ```apply safe ``` chaieb@33153 ` 679` ```apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) ``` chaieb@33153 ` 680` ```apply (rule_tac x = "qa *** qaa" in exI) ``` chaieb@33153 ` 681` ```apply (simp add: poly_mult mult_ac del: pmult_Cons) ``` chaieb@33153 ` 682` ```apply (drule_tac a = a in order_decomp)+ ``` chaieb@33153 ` 683` ```apply safe ``` chaieb@33153 ` 684` ```apply (subgoal_tac "[-a,1] divides (qa *** qaa) ") ``` chaieb@33153 ` 685` ```apply (simp add: poly_primes del: pmult_Cons) ``` chaieb@33153 ` 686` ```apply (auto simp add: divides_def simp del: pmult_Cons) ``` chaieb@33153 ` 687` ```apply (rule_tac x = qb in exI) ``` chaieb@33153 ` 688` ```apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))") ``` chaieb@33153 ` 689` ```apply (drule poly_mult_left_cancel [THEN iffD1], force) ``` chaieb@33153 ` 690` ```apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ") ``` chaieb@33153 ` 691` ```apply (drule poly_mult_left_cancel [THEN iffD1], force) ``` chaieb@33153 ` 692` ```apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) ``` chaieb@33153 ` 693` ```done ``` chaieb@33153 ` 694` chaieb@33153 ` 695` chaieb@33153 ` 696` chaieb@33153 ` 697` ```lemma order_root2: "poly p \ poly [] ==> (poly p a = 0) = (order (a::'a::{idom,ring_char_0}) p \ 0)" ``` chaieb@33153 ` 698` ```by (rule order_root [THEN ssubst], auto) ``` chaieb@33153 ` 699` chaieb@33153 ` 700` chaieb@33153 ` 701` ```lemma pmult_one: "[1] *** p = p" ``` chaieb@33153 ` 702` ```by auto ``` chaieb@33153 ` 703` ```declare pmult_one [simp] ``` chaieb@33153 ` 704` chaieb@33153 ` 705` ```lemma poly_Nil_zero: "poly [] = poly [0]" ``` chaieb@33153 ` 706` ```by (simp add: fun_eq) ``` chaieb@33153 ` 707` chaieb@33153 ` 708` ```lemma rsquarefree_decomp: ``` chaieb@33153 ` 709` ``` "[| rsquarefree p; poly p a = (0::'a::{idom,ring_char_0}) |] ``` chaieb@33153 ` 710` ``` ==> \q. (poly p = poly ([-a, 1] *** q)) & poly q a \ 0" ``` chaieb@33153 ` 711` ```apply (simp add: rsquarefree_def, safe) ``` chaieb@33153 ` 712` ```apply (frule_tac a = a in order_decomp) ``` chaieb@33153 ` 713` ```apply (drule_tac x = a in spec) ``` chaieb@33153 ` 714` ```apply (drule_tac a = a in order_root2 [symmetric]) ``` chaieb@33153 ` 715` ```apply (auto simp del: pmult_Cons) ``` chaieb@33153 ` 716` ```apply (rule_tac x = q in exI, safe) ``` chaieb@33153 ` 717` ```apply (simp add: poly_mult fun_eq) ``` chaieb@33153 ` 718` ```apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1]) ``` chaieb@33153 ` 719` ```apply (simp add: divides_def del: pmult_Cons, safe) ``` chaieb@33153 ` 720` ```apply (drule_tac x = "[]" in spec) ``` chaieb@33153 ` 721` ```apply (auto simp add: fun_eq) ``` chaieb@33153 ` 722` ```done ``` chaieb@33153 ` 723` chaieb@33153 ` 724` chaieb@33153 ` 725` ```text{*Normalization of a polynomial.*} ``` chaieb@33153 ` 726` chaieb@33153 ` 727` ```lemma poly_normalize: "poly (pnormalize p) = poly p" ``` chaieb@33153 ` 728` ```apply (induct "p") ``` chaieb@33153 ` 729` ```apply (auto simp add: fun_eq) ``` chaieb@33153 ` 730` ```done ``` chaieb@33153 ` 731` ```declare poly_normalize [simp] ``` chaieb@33153 ` 732` chaieb@33153 ` 733` chaieb@33153 ` 734` ```text{*The degree of a polynomial.*} ``` chaieb@33153 ` 735` chaieb@33153 ` 736` ```lemma lemma_degree_zero: ``` chaieb@33153 ` 737` ``` "list_all (%c. c = 0) p \ pnormalize p = []" ``` chaieb@33153 ` 738` ```by (induct "p", auto) ``` chaieb@33153 ` 739` chaieb@33153 ` 740` ```lemma degree_zero: "(poly p = poly ([]:: (('a::{idom,ring_char_0}) list))) \ (degree p = 0)" ``` chaieb@33153 ` 741` ```apply (simp add: degree_def) ``` chaieb@33153 ` 742` ```apply (case_tac "pnormalize p = []") ``` chaieb@33153 ` 743` ```apply (auto simp add: poly_zero lemma_degree_zero ) ``` chaieb@33153 ` 744` ```done ``` chaieb@33153 ` 745` chaieb@33153 ` 746` ```lemma pnormalize_sing: "(pnormalize [x] = [x]) \ x \ 0" by simp ``` chaieb@33153 ` 747` ```lemma pnormalize_pair: "y \ 0 \ (pnormalize [x, y] = [x, y])" by simp ``` chaieb@33153 ` 748` ```lemma pnormal_cons: "pnormal p \ pnormal (c#p)" ``` chaieb@33153 ` 749` ``` unfolding pnormal_def by simp ``` chaieb@33153 ` 750` ```lemma pnormal_tail: "p\[] \ pnormal (c#p) \ pnormal p" ``` chaieb@33153 ` 751` ``` unfolding pnormal_def ``` chaieb@33153 ` 752` ``` apply (cases "pnormalize p = []", auto) ``` chaieb@33153 ` 753` ``` by (cases "c = 0", auto) ``` chaieb@33153 ` 754` ```lemma pnormal_last_nonzero: "pnormal p ==> last p \ 0" ``` chaieb@33153 ` 755` ``` apply (induct p, auto simp add: pnormal_def) ``` chaieb@33153 ` 756` ``` apply (case_tac "pnormalize p = []", auto) ``` chaieb@33153 ` 757` ``` by (case_tac "a=0", auto) ``` chaieb@33153 ` 758` ```lemma pnormal_length: "pnormal p \ 0 < length p" ``` chaieb@33153 ` 759` ``` unfolding pnormal_def length_greater_0_conv by blast ``` chaieb@33153 ` 760` ```lemma pnormal_last_length: "\0 < length p ; last p \ 0\ \ pnormal p" ``` chaieb@33153 ` 761` ``` apply (induct p, auto) ``` chaieb@33153 ` 762` ``` apply (case_tac "p = []", auto) ``` chaieb@33153 ` 763` ``` apply (simp add: pnormal_def) ``` chaieb@33153 ` 764` ``` by (rule pnormal_cons, auto) ``` chaieb@33153 ` 765` ```lemma pnormal_id: "pnormal p \ (0 < length p \ last p \ 0)" ``` chaieb@33153 ` 766` ``` using pnormal_last_length pnormal_length pnormal_last_nonzero by blast ``` chaieb@33153 ` 767` chaieb@33153 ` 768` ```text{*Tidier versions of finiteness of roots.*} ``` chaieb@33153 ` 769` chaieb@33153 ` 770` ```lemma poly_roots_finite_set: "poly p \ poly [] ==> finite {x::'a::{idom,ring_char_0}. poly p x = 0}" ``` chaieb@33153 ` 771` ```unfolding poly_roots_finite . ``` chaieb@33153 ` 772` chaieb@33153 ` 773` ```text{*bound for polynomial.*} ``` chaieb@33153 ` 774` chaieb@33153 ` 775` ```lemma poly_mono: "abs(x) \ k ==> abs(poly p (x::'a::{ordered_idom})) \ poly (map abs p) k" ``` chaieb@33153 ` 776` ```apply (induct "p", auto) ``` chaieb@33153 ` 777` ```apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans) ``` chaieb@33153 ` 778` ```apply (rule abs_triangle_ineq) ``` chaieb@33153 ` 779` ```apply (auto intro!: mult_mono simp add: abs_mult) ``` chaieb@33153 ` 780` ```done ``` chaieb@33153 ` 781` chaieb@33153 ` 782` ```lemma poly_Sing: "poly [c] x = c" by simp ``` chaieb@33153 ` 783` ```end ```