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)
  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)

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.