*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] apply (cases a b c)*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 08 Jul 2014 20:22:00 +0200*In-reply-to*: <711F258F-2E61-48A9-8D71-36CBEE32B8D8@cmu.edu>*Organization*: TU München*References*: <20140620135300.GA30547@tbrk.org> <1403272691.31583.4.camel@lapnipkow5> <07E66DDE-6505-4759-BF67-1F157C187834@cmu.edu> <1404808089.3675.2.camel@lapnipkow5> <711F258F-2E61-48A9-8D71-36CBEE32B8D8@cmu.edu>

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

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

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

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

- Previous by Date: Re: [isabelle] apply (cases a b c)
- Next by Date: Re: [isabelle] Isabelle2014-RC0 available for testing
- Previous by Thread: Re: [isabelle] apply (cases a b c)
- Next by Thread: [isabelle] Isabelle2014-RC0: symbol completion in antiquotations
- 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