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.