equal
deleted
inserted
replaced
61 understood how to use both mechanisms for dealing with quotient |
61 understood how to use both mechanisms for dealing with quotient |
62 constructions in HOL (see \cite{Homeier05,Paulson06}). For example the |
62 constructions in HOL (see \cite{Homeier05,Paulson06}). For example the |
63 integers in Isabelle/HOL are constructed by a quotient construction over the |
63 integers in Isabelle/HOL are constructed by a quotient construction over the |
64 type @{typ "nat \<times> nat"} and the equivalence relation |
64 type @{typ "nat \<times> nat"} and the equivalence relation |
65 |
65 |
66 @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"} |
66 @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"} |
67 |
67 |
68 \noindent |
68 \noindent |
69 This constructions yields the new type @{typ int} and definitions for @{text |
69 This constructions yields the new type @{typ int} and definitions for @{text |
70 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of |
70 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of |
71 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations |
71 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations |