Email Gateway (Jun 03 2025 at 07:57): Email Gateway (Jun 03 2025 at 07:57):From: Tobias Nipkow <nipkow@in.tum.de>
Larry recently needed a subtraction function on lists. Of course it is easy to
define, but there are at least two alternatives:
definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = filter (λx. x ∉ set ys) xs"
definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"
One is geared towards sets, the othe one towards multisets. (Larry remarked that
the latter turns lists into a monus = monoid with minus, but we don't use the
class system on lists).
Any comments? Should we have both of them? Names? Notation? Definition vs
abbreviation (definitions require more thms that are for free with abbrev.)? ...
Tobias
Email Gateway (Jun 03 2025 at 19:16):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
I like both, although both are ignoring the non-commutative nature of
the subtracted lists and, as Tobias said, they are more about sets
(therefore it is not clear to me immediately in what sense we would get
a monus on lists).
How about the third one geared towards non-commutativity of lists:
fun minus_list_list :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_list xs [] = xs" |
"minus_list_list [] ys = []" |
"minus_list_list (x # xs) (y # ys) = (if x = y then minus_list_list xs
ys else x # (minus_list_list xs (y # ys)))"
I believe any of them should be a definition (if introduced), not
abbreviation. Not sure they deserve a special notation, but that would
depend on applications.
Stepan
On 03-Jun-25 9:57 AM, Tobias Nipkow wrote:
Larry recently needed a subtraction function on lists. Of course it is
easy to define, but there are at least two alternatives:definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = filter (λx. x ∉ set ys) xs"definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"One is geared towards sets, the othe one towards multisets. (Larry
remarked that the latter turns lists into a monus = monoid with minus,
but we don't use the class system on lists).Any comments? Should we have both of them? Names? Notation? Definition
vs abbreviation (definitions require more thms that are for free with
abbrev.)? ...Tobias
Email Gateway (Jun 04 2025 at 09:36):From: 山田晃久 <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I'd like to remark that minus_list_mset x y and minus_list_list x y are left divisors y\x rather than right x/y for @, in the sense
In this sense, the arguments may be flipped. Then minus_list_mset would just be "foldr remove1" for which an abbreviation would suffice.
(of course, I do not propose \ as notation.)
For naming, I'd propose something related to (left) factors. "minus" would be confusing when one sees strings as regular expressions.
Best,
Akihisa
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Sent: Wednesday, June 4, 2025 4:15
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Minus on lists
I like both, although both are ignoring the non-commutative nature of
the subtracted lists and, as Tobias said, they are more about sets
(therefore it is not clear to me immediately in what sense we would get
a monus on lists).
How about the third one geared towards non-commutativity of lists:
fun minus_list_list :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_list xs [] = xs" |
"minus_list_list [] ys = []" |
"minus_list_list (x # xs) (y # ys) = (if x = y then minus_list_list xs
ys else x # (minus_list_list xs (y # ys)))"
I believe any of them should be a definition (if introduced), not
abbreviation. Not sure they deserve a special notation, but that would
depend on applications.
Stepan
On 03-Jun-25 9:57 AM, Tobias Nipkow wrote:
Larry recently needed a subtraction function on lists. Of course it is
easy to define, but there are at least two alternatives:definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = filter (λx. x ∉ set ys) xs"definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"One is geared towards sets, the othe one towards multisets. (Larry
remarked that the latter turns lists into a monus = monoid with minus,
but we don't use the class system on lists).Any comments? Should we have both of them? Names? Notation? Definition
vs abbreviation (definitions require more thms that are for free with
abbrev.)? ...Tobias
Email Gateway (Jun 04 2025 at 19:56):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Am 03.06.25 um 09:57 schrieb Tobias Nipkow:
Larry recently needed a subtraction function on lists. Of course it is
easy to define, but there are at least two alternatives:definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = filter (λx. x ∉ set ys) xs"definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"
Just two further remarks:
In Isabelle/ML, there is a counterpart to minus_list_set names
subtract
https://isabelle.sketis.net/repos/isabelle/file/tip/src/Pure/library.ML#l179
I don’t know the envisaged application, but it can also be defined as
symmetric difference:
definition symmetric_remove1 :: ‹'a ⇒ 'a list ⇒ 'a list›
where ‹symmetric_remove1 x xs =
(if x \<in> set xs then remove1 x xs else x # xs)›
definition symmetric_subtract :: ‹'a list ⇒ 'a list ⇒ 'a list›
where ‹symmetric_subtract = foldr symmetric_remove1›
value ‹symmetric_subtract [2, 3, 4, 3] [1, 2, 3, 2, 1 :: int]›
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jun 06 2025 at 04:56):From: Tobias Nipkow <nipkow@in.tum.de>
Stepan,
Do you have some application of minus_list_list in mind or was it more for
completeness?
Tobias
On 03/06/2025 21:15, Stepan Holub (via cl-isabelle-users Mailing List) wrote:
I like both, although both are ignoring the non-commutative nature of the
subtracted lists and, as Tobias said, they are more about sets (therefore it is
not clear to me immediately in what sense we would get a monus on lists).How about the third one geared towards non-commutativity of lists:
fun minus_list_list :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_list xs [] = xs" |
"minus_list_list [] ys = []" |
"minus_list_list (x # xs) (y # ys) = (if x = y then minus_list_list xs ys else x(minus_list_list xs (y # ys)))"
I believe any of them should be a definition (if introduced), not abbreviation.
Not sure they deserve a special notation, but that would depend on applications.Stepan
On 03-Jun-25 9:57 AM, Tobias Nipkow wrote:
Larry recently needed a subtraction function on lists. Of course it is easy to
define, but there are at least two alternatives:definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = filter (λx. x ∉ set ys) xs"definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"One is geared towards sets, the othe one towards multisets. (Larry remarked
that the latter turns lists into a monus = monoid with minus, but we don't use
the class system on lists).Any comments? Should we have both of them? Names? Notation? Definition vs
abbreviation (definitions require more thms that are for free with abbrev.)? ...Tobias
Email Gateway (Jun 06 2025 at 05:47):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
I have no direct application in mind. My motivation:
it occurred to me as the most natural meaning of "minus on lists"
(/qua /lists)
it is closely related to the ordering "(scattered) subword": x - y
then means "remove the first scattered occurrence of (a prefix of) y from x"
That ordering, needless to say, is important, see for example
https://link.springer.com/chapter/10.1007/978-3-540-85780-8_38
Stepan
On 06-Jun-25 6:55 AM, Tobias Nipkow wrote:
Stepan,
Do you have some application of minus_list_list in mind or was it more
for completeness?Tobias
On 03/06/2025 21:15, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:I like both, although both are ignoring the non-commutative nature of
the subtracted lists and, as Tobias said, they are more about sets
(therefore it is not clear to me immediately in what sense we would
get a monus on lists).How about the third one geared towards non-commutativity of lists:
fun minus_list_list :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_list xs [] = xs" |
"minus_list_list [] ys = []" |
"minus_list_list (x # xs) (y # ys) = (if x = y then minus_list_list
xs ys else x # (minus_list_list xs (y # ys)))"I believe any of them should be a definition (if introduced), not
abbreviation. Not sure they deserve a special notation, but that
would depend on applications.Stepan
On 03-Jun-25 9:57 AM, Tobias Nipkow wrote:
Larry recently needed a subtraction function on lists. Of course it
is easy to define, but there are at least two alternatives:definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = filter (λx. x ∉ set ys) xs"definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"One is geared towards sets, the othe one towards multisets. (Larry
remarked that the latter turns lists into a monus = monoid with
minus, but we don't use the class system on lists).Any comments? Should we have both of them? Names? Notation?
Definition vs abbreviation (definitions require more thms that are
for free with abbrev.)? ...Tobias
Email Gateway (Jun 14 2025 at 13:23):From: Tobias Nipkow <nipkow@in.tum.de>
I have now added
definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"
definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = foldr removeAll ys xs"
(and supporting lemmas) to theory List. I have also located a few theories in
the AFP that defined their own versions of the above and replaced the local
versions. [Fabian's flexible search tool https://search.isabelle.in.tum.de/ was
very helpful here.]
Enjoy.
Tobias
On 03/06/2025 09:57, Tobias Nipkow wrote:
Larry recently needed a subtraction function on lists. Of course it is easy to
define, but there are at least two alternatives:definition minus_list_set :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_set xs ys = filter (λx. x ∉ set ys) xs"definition minus_list_mset :: "'a list ⇒ 'a list ⇒ 'a list" where
"minus_list_mset xs ys = foldr remove1 ys xs"One is geared towards sets, the othe one towards multisets. (Larry remarked that
the latter turns lists into a monus = monoid with minus, but we don't use the
class system on lists).Any comments? Should we have both of them? Names? Notation? Definition vs
abbreviation (definitions require more thms that are for free with abbrev.)? ...Tobias
Last updated: Jun 20 2025 at 12:44 UTC