[isabelle] case split on tuples
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] case split on tuples
- From: Christian Sternagel <christian.sternagel at uibk.ac.at>
- Date: Mon, 27 Jun 2011 13:44:36 +0200
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:18.104.22.168) Gecko/20110428 Fedora/3.1.10-1.fc15 Lightning/1.0b2 Thunderbird/3.1.10
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
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and