# HG changeset patch
# User hoelzl
# Date 1311169343 -7200
# Node ID 6cc1875cf35da11b0d8c31e9eea33712475e723e
# Parent  b2218b8265ea93fce74b503a334b75dedbf290c4
add code generator setup and tests for ereal

diff -r b2218b8265ea -r 6cc1875cf35d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Jul 20 15:09:53 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jul 20 15:42:23 2011 +0200
@@ -75,6 +75,15 @@
     and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
   by (simp_all add: infinity_ereal_def)
 
+declare
+  PInfty_eq_infinity[code_post]
+  MInfty_eq_minfinity[code_post]
+
+lemma [code_unfold]:
+  "\<infinity> = PInfty"
+  "-PInfty = MInfty"
+  by simp_all
+
 lemma inj_ereal[simp]: "inj_on ereal A"
   unfolding inj_on_def by auto
 
@@ -2540,4 +2549,14 @@
   "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
   by (metis sup_ereal_def sup_least)
 
+subsubsection {* Tests for code generator *}
+
+(* A small list of simple arithmetic expressions *)
+
+value [code] "- \<infinity> :: ereal"
+value [code] "\<bar>-\<infinity>\<bar> :: ereal"
+value [code] "4 + 5 / 4 - ereal 2 :: ereal"
+value [code] "ereal 3 < \<infinity>"
+value [code] "real (\<infinity>::ereal) = 0"
+
 end