*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] apply (cases a b c)*From*: Vadim Zaliva <vzaliva at cmu.edu>*Date*: Tue, 8 Jul 2014 11:02:11 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1404808089.3675.2.camel@lapnipkow5>*References*: <20140620135300.GA30547@tbrk.org> <1403272691.31583.4.camel@lapnipkow5> <07E66DDE-6505-4759-BF67-1F157C187834@cmu.edu> <1404808089.3675.2.camel@lapnipkow5>*Sender*: Vadim Zaliva <vadim.zaliva at west.cmu.edu>

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

**Follow-Ups**:**Re: [isabelle] apply (cases a b c)***From:*Johannes Hölzl

**References**:**Re: [isabelle] apply (cases a b c)***From:*Vadim Zaliva

**Re: [isabelle] apply (cases a b c)***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Isabelle2014-RC0 available for testing
- Next by Date: Re: [isabelle] apply (cases a b c)
- Previous by Thread: Re: [isabelle] apply (cases a b c)
- Next by Thread: Re: [isabelle] apply (cases a b c)
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list