# [isabelle] help with recdef definition and induction

```1st.:
Is there some "For-Newbie Forum/Chat" about Isabelle? I think most of my
questions are about how to proceed more than how Isabelle works.
Forgive me for that.

2nd.:
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)

3rd.:
Consider the following function:

consts sum1 :: '[nat,nat] => nat"
primrec
"sum1 m 0 = m"
"sum1 m (Suc n) = sum1 (Suc m) n"

Then I try to prove:

lemma 1: "sum 0 n = n"

by
apply (induct_tac n, auto)

resulting this:

!!n. sum1  0 n = n ==> sum1 (Suc 0) n = Suc n

but this remaing stage seems trivial by definition of sum1.
Is 'auto' instead other more specific methods a mistake?

Doesn't Isabelle allow the Complete Induction?

Thank You
Lucas

```

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