# [isabelle] reusable proofs

`Suppose I have an inductive definition "is_number n" which specifies
``whether n is a number. If n is even, then n is a number. If n is odd,
``then n is a number. "even n" and "odd n" are also inductive definitions.
`
theory MyNumber imports Main begin
inductive even :: "nat ⇒ bool" where
even0: "even 0" |
evenSS: "⟦even n⟧ ⟹ even (Suc (Suc n))"
inductive odd :: "nat ⇒ bool" where
odd1: "odd (Suc 0)" |
oddSS: "⟦odd n⟧ ⟹ odd (Suc (Suc n))"
inductive is_number :: "nat ⇒ bool" where
o: "⟦odd n⟧ ⟹ is_number n" |
e: "⟦even n⟧ ⟹ is_number n"
end

`Suppose I wanted to prove that (Suc (Suc (Suc (Suc 0)))) is a number. I
``could do the following.
`
lemma "is_number (Suc (Suc (Suc (Suc 0))))"
apply (rule e)
apply (rule evenSS)+
apply (rule even0)
done

`The problem is that this proof is not "reusable" in the MyNumber theory.
``If will fail if I try to prove whether 0 or any odd number is a number.
`

`One way to have a proof that can be "reused" (at least in this case) is
``to use code_pred.
`
code_pred is_number .
lemma "is_number (Suc (Suc (Suc (Suc 0))))"
by eval
lemma "is_number 0"
by eval
lemma "is_number (Suc (Suc (Suc 0)))"
by eval

`Are there any other proof techniques other than using code_pred such
``that the proofs are more "reusable"?
`
Thank you,
Amarin

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