Re: [isabelle] reusable proofs



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"?





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