[isabelle] help with recdef definition and induction
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.
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)
Consider the following function:
consts sum1 :: '[nat,nat] => nat"
"sum1 m 0 = m"
"sum1 m (Suc n) = sum1 (Suc m) n"
Then I try to prove:
lemma 1: "sum 0 n = n"
apply (induct_tac n, auto)
!!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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and