equal
deleted
inserted
replaced
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 |