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



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!

Vadim

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,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva





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