# HG changeset patch
# User haftmann
# Date 1186667573 -7200
# Node ID 4031da6d8ba324c00bad0847bb05a42f10b6319c
# Parent  c9e3cb5e568147186139bdfc1b79ff1d15492e54
adaptions for code generation

diff -r c9e3cb5e5681 -r 4031da6d8ba3 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Aug 09 15:52:49 2007 +0200
+++ b/src/HOL/Real/Rational.thy	Thu Aug 09 15:52:53 2007 +0200
@@ -81,7 +81,11 @@
 
 definition
   Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
-  "Fract a b = Abs_Rat (ratrel``{(a,b)})"
+  [code func del]: "Fract a b = Abs_Rat (ratrel``{(a,b)})"
+
+lemma Fract_zero:
+  "Fract k 0 = Fract l 0"
+  by (simp add: Fract_def ratrel_def)
 
 theorem Rat_cases [case_names Fract, cases type: rat]:
     "(!!a b. q = Fract a b ==> b \<noteq> 0 ==> C) ==> C"
@@ -161,9 +165,11 @@
 
 instance rat :: zero
   Zero_rat_def: "0 == Fract 0 1" ..
+lemmas [code func del] = Zero_rat_def
 
 instance rat :: one
   One_rat_def: "1 == Fract 1 1" ..
+lemmas [code func del] = One_rat_def
 
 instance rat :: plus
   add_rat_def:
@@ -176,7 +182,7 @@
   minus_rat_def:
     "- q == Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
   diff_rat_def:  "q - r == q + - (r::rat)" ..
-lemmas [code func del] = minus_rat_def
+lemmas [code func del] = minus_rat_def diff_rat_def
 
 instance rat :: times
   mult_rat_def:
@@ -191,7 +197,7 @@
         Abs_Rat (\<Union>x \<in> Rep_Rat q.
             ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})"
   divide_rat_def:  "q / r == q * inverse (r::rat)" ..
-lemmas [code func del] = inverse_rat_def
+lemmas [code func del] = inverse_rat_def divide_rat_def
 
 instance rat :: ord
   le_rat_def:
@@ -459,6 +465,9 @@
 lemma Fract_of_int_eq: "Fract k 1 = of_int k"
 by (rule of_int_rat [symmetric])
 
+lemma Fract_of_int_quotient: "Fract k l = (if l = 0 then Fract 1 0 else of_int k / of_int l)"
+by (auto simp add: Fract_zero Fract_of_int_eq [symmetric] divide_rat)
+
 
 subsection {* Numerals and Arithmetic *}
 
@@ -474,14 +483,14 @@
 
 subsection {* Embedding from Rationals to other Fields *}
 
-axclass field_char_0 < field, ring_char_0
+class field_char_0 = field + ring_char_0
 
 instance ordered_field < field_char_0 ..
 
 definition
   of_rat :: "rat \<Rightarrow> 'a::field_char_0"
 where
-  "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
+  [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
 
 lemma of_rat_congruent:
   "(\<lambda>(a, b). {of_int a / of_int b::'a::field_char_0}) respects ratrel"
@@ -570,4 +579,14 @@
 lemmas zero_rat = Zero_rat_def
 lemmas one_rat = One_rat_def
 
+abbreviation
+  rat_of_nat :: "nat \<Rightarrow> rat"
+where
+  "rat_of_nat \<equiv> of_nat"
+
+abbreviation
+  rat_of_int :: "int \<Rightarrow> rat"
+where
+  "rat_of_int \<equiv> of_int"
+
 end
diff -r c9e3cb5e5681 -r 4031da6d8ba3 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Aug 09 15:52:49 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Aug 09 15:52:53 2007 +0200
@@ -25,39 +25,42 @@
   real_of_preal :: "preal => real" where
   "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
 
-consts
-   (*overloaded constant for injecting other types into "real"*)
-   real :: "'a => real"
-
 instance real :: zero
   real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
+lemmas [code func del] = real_zero_def
 
 instance real :: one
   real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
+lemmas [code func del] = real_one_def
 
 instance real :: plus
   real_add_def: "z + w ==
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
 		 { Abs_Real(realrel``{(x+u, y+v)}) })" ..
+lemmas [code func del] = real_add_def
 
 instance real :: minus
   real_minus_def: "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   real_diff_def: "r - (s::real) == r + - s" ..
+lemmas [code func del] = real_minus_def real_diff_def
 
 instance real :: times
   real_mult_def:
     "z * w ==
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
 		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
+lemmas [code func del] = real_mult_def
 
 instance real :: inverse
   real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
   real_divide_def: "R / (S::real) == R * inverse S" ..
+lemmas [code func del] = real_inverse_def real_divide_def
 
 instance real :: ord
   real_le_def: "z \<le> (w::real) == 
     \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
   real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
+lemmas [code func del] = real_le_def real_less_def
 
 instance real :: abs
   real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
@@ -520,23 +523,36 @@
 by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
 
 
-subsection{*Embedding the Integers into the Reals*}
+subsection {* Embedding numbers into the Reals *}
+
+abbreviation
+  real_of_nat :: "nat \<Rightarrow> real"
+where
+  "real_of_nat \<equiv> of_nat"
+
+abbreviation
+  real_of_int :: "int \<Rightarrow> real"
+where
+  "real_of_int \<equiv> of_int"
+
+abbreviation
+  real_of_rat :: "rat \<Rightarrow> real"
+where
+  "real_of_rat \<equiv> of_rat"
+
+consts
+  (*overloaded constant for injecting other types into "real"*)
+  real :: "'a => real"
 
 defs (overloaded)
-  real_of_nat_def: "real z == of_nat z"
-  real_of_int_def: "real z == of_int z"
+  real_of_nat_def [code unfold]: "real == real_of_nat"
+  real_of_int_def [code unfold]: "real == real_of_int"
 
 lemma real_eq_of_nat: "real = of_nat"
-  apply (rule ext)
-  apply (unfold real_of_nat_def)
-  apply (rule refl)
-  done
+  unfolding real_of_nat_def ..
 
 lemma real_eq_of_int: "real = of_int"
-  apply (rule ext)
-  apply (unfold real_of_int_def)
-  apply (rule refl)
-  done
+  unfolding real_of_int_def ..
 
 lemma real_of_int_zero [simp]: "real (0::int) = 0"  
 by (simp add: real_of_int_def) 
@@ -811,14 +827,14 @@
 
 subsection{*Numerals and Arithmetic*}
 
-instance real :: number ..
+instance real :: number_ring
+  real_number_of_def: "number_of w \<equiv> real_of_int w"
+  by intro_classes (simp add: real_number_of_def)
 
-defs (overloaded)
-  real_number_of_def: "(number_of w :: real) == of_int w"
-    --{*the type constraint is essential!*}
+lemma [code, code unfold]:
+  "number_of k = real_of_int (number_of k)"
+  unfolding number_of_is_id real_number_of_def ..
 
-instance real :: number_ring
-by (intro_classes, simp add: real_number_of_def) 
 
 text{*Collapse applications of @{term real} to @{term number_of}*}
 lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
@@ -940,8 +956,4 @@
   "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
   "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
 
-lemma [code, code unfold]:
-  "number_of k = real (number_of k :: int)"
-  by simp
-
 end