src/HOL/Algebra/UnivPoly.thy
 author wenzelm Thu May 06 14:14:18 2004 +0200 (2004-05-06) changeset 14706 71590b7733b7 parent 14666 65f8680c3f16 child 14963 d584e32f7d46 permissions -rw-r--r--
tuned document;
 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` wenzelm@14577 ` 8` ```header {* Univariate Polynomials *} ``` ballarin@13940 ` 9` wenzelm@14577 ` 10` ```theory UnivPoly = Module: ``` ballarin@13940 ` 11` ballarin@14553 ` 12` ```text {* ``` wenzelm@14666 ` 13` ``` Polynomials are formalised as modules with additional operations for ``` wenzelm@14666 ` 14` ``` extracting coefficients from polynomials and for obtaining monomials ``` wenzelm@14666 ` 15` ``` from coefficients and exponents (record @{text "up_ring"}). The ``` wenzelm@14666 ` 16` ``` carrier set is a set of bounded functions from Nat to the ``` wenzelm@14666 ` 17` ``` coefficient domain. Bounded means that these functions return zero ``` wenzelm@14666 ` 18` ``` above a certain bound (the degree). There is a chapter on the ``` wenzelm@14706 ` 19` ``` formalisation of polynomials in the PhD thesis \cite{Ballarin:1999}, ``` wenzelm@14706 ` 20` ``` which was implemented with axiomatic type classes. This was later ``` wenzelm@14706 ` 21` ``` ported to Locales. ``` ballarin@14553 ` 22` ```*} ``` ballarin@14553 ` 23` wenzelm@14666 ` 24` ballarin@13949 ` 25` ```subsection {* The Constructor for Univariate Polynomials *} ``` ballarin@13940 ` 26` wenzelm@14666 ` 27` ```locale bound = ``` wenzelm@14666 ` 28` ``` fixes z :: 'a ``` wenzelm@14666 ` 29` ``` and n :: nat ``` wenzelm@14666 ` 30` ``` and f :: "nat => 'a" ``` wenzelm@14666 ` 31` ``` assumes bound: "!!m. n < m \ f m = z" ``` ballarin@13940 ` 32` wenzelm@14666 ` 33` ```declare bound.intro [intro!] ``` wenzelm@14666 ` 34` ``` and bound.bound [dest] ``` ballarin@13940 ` 35` ballarin@13940 ` 36` ```lemma bound_below: ``` wenzelm@14666 ` 37` ``` assumes bound: "bound z m f" and nonzero: "f n \ z" shows "n \ m" ``` ballarin@13940 ` 38` ```proof (rule classical) ``` ballarin@13940 ` 39` ``` assume "~ ?thesis" ``` ballarin@13940 ` 40` ``` then have "m < n" by arith ``` ballarin@13940 ` 41` ``` with bound have "f n = z" .. ``` ballarin@13940 ` 42` ``` with nonzero show ?thesis by contradiction ``` ballarin@13940 ` 43` ```qed ``` ballarin@13940 ` 44` ballarin@13940 ` 45` ```record ('a, 'p) up_ring = "('a, 'p) module" + ``` ballarin@13940 ` 46` ``` monom :: "['a, nat] => 'p" ``` ballarin@13940 ` 47` ``` coeff :: "['p, nat] => 'a" ``` ballarin@13940 ` 48` wenzelm@14651 ` 49` ```constdefs (structure R) ``` wenzelm@14651 ` 50` ``` up :: "_ => (nat => 'a) set" ``` wenzelm@14651 ` 51` ``` "up R == {f. f \ UNIV -> carrier R & (EX n. bound \ n f)}" ``` wenzelm@14651 ` 52` ``` UP :: "_ => ('a, nat => 'a) up_ring" ``` ballarin@13940 ` 53` ``` "UP R == (| ``` ballarin@13940 ` 54` ``` carrier = up R, ``` wenzelm@14651 ` 55` ``` mult = (%p:up R. %q:up R. %n. \i \ {..n}. p i \ q (n-i)), ``` wenzelm@14651 ` 56` ``` one = (%i. if i=0 then \ else \), ``` wenzelm@14651 ` 57` ``` zero = (%i. \), ``` wenzelm@14651 ` 58` ``` add = (%p:up R. %q:up R. %i. p i \ q i), ``` wenzelm@14651 ` 59` ``` smult = (%a:carrier R. %p:up R. %i. a \ p i), ``` wenzelm@14651 ` 60` ``` monom = (%a:carrier R. %n i. if i=n then a else \), ``` ballarin@13940 ` 61` ``` coeff = (%p:up R. %n. p n) |)" ``` ballarin@13940 ` 62` ballarin@13940 ` 63` ```text {* ``` ballarin@13940 ` 64` ``` Properties of the set of polynomials @{term up}. ``` ballarin@13940 ` 65` ```*} ``` ballarin@13940 ` 66` ballarin@13940 ` 67` ```lemma mem_upI [intro]: ``` ballarin@13940 ` 68` ``` "[| !!n. f n \ carrier R; EX n. bound (zero R) n f |] ==> f \ up R" ``` ballarin@13940 ` 69` ``` by (simp add: up_def Pi_def) ``` ballarin@13940 ` 70` ballarin@13940 ` 71` ```lemma mem_upD [dest]: ``` ballarin@13940 ` 72` ``` "f \ up R ==> f n \ carrier R" ``` ballarin@13940 ` 73` ``` by (simp add: up_def Pi_def) ``` ballarin@13940 ` 74` ballarin@13940 ` 75` ```lemma (in cring) bound_upD [dest]: ``` ballarin@13940 ` 76` ``` "f \ up R ==> EX n. bound \ n f" ``` ballarin@13940 ` 77` ``` by (simp add: up_def) ``` ballarin@13940 ` 78` ballarin@13940 ` 79` ```lemma (in cring) up_one_closed: ``` ballarin@13940 ` 80` ``` "(%n. if n = 0 then \ else \) \ up R" ``` ballarin@13940 ` 81` ``` using up_def by force ``` ballarin@13940 ` 82` ballarin@13940 ` 83` ```lemma (in cring) up_smult_closed: ``` ballarin@13940 ` 84` ``` "[| a \ carrier R; p \ up R |] ==> (%i. a \ p i) \ up R" ``` ballarin@13940 ` 85` ``` by force ``` ballarin@13940 ` 86` ballarin@13940 ` 87` ```lemma (in cring) up_add_closed: ``` ballarin@13940 ` 88` ``` "[| p \ up R; q \ up R |] ==> (%i. p i \ q i) \ up R" ``` ballarin@13940 ` 89` ```proof ``` ballarin@13940 ` 90` ``` fix n ``` ballarin@13940 ` 91` ``` assume "p \ up R" and "q \ up R" ``` ballarin@13940 ` 92` ``` then show "p n \ q n \ carrier R" ``` ballarin@13940 ` 93` ``` by auto ``` ballarin@13940 ` 94` ```next ``` ballarin@13940 ` 95` ``` assume UP: "p \ up R" "q \ up R" ``` ballarin@13940 ` 96` ``` show "EX n. bound \ n (%i. p i \ q i)" ``` ballarin@13940 ` 97` ``` proof - ``` ballarin@13940 ` 98` ``` from UP obtain n where boundn: "bound \ n p" by fast ``` ballarin@13940 ` 99` ``` from UP obtain m where boundm: "bound \ m q" by fast ``` ballarin@13940 ` 100` ``` have "bound \ (max n m) (%i. p i \ q i)" ``` ballarin@13940 ` 101` ``` proof ``` ballarin@13940 ` 102` ``` fix i ``` ballarin@13940 ` 103` ``` assume "max n m < i" ``` ballarin@13940 ` 104` ``` with boundn and boundm and UP show "p i \ q i = \" by fastsimp ``` ballarin@13940 ` 105` ``` qed ``` ballarin@13940 ` 106` ``` then show ?thesis .. ``` ballarin@13940 ` 107` ``` qed ``` ballarin@13940 ` 108` ```qed ``` ballarin@13940 ` 109` ballarin@13940 ` 110` ```lemma (in cring) up_a_inv_closed: ``` ballarin@13940 ` 111` ``` "p \ up R ==> (%i. \ (p i)) \ up R" ``` ballarin@13940 ` 112` ```proof ``` ballarin@13940 ` 113` ``` assume R: "p \ up R" ``` ballarin@13940 ` 114` ``` then obtain n where "bound \ n p" by auto ``` ballarin@13940 ` 115` ``` then have "bound \ n (%i. \ p i)" by auto ``` ballarin@13940 ` 116` ``` then show "EX n. bound \ n (%i. \ p i)" by auto ``` ballarin@13940 ` 117` ```qed auto ``` ballarin@13940 ` 118` ballarin@13940 ` 119` ```lemma (in cring) up_mult_closed: ``` ballarin@13940 ` 120` ``` "[| p \ up R; q \ up R |] ==> ``` wenzelm@14666 ` 121` ``` (%n. \i \ {..n}. p i \ q (n-i)) \ up R" ``` ballarin@13940 ` 122` ```proof ``` ballarin@13940 ` 123` ``` fix n ``` ballarin@13940 ` 124` ``` assume "p \ up R" "q \ up R" ``` wenzelm@14666 ` 125` ``` then show "(\i \ {..n}. p i \ q (n-i)) \ carrier R" ``` ballarin@13940 ` 126` ``` by (simp add: mem_upD funcsetI) ``` ballarin@13940 ` 127` ```next ``` ballarin@13940 ` 128` ``` assume UP: "p \ up R" "q \ up R" ``` wenzelm@14666 ` 129` ``` show "EX n. bound \ n (%n. \i \ {..n}. p i \ q (n-i))" ``` ballarin@13940 ` 130` ``` proof - ``` ballarin@13940 ` 131` ``` from UP obtain n where boundn: "bound \ n p" by fast ``` ballarin@13940 ` 132` ``` from UP obtain m where boundm: "bound \ m q" by fast ``` wenzelm@14666 ` 133` ``` have "bound \ (n + m) (%n. \i \ {..n}. p i \ q (n - i))" ``` ballarin@13940 ` 134` ``` proof ``` wenzelm@14666 ` 135` ``` fix k assume bound: "n + m < k" ``` ballarin@13940 ` 136` ``` { ``` wenzelm@14666 ` 137` ``` fix i ``` wenzelm@14666 ` 138` ``` have "p i \ q (k-i) = \" ``` wenzelm@14666 ` 139` ``` proof (cases "n < i") ``` wenzelm@14666 ` 140` ``` case True ``` wenzelm@14666 ` 141` ``` with boundn have "p i = \" by auto ``` ballarin@13940 ` 142` ``` moreover from UP have "q (k-i) \ carrier R" by auto ``` wenzelm@14666 ` 143` ``` ultimately show ?thesis by simp ``` wenzelm@14666 ` 144` ``` next ``` wenzelm@14666 ` 145` ``` case False ``` wenzelm@14666 ` 146` ``` with bound have "m < k-i" by arith ``` wenzelm@14666 ` 147` ``` with boundm have "q (k-i) = \" by auto ``` wenzelm@14666 ` 148` ``` moreover from UP have "p i \ carrier R" by auto ``` wenzelm@14666 ` 149` ``` ultimately show ?thesis by simp ``` wenzelm@14666 ` 150` ``` qed ``` ballarin@13940 ` 151` ``` } ``` wenzelm@14666 ` 152` ``` then show "(\i \ {..k}. p i \ q (k-i)) = \" ``` wenzelm@14666 ` 153` ``` by (simp add: Pi_def) ``` ballarin@13940 ` 154` ``` qed ``` ballarin@13940 ` 155` ``` then show ?thesis by fast ``` ballarin@13940 ` 156` ``` qed ``` ballarin@13940 ` 157` ```qed ``` ballarin@13940 ` 158` wenzelm@14666 ` 159` ballarin@13940 ` 160` ```subsection {* Effect of operations on coefficients *} ``` ballarin@13940 ` 161` ballarin@13940 ` 162` ```locale UP = struct R + struct P + ``` ballarin@13940 ` 163` ``` defines P_def: "P == UP R" ``` ballarin@13940 ` 164` ballarin@13940 ` 165` ```locale UP_cring = UP + cring R ``` ballarin@13940 ` 166` ballarin@13940 ` 167` ```locale UP_domain = UP_cring + "domain" R ``` ballarin@13940 ` 168` ballarin@13940 ` 169` ```text {* ``` wenzelm@14651 ` 170` ``` Temporarily declare @{text UP.P_def} as simp rule. ``` wenzelm@14651 ` 171` ```*} (* TODO: use antiquotation once text (in locale) is supported. *) ``` ballarin@13940 ` 172` ballarin@13940 ` 173` ```declare (in UP) P_def [simp] ``` ballarin@13940 ` 174` ballarin@13940 ` 175` ```lemma (in UP_cring) coeff_monom [simp]: ``` ballarin@13940 ` 176` ``` "a \ carrier R ==> ``` ballarin@13940 ` 177` ``` coeff P (monom P a m) n = (if m=n then a else \)" ``` ballarin@13940 ` 178` ```proof - ``` ballarin@13940 ` 179` ``` assume R: "a \ carrier R" ``` ballarin@13940 ` 180` ``` then have "(%n. if n = m then a else \) \ up R" ``` ballarin@13940 ` 181` ``` using up_def by force ``` ballarin@13940 ` 182` ``` with R show ?thesis by (simp add: UP_def) ``` ballarin@13940 ` 183` ```qed ``` ballarin@13940 ` 184` ballarin@13940 ` 185` ```lemma (in UP_cring) coeff_zero [simp]: ``` ballarin@13940 ` 186` ``` "coeff P \\<^sub>2 n = \" ``` ballarin@13940 ` 187` ``` by (auto simp add: UP_def) ``` ballarin@13940 ` 188` ballarin@13940 ` 189` ```lemma (in UP_cring) coeff_one [simp]: ``` ballarin@13940 ` 190` ``` "coeff P \\<^sub>2 n = (if n=0 then \ else \)" ``` ballarin@13940 ` 191` ``` using up_one_closed by (simp add: UP_def) ``` ballarin@13940 ` 192` ballarin@13940 ` 193` ```lemma (in UP_cring) coeff_smult [simp]: ``` ballarin@13940 ` 194` ``` "[| a \ carrier R; p \ carrier P |] ==> ``` ballarin@13940 ` 195` ``` coeff P (a \\<^sub>2 p) n = a \ coeff P p n" ``` ballarin@13940 ` 196` ``` by (simp add: UP_def up_smult_closed) ``` ballarin@13940 ` 197` ballarin@13940 ` 198` ```lemma (in UP_cring) coeff_add [simp]: ``` ballarin@13940 ` 199` ``` "[| p \ carrier P; q \ carrier P |] ==> ``` ballarin@13940 ` 200` ``` coeff P (p \\<^sub>2 q) n = coeff P p n \ coeff P q n" ``` ballarin@13940 ` 201` ``` by (simp add: UP_def up_add_closed) ``` ballarin@13940 ` 202` ballarin@13940 ` 203` ```lemma (in UP_cring) coeff_mult [simp]: ``` ballarin@13940 ` 204` ``` "[| p \ carrier P; q \ carrier P |] ==> ``` wenzelm@14666 ` 205` ``` coeff P (p \\<^sub>2 q) n = (\i \ {..n}. coeff P p i \ coeff P q (n-i))" ``` ballarin@13940 ` 206` ``` by (simp add: UP_def up_mult_closed) ``` ballarin@13940 ` 207` ballarin@13940 ` 208` ```lemma (in UP) up_eqI: ``` ballarin@13940 ` 209` ``` assumes prem: "!!n. coeff P p n = coeff P q n" ``` ballarin@13940 ` 210` ``` and R: "p \ carrier P" "q \ carrier P" ``` ballarin@13940 ` 211` ``` shows "p = q" ``` ballarin@13940 ` 212` ```proof ``` ballarin@13940 ` 213` ``` fix x ``` ballarin@13940 ` 214` ``` from prem and R show "p x = q x" by (simp add: UP_def) ``` ballarin@13940 ` 215` ```qed ``` wenzelm@14666 ` 216` ballarin@13940 ` 217` ```subsection {* Polynomials form a commutative ring. *} ``` ballarin@13940 ` 218` wenzelm@14666 ` 219` ```text {* Operations are closed over @{term P}. *} ``` ballarin@13940 ` 220` ballarin@13940 ` 221` ```lemma (in UP_cring) UP_mult_closed [simp]: ``` ballarin@13940 ` 222` ``` "[| p \ carrier P; q \ carrier P |] ==> p \\<^sub>2 q \ carrier P" ``` ballarin@13940 ` 223` ``` by (simp add: UP_def up_mult_closed) ``` ballarin@13940 ` 224` ballarin@13940 ` 225` ```lemma (in UP_cring) UP_one_closed [simp]: ``` ballarin@13940 ` 226` ``` "\\<^sub>2 \ carrier P" ``` ballarin@13940 ` 227` ``` by (simp add: UP_def up_one_closed) ``` ballarin@13940 ` 228` ballarin@13940 ` 229` ```lemma (in UP_cring) UP_zero_closed [intro, simp]: ``` ballarin@13940 ` 230` ``` "\\<^sub>2 \ carrier P" ``` ballarin@13940 ` 231` ``` by (auto simp add: UP_def) ``` ballarin@13940 ` 232` ballarin@13940 ` 233` ```lemma (in UP_cring) UP_a_closed [intro, simp]: ``` ballarin@13940 ` 234` ``` "[| p \ carrier P; q \ carrier P |] ==> p \\<^sub>2 q \ carrier P" ``` ballarin@13940 ` 235` ``` by (simp add: UP_def up_add_closed) ``` ballarin@13940 ` 236` ballarin@13940 ` 237` ```lemma (in UP_cring) monom_closed [simp]: ``` ballarin@13940 ` 238` ``` "a \ carrier R ==> monom P a n \ carrier P" ``` ballarin@13940 ` 239` ``` by (auto simp add: UP_def up_def Pi_def) ``` ballarin@13940 ` 240` ballarin@13940 ` 241` ```lemma (in UP_cring) UP_smult_closed [simp]: ``` ballarin@13940 ` 242` ``` "[| a \ carrier R; p \ carrier P |] ==> a \\<^sub>2 p \ carrier P" ``` ballarin@13940 ` 243` ``` by (simp add: UP_def up_smult_closed) ``` ballarin@13940 ` 244` ballarin@13940 ` 245` ```lemma (in UP) coeff_closed [simp]: ``` ballarin@13940 ` 246` ``` "p \ carrier P ==> coeff P p n \ carrier R" ``` ballarin@13940 ` 247` ``` by (auto simp add: UP_def) ``` ballarin@13940 ` 248` ballarin@13940 ` 249` ```declare (in UP) P_def [simp del] ``` ballarin@13940 ` 250` ballarin@13940 ` 251` ```text {* Algebraic ring properties *} ``` ballarin@13940 ` 252` ballarin@13940 ` 253` ```lemma (in UP_cring) UP_a_assoc: ``` ballarin@13940 ` 254` ``` assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" ``` ballarin@13940 ` 255` ``` shows "(p \\<^sub>2 q) \\<^sub>2 r = p \\<^sub>2 (q \\<^sub>2 r)" ``` ballarin@13940 ` 256` ``` by (rule up_eqI, simp add: a_assoc R, simp_all add: R) ``` ballarin@13940 ` 257` ballarin@13940 ` 258` ```lemma (in UP_cring) UP_l_zero [simp]: ``` ballarin@13940 ` 259` ``` assumes R: "p \ carrier P" ``` ballarin@13940 ` 260` ``` shows "\\<^sub>2 \\<^sub>2 p = p" ``` ballarin@13940 ` 261` ``` by (rule up_eqI, simp_all add: R) ``` ballarin@13940 ` 262` ballarin@13940 ` 263` ```lemma (in UP_cring) UP_l_neg_ex: ``` ballarin@13940 ` 264` ``` assumes R: "p \ carrier P" ``` ballarin@13940 ` 265` ``` shows "EX q : carrier P. q \\<^sub>2 p = \\<^sub>2" ``` ballarin@13940 ` 266` ```proof - ``` ballarin@13940 ` 267` ``` let ?q = "%i. \ (p i)" ``` ballarin@13940 ` 268` ``` from R have closed: "?q \ carrier P" ``` ballarin@13940 ` 269` ``` by (simp add: UP_def P_def up_a_inv_closed) ``` ballarin@13940 ` 270` ``` from R have coeff: "!!n. coeff P ?q n = \ (coeff P p n)" ``` ballarin@13940 ` 271` ``` by (simp add: UP_def P_def up_a_inv_closed) ``` ballarin@13940 ` 272` ``` show ?thesis ``` ballarin@13940 ` 273` ``` proof ``` ballarin@13940 ` 274` ``` show "?q \\<^sub>2 p = \\<^sub>2" ``` ballarin@13940 ` 275` ``` by (auto intro!: up_eqI simp add: R closed coeff R.l_neg) ``` ballarin@13940 ` 276` ``` qed (rule closed) ``` ballarin@13940 ` 277` ```qed ``` ballarin@13940 ` 278` ballarin@13940 ` 279` ```lemma (in UP_cring) UP_a_comm: ``` ballarin@13940 ` 280` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@13940 ` 281` ``` shows "p \\<^sub>2 q = q \\<^sub>2 p" ``` ballarin@13940 ` 282` ``` by (rule up_eqI, simp add: a_comm R, simp_all add: R) ``` ballarin@13940 ` 283` ballarin@13940 ` 284` ```ML_setup {* ``` wenzelm@14590 ` 285` ``` simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; ``` wenzelm@14590 ` 286` ```*} ``` ballarin@13940 ` 287` ballarin@13940 ` 288` ```lemma (in UP_cring) UP_m_assoc: ``` ballarin@13940 ` 289` ``` assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" ``` ballarin@13940 ` 290` ``` shows "(p \\<^sub>2 q) \\<^sub>2 r = p \\<^sub>2 (q \\<^sub>2 r)" ``` ballarin@13940 ` 291` ```proof (rule up_eqI) ``` ballarin@13940 ` 292` ``` fix n ``` ballarin@13940 ` 293` ``` { ``` ballarin@13940 ` 294` ``` fix k and a b c :: "nat=>'a" ``` ballarin@13940 ` 295` ``` assume R: "a \ UNIV -> carrier R" "b \ UNIV -> carrier R" ``` ballarin@13940 ` 296` ``` "c \ UNIV -> carrier R" ``` ballarin@13940 ` 297` ``` then have "k <= n ==> ``` wenzelm@14666 ` 298` ``` (\j \ {..k}. (\i \ {..j}. a i \ b (j-i)) \ c (n-j)) = ``` wenzelm@14666 ` 299` ``` (\j \ {..k}. a j \ (\i \ {..k-j}. b i \ c (n-j-i)))" ``` wenzelm@14666 ` 300` ``` (concl is "?eq k") ``` ballarin@13940 ` 301` ``` proof (induct k) ``` ballarin@13940 ` 302` ``` case 0 then show ?case by (simp add: Pi_def m_assoc) ``` ballarin@13940 ` 303` ``` next ``` ballarin@13940 ` 304` ``` case (Suc k) ``` ballarin@13940 ` 305` ``` then have "k <= n" by arith ``` ballarin@13940 ` 306` ``` then have "?eq k" by (rule Suc) ``` ballarin@13940 ` 307` ``` with R show ?case ``` wenzelm@14666 ` 308` ``` by (simp cong: finsum_cong ``` ballarin@13940 ` 309` ``` add: Suc_diff_le Pi_def l_distr r_distr m_assoc) ``` ballarin@13940 ` 310` ``` (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc) ``` ballarin@13940 ` 311` ``` qed ``` ballarin@13940 ` 312` ``` } ``` ballarin@13940 ` 313` ``` with R show "coeff P ((p \\<^sub>2 q) \\<^sub>2 r) n = coeff P (p \\<^sub>2 (q \\<^sub>2 r)) n" ``` ballarin@13940 ` 314` ``` by (simp add: Pi_def) ``` ballarin@13940 ` 315` ```qed (simp_all add: R) ``` ballarin@13940 ` 316` ballarin@13940 ` 317` ```ML_setup {* ``` wenzelm@14590 ` 318` ``` simpset_ref() := simpset() setsubgoaler asm_simp_tac; ``` wenzelm@14590 ` 319` ```*} ``` ballarin@13940 ` 320` ballarin@13940 ` 321` ```lemma (in UP_cring) UP_l_one [simp]: ``` ballarin@13940 ` 322` ``` assumes R: "p \ carrier P" ``` ballarin@13940 ` 323` ``` shows "\\<^sub>2 \\<^sub>2 p = p" ``` ballarin@13940 ` 324` ```proof (rule up_eqI) ``` ballarin@13940 ` 325` ``` fix n ``` ballarin@13940 ` 326` ``` show "coeff P (\\<^sub>2 \\<^sub>2 p) n = coeff P p n" ``` ballarin@13940 ` 327` ``` proof (cases n) ``` ballarin@13940 ` 328` ``` case 0 with R show ?thesis by simp ``` ballarin@13940 ` 329` ``` next ``` ballarin@13940 ` 330` ``` case Suc with R show ?thesis ``` ballarin@13940 ` 331` ``` by (simp del: finsum_Suc add: finsum_Suc2 Pi_def) ``` ballarin@13940 ` 332` ``` qed ``` ballarin@13940 ` 333` ```qed (simp_all add: R) ``` ballarin@13940 ` 334` ballarin@13940 ` 335` ```lemma (in UP_cring) UP_l_distr: ``` ballarin@13940 ` 336` ``` assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" ``` ballarin@13940 ` 337` ``` shows "(p \\<^sub>2 q) \\<^sub>2 r = (p \\<^sub>2 r) \\<^sub>2 (q \\<^sub>2 r)" ``` ballarin@13940 ` 338` ``` by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R) ``` ballarin@13940 ` 339` ballarin@13940 ` 340` ```lemma (in UP_cring) UP_m_comm: ``` ballarin@13940 ` 341` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@13940 ` 342` ``` shows "p \\<^sub>2 q = q \\<^sub>2 p" ``` ballarin@13940 ` 343` ```proof (rule up_eqI) ``` wenzelm@14666 ` 344` ``` fix n ``` ballarin@13940 ` 345` ``` { ``` ballarin@13940 ` 346` ``` fix k and a b :: "nat=>'a" ``` ballarin@13940 ` 347` ``` assume R: "a \ UNIV -> carrier R" "b \ UNIV -> carrier R" ``` wenzelm@14666 ` 348` ``` then have "k <= n ==> ``` wenzelm@14666 ` 349` ``` (\i \ {..k}. a i \ b (n-i)) = ``` wenzelm@14666 ` 350` ``` (\i \ {..k}. a (k-i) \ b (i+n-k))" ``` wenzelm@14666 ` 351` ``` (concl is "?eq k") ``` ballarin@13940 ` 352` ``` proof (induct k) ``` ballarin@13940 ` 353` ``` case 0 then show ?case by (simp add: Pi_def) ``` ballarin@13940 ` 354` ``` next ``` ballarin@13940 ` 355` ``` case (Suc k) then show ?case ``` wenzelm@14666 ` 356` ``` by (subst finsum_Suc2) (simp add: Pi_def a_comm)+ ``` ballarin@13940 ` 357` ``` qed ``` ballarin@13940 ` 358` ``` } ``` ballarin@13940 ` 359` ``` note l = this ``` ballarin@13940 ` 360` ``` from R show "coeff P (p \\<^sub>2 q) n = coeff P (q \\<^sub>2 p) n" ``` ballarin@13940 ` 361` ``` apply (simp add: Pi_def) ``` ballarin@13940 ` 362` ``` apply (subst l) ``` ballarin@13940 ` 363` ``` apply (auto simp add: Pi_def) ``` ballarin@13940 ` 364` ``` apply (simp add: m_comm) ``` ballarin@13940 ` 365` ``` done ``` ballarin@13940 ` 366` ```qed (simp_all add: R) ``` ballarin@13940 ` 367` ballarin@13940 ` 368` ```theorem (in UP_cring) UP_cring: ``` ballarin@13940 ` 369` ``` "cring P" ``` ballarin@13940 ` 370` ``` by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero ``` ballarin@13940 ` 371` ``` UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr) ``` ballarin@13940 ` 372` ballarin@14399 ` 373` ```lemma (in UP_cring) UP_ring: (* preliminary *) ``` ballarin@14399 ` 374` ``` "ring P" ``` ballarin@14399 ` 375` ``` by (auto intro: ring.intro cring.axioms UP_cring) ``` ballarin@14399 ` 376` ballarin@13940 ` 377` ```lemma (in UP_cring) UP_a_inv_closed [intro, simp]: ``` ballarin@13940 ` 378` ``` "p \ carrier P ==> \\<^sub>2 p \ carrier P" ``` ballarin@13940 ` 379` ``` by (rule abelian_group.a_inv_closed ``` ballarin@14399 ` 380` ``` [OF ring.is_abelian_group [OF UP_ring]]) ``` ballarin@13940 ` 381` ballarin@13940 ` 382` ```lemma (in UP_cring) coeff_a_inv [simp]: ``` ballarin@13940 ` 383` ``` assumes R: "p \ carrier P" ``` ballarin@13940 ` 384` ``` shows "coeff P (\\<^sub>2 p) n = \ (coeff P p n)" ``` ballarin@13940 ` 385` ```proof - ``` ballarin@13940 ` 386` ``` from R coeff_closed UP_a_inv_closed have ``` ballarin@13940 ` 387` ``` "coeff P (\\<^sub>2 p) n = \ coeff P p n \ (coeff P p n \ coeff P (\\<^sub>2 p) n)" ``` ballarin@13940 ` 388` ``` by algebra ``` ballarin@13940 ` 389` ``` also from R have "... = \ (coeff P p n)" ``` ballarin@13940 ` 390` ``` by (simp del: coeff_add add: coeff_add [THEN sym] ``` ballarin@14399 ` 391` ``` abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]]) ``` ballarin@13940 ` 392` ``` finally show ?thesis . ``` ballarin@13940 ` 393` ```qed ``` ballarin@13940 ` 394` ballarin@13940 ` 395` ```text {* ``` ballarin@13940 ` 396` ``` Instantiation of lemmas from @{term cring}. ``` ballarin@13940 ` 397` ```*} ``` ballarin@13940 ` 398` ballarin@13940 ` 399` ```lemma (in UP_cring) UP_monoid: ``` ballarin@13940 ` 400` ``` "monoid P" ``` ballarin@13940 ` 401` ``` by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro ``` ballarin@13940 ` 402` ``` UP_cring) ``` ballarin@13940 ` 403` ```(* TODO: provide cring.is_monoid *) ``` ballarin@13940 ` 404` ballarin@13940 ` 405` ```lemma (in UP_cring) UP_comm_semigroup: ``` ballarin@13940 ` 406` ``` "comm_semigroup P" ``` ballarin@13940 ` 407` ``` by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro ``` ballarin@13940 ` 408` ``` UP_cring) ``` ballarin@13940 ` 409` ballarin@13940 ` 410` ```lemma (in UP_cring) UP_comm_monoid: ``` ballarin@13940 ` 411` ``` "comm_monoid P" ``` ballarin@13940 ` 412` ``` by (fast intro!: cring.is_comm_monoid UP_cring) ``` ballarin@13940 ` 413` ballarin@13940 ` 414` ```lemma (in UP_cring) UP_abelian_monoid: ``` ballarin@13940 ` 415` ``` "abelian_monoid P" ``` ballarin@14399 ` 416` ``` by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring) ``` ballarin@13940 ` 417` ballarin@13940 ` 418` ```lemma (in UP_cring) UP_abelian_group: ``` ballarin@13940 ` 419` ``` "abelian_group P" ``` ballarin@14399 ` 420` ``` by (fast intro!: ring.is_abelian_group UP_ring) ``` ballarin@13940 ` 421` ballarin@13940 ` 422` ```lemmas (in UP_cring) UP_r_one [simp] = ``` ballarin@13940 ` 423` ``` monoid.r_one [OF UP_monoid] ``` ballarin@13940 ` 424` ballarin@13940 ` 425` ```lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] = ``` ballarin@13940 ` 426` ``` monoid.nat_pow_closed [OF UP_monoid] ``` ballarin@13940 ` 427` ballarin@13940 ` 428` ```lemmas (in UP_cring) UP_nat_pow_0 [simp] = ``` ballarin@13940 ` 429` ``` monoid.nat_pow_0 [OF UP_monoid] ``` ballarin@13940 ` 430` ballarin@13940 ` 431` ```lemmas (in UP_cring) UP_nat_pow_Suc [simp] = ``` ballarin@13940 ` 432` ``` monoid.nat_pow_Suc [OF UP_monoid] ``` ballarin@13940 ` 433` ballarin@13940 ` 434` ```lemmas (in UP_cring) UP_nat_pow_one [simp] = ``` ballarin@13940 ` 435` ``` monoid.nat_pow_one [OF UP_monoid] ``` ballarin@13940 ` 436` ballarin@13940 ` 437` ```lemmas (in UP_cring) UP_nat_pow_mult = ``` ballarin@13940 ` 438` ``` monoid.nat_pow_mult [OF UP_monoid] ``` ballarin@13940 ` 439` ballarin@13940 ` 440` ```lemmas (in UP_cring) UP_nat_pow_pow = ``` ballarin@13940 ` 441` ``` monoid.nat_pow_pow [OF UP_monoid] ``` ballarin@13940 ` 442` ballarin@13940 ` 443` ```lemmas (in UP_cring) UP_m_lcomm = ``` ballarin@13940 ` 444` ``` comm_semigroup.m_lcomm [OF UP_comm_semigroup] ``` ballarin@13940 ` 445` ballarin@13940 ` 446` ```lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm ``` ballarin@13940 ` 447` ballarin@13940 ` 448` ```lemmas (in UP_cring) UP_nat_pow_distr = ``` ballarin@13940 ` 449` ``` comm_monoid.nat_pow_distr [OF UP_comm_monoid] ``` ballarin@13940 ` 450` ballarin@13940 ` 451` ```lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid] ``` ballarin@13940 ` 452` ballarin@13940 ` 453` ```lemmas (in UP_cring) UP_r_zero [simp] = ``` ballarin@13940 ` 454` ``` abelian_monoid.r_zero [OF UP_abelian_monoid] ``` ballarin@13940 ` 455` ballarin@13940 ` 456` ```lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm ``` ballarin@13940 ` 457` ballarin@13940 ` 458` ```lemmas (in UP_cring) UP_finsum_empty [simp] = ``` ballarin@13940 ` 459` ``` abelian_monoid.finsum_empty [OF UP_abelian_monoid] ``` ballarin@13940 ` 460` ballarin@13940 ` 461` ```lemmas (in UP_cring) UP_finsum_insert [simp] = ``` ballarin@13940 ` 462` ``` abelian_monoid.finsum_insert [OF UP_abelian_monoid] ``` ballarin@13940 ` 463` ballarin@13940 ` 464` ```lemmas (in UP_cring) UP_finsum_zero [simp] = ``` ballarin@13940 ` 465` ``` abelian_monoid.finsum_zero [OF UP_abelian_monoid] ``` ballarin@13940 ` 466` ballarin@13940 ` 467` ```lemmas (in UP_cring) UP_finsum_closed [simp] = ``` ballarin@13940 ` 468` ``` abelian_monoid.finsum_closed [OF UP_abelian_monoid] ``` ballarin@13940 ` 469` ballarin@13940 ` 470` ```lemmas (in UP_cring) UP_finsum_Un_Int = ``` ballarin@13940 ` 471` ``` abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid] ``` ballarin@13940 ` 472` ballarin@13940 ` 473` ```lemmas (in UP_cring) UP_finsum_Un_disjoint = ``` ballarin@13940 ` 474` ``` abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid] ``` ballarin@13940 ` 475` ballarin@13940 ` 476` ```lemmas (in UP_cring) UP_finsum_addf = ``` ballarin@13940 ` 477` ``` abelian_monoid.finsum_addf [OF UP_abelian_monoid] ``` ballarin@13940 ` 478` ballarin@13940 ` 479` ```lemmas (in UP_cring) UP_finsum_cong' = ``` ballarin@13940 ` 480` ``` abelian_monoid.finsum_cong' [OF UP_abelian_monoid] ``` ballarin@13940 ` 481` ballarin@13940 ` 482` ```lemmas (in UP_cring) UP_finsum_0 [simp] = ``` ballarin@13940 ` 483` ``` abelian_monoid.finsum_0 [OF UP_abelian_monoid] ``` ballarin@13940 ` 484` ballarin@13940 ` 485` ```lemmas (in UP_cring) UP_finsum_Suc [simp] = ``` ballarin@13940 ` 486` ``` abelian_monoid.finsum_Suc [OF UP_abelian_monoid] ``` ballarin@13940 ` 487` ballarin@13940 ` 488` ```lemmas (in UP_cring) UP_finsum_Suc2 = ``` ballarin@13940 ` 489` ``` abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid] ``` ballarin@13940 ` 490` ballarin@13940 ` 491` ```lemmas (in UP_cring) UP_finsum_add [simp] = ``` ballarin@13940 ` 492` ``` abelian_monoid.finsum_add [OF UP_abelian_monoid] ``` ballarin@13940 ` 493` ballarin@13940 ` 494` ```lemmas (in UP_cring) UP_finsum_cong = ``` ballarin@13940 ` 495` ``` abelian_monoid.finsum_cong [OF UP_abelian_monoid] ``` ballarin@13940 ` 496` ballarin@13940 ` 497` ```lemmas (in UP_cring) UP_minus_closed [intro, simp] = ``` ballarin@13940 ` 498` ``` abelian_group.minus_closed [OF UP_abelian_group] ``` ballarin@13940 ` 499` ballarin@13940 ` 500` ```lemmas (in UP_cring) UP_a_l_cancel [simp] = ``` ballarin@13940 ` 501` ``` abelian_group.a_l_cancel [OF UP_abelian_group] ``` ballarin@13940 ` 502` ballarin@13940 ` 503` ```lemmas (in UP_cring) UP_a_r_cancel [simp] = ``` ballarin@13940 ` 504` ``` abelian_group.a_r_cancel [OF UP_abelian_group] ``` ballarin@13940 ` 505` ballarin@13940 ` 506` ```lemmas (in UP_cring) UP_l_neg = ``` ballarin@13940 ` 507` ``` abelian_group.l_neg [OF UP_abelian_group] ``` ballarin@13940 ` 508` ballarin@13940 ` 509` ```lemmas (in UP_cring) UP_r_neg = ``` ballarin@13940 ` 510` ``` abelian_group.r_neg [OF UP_abelian_group] ``` ballarin@13940 ` 511` ballarin@13940 ` 512` ```lemmas (in UP_cring) UP_minus_zero [simp] = ``` ballarin@13940 ` 513` ``` abelian_group.minus_zero [OF UP_abelian_group] ``` ballarin@13940 ` 514` ballarin@13940 ` 515` ```lemmas (in UP_cring) UP_minus_minus [simp] = ``` ballarin@13940 ` 516` ``` abelian_group.minus_minus [OF UP_abelian_group] ``` ballarin@13940 ` 517` ballarin@13940 ` 518` ```lemmas (in UP_cring) UP_minus_add = ``` ballarin@13940 ` 519` ``` abelian_group.minus_add [OF UP_abelian_group] ``` ballarin@13940 ` 520` ballarin@13940 ` 521` ```lemmas (in UP_cring) UP_r_neg2 = ``` ballarin@13940 ` 522` ``` abelian_group.r_neg2 [OF UP_abelian_group] ``` ballarin@13940 ` 523` ballarin@13940 ` 524` ```lemmas (in UP_cring) UP_r_neg1 = ``` ballarin@13940 ` 525` ``` abelian_group.r_neg1 [OF UP_abelian_group] ``` ballarin@13940 ` 526` ballarin@13940 ` 527` ```lemmas (in UP_cring) UP_r_distr = ``` ballarin@14399 ` 528` ``` ring.r_distr [OF UP_ring] ``` ballarin@13940 ` 529` ballarin@13940 ` 530` ```lemmas (in UP_cring) UP_l_null [simp] = ``` ballarin@14399 ` 531` ``` ring.l_null [OF UP_ring] ``` ballarin@13940 ` 532` ballarin@13940 ` 533` ```lemmas (in UP_cring) UP_r_null [simp] = ``` ballarin@14399 ` 534` ``` ring.r_null [OF UP_ring] ``` ballarin@13940 ` 535` ballarin@13940 ` 536` ```lemmas (in UP_cring) UP_l_minus = ``` ballarin@14399 ` 537` ``` ring.l_minus [OF UP_ring] ``` ballarin@13940 ` 538` ballarin@13940 ` 539` ```lemmas (in UP_cring) UP_r_minus = ``` ballarin@14399 ` 540` ``` ring.r_minus [OF UP_ring] ``` ballarin@13940 ` 541` ballarin@13940 ` 542` ```lemmas (in UP_cring) UP_finsum_ldistr = ``` ballarin@13940 ` 543` ``` cring.finsum_ldistr [OF UP_cring] ``` ballarin@13940 ` 544` ballarin@13940 ` 545` ```lemmas (in UP_cring) UP_finsum_rdistr = ``` ballarin@13940 ` 546` ``` cring.finsum_rdistr [OF UP_cring] ``` ballarin@13940 ` 547` wenzelm@14666 ` 548` ballarin@13940 ` 549` ```subsection {* Polynomials form an Algebra *} ``` ballarin@13940 ` 550` ballarin@13940 ` 551` ```lemma (in UP_cring) UP_smult_l_distr: ``` ballarin@13940 ` 552` ``` "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==> ``` ballarin@13940 ` 553` ``` (a \ b) \\<^sub>2 p = a \\<^sub>2 p \\<^sub>2 b \\<^sub>2 p" ``` ballarin@13940 ` 554` ``` by (rule up_eqI) (simp_all add: R.l_distr) ``` ballarin@13940 ` 555` ballarin@13940 ` 556` ```lemma (in UP_cring) UP_smult_r_distr: ``` ballarin@13940 ` 557` ``` "[| a \ carrier R; p \ carrier P; q \ carrier P |] ==> ``` ballarin@13940 ` 558` ``` a \\<^sub>2 (p \\<^sub>2 q) = a \\<^sub>2 p \\<^sub>2 a \\<^sub>2 q" ``` ballarin@13940 ` 559` ``` by (rule up_eqI) (simp_all add: R.r_distr) ``` ballarin@13940 ` 560` ballarin@13940 ` 561` ```lemma (in UP_cring) UP_smult_assoc1: ``` ballarin@13940 ` 562` ``` "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==> ``` ballarin@13940 ` 563` ``` (a \ b) \\<^sub>2 p = a \\<^sub>2 (b \\<^sub>2 p)" ``` ballarin@13940 ` 564` ``` by (rule up_eqI) (simp_all add: R.m_assoc) ``` ballarin@13940 ` 565` ballarin@13940 ` 566` ```lemma (in UP_cring) UP_smult_one [simp]: ``` ballarin@13940 ` 567` ``` "p \ carrier P ==> \ \\<^sub>2 p = p" ``` ballarin@13940 ` 568` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 569` ballarin@13940 ` 570` ```lemma (in UP_cring) UP_smult_assoc2: ``` ballarin@13940 ` 571` ``` "[| a \ carrier R; p \ carrier P; q \ carrier P |] ==> ``` ballarin@13940 ` 572` ``` (a \\<^sub>2 p) \\<^sub>2 q = a \\<^sub>2 (p \\<^sub>2 q)" ``` ballarin@13940 ` 573` ``` by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def) ``` ballarin@13940 ` 574` ballarin@13940 ` 575` ```text {* ``` ballarin@13940 ` 576` ``` Instantiation of lemmas from @{term algebra}. ``` ballarin@13940 ` 577` ```*} ``` ballarin@13940 ` 578` ballarin@13940 ` 579` ```(* TODO: move to CRing.thy, really a fact missing from the locales package *) ``` ballarin@13940 ` 580` ballarin@13940 ` 581` ```lemma (in cring) cring: ``` ballarin@13940 ` 582` ``` "cring R" ``` ballarin@13940 ` 583` ``` by (fast intro: cring.intro prems) ``` ballarin@13940 ` 584` ballarin@13940 ` 585` ```lemma (in UP_cring) UP_algebra: ``` ballarin@13940 ` 586` ``` "algebra R P" ``` ballarin@13940 ` 587` ``` by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr ``` ballarin@13940 ` 588` ``` UP_smult_assoc1 UP_smult_assoc2) ``` ballarin@13940 ` 589` ballarin@13940 ` 590` ```lemmas (in UP_cring) UP_smult_l_null [simp] = ``` ballarin@13940 ` 591` ``` algebra.smult_l_null [OF UP_algebra] ``` ballarin@13940 ` 592` ballarin@13940 ` 593` ```lemmas (in UP_cring) UP_smult_r_null [simp] = ``` ballarin@13940 ` 594` ``` algebra.smult_r_null [OF UP_algebra] ``` ballarin@13940 ` 595` ballarin@13940 ` 596` ```lemmas (in UP_cring) UP_smult_l_minus = ``` ballarin@13940 ` 597` ``` algebra.smult_l_minus [OF UP_algebra] ``` ballarin@13940 ` 598` ballarin@13940 ` 599` ```lemmas (in UP_cring) UP_smult_r_minus = ``` ballarin@13940 ` 600` ``` algebra.smult_r_minus [OF UP_algebra] ``` ballarin@13940 ` 601` ballarin@13949 ` 602` ```subsection {* Further lemmas involving monomials *} ``` ballarin@13940 ` 603` ballarin@13940 ` 604` ```lemma (in UP_cring) monom_zero [simp]: ``` ballarin@13940 ` 605` ``` "monom P \ n = \\<^sub>2" ``` ballarin@13940 ` 606` ``` by (simp add: UP_def P_def) ``` ballarin@13940 ` 607` ballarin@13940 ` 608` ```ML_setup {* ``` wenzelm@14590 ` 609` ``` simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; ``` wenzelm@14590 ` 610` ```*} ``` ballarin@13940 ` 611` ballarin@13940 ` 612` ```lemma (in UP_cring) monom_mult_is_smult: ``` ballarin@13940 ` 613` ``` assumes R: "a \ carrier R" "p \ carrier P" ``` ballarin@13940 ` 614` ``` shows "monom P a 0 \\<^sub>2 p = a \\<^sub>2 p" ``` ballarin@13940 ` 615` ```proof (rule up_eqI) ``` ballarin@13940 ` 616` ``` fix n ``` ballarin@13940 ` 617` ``` have "coeff P (p \\<^sub>2 monom P a 0) n = coeff P (a \\<^sub>2 p) n" ``` ballarin@13940 ` 618` ``` proof (cases n) ``` ballarin@13940 ` 619` ``` case 0 with R show ?thesis by (simp add: R.m_comm) ``` ballarin@13940 ` 620` ``` next ``` ballarin@13940 ` 621` ``` case Suc with R show ?thesis ``` ballarin@13940 ` 622` ``` by (simp cong: finsum_cong add: R.r_null Pi_def) ``` ballarin@13940 ` 623` ``` (simp add: m_comm) ``` ballarin@13940 ` 624` ``` qed ``` ballarin@13940 ` 625` ``` with R show "coeff P (monom P a 0 \\<^sub>2 p) n = coeff P (a \\<^sub>2 p) n" ``` ballarin@13940 ` 626` ``` by (simp add: UP_m_comm) ``` ballarin@13940 ` 627` ```qed (simp_all add: R) ``` ballarin@13940 ` 628` ballarin@13940 ` 629` ```ML_setup {* ``` wenzelm@14590 ` 630` ``` simpset_ref() := simpset() setsubgoaler asm_simp_tac; ``` wenzelm@14590 ` 631` ```*} ``` ballarin@13940 ` 632` ballarin@13940 ` 633` ```lemma (in UP_cring) monom_add [simp]: ``` ballarin@13940 ` 634` ``` "[| a \ carrier R; b \ carrier R |] ==> ``` ballarin@13940 ` 635` ``` monom P (a \ b) n = monom P a n \\<^sub>2 monom P b n" ``` ballarin@13940 ` 636` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 637` ballarin@13940 ` 638` ```ML_setup {* ``` wenzelm@14590 ` 639` ``` simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; ``` wenzelm@14590 ` 640` ```*} ``` ballarin@13940 ` 641` ballarin@13940 ` 642` ```lemma (in UP_cring) monom_one_Suc: ``` ballarin@13940 ` 643` ``` "monom P \ (Suc n) = monom P \ n \\<^sub>2 monom P \ 1" ``` ballarin@13940 ` 644` ```proof (rule up_eqI) ``` ballarin@13940 ` 645` ``` fix k ``` ballarin@13940 ` 646` ``` show "coeff P (monom P \ (Suc n)) k = coeff P (monom P \ n \\<^sub>2 monom P \ 1) k" ``` ballarin@13940 ` 647` ``` proof (cases "k = Suc n") ``` ballarin@13940 ` 648` ``` case True show ?thesis ``` ballarin@13940 ` 649` ``` proof - ``` wenzelm@14666 ` 650` ``` from True have less_add_diff: ``` wenzelm@14666 ` 651` ``` "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith ``` ballarin@13940 ` 652` ``` from True have "coeff P (monom P \ (Suc n)) k = \" by simp ``` ballarin@13940 ` 653` ``` also from True ``` wenzelm@14666 ` 654` ``` have "... = (\i \ {..n(} \ {n}. coeff P (monom P \ n) i \ ``` wenzelm@14666 ` 655` ``` coeff P (monom P \ 1) (k - i))" ``` wenzelm@14666 ` 656` ``` by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def) ``` wenzelm@14666 ` 657` ``` also have "... = (\i \ {..n}. coeff P (monom P \ n) i \ ``` wenzelm@14666 ` 658` ``` coeff P (monom P \ 1) (k - i))" ``` wenzelm@14666 ` 659` ``` by (simp only: ivl_disj_un_singleton) ``` wenzelm@14666 ` 660` ``` also from True have "... = (\i \ {..n} \ {)n..k}. coeff P (monom P \ n) i \ ``` wenzelm@14666 ` 661` ``` coeff P (monom P \ 1) (k - i))" ``` wenzelm@14666 ` 662` ``` by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one ``` wenzelm@14666 ` 663` ``` order_less_imp_not_eq Pi_def) ``` ballarin@13940 ` 664` ``` also from True have "... = coeff P (monom P \ n \\<^sub>2 monom P \ 1) k" ``` wenzelm@14666 ` 665` ``` by (simp add: ivl_disj_un_one) ``` ballarin@13940 ` 666` ``` finally show ?thesis . ``` ballarin@13940 ` 667` ``` qed ``` ballarin@13940 ` 668` ``` next ``` ballarin@13940 ` 669` ``` case False ``` ballarin@13940 ` 670` ``` note neq = False ``` ballarin@13940 ` 671` ``` let ?s = ``` wenzelm@14666 ` 672` ``` "\i. (if n = i then \ else \) \ (if Suc 0 = k - i then \ else \)" ``` ballarin@13940 ` 673` ``` from neq have "coeff P (monom P \ (Suc n)) k = \" by simp ``` wenzelm@14666 ` 674` ``` also have "... = (\i \ {..k}. ?s i)" ``` ballarin@13940 ` 675` ``` proof - ``` wenzelm@14666 ` 676` ``` have f1: "(\i \ {..n(}. ?s i) = \" by (simp cong: finsum_cong add: Pi_def) ``` wenzelm@14666 ` 677` ``` from neq have f2: "(\i \ {n}. ?s i) = \" ``` wenzelm@14666 ` 678` ``` by (simp cong: finsum_cong add: Pi_def) arith ``` wenzelm@14666 ` 679` ``` have f3: "n < k ==> (\i \ {)n..k}. ?s i) = \" ``` wenzelm@14666 ` 680` ``` by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def) ``` ballarin@13940 ` 681` ``` show ?thesis ``` ballarin@13940 ` 682` ``` proof (cases "k < n") ``` wenzelm@14666 ` 683` ``` case True then show ?thesis by (simp cong: finsum_cong add: Pi_def) ``` ballarin@13940 ` 684` ``` next ``` wenzelm@14666 ` 685` ``` case False then have n_le_k: "n <= k" by arith ``` wenzelm@14666 ` 686` ``` show ?thesis ``` wenzelm@14666 ` 687` ``` proof (cases "n = k") ``` wenzelm@14666 ` 688` ``` case True ``` wenzelm@14666 ` 689` ``` then have "\ = (\i \ {..n(} \ {n}. ?s i)" ``` wenzelm@14666 ` 690` ``` by (simp cong: finsum_cong add: finsum_Un_disjoint ``` wenzelm@14666 ` 691` ``` ivl_disj_int_singleton Pi_def) ``` wenzelm@14666 ` 692` ``` also from True have "... = (\i \ {..k}. ?s i)" ``` wenzelm@14666 ` 693` ``` by (simp only: ivl_disj_un_singleton) ``` wenzelm@14666 ` 694` ``` finally show ?thesis . ``` wenzelm@14666 ` 695` ``` next ``` wenzelm@14666 ` 696` ``` case False with n_le_k have n_less_k: "n < k" by arith ``` wenzelm@14666 ` 697` ``` with neq have "\ = (\i \ {..n(} \ {n}. ?s i)" ``` wenzelm@14666 ` 698` ``` by (simp add: finsum_Un_disjoint f1 f2 ``` wenzelm@14666 ` 699` ``` ivl_disj_int_singleton Pi_def del: Un_insert_right) ``` wenzelm@14666 ` 700` ``` also have "... = (\i \ {..n}. ?s i)" ``` wenzelm@14666 ` 701` ``` by (simp only: ivl_disj_un_singleton) ``` wenzelm@14666 ` 702` ``` also from n_less_k neq have "... = (\i \ {..n} \ {)n..k}. ?s i)" ``` wenzelm@14666 ` 703` ``` by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def) ``` wenzelm@14666 ` 704` ``` also from n_less_k have "... = (\i \ {..k}. ?s i)" ``` wenzelm@14666 ` 705` ``` by (simp only: ivl_disj_un_one) ``` wenzelm@14666 ` 706` ``` finally show ?thesis . ``` wenzelm@14666 ` 707` ``` qed ``` ballarin@13940 ` 708` ``` qed ``` ballarin@13940 ` 709` ``` qed ``` ballarin@13940 ` 710` ``` also have "... = coeff P (monom P \ n \\<^sub>2 monom P \ 1) k" by simp ``` ballarin@13940 ` 711` ``` finally show ?thesis . ``` ballarin@13940 ` 712` ``` qed ``` ballarin@13940 ` 713` ```qed (simp_all) ``` ballarin@13940 ` 714` ballarin@13940 ` 715` ```ML_setup {* ``` wenzelm@14590 ` 716` ``` simpset_ref() := simpset() setsubgoaler asm_simp_tac; ``` wenzelm@14590 ` 717` ```*} ``` ballarin@13940 ` 718` ballarin@13940 ` 719` ```lemma (in UP_cring) monom_mult_smult: ``` ballarin@13940 ` 720` ``` "[| a \ carrier R; b \ carrier R |] ==> monom P (a \ b) n = a \\<^sub>2 monom P b n" ``` ballarin@13940 ` 721` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 722` ballarin@13940 ` 723` ```lemma (in UP_cring) monom_one [simp]: ``` ballarin@13940 ` 724` ``` "monom P \ 0 = \\<^sub>2" ``` ballarin@13940 ` 725` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 726` ballarin@13940 ` 727` ```lemma (in UP_cring) monom_one_mult: ``` ballarin@13940 ` 728` ``` "monom P \ (n + m) = monom P \ n \\<^sub>2 monom P \ m" ``` ballarin@13940 ` 729` ```proof (induct n) ``` ballarin@13940 ` 730` ``` case 0 show ?case by simp ``` ballarin@13940 ` 731` ```next ``` ballarin@13940 ` 732` ``` case Suc then show ?case ``` ballarin@13940 ` 733` ``` by (simp only: add_Suc monom_one_Suc) (simp add: UP_m_ac) ``` ballarin@13940 ` 734` ```qed ``` ballarin@13940 ` 735` ballarin@13940 ` 736` ```lemma (in UP_cring) monom_mult [simp]: ``` ballarin@13940 ` 737` ``` assumes R: "a \ carrier R" "b \ carrier R" ``` ballarin@13940 ` 738` ``` shows "monom P (a \ b) (n + m) = monom P a n \\<^sub>2 monom P b m" ``` ballarin@13940 ` 739` ```proof - ``` ballarin@13940 ` 740` ``` from R have "monom P (a \ b) (n + m) = monom P (a \ b \ \) (n + m)" by simp ``` ballarin@13940 ` 741` ``` also from R have "... = a \ b \\<^sub>2 monom P \ (n + m)" ``` ballarin@13940 ` 742` ``` by (simp add: monom_mult_smult del: r_one) ``` ballarin@13940 ` 743` ``` also have "... = a \ b \\<^sub>2 (monom P \ n \\<^sub>2 monom P \ m)" ``` ballarin@13940 ` 744` ``` by (simp only: monom_one_mult) ``` ballarin@13940 ` 745` ``` also from R have "... = a \\<^sub>2 (b \\<^sub>2 (monom P \ n \\<^sub>2 monom P \ m))" ``` ballarin@13940 ` 746` ``` by (simp add: UP_smult_assoc1) ``` ballarin@13940 ` 747` ``` also from R have "... = a \\<^sub>2 (b \\<^sub>2 (monom P \ m \\<^sub>2 monom P \ n))" ``` ballarin@13940 ` 748` ``` by (simp add: UP_m_comm) ``` ballarin@13940 ` 749` ``` also from R have "... = a \\<^sub>2 ((b \\<^sub>2 monom P \ m) \\<^sub>2 monom P \ n)" ``` ballarin@13940 ` 750` ``` by (simp add: UP_smult_assoc2) ``` ballarin@13940 ` 751` ``` also from R have "... = a \\<^sub>2 (monom P \ n \\<^sub>2 (b \\<^sub>2 monom P \ m))" ``` ballarin@13940 ` 752` ``` by (simp add: UP_m_comm) ``` ballarin@13940 ` 753` ``` also from R have "... = (a \\<^sub>2 monom P \ n) \\<^sub>2 (b \\<^sub>2 monom P \ m)" ``` ballarin@13940 ` 754` ``` by (simp add: UP_smult_assoc2) ``` ballarin@13940 ` 755` ``` also from R have "... = monom P (a \ \) n \\<^sub>2 monom P (b \ \) m" ``` ballarin@13940 ` 756` ``` by (simp add: monom_mult_smult del: r_one) ``` ballarin@13940 ` 757` ``` also from R have "... = monom P a n \\<^sub>2 monom P b m" by simp ``` ballarin@13940 ` 758` ``` finally show ?thesis . ``` ballarin@13940 ` 759` ```qed ``` ballarin@13940 ` 760` ballarin@13940 ` 761` ```lemma (in UP_cring) monom_a_inv [simp]: ``` ballarin@13940 ` 762` ``` "a \ carrier R ==> monom P (\ a) n = \\<^sub>2 monom P a n" ``` ballarin@13940 ` 763` ``` by (rule up_eqI) simp_all ``` ballarin@13940 ` 764` ballarin@13940 ` 765` ```lemma (in UP_cring) monom_inj: ``` ballarin@13940 ` 766` ``` "inj_on (%a. monom P a n) (carrier R)" ``` ballarin@13940 ` 767` ```proof (rule inj_onI) ``` ballarin@13940 ` 768` ``` fix x y ``` ballarin@13940 ` 769` ``` assume R: "x \ carrier R" "y \ carrier R" and eq: "monom P x n = monom P y n" ``` ballarin@13940 ` 770` ``` then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp ``` ballarin@13940 ` 771` ``` with R show "x = y" by simp ``` ballarin@13940 ` 772` ```qed ``` ballarin@13940 ` 773` ballarin@13949 ` 774` ```subsection {* The degree function *} ``` ballarin@13940 ` 775` wenzelm@14651 ` 776` ```constdefs (structure R) ``` wenzelm@14651 ` 777` ``` deg :: "[_, nat => 'a] => nat" ``` wenzelm@14651 ` 778` ``` "deg R p == LEAST n. bound \ n (coeff (UP R) p)" ``` ballarin@13940 ` 779` ballarin@13940 ` 780` ```lemma (in UP_cring) deg_aboveI: ``` wenzelm@14666 ` 781` ``` "[| (!!m. n < m ==> coeff P p m = \); p \ carrier P |] ==> deg R p <= n" ``` ballarin@13940 ` 782` ``` by (unfold deg_def P_def) (fast intro: Least_le) ``` ballarin@13940 ` 783` ```(* ``` ballarin@13940 ` 784` ```lemma coeff_bound_ex: "EX n. bound n (coeff p)" ``` ballarin@13940 ` 785` ```proof - ``` ballarin@13940 ` 786` ``` have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) ``` ballarin@13940 ` 787` ``` then obtain n where "bound n (coeff p)" by (unfold UP_def) fast ``` ballarin@13940 ` 788` ``` then show ?thesis .. ``` ballarin@13940 ` 789` ```qed ``` wenzelm@14666 ` 790` ballarin@13940 ` 791` ```lemma bound_coeff_obtain: ``` ballarin@13940 ` 792` ``` assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P" ``` ballarin@13940 ` 793` ```proof - ``` ballarin@13940 ` 794` ``` have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) ``` ballarin@13940 ` 795` ``` then obtain n where "bound n (coeff p)" by (unfold UP_def) fast ``` ballarin@13940 ` 796` ``` with prem show P . ``` ballarin@13940 ` 797` ```qed ``` ballarin@13940 ` 798` ```*) ``` ballarin@13940 ` 799` ```lemma (in UP_cring) deg_aboveD: ``` ballarin@13940 ` 800` ``` "[| deg R p < m; p \ carrier P |] ==> coeff P p m = \" ``` ballarin@13940 ` 801` ```proof - ``` ballarin@13940 ` 802` ``` assume R: "p \ carrier P" and "deg R p < m" ``` wenzelm@14666 ` 803` ``` from R obtain n where "bound \ n (coeff P p)" ``` ballarin@13940 ` 804` ``` by (auto simp add: UP_def P_def) ``` ballarin@13940 ` 805` ``` then have "bound \ (deg R p) (coeff P p)" ``` ballarin@13940 ` 806` ``` by (auto simp: deg_def P_def dest: LeastI) ``` wenzelm@14666 ` 807` ``` then show ?thesis .. ``` ballarin@13940 ` 808` ```qed ``` ballarin@13940 ` 809` ballarin@13940 ` 810` ```lemma (in UP_cring) deg_belowI: ``` ballarin@13940 ` 811` ``` assumes non_zero: "n ~= 0 ==> coeff P p n ~= \" ``` ballarin@13940 ` 812` ``` and R: "p \ carrier P" ``` ballarin@13940 ` 813` ``` shows "n <= deg R p" ``` wenzelm@14666 ` 814` ```-- {* Logically, this is a slightly stronger version of ``` ballarin@13940 ` 815` ``` @{thm [source] deg_aboveD} *} ``` ballarin@13940 ` 816` ```proof (cases "n=0") ``` ballarin@13940 ` 817` ``` case True then show ?thesis by simp ``` ballarin@13940 ` 818` ```next ``` ballarin@13940 ` 819` ``` case False then have "coeff P p n ~= \" by (rule non_zero) ``` ballarin@13940 ` 820` ``` then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R) ``` ballarin@13940 ` 821` ``` then show ?thesis by arith ``` ballarin@13940 ` 822` ```qed ``` ballarin@13940 ` 823` ballarin@13940 ` 824` ```lemma (in UP_cring) lcoeff_nonzero_deg: ``` ballarin@13940 ` 825` ``` assumes deg: "deg R p ~= 0" and R: "p \ carrier P" ``` ballarin@13940 ` 826` ``` shows "coeff P p (deg R p) ~= \" ``` ballarin@13940 ` 827` ```proof - ``` ballarin@13940 ` 828` ``` from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \" ``` ballarin@13940 ` 829` ``` proof - ``` ballarin@13940 ` 830` ``` have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)" ``` ballarin@13940 ` 831` ``` by arith ``` ballarin@13940 ` 832` ```(* TODO: why does proof not work with "1" *) ``` ballarin@13940 ` 833` ``` from deg have "deg R p - 1 < (LEAST n. bound \ n (coeff P p))" ``` ballarin@13940 ` 834` ``` by (unfold deg_def P_def) arith ``` ballarin@13940 ` 835` ``` then have "~ bound \ (deg R p - 1) (coeff P p)" by (rule not_less_Least) ``` ballarin@13940 ` 836` ``` then have "EX m. deg R p - 1 < m & coeff P p m ~= \" ``` ballarin@13940 ` 837` ``` by (unfold bound_def) fast ``` ballarin@13940 ` 838` ``` then have "EX m. deg R p <= m & coeff P p m ~= \" by (simp add: deg minus) ``` wenzelm@14666 ` 839` ``` then show ?thesis by auto ``` ballarin@13940 ` 840` ``` qed ``` ballarin@13940 ` 841` ``` with deg_belowI R have "deg R p = m" by fastsimp ``` ballarin@13940 ` 842` ``` with m_coeff show ?thesis by simp ``` ballarin@13940 ` 843` ```qed ``` ballarin@13940 ` 844` ballarin@13940 ` 845` ```lemma (in UP_cring) lcoeff_nonzero_nonzero: ``` ballarin@13940 ` 846` ``` assumes deg: "deg R p = 0" and nonzero: "p ~= \\<^sub>2" and R: "p \ carrier P" ``` ballarin@13940 ` 847` ``` shows "coeff P p 0 ~= \" ``` ballarin@13940 ` 848` ```proof - ``` ballarin@13940 ` 849` ``` have "EX m. coeff P p m ~= \" ``` ballarin@13940 ` 850` ``` proof (rule classical) ``` ballarin@13940 ` 851` ``` assume "~ ?thesis" ``` ballarin@13940 ` 852` ``` with R have "p = \\<^sub>2" by (auto intro: up_eqI) ``` ballarin@13940 ` 853` ``` with nonzero show ?thesis by contradiction ``` ballarin@13940 ` 854` ``` qed ``` ballarin@13940 ` 855` ``` then obtain m where coeff: "coeff P p m ~= \" .. ``` ballarin@13940 ` 856` ``` then have "m <= deg R p" by (rule deg_belowI) ``` ballarin@13940 ` 857` ``` then have "m = 0" by (simp add: deg) ``` ballarin@13940 ` 858` ``` with coeff show ?thesis by simp ``` ballarin@13940 ` 859` ```qed ``` ballarin@13940 ` 860` ballarin@13940 ` 861` ```lemma (in UP_cring) lcoeff_nonzero: ``` ballarin@13940 ` 862` ``` assumes neq: "p ~= \\<^sub>2" and R: "p \ carrier P" ``` ballarin@13940 ` 863` ``` shows "coeff P p (deg R p) ~= \" ``` ballarin@13940 ` 864` ```proof (cases "deg R p = 0") ``` ballarin@13940 ` 865` ``` case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero) ``` ballarin@13940 ` 866` ```next ``` ballarin@13940 ` 867` ``` case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg) ``` ballarin@13940 ` 868` ```qed ``` ballarin@13940 ` 869` ballarin@13940 ` 870` ```lemma (in UP_cring) deg_eqI: ``` ballarin@13940 ` 871` ``` "[| !!m. n < m ==> coeff P p m = \; ``` ballarin@13940 ` 872` ``` !!n. n ~= 0 ==> coeff P p n ~= \; p \ carrier P |] ==> deg R p = n" ``` ballarin@13940 ` 873` ```by (fast intro: le_anti_sym deg_aboveI deg_belowI) ``` ballarin@13940 ` 874` ballarin@13940 ` 875` ```(* Degree and polynomial operations *) ``` ballarin@13940 ` 876` ballarin@13940 ` 877` ```lemma (in UP_cring) deg_add [simp]: ``` ballarin@13940 ` 878` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@13940 ` 879` ``` shows "deg R (p \\<^sub>2 q) <= max (deg R p) (deg R q)" ``` ballarin@13940 ` 880` ```proof (cases "deg R p <= deg R q") ``` ballarin@13940 ` 881` ``` case True show ?thesis ``` wenzelm@14666 ` 882` ``` by (rule deg_aboveI) (simp_all add: True R deg_aboveD) ``` ballarin@13940 ` 883` ```next ``` ballarin@13940 ` 884` ``` case False show ?thesis ``` ballarin@13940 ` 885` ``` by (rule deg_aboveI) (simp_all add: False R deg_aboveD) ``` ballarin@13940 ` 886` ```qed ``` ballarin@13940 ` 887` ballarin@13940 ` 888` ```lemma (in UP_cring) deg_monom_le: ``` ballarin@13940 ` 889` ``` "a \ carrier R ==> deg R (monom P a n) <= n" ``` ballarin@13940 ` 890` ``` by (intro deg_aboveI) simp_all ``` ballarin@13940 ` 891` ballarin@13940 ` 892` ```lemma (in UP_cring) deg_monom [simp]: ``` ballarin@13940 ` 893` ``` "[| a ~= \; a \ carrier R |] ==> deg R (monom P a n) = n" ``` ballarin@13940 ` 894` ``` by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) ``` ballarin@13940 ` 895` ballarin@13940 ` 896` ```lemma (in UP_cring) deg_const [simp]: ``` ballarin@13940 ` 897` ``` assumes R: "a \ carrier R" shows "deg R (monom P a 0) = 0" ``` ballarin@13940 ` 898` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 899` ``` show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R) ``` ballarin@13940 ` 900` ```next ``` ballarin@13940 ` 901` ``` show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R) ``` ballarin@13940 ` 902` ```qed ``` ballarin@13940 ` 903` ballarin@13940 ` 904` ```lemma (in UP_cring) deg_zero [simp]: ``` ballarin@13940 ` 905` ``` "deg R \\<^sub>2 = 0" ``` ballarin@13940 ` 906` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 907` ``` show "deg R \\<^sub>2 <= 0" by (rule deg_aboveI) simp_all ``` ballarin@13940 ` 908` ```next ``` ballarin@13940 ` 909` ``` show "0 <= deg R \\<^sub>2" by (rule deg_belowI) simp_all ``` ballarin@13940 ` 910` ```qed ``` ballarin@13940 ` 911` ballarin@13940 ` 912` ```lemma (in UP_cring) deg_one [simp]: ``` ballarin@13940 ` 913` ``` "deg R \\<^sub>2 = 0" ``` ballarin@13940 ` 914` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 915` ``` show "deg R \\<^sub>2 <= 0" by (rule deg_aboveI) simp_all ``` ballarin@13940 ` 916` ```next ``` ballarin@13940 ` 917` ``` show "0 <= deg R \\<^sub>2" by (rule deg_belowI) simp_all ``` ballarin@13940 ` 918` ```qed ``` ballarin@13940 ` 919` ballarin@13940 ` 920` ```lemma (in UP_cring) deg_uminus [simp]: ``` ballarin@13940 ` 921` ``` assumes R: "p \ carrier P" shows "deg R (\\<^sub>2 p) = deg R p" ``` ballarin@13940 ` 922` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 923` ``` show "deg R (\\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R) ``` ballarin@13940 ` 924` ```next ``` wenzelm@14666 ` 925` ``` show "deg R p <= deg R (\\<^sub>2 p)" ``` ballarin@13940 ` 926` ``` by (simp add: deg_belowI lcoeff_nonzero_deg ``` ballarin@13940 ` 927` ``` inj_on_iff [OF a_inv_inj, of _ "\", simplified] R) ``` ballarin@13940 ` 928` ```qed ``` ballarin@13940 ` 929` ballarin@13940 ` 930` ```lemma (in UP_domain) deg_smult_ring: ``` ballarin@13940 ` 931` ``` "[| a \ carrier R; p \ carrier P |] ==> ``` ballarin@13940 ` 932` ``` deg R (a \\<^sub>2 p) <= (if a = \ then 0 else deg R p)" ``` ballarin@13940 ` 933` ``` by (cases "a = \") (simp add: deg_aboveI deg_aboveD)+ ``` ballarin@13940 ` 934` ballarin@13940 ` 935` ```lemma (in UP_domain) deg_smult [simp]: ``` ballarin@13940 ` 936` ``` assumes R: "a \ carrier R" "p \ carrier P" ``` ballarin@13940 ` 937` ``` shows "deg R (a \\<^sub>2 p) = (if a = \ then 0 else deg R p)" ``` ballarin@13940 ` 938` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 939` ``` show "deg R (a \\<^sub>2 p) <= (if a = \ then 0 else deg R p)" ``` ballarin@13940 ` 940` ``` by (rule deg_smult_ring) ``` ballarin@13940 ` 941` ```next ``` ballarin@13940 ` 942` ``` show "(if a = \ then 0 else deg R p) <= deg R (a \\<^sub>2 p)" ``` ballarin@13940 ` 943` ``` proof (cases "a = \") ``` ballarin@13940 ` 944` ``` qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R) ``` ballarin@13940 ` 945` ```qed ``` ballarin@13940 ` 946` ballarin@13940 ` 947` ```lemma (in UP_cring) deg_mult_cring: ``` ballarin@13940 ` 948` ``` assumes R: "p \ carrier P" "q \ carrier P" ``` ballarin@13940 ` 949` ``` shows "deg R (p \\<^sub>2 q) <= deg R p + deg R q" ``` ballarin@13940 ` 950` ```proof (rule deg_aboveI) ``` ballarin@13940 ` 951` ``` fix m ``` ballarin@13940 ` 952` ``` assume boundm: "deg R p + deg R q < m" ``` ballarin@13940 ` 953` ``` { ``` ballarin@13940 ` 954` ``` fix k i ``` ballarin@13940 ` 955` ``` assume boundk: "deg R p + deg R q < k" ``` ballarin@13940 ` 956` ``` then have "coeff P p i \ coeff P q (k - i) = \" ``` ballarin@13940 ` 957` ``` proof (cases "deg R p < i") ``` ballarin@13940 ` 958` ``` case True then show ?thesis by (simp add: deg_aboveD R) ``` ballarin@13940 ` 959` ``` next ``` ballarin@13940 ` 960` ``` case False with boundk have "deg R q < k - i" by arith ``` ballarin@13940 ` 961` ``` then show ?thesis by (simp add: deg_aboveD R) ``` ballarin@13940 ` 962` ``` qed ``` ballarin@13940 ` 963` ``` } ``` ballarin@13940 ` 964` ``` with boundm R show "coeff P (p \\<^sub>2 q) m = \" by simp ``` ballarin@13940 ` 965` ```qed (simp add: R) ``` ballarin@13940 ` 966` ballarin@13940 ` 967` ```ML_setup {* ``` wenzelm@14590 ` 968` ``` simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; ``` wenzelm@14590 ` 969` ```*} ``` ballarin@13940 ` 970` ballarin@13940 ` 971` ```lemma (in UP_domain) deg_mult [simp]: ``` ballarin@13940 ` 972` ``` "[| p ~= \\<^sub>2; q ~= \\<^sub>2; p \ carrier P; q \ carrier P |] ==> ``` ballarin@13940 ` 973` ``` deg R (p \\<^sub>2 q) = deg R p + deg R q" ``` ballarin@13940 ` 974` ```proof (rule le_anti_sym) ``` ballarin@13940 ` 975` ``` assume "p \ carrier P" " q \ carrier P" ``` ballarin@13940 ` 976` ``` show "deg R (p \\<^sub>2 q) <= deg R p + deg R q" by (rule deg_mult_cring) ``` ballarin@13940 ` 977` ```next ``` ballarin@13940 ` 978` ``` let ?s = "(%i. coeff P p i \ coeff P q (deg R p + deg R q - i))" ``` ballarin@13940 ` 979` ``` assume R: "p \ carrier P" "q \ carrier P" and nz: "p ~= \\<^sub>2" "q ~= \\<^sub>2" ``` ballarin@13940 ` 980` ``` have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith ``` ballarin@13940 ` 981` ``` show "deg R p + deg R q <= deg R (p \\<^sub>2 q)" ``` ballarin@13940 ` 982` ``` proof (rule deg_belowI, simp add: R) ``` ballarin@13940 ` 983` ``` have "finsum R ?s {.. deg R p + deg R q} ``` ballarin@13940 ` 984` ``` = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})" ``` ballarin@13940 ` 985` ``` by (simp only: ivl_disj_un_one) ``` ballarin@13940 ` 986` ``` also have "... = finsum R ?s {deg R p .. deg R p + deg R q}" ``` ballarin@13940 ` 987` ``` by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one ``` ballarin@13940 ` 988` ``` deg_aboveD less_add_diff R Pi_def) ``` ballarin@13940 ` 989` ``` also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})" ``` ballarin@13940 ` 990` ``` by (simp only: ivl_disj_un_singleton) ``` wenzelm@14666 ` 991` ``` also have "... = coeff P p (deg R p) \ coeff P q (deg R q)" ``` ballarin@13940 ` 992` ``` by (simp cong: finsum_cong add: finsum_Un_disjoint ``` wenzelm@14666 ` 993` ``` ivl_disj_int_singleton deg_aboveD R Pi_def) ``` wenzelm@14666 ` 994` ``` finally have "finsum R ?s {.. deg R p + deg R q} ``` ballarin@13940 ` 995` ``` = coeff P p (deg R p) \ coeff P q (deg R q)" . ``` ballarin@13940 ` 996` ``` with nz show "finsum R ?s {.. deg R p + deg R q} ~= \" ``` ballarin@13940 ` 997` ``` by (simp add: integral_iff lcoeff_nonzero R) ``` ballarin@13940 ` 998` ``` qed (simp add: R) ``` ballarin@13940 ` 999` ``` qed ``` ballarin@13940 ` 1000` ballarin@13940 ` 1001` ```lemma (in UP_cring) coeff_finsum: ``` ballarin@13940 ` 1002` ``` assumes fin: "finite A" ``` ballarin@13940 ` 1003` ``` shows "p \ A -> carrier P ==> ``` ballarin@13940 ` 1004` ``` coeff P (finsum P p A) k == finsum R (%i. coeff P (p i) k) A" ``` ballarin@13940 ` 1005` ``` using fin by induct (auto simp: Pi_def) ``` ballarin@13940 ` 1006` ballarin@13940 ` 1007` ```ML_setup {* ``` wenzelm@14590 ` 1008` ``` simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; ``` wenzelm@14590 ` 1009` ```*} ``` ballarin@13940 ` 1010` ballarin@13940 ` 1011` ```lemma (in UP_cring) up_repr: ``` ballarin@13940 ` 1012` ``` assumes R: "p \ carrier P" ``` wenzelm@14666 ` 1013` ``` shows "(\\<^sub>2 i \ {..deg R p}. monom P (coeff P p i) i) = p" ``` ballarin@13940 ` 1014` ```proof (rule up_eqI) ``` ballarin@13940 ` 1015` ``` let ?s = "(%i. monom P (coeff P p i) i)" ``` ballarin@13940 ` 1016` ``` fix k ``` ballarin@13940 ` 1017` ``` from R have RR: "!!i. (if i = k then coeff P p i else \) \ carrier R" ``` ballarin@13940 ` 1018` ``` by simp ``` ballarin@13940 ` 1019` ``` show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k" ``` ballarin@13940 ` 1020` ``` proof (cases "k <= deg R p") ``` ballarin@13940 ` 1021` ``` case True ``` wenzelm@14666 ` 1022` ``` hence "coeff P (finsum P ?s {..deg R p}) k = ``` ballarin@13940 ` 1023` ``` coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k" ``` ballarin@13940 ` 1024` ``` by (simp only: ivl_disj_un_one) ``` ballarin@13940 ` 1025` ``` also from True ``` ballarin@13940 ` 1026` ``` have "... = coeff P (finsum P ?s {..k}) k" ``` ballarin@13940 ` 1027` ``` by (simp cong: finsum_cong add: finsum_Un_disjoint ``` wenzelm@14666 ` 1028` ``` ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def) ``` ballarin@13940 ` 1029` ``` also ``` ballarin@13940 ` 1030` ``` have "... = coeff P (finsum P ?s ({..k(} Un {k})) k" ``` ballarin@13940 ` 1031` ``` by (simp only: ivl_disj_un_singleton) ``` ballarin@13940 ` 1032` ``` also have "... = coeff P p k" ``` ballarin@13940 ` 1033` ``` by (simp cong: finsum_cong add: setsum_Un_disjoint ``` wenzelm@14666 ` 1034` ``` ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def) ``` ballarin@13940 ` 1035` ``` finally show ?thesis . ``` ballarin@13940 ` 1036` ``` next ``` ballarin@13940 ` 1037` ``` case False ``` wenzelm@14666 ` 1038` ``` hence "coeff P (finsum P ?s {..deg R p}) k = ``` ballarin@13940 ` 1039` ``` coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k" ``` ballarin@13940 ` 1040` ``` by (simp only: ivl_disj_un_singleton) ``` ballarin@13940 ` 1041` ``` also from False have "... = coeff P p k" ``` ballarin@13940 ` 1042` ``` by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton ``` ballarin@13940 ` 1043` ``` coeff_finsum deg_aboveD R Pi_def) ``` ballarin@13940 ` 1044` ``` finally show ?thesis . ``` ballarin@13940 ` 1045` ``` qed ``` ballarin@13940 ` 1046` ```qed (simp_all add: R Pi_def) ``` ballarin@13940 ` 1047` ballarin@13940 ` 1048` ```lemma (in UP_cring) up_repr_le: ``` ballarin@13940 ` 1049` ``` "[| deg R p <= n; p \ carrier P |] ==> ``` ballarin@13940 ` 1050` ``` finsum P (%i. monom P (coeff P p i) i) {..n} = p" ``` ballarin@13940 ` 1051` ```proof - ``` ballarin@13940 ` 1052` ``` let ?s = "(%i. monom P (coeff P p i) i)" ``` ballarin@13940 ` 1053` ``` assume R: "p \ carrier P" and "deg R p <= n" ``` ballarin@13940 ` 1054` ``` then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})" ``` ballarin@13940 ` 1055` ``` by (simp only: ivl_disj_un_one) ``` ballarin@13940 ` 1056` ``` also have "... = finsum P ?s {..deg R p}" ``` ballarin@13940 ` 1057` ``` by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one ``` ballarin@13940 ` 1058` ``` deg_aboveD R Pi_def) ``` ballarin@13940 ` 1059` ``` also have "... = p" by (rule up_repr) ``` ballarin@13940 ` 1060` ``` finally show ?thesis . ``` ballarin@13940 ` 1061` ```qed ``` ballarin@13940 ` 1062` ballarin@13940 ` 1063` ```ML_setup {* ``` wenzelm@14590 ` 1064` ``` simpset_ref() := simpset() setsubgoaler asm_simp_tac; ``` wenzelm@14590 ` 1065` ```*} ``` ballarin@13940 ` 1066` ballarin@13949 ` 1067` ```subsection {* Polynomials over an integral domain form an integral domain *} ``` ballarin@13940 ` 1068` ballarin@13940 ` 1069` ```lemma domainI: ``` ballarin@13940 ` 1070` ``` assumes cring: "cring R" ``` ballarin@13940 ` 1071` ``` and one_not_zero: "one R ~= zero R" ``` ballarin@13940 ` 1072` ``` and integral: "!!a b. [| mult R a b = zero R; a \ carrier R; ``` ballarin@13940 ` 1073` ``` b \ carrier R |] ==> a = zero R | b = zero R" ``` ballarin@13940 ` 1074` ``` shows "domain R" ``` ballarin@13940 ` 1075` ``` by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems ``` ballarin@13940 ` 1076` ``` del: disjCI) ``` ballarin@13940 ` 1077` ballarin@13940 ` 1078` ```lemma (in UP_domain) UP_one_not_zero: ``` ballarin@13940 ` 1079` ``` "\\<^sub>2 ~= \\<^sub>2" ``` ballarin@13940 ` 1080` ```proof ``` ballarin@13940 ` 1081` ``` assume "\\<^sub>2 = \\<^sub>2" ``` ballarin@13940 ` 1082` ``` hence "coeff P \\<^sub>2 0 = (coeff P \\<^sub>2 0)" by simp ``` ballarin@13940 ` 1083` ``` hence "\ = \" by simp ``` ballarin@13940 ` 1084` ``` with one_not_zero show "False" by contradiction ``` ballarin@13940 ` 1085` ```qed ``` ballarin@13940 ` 1086` ballarin@13940 ` 1087` ```lemma (in UP_domain) UP_integral: ``` ballarin@13940 ` 1088` ``` "[| p \\<^sub>2 q = \\<^sub>2; p \ carrier P; q \ carrier P |] ==> p = \\<^sub>2 | q = \\<^sub>2" ``` ballarin@13940 ` 1089` ```proof - ``` ballarin@13940 ` 1090` ``` fix p q ``` ballarin@13940 ` 1091` ``` assume pq: "p \\<^sub>2 q = \\<^sub>2" and R: "p \ carrier P" "q \ carrier P" ``` ballarin@13940 ` 1092` ``` show "p = \\<^sub>2 | q = \\<^sub>2" ``` ballarin@13940 ` 1093` ``` proof (rule classical) ``` ballarin@13940 ` 1094` ``` assume c: "~ (p = \\<^sub>2 | q = \\<^sub>2)" ``` ballarin@13940 ` 1095` ``` with R have "deg R p + deg R q = deg R (p \\<^sub>2 q)" by simp ``` ballarin@13940 ` 1096` ``` also from pq have "... = 0" by simp ``` ballarin@13940 ` 1097` ``` finally have "deg R p + deg R q = 0" . ``` ballarin@13940 ` 1098` ``` then have f1: "deg R p = 0 & deg R q = 0" by simp ``` wenzelm@14666 ` 1099` ``` from f1 R have "p = (\\<^sub>2 i \ {..0}. monom P (coeff P p i) i)" ``` ballarin@13940 ` 1100` ``` by (simp only: up_repr_le) ``` ballarin@13940 ` 1101` ``` also from R have "... = monom P (coeff P p 0) 0" by simp ``` ballarin@13940 ` 1102` ``` finally have p: "p = monom P (coeff P p 0) 0" . ``` wenzelm@14666 ` 1103` ``` from f1 R have "q = (\\<^sub>2 i \ {..0}. monom P (coeff P q i) i)" ``` ballarin@13940 ` 1104` ``` by (simp only: up_repr_le) ``` ballarin@13940 ` 1105` ``` also from R have "... = monom P (coeff P q 0) 0" by simp ``` ballarin@13940 ` 1106` ``` finally have q: "q = monom P (coeff P q 0) 0" . ``` ballarin@13940 ` 1107` ``` from R have "coeff P p 0 \ coeff P q 0 = coeff P (p \\<^sub>2 q) 0" by simp ``` ballarin@13940 ` 1108` ``` also from pq have "... = \" by simp ``` ballarin@13940 ` 1109` ``` finally have "coeff P p 0 \ coeff P q 0 = \" . ``` ballarin@13940 ` 1110` ``` with R have "coeff P p 0 = \ | coeff P q 0 = \" ``` ballarin@13940 ` 1111` ``` by (simp add: R.integral_iff) ``` ballarin@13940 ` 1112` ``` with p q show "p = \\<^sub>2 | q = \\<^sub>2" by fastsimp ``` ballarin@13940 ` 1113` ``` qed ``` ballarin@13940 ` 1114` ```qed ``` ballarin@13940 ` 1115` ballarin@13940 ` 1116` ```theorem (in UP_domain) UP_domain: ``` ballarin@13940 ` 1117` ``` "domain P" ``` ballarin@13940 ` 1118` ``` by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI) ``` ballarin@13940 ` 1119` ballarin@13940 ` 1120` ```text {* ``` ballarin@13940 ` 1121` ``` Instantiation of results from @{term domain}. ``` ballarin@13940 ` 1122` ```*} ``` ballarin@13940 ` 1123` ballarin@13940 ` 1124` ```lemmas (in UP_domain) UP_zero_not_one [simp] = ``` ballarin@13940 ` 1125` ``` domain.zero_not_one [OF UP_domain] ``` ballarin@13940 ` 1126` ballarin@13940 ` 1127` ```lemmas (in UP_domain) UP_integral_iff = ``` ballarin@13940 ` 1128` ``` domain.integral_iff [OF UP_domain] ``` ballarin@13940 ` 1129` ballarin@13940 ` 1130` ```lemmas (in UP_domain) UP_m_lcancel = ``` ballarin@13940 ` 1131` ``` domain.m_lcancel [OF UP_domain] ``` ballarin@13940 ` 1132` ballarin@13940 ` 1133` ```lemmas (in UP_domain) UP_m_rcancel = ``` ballarin@13940 ` 1134` ``` domain.m_rcancel [OF UP_domain] ``` ballarin@13940 ` 1135` ballarin@13940 ` 1136` ```lemma (in UP_domain) smult_integral: ``` ballarin@13940 ` 1137` ``` "[| a \\<^sub>2 p = \\<^sub>2; a \ carrier R; p \ carrier P |] ==> a = \ | p = \\<^sub>2" ``` ballarin@13940 ` 1138` ``` by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff ``` ballarin@13940 ` 1139` ``` inj_on_iff [OF monom_inj, of _ "\", simplified]) ``` ballarin@13940 ` 1140` wenzelm@14666 ` 1141` ballarin@13949 ` 1142` ```subsection {* Evaluation Homomorphism and Universal Property*} ``` ballarin@13940 ` 1143` wenzelm@14666 ` 1144` ```(* alternative congruence rule (possibly more efficient) ``` wenzelm@14666 ` 1145` ```lemma (in abelian_monoid) finsum_cong2: ``` wenzelm@14666 ` 1146` ``` "[| !!i. i \ A ==> f i \ carrier G = True; A = B; ``` wenzelm@14666 ` 1147` ``` !!i. i \ B ==> f i = g i |] ==> finsum G f A = finsum G g B" ``` wenzelm@14666 ` 1148` ``` sorry*) ``` wenzelm@14666 ` 1149` ballarin@13940 ` 1150` ```ML_setup {* ``` wenzelm@14590 ` 1151` ``` simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; ``` wenzelm@14590 ` 1152` ```*} ``` ballarin@13940 ` 1153` ballarin@13940 ` 1154` ```theorem (in cring) diagonal_sum: ``` ballarin@13940 ` 1155` ``` "[| f \ {..n + m::nat} -> carrier R; g \ {..n + m} -> carrier R |] ==> ``` wenzelm@14666 ` 1156` ``` (\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) = ``` wenzelm@14666 ` 1157` ``` (\k \ {..n + m}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1158` ```proof - ``` ballarin@13940 ` 1159` ``` assume Rf: "f \ {..n + m} -> carrier R" and Rg: "g \ {..n + m} -> carrier R" ``` ballarin@13940 ` 1160` ``` { ``` ballarin@13940 ` 1161` ``` fix j ``` ballarin@13940 ` 1162` ``` have "j <= n + m ==> ``` wenzelm@14666 ` 1163` ``` (\k \ {..j}. \i \ {..k}. f i \ g (k - i)) = ``` wenzelm@14666 ` 1164` ``` (\k \ {..j}. \i \ {..j - k}. f k \ g i)" ``` ballarin@13940 ` 1165` ``` proof (induct j) ``` ballarin@13940 ` 1166` ``` case 0 from Rf Rg show ?case by (simp add: Pi_def) ``` ballarin@13940 ` 1167` ``` next ``` wenzelm@14666 ` 1168` ``` case (Suc j) ``` ballarin@13940 ` 1169` ``` (* The following could be simplified if there was a reasoner for ``` wenzelm@14666 ` 1170` ``` total orders integrated with simip. *) ``` ballarin@13940 ` 1171` ``` have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \ carrier R" ``` wenzelm@14666 ` 1172` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) arith ``` ballarin@13940 ` 1173` ``` have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \ carrier R" ``` wenzelm@14666 ` 1174` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) arith ``` ballarin@13940 ` 1175` ``` have R9: "!!i k. [| k <= Suc j |] ==> f k \ carrier R" ``` wenzelm@14666 ` 1176` ``` using Suc by (auto intro!: funcset_mem [OF Rf]) ``` ballarin@13940 ` 1177` ``` have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \ carrier R" ``` wenzelm@14666 ` 1178` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) arith ``` ballarin@13940 ` 1179` ``` have R11: "g 0 \ carrier R" ``` wenzelm@14666 ` 1180` ``` using Suc by (auto intro!: funcset_mem [OF Rg]) ``` ballarin@13940 ` 1181` ``` from Suc show ?case ``` wenzelm@14666 ` 1182` ``` by (simp cong: finsum_cong add: Suc_diff_le a_ac ``` wenzelm@14666 ` 1183` ``` Pi_def R6 R8 R9 R10 R11) ``` ballarin@13940 ` 1184` ``` qed ``` ballarin@13940 ` 1185` ``` } ``` ballarin@13940 ` 1186` ``` then show ?thesis by fast ``` ballarin@13940 ` 1187` ```qed ``` ballarin@13940 ` 1188` ballarin@13940 ` 1189` ```lemma (in abelian_monoid) boundD_carrier: ``` ballarin@13940 ` 1190` ``` "[| bound \ n f; n < m |] ==> f m \ carrier G" ``` ballarin@13940 ` 1191` ``` by auto ``` ballarin@13940 ` 1192` ballarin@13940 ` 1193` ```theorem (in cring) cauchy_product: ``` ballarin@13940 ` 1194` ``` assumes bf: "bound \ n f" and bg: "bound \ m g" ``` ballarin@13940 ` 1195` ``` and Rf: "f \ {..n} -> carrier R" and Rg: "g \ {..m} -> carrier R" ``` wenzelm@14666 ` 1196` ``` shows "(\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) = ``` wenzelm@14666 ` 1197` ``` (\i \ {..n}. f i) \ (\i \ {..m}. g i)" (* State revese direction? *) ``` ballarin@13940 ` 1198` ```proof - ``` ballarin@13940 ` 1199` ``` have f: "!!x. f x \ carrier R" ``` ballarin@13940 ` 1200` ``` proof - ``` ballarin@13940 ` 1201` ``` fix x ``` ballarin@13940 ` 1202` ``` show "f x \ carrier R" ``` ballarin@13940 ` 1203` ``` using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def) ``` ballarin@13940 ` 1204` ``` qed ``` ballarin@13940 ` 1205` ``` have g: "!!x. g x \ carrier R" ``` ballarin@13940 ` 1206` ``` proof - ``` ballarin@13940 ` 1207` ``` fix x ``` ballarin@13940 ` 1208` ``` show "g x \ carrier R" ``` ballarin@13940 ` 1209` ``` using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def) ``` ballarin@13940 ` 1210` ``` qed ``` wenzelm@14666 ` 1211` ``` from f g have "(\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) = ``` wenzelm@14666 ` 1212` ``` (\k \ {..n + m}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1213` ``` by (simp add: diagonal_sum Pi_def) ``` wenzelm@14666 ` 1214` ``` also have "... = (\k \ {..n} \ {)n..n + m}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1215` ``` by (simp only: ivl_disj_un_one) ``` wenzelm@14666 ` 1216` ``` also from f g have "... = (\k \ {..n}. \i \ {..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1217` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1218` ``` add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` wenzelm@14666 ` 1219` ``` also from f g have "... = (\k \ {..n}. \i \ {..m} \ {)m..n + m - k}. f k \ g i)" ``` ballarin@13940 ` 1220` ``` by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def) ``` wenzelm@14666 ` 1221` ``` also from f g have "... = (\k \ {..n}. \i \ {..m}. f k \ g i)" ``` ballarin@13940 ` 1222` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1223` ``` add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` wenzelm@14666 ` 1224` ``` also from f g have "... = (\i \ {..n}. f i) \ (\i \ {..m}. g i)" ``` ballarin@13940 ` 1225` ``` by (simp add: finsum_ldistr diagonal_sum Pi_def, ``` ballarin@13940 ` 1226` ``` simp cong: finsum_cong add: finsum_rdistr Pi_def) ``` ballarin@13940 ` 1227` ``` finally show ?thesis . ``` ballarin@13940 ` 1228` ```qed ``` ballarin@13940 ` 1229` ballarin@13940 ` 1230` ```lemma (in UP_cring) const_ring_hom: ``` ballarin@13940 ` 1231` ``` "(%a. monom P a 0) \ ring_hom R P" ``` ballarin@13940 ` 1232` ``` by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult) ``` ballarin@13940 ` 1233` wenzelm@14651 ` 1234` ```constdefs (structure S) ``` wenzelm@14651 ` 1235` ``` eval :: "[_, _, 'a => 'b, 'b, nat => 'a] => 'b" ``` wenzelm@14651 ` 1236` ``` "eval R S phi s == \p \ carrier (UP R). ``` wenzelm@14651 ` 1237` ``` \i \ {..deg R p}. phi (coeff (UP R) p i) \ pow S s i" ``` ballarin@13940 ` 1238` ```(* ``` ballarin@13940 ` 1239` ``` "eval R S phi s p == if p \ carrier (UP R) ``` ballarin@13940 ` 1240` ``` then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p} ``` ballarin@13940 ` 1241` ``` else arbitrary" ``` ballarin@13940 ` 1242` ```*) ``` wenzelm@14666 ` 1243` ballarin@13940 ` 1244` ```locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R ``` ballarin@13940 ` 1245` ballarin@13940 ` 1246` ```lemma (in ring_hom_UP_cring) eval_on_carrier: ``` ballarin@13940 ` 1247` ``` "p \ carrier P ==> ``` ballarin@13940 ` 1248` ``` eval R S phi s p = ``` wenzelm@14666 ` 1249` ``` (\\<^sub>2 i \ {..deg R p}. phi (coeff P p i) \\<^sub>2 pow S s i)" ``` ballarin@13940 ` 1250` ``` by (unfold eval_def, fold P_def) simp ``` ballarin@13940 ` 1251` ballarin@13940 ` 1252` ```lemma (in ring_hom_UP_cring) eval_extensional: ``` ballarin@13940 ` 1253` ``` "eval R S phi s \ extensional (carrier P)" ``` ballarin@13940 ` 1254` ``` by (unfold eval_def, fold P_def) simp ``` ballarin@13940 ` 1255` ballarin@13940 ` 1256` ```theorem (in ring_hom_UP_cring) eval_ring_hom: ``` ballarin@13940 ` 1257` ``` "s \ carrier S ==> eval R S h s \ ring_hom P S" ``` ballarin@13940 ` 1258` ```proof (rule ring_hom_memI) ``` ballarin@13940 ` 1259` ``` fix p ``` ballarin@13940 ` 1260` ``` assume RS: "p \ carrier P" "s \ carrier S" ``` ballarin@13940 ` 1261` ``` then show "eval R S h s p \ carrier S" ``` ballarin@13940 ` 1262` ``` by (simp only: eval_on_carrier) (simp add: Pi_def) ``` ballarin@13940 ` 1263` ```next ``` ballarin@13940 ` 1264` ``` fix p q ``` ballarin@13940 ` 1265` ``` assume RS: "p \ carrier P" "q \ carrier P" "s \ carrier S" ``` ballarin@13940 ` 1266` ``` then show "eval R S h s (p \\<^sub>3 q) = eval R S h s p \\<^sub>2 eval R S h s q" ``` ballarin@13940 ` 1267` ``` proof (simp only: eval_on_carrier UP_mult_closed) ``` ballarin@13940 ` 1268` ``` from RS have ``` wenzelm@14666 ` 1269` ``` "(\\<^sub>2 i \ {..deg R (p \\<^sub>3 q)}. h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i) = ``` wenzelm@14666 ` 1270` ``` (\\<^sub>2 i \ {..deg R (p \\<^sub>3 q)} \ {)deg R (p \\<^sub>3 q)..deg R p + deg R q}. ``` wenzelm@14666 ` 1271` ``` h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1272` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1273` ``` add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def ``` wenzelm@14666 ` 1274` ``` del: coeff_mult) ``` ballarin@13940 ` 1275` ``` also from RS have "... = ``` wenzelm@14666 ` 1276` ``` (\\<^sub>2 i \ {..deg R p + deg R q}. h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1277` ``` by (simp only: ivl_disj_un_one deg_mult_cring) ``` ballarin@13940 ` 1278` ``` also from RS have "... = ``` wenzelm@14666 ` 1279` ``` (\\<^sub>2 i \ {..deg R p + deg R q}. ``` wenzelm@14666 ` 1280` ``` \\<^sub>2 k \ {..i}. h (coeff P p k) \\<^sub>2 h (coeff P q (i - k)) \\<^sub>2 (s (^)\<^sub>2 k \\<^sub>2 s (^)\<^sub>2 (i - k)))" ``` ballarin@13940 ` 1281` ``` by (simp cong: finsum_cong add: nat_pow_mult Pi_def ``` wenzelm@14666 ` 1282` ``` S.m_ac S.finsum_rdistr) ``` ballarin@13940 ` 1283` ``` also from RS have "... = ``` wenzelm@14666 ` 1284` ``` (\\<^sub>2i\{..deg R p}. h (coeff P p i) \\<^sub>2 s (^)\<^sub>2 i) \\<^sub>2 ``` wenzelm@14666 ` 1285` ``` (\\<^sub>2i\{..deg R q}. h (coeff P q i) \\<^sub>2 s (^)\<^sub>2 i)" ``` wenzelm@14666 ` 1286` ``` by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac ``` wenzelm@14666 ` 1287` ``` Pi_def) ``` ballarin@13940 ` 1288` ``` finally show ``` wenzelm@14666 ` 1289` ``` "(\\<^sub>2 i \ {..deg R (p \\<^sub>3 q)}. h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i) = ``` wenzelm@14666 ` 1290` ``` (\\<^sub>2 i \ {..deg R p}. h (coeff P p i) \\<^sub>2 s (^)\<^sub>2 i) \\<^sub>2 ``` wenzelm@14666 ` 1291` ``` (\\<^sub>2 i \ {..deg R q}. h (coeff P q i) \\<^sub>2 s (^)\<^sub>2 i)" . ``` ballarin@13940 ` 1292` ``` qed ``` ballarin@13940 ` 1293` ```next ``` ballarin@13940 ` 1294` ``` fix p q ``` ballarin@13940 ` 1295` ``` assume RS: "p \ carrier P" "q \ carrier P" "s \ carrier S" ``` ballarin@13940 ` 1296` ``` then show "eval R S h s (p \\<^sub>3 q) = eval R S h s p \\<^sub>2 eval R S h s q" ``` ballarin@13940 ` 1297` ``` proof (simp only: eval_on_carrier UP_a_closed) ``` ballarin@13940 ` 1298` ``` from RS have ``` wenzelm@14666 ` 1299` ``` "(\\<^sub>2i \ {..deg R (p \\<^sub>3 q)}. h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i) = ``` wenzelm@14666 ` 1300` ``` (\\<^sub>2i \ {..deg R (p \\<^sub>3 q)} \ {)deg R (p \\<^sub>3 q)..max (deg R p) (deg R q)}. ``` wenzelm@14666 ` 1301` ``` h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1302` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1303` ``` add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def ``` wenzelm@14666 ` 1304` ``` del: coeff_add) ``` ballarin@13940 ` 1305` ``` also from RS have "... = ``` wenzelm@14666 ` 1306` ``` (\\<^sub>2 i \ {..max (deg R p) (deg R q)}. h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1307` ``` by (simp add: ivl_disj_un_one) ``` ballarin@13940 ` 1308` ``` also from RS have "... = ``` wenzelm@14666 ` 1309` ``` (\\<^sub>2i\{..max (deg R p) (deg R q)}. h (coeff P p i) \\<^sub>2 s (^)\<^sub>2 i) \\<^sub>2 ``` wenzelm@14666 ` 1310` ``` (\\<^sub>2i\{..max (deg R p) (deg R q)}. h (coeff P q i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1311` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1312` ``` add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` ballarin@13940 ` 1313` ``` also have "... = ``` wenzelm@14666 ` 1314` ``` (\\<^sub>2 i \ {..deg R p} \ {)deg R p..max (deg R p) (deg R q)}. ``` wenzelm@14666 ` 1315` ``` h (coeff P p i) \\<^sub>2 s (^)\<^sub>2 i) \\<^sub>2 ``` wenzelm@14666 ` 1316` ``` (\\<^sub>2 i \ {..deg R q} \ {)deg R q..max (deg R p) (deg R q)}. ``` wenzelm@14666 ` 1317` ``` h (coeff P q i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1318` ``` by (simp only: ivl_disj_un_one le_maxI1 le_maxI2) ``` ballarin@13940 ` 1319` ``` also from RS have "... = ``` wenzelm@14666 ` 1320` ``` (\\<^sub>2 i \ {..deg R p}. h (coeff P p i) \\<^sub>2 s (^)\<^sub>2 i) \\<^sub>2 ``` wenzelm@14666 ` 1321` ``` (\\<^sub>2 i \ {..deg R q}. h (coeff P q i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1322` ``` by (simp cong: finsum_cong ``` wenzelm@14666 ` 1323` ``` add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` ballarin@13940 ` 1324` ``` finally show ``` wenzelm@14666 ` 1325` ``` "(\\<^sub>2i \ {..deg R (p \\<^sub>3 q)}. h (coeff P (p \\<^sub>3 q) i) \\<^sub>2 s (^)\<^sub>2 i) = ``` wenzelm@14666 ` 1326` ``` (\\<^sub>2i \ {..deg R p}. h (coeff P p i) \\<^sub>2 s (^)\<^sub>2 i) \\<^sub>2 ``` wenzelm@14666 ` 1327` ``` (\\<^sub>2i \ {..deg R q}. h (coeff P q i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1328` ``` . ``` ballarin@13940 ` 1329` ``` qed ``` ballarin@13940 ` 1330` ```next ``` ballarin@13940 ` 1331` ``` assume S: "s \ carrier S" ``` ballarin@13940 ` 1332` ``` then show "eval R S h s \\<^sub>3 = \\<^sub>2" ``` ballarin@13940 ` 1333` ``` by (simp only: eval_on_carrier UP_one_closed) simp ``` ballarin@13940 ` 1334` ```qed ``` ballarin@13940 ` 1335` ballarin@13940 ` 1336` ```text {* Instantiation of ring homomorphism lemmas. *} ``` ballarin@13940 ` 1337` ballarin@13940 ` 1338` ```lemma (in ring_hom_UP_cring) ring_hom_cring_P_S: ``` ballarin@13940 ` 1339` ``` "s \ carrier S ==> ring_hom_cring P S (eval R S h s)" ``` ballarin@13940 ` 1340` ``` by (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems ``` ballarin@13940 ` 1341` ``` intro: ring_hom_cring_axioms.intro eval_ring_hom) ``` ballarin@13940 ` 1342` ballarin@13940 ` 1343` ```lemma (in ring_hom_UP_cring) UP_hom_closed [intro, simp]: ``` ballarin@13940 ` 1344` ``` "[| s \ carrier S; p \ carrier P |] ==> eval R S h s p \ carrier S" ``` ballarin@13940 ` 1345` ``` by (rule ring_hom_cring.hom_closed [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1346` ballarin@13940 ` 1347` ```lemma (in ring_hom_UP_cring) UP_hom_mult [simp]: ``` ballarin@13940 ` 1348` ``` "[| s \ carrier S; p \ carrier P; q \ carrier P |] ==> ``` ballarin@13940 ` 1349` ``` eval R S h s (p \\<^sub>3 q) = eval R S h s p \\<^sub>2 eval R S h s q" ``` ballarin@13940 ` 1350` ``` by (rule ring_hom_cring.hom_mult [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1351` ballarin@13940 ` 1352` ```lemma (in ring_hom_UP_cring) UP_hom_add [simp]: ``` ballarin@13940 ` 1353` ``` "[| s \ carrier S; p \ carrier P; q \ carrier P |] ==> ``` ballarin@13940 ` 1354` ``` eval R S h s (p \\<^sub>3 q) = eval R S h s p \\<^sub>2 eval R S h s q" ``` ballarin@13940 ` 1355` ``` by (rule ring_hom_cring.hom_add [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1356` ballarin@13940 ` 1357` ```lemma (in ring_hom_UP_cring) UP_hom_one [simp]: ``` ballarin@13940 ` 1358` ``` "s \ carrier S ==> eval R S h s \\<^sub>3 = \\<^sub>2" ``` ballarin@13940 ` 1359` ``` by (rule ring_hom_cring.hom_one [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1360` ballarin@13940 ` 1361` ```lemma (in ring_hom_UP_cring) UP_hom_zero [simp]: ``` ballarin@13940 ` 1362` ``` "s \ carrier S ==> eval R S h s \\<^sub>3 = \\<^sub>2" ``` ballarin@13940 ` 1363` ``` by (rule ring_hom_cring.hom_zero [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1364` ballarin@13940 ` 1365` ```lemma (in ring_hom_UP_cring) UP_hom_a_inv [simp]: ``` ballarin@13940 ` 1366` ``` "[| s \ carrier S; p \ carrier P |] ==> ``` ballarin@13940 ` 1367` ``` (eval R S h s) (\\<^sub>3 p) = \\<^sub>2 (eval R S h s) p" ``` ballarin@13940 ` 1368` ``` by (rule ring_hom_cring.hom_a_inv [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1369` ballarin@13940 ` 1370` ```lemma (in ring_hom_UP_cring) UP_hom_finsum [simp]: ``` ballarin@13940 ` 1371` ``` "[| s \ carrier S; finite A; f \ A -> carrier P |] ==> ``` ballarin@13940 ` 1372` ``` (eval R S h s) (finsum P f A) = finsum S (eval R S h s o f) A" ``` ballarin@13940 ` 1373` ``` by (rule ring_hom_cring.hom_finsum [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1374` ballarin@13940 ` 1375` ```lemma (in ring_hom_UP_cring) UP_hom_finprod [simp]: ``` ballarin@13940 ` 1376` ``` "[| s \ carrier S; finite A; f \ A -> carrier P |] ==> ``` ballarin@13940 ` 1377` ``` (eval R S h s) (finprod P f A) = finprod S (eval R S h s o f) A" ``` ballarin@13940 ` 1378` ``` by (rule ring_hom_cring.hom_finprod [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1379` ballarin@13940 ` 1380` ```text {* Further properties of the evaluation homomorphism. *} ``` ballarin@13940 ` 1381` ballarin@13940 ` 1382` ```(* The following lemma could be proved in UP\_cring with the additional ``` ballarin@13940 ` 1383` ``` assumption that h is closed. *) ``` ballarin@13940 ` 1384` ballarin@13940 ` 1385` ```lemma (in ring_hom_UP_cring) eval_const: ``` ballarin@13940 ` 1386` ``` "[| s \ carrier S; r \ carrier R |] ==> eval R S h s (monom P r 0) = h r" ``` ballarin@13940 ` 1387` ``` by (simp only: eval_on_carrier monom_closed) simp ``` ballarin@13940 ` 1388` ballarin@13940 ` 1389` ```text {* The following proof is complicated by the fact that in arbitrary ``` ballarin@13940 ` 1390` ``` rings one might have @{term "one R = zero R"}. *} ``` ballarin@13940 ` 1391` ballarin@13940 ` 1392` ```(* TODO: simplify by cases "one R = zero R" *) ``` ballarin@13940 ` 1393` ballarin@13940 ` 1394` ```lemma (in ring_hom_UP_cring) eval_monom1: ``` ballarin@13940 ` 1395` ``` "s \ carrier S ==> eval R S h s (monom P \ 1) = s" ``` ballarin@13940 ` 1396` ```proof (simp only: eval_on_carrier monom_closed R.one_closed) ``` ballarin@13940 ` 1397` ``` assume S: "s \ carrier S" ``` wenzelm@14666 ` 1398` ``` then have ``` wenzelm@14666 ` 1399` ``` "(\\<^sub>2 i \ {..deg R (monom P \ 1)}. h (coeff P (monom P \ 1) i) \\<^sub>2 s (^)\<^sub>2 i) = ``` wenzelm@14666 ` 1400` ``` (\\<^sub>2i\{..deg R (monom P \ 1)} \ {)deg R (monom P \ 1)..1}. ``` wenzelm@14666 ` 1401` ``` h (coeff P (monom P \ 1) i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1402` ``` by (simp cong: finsum_cong del: coeff_monom ``` ballarin@13940 ` 1403` ``` add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def) ``` wenzelm@14666 ` 1404` ``` also have "... = ``` wenzelm@14666 ` 1405` ``` (\\<^sub>2 i \ {..1}. h (coeff P (monom P \ 1) i) \\<^sub>2 s (^)\<^sub>2 i)" ``` ballarin@13940 ` 1406` ``` by (simp only: ivl_disj_un_one deg_monom_le R.one_closed) ``` ballarin@13940 ` 1407` ``` also have "... = s" ``` ballarin@13940 ` 1408` ``` proof (cases "s = \\<^sub>2") ``` ballarin@13940 ` 1409` ``` case True then show ?thesis by (simp add: Pi_def) ``` ballarin@13940 ` 1410` ``` next ``` ballarin@13940 ` 1411` ``` case False with S show ?thesis by (simp add: Pi_def) ``` ballarin@13940 ` 1412` ``` qed ``` wenzelm@14666 ` 1413` ``` finally show "(\\<^sub>2 i \ {..deg R (monom P \ 1)}. ``` wenzelm@14666 ` 1414` ``` h (coeff P (monom P \ 1) i) \\<^sub>2 s (^)\<^sub>2 i) = s" . ``` ballarin@13940 ` 1415` ```qed ``` ballarin@13940 ` 1416` ballarin@13940 ` 1417` ```lemma (in UP_cring) monom_pow: ``` ballarin@13940 ` 1418` ``` assumes R: "a \ carrier R" ``` ballarin@13940 ` 1419` ``` shows "(monom P a n) (^)\<^sub>2 m = monom P (a (^) m) (n * m)" ``` ballarin@13940 ` 1420` ```proof (induct m) ``` ballarin@13940 ` 1421` ``` case 0 from R show ?case by simp ``` ballarin@13940 ` 1422` ```next ``` ballarin@13940 ` 1423` ``` case Suc with R show ?case ``` ballarin@13940 ` 1424` ``` by (simp del: monom_mult add: monom_mult [THEN sym] add_commute) ``` ballarin@13940 ` 1425` ```qed ``` ballarin@13940 ` 1426` ballarin@13940 ` 1427` ```lemma (in ring_hom_cring) hom_pow [simp]: ``` ballarin@13940 ` 1428` ``` "x \ carrier R ==> h (x (^) n) = h x (^)\<^sub>2 (n::nat)" ``` ballarin@13940 ` 1429` ``` by (induct n) simp_all ``` ballarin@13940 ` 1430` ballarin@13940 ` 1431` ```lemma (in ring_hom_UP_cring) UP_hom_pow [simp]: ``` ballarin@13940 ` 1432` ``` "[| s \ carrier S; p \ carrier P |] ==> ``` ballarin@13940 ` 1433` ``` (eval R S h s) (p (^)\<^sub>3 n) = eval R S h s p (^)\<^sub>2 (n::nat)" ``` ballarin@13940 ` 1434` ``` by (rule ring_hom_cring.hom_pow [OF ring_hom_cring_P_S]) ``` ballarin@13940 ` 1435` ballarin@13940 ` 1436` ```lemma (in ring_hom_UP_cring) eval_monom: ``` ballarin@13940 ` 1437` ``` "[| s \ carrier S; r \ carrier R |] ==> ``` ballarin@13940 ` 1438` ``` eval R S h s (monom P r n) = h r \\<^sub>2 s (^)\<^sub>2 n" ``` ballarin@13940 ` 1439` ```proof - ``` ballarin@13940 ` 1440` ``` assume RS: "s \ carrier S" "r \ carrier R" ``` ballarin@13940 ` 1441` ``` then have "eval R S h s (monom P r n) = ``` ballarin@13940 ` 1442` ``` eval R S h s (monom P r 0 \\<^sub>3 (monom P \ 1) (^)\<^sub>3 n)" ``` ballarin@13940 ` 1443` ``` by (simp del: monom_mult UP_hom_mult UP_hom_pow ``` ballarin@13940 ` 1444` ``` add: monom_mult [THEN sym] monom_pow) ``` ballarin@13940 ` 1445` ``` also from RS eval_monom1 have "... = h r \\<^sub>2 s (^)\<^sub>2 n" ``` ballarin@13940 ` 1446` ``` by (simp add: eval_const) ``` ballarin@13940 ` 1447` ``` finally show ?thesis . ``` ballarin@13940 ` 1448` ```qed ``` ballarin@13940 ` 1449` ballarin@13940 ` 1450` ```lemma (in ring_hom_UP_cring) eval_smult: ``` ballarin@13940 ` 1451` ``` "[| s \ carrier S; r \ carrier R; p \ carrier P |] ==> ``` ballarin@13940 ` 1452` ``` eval R S h s (r \\<^sub>3 p) = h r \\<^sub>2 eval R S h s p" ``` ballarin@13940 ` 1453` ``` by (simp add: monom_mult_is_smult [THEN sym] eval_const) ``` ballarin@13940 ` 1454` ballarin@13940 ` 1455` ```lemma ring_hom_cringI: ``` ballarin@13940 ` 1456` ``` assumes "cring R" ``` ballarin@13940 ` 1457` ``` and "cring S" ``` ballarin@13940 ` 1458` ``` and "h \ ring_hom R S" ``` ballarin@13940 ` 1459` ``` shows "ring_hom_cring R S h" ``` ballarin@13940 ` 1460` ``` by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro ``` ballarin@13940 ` 1461` ``` cring.axioms prems) ``` ballarin@13940 ` 1462` ballarin@13940 ` 1463` ```lemma (in ring_hom_UP_cring) UP_hom_unique: ``` ballarin@13940 ` 1464` ``` assumes Phi: "Phi \ ring_hom P S" "Phi (monom P \ (Suc 0)) = s" ``` ballarin@13940 ` 1465` ``` "!!r. r \ carrier R ==> Phi (monom P r 0) = h r" ``` ballarin@13940 ` 1466` ``` and Psi: "Psi \ ring_hom P S" "Psi (monom P \ (Suc 0)) = s" ``` ballarin@13940 ` 1467` ``` "!!r. r \ carrier R ==> Psi (monom P r 0) = h r" ``` ballarin@13940 ` 1468` ``` and RS: "s \ carrier S" "p \ carrier P" ``` ballarin@13940 ` 1469` ``` shows "Phi p = Psi p" ``` ballarin@13940 ` 1470` ```proof - ``` ballarin@13940 ` 1471` ``` have Phi_hom: "ring_hom_cring P S Phi" ``` ballarin@13940 ` 1472` ``` by (auto intro: ring_hom_cringI UP_cring S.cring Phi) ``` ballarin@13940 ` 1473` ``` have Psi_hom: "ring_hom_cring P S Psi" ``` ballarin@13940 ` 1474` ``` by (auto intro: ring_hom_cringI UP_cring S.cring Psi) ``` wenzelm@14666 ` 1475` ``` have "Phi p = Phi (\\<^sub>3i \ {..deg R p}. monom P (coeff P p i) 0 \\<^sub>3 monom P \ 1 (^)\<^sub>3 i)" ``` ballarin@13940 ` 1476` ``` by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult) ``` wenzelm@14666 ` 1477` ``` also have "... = Psi (\\<^sub>3i\{..deg R p}. monom P (coeff P p i) 0 \\<^sub>3 monom P \ 1 (^)\<^sub>3 i)" ``` wenzelm@14666 ` 1478` ``` by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom] ``` ballarin@13940 ` 1479` ``` ring_hom_cring.hom_mult [OF Phi_hom] ``` ballarin@13940 ` 1480` ``` ring_hom_cring.hom_pow [OF Phi_hom] Phi ``` wenzelm@14666 ` 1481` ``` ring_hom_cring.hom_finsum [OF Psi_hom] ``` ballarin@13940 ` 1482` ``` ring_hom_cring.hom_mult [OF Psi_hom] ``` ballarin@13940 ` 1483` ``` ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def) ``` ballarin@13940 ` 1484` ``` also have "... = Psi p" ``` ballarin@13940 ` 1485` ``` by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult) ``` ballarin@13940 ` 1486` ``` finally show ?thesis . ``` ballarin@13940 ` 1487` ```qed ``` ballarin@13940 ` 1488` ballarin@13940 ` 1489` ballarin@13940 ` 1490` ```theorem (in ring_hom_UP_cring) UP_universal_property: ``` ballarin@13940 ` 1491` ``` "s \ carrier S ==> ``` ballarin@13940 ` 1492` ``` EX! Phi. Phi \ ring_hom P S \ extensional (carrier P) & ``` wenzelm@14666 ` 1493` ``` Phi (monom P \ 1) = s & ``` ballarin@13940 ` 1494` ``` (ALL r : carrier R. Phi (monom P r 0) = h r)" ``` wenzelm@14666 ` 1495` ``` using eval_monom1 ``` ballarin@13940 ` 1496` ``` apply (auto intro: eval_ring_hom eval_const eval_extensional) ``` wenzelm@14666 ` 1497` ``` apply (rule extensionalityI) ``` wenzelm@14666 ` 1498` ``` apply (auto intro: UP_hom_unique) ``` wenzelm@14666 ` 1499` ``` done ``` ballarin@13940 ` 1500` ballarin@13940 ` 1501` ```subsection {* Sample application of evaluation homomorphism *} ``` ballarin@13940 ` 1502` ballarin@13940 ` 1503` ```lemma ring_hom_UP_cringI: ``` ballarin@13940 ` 1504` ``` assumes "cring R" ``` ballarin@13940 ` 1505` ``` and "cring S" ``` ballarin@13940 ` 1506` ``` and "h \ ring_hom R S" ``` ballarin@13940 ` 1507` ``` shows "ring_hom_UP_cring R S h" ``` ballarin@13940 ` 1508` ``` by (fast intro: ring_hom_UP_cring.intro ring_hom_cring_axioms.intro ``` ballarin@13940 ` 1509` ``` cring.axioms prems) ``` ballarin@13940 ` 1510` ballarin@13975 ` 1511` ```constdefs ``` ballarin@13975 ` 1512` ``` INTEG :: "int ring" ``` ballarin@13975 ` 1513` ``` "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)" ``` ballarin@13975 ` 1514` ballarin@13975 ` 1515` ```lemma cring_INTEG: ``` ballarin@13975 ` 1516` ``` "cring INTEG" ``` ballarin@13975 ` 1517` ``` by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI ``` ballarin@13975 ` 1518` ``` zadd_zminus_inverse2 zadd_zmult_distrib) ``` ballarin@13975 ` 1519` ballarin@13940 ` 1520` ```lemma INTEG_id: ``` ballarin@13940 ` 1521` ``` "ring_hom_UP_cring INTEG INTEG id" ``` ballarin@13940 ` 1522` ``` by (fast intro: ring_hom_UP_cringI cring_INTEG id_ring_hom) ``` ballarin@13940 ` 1523` ballarin@13940 ` 1524` ```text {* ``` ballarin@13940 ` 1525` ``` An instantiation mechanism would now import all theorems and lemmas ``` ballarin@13940 ` 1526` ``` valid in the context of homomorphisms between @{term INTEG} and @{term ``` wenzelm@14666 ` 1527` ``` "UP INTEG"}. ``` wenzelm@14666 ` 1528` ```*} ``` ballarin@13940 ` 1529` ballarin@13940 ` 1530` ```lemma INTEG_closed [intro, simp]: ``` ballarin@13940 ` 1531` ``` "z \ carrier INTEG" ``` ballarin@13940 ` 1532` ``` by (unfold INTEG_def) simp ``` ballarin@13940 ` 1533` ballarin@13940 ` 1534` ```lemma INTEG_mult [simp]: ``` ballarin@13940 ` 1535` ``` "mult INTEG z w = z * w" ``` ballarin@13940 ` 1536` ``` by (unfold INTEG_def) simp ``` ballarin@13940 ` 1537` ballarin@13940 ` 1538` ```lemma INTEG_pow [simp]: ``` ballarin@13940 ` 1539` ``` "pow INTEG z n = z ^ n" ``` ballarin@13940 ` 1540` ``` by (induct n) (simp_all add: INTEG_def nat_pow_def) ``` ballarin@13940 ` 1541` ballarin@13940 ` 1542` ```lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500" ``` ballarin@13940 ` 1543` ``` by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id]) ``` ballarin@13940 ` 1544` wenzelm@14590 ` 1545` ```end ```