renamed constructor RatC to Rational
authorhaftmann
Tue Sep 18 07:36:13 2007 +0200 (2007-09-18)
changeset 246228116eb022282
parent 24621 97d403d9ab54
child 24623 7b2bc73405b8
renamed constructor RatC to Rational
src/HOL/Real/Rational.thy
     1.1 --- a/src/HOL/Real/Rational.thy	Tue Sep 18 07:36:12 2007 +0200
     1.2 +++ b/src/HOL/Real/Rational.thy	Tue Sep 18 07:36:13 2007 +0200
     1.3 @@ -596,27 +596,27 @@
     1.4  subsection {* Implementation of rational numbers as pairs of integers *}
     1.5  
     1.6  definition
     1.7 -  RatC :: "int \<times> int \<Rightarrow> rat"
     1.8 +  Rational :: "int \<times> int \<Rightarrow> rat"
     1.9  where
    1.10 -  "RatC = INum"
    1.11 +  "Rational = INum"
    1.12  
    1.13 -code_datatype RatC
    1.14 +code_datatype Rational
    1.15  
    1.16 -lemma RatC_simp:
    1.17 -  "RatC (k, l) = rat_of_int k / rat_of_int l"
    1.18 -  unfolding RatC_def INum_def by simp
    1.19 +lemma Rational_simp:
    1.20 +  "Rational (k, l) = rat_of_int k / rat_of_int l"
    1.21 +  unfolding Rational_def INum_def by simp
    1.22  
    1.23 -lemma RatC_zero [simp]: "RatC 0\<^sub>N = 0"
    1.24 -  by (simp add: RatC_simp)
    1.25 +lemma Rational_zero [simp]: "Rational 0\<^sub>N = 0"
    1.26 +  by (simp add: Rational_simp)
    1.27  
    1.28 -lemma RatC_lit [simp]: "RatC i\<^sub>N = rat_of_int i"
    1.29 -  by (simp add: RatC_simp)
    1.30 +lemma Rational_lit [simp]: "Rational i\<^sub>N = rat_of_int i"
    1.31 +  by (simp add: Rational_simp)
    1.32  
    1.33  lemma zero_rat_code [code, code unfold]:
    1.34 -  "0 = RatC 0\<^sub>N" by simp
    1.35 +  "0 = Rational 0\<^sub>N" by simp
    1.36  
    1.37  lemma zero_rat_code [code, code unfold]:
    1.38 -  "1 = RatC 1\<^sub>N" by simp
    1.39 +  "1 = Rational 1\<^sub>N" by simp
    1.40  
    1.41  lemma [code, code unfold]:
    1.42    "number_of k = rat_of_int (number_of k)"
    1.43 @@ -630,63 +630,64 @@
    1.44    unfolding Fract'_def ..
    1.45  
    1.46  lemma [code]:
    1.47 -  "Fract' True k l = (if l \<noteq> 0 then RatC (k, l) else Fract 1 0)"
    1.48 -  by (simp add: Fract'_def RatC_simp Fract_of_int_quotient [of k l])
    1.49 +  "Fract' True k l = (if l \<noteq> 0 then Rational (k, l) else Fract 1 0)"
    1.50 +  by (simp add: Fract'_def Rational_simp Fract_of_int_quotient [of k l])
    1.51  
    1.52  lemma [code]:
    1.53 -  "of_rat (RatC (k, l)) = (if l \<noteq> 0 then of_int k / of_int l else 0)"
    1.54 +  "of_rat (Rational (k, l)) = (if l \<noteq> 0 then of_int k / of_int l else 0)"
    1.55    by (cases "l = 0")
    1.56 -    (auto simp add: RatC_simp of_rat_rat [simplified Fract_of_int_quotient [of k l], symmetric])
    1.57 +    (auto simp add: Rational_simp of_rat_rat [simplified Fract_of_int_quotient [of k l], symmetric])
    1.58  
    1.59  instance rat :: eq ..
    1.60  
    1.61 -lemma rat_eq_code [code]: "RatC x = RatC y \<longleftrightarrow> normNum x = normNum y"
    1.62 -  unfolding RatC_def INum_normNum_iff ..
    1.63 +lemma rat_eq_code [code]: "Rational x = Rational y \<longleftrightarrow> normNum x = normNum y"
    1.64 +  unfolding Rational_def INum_normNum_iff ..
    1.65  
    1.66 -lemma rat_less_eq_code [code]: "RatC x \<le> RatC y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
    1.67 +lemma rat_less_eq_code [code]: "Rational x \<le> Rational y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
    1.68  proof -
    1.69 -  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> RatC (normNum x) \<le> RatC (normNum y)" 
    1.70 -    by (simp add: RatC_def del: normNum)
    1.71 -  also have "\<dots> = (RatC x \<le> RatC y)" by (simp add: RatC_def)
    1.72 +  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Rational (normNum x) \<le> Rational (normNum y)" 
    1.73 +    by (simp add: Rational_def del: normNum)
    1.74 +  also have "\<dots> = (Rational x \<le> Rational y)" by (simp add: Rational_def)
    1.75    finally show ?thesis by simp
    1.76  qed
    1.77  
    1.78 -lemma rat_less_code [code]: "RatC x < RatC y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
    1.79 +lemma rat_less_code [code]: "Rational x < Rational y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
    1.80  proof -
    1.81 -  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> RatC (normNum x) < RatC (normNum y)" 
    1.82 -    by (simp add: RatC_def del: normNum)
    1.83 -  also have "\<dots> = (RatC x < RatC y)" by (simp add: RatC_def)
    1.84 +  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Rational (normNum x) < Rational (normNum y)" 
    1.85 +    by (simp add: Rational_def del: normNum)
    1.86 +  also have "\<dots> = (Rational x < Rational y)" by (simp add: Rational_def)
    1.87    finally show ?thesis by simp
    1.88  qed
    1.89  
    1.90 -lemma rat_add_code [code]: "RatC x + RatC y = RatC (x +\<^sub>N y)"
    1.91 -  unfolding RatC_def by simp
    1.92 +lemma rat_add_code [code]: "Rational x + Rational y = Rational (x +\<^sub>N y)"
    1.93 +  unfolding Rational_def by simp
    1.94  
    1.95 -lemma rat_mul_code [code]: "RatC x * RatC y = RatC (x *\<^sub>N y)"
    1.96 -  unfolding RatC_def by simp
    1.97 +lemma rat_mul_code [code]: "Rational x * Rational y = Rational (x *\<^sub>N y)"
    1.98 +  unfolding Rational_def by simp
    1.99  
   1.100 -lemma rat_neg_code [code]: "- RatC x = RatC (~\<^sub>N x)"
   1.101 -  unfolding RatC_def by simp
   1.102 +lemma rat_neg_code [code]: "- Rational x = Rational (~\<^sub>N x)"
   1.103 +  unfolding Rational_def by simp
   1.104  
   1.105 -lemma rat_sub_code [code]: "RatC x - RatC y = RatC (x -\<^sub>N y)"
   1.106 -  unfolding RatC_def by simp
   1.107 +lemma rat_sub_code [code]: "Rational x - Rational y = Rational (x -\<^sub>N y)"
   1.108 +  unfolding Rational_def by simp
   1.109  
   1.110 -lemma rat_inv_code [code]: "inverse (RatC x) = RatC (Ninv x)"
   1.111 -  unfolding RatC_def Ninv divide_rat_def by simp
   1.112 +lemma rat_inv_code [code]: "inverse (Rational x) = Rational (Ninv x)"
   1.113 +  unfolding Rational_def Ninv divide_rat_def by simp
   1.114  
   1.115 -lemma rat_div_code [code]: "RatC x / RatC y = RatC (x \<div>\<^sub>N y)"
   1.116 -  unfolding RatC_def by simp
   1.117 +lemma rat_div_code [code]: "Rational x / Rational y = Rational (x \<div>\<^sub>N y)"
   1.118 +  unfolding Rational_def by simp
   1.119  
   1.120 -text {* Setup for old code generator *}
   1.121 +text {* Setup for SML code generator *}
   1.122  
   1.123  types_code
   1.124    rat ("(int */ int)")
   1.125  attach (term_of) {*
   1.126  fun term_of_rat (p, q) =
   1.127 -  let val rT = Type ("Rational.rat", [])
   1.128 +  let
   1.129 +    val rT = @{typ rat}
   1.130    in
   1.131      if q = 1 orelse p = 0 then HOLogic.mk_number rT p
   1.132 -    else Const ("HOL.inverse_class.divide", [rT, rT] ---> rT) $
   1.133 +    else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $
   1.134        HOLogic.mk_number rT p $ HOLogic.mk_number rT q
   1.135    end;
   1.136  *}
   1.137 @@ -705,7 +706,7 @@
   1.138  *}
   1.139  
   1.140  consts_code
   1.141 -  RatC ("(_)")
   1.142 +  Rational ("(_)")
   1.143  
   1.144  consts_code
   1.145    "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")