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