*To*: Lucas Cavalcante <thesupervisar at gmail.com>*Subject*: Re: [isabelle] help with recdef definition and induction*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Fri, 17 Aug 2007 10:52:49 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <b4d8f2180708161045p4195014ay11a9a2b99159ba6e@mail.gmail.com>*Organization*: Technische Universität München*References*: <b4d8f2180708161045p4195014ay11a9a2b99159ba6e@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.13) Gecko/20060417

Lucas Cavalcante wrote:

Once I need to apply induction in a variable with 'bool' datatype I need to 'measure' this variable when using recdef. Is there a way how to make it by using primrec, or i will need recdef? If recdef is needed, i will need 'measure'. Thus I need the function to define itself. I was trying something like that: consts f :: "bool => nat" primrec "f (~P) = 1 + f P" "f (P->Q) = 1 + f P + f Q" ... (the other conectives, like &, | and <->) "f P = 0" But it says there is a constructor missing. (Then I began to use recdef)

It seems that you are confusing the datatype "bool" with the datatype of boolean formulae. Note that for example the term "(~ True) --> False" of type "bool" is equivalent to the term "True", but the above function would map the former term to 2 and the latter to 0. Therefore, such a function cannot exist. While the datatype "bool" just consists of the two constructors "True" and "False", the datatype of boolean formulae could be defined as follows: datatype form = TT | FF | Neg form | Impl form form | And form form | Or form form | ... Note that the datatype package already provides a "size" function for this datatype automatically. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

**References**:**[isabelle] help with recdef definition and induction***From:*Lucas Cavalcante

- Previous by Date: Re: [isabelle] help with recdef definition and induction
- Next by Date: [isabelle] Isabelle Slowdown
- Previous by Thread: Re: [isabelle] help with recdef definition and induction
- Next by Thread: [isabelle] Isabelle Slowdown
- Cl-isabelle-users August 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