# Re: [isabelle] apply (cases a b c)

```case_product should work with any case-style theorem of the form
R x y ==> (case one over x y ==> P) ==> (case two over x y ==> P) ==>
P
(where R is the inductive predicate. it is optional)

So you can write:

dt.cases[case_product dt.cases]

- Johannes

Am Montag, den 07.07.2014, 18:55 -0700 schrieb Vadim Zaliva:
> Hi!
>
> If there is a way to use case_product attribute for inductive definitions?
> For example if I have "inductive dt ..." it gives me dt.cases but no dt.exhaust.
> Thanks!
>
>
> On Jun 20, 2014, at 06:58 , Johannes Hölzl <hoelzl at in.tum.de> wrote:
>
> > You can use the case_product attribute:
> >
> >  by (cases a b rule: dt.exhaust[case_product dt.exhaust])
> >     simp_all
> >
> > And yes, I think it would be worth to extend the case method.
> >
> > - Johannes
> >
> > Am Freitag, den 20.06.2014, 15:53 +0200 schrieb Timothy Bourke:
> >> Is there a built-in way to generate subgoals for all cases of a set of
> >> variables?
> >>
> >> For instance, suppose I have the definitions:
> >>
> >>  datatype dt = Num int | Infinity
> >>
> >>  fun plus :: "dt ⇒ dt ⇒ dt"
> >>  where
> >>    "plus Infinity _ = Infinity"
> >>  | "plus _ Infinity = Infinity"
> >>  | "plus (Num a) (Num b) = Num (a + b)"
> >>
> >> And now that I want to show:
> >>
> >>  lemma "plus a b = plus b a"
> >>
> >> I would like to be able to type:
> >>    by (cases a b) simp_all
> >>
> >> But this is not supported.
> >>
> >> I know that I can type:
> >>  by (tactic "(List.foldl (op THEN_ALL_NEW) (fn i => all_tac)
> >>                (List.map (Induct_Tacs.case_tac @{context}) ["a", "b"]) 1)")
> >>     simp_all
> >>
> >> But somehow this is not very pleasing!
> >>
> >> So, is there a good way to do this?
> >>
> >> Would it be worth extending the cases method?
> >>
> >> Tim.
> >>
> >
> >
> >
>
> Sincerely,
>
> --
> CMU ECE PhD student
> Mobile: +1(510)220-1060
> Skype: vzaliva
>

```

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