# HG changeset patch
# User berghofe
# Date 1064239489 -7200
# Node ID 8953b566dfed188613d5d29381d2ae848ff3ee96
# Parent  30e41f63712e09232d287724799b0b30cb683f9c
Improved efficiency of code generated for functions int and nat.

diff -r 30e41f63712e -r 8953b566dfed src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Mon Sep 22 16:02:51 2003 +0200
+++ b/src/HOL/Integ/NatBin.thy	Mon Sep 22 16:04:49 2003 +0200
@@ -78,10 +78,22 @@
 types_code
   "int" ("int")
 
-lemmas [code] = int_0 int_Suc
+constdefs
+  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
+  "int_aux i n == (i + int n)"
+  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
+  "nat_aux n i == (n + nat i)"
 
-lemma [code]: "nat x = (if x <= 0 then 0 else Suc (nat (x - 1)))"
-  by (simp add: Suc_nat_eq_nat_zadd1)
+lemma [code]:
+  "int_aux i 0 = i"
+  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
+  "int n = int_aux 0 n"
+  by (simp add: int_aux_def)+
+
+lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
+  by (simp add: nat_aux_def Suc_nat_eq_nat_zadd1) -- {* tail recursive *}
+lemma [code]: "nat i = nat_aux 0 i"
+  by (simp add: nat_aux_def)
 
 consts_code
   "0" :: "int"                  ("0")