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



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.