src/HOL/Rat.thy
 changeset 52146 ceb31e1ded30 parent 51956 a4d81cdebf8b child 53012 cb82606b8215 child 53015 a1119cf551e8
```--- a/src/HOL/Rat.thy	Sat May 25 17:08:43 2013 +0200
+++ b/src/HOL/Rat.thy	Sat May 25 17:13:34 2013 +0200
@@ -341,7 +341,7 @@
proof -
have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
by (rule sym) (auto intro: normalize_eq)
-  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos)
+  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos)
by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
by (rule normalize_coprime) simp
@@ -1106,16 +1106,42 @@
ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat

-subsection{* Float syntax *}
+
+subsection {* Float syntax *}

syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")

-ML_file "Tools/float_syntax.ML"
-setup Float_Syntax.setup
+parse_translation {*
+  let
+    fun mk_number i =
+      let
+        fun mk 1 = Syntax.const @{const_syntax Num.One}
+          | mk i =
+              let val (q, r) = Integer.div_mod i 2
+              in HOLogic.mk_bit r \$ (mk q) end;
+      in
+        if i = 0 then Syntax.const @{const_syntax Groups.zero}
+        else if i > 0 then Syntax.const @{const_syntax Num.numeral} \$ mk i
+        else Syntax.const @{const_syntax Num.neg_numeral} \$ mk (~i)
+      end;
+
+    fun mk_frac str =
+      let
+        val {mant = i, exp = n} = Lexicon.read_float str;
+        val exp = Syntax.const @{const_syntax Power.power};
+        val ten = mk_number 10;
+        val exp10 = if n = 1 then ten else exp \$ ten \$ mk_number n;
+      in Syntax.const @{const_syntax divide} \$ mk_number i \$ exp10 end;
+
+    fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) \$ t \$ u] = c \$ float_tr [t] \$ u
+      | float_tr [t as Const (str, _)] = mk_frac str
+      | float_tr ts = raise TERM ("float_tr", ts);
+  in [(@{syntax_const "_Float"}, K float_tr)] end
+*}

text{* Test: *}
lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
-by simp
+  by simp

hide_const (open) normalize positive```