[isabelle] case split on tuples



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.