src/HOL/Algebra/UnivPoly.thy
 author wenzelm Wed Jun 13 00:01:41 2007 +0200 (2007-06-13) changeset 23350 50c5b0912a0c parent 22931 11cc1ccad58e child 26202 51f8a696cd8d permissions -rw-r--r--
tuned proofs: avoid implicit prems;
 ballarin@13940 ` 1` ```(* ``` wenzelm@14706 ` 2` ``` Title: HOL/Algebra/UnivPoly.thy ``` ballarin@13940 ` 3` ``` Id: \$Id\$ ``` ballarin@13940 ` 4` ``` Author: Clemens Ballarin, started 9 December 1996 ``` ballarin@13940 ` 5` ``` Copyright: Clemens Ballarin ``` ballarin@13940 ` 6` ```*) ``` ballarin@13940 ` 7` ballarin@20318 ` 8` ```theory UnivPoly imports Module begin ``` ballarin@13940 ` 9` ballarin@20318 ` 10` ballarin@20318 ` 11` ```section {* Univariate Polynomials *} ``` ballarin@13940 ` 12` ballarin@14553 ` 13` ```text {* ``` wenzelm@14666 ` 14` ``` Polynomials are formalised as modules with additional operations for ``` wenzelm@14666 ` 15` ``` extracting coefficients from polynomials and for obtaining monomials ``` wenzelm@14666 ` 16` ``` from coefficients and exponents (record @{text "up_ring"}). The ``` wenzelm@14666 ` 17` ``` carrier set is a set of bounded functions from Nat to the ``` wenzelm@14666 ` 18` ``` coefficient domain. Bounded means that these functions return zero ``` wenzelm@14666 ` 19` ``` above a certain bound (the degree). There is a chapter on the ``` wenzelm@14706 ` 20` ``` formalisation of polynomials in the PhD thesis \cite{Ballarin:1999}, ``` wenzelm@14706 ` 21` ``` which was implemented with axiomatic type classes. This was later ``` wenzelm@14706 ` 22` ``` ported to Locales. ``` ballarin@14553 ` 23` ```*} ``` ballarin@14553 ` 24` wenzelm@14666 ` 25` ballarin@13949 ` 26` ```subsection {* The Constructor for Univariate Polynomials *} ``` ballarin@13940 ` 27` ballarin@15095 ` 28` ```text {* ``` ballarin@15095 ` 29` ``` Functions with finite support. ``` ballarin@15095 ` 30` ```*} ``` ballarin@15095 ` 31` wenzelm@14666 ` 32` ```locale bound = ``` wenzelm@14666 ` 33` ``` fixes z :: 'a ``` wenzelm@14666 ` 34` ``` and n :: nat ``` wenzelm@14666 ` 35` ``` and f :: "nat => 'a" ``` wenzelm@14666 ` 36` ``` assumes bound: "!!m. n < m \ f m = z" ``` ballarin@13940 ` 37` wenzelm@14666 ` 38` ```declare bound.intro [intro!] ``` wenzelm@14666 ` 39` ``` and bound.bound [dest] ``` ballarin@13940 ` 40` ballarin@13940 ` 41` ```lemma bound_below: ``` wenzelm@14666 ` 42` ``` assumes bound: "bound z m f" and nonzero: "f n \ z" shows "n \ m" ``` ballarin@13940 ` 43` ```proof (rule classical) ``` ballarin@13940 ` 44` ``` assume "~ ?thesis" ``` ballarin@13940 ` 45` ``` then have "m < n" by arith ``` ballarin@13940 ` 46` ``` with bound have "f n = z" .. ``` ballarin@13940 ` 47` ``` with nonzero show ?thesis by contradiction ``` ballarin@13940 ` 48` ```qed ``` ballarin@13940 ` 49` ballarin@13940 ` 50` ```record ('a, 'p) up_ring = "('a, 'p) module" + ``` ballarin@13940 ` 51` ``` monom :: "['a, nat] => 'p" ``` ballarin@13940 ` 52` ``` coeff :: "['p, nat] => 'a" ``` ballarin@13940 ` 53` wenzelm@14651 ` 54` ```constdefs (structure R) ``` ballarin@15095 ` 55` ``` up :: "('a, 'm) ring_scheme => (nat => 'a) set" ``` wenzelm@14651 ` 56` ``` "up R == {f. f \ UNIV -> carrier R & (EX n. bound \ n f)}" ``` ballarin@15095 ` 57` ``` UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring" ``` ballarin@13940 ` 58` ``` "UP R == (| ``` ballarin@13940 ` 59` ``` carrier = up R, ``` wenzelm@14651 ` 60` ``` mult = (%p:up R. %q:up R. %n. \i \ {..n}. p i \ q (n-i)), ``` wenzelm@14651 ` 61` ``` one = (%i. if i=0 then \ else \), ``` wenzelm@14651 ` 62` ``` zero = (%i. \), ``` wenzelm@14651 ` 63` ``` add = (%p:up R. %q:up R. %i. p i \ q i), ``` wenzelm@14651 ` 64` ``` smult = (%a:carrier R. %p:up R. %i. a \ p i), ``` wenzelm@14651 ` 65` ``` monom = (%a:carrier R. %n i. if i=n then a else \), ``` ballarin@13940 ` 66` ``` coeff = (%p:up R. %n. p n) |)" ``` ballarin@13940 ` 67` ballarin@13940 ` 68` ```text {* ``` ballarin@13940 ` 69` ``` Properties of the set of polynomials @{term up}. ``` ballarin@13940 ` 70` ```*} ``` ballarin@13940 ` 71` ballarin@13940 ` 72` ```lemma mem_upI [intro]: ``` ballarin@13940 ` 73` ``` "[| !!n. f n \ carrier R; EX n. bound (zero R) n f |] ==> f \ up R" ``` ballarin@13940 ` 74` ``` by (simp add: up_def Pi_def) ``` ballarin@13940 ` 75` ballarin@13940 ` 76` ```lemma mem_upD [dest]: ``` ballarin@13940 ` 77` ``` "f \ up R ==> f n \ carrier R" ``` ballarin@13940 ` 78` ``` by (simp add: up_def Pi_def) ``` ballarin@13940 ` 79` ballarin@13940 ` 80` ```lemma (in cring) bound_upD [dest]: ``` ballarin@13940 ` 81` ``` "f \ up R ==> EX n. bound \ n f" ``` ballarin@13940 ` 82` ``` by (simp add: up_def) ``` ballarin@13940 ` 83` ballarin@13940 ` 84` ```lemma (in cring) up_one_closed: ``` ballarin@13940 ` 85` ``` "(%n. if n = 0 then \ else \) \ up R" ``` ballarin@13940 ` 86` ``` using up_def by force ``` ballarin@13940 ` 87` ballarin@13940 ` 88` ```lemma (in cring) up_smult_closed: ``` ballarin@13940 ` 89` ``` "[| a \ carrier R; p \ up R |] ==> (%i. a \ p i) \ up R" ``` ballarin@13940 ` 90` ``` by force ``` ballarin@13940 ` 91` ballarin@13940 ` 92` ```lemma (in cring) up_add_closed: ``` ballarin@13940 ` 93` ``` "[| p \ up R; q \ up R |] ==> (%i. p i \ q i) \ up R" ``` ballarin@13940 ` 94` ```proof ``` ballarin@13940 ` 95` ``` fix n ``` ballarin@13940 ` 96` ``` assume "p \ up R" and "q \ up R" ``` ballarin@13940 ` 97` ``` then show "p n \ q n \ carrier R" ``` ballarin@13940 ` 98` ``` by auto ``` ballarin@13940 ` 99` ```next ``` ballarin@13940 ` 100` ``` assume UP: "p \ up R" "q \ up R" ``` ballarin@13940 ` 101` ``` show "EX n. bound \ n (%i. p i \ q i)" ``` ballarin@13940 ` 102` ``` proof - ``` ballarin@13940 ` 103` ``` from UP obtain n where boundn: "bound \ n p" by fast ``` ballarin@13940 ` 104` ``` from UP obtain m where boundm: "bound \ m q" by fast ``` ballarin@13940 ` 105` ``` have "bound \ (max n m) (%i. p i \ q i)" ``` ballarin@13940 ` 106` ``` proof ``` ballarin@13940 ` 107` ``` fix i ``` ballarin@13940 ` 108` ``` assume "max n m < i" ``` ballarin@13940 ` 109` ``` with boundn and boundm and UP show "p i \ q i = \" by fastsimp ``` ballarin@13940 ` 110` ``` qed ``` ballarin@13940 ` 111` ``` then show ?thesis .. ``` ballarin@13940 ` 112` ``` qed ``` ballarin@13940 ` 113` ```qed ``` ballarin@13940 ` 114` ballarin@13940 ` 115` ```lemma (in cring) up_a_inv_closed: ``` ballarin@13940 ` 116` ``` "p \ up R ==> (%i. \ (p i)) \ up R" ``` ballarin@13940 ` 117` ```proof ``` ballarin@13940 ` 118` ``` assume R: "p \ up R" ``` ballarin@13940 ` 119` ``` then obtain n where "bound \ n p" by auto ``` ballarin@13940 ` 120` ``` then have "bound \ n (%i. \ p i)" by auto ``` ballarin@13940 ` 121` ``` then show "EX n. bound \ n (%i. \ p i)" by auto ``` ballarin@13940 ` 122` ```qed auto ``` ballarin@13940 ` 123` ballarin@13940 ` 124` ```lemma (in cring) up_mult_closed: ``` ballarin@13940 ` 125` ``` "[| p \ up R; q \ up R |] ==> ``` wenzelm@14666 ` 126` ``` (%n. \i \ {..n}. p i \ q (n-i)) \ up R" ``` ballarin@13940 ` 127` ```proof ``` ballarin@13940 ` 128` ``` fix n ``` ballarin@13940 ` 129` ``` assume "p \ up R" "q \ up R" ``` wenzelm@14666 ` 130` ``` then show "(\i \ {..n}. p i \ q (n-i)) \ carrier R" ``` ballarin@13940 ` 131` ``` by (simp add: mem_upD funcsetI) ``` ballarin@13940 ` 132` ```next ``` ballarin@13940 ` 133` ``` assume UP: "p \ up R" "q \ up R" ``` wenzelm@14666 ` 134` ``` show "EX n. bound \ n (%n. \i \ {..n}. p i \ q (n-i))" ``` ballarin@13940 ` 135` ``` proof - ``` ballarin@13940 ` 136` ``` from UP obtain n where boundn: "bound \ n p" by fast ``` ballarin@13940 ` 137` ``` from UP obtain m where boundm: "bound \ m q" by fast ``` wenzelm@14666 ` 138` ``` have "bound \ (n + m) (%n. \i \ {..n}. p i \ q (n - i))" ``` ballarin@13940 ` 139` ``` proof ``` wenzelm@14666 ` 140` ``` fix k assume bound: "n + m < k" ``` ballarin@13940 ` 141` ``` { ``` wenzelm@14666 ` 142` ``` fix i ``` wenzelm@14666 ` 143` ``` have "p i \ q (k-i) = \" ``` wenzelm@14666 ` 144` ``` proof (cases "n < i") ``` wenzelm@14666 ` 145` ``` case True ``` wenzelm@14666 ` 146` ``` with boundn have "p i = \" by auto ``` ballarin@13940 ` 147` ``` moreover from UP have "q (k-i) \ carrier R" by auto ``` wenzelm@14666 ` 148` ``` ultimately show ?thesis by simp ``` wenzelm@14666 ` 149` ``` next ``` wenzelm@14666 ` 150` ``` case False ``` wenzelm@14666 ` 151` ``` with bound have "m < k-i" by arith ``` wenzelm@14666 ` 152` ``` with boundm have "q (k-i) = \" by auto ``` wenzelm@14666 ` 153` ``` moreover from UP have "p i \ carrier R" by auto ``` wenzelm@14666 ` 154` ``` ultimately show ?thesis by simp ``` wenzelm@14666 ` 155` ``` qed ``` ballarin@13940 ` 156` ``` } ``` wenzelm@14666 ` 157` ``` then show "(\i \ {..k}. p i \ q (k-i)) = \" ``` wenzelm@14666 ` 158` ``` by (simp add: Pi_def) ``` ballarin@13940 ` 159` ``` qed ``` ballarin@13940 ` 160` ``` then show ?thesis by fast ``` ballarin@13940 ` 161` ``` qed ``` ballarin@13940 ` 162` ```qed ``` ballarin@13940 ` 163` wenzelm@14666 ` 164` ballarin@20318 ` 165` ```subsection {* Effect of Operations on Coefficients *} ``` ballarin@13940 ` 166` ballarin@19783 ` 167` ```locale UP = ``` ballarin@19783 ` 168` ``` fixes R (structure) and P (structure) ``` ballarin@13940 ` 169` ``` defines P_def: "P == UP R" ``` ballarin@13940 ` 170` ballarin@13940 ` 171` ```locale UP_cring = UP + cring R ``` ballarin@13940 ` 172` ballarin@13940 ` 173` ```locale UP_domain = UP_cring + "domain" R ``` ballarin@13940 ` 174` ballarin@13940 ` 175` ```text {* ``` ballarin@15095 ` 176` ``` Temporarily declare @{thm [locale=UP] P_def} as simp rule. ``` ballarin@15095 ` 177` ```*} ``` ballarin@13940 ` 178` ballarin@13940 ` 179` ```declare (in UP) P_def [simp] ``` ballarin@13940 ` 180` ballarin@13940 ` 181` ```lemma (in UP_cring) coeff_monom [simp]: ``` ballarin@13940 ` 182` ``` "a \ carrier R ==> ``` ballarin@13940 ` 183` ``` coeff P (monom P a m) n = (if m=n then a else \)" ``` ballarin@13940 ` 184` ```proof - ``` ballarin@13940 ` 185` ``` assume R: "a \ carrier R" ``` ballarin@13940 ` 186` ``` then have "(%n. if n = m then a else \) \ up R" ``` ballarin@13940 ` 187` ``` using up_def by force ``` ballarin@13940 ` 188` ``` with R show ?thesis by (simp add: UP_def) ``` ballarin@13940 ` 189` ```qed ``` ballarin@13940 ` 190` ballarin@13940 ` 191` ```lemma (in UP_cring) coeff_zero [simp]: ``` ballarin@15095 ` 192` ``` "coeff P \\<^bsub>P\<^esub> n = \" ``` ballarin@13940 ` 193` ``` by (auto simp add: UP_def) ``` ballarin@13940 ` 194` ballarin@13940 ` 195` ```lemma (in UP_cring) coeff_one [simp]: ``` ballarin@15095 ` 196` ``` "coeff P \\<^bsub>P\<^esub> n = (if n=0 then \ else \)" ``` ballarin@13940 ` 197` ``` using up_one_closed by (simp add: UP_def) ``` ballarin@13940 ` 198` ballarin@13940 ` 199` ```lemma (in UP_cring) coeff_smult [simp]: ``` ballarin@13940 ` 200` ``` "[| a \ carrier R; p \ carrier P |] ==> ``` ballarin@15095 ` 201` ``` coeff P (a \\<^bsub>P\<^esub> p) n = a \ coeff P p n" ``` ballarin@13940 ` 202` ``` by (simp add: UP_def up_smult_closed) ``` ballarin@13940 ` 203` ballarin@13940 ` 204` ```lemma (in UP_cring) coeff_add [simp]: ``` ballarin@13940 ` 205` ``` "[| p \ carrier P; q \ carrier P |] ==> ``` ballarin@15095 ` 206` ``` coeff P (p \\<^bsub>P\<^esub> q) n = coeff P p n \ coeff P q n" ``` ballarin@13940 ` 207` ``` by (simp add: UP_def up_add_closed) ``` ballarin@13940 ` 208` ballarin@13940 ` 209` ```lemma (in UP_cring) coeff_mult [simp]: ``` ballarin@13940 ` 210` ``` "[| p \ carrier P; q \ carrier P |] ==> ``` ballarin@15095 ` 211` ``` coeff P (p \\<^bsub>P\<^esub> q) n = (\i \ {..n}. coeff P p i \ coeff P q (n-i))" ``` ballarin@13940 ` 212` ``` by (simp add: UP_def up_mult_closed) ``` ballarin@13940 ` 213` ballarin@13940 ` 214` ```lemma (in UP) up_eqI: ``` ballarin@13940 ` 215` ``` assumes prem: "!!n. coeff P p n = coeff P q n" ``` ballarin@13940 ` 216` ``` and R: "p \ carrier P" "q \ carrier P" ``` ballarin@13940 ` 217` ``` shows "p = q" ``` ballarin@13940 ` 218` ```proof ``` ballarin@13940 ` 219` ``` fix x ``` ballarin@13940 ` 220` ``` from prem and R show "p x = q x" by (simp add: UP_def) ``` ballarin@13940 ` 221` ```qed ``` wenzelm@14666 ` 222` ballarin@20318 ` 223` ballarin@20318 ` 224` ```subsection {* Polynomials Form a Commutative Ring. *} ``` ballarin@13940 ` 225` wenzelm@14666 ` 226` ```text {* Operations are closed over @{term P}. *} ``` ballarin@13940 ` 227` ballarin@13940 ` 228` ```lemma (in UP_cring) UP_mult_closed [simp]: ``` ballarin@15095 ` 229` ``` "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" ``` ballarin@13940 ` 230` ``` by (simp add: UP_def up_mult_closed) ``` ballarin@13940 ` 231` ballarin@13940 ` 232` ```lemma (in UP_cring) UP_one_closed [simp]: ``` ballarin@15095 ` 233` ``` "\\<^bsub>P\<^esub> \ carrier P" ``` ballarin@13940 ` 234` ``` by (simp add: UP_def up_one_closed) ``` ballarin@13940 ` 235` ballarin@13940 ` 236` ```lemma (in UP_cring) UP_zero_closed [intro, simp]: ``` ballarin@15095 ` 237` ``` "\\<^bsub>P\<^esub> \ carrier P" ``` ballarin@13940 ` 238` ``` by (auto simp add: UP_def) ``` ballarin@13940 ` 239` ballarin@13940 ` 240` ```lemma (in UP_cring) UP_a_closed [intro, simp]: ``` ballarin@15095 ` 241` ``` "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" ``` ballarin@13940 ` 242` ``` by (simp add: UP_def up_add_closed) ``` ballarin@13940 ` 243` ballarin@13940 ` 244` ```lemma (in UP_cring) monom_closed [simp]: ``` ballarin@13940 ` 245` ``` "a \ carrier R ==> monom P a n \ carrier P" ``` ballarin@13940 ` 246` ``` by (auto simp add: UP_def up_def Pi_def) ``` ballarin@13940 ` 247` ballarin@13940 ` 248` ```lemma (in UP_cring) UP_smult_closed [simp]: ``` ballarin@15095 ` 249` ``` "[| a \ carrier R; p \ carrier P |] ==> a \\<^bsub>P\<^esub> p \ carrier P" ``` ballarin@13940 ` 250` ``` by (simp add: UP_def up_smult_closed) ``` ballarin@13940 ` 251` ballarin@13940 ` 252` ```lemma (in UP) coeff_closed [simp]: ``` ballarin@13940 ` 253` ``` "p \ carrier P ==> coeff P p n \ carrier R" ``` ballarin@13940 ` 254` ``` by (auto simp add: UP_def) ``` ballarin@13940 ` 255` ballarin@13940 ` 256` ```declare (in UP) P_def [simp del] ``` ballarin@13940 ` 257` ballarin@13940 ` 258` ```text {* Algebraic ring properties *} ``` ballarin@13940 ` 259` ballarin@13940 ` 260` ```lemma (in UP_cring) UP_a_assoc: ``` ballarin@13940 ` 261` ``` assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" ``` ballarin@15095 ` 262` ``` shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" ``` ballarin@13940 ` 263` ``` by (rule up_eqI, simp add: a_assoc R, simp_all add: R) ``` ballarin@13940 ` 264` ballarin@13940 ` 265` ```lemma (in UP_cring) UP_l_zero [simp]: ``` ballarin@13940 ` 266` ``` assumes R: "p \ carrier P" ``` ballarin@15095 ` 267` ``` shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p" ``` ballarin@13940 ` 268` ``` by (rule up_eqI, simp_all add: R) ``` ballarin@13940 ` 269` ballarin@13940 ` 270` ```lemma (in UP_cring) UP_l_neg_ex: ``` ballarin@13940 ` 271` ``` assumes R: "p \ carrier P" ``` ballarin@15095 ` 272` ``` shows "EX q : carrier P. q \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 273` ```proof - ``` ballarin@13940 ` 274` ``` let ?q = "%i. \ (p i)" ``` ballarin@13940 ` 275` ``` from R have closed: "?q \ carrier P" ``` ballarin@13940 ` 276` ``` by (simp add: UP_def P_def up_a_inv_closed) ``` ballarin@13940 ` 277` ``` from R have coeff: "!!n. coeff P ?q n = \ (coeff P p n)" ``` ballarin@13940 ` 278` ``` by (simp add: UP_def P_def up_a_inv_closed) ``` ballarin@13940 ` 279` ``` show ?thesis ``` ballarin@13940 ` 280` ``` proof ``` ballarin@15095 ` 281` ``` show "?q \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 282` ``` by (auto intro!: up_eqI simp add: R closed coeff R.l_neg) ``` ballarin@13940 ` 283` ``` qed (rule closed) ``` ballarin@13940 ` 284` ```qed ``` ballarin@13940 ` 285` ballarin@13940 ` 286` ```lemma (in UP_cring) UP_a_comm: ``` ballarin@13940 ` 287` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@15095 ` 288` ``` shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p" ``` ballarin@13940 ` 289` ``` by (rule up_eqI, simp add: a_comm R, simp_all add: R) ``` ballarin@13940 ` 290` ballarin@13940 ` 291` ```lemma (in UP_cring) UP_m_assoc: ``` ballarin@13940 ` 292` ``` assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" ``` ballarin@15095 ` 293` ``` shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" ``` ballarin@13940 ` 294` ```proof (rule up_eqI) ``` ballarin@13940 ` 295` ``` fix n ``` ballarin@13940 ` 296` ``` { ``` ballarin@13940 ` 297` ``` fix k and a b c :: "nat=>'a" ``` ballarin@13940 ` 298` ``` assume R: "a \ UNIV -> carrier R" "b \ UNIV -> carrier R" ``` ballarin@13940 ` 299` ``` "c \ UNIV -> carrier R" ``` ballarin@13940 ` 300` ``` then have "k <= n ==> ``` wenzelm@14666 ` 301` ``` (\j \ {..k}. (\i \ {..j}. a i \ b (j-i)) \ c (n-j)) = ``` wenzelm@14666 ` 302` ``` (\j \ {..k}. a j \ (\i \ {..k-j}. b i \ c (n-j-i)))" ``` wenzelm@19582 ` 303` ``` (is "_ \ ?eq k") ``` ballarin@13940 ` 304` ``` proof (induct k) ``` ballarin@13940 ` 305` ``` case 0 then show ?case by (simp add: Pi_def m_assoc) ``` ballarin@13940 ` 306` ``` next ``` ballarin@13940 ` 307` ``` case (Suc k) ``` ballarin@13940 ` 308` ``` then have "k <= n" by arith ``` wenzelm@23350 ` 309` ``` from this R have "?eq k" by (rule Suc) ``` ballarin@13940 ` 310` ``` with R show ?case ``` wenzelm@14666 ` 311` ``` by (simp cong: finsum_cong ``` ballarin@13940 ` 312` ``` add: Suc_diff_le Pi_def l_distr r_distr m_assoc) ``` ballarin@13940 ` 313` ``` (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc) ``` ballarin@13940 ` 314` ``` qed ``` ballarin@13940 ` 315` ``` } ``` ballarin@15095 ` 316` ``` with R show "coeff P ((p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r) n = coeff P (p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)) n" ``` ballarin@13940 ` 317` ``` by (simp add: Pi_def) ``` ballarin@13940 ` 318` ```qed (simp_all add: R) ``` ballarin@13940 ` 319` ballarin@13940 ` 320` ```lemma (in UP_cring) UP_l_one [simp]: ``` ballarin@13940 ` 321` ``` assumes R: "p \ carrier P" ``` ballarin@15095 ` 322` ``` shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p" ``` ballarin@13940 ` 323` ```proof (rule up_eqI) ``` ballarin@13940 ` 324` ``` fix n ``` ballarin@15095 ` 325` ``` show "coeff P (\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p) n = coeff P p n" ``` ballarin@13940 ` 326` ``` proof (cases n) ``` ballarin@13940 ` 327` ``` case 0 with R show ?thesis by simp ``` ballarin@13940 ` 328` ``` next ``` ballarin@13940 ` 329` ``` case Suc with R show ?thesis ``` ballarin@13940 ` 330` ``` by (simp del: finsum_Suc add: finsum_Suc2 Pi_def) ``` ballarin@13940 ` 331` ``` qed ``` ballarin@13940 ` 332` ```qed (simp_all add: R) ``` ballarin@13940 ` 333` ballarin@13940 ` 334` ```lemma (in UP_cring) UP_l_distr: ``` ballarin@13940 ` 335` ``` assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" ``` ballarin@15095 ` 336` ``` shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = (p \\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" ``` ballarin@13940 ` 337` ``` by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R) ``` ballarin@13940 ` 338` ballarin@13940 ` 339` ```lemma (in UP_cring) UP_m_comm: ``` ballarin@13940 ` 340` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@15095 ` 341` ``` shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p" ``` ballarin@13940 ` 342` ```proof (rule up_eqI) ``` wenzelm@14666 ` 343` ``` fix n ``` ballarin@13940 ` 344` ``` { ``` ballarin@13940 ` 345` ``` fix k and a b :: "nat=>'a" ``` ballarin@13940 ` 346` ``` assume R: "a \ UNIV -> carrier R" "b \ UNIV -> carrier R" ``` wenzelm@14666 ` 347` ``` then have "k <= n ==> ``` wenzelm@14666 ` 348` ``` (\i \ {..k}. a i \ b (n-i)) = ``` wenzelm@14666 ` 349` ``` (\i \ {..k}. a (k-i) \ b (i+n-k))" ``` wenzelm@19582 ` 350` ``` (is "_ \ ?eq k") ``` ballarin@13940 ` 351` ``` proof (induct k) ``` ballarin@13940 ` 352` ``` case 0 then show ?case by (simp add: Pi_def) ``` ballarin@13940 ` 353` ``` next ``` ballarin@13940 ` 354` ``` case (Suc k) then show ?case ``` paulson@15944 ` 355` ``` by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+ ``` ballarin@13940 ` 356` ``` qed ``` ballarin@13940 ` 357` ``` } ``` ballarin@13940 ` 358` ``` note l = this ``` ballarin@15095 ` 359` ``` from R show "coeff P (p \\<^bsub>P\<^esub> q) n = coeff P (q \\<^bsub>P\<^esub> p) n" ``` ballarin@13940 ` 360` ``` apply (simp add: Pi_def) ``` ballarin@13940 ` 361` ``` apply (subst l) ``` ballarin@13940 ` 362` ``` apply (auto simp add: Pi_def) ``` ballarin@13940 ` 363` ``` apply (simp add: m_comm) ``` ballarin@13940 ` 364` ``` done ``` ballarin@13940 ` 365` ```qed (simp_all add: R) ``` ballarin@13940 ` 366` ballarin@13940 ` 367` ```theorem (in UP_cring) UP_cring: ``` ballarin@13940 ` 368` ``` "cring P" ``` ballarin@13940 ` 369` ``` by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero ``` ballarin@13940 ` 370` ``` UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr) ``` ballarin@13940 ` 371` ballarin@17094 ` 372` ```lemma (in UP_cring) UP_ring: ``` ballarin@17094 ` 373` ``` (* preliminary, ``` ballarin@17094 ` 374` ``` we want "UP_ring R P ==> ring P", not "UP_cring R P ==> ring P" *) ``` ballarin@14399 ` 375` ``` "ring P" ``` ballarin@14399 ` 376` ``` by (auto intro: ring.intro cring.axioms UP_cring) ``` ballarin@14399 ` 377` ballarin@13940 ` 378` ```lemma (in UP_cring) UP_a_inv_closed [intro, simp]: ``` ballarin@15095 ` 379` ``` "p \ carrier P ==> \\<^bsub>P\<^esub> p \ carrier P" ``` ballarin@13940 ` 380` ``` by (rule abelian_group.a_inv_closed ``` ballarin@14399 ` 381` ``` [OF ring.is_abelian_group [OF UP_ring]]) ``` ballarin@13940 ` 382` ballarin@13940 ` 383` ```lemma (in UP_cring) coeff_a_inv [simp]: ``` ballarin@13940 ` 384` ``` assumes R: "p \ carrier P" ``` ballarin@15095 ` 385` ``` shows "coeff P (\\<^bsub>P\<^esub> p) n = \ (coeff P p n)" ``` ballarin@13940 ` 386` ```proof - ``` ballarin@13940 ` 387` ``` from R coeff_closed UP_a_inv_closed have ``` ballarin@15095 ` 388` ``` "coeff P (\\<^bsub>P\<^esub> p) n = \ coeff P p n \ (coeff P p n \ coeff P (\\<^bsub>P\<^esub> p) n)" ``` ballarin@13940 ` 389` ``` by algebra ``` ballarin@13940 ` 390` ``` also from R have "... = \ (coeff P p n)" ``` ballarin@13940 ` 391` ``` by (simp del: coeff_add add: coeff_add [THEN sym] ``` ballarin@14399 ` 392` ``` abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]]) ``` ballarin@13940 ` 393` ``` finally show ?thesis . ``` ballarin@13940 ` 394` ```qed ``` ballarin@13940 ` 395` ballarin@13940 ` 396` ```text {* ``` ballarin@17094 ` 397` ``` Interpretation of lemmas from @{term cring}. Saves lifting 43 ``` ballarin@17094 ` 398` ``` lemmas manually. ``` ballarin@13940 ` 399` ```*} ``` ballarin@13940 ` 400` ballarin@17094 ` 401` ```interpretation UP_cring < cring P ``` ballarin@19984 ` 402` ``` by intro_locales ``` ballarin@19931 ` 403` ``` (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+ ``` ballarin@13940 ` 404` wenzelm@14666 ` 405` ballarin@20318 ` 406` ```subsection {* Polynomials Form an Algebra *} ``` ballarin@13940 ` 407` ballarin@13940 ` 408` ```lemma (in UP_cring) UP_smult_l_distr: ``` ballarin@13940 ` 409` ``` "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==> ``` ballarin@15095 ` 410` ``` (a \ b) \\<^bsub>P\<^esub> p = a \\<^bsub>P\<^esub> p \\<^bsub>P\<^esub> b \\<^bsub>P\<^esub> p" ``` ballarin@13940 ` 411` ``` by (rule up_eqI) (simp_all add: R.l_distr) ``` ballarin@13940 ` 412` ballarin@13940 ` 413` ```lemma (in UP_cring) UP_smult_r_distr: ``` ballarin@13940 ` 414` ``` "[| a \ carrier R; p \ carrier P; q \ carrier P |] ==> ``` ballarin@15095 ` 415` ``` a \\<^bsub>P\<^esub> (p \\<^bsub>P\<^esub> q) = a \\<^bsub>P\<^esub> p \\<^bsub>P\<^esub> a \\<^bsub>P\<^esub> q" ``` ballarin@13940 ` 416` ``` by (rule up_eqI) (simp_all add: R.r_distr) ``` ballarin@13940 ` 417` ballarin@13940 ` 418` ```lemma (in UP_cring) UP_smult_assoc1: ``` ballarin@13940 ` 419` ``` "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==> ``` ballarin@15095 ` 420` ``` (a \ b) \\<^bsub>P\<^esub> p = a \\<^bsub>P\<^esub> (b \\<^bsub>P\<^esub> p)" ``` ballarin@13940 ` 421` ``` by (rule up_eqI) (simp_all add: R.m_assoc) ``` ballarin@13940 ` 422` ballarin@13940 ` 423` ```lemma (in UP_cring) UP_smult_one [simp]: ``` ballarin@15095 ` 424` ``` "p \ carrier P ==> \ \\<^bsub>P\<^esub> p = p" ``` ballarin@13940 ` 425` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 426` ballarin@13940 ` 427` ```lemma (in UP_cring) UP_smult_assoc2: ``` ballarin@13940 ` 428` ``` "[| a \ carrier R; p \ carrier P; q \ carrier P |] ==> ``` ballarin@15095 ` 429` ``` (a \\<^bsub>P\<^esub> p) \\<^bsub>P\<^esub> q = a \\<^bsub>P\<^esub> (p \\<^bsub>P\<^esub> q)" ``` ballarin@13940 ` 430` ``` by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def) ``` ballarin@13940 ` 431` ballarin@13940 ` 432` ```text {* ``` ballarin@17094 ` 433` ``` Interpretation of lemmas from @{term algebra}. ``` ballarin@13940 ` 434` ```*} ``` ballarin@13940 ` 435` ballarin@13940 ` 436` ```lemma (in cring) cring: ``` ballarin@13940 ` 437` ``` "cring R" ``` ballarin@13940 ` 438` ``` by (fast intro: cring.intro prems) ``` ballarin@13940 ` 439` ballarin@13940 ` 440` ```lemma (in UP_cring) UP_algebra: ``` ballarin@13940 ` 441` ``` "algebra R P" ``` ballarin@17094 ` 442` ``` by (auto intro: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr ``` ballarin@13940 ` 443` ``` UP_smult_assoc1 UP_smult_assoc2) ``` ballarin@13940 ` 444` ballarin@17094 ` 445` ```interpretation UP_cring < algebra R P ``` ballarin@19984 ` 446` ``` by intro_locales ``` ballarin@19931 ` 447` ``` (rule module.axioms algebra.axioms UP_algebra)+ ``` ballarin@13940 ` 448` ballarin@13940 ` 449` ballarin@20318 ` 450` ```subsection {* Further Lemmas Involving Monomials *} ``` ballarin@13940 ` 451` ballarin@13940 ` 452` ```lemma (in UP_cring) monom_zero [simp]: ``` ballarin@15095 ` 453` ``` "monom P \ n = \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 454` ``` by (simp add: UP_def P_def) ``` ballarin@13940 ` 455` ballarin@13940 ` 456` ```lemma (in UP_cring) monom_mult_is_smult: ``` ballarin@13940 ` 457` ``` assumes R: "a \ carrier R" "p \ carrier P" ``` ballarin@15095 ` 458` ``` shows "monom P a 0 \\<^bsub>P\<^esub> p = a \\<^bsub>P\<^esub> p" ``` ballarin@13940 ` 459` ```proof (rule up_eqI) ``` ballarin@13940 ` 460` ``` fix n ``` ballarin@15095 ` 461` ``` have "coeff P (p \\<^bsub>P\<^esub> monom P a 0) n = coeff P (a \\<^bsub>P\<^esub> p) n" ``` ballarin@13940 ` 462` ``` proof (cases n) ``` ballarin@13940 ` 463` ``` case 0 with R show ?thesis by (simp add: R.m_comm) ``` ballarin@13940 ` 464` ``` next ``` ballarin@13940 ` 465` ``` case Suc with R show ?thesis ``` ballarin@17094 ` 466` ``` by (simp cong: R.finsum_cong add: R.r_null Pi_def) ``` ballarin@17094 ` 467` ``` (simp add: R.m_comm) ``` ballarin@13940 ` 468` ``` qed ``` ballarin@15095 ` 469` ``` with R show "coeff P (monom P a 0 \\<^bsub>P\<^esub> p) n = coeff P (a \\<^bsub>P\<^esub> p) n" ``` ballarin@13940 ` 470` ``` by (simp add: UP_m_comm) ``` ballarin@13940 ` 471` ```qed (simp_all add: R) ``` ballarin@13940 ` 472` ballarin@13940 ` 473` ```lemma (in UP_cring) monom_add [simp]: ``` ballarin@13940 ` 474` ``` "[| a \ carrier R; b \ carrier R |] ==> ``` ballarin@15095 ` 475` ``` monom P (a \ b) n = monom P a n \\<^bsub>P\<^esub> monom P b n" ``` ballarin@13940 ` 476` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 477` ballarin@13940 ` 478` ```lemma (in UP_cring) monom_one_Suc: ``` ballarin@15095 ` 479` ``` "monom P \ (Suc n) = monom P \ n \\<^bsub>P\<^esub> monom P \ 1" ``` ballarin@13940 ` 480` ```proof (rule up_eqI) ``` ballarin@13940 ` 481` ``` fix k ``` ballarin@15095 ` 482` ``` show "coeff P (monom P \ (Suc n)) k = coeff P (monom P \ n \\<^bsub>P\<^esub> monom P \ 1) k" ``` ballarin@13940 ` 483` ``` proof (cases "k = Suc n") ``` ballarin@13940 ` 484` ``` case True show ?thesis ``` ballarin@13940 ` 485` ``` proof - ``` wenzelm@14666 ` 486` ``` from True have less_add_diff: ``` wenzelm@14666 ` 487` ``` "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith ``` ballarin@13940 ` 488` ``` from True have "coeff P (monom P \ (Suc n)) k = \" by simp ``` ballarin@13940 ` 489` ``` also from True ``` nipkow@15045 ` 490` ``` have "... = (\i \ {.. {n}. coeff P (monom P \ n) i \ ``` wenzelm@14666 ` 491` ``` coeff P (monom P \ 1) (k - i))" ``` ballarin@17094 ` 492` ``` by (simp cong: R.finsum_cong add: Pi_def) ``` wenzelm@14666 ` 493` ``` also have "... = (\i \ {..n}. coeff P (monom P \ n) i \ ``` wenzelm@14666 ` 494` ``` coeff P (monom P \ 1) (k - i))" ``` wenzelm@14666 ` 495` ``` by (simp only: ivl_disj_un_singleton) ``` ballarin@15095 ` 496` ``` also from True ``` ballarin@15095 ` 497` ``` have "... = (\i \ {..n} \ {n<..k}. coeff P (monom P \ n) i \ ``` wenzelm@14666 ` 498` ``` coeff P (monom P \ 1) (k - i))" ``` ballarin@17094 ` 499` ``` by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one ``` wenzelm@14666 ` 500` ``` order_less_imp_not_eq Pi_def) ``` ballarin@15095 ` 501` ``` also from True have "... = coeff P (monom P \ n \\<^bsub>P\<^esub> monom P \ 1) k" ``` wenzelm@14666 ` 502` ``` by (simp add: ivl_disj_un_one) ``` ballarin@13940 ` 503` ``` finally show ?thesis . ``` ballarin@13940 ` 504` ``` qed ``` ballarin@13940 ` 505` ``` next ``` ballarin@13940 ` 506` ``` case False ``` ballarin@13940 ` 507` ``` note neq = False ``` ballarin@13940 ` 508` ``` let ?s = ``` wenzelm@14666 ` 509` ``` "\i. (if n = i then \ else \) \ (if Suc 0 = k - i then \ else \)" ``` ballarin@13940 ` 510` ``` from neq have "coeff P (monom P \ (Suc n)) k = \" by simp ``` wenzelm@14666 ` 511` ``` also have "... = (\i \ {..k}. ?s i)" ``` ballarin@13940 ` 512` ``` proof - ``` ballarin@15095 ` 513` ``` have f1: "(\i \ {.." ``` ballarin@17094 ` 514` ``` by (simp cong: R.finsum_cong add: Pi_def) ``` wenzelm@14666 ` 515` ``` from neq have f2: "(\i \ {n}. ?s i) = \" ``` webertj@20432 ` 516` ``` by (simp cong: R.finsum_cong add: Pi_def) arith ``` nipkow@15045 ` 517` ``` have f3: "n < k ==> (\i \ {n<..k}. ?s i) = \" ``` ballarin@17094 ` 518` ``` by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def) ``` ballarin@13940 ` 519` ``` show ?thesis ``` ballarin@13940 ` 520` ``` proof (cases "k < n") ``` ballarin@17094 ` 521` ``` case True then show ?thesis by (simp cong: R.finsum_cong add: Pi_def) ``` ballarin@13940 ` 522` ``` next ``` wenzelm@14666 ` 523` ``` case False then have n_le_k: "n <= k" by arith ``` wenzelm@14666 ` 524` ``` show ?thesis ``` wenzelm@14666 ` 525` ``` proof (cases "n = k") ``` wenzelm@14666 ` 526` ``` case True ``` nipkow@15045 ` 527` ``` then have "\ = (\i \ {.. {n}. ?s i)" ``` ballarin@17094 ` 528` ``` by (simp cong: R.finsum_cong add: ivl_disj_int_singleton Pi_def) ``` wenzelm@14666 ` 529` ``` also from True have "... = (\i \ {..k}. ?s i)" ``` wenzelm@14666 ` 530` ``` by (simp only: ivl_disj_un_singleton) ``` wenzelm@14666 ` 531` ``` finally show ?thesis . ``` wenzelm@14666 ` 532` ``` next ``` wenzelm@14666 ` 533` ``` case False with n_le_k have n_less_k: "n < k" by arith ``` nipkow@15045 ` 534` ``` with neq have "\ = (\i \ {.. {n}. ?s i)" ``` ballarin@17094 ` 535` ``` by (simp add: R.finsum_Un_disjoint f1 f2 ``` wenzelm@14666 ` 536` ``` ivl_disj_int_singleton Pi_def del: Un_insert_right) ``` wenzelm@14666 ` 537` ``` also have "... = (\i \ {..n}. ?s i)" ``` wenzelm@14666 ` 538` ``` by (simp only: ivl_disj_un_singleton) ``` nipkow@15045 ` 539` ``` also from n_less_k neq have "... = (\i \ {..n} \ {n<..k}. ?s i)" ``` ballarin@17094 ` 540` ``` by (simp add: R.finsum_Un_disjoint f3 ivl_disj_int_one Pi_def) ``` wenzelm@14666 ` 541` ``` also from n_less_k have "... = (\i \ {..k}. ?s i)" ``` wenzelm@14666 ` 542` ``` by (simp only: ivl_disj_un_one) ``` wenzelm@14666 ` 543` ``` finally show ?thesis . ``` wenzelm@14666 ` 544` ``` qed ``` ballarin@13940 ` 545` ``` qed ``` ballarin@13940 ` 546` ``` qed ``` ballarin@15095 ` 547` ``` also have "... = coeff P (monom P \ n \\<^bsub>P\<^esub> monom P \ 1) k" by simp ``` ballarin@13940 ` 548` ``` finally show ?thesis . ``` ballarin@13940 ` 549` ``` qed ``` ballarin@13940 ` 550` ```qed (simp_all) ``` ballarin@13940 ` 551` ballarin@13940 ` 552` ```lemma (in UP_cring) monom_mult_smult: ``` ballarin@15095 ` 553` ``` "[| a \ carrier R; b \ carrier R |] ==> monom P (a \ b) n = a \\<^bsub>P\<^esub> monom P b n" ``` ballarin@13940 ` 554` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 555` ballarin@13940 ` 556` ```lemma (in UP_cring) monom_one [simp]: ``` ballarin@15095 ` 557` ``` "monom P \ 0 = \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 558` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 559` ballarin@13940 ` 560` ```lemma (in UP_cring) monom_one_mult: ``` ballarin@15095 ` 561` ``` "monom P \ (n + m) = monom P \ n \\<^bsub>P\<^esub> monom P \ m" ``` ballarin@13940 ` 562` ```proof (induct n) ``` ballarin@13940 ` 563` ``` case 0 show ?case by simp ``` ballarin@13940 ` 564` ```next ``` ballarin@13940 ` 565` ``` case Suc then show ?case ``` ballarin@17094 ` 566` ``` by (simp only: add_Suc monom_one_Suc) (simp add: P.m_ac) ``` ballarin@13940 ` 567` ```qed ``` ballarin@13940 ` 568` ballarin@13940 ` 569` ```lemma (in UP_cring) monom_mult [simp]: ``` ballarin@13940 ` 570` ``` assumes R: "a \ carrier R" "b \ carrier R" ``` ballarin@15095 ` 571` ``` shows "monom P (a \ b) (n + m) = monom P a n \\<^bsub>P\<^esub> monom P b m" ``` ballarin@13940 ` 572` ```proof - ``` ballarin@13940 ` 573` ``` from R have "monom P (a \ b) (n + m) = monom P (a \ b \ \) (n + m)" by simp ``` ballarin@15095 ` 574` ``` also from R have "... = a \ b \\<^bsub>P\<^esub> monom P \ (n + m)" ``` ballarin@17094 ` 575` ``` by (simp add: monom_mult_smult del: R.r_one) ``` ballarin@15095 ` 576` ``` also have "... = a \ b \\<^bsub>P\<^esub> (monom P \ n \\<^bsub>P\<^esub> monom P \ m)" ``` ballarin@13940 ` 577` ``` by (simp only: monom_one_mult) ``` ballarin@15095 ` 578` ``` also from R have "... = a \\<^bsub>P\<^esub> (b \\<^bsub>P\<^esub> (monom P \ n \\<^bsub>P\<^esub> monom P \ m))" ``` ballarin@13940 ` 579` ``` by (simp add: UP_smult_assoc1) ``` ballarin@15095 ` 580` ``` also from R have "... = a \\<^bsub>P\<^esub> (b \\<^bsub>P\<^esub> (monom P \ m \\<^bsub>P\<^esub> monom P \ n))" ``` ballarin@17094 ` 581` ``` by (simp add: P.m_comm) ``` ballarin@15095 ` 582` ``` also from R have "... = a \\<^bsub>P\<^esub> ((b \\<^bsub>P\<^esub> monom P \ m) \\<^bsub>P\<^esub> monom P \ n)" ``` ballarin@13940 ` 583` ``` by (simp add: UP_smult_assoc2) ``` ballarin@15095 ` 584` ``` also from R have "... = a \\<^bsub>P\<^esub> (monom P \ n \\<^bsub>P\<^esub> (b \\<^bsub>P\<^esub> monom P \ m))" ``` ballarin@17094 ` 585` ``` by (simp add: P.m_comm) ``` ballarin@15095 ` 586` ``` also from R have "... = (a \\<^bsub>P\<^esub> monom P \ n) \\<^bsub>P\<^esub> (b \\<^bsub>P\<^esub> monom P \ m)" ``` ballarin@13940 ` 587` ``` by (simp add: UP_smult_assoc2) ``` ballarin@15095 ` 588` ``` also from R have "... = monom P (a \ \) n \\<^bsub>P\<^esub> monom P (b \ \) m" ``` ballarin@17094 ` 589` ``` by (simp add: monom_mult_smult del: R.r_one) ``` ballarin@15095 ` 590` ``` also from R have "... = monom P a n \\<^bsub>P\<^esub> monom P b m" by simp ``` ballarin@13940 ` 591` ``` finally show ?thesis . ``` ballarin@13940 ` 592` ```qed ``` ballarin@13940 ` 593` ballarin@13940 ` 594` ```lemma (in UP_cring) monom_a_inv [simp]: ``` ballarin@15095 ` 595` ``` "a \ carrier R ==> monom P (\ a) n = \\<^bsub>P\<^esub> monom P a n" ``` ballarin@13940 ` 596` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 597` ballarin@13940 ` 598` ```lemma (in UP_cring) monom_inj: ``` ballarin@13940 ` 599` ``` "inj_on (%a. monom P a n) (carrier R)" ``` ballarin@13940 ` 600` ```proof (rule inj_onI) ``` ballarin@13940 ` 601` ``` fix x y ``` ballarin@13940 ` 602` ``` assume R: "x \ carrier R" "y \ carrier R" and eq: "monom P x n = monom P y n" ``` ballarin@13940 ` 603` ``` then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp ``` ballarin@13940 ` 604` ``` with R show "x = y" by simp ``` ballarin@13940 ` 605` ```qed ``` ballarin@13940 ` 606` ballarin@17094 ` 607` ballarin@20318 ` 608` ```subsection {* The Degree Function *} ``` ballarin@13940 ` 609` wenzelm@14651 ` 610` ```constdefs (structure R) ``` ballarin@15095 ` 611` ``` deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat" ``` wenzelm@14651 ` 612` ``` "deg R p == LEAST n. bound \ n (coeff (UP R) p)" ``` ballarin@13940 ` 613` ballarin@13940 ` 614` ```lemma (in UP_cring) deg_aboveI: ``` wenzelm@14666 ` 615` ``` "[| (!!m. n < m ==> coeff P p m = \); p \ carrier P |] ==> deg R p <= n" ``` ballarin@13940 ` 616` ``` by (unfold deg_def P_def) (fast intro: Least_le) ``` ballarin@15095 ` 617` ballarin@13940 ` 618` ```(* ``` ballarin@13940 ` 619` ```lemma coeff_bound_ex: "EX n. bound n (coeff p)" ``` ballarin@13940 ` 620` ```proof - ``` ballarin@13940 ` 621` ``` have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) ``` ballarin@13940 ` 622` ``` then obtain n where "bound n (coeff p)" by (unfold UP_def) fast ``` ballarin@13940 ` 623` ``` then show ?thesis .. ``` ballarin@13940 ` 624` ```qed ``` wenzelm@14666 ` 625` ballarin@13940 ` 626` ```lemma bound_coeff_obtain: ``` ballarin@13940 ` 627` ``` assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P" ``` ballarin@13940 ` 628` ```proof - ``` ballarin@13940 ` 629` ``` have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) ``` ballarin@13940 ` 630` ``` then obtain n where "bound n (coeff p)" by (unfold UP_def) fast ``` ballarin@13940 ` 631` ``` with prem show P . ``` ballarin@13940 ` 632` ```qed ``` ballarin@13940 ` 633` ```*) ``` ballarin@15095 ` 634` ballarin@13940 ` 635` ```lemma (in UP_cring) deg_aboveD: ``` wenzelm@23350 ` 636` ``` assumes "deg R p < m" and "p \ carrier P" ``` wenzelm@23350 ` 637` ``` shows "coeff P p m = \" ``` ballarin@13940 ` 638` ```proof - ``` wenzelm@23350 ` 639` ``` from `p \ carrier P` obtain n where "bound \ n (coeff P p)" ``` ballarin@13940 ` 640` ``` by (auto simp add: UP_def P_def) ``` ballarin@13940 ` 641` ``` then have "bound \ (deg R p) (coeff P p)" ``` ballarin@13940 ` 642` ``` by (auto simp: deg_def P_def dest: LeastI) ``` wenzelm@23350 ` 643` ``` from this and `deg R p < m` show ?thesis .. ``` ballarin@13940 ` 644` ```qed ``` ballarin@13940 ` 645` ballarin@13940 ` 646` ```lemma (in UP_cring) deg_belowI: ``` ballarin@13940 ` 647` ``` assumes non_zero: "n ~= 0 ==> coeff P p n ~= \" ``` ballarin@13940 ` 648` ``` and R: "p \ carrier P" ``` ballarin@13940 ` 649` ``` shows "n <= deg R p" ``` wenzelm@14666 ` 650` ```-- {* Logically, this is a slightly stronger version of ``` ballarin@15095 ` 651` ``` @{thm [source] deg_aboveD} *} ``` ballarin@13940 ` 652` ```proof (cases "n=0") ``` ballarin@13940 ` 653` ``` case True then show ?thesis by simp ``` ballarin@13940 ` 654` ```next ``` ballarin@13940 ` 655` ``` case False then have "coeff P p n ~= \" by (rule non_zero) ``` ballarin@13940 ` 656` ``` then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R) ``` ballarin@13940 ` 657` ``` then show ?thesis by arith ``` ballarin@13940 ` 658` ```qed ``` ballarin@13940 ` 659` ballarin@13940 ` 660` ```lemma (in UP_cring) lcoeff_nonzero_deg: ``` ballarin@13940 ` 661` ``` assumes deg: "deg R p ~= 0" and R: "p \ carrier P" ``` ballarin@13940 ` 662` ``` shows "coeff P p (deg R p) ~= \" ``` ballarin@13940 ` 663` ```proof - ``` ballarin@13940 ` 664` ``` from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \" ``` ballarin@13940 ` 665` ``` proof - ``` ballarin@13940 ` 666` ``` have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)" ``` ballarin@13940 ` 667` ``` by arith ``` ballarin@15095 ` 668` ```(* TODO: why does simplification below not work with "1" *) ``` ballarin@13940 ` 669` ``` from deg have "deg R p - 1 < (LEAST n. bound \ n (coeff P p))" ``` ballarin@13940 ` 670` ``` by (unfold deg_def P_def) arith ``` ballarin@13940 ` 671` ``` then have "~ bound \ (deg R p - 1) (coeff P p)" by (rule not_less_Least) ``` ballarin@13940 ` 672` ``` then have "EX m. deg R p - 1 < m & coeff P p m ~= \" ``` ballarin@13940 ` 673` ``` by (unfold bound_def) fast ``` ballarin@13940 ` 674` ``` then have "EX m. deg R p <= m & coeff P p m ~= \" by (simp add: deg minus) ``` wenzelm@23350 ` 675` ``` then show ?thesis by (auto intro: that) ``` ballarin@13940 ` 676` ``` qed ``` ballarin@13940 ` 677` ``` with deg_belowI R have "deg R p = m" by fastsimp ``` ballarin@13940 ` 678` ``` with m_coeff show ?thesis by simp ``` ballarin@13940 ` 679` ```qed ``` ballarin@13940 ` 680` ballarin@13940 ` 681` ```lemma (in UP_cring) lcoeff_nonzero_nonzero: ``` ballarin@15095 ` 682` ``` assumes deg: "deg R p = 0" and nonzero: "p ~= \\<^bsub>P\<^esub>" and R: "p \ carrier P" ``` ballarin@13940 ` 683` ``` shows "coeff P p 0 ~= \" ``` ballarin@13940 ` 684` ```proof - ``` ballarin@13940 ` 685` ``` have "EX m. coeff P p m ~= \" ``` ballarin@13940 ` 686` ``` proof (rule classical) ``` ballarin@13940 ` 687` ``` assume "~ ?thesis" ``` ballarin@15095 ` 688` ``` with R have "p = \\<^bsub>P\<^esub>" by (auto intro: up_eqI) ``` ballarin@13940 ` 689` ``` with nonzero show ?thesis by contradiction ``` ballarin@13940 ` 690` ``` qed ``` ballarin@13940 ` 691` ``` then obtain m where coeff: "coeff P p m ~= \" .. ``` wenzelm@23350 ` 692` ``` from this and R have "m <= deg R p" by (rule deg_belowI) ``` ballarin@13940 ` 693` ``` then have "m = 0" by (simp add: deg) ``` ballarin@13940 ` 694` ``` with coeff show ?thesis by simp ``` ballarin@13940 ` 695` ```qed ``` ballarin@13940 ` 696` ballarin@13940 ` 697` ```lemma (in UP_cring) lcoeff_nonzero: ``` ballarin@15095 ` 698` ``` assumes neq: "p ~= \\<^bsub>P\<^esub>" and R: "p \ carrier P" ``` ballarin@13940 ` 699` ``` shows "coeff P p (deg R p) ~= \" ``` ballarin@13940 ` 700` ```proof (cases "deg R p = 0") ``` ballarin@13940 ` 701` ``` case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero) ``` ballarin@13940 ` 702` ```next ``` ballarin@13940 ` 703` ``` case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg) ``` ballarin@13940 ` 704` ```qed ``` ballarin@13940 ` 705` ballarin@13940 ` 706` ```lemma (in UP_cring) deg_eqI: ``` ballarin@13940 ` 707` ``` "[| !!m. n < m ==> coeff P p m = \; ``` ballarin@13940 ` 708` ``` !!n. n ~= 0 ==> coeff P p n ~= \; p \ carrier P |] ==> deg R p = n" ``` ballarin@13940 ` 709` ```by (fast intro: le_anti_sym deg_aboveI deg_belowI) ``` ballarin@13940 ` 710` ballarin@17094 ` 711` ```text {* Degree and polynomial operations *} ``` ballarin@13940 ` 712` ballarin@13940 ` 713` ```lemma (in UP_cring) deg_add [simp]: ``` ballarin@13940 ` 714` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@15095 ` 715` ``` shows "deg R (p \\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)" ``` ballarin@13940 ` 716` ```proof (cases "deg R p <= deg R q") ``` ballarin@13940 ` 717` ``` case True show ?thesis ``` wenzelm@14666 ` 718` ``` by (rule deg_aboveI) (simp_all add: True R deg_aboveD) ``` ballarin@13940 ` 719` ```next ``` ballarin@13940 ` 720` ``` case False show ?thesis ``` ballarin@13940 ` 721` ``` by (rule deg_aboveI) (simp_all add: False R deg_aboveD) ``` ballarin@13940 ` 722` ```qed ``` ballarin@13940 ` 723` ballarin@13940 ` 724` ```lemma (in UP_cring) deg_monom_le: ``` ballarin@13940 ` 725` ``` "a \ carrier R ==> deg R (monom P a n) <= n" ``` ballarin@13940 ` 726` ``` by (intro deg_aboveI) simp_all ``` ballarin@13940 ` 727` ballarin@13940 ` 728` ```lemma (in UP_cring) deg_monom [simp]: ``` ballarin@13940 ` 729` ``` "[| a ~= \; a \ carrier R |] ==> deg R (monom P a n) = n" ``` ballarin@13940 ` 730` ``` by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) ``` ballarin@13940 ` 731` ballarin@13940 ` 732` ```lemma (in UP_cring) deg_const [simp]: ``` ballarin@13940 ` 733` ``` assumes R: "a \ carrier R" shows "deg R (monom P a 0) = 0" ``` ballarin@13940 ` 734` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 735` ``` show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R) ``` ballarin@13940 ` 736` ```next ``` ballarin@13940 ` 737` ``` show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R) ``` ballarin@13940 ` 738` ```qed ``` ballarin@13940 ` 739` ballarin@13940 ` 740` ```lemma (in UP_cring) deg_zero [simp]: ``` ballarin@15095 ` 741` ``` "deg R \\<^bsub>P\<^esub> = 0" ``` ballarin@13940 ` 742` ```proof (rule le_anti_sym) ``` ballarin@15095 ` 743` ``` show "deg R \\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all ``` ballarin@13940 ` 744` ```next ``` ballarin@15095 ` 745` ``` show "0 <= deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all ``` ballarin@13940 ` 746` ```qed ``` ballarin@13940 ` 747` ballarin@13940 ` 748` ```lemma (in UP_cring) deg_one [simp]: ``` ballarin@15095 ` 749` ``` "deg R \\<^bsub>P\<^esub> = 0" ``` ballarin@13940 ` 750` ```proof (rule le_anti_sym) ``` ballarin@15095 ` 751` ``` show "deg R \\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all ``` ballarin@13940 ` 752` ```next ``` ballarin@15095 ` 753` ``` show "0 <= deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all ``` ballarin@13940 ` 754` ```qed ``` ballarin@13940 ` 755` ballarin@13940 ` 756` ```lemma (in UP_cring) deg_uminus [simp]: ``` ballarin@15095 ` 757` ``` assumes R: "p \ carrier P" shows "deg R (\\<^bsub>P\<^esub> p) = deg R p" ``` ballarin@13940 ` 758` ```proof (rule le_anti_sym) ``` ballarin@15095 ` 759` ``` show "deg R (\\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R) ``` ballarin@13940 ` 760` ```next ``` ballarin@15095 ` 761` ``` show "deg R p <= deg R (\\<^bsub>P\<^esub> p)" ``` ballarin@13940 ` 762` ``` by (simp add: deg_belowI lcoeff_nonzero_deg ``` ballarin@17094 ` 763` ``` inj_on_iff [OF R.a_inv_inj, of _ "\", simplified] R) ``` ballarin@13940 ` 764` ```qed ``` ballarin@13940 ` 765` ballarin@13940 ` 766` ```lemma (in UP_domain) deg_smult_ring: ``` ballarin@13940 ` 767` ``` "[| a \ carrier R; p \ carrier P |] ==> ``` ballarin@15095 ` 768` ``` deg R (a \\<^bsub>P\<^esub> p) <= (if a = \ then 0 else deg R p)" ``` ballarin@13940 ` 769` ``` by (cases "a = \") (simp add: deg_aboveI deg_aboveD)+ ``` ballarin@13940 ` 770` ballarin@13940 ` 771` ```lemma (in UP_domain) deg_smult [simp]: ``` ballarin@13940 ` 772` ``` assumes R: "a \ carrier R" "p \ carrier P" ``` ballarin@15095 ` 773` ``` shows "deg R (a \\<^bsub>P\<^esub> p) = (if a = \ then 0 else deg R p)" ``` ballarin@13940 ` 774` ```proof (rule le_anti_sym) ``` ballarin@15095 ` 775` ``` show "deg R (a \\<^bsub>P\<^esub> p) <= (if a = \ then 0 else deg R p)" ``` wenzelm@23350 ` 776` ``` using R by (rule deg_smult_ring) ``` ballarin@13940 ` 777` ```next ``` ballarin@15095 ` 778` ``` show "(if a = \ then 0 else deg R p) <= deg R (a \\<^bsub>P\<^esub> p)" ``` ballarin@13940 ` 779` ``` proof (cases "a = \") ``` ballarin@13940 ` 780` ``` qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R) ``` ballarin@13940 ` 781` ```qed ``` ballarin@13940 ` 782` ballarin@13940 ` 783` ```lemma (in UP_cring) deg_mult_cring: ``` ballarin@13940 ` 784` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@15095 ` 785` ``` shows "deg R (p \\<^bsub>P\<^esub> q) <= deg R p + deg R q" ``` ballarin@13940 ` 786` ```proof (rule deg_aboveI) ``` ballarin@13940 ` 787` ``` fix m ``` ballarin@13940 ` 788` ``` assume boundm: "deg R p + deg R q < m" ``` ballarin@13940 ` 789` ``` { ``` ballarin@13940 ` 790` ``` fix k i ``` ballarin@13940 ` 791` ``` assume boundk: "deg R p + deg R q < k" ``` ballarin@13940 ` 792` ``` then have "coeff P p i \ coeff P q (k - i) = \" ``` ballarin@13940 ` 793` ``` proof (cases "deg R p < i") ``` ballarin@13940 ` 794` ``` case True then show ?thesis by (simp add: deg_aboveD R) ``` ballarin@13940 ` 795` ``` next ``` ballarin@13940 ` 796` ``` case False with boundk have "deg R q < k - i" by arith ``` ballarin@13940 ` 797` ``` then show ?thesis by (simp add: deg_aboveD R) ``` ballarin@13940 ` 798` ``` qed ``` ballarin@13940 ` 799` ``` } ``` ballarin@15095 ` 800` ``` with boundm R show "coeff P (p \\<^bsub>P\<^esub> q) m = \" by simp ``` ballarin@13940 ` 801` ```qed (simp add: R) ``` ballarin@13940 ` 802` ballarin@13940 ` 803` ```lemma (in UP_domain) deg_mult [simp]: ``` ballarin@15095 ` 804` ``` "[| p ~= \\<^bsub>P\<^esub>; q ~= \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> ``` ballarin@15095 ` 805` ``` deg R (p \\<^bsub>P\<^esub> q) = deg R p + deg R q" ``` ballarin@13940 ` 806` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 807` ``` assume "p \ carrier P" " q \ carrier P" ``` wenzelm@23350 ` 808` ``` then show "deg R (p \\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring) ``` ballarin@13940 ` 809` ```next ``` ballarin@13940 ` 810` ``` let ?s = "(%i. coeff P p i \ coeff P q (deg R p + deg R q - i))" ``` ballarin@15095 ` 811` ``` assume R: "p \ carrier P" "q \ carrier P" and nz: "p ~= \\<^bsub>P\<^esub>" "q ~= \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 812` ``` have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith ``` ballarin@15095 ` 813` ``` show "deg R p + deg R q <= deg R (p \\<^bsub>P\<^esub> q)" ``` ballarin@13940 ` 814` ``` proof (rule deg_belowI, simp add: R) ``` ballarin@15095 ` 815` ``` have "(\i \ {.. deg R p + deg R q}. ?s i) ``` ballarin@15095 ` 816` ``` = (\i \ {..< deg R p} \ {deg R p .. deg R p + deg R q}. ?s i)" ``` ballarin@13940 ` 817` ``` by (simp only: ivl_disj_un_one) ``` ballarin@15095 ` 818` ``` also have "... = (\i \ {deg R p .. deg R p + deg R q}. ?s i)" ``` ballarin@17094 ` 819` ``` by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one ``` ballarin@13940 ` 820` ``` deg_aboveD less_add_diff R Pi_def) ``` ballarin@15095 ` 821` ``` also have "...= (\i \ {deg R p} \ {deg R p <.. deg R p + deg R q}. ?s i)" ``` ballarin@13940 ` 822` ``` by (simp only: ivl_disj_un_singleton) ``` wenzelm@14666 ` 823` ``` also have "... = coeff P p (deg R p) \ coeff P q (deg R q)" ``` ballarin@17094 ` 824` ``` by (simp cong: R.finsum_cong ``` ballarin@17094 ` 825` ``` add: ivl_disj_int_singleton deg_aboveD R Pi_def) ``` ballarin@15095 ` 826` ``` finally have "(\i \ {.. deg R p + deg R q}. ?s i) ``` ballarin@13940 ` 827` ``` = coeff P p (deg R p) \ coeff P q (deg R q)" . ``` ballarin@15095 ` 828` ``` with nz show "(\i \ {.. deg R p + deg R q}. ?s i) ~= \" ``` ballarin@13940 ` 829` ``` by (simp add: integral_iff lcoeff_nonzero R) ``` ballarin@13940 ` 830` ``` qed (simp add: R) ``` ballarin@13940 ` 831` ``` qed ``` ballarin@13940 ` 832` ballarin@13940 ` 833` ```lemma (in UP_cring) coeff_finsum: ``` ballarin@13940 ` 834` ``` assumes fin: "finite A" ``` ballarin@13940 ` 835` ``` shows "p \ A -> carrier P ==> ``` ballarin@15095 ` 836` ``` coeff P (finsum P p A) k = (\i \ A. coeff P (p i) k)" ``` ballarin@13940 ` 837` ``` using fin by induct (auto simp: Pi_def) ``` ballarin@13940 ` 838` ballarin@13940 ` 839` ```lemma (in UP_cring) up_repr: ``` ballarin@13940 ` 840` ``` assumes R: "p \ carrier P" ``` ballarin@15095 ` 841` ``` shows "(\\<^bsub>P\<^esub> i \ {..deg R p}. monom P (coeff P p i) i) = p" ``` ballarin@13940 ` 842` ```proof (rule up_eqI) ``` ballarin@13940 ` 843` ``` let ?s = "(%i. monom P (coeff P p i) i)" ``` ballarin@13940 ` 844` ``` fix k ``` ballarin@13940 ` 845` ``` from R have RR: "!!i. (if i = k then coeff P p i else \) \ carrier R" ``` ballarin@13940 ` 846` ``` by simp ``` ballarin@15095 ` 847` ``` show "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k = coeff P p k" ``` ballarin@13940 ` 848` ``` proof (cases "k <= deg R p") ``` ballarin@13940 ` 849` ``` case True ``` ballarin@15095 ` 850` ``` hence "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k = ``` ballarin@15095 ` 851` ``` coeff P (\\<^bsub>P\<^esub> i \ {..k} \ {k<..deg R p}. ?s i) k" ``` ballarin@13940 ` 852` ``` by (simp only: ivl_disj_un_one) ``` ballarin@13940 ` 853` ``` also from True ``` ballarin@15095 ` 854` ``` have "... = coeff P (\\<^bsub>P\<^esub> i \ {..k}. ?s i) k" ``` ballarin@17094 ` 855` ``` by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ``` wenzelm@14666 ` 856` ``` ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def) ``` ballarin@13940 ` 857` ``` also ``` ballarin@15095 ` 858` ``` have "... = coeff P (\\<^bsub>P\<^esub> i \ {.. {k}. ?s i) k" ``` ballarin@13940 ` 859` ``` by (simp only: ivl_disj_un_singleton) ``` ballarin@13940 ` 860` ``` also have "... = coeff P p k" ``` ballarin@17094 ` 861` ``` by (simp cong: R.finsum_cong ``` ballarin@17094 ` 862` ``` add: ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def) ``` ballarin@13940 ` 863` ``` finally show ?thesis . ``` ballarin@13940 ` 864` ``` next ``` ballarin@13940 ` 865` ``` case False ``` ballarin@15095 ` 866` ``` hence "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k = ``` ballarin@15095 ` 867` ``` coeff P (\\<^bsub>P\<^esub> i \ {.. {deg R p}. ?s i) k" ``` ballarin@13940 ` 868` ``` by (simp only: ivl_disj_un_singleton) ``` ballarin@13940 ` 869` ``` also from False have "... = coeff P p k" ``` ballarin@17094 ` 870` ``` by (simp cong: R.finsum_cong ``` ballarin@17094 ` 871` ``` add: ivl_disj_int_singleton coeff_finsum deg_aboveD R Pi_def) ``` ballarin@13940 ` 872` ``` finally show ?thesis . ``` ballarin@13940 ` 873` ``` qed ``` ballarin@13940 ` 874` ```qed (simp_all add: R Pi_def) ``` ballarin@13940 ` 875` ballarin@13940 ` 876` ```lemma (in UP_cring) up_repr_le: ``` ballarin@13940 ` 877` ``` "[| deg R p <= n; p \ carrier P |] ==> ``` ballarin@15095 ` 878` ``` (\\<^bsub>P\<^esub> i \ {..n}. monom P (coeff P p i) i) = p" ``` ballarin@13940 ` 879` ```proof - ``` ballarin@13940 ` 880` ``` let ?s = "(%i. monom P (coeff P p i) i)" ``` ballarin@13940 ` 881` ``` assume R: "p \ carrier P" and "deg R p <= n" ``` ballarin@15095 ` 882` ``` then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} \ {deg R p<..n})" ``` ballarin@13940 ` 883` ``` by (simp only: ivl_disj_un_one) ``` ballarin@13940 ` 884` ``` also have "... = finsum P ?s {..deg R p}" ``` ballarin@17094 ` 885` ``` by (simp cong: P.finsum_cong add: P.finsum_Un_disjoint ivl_disj_int_one ``` ballarin@13940 ` 886` ``` deg_aboveD R Pi_def) ``` wenzelm@23350 ` 887` ``` also have "... = p" using R by (rule up_repr) ``` ballarin@13940 ` 888` ``` finally show ?thesis . ``` ballarin@13940 ` 889` ```qed ``` ballarin@13940 ` 890` ballarin@17094 ` 891` ballarin@20318 ` 892` ```subsection {* Polynomials over Integral Domains *} ``` ballarin@13940 ` 893` ballarin@13940 ` 894` ```lemma domainI: ``` ballarin@13940 ` 895` ``` assumes cring: "cring R" ``` ballarin@13940 ` 896` ``` and one_not_zero: "one R ~= zero R" ``` ballarin@13940 ` 897` ``` and integral: "!!a b. [| mult R a b = zero R; a \ carrier R; ``` ballarin@13940 ` 898` ``` b \ carrier R |] ==> a = zero R | b = zero R" ``` ballarin@13940 ` 899` ``` shows "domain R" ``` ballarin@13940 ` 900` ``` by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems ``` ballarin@13940 ` 901` ``` del: disjCI) ``` ballarin@13940 ` 902` ballarin@13940 ` 903` ```lemma (in UP_domain) UP_one_not_zero: ``` ballarin@15095 ` 904` ``` "\\<^bsub>P\<^esub> ~= \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 905` ```proof ``` ballarin@15095 ` 906` ``` assume "\\<^bsub>P\<^esub> = \\<^bsub>P\<^esub>" ``` ballarin@15095 ` 907` ``` hence "coeff P \\<^bsub>P\<^esub> 0 = (coeff P \\<^bsub>P\<^esub> 0)" by simp ``` ballarin@13940 ` 908` ``` hence "\ = \" by simp ``` ballarin@13940 ` 909` ``` with one_not_zero show "False" by contradiction ``` ballarin@13940 ` 910` ```qed ``` ballarin@13940 ` 911` ballarin@13940 ` 912` ```lemma (in UP_domain) UP_integral: ``` ballarin@15095 ` 913` ``` "[| p \\<^bsub>P\<^esub> q = \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 914` ```proof - ``` ballarin@13940 ` 915` ``` fix p q ``` ballarin@15095 ` 916` ``` assume pq: "p \\<^bsub>P\<^esub> q = \\<^bsub>P\<^esub>" and R: "p \ carrier P" "q \ carrier P" ``` ballarin@15095 ` 917` ``` show "p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>" ``` ballarin@13940 ` 918` ``` proof (rule classical) ``` ballarin@15095 ` 919` ``` assume c: "~ (p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>)" ``` ballarin@15095 ` 920` ``` with R have "deg R p + deg R q = deg R (p \\<^bsub>P\<^esub> q)" by simp ``` ballarin@13940 ` 921` ``` also from pq have "... = 0" by simp ``` ballarin@13940 ` 922` ``` finally have "deg R p + deg R q = 0" . ``` ballarin@13940 ` 923` ``` then have f1: "deg R p = 0 & deg R q = 0" by simp ``` ballarin@15095 ` 924` ``` from f1 R have "p = (\\<^bsub>P\<^esub> i \ {..0}. monom P (coeff P p i) i)" ``` ballarin@13940 ` 925` ``` by (simp only: up_repr_le) ``` ballarin@13940 ` 926` ``` also from R have "... = monom P (coeff P p 0) 0" by simp ``` ballarin@13940 ` 927` ``` finally have p: "p = monom P (coeff P p 0) 0" . ``` ballarin@15095 ` 928` ``` from f1 R have "q = (\\<^bsub>P\<^esub> i \ {..0}. monom P (coeff P q i) i)" ``` ballarin@13940 ` 929` ``` by (simp only: up_repr_le) ``` ballarin@13940 ` 930` ``` also from R have "... = monom P (coeff P q 0) 0" by simp ``` ballarin@13940 ` 931` ``` finally have q: "q = monom P (coeff P q 0) 0" . ``` ballarin@15095 ` 932` ``` from R have "coeff P p 0 \ coeff P q 0 = coeff P (p \\<^bsub>P\<^esub> q) 0" by simp ``` ballarin@13940 ` 933` ``` also from pq have "... = \" by simp ``` ballarin@13940 ` 934` ``` finally have "coeff P p 0 \ coeff P q 0 = \" . ``` ballarin@13940 ` 935` ``` with R have "coeff P p 0 = \ | coeff P q 0 = \" ``` ballarin@13940 ` 936` ``` by (simp add: R.integral_iff) ``` ballarin@15095 ` 937` ``` with p q show "p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>" by fastsimp ``` ballarin@13940 ` 938` ``` qed ``` ballarin@13940 ` 939` ```qed ``` ballarin@13940 ` 940` ballarin@13940 ` 941` ```theorem (in UP_domain) UP_domain: ``` ballarin@13940 ` 942` ``` "domain P" ``` ballarin@13940 ` 943` ``` by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI) ``` ballarin@13940 ` 944` ballarin@13940 ` 945` ```text {* ``` ballarin@17094 ` 946` ``` Interpretation of theorems from @{term domain}. ``` ballarin@13940 ` 947` ```*} ``` ballarin@13940 ` 948` ballarin@17094 ` 949` ```interpretation UP_domain < "domain" P ``` ballarin@19984 ` 950` ``` by intro_locales (rule domain.axioms UP_domain)+ ``` ballarin@13940 ` 951` wenzelm@14666 ` 952` ballarin@20318 ` 953` ```subsection {* The Evaluation Homomorphism and Universal Property*} ``` ballarin@13940 ` 954` wenzelm@14666 ` 955` ```(* alternative congruence rule (possibly more efficient) ``` wenzelm@14666 ` 956` ```lemma (in abelian_monoid) finsum_cong2: ``` wenzelm@14666 ` 957` ``` "[| !!i. i \ A ==> f i \ carrier G = True; A = B; ``` wenzelm@14666 ` 958` ``` !!i. i \ B ==> f i = g i |] ==> finsum G f A = finsum G g B" ``` wenzelm@14666 ` 959` ``` sorry*) ``` wenzelm@14666 ` 960` ballarin@13940 ` 961` ```theorem (in cring) diagonal_sum: ``` ballarin@13940 ` 962` ``` "[| f \ {..n + m::nat} -> carrier R; g \ {..n + m} -> carrier R |] ==> ``` wenzelm@14666 ` 963` ``` (\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) = ``` wenzelm@14666 ` 964` ``` (\k \ {..n + m}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 965` ```proof - ``` ballarin@13940 ` 966` ``` assume Rf: "f \ {..n + m} -> carrier R" and Rg: "g \ {..n + m} -> carrier R" ``` ballarin@13940 ` 967` ``` { ``` ballarin@13940 ` 968` ``` fix j ``` ballarin@13940 ` 969` ``` have "j <= n + m ==> ``` wenzelm@14666 ` 970` ``` (\k \ {..j}. \i \ {..k}. f i \ g (k - i)) = ``` wenzelm@14666 ` 971` ``` (\k \ {..j}. \i \ {..j - k}. f k \ g i)" ``` ballarin@13940 ` 972` ``` proof (induct j) ``` ballarin@13940 ` 973` ``` case 0 from Rf Rg show ?case by (simp add: Pi_def) ``` ballarin@13940 ` 974` ``` next ``` wenzelm@14666 ` 975` ``` case (Suc j) ``` ballarin@13940 ` 976` ``` have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \ carrier R" ``` webertj@20217 ` 977` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) ``` ballarin@13940 ` 978` ``` have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \ carrier R" ``` webertj@20217 ` 979` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) ``` ballarin@13940 ` 980` ``` have R9: "!!i k. [| k <= Suc j |] ==> f k \ carrier R" ``` wenzelm@14666 ` 981` ``` using Suc by (auto intro!: funcset_mem [OF Rf]) ``` ballarin@13940 ` 982` ``` have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \ carrier R" ``` webertj@20217 ` 983` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) ``` ballarin@13940 ` 984` ``` have R11: "g 0 \ carrier R" ``` wenzelm@14666 ` 985` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) ``` ballarin@13940 ` 986` ``` from Suc show ?case ``` wenzelm@14666 ` 987` ``` by (simp cong: finsum_cong add: Suc_diff_le a_ac ``` wenzelm@14666 ` 988` ``` Pi_def R6 R8 R9 R10 R11) ``` ballarin@13940 ` 989` ``` qed ``` ballarin@13940 ` 990` ``` } ``` ballarin@13940 ` 991` ``` then show ?thesis by fast ``` ballarin@13940 ` 992` ```qed ``` ballarin@13940 ` 993` ballarin@13940 ` 994` ```lemma (in abelian_monoid) boundD_carrier: ``` ballarin@13940 ` 995` ``` "[| bound \ n f; n < m |] ==> f m \ carrier G" ``` ballarin@13940 ` 996` ``` by auto ``` ballarin@13940 ` 997` ballarin@13940 ` 998` ```theorem (in cring) cauchy_product: ``` ballarin@13940 ` 999` ``` assumes bf: "bound \ n f" and bg: "bound \ m g" ``` ballarin@13940 ` 1000` ``` and Rf: "f \ {..n} -> carrier R" and Rg: "g \ {..m} -> carrier R" ``` wenzelm@14666 ` 1001` ``` shows "(\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) = ``` ballarin@17094 ` 1002` ``` (\i \ {..n}. f i) \ (\i \ {..m}. g i)" (* State reverse direction? *) ``` ballarin@13940 ` 1003` ```proof - ``` ballarin@13940 ` 1004` ``` have f: "!!x. f x \ carrier R" ``` ballarin@13940 ` 1005` ``` proof - ``` ballarin@13940 ` 1006` ``` fix x ``` ballarin@13940 ` 1007` ``` show "f x \ carrier R" ``` ballarin@13940 ` 1008` ``` using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def) ``` ballarin@13940 ` 1009` ``` qed ``` ballarin@13940 ` 1010` ``` have g: "!!x. g x \ carrier R" ``` ballarin@13940 ` 1011` ``` proof - ``` ballarin@13940 ` 1012` ``` fix x ``` ballarin@13940 ` 1013` ``` show "g x \ carrier R" ``` ballarin@13940 ` 1014` ``` using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def) ``` ballarin@13940 ` 1015` ``` qed ``` wenzelm@14666 ` 1016` ``` from f g have "(\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) = ``` wenzelm@14666 ` 1017` ``` (\k \ {..n + m}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1018` ``` by (simp add: diagonal_sum Pi_def) ``` nipkow@15045 ` 1019` ``` also have "... = (\k \ {..n} \ {n<..n + m}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1020` ``` by (simp only: ivl_disj_un_one) ``` wenzelm@14666 ` 1021` ``` also from f g have "... = (\k \ {..n}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1022` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1023` ``` add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` ballarin@15095 ` 1024` ``` also from f g ``` ballarin@15095 ` 1025` ``` have "... = (\k \ {..n}. \i \ {..m} \ {m<..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1026` ``` by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def) ``` wenzelm@14666 ` 1027` ``` also from f g have "... = (\k \ {..n}. \i \ {..m}. f k \ g i)" ``` ballarin@13940 ` 1028` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1029` ``` add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` wenzelm@14666 ` 1030` ``` also from f g have "... = (\i \ {..n}. f i) \ (\i \ {..m}. g i)" ``` ballarin@13940 ` 1031` ``` by (simp add: finsum_ldistr diagonal_sum Pi_def, ``` ballarin@13940 ` 1032` ``` simp cong: finsum_cong add: finsum_rdistr Pi_def) ``` ballarin@13940 ` 1033` ``` finally show ?thesis . ``` ballarin@13940 ` 1034` ```qed ``` ballarin@13940 ` 1035` ballarin@13940 ` 1036` ```lemma (in UP_cring) const_ring_hom: ``` ballarin@13940 ` 1037` ``` "(%a. monom P a 0) \ ring_hom R P" ``` ballarin@13940 ` 1038` ``` by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult) ``` ballarin@13940 ` 1039` wenzelm@14651 ` 1040` ```constdefs (structure S) ``` ballarin@15095 ` 1041` ``` eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme, ``` ballarin@15095 ` 1042` ``` 'a => 'b, 'b, nat => 'a] => 'b" ``` wenzelm@14651 ` 1043` ``` "eval R S phi s == \p \ carrier (UP R). ``` ballarin@15095 ` 1044` ``` \i \ {..deg R p}. phi (coeff (UP R) p i) \ s (^) i" ``` ballarin@15095 ` 1045` wenzelm@14666 ` 1046` ballarin@15095 ` 1047` ```lemma (in UP) eval_on_carrier: ``` ballarin@19783 ` 1048` ``` fixes S (structure) ``` ballarin@17094 ` 1049` ``` shows "p \ carrier P ==> ``` ballarin@17094 ` 1050` ``` eval R S phi s p = (\\<^bsub>S\<^esub> i \ {..deg R p}. phi (coeff P p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@13940 ` 1051` ``` by (unfold eval_def, fold P_def) simp ``` ballarin@13940 ` 1052` ballarin@15095 ` 1053` ```lemma (in UP) eval_extensional: ``` ballarin@17094 ` 1054` ``` "eval R S phi p \ extensional (carrier P)" ``` ballarin@13940 ` 1055` ``` by (unfold eval_def, fold P_def) simp ``` ballarin@13940 ` 1056` ballarin@17094 ` 1057` ballarin@17094 ` 1058` ```text {* The universal property of the polynomial ring *} ``` ballarin@17094 ` 1059` ballarin@17094 ` 1060` ```locale UP_pre_univ_prop = ring_hom_cring R S h + UP_cring R P ``` ballarin@17094 ` 1061` ballarin@19783 ` 1062` ```locale UP_univ_prop = UP_pre_univ_prop + ``` ballarin@19783 ` 1063` ``` fixes s and Eval ``` ballarin@17094 ` 1064` ``` assumes indet_img_carrier [simp, intro]: "s \ carrier S" ``` ballarin@17094 ` 1065` ``` defines Eval_def: "Eval == eval R S h s" ``` ballarin@17094 ` 1066` ballarin@17094 ` 1067` ```theorem (in UP_pre_univ_prop) eval_ring_hom: ``` ballarin@17094 ` 1068` ``` assumes S: "s \ carrier S" ``` ballarin@17094 ` 1069` ``` shows "eval R S h s \ ring_hom P S" ``` ballarin@13940 ` 1070` ```proof (rule ring_hom_memI) ``` ballarin@13940 ` 1071` ``` fix p ``` ballarin@17094 ` 1072` ``` assume R: "p \ carrier P" ``` ballarin@13940 ` 1073` ``` then show "eval R S h s p \ carrier S" ``` ballarin@17094 ` 1074` ``` by (simp only: eval_on_carrier) (simp add: S Pi_def) ``` ballarin@13940 ` 1075` ```next ``` ballarin@13940 ` 1076` ``` fix p q ``` ballarin@17094 ` 1077` ``` assume R: "p \ carrier P" "q \ carrier P" ``` ballarin@15095 ` 1078` ``` then show "eval R S h s (p \\<^bsub>P\<^esub> q) = eval R S h s p \\<^bsub>S\<^esub> eval R S h s q" ``` ballarin@13940 ` 1079` ``` proof (simp only: eval_on_carrier UP_mult_closed) ``` ballarin@17094 ` 1080` ``` from R S have ``` ballarin@15095 ` 1081` ``` "(\\<^bsub>S\<^esub> i \ {..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = ``` ballarin@15095 ` 1082` ``` (\\<^bsub>S\<^esub> i \ {..deg R (p \\<^bsub>P\<^esub> q)} \ {deg R (p \\<^bsub>P\<^esub> q)<..deg R p + deg R q}. ``` ballarin@15095 ` 1083` ``` h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@17094 ` 1084` ``` by (simp cong: S.finsum_cong ``` ballarin@17094 ` 1085` ``` add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def ``` wenzelm@14666 ` 1086` ``` del: coeff_mult) ``` ballarin@17094 ` 1087` ``` also from R have "... = ``` ballarin@15095 ` 1088` ``` (\\<^bsub>S\<^esub> i \ {..deg R p + deg R q}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@13940 ` 1089` ``` by (simp only: ivl_disj_un_one deg_mult_cring) ``` ballarin@17094 ` 1090` ``` also from R S have "... = ``` ballarin@15095 ` 1091` ``` (\\<^bsub>S\<^esub> i \ {..deg R p + deg R q}. ``` ballarin@15095 ` 1092` ``` \\<^bsub>S\<^esub> k \ {..i}. ``` ballarin@15095 ` 1093` ``` h (coeff P p k) \\<^bsub>S\<^esub> h (coeff P q (i - k)) \\<^bsub>S\<^esub> ``` ballarin@15095 ` 1094` ``` (s (^)\<^bsub>S\<^esub> k \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))" ``` ballarin@17094 ` 1095` ``` by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def ``` wenzelm@14666 ` 1096` ``` S.m_ac S.finsum_rdistr) ``` ballarin@17094 ` 1097` ``` also from R S have "... = ``` ballarin@15095 ` 1098` ``` (\\<^bsub>S\<^esub> i\{..deg R p}. h (coeff P p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \\<^bsub>S\<^esub> ``` ballarin@15095 ` 1099` ``` (\\<^bsub>S\<^esub> i\{..deg R q}. h (coeff P q i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` wenzelm@14666 ` 1100` ``` by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac ``` wenzelm@14666 ` 1101` ``` Pi_def) ``` ballarin@13940 ` 1102` ``` finally show ``` ballarin@15095 ` 1103` ``` "(\\<^bsub>S\<^esub> i \ {..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = ``` ballarin@15095 ` 1104` ``` (\\<^bsub>S\<^esub> i \ {..deg R p}. h (coeff P p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \\<^bsub>S\<^esub> ``` ballarin@15095 ` 1105` ``` (\\<^bsub>S\<^esub> i \ {..deg R q}. h (coeff P q i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" . ``` ballarin@13940 ` 1106` ``` qed ``` ballarin@13940 ` 1107` ```next ``` ballarin@13940 ` 1108` ``` fix p q ``` ballarin@17094 ` 1109` ``` assume R: "p \ carrier P" "q \ carrier P" ``` ballarin@15095 ` 1110` ``` then show "eval R S h s (p \\<^bsub>P\<^esub> q) = eval R S h s p \\<^bsub>S\<^esub> eval R S h s q" ``` ballarin@17094 ` 1111` ``` proof (simp only: eval_on_carrier P.a_closed) ``` ballarin@17094 ` 1112` ``` from S R have ``` ballarin@15095 ` 1113` ``` "(\\<^bsub>S \<^esub>i\{..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = ``` ballarin@15095 ` 1114` ``` (\\<^bsub>S \<^esub>i\{..deg R (p \\<^bsub>P\<^esub> q)} \ {deg R (p \\<^bsub>P\<^esub> q)<..max (deg R p) (deg R q)}. ``` ballarin@15095 ` 1115` ``` h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@17094 ` 1116` ``` by (simp cong: S.finsum_cong ``` ballarin@17094 ` 1117` ``` add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def ``` wenzelm@14666 ` 1118` ``` del: coeff_add) ``` ballarin@17094 ` 1119` ``` also from R have "... = ``` ballarin@15095 ` 1120` ``` (\\<^bsub>S\<^esub> i \ {..max (deg R p) (deg R q)}. ``` ballarin@15095 ` 1121` ``` h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@13940 ` 1122` ``` by (simp add: ivl_disj_un_one) ``` ballarin@17094 ` 1123` ``` also from R S have "... = ``` ballarin@15095 ` 1124` ``` (\\<^bsub>S\<^esub>i\{..max (deg R p) (deg R q)}. h (coeff P p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \\<^bsub>S\<^esub> ``` ballarin@15095 ` 1125` ``` (\\<^bsub>S\<^esub>i\{..max (deg R p) (deg R q)}. h (coeff P q i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@17094 ` 1126` ``` by (simp cong: S.finsum_cong ``` ballarin@17094 ` 1127` ``` add: S.l_distr deg_aboveD ivl_disj_int_one Pi_def) ``` ballarin@13940 ` 1128` ``` also have "... = ``` ballarin@15095 ` 1129` ``` (\\<^bsub>S\<^esub> i \ {..deg R p} \ {deg R p<..max (deg R p) (deg R q)}. ``` ballarin@15095 ` 1130` ``` h (coeff P p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \\<^bsub>S\<^esub> ``` ballarin@15095 ` 1131` ``` (\\<^bsub>S\<^esub> i \ {..deg R q} \ {deg R q<..max (deg R p) (deg R q)}. ``` ballarin@15095 ` 1132` ``` h (coeff P q i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@13940 ` 1133` ``` by (simp only: ivl_disj_un_one le_maxI1 le_maxI2) ``` ballarin@17094 ` 1134` ``` also from R S have "... = ``` ballarin@15095 ` 1135` ``` (\\<^bsub>S\<^esub> i \ {..deg R p}. h (coeff P p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \\<^bsub>S\<^esub> ``` ballarin@15095 ` 1136` ``` (\\<^bsub>S\<^esub> i \ {..deg R q}. h (coeff P q i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@17094 ` 1137` ``` by (simp cong: S.finsum_cong ``` ballarin@17094 ` 1138` ``` add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` ballarin@13940 ` 1139` ``` finally show ``` ballarin@15095 ` 1140` ``` "(\\<^bsub>S\<^esub>i \ {..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = ``` ballarin@15095 ` 1141` ``` (\\<^bsub>S\<^esub>i \ {..deg R p}. h (coeff P p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \\<^bsub>S\<^esub> ``` ballarin@15095 ` 1142` ``` (\\<^bsub>S\<^esub>i \ {..deg R q}. h (coeff P q i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" . ``` ballarin@13940 ` 1143` ``` qed ``` ballarin@13940 ` 1144` ```next ``` ballarin@17094 ` 1145` ``` show "eval R S h s \\<^bsub>P\<^esub> = \\<^bsub>S\<^esub>" ``` ballarin@13940 ` 1146` ``` by (simp only: eval_on_carrier UP_one_closed) simp ``` ballarin@13940 ` 1147` ```qed ``` ballarin@13940 ` 1148` ballarin@17094 ` 1149` ```text {* Interpretation of ring homomorphism lemmas. *} ``` ballarin@13940 ` 1150` ballarin@17094 ` 1151` ```interpretation UP_univ_prop < ring_hom_cring P S Eval ``` ballarin@19931 ` 1152` ``` apply (unfold Eval_def) ``` ballarin@19984 ` 1153` ``` apply intro_locales ``` ballarin@19931 ` 1154` ``` apply (rule ring_hom_cring.axioms) ``` ballarin@19931 ` 1155` ``` apply (rule ring_hom_cring.intro) ``` ballarin@19984 ` 1156` ``` apply unfold_locales ``` ballarin@19931 ` 1157` ``` apply (rule eval_ring_hom) ``` ballarin@19931 ` 1158` ``` apply rule ``` ballarin@19931 ` 1159` ``` done ``` ballarin@19931 ` 1160` ballarin@13940 ` 1161` ballarin@13940 ` 1162` ```text {* Further properties of the evaluation homomorphism. *} ``` ballarin@13940 ` 1163` wenzelm@21502 ` 1164` ```text {* ``` wenzelm@21502 ` 1165` ``` The following lemma could be proved in @{text UP_cring} with the additional ``` wenzelm@21502 ` 1166` ``` assumption that @{text h} is closed. *} ``` ballarin@13940 ` 1167` ballarin@17094 ` 1168` ```lemma (in UP_pre_univ_prop) eval_const: ``` ballarin@13940 ` 1169` ``` "[| s \ carrier S; r \ carrier R |] ==> eval R S h s (monom P r 0) = h r" ``` ballarin@13940 ` 1170` ``` by (simp only: eval_on_carrier monom_closed) simp ``` ballarin@13940 ` 1171` ballarin@13940 ` 1172` ```text {* The following proof is complicated by the fact that in arbitrary ``` ballarin@13940 ` 1173` ``` rings one might have @{term "one R = zero R"}. *} ``` ballarin@13940 ` 1174` ballarin@13940 ` 1175` ```(* TODO: simplify by cases "one R = zero R" *) ``` ballarin@13940 ` 1176` ballarin@17094 ` 1177` ```lemma (in UP_pre_univ_prop) eval_monom1: ``` ballarin@17094 ` 1178` ``` assumes S: "s \ carrier S" ``` ballarin@17094 ` 1179` ``` shows "eval R S h s (monom P \ 1) = s" ``` ballarin@13940 ` 1180` ```proof (simp only: eval_on_carrier monom_closed R.one_closed) ``` ballarin@17094 ` 1181` ``` from S have ``` ballarin@15095 ` 1182` ``` "(\\<^bsub>S\<^esub> i\{..deg R (monom P \ 1)}. h (coeff P (monom P \ 1) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = ``` ballarin@15095 ` 1183` ``` (\\<^bsub>S\<^esub> i\{..deg R (monom P \ 1)} \ {deg R (monom P \ 1)<..1}. ``` ballarin@15095 ` 1184` ``` h (coeff P (monom P \ 1) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@17094 ` 1185` ``` by (simp cong: S.finsum_cong del: coeff_monom ``` ballarin@17094 ` 1186` ``` add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` wenzelm@14666 ` 1187` ``` also have "... = ``` ballarin@15095 ` 1188` ``` (\\<^bsub>S\<^esub> i \ {..1}. h (coeff P (monom P \ 1) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" ``` ballarin@13940 ` 1189` ``` by (simp only: ivl_disj_un_one deg_monom_le R.one_closed) ``` ballarin@13940 ` 1190` ``` also have "... = s" ``` ballarin@15095 ` 1191` ``` proof (cases "s = \\<^bsub>S\<^esub>") ``` ballarin@13940 ` 1192` ``` case True then show ?thesis by (simp add: Pi_def) ``` ballarin@13940 ` 1193` ``` next ``` ballarin@17094 ` 1194` ``` case False then show ?thesis by (simp add: S Pi_def) ``` ballarin@13940 ` 1195` ``` qed ``` ballarin@15095 ` 1196` ``` finally show "(\\<^bsub>S\<^esub> i \ {..deg R (monom P \ 1)}. ``` ballarin@15095 ` 1197` ``` h (coeff P (monom P \ 1) i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = s" . ``` ballarin@13940 ` 1198` ```qed ``` ballarin@13940 ` 1199` ballarin@13940 ` 1200` ```lemma (in UP_cring) monom_pow: ``` ballarin@13940 ` 1201` ``` assumes R: "a \ carrier R" ``` ballarin@15095 ` 1202` ``` shows "(monom P a n) (^)\<^bsub>P\<^esub> m = monom P (a (^) m) (n * m)" ``` ballarin@13940 ` 1203` ```proof (induct m) ``` ballarin@13940 ` 1204` ``` case 0 from R show ?case by simp ``` ballarin@13940 ` 1205` ```next ``` ballarin@13940 ` 1206` ``` case Suc with R show ?case ``` ballarin@13940 ` 1207` ``` by (simp del: monom_mult add: monom_mult [THEN sym] add_commute) ``` ballarin@13940 ` 1208` ```qed ``` ballarin@13940 ` 1209` ballarin@13940 ` 1210` ```lemma (in ring_hom_cring) hom_pow [simp]: ``` ballarin@15095 ` 1211` ``` "x \ carrier R ==> h (x (^) n) = h x (^)\<^bsub>S\<^esub> (n::nat)" ``` ballarin@13940 ` 1212` ``` by (induct n) simp_all ``` ballarin@13940 ` 1213` ballarin@17094 ` 1214` ```lemma (in UP_univ_prop) Eval_monom: ``` ballarin@17094 ` 1215` ``` "r \ carrier R ==> Eval (monom P r n) = h r \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" ``` ballarin@13940 ` 1216` ```proof - ``` ballarin@17094 ` 1217` ``` assume R: "r \ carrier R" ``` ballarin@17094 ` 1218` ``` from R have "Eval (monom P r n) = Eval (monom P r 0 \\<^bsub>P\<^esub> (monom P \ 1) (^)\<^bsub>P\<^esub> n)" ``` ballarin@17094 ` 1219` ``` by (simp del: monom_mult add: monom_mult [THEN sym] monom_pow) ``` ballarin@15095 ` 1220` ``` also ``` ballarin@17094 ` 1221` ``` from R eval_monom1 [where s = s, folded Eval_def] ``` ballarin@17094 ` 1222` ``` have "... = h r \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" ``` ballarin@17094 ` 1223` ``` by (simp add: eval_const [where s = s, folded Eval_def]) ``` ballarin@13940 ` 1224` ``` finally show ?thesis . ``` ballarin@13940 ` 1225` ```qed ``` ballarin@13940 ` 1226` ballarin@17094 ` 1227` ```lemma (in UP_pre_univ_prop) eval_monom: ``` ballarin@17094 ` 1228` ``` assumes R: "r \ carrier R" and S: "s \ carrier S" ``` ballarin@17094 ` 1229` ``` shows "eval R S h s (monom P r n) = h r \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" ``` ballarin@15095 ` 1230` ```proof - ``` ballarin@19931 ` 1231` ``` interpret UP_univ_prop [R S h P s _] ``` wenzelm@22931 ` 1232` ``` using `UP_pre_univ_prop R S h` P_def R S ``` wenzelm@22931 ` 1233` ``` by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro) ``` ballarin@17094 ` 1234` ``` from R ``` ballarin@17094 ` 1235` ``` show ?thesis by (rule Eval_monom) ``` ballarin@17094 ` 1236` ```qed ``` ballarin@17094 ` 1237` ballarin@17094 ` 1238` ```lemma (in UP_univ_prop) Eval_smult: ``` ballarin@17094 ` 1239` ``` "[| r \ carrier R; p \ carrier P |] ==> Eval (r \\<^bsub>P\<^esub> p) = h r \\<^bsub>S\<^esub> Eval p" ``` ballarin@17094 ` 1240` ```proof - ``` ballarin@17094 ` 1241` ``` assume R: "r \ carrier R" and P: "p \ carrier P" ``` ballarin@17094 ` 1242` ``` then show ?thesis ``` ballarin@17094 ` 1243` ``` by (simp add: monom_mult_is_smult [THEN sym] ``` ballarin@17094 ` 1244` ``` eval_const [where s = s, folded Eval_def]) ``` ballarin@15095 ` 1245` ```qed ``` ballarin@13940 ` 1246` ballarin@13940 ` 1247` ```lemma ring_hom_cringI: ``` ballarin@13940 ` 1248` ``` assumes "cring R" ``` ballarin@13940 ` 1249` ``` and "cring S" ``` ballarin@13940 ` 1250` ``` and "h \ ring_hom R S" ``` ballarin@13940 ` 1251` ``` shows "ring_hom_cring R S h" ``` ballarin@13940 ` 1252` ``` by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro ``` ballarin@13940 ` 1253` ``` cring.axioms prems) ``` ballarin@13940 ` 1254` ballarin@17094 ` 1255` ```lemma (in UP_pre_univ_prop) UP_hom_unique: ``` ballarin@17094 ` 1256` ``` includes ring_hom_cring P S Phi ``` ballarin@17094 ` 1257` ``` assumes Phi: "Phi (monom P \ (Suc 0)) = s" ``` ballarin@13940 ` 1258` ``` "!!r. r \ carrier R ==> Phi (monom P r 0) = h r" ``` ballarin@17094 ` 1259` ``` includes ring_hom_cring P S Psi ``` ballarin@17094 ` 1260` ``` assumes Psi: "Psi (monom P \ (Suc 0)) = s" ``` ballarin@13940 ` 1261` ``` "!!r. r \ carrier R ==> Psi (monom P r 0) = h r" ``` ballarin@17094 ` 1262` ``` and P: "p \ carrier P" and S: "s \ carrier S" ``` ballarin@13940 ` 1263` ``` shows "Phi p = Psi p" ``` ballarin@13940 ` 1264` ```proof - ``` ballarin@15095 ` 1265` ``` have "Phi p = ``` ballarin@15095 ` 1266` ``` Phi (\\<^bsub>P \<^esub>i \ {..deg R p}. monom P (coeff P p i) 0 \\<^bsub>P\<^esub> monom P \ 1 (^)\<^bsub>P\<^esub> i)" ``` ballarin@17094 ` 1267` ``` by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult) ``` ballarin@15696 ` 1268` ``` also ``` ballarin@15696 ` 1269` ``` have "... = ``` ballarin@15095 ` 1270` ``` Psi (\\<^bsub>P \<^esub>i\{..deg R p}. monom P (coeff P p i) 0 \\<^bsub>P\<^esub> monom P \ 1 (^)\<^bsub>P\<^esub> i)" ``` ballarin@17094 ` 1271` ``` by (simp add: Phi Psi P Pi_def comp_def) ``` ballarin@13940 ` 1272` ``` also have "... = Psi p" ``` ballarin@17094 ` 1273` ``` by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult) ``` ballarin@13940 ` 1274` ``` finally show ?thesis . ``` ballarin@13940 ` 1275` ```qed ``` ballarin@13940 ` 1276` ballarin@17094 ` 1277` ```lemma (in UP_pre_univ_prop) ring_homD: ``` ballarin@17094 ` 1278` ``` assumes Phi: "Phi \ ring_hom P S" ``` ballarin@17094 ` 1279` ``` shows "ring_hom_cring P S Phi" ``` ballarin@17094 ` 1280` ```proof (rule ring_hom_cring.intro) ``` ballarin@17094 ` 1281` ``` show "ring_hom_cring_axioms P S Phi" ``` ballarin@17094 ` 1282` ``` by (rule ring_hom_cring_axioms.intro) (rule Phi) ``` ballarin@19984 ` 1283` ```qed unfold_locales ``` ballarin@17094 ` 1284` ballarin@17094 ` 1285` ```theorem (in UP_pre_univ_prop) UP_universal_property: ``` ballarin@17094 ` 1286` ``` assumes S: "s \ carrier S" ``` ballarin@17094 ` 1287` ``` shows "EX! Phi. Phi \ ring_hom P S \ extensional (carrier P) & ``` wenzelm@14666 ` 1288` ``` Phi (monom P \ 1) = s & ``` ballarin@13940 ` 1289` ``` (ALL r : carrier R. Phi (monom P r 0) = h r)" ``` ballarin@17094 ` 1290` ``` using S eval_monom1 ``` ballarin@13940 ` 1291` ``` apply (auto intro: eval_ring_hom eval_const eval_extensional) ``` wenzelm@14666 ` 1292` ``` apply (rule extensionalityI) ``` ballarin@17094 ` 1293` ``` apply (auto intro: UP_hom_unique ring_homD) ``` wenzelm@14666 ` 1294` ``` done ``` ballarin@13940 ` 1295` ballarin@17094 ` 1296` ballarin@20318 ` 1297` ```subsection {* Sample Application of Evaluation Homomorphism *} ``` ballarin@13940 ` 1298` ballarin@17094 ` 1299` ```lemma UP_pre_univ_propI: ``` ballarin@13940 ` 1300` ``` assumes "cring R" ``` ballarin@13940 ` 1301` ``` and "cring S" ``` ballarin@13940 ` 1302` ``` and "h \ ring_hom R S" ``` ballarin@19931 ` 1303` ``` shows "UP_pre_univ_prop R S h" ``` wenzelm@23350 ` 1304` ``` using assms ``` ballarin@19931 ` 1305` ``` by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro ``` ballarin@19931 ` 1306` ``` ring_hom_cring_axioms.intro UP_cring.intro) ``` ballarin@13940 ` 1307` ballarin@13975 ` 1308` ```constdefs ``` ballarin@13975 ` 1309` ``` INTEG :: "int ring" ``` ballarin@13975 ` 1310` ``` "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)" ``` ballarin@13975 ` 1311` ballarin@15095 ` 1312` ```lemma INTEG_cring: ``` ballarin@13975 ` 1313` ``` "cring INTEG" ``` ballarin@13975 ` 1314` ``` by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI ``` ballarin@13975 ` 1315` ``` zadd_zminus_inverse2 zadd_zmult_distrib) ``` ballarin@13975 ` 1316` ballarin@15095 ` 1317` ```lemma INTEG_id_eval: ``` ballarin@17094 ` 1318` ``` "UP_pre_univ_prop INTEG INTEG id" ``` ballarin@17094 ` 1319` ``` by (fast intro: UP_pre_univ_propI INTEG_cring id_ring_hom) ``` ballarin@13940 ` 1320` ballarin@13940 ` 1321` ```text {* ``` ballarin@17094 ` 1322` ``` Interpretation now enables to import all theorems and lemmas ``` ballarin@13940 ` 1323` ``` valid in the context of homomorphisms between @{term INTEG} and @{term ``` ballarin@15095 ` 1324` ``` "UP INTEG"} globally. ``` wenzelm@14666 ` 1325` ```*} ``` ballarin@13940 ` 1326` ballarin@17094 ` 1327` ```interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] ``` ballarin@19931 ` 1328` ``` apply simp ``` ballarin@15763 ` 1329` ``` using INTEG_id_eval ``` ballarin@19931 ` 1330` ``` apply simp ``` ballarin@19931 ` 1331` ``` done ``` ballarin@15763 ` 1332` ballarin@13940 ` 1333` ```lemma INTEG_closed [intro, simp]: ``` ballarin@13940 ` 1334` ``` "z \ carrier INTEG" ``` ballarin@13940 ` 1335` ``` by (unfold INTEG_def) simp ``` ballarin@13940 ` 1336` ballarin@13940 ` 1337` ```lemma INTEG_mult [simp]: ``` ballarin@13940 ` 1338` ``` "mult INTEG z w = z * w" ``` ballarin@13940 ` 1339` ``` by (unfold INTEG_def) simp ``` ballarin@13940 ` 1340` ballarin@13940 ` 1341` ```lemma INTEG_pow [simp]: ``` ballarin@13940 ` 1342` ``` "pow INTEG z n = z ^ n" ``` ballarin@13940 ` 1343` ``` by (induct n) (simp_all add: INTEG_def nat_pow_def) ``` ballarin@13940 ` 1344` ballarin@13940 ` 1345` ```lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500" ``` ballarin@15763 ` 1346` ``` by (simp add: INTEG.eval_monom) ``` ballarin@13940 ` 1347` wenzelm@14590 ` 1348` ```end ```