theory More_Advanced_Topics imports Main begin (* Construct the integers as a quotient of two natural numbers, following the start I made in lectures. Capture the notion of an additive semigroup, additive monoid, and additive commutative monoid, as a hierarchy of locales in Isabelle. Capture the notion of a multiplicative semigroup, multiplicative monoid, and multiplicative commutative monoid, as a hierarchy of locales in Isabelle. Use the two definition of multiplicative commutative monoid and additive commutative monoids that you have just defined to capture the notion of a commutative semiring. Show that identities are unique in (multiplicative and additive) monoids. Define a generic exponentiation operation of type "'a \ nat \ 'a" in multiplicative monoids. Show that the usual laws of exponents hold in commutative monoids: 1. x\<^sup>mx\<^sup>n = x\<^sup>m\<^sup>+\<^sup>n 2. (x\<^sup>m)\<^sup>n = x\<^sup>(\<^sup>m\<^sup>n\<^sup>) 3. x\<^sup>1 = x 4. 1\<^sup>x = 1 (for x \ 0) 5. (xy)\<^sup>n = x\<^sup>ny\<^sup>n Show that your integer quotient_type can be interpreted as a commutative semiring. Obtain as a corollary of the above that the laws of exponents hold for your integer datatype, and the additive and multiplicative identities of the integer type are unique. *) end