Hi Mathias, there is at least the type class 'canonically_ordered_monoid' which has the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a. Are the multisets already in this typeclass?
- Johannes Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb 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_ze > ro > 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/isabel > le-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev