src/HOL/Rat.thy
 changeset 52146 ceb31e1ded30 parent 51956 a4d81cdebf8b child 53012 cb82606b8215 child 53015 a1119cf551e8
equal 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] =`