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



You can also use the custom induct or cases rules provided by the "fun" command.

lemma "plus a b = plus b a"
apply (cases "(a, b)" rule: plus.cases)

or

lemma "plus a b = plus b a"
apply (induct a b rule: plus.induct)

These give you one case corresponding to each equation in plus.simps,
which may be a different set of cases than you would get with the
case_product rule.

- Brian


On Fri, Jun 20, 2014 at 6:58 AM, 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.
>>
>
>
>




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