Re: [isabelle] reusable proofs

Thank you.


On 11/04/2014 04:32 PM, Wenda Li wrote:
Alternatively, we can prove some general lemmas:

lemma even_or_odd:"even n ∨ odd n"
  apply (induct n rule:nat_less_induct)
  apply (case_tac n,simp add:even0)
  apply (case_tac nat,simp add:odd1)
  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)


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> wrote:

Are there any other proof techniques other than using code_pred such that the proofs are more "reusable"?

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