Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] case split on tuples


view this post on Zulip Email Gateway (Aug 18 2022 at 17:50):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,

recently I noticed that when using cases on right-nested tuples in Isar,
I obtain just a single case (by the name "fields"), which is very
convenient. E.g.,

lemma "EX a b c d. (z :: 'a * 'b * 'c * 'd) = (a, b, c, d)"
proof (cases z)
case (fields a b c d)
thus ?thesis by simp
qed

I started to rely on this behavior and used an ever deeper nesting of
tuples... until (starting with 8 components) it didn't work any longer.
What is the reason that at most 7 components are split?

cheers

chris

view this post on Zulip Email Gateway (Aug 18 2022 at 17:50):

From: Makarius <makarius@sketis.net>
The setup in src/HOL/Product_Type.thy assumes that tuples have max. 7
fields, see prod_cases7 etc. When I introduced that any years ago, the
reasoning was that with many fields it is better to use records anyway.

The scala library has similar treatment for tuples of "reasonable size",
where they define it as <= 22 fields.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 17:50):

From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Chris,

if you look at ~~/src/HOL/Product_Type.thy you will find the rule:

lemma prod_cases7 [cases type]:
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
by (cases y, case_tac f) blast

Which adds the case rule for a 7-tuple. So by adding:

lemma prod_cases8 [cases type]:
obtains (fields) a b c d e f g h where "y = (a, b, c, d, e, f, g, h)"
by (cases y, case_tac f) blast

lemma prod_induct8 [case_names fields, induct type]:
"(!!a b c d e f g h. P (a, b, c, d, e, f, g, h)) ==> P x"
by (cases x) blast

you can extend this behaviour for a 8-tuple.


Last updated: Nov 21 2024 at 12:39 UTC