[isabelle-dev] Simplification theorems with more general typeclasses

[Johannes Hölzl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev