# HG changeset patch
# User haftmann
# Date 1291304355 -3600
# Node ID 3c45d6753fd0e031255ab3906ba2a0ba9fa317a7
# Parent  7046acb44f7a41fc8b042947ca6f722406ba8215# Parent  da4bdafeef7c5cd98e53eef44c5733529bc47a07
merged

diff -r 7046acb44f7a -r 3c45d6753fd0 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Dec 02 16:17:01 2010 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Dec 02 16:39:15 2010 +0100
@@ -138,28 +138,37 @@
 
 subsubsection {* Numeric types *}
 
-definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
-  "term_of_num two = (\<lambda>_. dummy_term)"
+definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where
+  "term_of_num_semiring two = (\<lambda>_. dummy_term)"
 
-lemma (in term_syntax) term_of_num_code [code]:
-  "term_of_num two k = (if k = 0 then termify Int.Pls
+lemma (in term_syntax) term_of_num_semiring_code [code]:
+  "term_of_num_semiring two k = (if k = 0 then termify Int.Pls
     else (if k mod two = 0
-      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
-      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
-  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
+      then termify Int.Bit0 <\<cdot>> term_of_num_semiring two (k div two)
+      else termify Int.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))"
+  by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def Let_def)
 
 lemma (in term_syntax) term_of_nat_code [code]:
-  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
+  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n"
+  by (simp only: term_of_anything)
+
+lemma (in term_syntax) term_of_code_numeral_code [code]:
+  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num_semiring (2::code_numeral) k"
   by (simp only: term_of_anything)
 
+definition term_of_num_ring :: "'a\<Colon>ring_div \<Rightarrow> 'a \<Rightarrow> term" where
+  "term_of_num_ring two = (\<lambda>_. dummy_term)"
+
+lemma (in term_syntax) term_of_num_ring_code [code]:
+  "term_of_num_ring two k = (if k = 0 then termify Int.Pls
+    else if k = -1 then termify Int.Min
+    else if k mod two = 0 then termify Int.Bit0 <\<cdot>> term_of_num_ring two (k div two)
+    else termify Int.Bit1 <\<cdot>> term_of_num_ring two (k div two))"
+  by (auto simp add: term_of_anything Const_def App_def term_of_num_ring_def Let_def)
+
 lemma (in term_syntax) term_of_int_code [code]:
   "term_of (k::int) = (if k = 0 then termify (0 :: int)
-    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
-      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_code_numeral_code [code]:
-  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
+    else termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num_ring (2::int) k)"
   by (simp only: term_of_anything)
 
 
@@ -188,6 +197,6 @@
 
 
 hide_const dummy_term valapp
-hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing
+hide_const (open) Const App Abs termify valtermify term_of term_of_num_semiring term_of_num_ring tracing
 
 end
diff -r 7046acb44f7a -r 3c45d6753fd0 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Dec 02 16:17:01 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Dec 02 16:39:15 2010 +0100
@@ -1272,7 +1272,7 @@
 
 values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
 values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
-values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
+values [expected "{-1::int}"] "{b. minus_int_test 4 b 5}"
 
 subsection {* minus on bool *}