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

```Hm, do you need case distinction over X at all?

Why not:

proof (cases a b rule: type.exhaust[case_product type.exhaust])

Where type is the name of your type.

But maybe I didn't understand your goal. But for this I need more
information, for example the definition of your predicate X and type
"type" and the theorem you want to proof. You can also attach your
theory development if you want.

- Johannes

Am Dienstag, den 08.07.2014, 11:02 -0700 schrieb Vadim Zaliva:
> Johannes, thanks for the hint.
>
> I think I have a slightly different situation. I have induction rule in the form:
>
> inductive X :: "type ==> bool"
>   c1 : X ...
> | c2 : X ...
>
> and I need to prove something like this:
>
> X a ==> X b ==> X f(a,b)
>
> I am trying to write ISAR proof individually considering
> all combination of (c1,c2) constructors for 'a' and 'b':
>
> case(a=c1,b=c1)
> case(a=c1,b=c2)
> case(a=c2,b=c1)
> case(a=c2,b=c2)
>
> I was looking for something like this:
>
> proof(cases a b rule: X.cases)
>
> Alternatively perhaps there is a way to nest proof methods applying
>
> proof(cases a rule: X.cases)
>
> and
>
> proof(cases b rule: X.cases)
>
> sequentially?
>
> I am sorry about such naive question, I am new to Isabelle. Thanks!
>
>
>
> On Jul 8, 2014, at 01:28 , Johannes Hölzl <hoelzl at in.tum.de> wrote:
>
> > 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
> >>
> >
> >
>
> Sincerely,