Re: [isabelle] Questions about Isabelle

I took a quick look at your problem and attach a small theory file, in which I define your collatzNext function and prove a trivial property of it. To undertake the project you describe, you just have to do one step at a time, and your first step should be to read the tutorial:

It will take a while before you can become proficient enough to do a challenging project.
Larry Paulson

theory Collatz
imports Parity

 collatzNext :: "nat \<Rightarrow> nat"
 "collatzNext n = (if even n then (n div 2) else 3*n + 1)"

lemma "0<n \<Longrightarrow> 0 < collatzNext n"
apply (auto simp add: collatzNext_def)
apply (metis Suc_n_div_2_gt_zero lemma_even_div2)

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