Re: [isabelle] help with recdef definition and induction
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.
It does *not* follow trivially - you have no defn or lemma which tells
you what "sum1 (Suc 0) n" is. You need to prove such lemmas first.
This archive was generated by a fusion of
Pipermail (Mailman edition) and