Hi Johannes,
the multiset ordering (contrary to the subset ordering) does not have this
property:
lemma "{#0#} <= {#Suc 0#}”
unfolding Multiset_Order.le_multiset⇩H⇩O by auto
(the actual notation is #⊆# and not <=).
I tried locally to apply the changes of my previous email this week-end. Except
some proofs inside the typeclass definitions (i.e. in the files Groups.thy,
Rings.thy, and Missing_Ring.thy), no other changes were needed in Isabelle or
the AFP.
Thanks for your answer,
Mathias
> On 04 Jul 2016, at 13:22, Johannes Hölzl <hoe...@in.tum.de> wrote:
>
> 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
