# 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: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf
It will take a while before you can become proficient enough to do a challenging project.
Larry Paulson
theory Collatz
imports Parity
begin
definition
collatzNext :: "nat \<Rightarrow> nat"
where
"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)
done

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