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._______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
