928 |
928 |
929 |
929 |
930 subsection {* Implementation of rational real numbers as pairs of integers *} |
930 subsection {* Implementation of rational real numbers as pairs of integers *} |
931 |
931 |
932 definition |
932 definition |
933 RealC :: "int \<times> int \<Rightarrow> real" |
933 Ratreal :: "int \<times> int \<Rightarrow> real" |
934 where |
934 where |
935 "RealC = INum" |
935 "Ratreal = INum" |
936 |
936 |
937 code_datatype RealC |
937 code_datatype Ratreal |
938 |
938 |
939 lemma RealC_simp: |
939 lemma Ratreal_simp: |
940 "RealC (k, l) = real_of_int k / real_of_int l" |
940 "Ratreal (k, l) = real_of_int k / real_of_int l" |
941 unfolding RealC_def INum_def by simp |
941 unfolding Ratreal_def INum_def by simp |
942 |
942 |
943 lemma RealC_zero [simp]: "RealC 0\<^sub>N = 0" |
943 lemma Ratreal_zero [simp]: "Ratreal 0\<^sub>N = 0" |
944 by (simp add: RealC_simp) |
944 by (simp add: Ratreal_simp) |
945 |
945 |
946 lemma RealC_lit [simp]: "RealC i\<^sub>N = real_of_int i" |
946 lemma Ratreal_lit [simp]: "Ratreal i\<^sub>N = real_of_int i" |
947 by (simp add: RealC_simp) |
947 by (simp add: Ratreal_simp) |
948 |
948 |
949 lemma zero_real_code [code, code unfold]: |
949 lemma zero_real_code [code, code unfold]: |
950 "0 = RealC 0\<^sub>N" by simp |
950 "0 = Ratreal 0\<^sub>N" by simp |
951 |
951 |
952 lemma one_real_code [code, code unfold]: |
952 lemma one_real_code [code, code unfold]: |
953 "1 = RealC 1\<^sub>N" by simp |
953 "1 = Ratreal 1\<^sub>N" by simp |
954 |
954 |
955 instance real :: eq .. |
955 instance real :: eq .. |
956 |
956 |
957 lemma real_eq_code [code]: "RealC x = RealC y \<longleftrightarrow> normNum x = normNum y" |
957 lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y" |
958 unfolding RealC_def INum_normNum_iff .. |
958 unfolding Ratreal_def INum_normNum_iff .. |
959 |
959 |
960 lemma real_less_eq_code [code]: "RealC x \<le> RealC y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y" |
960 lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y" |
961 proof - |
961 proof - |
962 have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> RealC (normNum x) \<le> RealC (normNum y)" |
962 have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) \<le> Ratreal (normNum y)" |
963 by (simp add: RealC_def del: normNum) |
963 by (simp add: Ratreal_def del: normNum) |
964 also have "\<dots> = (RealC x \<le> RealC y)" by (simp add: RealC_def) |
964 also have "\<dots> = (Ratreal x \<le> Ratreal y)" by (simp add: Ratreal_def) |
965 finally show ?thesis by simp |
965 finally show ?thesis by simp |
966 qed |
966 qed |
967 |
967 |
968 lemma real_less_code [code]: "RealC x < RealC y \<longleftrightarrow> normNum x <\<^sub>N normNum y" |
968 lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> normNum x <\<^sub>N normNum y" |
969 proof - |
969 proof - |
970 have "normNum x <\<^sub>N normNum y \<longleftrightarrow> RealC (normNum x) < RealC (normNum y)" |
970 have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) < Ratreal (normNum y)" |
971 by (simp add: RealC_def del: normNum) |
971 by (simp add: Ratreal_def del: normNum) |
972 also have "\<dots> = (RealC x < RealC y)" by (simp add: RealC_def) |
972 also have "\<dots> = (Ratreal x < Ratreal y)" by (simp add: Ratreal_def) |
973 finally show ?thesis by simp |
973 finally show ?thesis by simp |
974 qed |
974 qed |
975 |
975 |
976 lemma real_add_code [code]: "RealC x + RealC y = RealC (x +\<^sub>N y)" |
976 lemma real_add_code [code]: "Ratreal x + Ratreal y = Ratreal (x +\<^sub>N y)" |
977 unfolding RealC_def by simp |
977 unfolding Ratreal_def by simp |
978 |
978 |
979 lemma real_mul_code [code]: "RealC x * RealC y = RealC (x *\<^sub>N y)" |
979 lemma real_mul_code [code]: "Ratreal x * Ratreal y = Ratreal (x *\<^sub>N y)" |
980 unfolding RealC_def by simp |
980 unfolding Ratreal_def by simp |
981 |
981 |
982 lemma real_neg_code [code]: "- RealC x = RealC (~\<^sub>N x)" |
982 lemma real_neg_code [code]: "- Ratreal x = Ratreal (~\<^sub>N x)" |
983 unfolding RealC_def by simp |
983 unfolding Ratreal_def by simp |
984 |
984 |
985 lemma real_sub_code [code]: "RealC x - RealC y = RealC (x -\<^sub>N y)" |
985 lemma real_sub_code [code]: "Ratreal x - Ratreal y = Ratreal (x -\<^sub>N y)" |
986 unfolding RealC_def by simp |
986 unfolding Ratreal_def by simp |
987 |
987 |
988 lemma real_inv_code [code]: "inverse (RealC x) = RealC (Ninv x)" |
988 lemma real_inv_code [code]: "inverse (Ratreal x) = Ratreal (Ninv x)" |
989 unfolding RealC_def Ninv real_divide_def by simp |
989 unfolding Ratreal_def Ninv real_divide_def by simp |
990 |
990 |
991 lemma real_div_code [code]: "RealC x / RealC y = RealC (x \<div>\<^sub>N y)" |
991 lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)" |
992 unfolding RealC_def by simp |
992 unfolding Ratreal_def by simp |
993 |
993 |
994 text {* Setup for old code generator *} |
994 text {* Setup for SML code generator *} |
995 |
995 |
996 types_code |
996 types_code |
997 real ("(int */ int)") |
997 real ("(int */ int)") |
998 attach (term_of) {* |
998 attach (term_of) {* |
999 fun term_of_real (p, q) = |
999 fun term_of_real (p, q) = |
1000 let val rT = HOLogic.realT |
1000 let |
|
1001 val rT = HOLogic.realT |
1001 in |
1002 in |
1002 if q = 1 orelse p = 0 then HOLogic.mk_number rT p |
1003 if q = 1 orelse p = 0 then HOLogic.mk_number rT p |
1003 else Const ("HOL.inverse_class.divide", [rT, rT] ---> rT) $ |
1004 else @{term "op / \<Colon> real \<Rightarrow> real \<Rightarrow> real"} $ |
1004 HOLogic.mk_number rT p $ HOLogic.mk_number rT q |
1005 HOLogic.mk_number rT p $ HOLogic.mk_number rT q |
1005 end; |
1006 end; |
1006 *} |
1007 *} |
1007 attach (test) {* |
1008 attach (test) {* |
1008 fun gen_real i = |
1009 fun gen_real i = |