src/HOL/Rat.thy
changeset 52146 ceb31e1ded30
parent 51956 a4d81cdebf8b
child 53012 cb82606b8215
child 53015 a1119cf551e8
equal deleted inserted replaced
52145:28963df2dffb 52146:ceb31e1ded30
   339 lemma quotient_of_Fract [code]:
   339 lemma quotient_of_Fract [code]:
   340   "quotient_of (Fract a b) = normalize (a, b)"
   340   "quotient_of (Fract a b) = normalize (a, b)"
   341 proof -
   341 proof -
   342   have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
   342   have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
   343     by (rule sym) (auto intro: normalize_eq)
   343     by (rule sym) (auto intro: normalize_eq)
   344   moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) 
   344   moreover have "0 < snd (normalize (a, b))" (is ?denom_pos)
   345     by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
   345     by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
   346   moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
   346   moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
   347     by (rule normalize_coprime) simp
   347     by (rule normalize_coprime) simp
   348   ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast
   348   ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast
   349   with quotient_of_unique have
   349   with quotient_of_unique have
  1104 lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
  1104 lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
  1105   one_rat_inst.one_rat ord_rat_inst.less_rat
  1105   one_rat_inst.one_rat ord_rat_inst.less_rat
  1106   ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
  1106   ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
  1107   uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
  1107   uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
  1108 
  1108 
  1109 subsection{* Float syntax *}
  1109 
       
  1110 subsection {* Float syntax *}
  1110 
  1111 
  1111 syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
  1112 syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
  1112 
  1113 
  1113 ML_file "Tools/float_syntax.ML"
  1114 parse_translation {*
  1114 setup Float_Syntax.setup
  1115   let
       
  1116     fun mk_number i =
       
  1117       let
       
  1118         fun mk 1 = Syntax.const @{const_syntax Num.One}
       
  1119           | mk i =
       
  1120               let val (q, r) = Integer.div_mod i 2
       
  1121               in HOLogic.mk_bit r $ (mk q) end;
       
  1122       in
       
  1123         if i = 0 then Syntax.const @{const_syntax Groups.zero}
       
  1124         else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
       
  1125         else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
       
  1126       end;
       
  1127 
       
  1128     fun mk_frac str =
       
  1129       let
       
  1130         val {mant = i, exp = n} = Lexicon.read_float str;
       
  1131         val exp = Syntax.const @{const_syntax Power.power};
       
  1132         val ten = mk_number 10;
       
  1133         val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
       
  1134       in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
       
  1135 
       
  1136     fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
       
  1137       | float_tr [t as Const (str, _)] = mk_frac str
       
  1138       | float_tr ts = raise TERM ("float_tr", ts);
       
  1139   in [(@{syntax_const "_Float"}, K float_tr)] end
       
  1140 *}
  1115 
  1141 
  1116 text{* Test: *}
  1142 text{* Test: *}
  1117 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
  1143 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
  1118 by simp
  1144   by simp
  1119 
  1145 
  1120 
  1146 
  1121 hide_const (open) normalize positive
  1147 hide_const (open) normalize positive
  1122 
  1148 
  1123 lemmas [transfer_rule del] =
  1149 lemmas [transfer_rule del] =