Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

For the record, I have now pushed the change to Isabelle, see 
http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd 
.

Mathias

> On 05 Jul 2016, at 14:03, Mathias Fleury  wrote:
> 
> Hi all,
> 
> after some more experiments, I found out that there is another difference 
> between explicit typeclass annotations and lemmas in the context: the former 
> theorems are included in instantiations but are not included in 
> interpretations. This usually does not make a difference, since there is 
> usually a single order on a type.
> 
> Instead, I introduced an additional typeclass to the hierarchy. The change 
> was successfully tested on testboard (mercurial diff 
> , status 
> ), and does not need 
> any AFP change.
> 
> 
> Does someone have an opinion on this change?
> 
> 
> Mathias
>  
>> On 04 Jul 2016, at 14:20, Mathias Fleury > > wrote:
>> 
>> 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 >> > 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
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> 

Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

Hi all,

after some more experiments, I found out that there is another difference 
between explicit typeclass annotations and lemmas in the context: the former 
theorems are included in instantiations but are not included in 
interpretations. This usually does not make a difference, since there is 
usually a single order on a type.

Instead, I introduced an additional typeclass to the hierarchy. The change was 
successfully tested on testboard (mercurial diff 
, status 
), and does not need 
any AFP change.


Does someone have an opinion on this change?


Mathias
 
> On 04 Jul 2016, at 14:20, Mathias Fleury  wrote:
> 
> 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 > > 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

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  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

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