[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.