# HG changeset patch
# User nipkow
# Date 1227962385 -3600
# Node ID 5f568bfc58d71e654eb46edbc0d50a8acd9ae443
# Parent  c999579a5166ba0e715a649a4b11f910b19ea14f
Floats for Real.

diff -r c999579a5166 -r 5f568bfc58d7 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Sat Nov 29 13:39:23 2008 +0100
+++ b/src/HOL/Real/RealDef.thy	Sat Nov 29 13:39:45 2008 +0100
@@ -998,7 +998,6 @@
 declare real_diff_def [symmetric, simp]
 *)
 
-
 subsubsection{*Density of the Reals*}
 
 lemma real_lbound_gt_zero:
diff -r c999579a5166 -r 5f568bfc58d7 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Sat Nov 29 13:39:23 2008 +0100
+++ b/src/HOL/Real/RealPow.thy	Sat Nov 29 13:39:45 2008 +0100
@@ -8,6 +8,7 @@
 
 theory RealPow
 imports RealDef
+uses ("float_syntax.ML")
 begin
 
 declare abs_mult_self [simp]
@@ -267,4 +268,15 @@
 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
 by (case_tac "n", auto)
 
+subsection{* Float syntax *}
+
+syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
+
+use "float_syntax.ML"
+setup FloatSyntax.setup
+
+text{* Test: *}
+lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"
+by simp
+
 end
diff -r c999579a5166 -r 5f568bfc58d7 src/HOL/Real/float_syntax.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/float_syntax.ML	Sat Nov 29 13:39:45 2008 +0100
@@ -0,0 +1,47 @@
+(*  ID:         $Id$
+    Authors:    Tobias Nipkow, TU Muenchen
+
+Concrete syntax for floats
+*)
+
+signature FLOAT_SYNTAX =
+sig
+  val setup: theory -> theory
+end;
+
+structure FloatSyntax: FLOAT_SYNTAX =
+struct
+
+(* parse translation *)
+
+local
+
+fun mk_number i =
+  let
+    fun mk 0 = Syntax.const @{const_name Int.Pls}
+      | mk ~1 =  Syntax.const @{const_name Int.Min}
+      | mk i = let val (q, r) = Integer.div_mod i 2
+               in HOLogic.mk_bit r $ (mk q) end;
+  in Syntax.const @{const_name Int.number_of} $ mk i end;
+
+fun mk_frac str =
+  let
+    val {mant=i, exp = n} = Syntax.read_float str;
+    val exp = Syntax.const @{const_name "Power.power"};
+    val ten = mk_number 10;
+    val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
+  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
+in
+
+fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
+  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
+
+end;