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



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!
> 
> 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.