src/HOL/Rat.thy
changeset 52146 ceb31e1ded30
parent 51956 a4d81cdebf8b
child 53012 cb82606b8215
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Rat.thy	Sat May 25 17:08:43 2013 +0200
     1.2 +++ b/src/HOL/Rat.thy	Sat May 25 17:13:34 2013 +0200
     1.3 @@ -341,7 +341,7 @@
     1.4  proof -
     1.5    have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
     1.6      by (rule sym) (auto intro: normalize_eq)
     1.7 -  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) 
     1.8 +  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos)
     1.9      by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
    1.10    moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
    1.11      by (rule normalize_coprime) simp
    1.12 @@ -1106,16 +1106,42 @@
    1.13    ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
    1.14    uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
    1.15  
    1.16 -subsection{* Float syntax *}
    1.17 +
    1.18 +subsection {* Float syntax *}
    1.19  
    1.20  syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
    1.21  
    1.22 -ML_file "Tools/float_syntax.ML"
    1.23 -setup Float_Syntax.setup
    1.24 +parse_translation {*
    1.25 +  let
    1.26 +    fun mk_number i =
    1.27 +      let
    1.28 +        fun mk 1 = Syntax.const @{const_syntax Num.One}
    1.29 +          | mk i =
    1.30 +              let val (q, r) = Integer.div_mod i 2
    1.31 +              in HOLogic.mk_bit r $ (mk q) end;
    1.32 +      in
    1.33 +        if i = 0 then Syntax.const @{const_syntax Groups.zero}
    1.34 +        else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
    1.35 +        else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
    1.36 +      end;
    1.37 +
    1.38 +    fun mk_frac str =
    1.39 +      let
    1.40 +        val {mant = i, exp = n} = Lexicon.read_float str;
    1.41 +        val exp = Syntax.const @{const_syntax Power.power};
    1.42 +        val ten = mk_number 10;
    1.43 +        val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
    1.44 +      in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
    1.45 +
    1.46 +    fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
    1.47 +      | float_tr [t as Const (str, _)] = mk_frac str
    1.48 +      | float_tr ts = raise TERM ("float_tr", ts);
    1.49 +  in [(@{syntax_const "_Float"}, K float_tr)] end
    1.50 +*}
    1.51  
    1.52  text{* Test: *}
    1.53  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
    1.54 -by simp
    1.55 +  by simp
    1.56  
    1.57  
    1.58  hide_const (open) normalize positive