author Cezary Kaliszyk Wed, 20 Jul 2011 16:15:33 +0200 changeset 43935 aa04d1e1e2cc parent 43934 2108763f298d (current diff) parent 43933 6cc1875cf35d (diff) child 43936 127749bbc639 child 43940 26ca0bad226a
merge
```--- a/src/HOL/Library/Extended_Real.thy	Wed Jul 20 16:14:49 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jul 20 16:15:33 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"

+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```
```--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 16:14:49 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 16:15:33 2011 +0200
@@ -554,11 +554,9 @@
ts2
|> eta_expand ctxt1 is_fol funcs
|> rpair ctxt1
-      |>> tap (map (tracing o PolyML.makestring))
|-> Lambda_Lifting.lift_lambdas NONE is_binder
|-> (fn (ts', defs) => fn ctxt' =>
map mk_trigger defs @ ts'
-          |> tap (map (tracing o PolyML.makestring))
|> intro_explicit_application ctxt' funcs
|> pair ctxt')
```