# 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 \ int \ 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 \ 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 (\x \ 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 (\x \ 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 \ 'a::field_char_0" where - "of_rat q = contents (\(a,b) \ Rep_Rat q. {of_int a / of_int b})" + [code func del]: "of_rat q = contents (\(a,b) \ Rep_Rat q. {of_int a / of_int b})" lemma of_rat_congruent: "(\(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 \ rat" +where + "rat_of_nat \ of_nat" + +abbreviation + rat_of_int :: "int \ rat" +where + "rat_of_int \ 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 (\(x,y) \ Rep_Real(z). \(u,v) \ 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 (\(x,y) \ 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 (\(x,y) \ Rep_Real(z). \(u,v) \ 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 \ (w::real) == \x y u v. x+v \ u+y & (x,y) \ Rep_Real z & (u,v) \ Rep_Real w" real_less_def: "(x < (y::real)) == (x \ y & x \ 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 \ real" +where + "real_of_nat \ of_nat" + +abbreviation + real_of_int :: "int \ real" +where + "real_of_int \ of_int" + +abbreviation + real_of_rat :: "rat \ real" +where + "real_of_rat \ 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 \ 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 \ real" ("Rat.rat'_of'_int") "real :: nat \ real" ("(Rat.rat'_of'_int o {*int*})") -lemma [code, code unfold]: - "number_of k = real (number_of k :: int)" - by simp - end