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
I was trying something like that:
consts f :: "bool => nat"
"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
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