author haftmann Tue Sep 18 07:36:13 2007 +0200 (2007-09-18) changeset 24622 8116eb022282 parent 24621 97d403d9ab54 child 24623 7b2bc73405b8
renamed constructor RatC to Rational
```     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")
```