src/HOL/ex/Dedekind_Real.thy
changeset 37765 26bdfb7b680b
parent 37388 793618618f78
child 39910 10097e0a9dbd
     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  definition
     1.6    cut :: "rat set => bool" where
     1.7 -  [code del]: "cut A = ({} \<subset> A &
     1.8 +  "cut A = ({} \<subset> A &
     1.9              A < {r. 0 < r} &
    1.10              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
    1.11  
    1.12 @@ -49,7 +49,7 @@
    1.13  
    1.14  definition
    1.15    psup :: "preal set => preal" where
    1.16 -  [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
    1.17 +  "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
    1.18  
    1.19  definition
    1.20    add_set :: "[rat set,rat set] => rat set" where
    1.21 @@ -57,7 +57,7 @@
    1.22  
    1.23  definition
    1.24    diff_set :: "[rat set,rat set] => rat set" where
    1.25 -  [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    1.26 +  "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    1.27  
    1.28  definition
    1.29    mult_set :: "[rat set,rat set] => rat set" where
    1.30 @@ -65,17 +65,17 @@
    1.31  
    1.32  definition
    1.33    inverse_set :: "rat set => rat set" where
    1.34 -  [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    1.35 +  "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    1.36  
    1.37  instantiation preal :: "{ord, plus, minus, times, inverse, one}"
    1.38  begin
    1.39  
    1.40  definition
    1.41 -  preal_less_def [code del]:
    1.42 +  preal_less_def:
    1.43      "R < S == Rep_preal R < Rep_preal S"
    1.44  
    1.45  definition
    1.46 -  preal_le_def [code del]:
    1.47 +  preal_le_def:
    1.48      "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
    1.49  
    1.50  definition
    1.51 @@ -1162,7 +1162,7 @@
    1.52  
    1.53  definition
    1.54    realrel   ::  "((preal * preal) * (preal * preal)) set" where
    1.55 -  [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    1.56 +  "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    1.57  
    1.58  typedef (Real)  real = "UNIV//realrel"
    1.59    by (auto simp add: quotient_def)
    1.60 @@ -1170,46 +1170,46 @@
    1.61  definition
    1.62    (** these don't use the overloaded "real" function: users don't see them **)
    1.63    real_of_preal :: "preal => real" where
    1.64 -  [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
    1.65 +  "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
    1.66  
    1.67  instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
    1.68  begin
    1.69  
    1.70  definition
    1.71 -  real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
    1.72 +  real_zero_def: "0 = Abs_Real(realrel``{(1, 1)})"
    1.73  
    1.74  definition
    1.75 -  real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
    1.76 +  real_one_def: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
    1.77  
    1.78  definition
    1.79 -  real_add_def [code del]: "z + w =
    1.80 +  real_add_def: "z + w =
    1.81         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.82                   { Abs_Real(realrel``{(x+u, y+v)}) })"
    1.83  
    1.84  definition
    1.85 -  real_minus_def [code del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.86 +  real_minus_def: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.87  
    1.88  definition
    1.89 -  real_diff_def [code del]: "r - (s::real) = r + - s"
    1.90 +  real_diff_def: "r - (s::real) = r + - s"
    1.91  
    1.92  definition
    1.93 -  real_mult_def [code del]:
    1.94 +  real_mult_def:
    1.95      "z * w =
    1.96         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.97                   { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
    1.98  
    1.99  definition
   1.100 -  real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
   1.101 +  real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
   1.102  
   1.103  definition
   1.104 -  real_divide_def [code del]: "R / (S::real) = R * inverse S"
   1.105 +  real_divide_def: "R / (S::real) = R * inverse S"
   1.106  
   1.107  definition
   1.108 -  real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
   1.109 +  real_le_def: "z \<le> (w::real) \<longleftrightarrow>
   1.110      (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
   1.111  
   1.112  definition
   1.113 -  real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   1.114 +  real_less_def: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   1.115  
   1.116  definition
   1.117    real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
   1.118 @@ -1656,7 +1656,7 @@
   1.119  begin
   1.120  
   1.121  definition
   1.122 -  real_number_of_def [code del]: "(number_of w :: real) = of_int w"
   1.123 +  real_number_of_def: "(number_of w :: real) = of_int w"
   1.124  
   1.125  instance
   1.126    by intro_classes (simp add: real_number_of_def)