[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.