correct code equation for term_of on integer
authorAndreas Lochbihler
Mon, 25 Aug 2014 09:08:45 +0200
changeset 58038 f8e6197668c9
parent 58037 f7be22c6646b
child 58039 469a375212c1
correct code equation for term_of on integer
src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Mon Aug 25 08:45:32 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Aug 25 09:08:45 2014 +0200
@@ -131,10 +131,14 @@
 declare [[code drop: "term_of :: integer \<Rightarrow> _"]]
 
 lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]:
-  "Code_Evaluation.term_of (i :: integer) =
-   Code_Evaluation.App
-    (Code_Evaluation.Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer)))
-    (term_of (num_of_integer i))"
+  "term_of (i :: integer) =
+  (if i > 0 then 
+     App (Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer)))
+      (term_of (num_of_integer i))
+   else if i = 0 then Const (STR ''Groups.zero_class.zero'') TYPEREP(integer)
+   else
+     App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer))
+       (term_of (- i)))"
 by(rule term_of_anything[THEN meta_eq_to_obj_eq])
 
 code_reserved Eval HOLogic