src/HOL/Number_Theory/Residues.thy
 changeset 35416 d8d7d1b785af parent 32479 521cc9bf2958 child 36350 bc7982c54e37
equal inserted replaced
35342:4dc65845eab3 35416:d8d7d1b785af
`    20  `
`    20  `
`    21   A locale for residue rings`
`    21   A locale for residue rings`
`    22 `
`    22 `
`    23 *)`
`    23 *)`
`    24 `
`    24 `
`    25 constdefs `
`    25 definition residue_ring :: "int => int ring" where`
`    26   residue_ring :: "int => int ring"`
`       `
`    27   "residue_ring m == (| `
`    26   "residue_ring m == (| `
`    28     carrier =       {0..m - 1}, `
`    27     carrier =       {0..m - 1}, `
`    29     mult =          (%x y. (x * y) mod m),`
`    28     mult =          (%x y. (x * y) mod m),`
`    30     one =           1,`
`    29     one =           1,`
`    31     zero =          0,`
`    30     zero =          0,`
`   285 `
`   284 `
`   286 subsection{* Euler's theorem *}`
`   285 subsection{* Euler's theorem *}`
`   287 `
`   286 `
`   288 (* the definition of the phi function *)`
`   287 (* the definition of the phi function *)`
`   289 `
`   288 `
`   290 constdefs`
`   289 definition phi :: "int => nat" where`
`   291   phi :: "int => nat"`
`       `
`   292   "phi m == card({ x. 0 < x & x < m & gcd x m = 1})" `
`   290   "phi m == card({ x. 0 < x & x < m & gcd x m = 1})" `
`   293 `
`   291 `
`   294 lemma phi_zero [simp]: "phi 0 = 0"`
`   292 lemma phi_zero [simp]: "phi 0 = 0"`
`   295   apply (subst phi_def)`
`   293   apply (subst phi_def)`
`   296 (* Auto hangs here. Once again, where is the simplification rule `
`   294 (* Auto hangs here. Once again, where is the simplification rule `