src/HOL/Real/RealDef.thy
 changeset 24623 7b2bc73405b8 parent 24534 09b9a47904b7 child 24630 351a308ab58d
```     1.1 --- a/src/HOL/Real/RealDef.thy	Tue Sep 18 07:36:13 2007 +0200
1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Sep 18 07:36:14 2007 +0200
1.3 @@ -930,77 +930,78 @@
1.4  subsection {* Implementation of rational real numbers as pairs of integers *}
1.5
1.6  definition
1.7 -  RealC :: "int \<times> int \<Rightarrow> real"
1.8 +  Ratreal :: "int \<times> int \<Rightarrow> real"
1.9  where
1.10 -  "RealC = INum"
1.11 +  "Ratreal = INum"
1.12
1.13 -code_datatype RealC
1.14 +code_datatype Ratreal
1.15
1.16 -lemma RealC_simp:
1.17 -  "RealC (k, l) = real_of_int k / real_of_int l"
1.18 -  unfolding RealC_def INum_def by simp
1.19 +lemma Ratreal_simp:
1.20 +  "Ratreal (k, l) = real_of_int k / real_of_int l"
1.21 +  unfolding Ratreal_def INum_def by simp
1.22
1.23 -lemma RealC_zero [simp]: "RealC 0\<^sub>N = 0"
1.24 -  by (simp add: RealC_simp)
1.25 +lemma Ratreal_zero [simp]: "Ratreal 0\<^sub>N = 0"
1.26 +  by (simp add: Ratreal_simp)
1.27
1.28 -lemma RealC_lit [simp]: "RealC i\<^sub>N = real_of_int i"
1.29 -  by (simp add: RealC_simp)
1.30 +lemma Ratreal_lit [simp]: "Ratreal i\<^sub>N = real_of_int i"
1.31 +  by (simp add: Ratreal_simp)
1.32
1.33  lemma zero_real_code [code, code unfold]:
1.34 -  "0 = RealC 0\<^sub>N" by simp
1.35 +  "0 = Ratreal 0\<^sub>N" by simp
1.36
1.37  lemma one_real_code [code, code unfold]:
1.38 -  "1 = RealC 1\<^sub>N" by simp
1.39 +  "1 = Ratreal 1\<^sub>N" by simp
1.40
1.41  instance real :: eq ..
1.42
1.43 -lemma real_eq_code [code]: "RealC x = RealC y \<longleftrightarrow> normNum x = normNum y"
1.44 -  unfolding RealC_def INum_normNum_iff ..
1.45 +lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y"
1.46 +  unfolding Ratreal_def INum_normNum_iff ..
1.47
1.48 -lemma real_less_eq_code [code]: "RealC x \<le> RealC y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
1.49 +lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
1.50  proof -
1.51 -  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> RealC (normNum x) \<le> RealC (normNum y)"
1.52 -    by (simp add: RealC_def del: normNum)
1.53 -  also have "\<dots> = (RealC x \<le> RealC y)" by (simp add: RealC_def)
1.54 +  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) \<le> Ratreal (normNum y)"
1.55 +    by (simp add: Ratreal_def del: normNum)
1.56 +  also have "\<dots> = (Ratreal x \<le> Ratreal y)" by (simp add: Ratreal_def)
1.57    finally show ?thesis by simp
1.58  qed
1.59
1.60 -lemma real_less_code [code]: "RealC x < RealC y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
1.61 +lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
1.62  proof -
1.63 -  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> RealC (normNum x) < RealC (normNum y)"
1.64 -    by (simp add: RealC_def del: normNum)
1.65 -  also have "\<dots> = (RealC x < RealC y)" by (simp add: RealC_def)
1.66 +  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Ratreal (normNum x) < Ratreal (normNum y)"
1.67 +    by (simp add: Ratreal_def del: normNum)
1.68 +  also have "\<dots> = (Ratreal x < Ratreal y)" by (simp add: Ratreal_def)
1.69    finally show ?thesis by simp
1.70  qed
1.71
1.72 -lemma real_add_code [code]: "RealC x + RealC y = RealC (x +\<^sub>N y)"
1.73 -  unfolding RealC_def by simp
1.74 +lemma real_add_code [code]: "Ratreal x + Ratreal y = Ratreal (x +\<^sub>N y)"
1.75 +  unfolding Ratreal_def by simp
1.76
1.77 -lemma real_mul_code [code]: "RealC x * RealC y = RealC (x *\<^sub>N y)"
1.78 -  unfolding RealC_def by simp
1.79 +lemma real_mul_code [code]: "Ratreal x * Ratreal y = Ratreal (x *\<^sub>N y)"
1.80 +  unfolding Ratreal_def by simp
1.81
1.82 -lemma real_neg_code [code]: "- RealC x = RealC (~\<^sub>N x)"
1.83 -  unfolding RealC_def by simp
1.84 +lemma real_neg_code [code]: "- Ratreal x = Ratreal (~\<^sub>N x)"
1.85 +  unfolding Ratreal_def by simp
1.86
1.87 -lemma real_sub_code [code]: "RealC x - RealC y = RealC (x -\<^sub>N y)"
1.88 -  unfolding RealC_def by simp
1.89 +lemma real_sub_code [code]: "Ratreal x - Ratreal y = Ratreal (x -\<^sub>N y)"
1.90 +  unfolding Ratreal_def by simp
1.91
1.92 -lemma real_inv_code [code]: "inverse (RealC x) = RealC (Ninv x)"
1.93 -  unfolding RealC_def Ninv real_divide_def by simp
1.94 +lemma real_inv_code [code]: "inverse (Ratreal x) = Ratreal (Ninv x)"
1.95 +  unfolding Ratreal_def Ninv real_divide_def by simp
1.96
1.97 -lemma real_div_code [code]: "RealC x / RealC y = RealC (x \<div>\<^sub>N y)"
1.98 -  unfolding RealC_def by simp
1.99 +lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
1.100 +  unfolding Ratreal_def by simp
1.101
1.102 -text {* Setup for old code generator *}
1.103 +text {* Setup for SML code generator *}
1.104
1.105  types_code
1.106    real ("(int */ int)")
1.107  attach (term_of) {*
1.108  fun term_of_real (p, q) =
1.109 -  let val rT = HOLogic.realT
1.110 +  let
1.111 +    val rT = HOLogic.realT
1.112    in
1.113      if q = 1 orelse p = 0 then HOLogic.mk_number rT p
1.114 -    else Const ("HOL.inverse_class.divide", [rT, rT] ---> rT) \$
1.115 +    else @{term "op / \<Colon> real \<Rightarrow> real \<Rightarrow> real"} \$
1.116        HOLogic.mk_number rT p \$ HOLogic.mk_number rT q
1.117    end;
1.118  *}
1.119 @@ -1019,7 +1020,7 @@
1.120  *}
1.121
1.122  consts_code
1.123 -  RealC ("(_)")
1.124 +  Ratreal ("(_)")
1.125
1.126  consts_code
1.127    "of_int :: int \<Rightarrow> real" ("\<module>real'_of'_int")
```