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