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

```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,