Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Multiset.cases names

Email Gateway (Aug 19 2022 at 13:57):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

I was wondering about the case-names of multiset_cases in Multiset.thy:

lemma multiset_cases [cases type, case_names empty add]:
assumes em: "M = {#} ==> P"
assumes add: "!! N x. M = N + {#x#} ==> P"
shows "P"
sorry

lemma "foo = {#}"
proof (cases foo)
print_cases
(* case names 1 and 2 *)
oops

So, the names "add" and "empty" for cases are not used at all.

If however, one would have declared

lemma multiset_cases [cases type, case_names empty add]:
assumes em: "M = {#} ⟹ P"
assumes add: "!! N x. M = N + {#x#} ⟹ P"
shows "P"
sorry

then everything works as expected

lemma "foo = {#}"
proof (cases foo)
print_cases
(* case names empty and add *)
oops

Perhaps this should be changed in a future release.
Kind regards,
René

Email Gateway (Aug 19 2022 at 13:57):

From: Lars Noschinski <noschinl@in.tum.de>
On 03.03.2014 09:43, René Thiemann wrote:

Dear all,

I was wondering about the case-names of multiset_cases in Multiset.thy:

lemma multiset_cases [cases type, case_names empty add]:
assumes em: "M = {#} ==> P"
assumes add: "!! N x. M = N + {#x#} ==> P"
shows "P"
sorry

lemma "foo = {#}"
proof (cases foo)
print_cases
(* case names 1 and 2 *)
oops

So, the names "add" and "empty" for cases are not used at all.

If however, one would have declared

lemma multiset_cases [cases type, case_names empty add]:
assumes em: "M = {#} ⟹ P"
assumes add: "!! N x. M = N + {#x#} ⟹ P"
shows "P"
sorry
I guess you meant [case_names empty add, cases type]?
Perhaps this should be changed in a future release.
Indeed.

Email Gateway (Aug 19 2022 at 13:57):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Ah, indeed, bad copy & paste mistake.

Email Gateway (Aug 19 2022 at 13:58):

From: Makarius <makarius@sketis.net>
Before there are more copy-paste accidents, just note that such
elimination rules can be written in a more structured way:

lemma multiset_cases [cases type]:
obtains (empty) "M = {#}"
| (add) N x where "M = N + {#x#}"

Here the case_names are already included, and the chance for mistakes
reduced. (There is no such form for induction rules, though.)

Further fine-points of ongoing Multiset library changes should probably be
discussed on isabelle-dev. Tobias has already applied some of your
patches, so it has become part of the development process.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC