| changeset 45694 | 4a8743618257 |
| parent 45607 | 16b4f5774621 |
| child 46027 | ff3c4f2bee01 |
| 45693:bbd2c7ffc02c | 45694:4a8743618257 |
|---|---|
16 subsection {* The equivalence relation underlying the integers *} |
16 subsection {* The equivalence relation underlying the integers *} |
17 |
17 |
18 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where |
18 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where |
19 "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" |
19 "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" |
20 |
20 |
21 typedef (Integ) |
21 definition "Integ = UNIV//intrel" |
22 int = "UNIV//intrel" |
22 |
23 by (auto simp add: quotient_def) |
23 typedef (open) int = Integ |
24 morphisms Rep_Integ Abs_Integ |
|
25 unfolding Integ_def by (auto simp add: quotient_def) |
|
24 |
26 |
25 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
27 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
26 begin |
28 begin |
27 |
29 |
28 definition |
30 definition |