# Re: [isabelle] reusable proofs

```Alternatively, we can prove some general lemmas:

lemma even_or_odd:"even n ∨ odd n"
apply (induct n rule:nat_less_induct)
by (metis evenSS less_Suc_eq oddSS)

lemma is_number: "is_number n" by (metis e even_or_odd o)

Then, we can have

lemma "is_number (Suc (Suc (Suc (Suc 0))))" by (rule is_number)

Wenda

On 2014-11-04 21:15, Lawrence Paulson wrote:
```
```Try one of these:

by (simp add: is_number.intros odd.intros even.intros)
by (metis is_number.intros odd.intros even.intros)
by (blast intro: is_number.intros intro!: odd.intros even.intros)

They all work with, e.g.,

lemma "is_number (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc 0))))))))))))))))))))))))))))))))))))))))))))))))))))))"

Larry Paulson

```
On 4 Nov 2014, at 20:03, Amarin Phaosawasdi <phaosaw2 at illinois.edu> wrote:
```
```
Are there any other proof techniques other than using code_pred such that the proofs are more "reusable"?
```
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

```

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