# [isabelle] nat_code Equation

Dear all,
I recently had to check some very large proof using the code that was generated by Isabelle.
Unfortunately we have not been able to parse the proof within reasonable time.
Therefore, we started to profile our parser (which is written as an Isabelle function)
and we stumbled upon a strange hotspot: nat!
In Code_Integer we have the following code-equation:
lemma nat_code [code]:
"nat k = (if k ≤ 0 then 0 else
let
(l, j) = divmod_int k 2;
n = nat l;
l' = n + n
in if j = 0 then l' else Suc l')"
proof -
have "2 = nat 2" by simp
show ?thesis
apply (subst mult_2 [symmetric])
apply (auto simp add: Let_def divmod_int_mod_div not_le
nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
apply (unfold `2 = nat 2`)
apply (subst nat_mod_distrib [symmetric])
apply simp_all
done
qed
Is there any reason why this is so complex? I would imagine a much simpler equation where
the proof is also simple.
lemma [code]: "nat k = (if k ≤ 0 then 0 else Suc (nat (k - 1)))"
proof (cases k)
case (nonneg n)
show ?thesis unfolding nonneg
by (induct n, auto)
qed simp
Best regards,
René
--
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck

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