[isabelle] nat_code Equation
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
(l, j) = divmod_int k 2;
n = nat l;
l' = n + n
in if j = 0 then l' else Suc l')"
have "2 = nat 2" by simp
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])
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)
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