Email Gateway (Aug 18 2022 at 17:50): 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
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
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: Apr 26 2024 at 01:06 UTC