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