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