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")