Re: [isabelle] case split on tuples



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.

 - Johannes


Am Montag, den 27.06.2011, 13:44 +0200 schrieb Christian Sternagel:
> 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.