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