adaptions for code generation
authorhaftmann
Thu Aug 09 15:52:53 2007 +0200 (2007-08-09)
changeset 241984031da6d8ba3
parent 24197 c9e3cb5e5681
child 24199 8be734b5f59f
adaptions for code generation
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Real/Rational.thy	Thu Aug 09 15:52:49 2007 +0200
     1.2 +++ b/src/HOL/Real/Rational.thy	Thu Aug 09 15:52:53 2007 +0200
     1.3 @@ -81,7 +81,11 @@
     1.4  
     1.5  definition
     1.6    Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
     1.7 -  "Fract a b = Abs_Rat (ratrel``{(a,b)})"
     1.8 +  [code func del]: "Fract a b = Abs_Rat (ratrel``{(a,b)})"
     1.9 +
    1.10 +lemma Fract_zero:
    1.11 +  "Fract k 0 = Fract l 0"
    1.12 +  by (simp add: Fract_def ratrel_def)
    1.13  
    1.14  theorem Rat_cases [case_names Fract, cases type: rat]:
    1.15      "(!!a b. q = Fract a b ==> b \<noteq> 0 ==> C) ==> C"
    1.16 @@ -161,9 +165,11 @@
    1.17  
    1.18  instance rat :: zero
    1.19    Zero_rat_def: "0 == Fract 0 1" ..
    1.20 +lemmas [code func del] = Zero_rat_def
    1.21  
    1.22  instance rat :: one
    1.23    One_rat_def: "1 == Fract 1 1" ..
    1.24 +lemmas [code func del] = One_rat_def
    1.25  
    1.26  instance rat :: plus
    1.27    add_rat_def:
    1.28 @@ -176,7 +182,7 @@
    1.29    minus_rat_def:
    1.30      "- q == Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
    1.31    diff_rat_def:  "q - r == q + - (r::rat)" ..
    1.32 -lemmas [code func del] = minus_rat_def
    1.33 +lemmas [code func del] = minus_rat_def diff_rat_def
    1.34  
    1.35  instance rat :: times
    1.36    mult_rat_def:
    1.37 @@ -191,7 +197,7 @@
    1.38          Abs_Rat (\<Union>x \<in> Rep_Rat q.
    1.39              ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})"
    1.40    divide_rat_def:  "q / r == q * inverse (r::rat)" ..
    1.41 -lemmas [code func del] = inverse_rat_def
    1.42 +lemmas [code func del] = inverse_rat_def divide_rat_def
    1.43  
    1.44  instance rat :: ord
    1.45    le_rat_def:
    1.46 @@ -459,6 +465,9 @@
    1.47  lemma Fract_of_int_eq: "Fract k 1 = of_int k"
    1.48  by (rule of_int_rat [symmetric])
    1.49  
    1.50 +lemma Fract_of_int_quotient: "Fract k l = (if l = 0 then Fract 1 0 else of_int k / of_int l)"
    1.51 +by (auto simp add: Fract_zero Fract_of_int_eq [symmetric] divide_rat)
    1.52 +
    1.53  
    1.54  subsection {* Numerals and Arithmetic *}
    1.55  
    1.56 @@ -474,14 +483,14 @@
    1.57  
    1.58  subsection {* Embedding from Rationals to other Fields *}
    1.59  
    1.60 -axclass field_char_0 < field, ring_char_0
    1.61 +class field_char_0 = field + ring_char_0
    1.62  
    1.63  instance ordered_field < field_char_0 ..
    1.64  
    1.65  definition
    1.66    of_rat :: "rat \<Rightarrow> 'a::field_char_0"
    1.67  where
    1.68 -  "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
    1.69 +  [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
    1.70  
    1.71  lemma of_rat_congruent:
    1.72    "(\<lambda>(a, b). {of_int a / of_int b::'a::field_char_0}) respects ratrel"
    1.73 @@ -570,4 +579,14 @@
    1.74  lemmas zero_rat = Zero_rat_def
    1.75  lemmas one_rat = One_rat_def
    1.76  
    1.77 +abbreviation
    1.78 +  rat_of_nat :: "nat \<Rightarrow> rat"
    1.79 +where
    1.80 +  "rat_of_nat \<equiv> of_nat"
    1.81 +
    1.82 +abbreviation
    1.83 +  rat_of_int :: "int \<Rightarrow> rat"
    1.84 +where
    1.85 +  "rat_of_int \<equiv> of_int"
    1.86 +
    1.87  end
     2.1 --- a/src/HOL/Real/RealDef.thy	Thu Aug 09 15:52:49 2007 +0200
     2.2 +++ b/src/HOL/Real/RealDef.thy	Thu Aug 09 15:52:53 2007 +0200
     2.3 @@ -25,39 +25,42 @@
     2.4    real_of_preal :: "preal => real" where
     2.5    "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
     2.6  
     2.7 -consts
     2.8 -   (*overloaded constant for injecting other types into "real"*)
     2.9 -   real :: "'a => real"
    2.10 -
    2.11  instance real :: zero
    2.12    real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
    2.13 +lemmas [code func del] = real_zero_def
    2.14  
    2.15  instance real :: one
    2.16    real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
    2.17 +lemmas [code func del] = real_one_def
    2.18  
    2.19  instance real :: plus
    2.20    real_add_def: "z + w ==
    2.21         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    2.22  		 { Abs_Real(realrel``{(x+u, y+v)}) })" ..
    2.23 +lemmas [code func del] = real_add_def
    2.24  
    2.25  instance real :: minus
    2.26    real_minus_def: "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    2.27    real_diff_def: "r - (s::real) == r + - s" ..
    2.28 +lemmas [code func del] = real_minus_def real_diff_def
    2.29  
    2.30  instance real :: times
    2.31    real_mult_def:
    2.32      "z * w ==
    2.33         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    2.34  		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
    2.35 +lemmas [code func del] = real_mult_def
    2.36  
    2.37  instance real :: inverse
    2.38    real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
    2.39    real_divide_def: "R / (S::real) == R * inverse S" ..
    2.40 +lemmas [code func del] = real_inverse_def real_divide_def
    2.41  
    2.42  instance real :: ord
    2.43    real_le_def: "z \<le> (w::real) == 
    2.44      \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
    2.45    real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
    2.46 +lemmas [code func del] = real_le_def real_less_def
    2.47  
    2.48  instance real :: abs
    2.49    real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
    2.50 @@ -520,23 +523,36 @@
    2.51  by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
    2.52  
    2.53  
    2.54 -subsection{*Embedding the Integers into the Reals*}
    2.55 +subsection {* Embedding numbers into the Reals *}
    2.56 +
    2.57 +abbreviation
    2.58 +  real_of_nat :: "nat \<Rightarrow> real"
    2.59 +where
    2.60 +  "real_of_nat \<equiv> of_nat"
    2.61 +
    2.62 +abbreviation
    2.63 +  real_of_int :: "int \<Rightarrow> real"
    2.64 +where
    2.65 +  "real_of_int \<equiv> of_int"
    2.66 +
    2.67 +abbreviation
    2.68 +  real_of_rat :: "rat \<Rightarrow> real"
    2.69 +where
    2.70 +  "real_of_rat \<equiv> of_rat"
    2.71 +
    2.72 +consts
    2.73 +  (*overloaded constant for injecting other types into "real"*)
    2.74 +  real :: "'a => real"
    2.75  
    2.76  defs (overloaded)
    2.77 -  real_of_nat_def: "real z == of_nat z"
    2.78 -  real_of_int_def: "real z == of_int z"
    2.79 +  real_of_nat_def [code unfold]: "real == real_of_nat"
    2.80 +  real_of_int_def [code unfold]: "real == real_of_int"
    2.81  
    2.82  lemma real_eq_of_nat: "real = of_nat"
    2.83 -  apply (rule ext)
    2.84 -  apply (unfold real_of_nat_def)
    2.85 -  apply (rule refl)
    2.86 -  done
    2.87 +  unfolding real_of_nat_def ..
    2.88  
    2.89  lemma real_eq_of_int: "real = of_int"
    2.90 -  apply (rule ext)
    2.91 -  apply (unfold real_of_int_def)
    2.92 -  apply (rule refl)
    2.93 -  done
    2.94 +  unfolding real_of_int_def ..
    2.95  
    2.96  lemma real_of_int_zero [simp]: "real (0::int) = 0"  
    2.97  by (simp add: real_of_int_def) 
    2.98 @@ -811,14 +827,14 @@
    2.99  
   2.100  subsection{*Numerals and Arithmetic*}
   2.101  
   2.102 -instance real :: number ..
   2.103 +instance real :: number_ring
   2.104 +  real_number_of_def: "number_of w \<equiv> real_of_int w"
   2.105 +  by intro_classes (simp add: real_number_of_def)
   2.106  
   2.107 -defs (overloaded)
   2.108 -  real_number_of_def: "(number_of w :: real) == of_int w"
   2.109 -    --{*the type constraint is essential!*}
   2.110 +lemma [code, code unfold]:
   2.111 +  "number_of k = real_of_int (number_of k)"
   2.112 +  unfolding number_of_is_id real_number_of_def ..
   2.113  
   2.114 -instance real :: number_ring
   2.115 -by (intro_classes, simp add: real_number_of_def) 
   2.116  
   2.117  text{*Collapse applications of @{term real} to @{term number_of}*}
   2.118  lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
   2.119 @@ -940,8 +956,4 @@
   2.120    "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
   2.121    "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
   2.122  
   2.123 -lemma [code, code unfold]:
   2.124 -  "number_of k = real (number_of k :: int)"
   2.125 -  by simp
   2.126 -
   2.127  end