Re: [isabelle] help with recdef definition and induction



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





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