Larry Paulson
2015-05-27 16:17:17 UTC
We currently define the type class semiring_numeral_div in the theory Divides, see attached snippet below. This type class is already general enough to allow some facts involving linearly ordered arithmetic types to be proved just once and be valid over the range from nat to real. The only problem is that type real is not an instance of semiring_numeral_div, for obvious reasons. Would it not be appropriate to attach the axiom le_add_diff_inverse2 to a more general type class, such as linordered_semidom?
Larry
subsection {* Generic numeral division with a pragmatic type class *}
text {*
The following type class contains everything necessary to formulate
a division algorithm in ring structures with numerals, restricted
to its positive segments. This is its primary motiviation, and it
could surely be formulated using a more fine-grained, more algebraic
and less technical class hierarchy.
*}
class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
assumes le_add_diff_inverse2: "b ≤ a ⟹ a - b + b = a"
Larry
subsection {* Generic numeral division with a pragmatic type class *}
text {*
The following type class contains everything necessary to formulate
a division algorithm in ring structures with numerals, restricted
to its positive segments. This is its primary motiviation, and it
could surely be formulated using a more fine-grained, more algebraic
and less technical class hierarchy.
*}
class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
assumes le_add_diff_inverse2: "b ≤ a ⟹ a - b + b = a"