1.1 --- a/src/HOL/Real/RealDef.thy	Sat Nov 29 13:39:23 2008 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Sat Nov 29 13:39:45 2008 +0100
     1.3 @@ -998,7 +998,6 @@
     1.4  declare real_diff_def [symmetric, simp]
     1.5  *)
     1.6  
     1.7 -
     1.8  subsubsection{*Density of the Reals*}
     1.9  
    1.10  lemma real_lbound_gt_zero:

     2.1 --- a/src/HOL/Real/RealPow.thy	Sat Nov 29 13:39:23 2008 +0100
     2.2 +++ b/src/HOL/Real/RealPow.thy	Sat Nov 29 13:39:45 2008 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  
     2.5  theory RealPow
     2.6  imports RealDef
     2.7 +uses ("float_syntax.ML")
     2.8  begin
     2.9  
    2.10  declare abs_mult_self [simp]
    2.11 @@ -267,4 +268,15 @@
    2.12  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
    2.13  by (case_tac "n", auto)
    2.14  
    2.15 +subsection{* Float syntax *}
    2.16 +
    2.17 +syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
    2.18 +
    2.19 +use "float_syntax.ML"
    2.20 +setup FloatSyntax.setup
    2.21 +
    2.22 +text{* Test: *}
    2.23 +lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"
    2.24 +by simp
    2.25 +
    2.26  end

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Real/float_syntax.ML	Sat Nov 29 13:39:45 2008 +0100
     3.3 @@ -0,0 +1,47 @@
     3.4 +(*  ID:         $Id$
     3.5 +    Authors:    Tobias Nipkow, TU Muenchen
     3.6 +
     3.7 +Concrete syntax for floats
     3.8 +*)
     3.9 +
    3.10 +signature FLOAT_SYNTAX =
    3.11 +sig
    3.12 +  val setup: theory -> theory
    3.13 +end;
    3.14 +
    3.15 +structure FloatSyntax: FLOAT_SYNTAX =
    3.16 +struct
    3.17 +
    3.18 +(* parse translation *)
    3.19 +
    3.20 +local
    3.21 +
    3.22 +fun mk_number i =
    3.23 +  let
    3.24 +    fun mk 0 = Syntax.const @{const_name Int.Pls}
    3.25 +      | mk ~1 =  Syntax.const @{const_name Int.Min}
    3.26 +      | mk i = let val (q, r) = Integer.div_mod i 2
    3.27 +               in HOLogic.mk_bit r $ (mk q) end;
    3.28 +  in Syntax.const @{const_name Int.number_of} $ mk i end;
    3.29 +
    3.30 +fun mk_frac str =
    3.31 +  let
    3.32 +    val {mant=i, exp = n} = Syntax.read_float str;
    3.33 +    val exp = Syntax.const @{const_name "Power.power"};
    3.34 +    val ten = mk_number 10;
    3.35 +    val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
    3.36 +  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
    3.37 +in
    3.38 +
    3.39 +fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
    3.40 +  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
    3.41 +
    3.42 +end;
    3.43 +
    3.44 +
    3.45 +(* theory setup *)
    3.46 +
    3.47 +val setup =
    3.48 +  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
    3.49 +
    3.50 +end;