# HG changeset patch
# User haftmann
# Date 1155017987 -7200
# Node ID 21e7e90939408f83f0b0e1d5225e6490487f6cf6
# Parent  50aaae6ae4db639ad1d4a20cd08480c19d53c7ab
improvements for 2nd codegenerator

diff -r 50aaae6ae4db -r 21e7e9093940 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Tue Aug 08 08:19:44 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Tue Aug 08 08:19:47 2006 +0200
@@ -51,39 +51,44 @@
 *}
   int ("(_)")
 
+definition
+  "nat_plus m n = nat (int m + int n)"
+  "nat_minus m n = nat (int m - int n)"
+  "nat_mult m n = nat (int m * int n)"
+  "nat_div m n = nat (fst (divAlg (int m, int n)))"
+  "nat_mod m n = nat (snd (divAlg (int m, int n)))"
+  "nat_less m n = (int m < int n)"
+  "nat_less_equal m n = (int m <= int n)"
+  "nat_eq m n = (int m = int n)"
+
 code_typapp nat
   ml (target_atom "IntInf.int")
   haskell (target_atom "Integer")
 
-definition
-  "nat_of_int (k::int) = (if k < 0 then - k else k)"
-
-lemma
-  "nat_of_int = abs"
-by (simp add: expand_fun_eq nat_of_int_def zabs_def)
-
-code_generate (ml, haskell) "abs :: int \<Rightarrow> int"
-
 code_constapp
+  "0::nat" (* all constructors of nat must be hidden *)
+    ml (target_atom "(0 :: IntInf.int)")
+    haskell (target_atom "0")
+  Suc (* all constructors of nat must be hidden *)
+    ml ("IntInf.+ (_, 1)")
+    haskell ("(+) 1 _")
   nat
-    ml ("{* abs :: int \<Rightarrow> int *}")
-    haskell ("{* abs :: int \<Rightarrow> int *}")
+    ml (target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)")
+    haskell (target_atom "(\\n :: Int -> if n < 0 then 0 else n)")
   int
     ml ("_")
     haskell ("_")
 
 text {*
-  Eliminate @{const "0::nat"} and @{const "Suc"}
+  Eliminate @{const "0::nat"} and @{const "1::nat"}
   by unfolding in place.
 *}
 
 lemma [code inline]:
   "0 = nat 0"
-  "Suc = (op +) 1"
+  "1 = nat 1"
 by (simp_all add: expand_fun_eq)
 
-declare elim_one_nat [code nofold]
-
 text {*
 Case analysis on natural numbers is rephrased using a conditional
 expression:
@@ -112,9 +117,27 @@
   by (simp add: zmod_int [symmetric])
 lemma [code]: "(m < n) = (int m < int n)"
   by simp
+
+lemma [code fun, code inline]: "m + n = nat_plus m n"
+  unfolding nat_plus_def by arith
+lemma [code fun, code inline]: "m - n = nat_minus m n"
+  unfolding nat_minus_def by arith
+lemma [code fun, code inline]: "m * n = nat_mult m n"
+  unfolding nat_mult_def by (simp add: zmult_int)
+lemma [code fun, code inline]: "m div n = nat_div m n"
+  unfolding nat_div_def div_def [symmetric] zdiv_int [symmetric] by simp
+lemma [code fun, code inline]: "m mod n = nat_mod m n"
+  unfolding nat_mod_def mod_def [symmetric] zmod_int [symmetric] by simp
+lemma [code fun, code inline]: "(m < n) = nat_less m n"
+  unfolding nat_less_def by simp
+lemma [code fun, code inline]: "(m <= n) = nat_less_equal m n"
+  unfolding nat_less_equal_def by simp
+lemma [code fun, code inline]: "(m = n) = nat_eq m n"
+  unfolding nat_eq_def by simp
 lemma [code fun]:
-  "(m = n) = (int m = int n)"
-  by simp
+  "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))"
+  unfolding nat_eq_def nat_minus_def int_aux_def by simp
+
 
 subsection {* Preprocessors *}