[isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

Dear type-classes and simplifier experts,

in the plan of instantiating multisets with the multiset ordering, I am trying to instantiate the multisets with additional typeclasses to get specific simplification theorems. The aim is to mimic the simplifier’s behaviour of other types like natural numbers. One of my problems can be nicely illustrated by the following lemma: “M <= M + N <-> 0 <= N”. 


Analog simplification rules already exist for rings (e.g., natural numbers*) and ordered groups too:
	thm Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_zero
	thm Groups.ordered_ab_group_add_class.le_add_same_cancel1
Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as [simp].


However, the multisets are neither a group (no inverse for the law “+”) nor a ring (no multiplication). I could duplicate the theorems, but I noticed that the proofs of the theorems do only rely on the fact it is a monoid_add (for the zero element) and an ordered_ab_semigroup_add_imp_le (for the order). The following theorem would work too and is general enough to include the multiset case:

lemma le_add_same_cancel1 [simp]:
  “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b ⟷ 0 ≤ b”
  using add_le_cancel_left [of a 0] by simp


Are there any obvious differences between this more general version with explicit type class annotations and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no, would it make sense to use this version in Isabelle?



Thanks in advance,
Mathias Fleury




* for natural numbers, the simproc Numeral_Simprocs.natle_cancel_numerals is able to do it too.
-------------- n�chster Teil --------------
Ein Dateianhang mit HTML-Daten wurde abgetrennt...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160628/e129ab90/attachment.html>