# HG changeset patch
# User wenzelm
# Date 1333823701 -7200
# Node ID 84d8952b5bd97f916c89d3511ca49f0184225e39
# Parent  b7625245a846d3299169faf7f996b7d298ea6258# Parent  8a5a1d26337fbca0a21ae78d1fc030c89d1fb580
merged

diff -r 8a5a1d26337f -r 84d8952b5bd9 src/HOL/Library/Target_Numeral.thy
--- a/src/HOL/Library/Target_Numeral.thy	Sat Apr 07 20:10:13 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy	Sat Apr 07 20:35:01 2012 +0200
@@ -163,6 +163,10 @@
   "int_of (max k l) = max (int_of k) (int_of l)"
   by (simp add: max_def less_eq_int_def)
 
+lemma of_nat_nat_of [simp]:
+  "of_nat (nat_of k) = max 0 k"
+  by (simp add: nat_of_def Target_Numeral.int_eq_iff less_eq_int_def max_def)
+
 
 subsection {* Code theorems for target language numerals *}
 
@@ -620,18 +624,25 @@
 
 subsection {* Implementation for @{typ nat} *}
 
+definition Nat :: "Target_Numeral.int \<Rightarrow> nat" where
+  "Nat = Target_Numeral.nat_of"
+
 definition of_nat :: "nat \<Rightarrow> Target_Numeral.int" where
   [code_abbrev]: "of_nat = Nat.of_nat"
 
-hide_const (open) of_nat
+hide_const (open) of_nat Nat
 
 lemma int_of_nat [simp]:
   "Target_Numeral.int_of (Target_Numeral.of_nat n) = of_nat n"
   by (simp add: of_nat_def)
 
 lemma [code abstype]:
-  "Target_Numeral.nat_of (Target_Numeral.of_nat n) = n"
-  by (simp add: nat_of_def)
+  "Target_Numeral.Nat (Target_Numeral.of_nat n) = n"
+  by (simp add: Nat_def nat_of_def)
+
+lemma [code abstract]:
+  "Target_Numeral.of_nat (Target_Numeral.nat_of k) = max 0 k"
+  by (simp add: of_nat_def)
 
 lemma [code_abbrev]:
   "nat (Int.Pos k) = nat_of_num k"
@@ -724,3 +735,4 @@
   by (simp add: of_nat_def of_int_of_nat max_def)
 
 end
+