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