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



Hm, do you need case distinction over X at all?

Why not:
 
 proof (cases a b rule: type.exhaust[case_product type.exhaust])

Where type is the name of your type.

But maybe I didn't understand your goal. But for this I need more
information, for example the definition of your predicate X and type
"type" and the theorem you want to proof. You can also attach your
theory development if you want.

 - Johannes

Am Dienstag, den 08.07.2014, 11:02 -0700 schrieb Vadim Zaliva:
> 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!
> 
> Vadim
> 
> 
> 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!
> >> 
> >> 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
> >> 
> > 
> > 
> 
> Sincerely,
> Vadim Zaliva
> 
> 






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