*To*: Carsten Varming <varming at cmu.edu>*Subject*: Re: [isabelle] easy going with trivial cases in inductive proofs*From*: Julien Narboux <Julien.Narboux at inria.fr>*Date*: Tue, 13 Mar 2007 09:11:26 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.LNX.4.64.0703122054070.2787@cvx>*References*: <Pine.LNX.4.64.0703122054070.2787@cvx>*Sender*: Julien Narboux <julien.narboux at gmail.com>*User-agent*: Thunderbird 1.5.0.10 (Macintosh/20070221)

Carsten Varming a écrit :

Hi, I am trying to use the Isar proof language to write nice inductive proofs. Some of my proofs have two or three interesting cases and a ton of trivial cases dealt with by a line for each case, eg: case Lookup thus ?case by auto next case Seq thus ?case by auto next case Update thus ?case by auto next case UpdateA thus ?case by auto next Is there some way to tell Isabelle using Isar that for the yet to be proved cases do: case * thus ?case by auto next It just not fun having to write a line for each trivial case. Carsten

Hi,

case Foo thus ?case by .... qed (auto) (* Lookup Seq Update UpdateA are solved by auto *) Best wishes, Julien

**References**:**[isabelle] easy going with trivial cases in inductive proofs***From:*Carsten Varming

- Previous by Date: [isabelle] easy going with trivial cases in inductive proofs
- Next by Date: Re: [isabelle] easy going with trivial cases in inductive proofs
- Previous by Thread: [isabelle] easy going with trivial cases in inductive proofs
- Next by Thread: Re: [isabelle] easy going with trivial cases in inductive proofs
- Cl-isabelle-users March 2007 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