src/HOL/Algebra/IntRing.thy
 author ballarin Tue Jul 24 15:29:57 2007 +0200 (2007-07-24) changeset 23957 54fab60ddc97 parent 22063 717425609192 child 24131 1099f6c73649 permissions -rw-r--r--
Interpretation of rings (as integers) maps defined operations to defined
operations..
 ballarin@20318 ` 1` ```(* ``` ballarin@20318 ` 2` ``` Title: HOL/Algebra/IntRing.thy ``` ballarin@20318 ` 3` ``` Id: \$Id\$ ``` ballarin@20318 ` 4` ``` Author: Stephan Hohe, TU Muenchen ``` ballarin@20318 ` 5` ```*) ``` ballarin@20318 ` 6` ballarin@20318 ` 7` ```theory IntRing ``` ballarin@20318 ` 8` ```imports QuotRing IntDef ``` ballarin@20318 ` 9` ```begin ``` ballarin@20318 ` 10` ballarin@20318 ` 11` ballarin@20318 ` 12` ```section {* The Ring of Integers *} ``` ballarin@20318 ` 13` ballarin@20318 ` 14` ```subsection {* Some properties of @{typ int} *} ``` ballarin@20318 ` 15` ballarin@20318 ` 16` ```lemma dvds_imp_abseq: ``` ballarin@20318 ` 17` ``` "\l dvd k; k dvd l\ \ abs l = abs (k::int)" ``` ballarin@20318 ` 18` ```apply (subst abs_split, rule conjI) ``` ballarin@20318 ` 19` ``` apply (clarsimp, subst abs_split, rule conjI) ``` ballarin@20318 ` 20` ``` apply (clarsimp) ``` ballarin@20318 ` 21` ``` apply (cases "k=0", simp) ``` ballarin@20318 ` 22` ``` apply (cases "l=0", simp) ``` ballarin@20318 ` 23` ``` apply (simp add: zdvd_anti_sym) ``` ballarin@20318 ` 24` ``` apply clarsimp ``` ballarin@20318 ` 25` ``` apply (cases "k=0", simp) ``` ballarin@20318 ` 26` ``` apply (simp add: zdvd_anti_sym) ``` ballarin@20318 ` 27` ```apply (clarsimp, subst abs_split, rule conjI) ``` ballarin@20318 ` 28` ``` apply (clarsimp) ``` ballarin@20318 ` 29` ``` apply (cases "l=0", simp) ``` ballarin@20318 ` 30` ``` apply (simp add: zdvd_anti_sym) ``` ballarin@20318 ` 31` ```apply (clarsimp) ``` ballarin@20318 ` 32` ```apply (subgoal_tac "-l = -k", simp) ``` ballarin@20318 ` 33` ```apply (intro zdvd_anti_sym, simp+) ``` ballarin@20318 ` 34` ```done ``` ballarin@20318 ` 35` ballarin@20318 ` 36` ```lemma abseq_imp_dvd: ``` ballarin@20318 ` 37` ``` assumes a_lk: "abs l = abs (k::int)" ``` ballarin@20318 ` 38` ``` shows "l dvd k" ``` ballarin@20318 ` 39` ```proof - ``` ballarin@20318 ` 40` ``` from a_lk ``` ballarin@20318 ` 41` ``` have "nat (abs l) = nat (abs k)" by simp ``` ballarin@20318 ` 42` ``` hence "nat (abs l) dvd nat (abs k)" by simp ``` ballarin@20318 ` 43` ``` hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff) ``` ballarin@20318 ` 44` ``` hence "abs l dvd k" by simp ``` ballarin@20318 ` 45` ``` thus "l dvd k" ``` ballarin@20318 ` 46` ``` apply (unfold dvd_def, cases "l<0") ``` ballarin@20318 ` 47` ``` defer 1 apply clarsimp ``` ballarin@20318 ` 48` ``` proof (clarsimp) ``` ballarin@20318 ` 49` ``` fix k ``` ballarin@20318 ` 50` ``` assume l0: "l < 0" ``` ballarin@20318 ` 51` ``` have "- (l * k) = l * (-k)" by simp ``` ballarin@20318 ` 52` ``` thus "\ka. - (l * k) = l * ka" by fast ``` ballarin@20318 ` 53` ``` qed ``` ballarin@20318 ` 54` ```qed ``` ballarin@20318 ` 55` ballarin@20318 ` 56` ```lemma dvds_eq_abseq: ``` ballarin@20318 ` 57` ``` "(l dvd k \ k dvd l) = (abs l = abs (k::int))" ``` ballarin@20318 ` 58` ```apply rule ``` ballarin@20318 ` 59` ``` apply (simp add: dvds_imp_abseq) ``` ballarin@20318 ` 60` ```apply (rule conjI) ``` ballarin@20318 ` 61` ``` apply (simp add: abseq_imp_dvd)+ ``` ballarin@20318 ` 62` ```done ``` ballarin@20318 ` 63` ballarin@20318 ` 64` ballarin@20318 ` 65` ballarin@20318 ` 66` ```subsection {* The Set of Integers as Algebraic Structure *} ``` ballarin@20318 ` 67` ballarin@20318 ` 68` ```subsubsection {* Definition of @{text "\"} *} ``` ballarin@20318 ` 69` ballarin@20318 ` 70` ```constdefs ``` ballarin@20318 ` 71` ``` int_ring :: "int ring" ("\") ``` ballarin@20318 ` 72` ``` "int_ring \ \carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\" ``` ballarin@20318 ` 73` ballarin@23957 ` 74` ```lemma int_Zcarr [intro!, simp]: ``` ballarin@20318 ` 75` ``` "k \ carrier \" ``` ballarin@23957 ` 76` ``` by (simp add: int_ring_def) ``` ballarin@20318 ` 77` ballarin@20318 ` 78` ```lemma int_is_cring: ``` ballarin@20318 ` 79` ``` "cring \" ``` ballarin@20318 ` 80` ```unfolding int_ring_def ``` ballarin@20318 ` 81` ```apply (rule cringI) ``` ballarin@20318 ` 82` ``` apply (rule abelian_groupI, simp_all) ``` ballarin@20318 ` 83` ``` defer 1 ``` ballarin@20318 ` 84` ``` apply (rule comm_monoidI, simp_all) ``` ballarin@20318 ` 85` ``` apply (rule zadd_zmult_distrib) ``` ballarin@20318 ` 86` ```apply (fast intro: zadd_zminus_inverse2) ``` ballarin@20318 ` 87` ```done ``` ballarin@20318 ` 88` ballarin@23957 ` 89` ```(* ``` ballarin@20318 ` 90` ```lemma int_is_domain: ``` ballarin@20318 ` 91` ``` "domain \" ``` ballarin@20318 ` 92` ```apply (intro domain.intro domain_axioms.intro) ``` ballarin@20318 ` 93` ``` apply (rule int_is_cring) ``` ballarin@20318 ` 94` ``` apply (unfold int_ring_def, simp+) ``` ballarin@20318 ` 95` ```done ``` ballarin@23957 ` 96` ```*) ``` ballarin@23957 ` 97` ```subsubsection {* Interpretations *} ``` ballarin@20318 ` 98` ballarin@23957 ` 99` ```text {* Since definitions of derived operations are global, their ``` ballarin@23957 ` 100` ``` interpretation needs to be done as early as possible --- that is, ``` ballarin@23957 ` 101` ``` with as few assumptions as possible. *} ``` ballarin@23957 ` 102` ballarin@23957 ` 103` ```interpretation int: monoid ["\"] ``` ballarin@23957 ` 104` ``` where "carrier \ = UNIV" ``` ballarin@23957 ` 105` ``` and "mult \ x y = x * y" ``` ballarin@23957 ` 106` ``` and "one \ = 1" ``` ballarin@23957 ` 107` ``` and "pow \ x n = x^n" ``` ballarin@23957 ` 108` ```proof - ``` ballarin@23957 ` 109` ``` -- "Specification" ``` ballarin@23957 ` 110` ``` show "monoid \" by (unfold_locales) (auto simp: int_ring_def) ``` ballarin@23957 ` 111` ``` then interpret int: monoid ["\"] . ``` ballarin@23957 ` 112` ballarin@23957 ` 113` ``` -- "Carrier" ``` ballarin@23957 ` 114` ``` show "carrier \ = UNIV" by (simp add: int_ring_def) ``` ballarin@23957 ` 115` ballarin@23957 ` 116` ``` -- "Operations" ``` ballarin@23957 ` 117` ``` { fix x y show "mult \ x y = x * y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 118` ``` note mult = this ``` ballarin@23957 ` 119` ``` show one: "one \ = 1" by (simp add: int_ring_def) ``` ballarin@23957 ` 120` ``` show "pow \ x n = x^n" by (induct n) (simp, simp add: int_ring_def)+ ``` ballarin@23957 ` 121` ```qed ``` ballarin@23957 ` 122` ballarin@23957 ` 123` ```interpretation int: comm_monoid ["\"] ``` ballarin@23957 ` 124` ``` where "finprod \ f A = (if finite A then setprod f A else arbitrary)" ``` ballarin@23957 ` 125` ```proof - ``` ballarin@23957 ` 126` ``` -- "Specification" ``` ballarin@23957 ` 127` ``` show "comm_monoid \" by (unfold_locales) (auto simp: int_ring_def) ``` ballarin@23957 ` 128` ``` then interpret int: comm_monoid ["\"] . ``` ballarin@23957 ` 129` ballarin@23957 ` 130` ``` -- "Operations" ``` ballarin@23957 ` 131` ``` { fix x y have "mult \ x y = x * y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 132` ``` note mult = this ``` ballarin@23957 ` 133` ``` have one: "one \ = 1" by (simp add: int_ring_def) ``` ballarin@23957 ` 134` ``` show "finprod \ f A = (if finite A then setprod f A else arbitrary)" ``` ballarin@23957 ` 135` ``` proof (cases "finite A") ``` ballarin@23957 ` 136` ``` case True then show ?thesis proof induct ``` ballarin@23957 ` 137` ``` case empty show ?case by (simp add: one) ``` ballarin@23957 ` 138` ``` next ``` ballarin@23957 ` 139` ``` case insert then show ?case by (simp add: Pi_def mult) ``` ballarin@23957 ` 140` ``` qed ``` ballarin@23957 ` 141` ``` next ``` ballarin@23957 ` 142` ``` case False then show ?thesis by (simp add: finprod_def) ``` ballarin@23957 ` 143` ``` qed ``` ballarin@23957 ` 144` ```qed ``` ballarin@23957 ` 145` ballarin@23957 ` 146` ```interpretation int: abelian_monoid ["\"] ``` ballarin@23957 ` 147` ``` where "zero \ = 0" ``` ballarin@23957 ` 148` ``` and "add \ x y = x + y" ``` ballarin@23957 ` 149` ``` and "finsum \ f A = (if finite A then setsum f A else arbitrary)" ``` ballarin@23957 ` 150` ```proof - ``` ballarin@23957 ` 151` ``` -- "Specification" ``` ballarin@23957 ` 152` ``` show "abelian_monoid \" by (unfold_locales) (auto simp: int_ring_def) ``` ballarin@23957 ` 153` ``` then interpret int: abelian_monoid ["\"] . ``` ballarin@20318 ` 154` ballarin@23957 ` 155` ``` -- "Operations" ``` ballarin@23957 ` 156` ``` { fix x y show "add \ x y = x + y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 157` ``` note add = this ``` ballarin@23957 ` 158` ``` show zero: "zero \ = 0" by (simp add: int_ring_def) ``` ballarin@23957 ` 159` ``` show "finsum \ f A = (if finite A then setsum f A else arbitrary)" ``` ballarin@23957 ` 160` ``` proof (cases "finite A") ``` ballarin@23957 ` 161` ``` case True then show ?thesis proof induct ``` ballarin@23957 ` 162` ``` case empty show ?case by (simp add: zero) ``` ballarin@23957 ` 163` ``` next ``` ballarin@23957 ` 164` ``` case insert then show ?case by (simp add: Pi_def add) ``` ballarin@23957 ` 165` ``` qed ``` ballarin@23957 ` 166` ``` next ``` ballarin@23957 ` 167` ``` case False then show ?thesis by (simp add: finsum_def finprod_def) ``` ballarin@23957 ` 168` ``` qed ``` ballarin@23957 ` 169` ```qed ``` ballarin@23957 ` 170` ballarin@23957 ` 171` ```interpretation int: abelian_group ["\"] ``` ballarin@23957 ` 172` ``` where "a_inv \ x = - x" ``` ballarin@23957 ` 173` ``` and "a_minus \ x y = x - y" ``` ballarin@23957 ` 174` ```proof - ``` ballarin@23957 ` 175` ``` -- "Specification" ``` ballarin@23957 ` 176` ``` show "abelian_group \" ``` ballarin@23957 ` 177` ``` proof (rule abelian_groupI) ``` ballarin@23957 ` 178` ``` show "!!x. x \ carrier \ ==> EX y : carrier \. y \\<^bsub>\\<^esub> x = \\<^bsub>\\<^esub>" ``` ballarin@23957 ` 179` ``` by (simp add: int_ring_def) arith ``` ballarin@23957 ` 180` ``` qed (auto simp: int_ring_def) ``` ballarin@23957 ` 181` ``` then interpret int: abelian_group ["\"] . ``` ballarin@23957 ` 182` ballarin@23957 ` 183` ``` -- "Operations" ``` ballarin@23957 ` 184` ``` { fix x y have "add \ x y = x + y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 185` ``` note add = this ``` ballarin@23957 ` 186` ``` have zero: "zero \ = 0" by (simp add: int_ring_def) ``` ballarin@23957 ` 187` ``` { fix x ``` ballarin@23957 ` 188` ``` have "add \ (-x) x = zero \" by (simp add: add zero) ``` ballarin@23957 ` 189` ``` then show "a_inv \ x = - x" by (simp add: int.minus_equality) } ``` ballarin@23957 ` 190` ``` note a_inv = this ``` ballarin@23957 ` 191` ``` show "a_minus \ x y = x - y" by (simp add: int.minus_eq add a_inv) ``` ballarin@23957 ` 192` ```qed ``` ballarin@23957 ` 193` ballarin@23957 ` 194` ```interpretation int: "domain" ["\"] ``` ballarin@23957 ` 195` ``` by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib) ``` ballarin@23957 ` 196` ballarin@23957 ` 197` ballarin@23957 ` 198` ```interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \ |)"] ``` ballarin@23957 ` 199` ``` where "lless (| carrier = UNIV::int set, le = op \ |) x y = (x < y)" ``` ballarin@23957 ` 200` ```proof - ``` ballarin@23957 ` 201` ``` show "partial_order (| carrier = UNIV::int set, le = op \ |)" ``` ballarin@23957 ` 202` ``` by unfold_locales simp_all ``` ballarin@23957 ` 203` ``` show "lless (| carrier = UNIV::int set, le = op \ |) x y = (x < y)" ``` ballarin@23957 ` 204` ``` by (simp add: lless_def) auto ``` ballarin@23957 ` 205` ```qed ``` ballarin@23957 ` 206` ballarin@23957 ` 207` ```interpretation int: lattice ["(| carrier = UNIV::int set, le = op \ |)"] ``` ballarin@23957 ` 208` ``` where "join (| carrier = UNIV::int set, le = op \ |) x y = max x y" ``` ballarin@23957 ` 209` ``` and "meet (| carrier = UNIV::int set, le = op \ |) x y = min x y" ``` ballarin@23957 ` 210` ```proof - ``` ballarin@23957 ` 211` ``` let ?Z = "(| carrier = UNIV::int set, le = op \ |)" ``` ballarin@23957 ` 212` ``` show "lattice ?Z" ``` ballarin@23957 ` 213` ``` apply unfold_locales ``` ballarin@23957 ` 214` ``` apply (simp add: least_def Upper_def) ``` ballarin@23957 ` 215` ``` apply arith ``` ballarin@23957 ` 216` ``` apply (simp add: greatest_def Lower_def) ``` ballarin@23957 ` 217` ``` apply arith ``` ballarin@23957 ` 218` ``` done ``` ballarin@23957 ` 219` ``` then interpret int: lattice ["?Z"] . ``` ballarin@23957 ` 220` ``` show "join ?Z x y = max x y" ``` ballarin@23957 ` 221` ``` apply (rule int.joinI) ``` ballarin@23957 ` 222` ``` apply (simp_all add: least_def Upper_def) ``` ballarin@23957 ` 223` ``` apply arith ``` ballarin@23957 ` 224` ``` done ``` ballarin@23957 ` 225` ``` show "meet ?Z x y = min x y" ``` ballarin@23957 ` 226` ``` apply (rule int.meetI) ``` ballarin@23957 ` 227` ``` apply (simp_all add: greatest_def Lower_def) ``` ballarin@23957 ` 228` ``` apply arith ``` ballarin@23957 ` 229` ``` done ``` ballarin@23957 ` 230` ```qed ``` ballarin@23957 ` 231` ballarin@23957 ` 232` ```interpretation int: total_order ["(| carrier = UNIV::int set, le = op \ |)"] ``` ballarin@23957 ` 233` ``` by unfold_locales clarsimp ``` ballarin@23957 ` 234` ballarin@23957 ` 235` ```(* ``` ballarin@20318 ` 236` ```lemma int_le_total_order: ``` ballarin@22063 ` 237` ``` "total_order (| carrier = UNIV::int set, le = op \ |)" ``` ballarin@22063 ` 238` ``` apply (rule partial_order.total_orderI) ``` ballarin@22063 ` 239` ``` apply (rule partial_order.intro, simp+) ``` ballarin@22063 ` 240` ``` apply clarsimp ``` ballarin@22063 ` 241` ``` done ``` ballarin@20318 ` 242` ballarin@21896 ` 243` ```lemma less_int: ``` ballarin@22063 ` 244` ``` "lless (| carrier = UNIV::int set, le = op \ |) = (op <)" ``` ballarin@22063 ` 245` ``` by (auto simp add: expand_fun_eq lless_def) ``` ballarin@21896 ` 246` ballarin@21896 ` 247` ```lemma join_int: ``` ballarin@22063 ` 248` ``` "join (| carrier = UNIV::int set, le = op \ |) = max" ``` ballarin@21896 ` 249` ``` apply (simp add: expand_fun_eq max_def) ``` ballarin@21896 ` 250` ``` apply (rule+) ``` ballarin@21896 ` 251` ``` apply (rule lattice.joinI) ``` ballarin@21896 ` 252` ``` apply (simp add: int_le_total_order total_order.axioms) ``` ballarin@22063 ` 253` ``` apply (simp add: least_def Upper_def) ``` ballarin@21896 ` 254` ``` apply arith ``` ballarin@21896 ` 255` ``` apply simp apply simp ``` ballarin@21896 ` 256` ``` apply (rule lattice.joinI) ``` ballarin@21896 ` 257` ``` apply (simp add: int_le_total_order total_order.axioms) ``` ballarin@22063 ` 258` ``` apply (simp add: least_def Upper_def) ``` ballarin@21896 ` 259` ``` apply arith ``` ballarin@21896 ` 260` ``` apply simp apply simp ``` ballarin@21896 ` 261` ``` done ``` ballarin@21896 ` 262` ballarin@21896 ` 263` ```lemma meet_int: ``` ballarin@22063 ` 264` ``` "meet (| carrier = UNIV::int set, le = op \ |) = min" ``` ballarin@21896 ` 265` ``` apply (simp add: expand_fun_eq min_def) ``` ballarin@21896 ` 266` ``` apply (rule+) ``` ballarin@21896 ` 267` ``` apply (rule lattice.meetI) ``` ballarin@21896 ` 268` ``` apply (simp add: int_le_total_order total_order.axioms) ``` ballarin@22063 ` 269` ``` apply (simp add: greatest_def Lower_def) ``` ballarin@21896 ` 270` ``` apply arith ``` ballarin@21896 ` 271` ``` apply simp apply simp ``` ballarin@21896 ` 272` ``` apply (rule lattice.meetI) ``` ballarin@21896 ` 273` ``` apply (simp add: int_le_total_order total_order.axioms) ``` ballarin@22063 ` 274` ``` apply (simp add: greatest_def Lower_def) ``` ballarin@21896 ` 275` ``` apply arith ``` ballarin@21896 ` 276` ``` apply simp apply simp ``` ballarin@21896 ` 277` ``` done ``` ballarin@21896 ` 278` ballarin@22063 ` 279` ```lemma carrier_int: ``` ballarin@22063 ` 280` ``` "carrier (| carrier = UNIV::int set, le = op \ |) = UNIV" ``` ballarin@22063 ` 281` ``` apply simp ``` ballarin@22063 ` 282` ``` done ``` ballarin@22063 ` 283` ballarin@22063 ` 284` ```text {* Interpretation unfolding @{text lless}, @{text join} and @{text ``` ballarin@21896 ` 285` ``` meet} since they have natural representations in @{typ int}. *} ``` ballarin@21896 ` 286` ballarin@21896 ` 287` ```interpretation ``` ballarin@22063 ` 288` ``` int [unfolded less_int join_int meet_int carrier_int]: ``` ballarin@22063 ` 289` ``` total_order ["(| carrier = UNIV::int set, le = op \ |)"] ``` ballarin@22063 ` 290` ``` by (rule int_le_total_order) ``` ballarin@23957 ` 291` ```*) ``` ballarin@20318 ` 292` ballarin@20318 ` 293` ballarin@20318 ` 294` ```subsubsection {* Generated Ideals of @{text "\"} *} ``` ballarin@20318 ` 295` ballarin@20318 ` 296` ```lemma int_Idl: ``` ballarin@20318 ` 297` ``` "Idl\<^bsub>\\<^esub> {a} = {x * a | x. True}" ``` ballarin@23957 ` 298` ``` apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def) ``` ballarin@23957 ` 299` ``` apply (simp add: cgenideal_def int_ring_def) ``` ballarin@23957 ` 300` ``` done ``` ballarin@20318 ` 301` ballarin@20318 ` 302` ```lemma multiples_principalideal: ``` ballarin@20318 ` 303` ``` "principalideal {x * a | x. True } \" ``` ballarin@20318 ` 304` ```apply (subst int_Idl[symmetric], rule principalidealI) ``` ballarin@23957 ` 305` ``` apply (rule int.genideal_ideal, simp) ``` ballarin@20318 ` 306` ```apply fast ``` ballarin@20318 ` 307` ```done ``` ballarin@20318 ` 308` ballarin@20318 ` 309` ```lemma prime_primeideal: ``` ballarin@20318 ` 310` ``` assumes prime: "prime (nat p)" ``` ballarin@20318 ` 311` ``` shows "primeideal (Idl\<^bsub>\\<^esub> {p}) \" ``` ballarin@20318 ` 312` ```apply (rule primeidealI) ``` ballarin@23957 ` 313` ``` apply (rule int.genideal_ideal, simp) ``` ballarin@20318 ` 314` ``` apply (rule int_is_cring) ``` ballarin@23957 ` 315` ``` apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) ``` ballarin@20318 ` 316` ``` apply (simp add: int_ring_def) ``` ballarin@20318 ` 317` ``` apply clarsimp defer 1 ``` ballarin@23957 ` 318` ``` apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) ``` ballarin@20318 ` 319` ``` apply (simp add: int_ring_def) ``` ballarin@20318 ` 320` ``` apply (elim exE) ``` ballarin@20318 ` 321` ```proof - ``` ballarin@20318 ` 322` ``` fix a b x ``` ballarin@20318 ` 323` ballarin@20318 ` 324` ``` from prime ``` ballarin@20318 ` 325` ``` have ppos: "0 <= p" by (simp add: prime_def) ``` ballarin@20318 ` 326` ``` have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x" ``` ballarin@20318 ` 327` ``` proof - ``` ballarin@20318 ` 328` ``` fix x ``` ballarin@20318 ` 329` ``` assume "nat p dvd nat (abs x)" ``` ballarin@20318 ` 330` ``` hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric]) ``` ballarin@20318 ` 331` ``` thus "p dvd x" by (simp add: ppos) ``` ballarin@20318 ` 332` ``` qed ``` ballarin@20318 ` 333` ballarin@20318 ` 334` ballarin@20318 ` 335` ``` assume "a * b = x * p" ``` ballarin@20318 ` 336` ``` hence "p dvd a * b" by simp ``` ballarin@20318 ` 337` ``` hence "nat p dvd nat (abs (a * b))" ``` ballarin@20318 ` 338` ``` apply (subst nat_dvd_iff, clarsimp) ``` ballarin@20318 ` 339` ``` apply (rule conjI, clarsimp, simp add: zabs_def) ``` ballarin@20318 ` 340` ``` proof (clarsimp) ``` ballarin@20318 ` 341` ``` assume a: " ~ 0 <= p" ``` ballarin@20318 ` 342` ``` from prime ``` ballarin@20318 ` 343` ``` have "0 < p" by (simp add: prime_def) ``` ballarin@20318 ` 344` ``` from a and this ``` ballarin@20318 ` 345` ``` have "False" by simp ``` ballarin@20318 ` 346` ``` thus "nat (abs (a * b)) = 0" .. ``` ballarin@20318 ` 347` ``` qed ``` ballarin@20318 ` 348` ``` hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib) ``` ballarin@20318 ` 349` ``` hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime]) ``` ballarin@20318 ` 350` ``` hence "p dvd a | p dvd b" by (fast intro: unnat) ``` ballarin@20318 ` 351` ``` thus "(EX x. a = x * p) | (EX x. b = x * p)" ``` ballarin@20318 ` 352` ``` proof ``` ballarin@20318 ` 353` ``` assume "p dvd a" ``` ballarin@20318 ` 354` ``` hence "EX x. a = p * x" by (simp add: dvd_def) ``` ballarin@20318 ` 355` ``` from this obtain x ``` ballarin@20318 ` 356` ``` where "a = p * x" by fast ``` ballarin@20318 ` 357` ``` hence "a = x * p" by simp ``` ballarin@20318 ` 358` ``` hence "EX x. a = x * p" by simp ``` ballarin@20318 ` 359` ``` thus "(EX x. a = x * p) | (EX x. b = x * p)" .. ``` ballarin@20318 ` 360` ``` next ``` ballarin@20318 ` 361` ``` assume "p dvd b" ``` ballarin@20318 ` 362` ``` hence "EX x. b = p * x" by (simp add: dvd_def) ``` ballarin@20318 ` 363` ``` from this obtain x ``` ballarin@20318 ` 364` ``` where "b = p * x" by fast ``` ballarin@20318 ` 365` ``` hence "b = x * p" by simp ``` ballarin@20318 ` 366` ``` hence "EX x. b = x * p" by simp ``` ballarin@20318 ` 367` ``` thus "(EX x. a = x * p) | (EX x. b = x * p)" .. ``` ballarin@20318 ` 368` ``` qed ``` ballarin@20318 ` 369` ```next ``` ballarin@20318 ` 370` ``` assume "UNIV = {uu. EX x. uu = x * p}" ``` ballarin@20318 ` 371` ``` from this obtain x ``` ballarin@20318 ` 372` ``` where "1 = x * p" by fast ``` ballarin@20318 ` 373` ``` from this [symmetric] ``` ballarin@20318 ` 374` ``` have "p * x = 1" by (subst zmult_commute) ``` ballarin@20318 ` 375` ``` hence "\p * x\ = 1" by simp ``` ballarin@20318 ` 376` ``` hence "\p\ = 1" by (rule abs_zmult_eq_1) ``` ballarin@20318 ` 377` ``` from this and prime ``` ballarin@20318 ` 378` ``` show "False" by (simp add: prime_def) ``` ballarin@20318 ` 379` ```qed ``` ballarin@20318 ` 380` ballarin@20318 ` 381` ballarin@20318 ` 382` ```subsubsection {* Ideals and Divisibility *} ``` ballarin@20318 ` 383` ballarin@20318 ` 384` ```lemma int_Idl_subset_ideal: ``` ballarin@20318 ` 385` ``` "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} = (k \ Idl\<^bsub>\\<^esub> {l})" ``` ballarin@23957 ` 386` ```by (rule int.Idl_subset_ideal', simp+) ``` ballarin@20318 ` 387` ballarin@20318 ` 388` ```lemma Idl_subset_eq_dvd: ``` ballarin@20318 ` 389` ``` "(Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) = (l dvd k)" ``` ballarin@20318 ` 390` ```apply (subst int_Idl_subset_ideal, subst int_Idl, simp) ``` ballarin@20318 ` 391` ```apply (rule, clarify) ``` ballarin@20318 ` 392` ```apply (simp add: dvd_def, clarify) ``` ballarin@23957 ` 393` ```apply (simp add: int.m_comm) ``` ballarin@20318 ` 394` ```done ``` ballarin@20318 ` 395` ballarin@20318 ` 396` ```lemma dvds_eq_Idl: ``` ballarin@20318 ` 397` ``` "(l dvd k \ k dvd l) = (Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l})" ``` ballarin@20318 ` 398` ```proof - ``` ballarin@20318 ` 399` ``` have a: "l dvd k = (Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric]) ``` ballarin@20318 ` 400` ``` have b: "k dvd l = (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric]) ``` ballarin@20318 ` 401` ballarin@20318 ` 402` ``` have "(l dvd k \ k dvd l) = ((Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) \ (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k}))" ``` ballarin@20318 ` 403` ``` by (subst a, subst b, simp) ``` ballarin@20318 ` 404` ``` also have "((Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) \ (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k})) = (Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l})" by (rule, fast+) ``` ballarin@20318 ` 405` ``` finally ``` ballarin@20318 ` 406` ``` show ?thesis . ``` ballarin@20318 ` 407` ```qed ``` ballarin@20318 ` 408` ballarin@20318 ` 409` ```lemma Idl_eq_abs: ``` ballarin@20318 ` 410` ``` "(Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l}) = (abs l = abs k)" ``` ballarin@20318 ` 411` ```apply (subst dvds_eq_abseq[symmetric]) ``` ballarin@20318 ` 412` ```apply (rule dvds_eq_Idl[symmetric]) ``` ballarin@20318 ` 413` ```done ``` ballarin@20318 ` 414` ballarin@20318 ` 415` ballarin@20318 ` 416` ```subsubsection {* Ideals and the Modulus *} ``` ballarin@20318 ` 417` ballarin@20318 ` 418` ```constdefs ``` ballarin@20318 ` 419` ``` ZMod :: "int => int => int set" ``` ballarin@20318 ` 420` ``` "ZMod k r == (Idl\<^bsub>\\<^esub> {k}) +>\<^bsub>\\<^esub> r" ``` ballarin@20318 ` 421` ballarin@20318 ` 422` ```lemmas ZMod_defs = ``` ballarin@20318 ` 423` ``` ZMod_def genideal_def ``` ballarin@20318 ` 424` ballarin@20318 ` 425` ```lemma rcos_zfact: ``` ballarin@20318 ` 426` ``` assumes kIl: "k \ ZMod l r" ``` ballarin@20318 ` 427` ``` shows "EX x. k = x * l + r" ``` ballarin@20318 ` 428` ```proof - ``` ballarin@20318 ` 429` ``` from kIl[unfolded ZMod_def] ``` ballarin@20318 ` 430` ``` have "\xl\Idl\<^bsub>\\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def) ``` ballarin@20318 ` 431` ``` from this obtain xl ``` ballarin@20318 ` 432` ``` where xl: "xl \ Idl\<^bsub>\\<^esub> {l}" ``` ballarin@20318 ` 433` ``` and k: "k = xl + r" ``` ballarin@20318 ` 434` ``` by auto ``` ballarin@20318 ` 435` ``` from xl obtain x ``` ballarin@20318 ` 436` ``` where "xl = x * l" ``` ballarin@20318 ` 437` ``` by (simp add: int_Idl, fast) ``` ballarin@20318 ` 438` ``` from k and this ``` ballarin@20318 ` 439` ``` have "k = x * l + r" by simp ``` ballarin@20318 ` 440` ``` thus "\x. k = x * l + r" .. ``` ballarin@20318 ` 441` ```qed ``` ballarin@20318 ` 442` ballarin@20318 ` 443` ```lemma ZMod_imp_zmod: ``` ballarin@20318 ` 444` ``` assumes zmods: "ZMod m a = ZMod m b" ``` ballarin@20318 ` 445` ``` shows "a mod m = b mod m" ``` ballarin@20318 ` 446` ```proof - ``` ballarin@23957 ` 447` ``` interpret ideal ["Idl\<^bsub>\\<^esub> {m}" \] by (rule int.genideal_ideal, fast) ``` ballarin@20318 ` 448` ``` from zmods ``` ballarin@20318 ` 449` ``` have "b \ ZMod m a" ``` ballarin@20318 ` 450` ``` unfolding ZMod_def ``` ballarin@20318 ` 451` ``` by (simp add: a_repr_independenceD) ``` ballarin@20318 ` 452` ``` from this ``` ballarin@20318 ` 453` ``` have "EX x. b = x * m + a" by (rule rcos_zfact) ``` ballarin@20318 ` 454` ``` from this obtain x ``` ballarin@20318 ` 455` ``` where "b = x * m + a" ``` ballarin@20318 ` 456` ``` by fast ``` ballarin@20318 ` 457` ballarin@20318 ` 458` ``` hence "b mod m = (x * m + a) mod m" by simp ``` ballarin@20318 ` 459` ``` also ``` ballarin@20318 ` 460` ``` have "\ = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq) ``` ballarin@20318 ` 461` ``` also ``` ballarin@20318 ` 462` ``` have "\ = a mod m" by simp ``` ballarin@20318 ` 463` ``` finally ``` ballarin@20318 ` 464` ``` have "b mod m = a mod m" . ``` ballarin@20318 ` 465` ``` thus "a mod m = b mod m" .. ``` ballarin@20318 ` 466` ```qed ``` ballarin@20318 ` 467` ballarin@20318 ` 468` ```lemma ZMod_mod: ``` ballarin@20318 ` 469` ``` shows "ZMod m a = ZMod m (a mod m)" ``` ballarin@20318 ` 470` ```proof - ``` ballarin@23957 ` 471` ``` interpret ideal ["Idl\<^bsub>\\<^esub> {m}" \] by (rule int.genideal_ideal, fast) ``` ballarin@20318 ` 472` ``` show ?thesis ``` ballarin@20318 ` 473` ``` unfolding ZMod_def ``` ballarin@20318 ` 474` ``` apply (rule a_repr_independence'[symmetric]) ``` ballarin@20318 ` 475` ``` apply (simp add: int_Idl a_r_coset_defs) ``` ballarin@20318 ` 476` ``` apply (simp add: int_ring_def) ``` ballarin@20318 ` 477` ``` proof - ``` ballarin@20318 ` 478` ``` have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality) ``` ballarin@20318 ` 479` ``` hence "a = (a div m) * m + (a mod m)" by simp ``` ballarin@20318 ` 480` ``` thus "\h. (\x. h = x * m) \ a = h + a mod m" by fast ``` ballarin@20318 ` 481` ``` qed simp ``` ballarin@20318 ` 482` ```qed ``` ballarin@20318 ` 483` ballarin@20318 ` 484` ```lemma zmod_imp_ZMod: ``` ballarin@20318 ` 485` ``` assumes modeq: "a mod m = b mod m" ``` ballarin@20318 ` 486` ``` shows "ZMod m a = ZMod m b" ``` ballarin@20318 ` 487` ```proof - ``` ballarin@20318 ` 488` ``` have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod) ``` ballarin@20318 ` 489` ``` also have "\ = ZMod m (b mod m)" by (simp add: modeq[symmetric]) ``` ballarin@20318 ` 490` ``` also have "\ = ZMod m b" by (rule ZMod_mod[symmetric]) ``` ballarin@20318 ` 491` ``` finally show ?thesis . ``` ballarin@20318 ` 492` ```qed ``` ballarin@20318 ` 493` ballarin@20318 ` 494` ```corollary ZMod_eq_mod: ``` ballarin@20318 ` 495` ``` shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)" ``` ballarin@20318 ` 496` ```by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod) ``` ballarin@20318 ` 497` ballarin@20318 ` 498` ballarin@20318 ` 499` ```subsubsection {* Factorization *} ``` ballarin@20318 ` 500` ballarin@20318 ` 501` ```constdefs ``` ballarin@20318 ` 502` ``` ZFact :: "int \ int set ring" ``` ballarin@20318 ` 503` ``` "ZFact k == \ Quot (Idl\<^bsub>\\<^esub> {k})" ``` ballarin@20318 ` 504` ballarin@20318 ` 505` ```lemmas ZFact_defs = ZFact_def FactRing_def ``` ballarin@20318 ` 506` ballarin@20318 ` 507` ```lemma ZFact_is_cring: ``` ballarin@20318 ` 508` ``` shows "cring (ZFact k)" ``` ballarin@20318 ` 509` ```apply (unfold ZFact_def) ``` ballarin@20318 ` 510` ```apply (rule ideal.quotient_is_cring) ``` ballarin@20318 ` 511` ``` apply (intro ring.genideal_ideal) ``` ballarin@20318 ` 512` ``` apply (simp add: cring.axioms[OF int_is_cring] ring.intro) ``` ballarin@20318 ` 513` ``` apply simp ``` ballarin@20318 ` 514` ```apply (rule int_is_cring) ``` ballarin@20318 ` 515` ```done ``` ballarin@20318 ` 516` ballarin@20318 ` 517` ```lemma ZFact_zero: ``` ballarin@20318 ` 518` ``` "carrier (ZFact 0) = (\a. {{a}})" ``` ballarin@23957 ` 519` ```apply (insert int.genideal_zero) ``` ballarin@20318 ` 520` ```apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) ``` ballarin@20318 ` 521` ```done ``` ballarin@20318 ` 522` ballarin@20318 ` 523` ```lemma ZFact_one: ``` ballarin@20318 ` 524` ``` "carrier (ZFact 1) = {UNIV}" ``` ballarin@20318 ` 525` ```apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) ``` ballarin@23957 ` 526` ```apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps]) ``` ballarin@20318 ` 527` ```apply (rule, rule, clarsimp) ``` ballarin@20318 ` 528` ``` apply (rule, rule, clarsimp) ``` ballarin@20318 ` 529` ``` apply (rule, clarsimp, arith) ``` ballarin@20318 ` 530` ```apply (rule, clarsimp) ``` ballarin@20318 ` 531` ```apply (rule exI[of _ "0"], clarsimp) ``` ballarin@20318 ` 532` ```done ``` ballarin@20318 ` 533` ballarin@20318 ` 534` ```lemma ZFact_prime_is_domain: ``` ballarin@20318 ` 535` ``` assumes pprime: "prime (nat p)" ``` ballarin@20318 ` 536` ``` shows "domain (ZFact p)" ``` ballarin@20318 ` 537` ```apply (unfold ZFact_def) ``` ballarin@20318 ` 538` ```apply (rule primeideal.quotient_is_domain) ``` ballarin@20318 ` 539` ```apply (rule prime_primeideal[OF pprime]) ``` ballarin@20318 ` 540` ```done ``` ballarin@20318 ` 541` ballarin@20318 ` 542` ```end ```