instantiation target rather than legacy instance
authorhaftmann
Fri Dec 07 15:07:59 2007 +0100 (2007-12-07)
changeset 25571c9e39eafc7a0
parent 25570 fdfbbb92dadf
child 25572 0c9052719f20
instantiation target rather than legacy instance
src/HOL/Complex/Complex.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/IntDef.thy
src/HOL/IntDiv.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Product_ord.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/NatBin.thy
src/HOL/Numeral.thy
src/HOL/Real/PReal.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealVector.thy
     1.1 --- a/src/HOL/Complex/Complex.thy	Fri Dec 07 15:07:56 2007 +0100
     1.2 +++ b/src/HOL/Complex/Complex.thy	Fri Dec 07 15:07:59 2007 +0100
     1.3 @@ -33,19 +33,24 @@
     1.4  
     1.5  subsection {* Addition and Subtraction *}
     1.6  
     1.7 -instance complex :: zero
     1.8 -  complex_zero_def:
     1.9 -    "0 \<equiv> Complex 0 0" ..
    1.10 +instantiation complex :: "{zero, plus, minus}"
    1.11 +begin
    1.12 +
    1.13 +definition
    1.14 +  complex_zero_def: "0 = Complex 0 0"
    1.15 +
    1.16 +definition
    1.17 +  complex_add_def: "x + y = Complex (Re x + Re y) (Im x + Im y)"
    1.18  
    1.19 -instance complex :: plus
    1.20 -  complex_add_def:
    1.21 -    "x + y \<equiv> Complex (Re x + Re y) (Im x + Im y)" ..
    1.22 +definition
    1.23 +  complex_minus_def: "- x = Complex (- Re x) (- Im x)"
    1.24  
    1.25 -instance complex :: minus
    1.26 -  complex_minus_def:
    1.27 -    "- x \<equiv> Complex (- Re x) (- Im x)"
    1.28 -  complex_diff_def:
    1.29 -    "x - (y\<Colon>complex) \<equiv> x + - y" ..
    1.30 +definition
    1.31 +  complex_diff_def: "x - (y\<Colon>complex) = x + - y"
    1.32 +
    1.33 +instance ..
    1.34 +
    1.35 +end
    1.36  
    1.37  lemma Complex_eq_0 [simp]: "(Complex a b = 0) = (a = 0 \<and> b = 0)"
    1.38  by (simp add: complex_zero_def)
    1.39 @@ -103,20 +108,26 @@
    1.40  
    1.41  subsection {* Multiplication and Division *}
    1.42  
    1.43 -instance complex :: one
    1.44 -  complex_one_def:
    1.45 -    "1 \<equiv> Complex 1 0" ..
    1.46 +instantiation complex :: "{one, times, inverse}"
    1.47 +begin
    1.48 +
    1.49 +definition
    1.50 +  complex_one_def: "1 = Complex 1 0"
    1.51 +
    1.52 +definition
    1.53 +  complex_mult_def: "x * y =
    1.54 +    Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)"
    1.55  
    1.56 -instance complex :: times
    1.57 -  complex_mult_def:
    1.58 -    "x * y \<equiv> Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)" ..
    1.59 +definition
    1.60 +  complex_inverse_def: "inverse x =
    1.61 +    Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
    1.62  
    1.63 -instance complex :: inverse
    1.64 -  complex_inverse_def:
    1.65 -    "inverse x \<equiv>
    1.66 -     Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
    1.67 -  complex_divide_def:
    1.68 -    "x / (y\<Colon>complex) \<equiv> x * inverse y" ..
    1.69 +definition
    1.70 +  complex_divide_def: "x / (y\<Colon>complex) = x * inverse y"
    1.71 +
    1.72 +instance ..
    1.73 +
    1.74 +end
    1.75  
    1.76  lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
    1.77  by (simp add: complex_one_def)
    1.78 @@ -193,12 +204,16 @@
    1.79  
    1.80  subsection {* Numerals and Arithmetic *}
    1.81  
    1.82 -instance complex :: number
    1.83 -  complex_number_of_def:
    1.84 -    "number_of w \<equiv> of_int w \<Colon> complex" ..
    1.85 +instantiation complex :: number_ring
    1.86 +begin
    1.87  
    1.88 -instance complex :: number_ring
    1.89 -by (intro_classes, simp only: complex_number_of_def)
    1.90 +definition
    1.91 +  complex_number_of_def: "number_of w = (of_int w \<Colon> complex)"
    1.92 +
    1.93 +instance
    1.94 +  by (intro_classes, simp only: complex_number_of_def)
    1.95 +
    1.96 +end
    1.97  
    1.98  lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
    1.99  by (induct n) simp_all
   1.100 @@ -225,9 +240,15 @@
   1.101  
   1.102  subsection {* Scalar Multiplication *}
   1.103  
   1.104 -instance complex :: scaleR
   1.105 -  complex_scaleR_def:
   1.106 -    "scaleR r x \<equiv> Complex (r * Re x) (r * Im x)" ..
   1.107 +instantiation complex :: scaleR
   1.108 +begin
   1.109 +
   1.110 +definition
   1.111 +  complex_scaleR_def: "scaleR r x = Complex (r * Re x) (r * Im x)"
   1.112 +
   1.113 +instance ..
   1.114 +
   1.115 +end
   1.116  
   1.117  lemma complex_scaleR [simp]:
   1.118    "scaleR r (Complex a b) = Complex (r * a) (r * b)"
   1.119 @@ -291,16 +312,29 @@
   1.120  
   1.121  subsection {* Vector Norm *}
   1.122  
   1.123 -instance complex :: norm
   1.124 -  complex_norm_def:
   1.125 -    "norm z \<equiv> sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)" ..
   1.126 +instantiation complex :: norm
   1.127 +begin
   1.128 +
   1.129 +definition
   1.130 +  complex_norm_def: "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
   1.131 +
   1.132 +instance ..
   1.133 +
   1.134 +end
   1.135  
   1.136  abbreviation
   1.137    cmod :: "complex \<Rightarrow> real" where
   1.138      "cmod \<equiv> norm"
   1.139  
   1.140 -instance complex :: sgn
   1.141 -  complex_sgn_def: "sgn x == x /\<^sub>R cmod x" ..
   1.142 +instantiation complex :: sgn
   1.143 +begin
   1.144 +
   1.145 +definition
   1.146 +  complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
   1.147 +
   1.148 +instance ..
   1.149 +
   1.150 +end
   1.151  
   1.152  lemmas cmod_def = complex_norm_def
   1.153  
     2.1 --- a/src/HOL/Divides.thy	Fri Dec 07 15:07:56 2007 +0100
     2.2 +++ b/src/HOL/Divides.thy	Fri Dec 07 15:07:59 2007 +0100
     2.3 @@ -15,11 +15,20 @@
     2.4    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
     2.5    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
     2.6  
     2.7 -instance nat :: Divides.div
     2.8 +instantiation nat :: Divides.div
     2.9 +begin
    2.10 +
    2.11 +definition
    2.12    div_def: "m div n == wfrec (pred_nat^+)
    2.13                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    2.14 +
    2.15 +definition
    2.16    mod_def: "m mod n == wfrec (pred_nat^+)
    2.17 -                          (%f j. if j<n | n=0 then j else f (j-n)) m" ..
    2.18 +                          (%f j. if j<n | n=0 then j else f (j-n)) m"
    2.19 +
    2.20 +instance ..
    2.21 +
    2.22 +end
    2.23  
    2.24  definition (in div)
    2.25    dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
     3.1 --- a/src/HOL/Finite_Set.thy	Fri Dec 07 15:07:56 2007 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Fri Dec 07 15:07:59 2007 +0100
     3.3 @@ -2665,32 +2665,48 @@
     3.4  lemma univ_unit [noatp]:
     3.5    "UNIV = {()}" by auto
     3.6  
     3.7 -instance unit :: finite
     3.8 -  "Finite_Set.itself \<equiv> TYPE(unit)"
     3.9 -proof
    3.10 +instantiation unit :: finite
    3.11 +begin
    3.12 +
    3.13 +definition
    3.14 +  "itself = TYPE(unit)"
    3.15 +
    3.16 +instance proof
    3.17    have "finite {()}" by simp
    3.18    also note univ_unit [symmetric]
    3.19    finally show "finite (UNIV :: unit set)" .
    3.20  qed
    3.21  
    3.22 +end
    3.23 +
    3.24  lemmas [code func] = univ_unit
    3.25  
    3.26  lemma univ_bool [noatp]:
    3.27    "UNIV = {False, True}" by auto
    3.28  
    3.29 -instance bool :: finite
    3.30 -  "itself \<equiv> TYPE(bool)"
    3.31 -proof
    3.32 +instantiation bool :: finite
    3.33 +begin
    3.34 +
    3.35 +definition
    3.36 +  "itself = TYPE(bool)"
    3.37 +
    3.38 +instance proof
    3.39    have "finite {False, True}" by simp
    3.40    also note univ_bool [symmetric]
    3.41    finally show "finite (UNIV :: bool set)" .
    3.42  qed
    3.43  
    3.44 +end
    3.45 +
    3.46  lemmas [code func] = univ_bool
    3.47  
    3.48 -instance * :: (finite, finite) finite
    3.49 -  "itself \<equiv> TYPE('a \<times> 'b)"
    3.50 -proof
    3.51 +instantiation * :: (finite, finite) finite
    3.52 +begin
    3.53 +
    3.54 +definition
    3.55 +  "itself = TYPE('a \<times> 'b)"
    3.56 +
    3.57 +instance proof
    3.58    show "finite (UNIV :: ('a \<times> 'b) set)"
    3.59    proof (rule finite_Prod_UNIV)
    3.60      show "finite (UNIV :: 'a set)" by (rule finite)
    3.61 @@ -2698,13 +2714,19 @@
    3.62    qed
    3.63  qed
    3.64  
    3.65 +end
    3.66 +
    3.67  lemma univ_prod [noatp, code func]:
    3.68    "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
    3.69    unfolding UNIV_Times_UNIV ..
    3.70  
    3.71 -instance "+" :: (finite, finite) finite
    3.72 -  "itself \<equiv> TYPE('a + 'b)"
    3.73 -proof
    3.74 +instantiation "+" :: (finite, finite) finite
    3.75 +begin
    3.76 +
    3.77 +definition
    3.78 +  "itself = TYPE('a + 'b)"
    3.79 +
    3.80 +instance proof
    3.81    have a: "finite (UNIV :: 'a set)" by (rule finite)
    3.82    have b: "finite (UNIV :: 'b set)" by (rule finite)
    3.83    from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
    3.84 @@ -2712,28 +2734,40 @@
    3.85    thus "finite (UNIV :: ('a + 'b) set)" by simp
    3.86  qed
    3.87  
    3.88 +end
    3.89 +
    3.90  lemma univ_sum [noatp, code func]:
    3.91    "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
    3.92    unfolding UNIV_Plus_UNIV ..
    3.93  
    3.94 -instance set :: (finite) finite
    3.95 -  "itself \<equiv> TYPE('a set)"
    3.96 -proof
    3.97 +instantiation set :: (finite) finite
    3.98 +begin
    3.99 +
   3.100 +definition
   3.101 +  "itself = TYPE('a set)"
   3.102 +
   3.103 +instance proof
   3.104    have "finite (UNIV :: 'a set)" by (rule finite)
   3.105    hence "finite (Pow (UNIV :: 'a set))"
   3.106      by (rule finite_Pow_iff [THEN iffD2])
   3.107    thus "finite (UNIV :: 'a set set)" by simp
   3.108  qed
   3.109  
   3.110 +end
   3.111 +
   3.112  lemma univ_set [noatp, code func]:
   3.113    "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
   3.114  
   3.115  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   3.116    by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   3.117  
   3.118 -instance "fun" :: (finite, finite) finite
   3.119 +instantiation "fun" :: (finite, finite) finite
   3.120 +begin
   3.121 +
   3.122 +definition
   3.123    "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
   3.124 -proof
   3.125 +
   3.126 +instance proof
   3.127    show "finite (UNIV :: ('a => 'b) set)"
   3.128    proof (rule finite_imageD)
   3.129      let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
   3.130 @@ -2742,6 +2776,8 @@
   3.131    qed
   3.132  qed
   3.133  
   3.134 +end
   3.135 +
   3.136  hide (open) const itself
   3.137  
   3.138  subsection {* Equality and order on functions *}
     4.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Fri Dec 07 15:07:56 2007 +0100
     4.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Dec 07 15:07:59 2007 +0100
     4.3 @@ -11,45 +11,137 @@
     4.4  
     4.5  subsection {* Syntactic classes *}
     4.6  
     4.7 -instance star :: (zero) zero
     4.8 -  star_zero_def:    "0 \<equiv> star_of 0" ..
     4.9 +instantiation star :: (zero) zero
    4.10 +begin
    4.11 +
    4.12 +definition
    4.13 +  star_zero_def:    "0 \<equiv> star_of 0"
    4.14 +
    4.15 +instance ..
    4.16 +
    4.17 +end
    4.18 +
    4.19 +instantiation star :: (one) one
    4.20 +begin
    4.21 +
    4.22 +definition
    4.23 +  star_one_def:     "1 \<equiv> star_of 1"
    4.24  
    4.25 -instance star :: (one) one
    4.26 -  star_one_def:     "1 \<equiv> star_of 1" ..
    4.27 +instance ..
    4.28 +
    4.29 +end
    4.30 +
    4.31 +instantiation star :: (plus) plus
    4.32 +begin
    4.33  
    4.34 -instance star :: (plus) plus
    4.35 -  star_add_def:     "(op +) \<equiv> *f2* (op +)" ..
    4.36 +definition
    4.37 +  star_add_def:     "(op +) \<equiv> *f2* (op +)"
    4.38 +
    4.39 +instance ..
    4.40 +
    4.41 +end
    4.42 +
    4.43 +instantiation star :: (times) times
    4.44 +begin
    4.45  
    4.46 -instance star :: (times) times
    4.47 -  star_mult_def:    "(op *) \<equiv> *f2* (op *)" ..
    4.48 +definition
    4.49 +  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
    4.50 +
    4.51 +instance ..
    4.52  
    4.53 -instance star :: (minus) minus
    4.54 +end
    4.55 +
    4.56 +instantiation star :: (minus) minus
    4.57 +begin
    4.58 +
    4.59 +definition
    4.60    star_minus_def:   "uminus \<equiv> *f* uminus"
    4.61 -  star_diff_def:    "(op -) \<equiv> *f2* (op -)" ..
    4.62 +
    4.63 +definition
    4.64 +  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
    4.65 +
    4.66 +instance ..
    4.67 +
    4.68 +end
    4.69  
    4.70 -instance star :: (abs) abs
    4.71 -  star_abs_def:     "abs \<equiv> *f* abs" ..
    4.72 +instantiation star :: (abs) abs
    4.73 +begin
    4.74 +
    4.75 +definition
    4.76 +  star_abs_def:     "abs \<equiv> *f* abs"
    4.77 +
    4.78 +instance ..
    4.79 +
    4.80 +end
    4.81 +
    4.82 +instantiation star :: (sgn) sgn
    4.83 +begin
    4.84  
    4.85 -instance star :: (sgn) sgn
    4.86 -  star_sgn_def:     "sgn \<equiv> *f* sgn" ..
    4.87 +definition
    4.88 +  star_sgn_def:     "sgn \<equiv> *f* sgn"
    4.89 +
    4.90 +instance ..
    4.91  
    4.92 -instance star :: (inverse) inverse
    4.93 +end
    4.94 +
    4.95 +instantiation star :: (inverse) inverse
    4.96 +begin
    4.97 +
    4.98 +definition
    4.99    star_divide_def:  "(op /) \<equiv> *f2* (op /)"
   4.100 -  star_inverse_def: "inverse \<equiv> *f* inverse" ..
   4.101 +
   4.102 +definition
   4.103 +  star_inverse_def: "inverse \<equiv> *f* inverse"
   4.104 +
   4.105 +instance ..
   4.106 +
   4.107 +end
   4.108  
   4.109 -instance star :: (number) number
   4.110 -  star_number_def:  "number_of b \<equiv> star_of (number_of b)" ..
   4.111 +instantiation star :: (number) number
   4.112 +begin
   4.113 +
   4.114 +definition
   4.115 +  star_number_def:  "number_of b \<equiv> star_of (number_of b)"
   4.116 +
   4.117 +instance ..
   4.118 +
   4.119 +end
   4.120 +
   4.121 +instantiation star :: (Divides.div) Divides.div
   4.122 +begin
   4.123  
   4.124 -instance star :: (Divides.div) Divides.div
   4.125 +definition
   4.126    star_div_def:     "(op div) \<equiv> *f2* (op div)"
   4.127 -  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)" ..
   4.128 +
   4.129 +definition
   4.130 +  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
   4.131 +
   4.132 +instance ..
   4.133 +
   4.134 +end
   4.135 +
   4.136 +instantiation star :: (power) power
   4.137 +begin
   4.138 +
   4.139 +definition
   4.140 +  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
   4.141  
   4.142 -instance star :: (power) power
   4.143 -  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
   4.144 +instance ..
   4.145 +
   4.146 +end
   4.147 +
   4.148 +instantiation star :: (ord) ord
   4.149 +begin
   4.150  
   4.151 -instance star :: (ord) ord
   4.152 +definition
   4.153    star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
   4.154 -  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
   4.155 +
   4.156 +definition
   4.157 +  star_less_def:    "(op <) \<equiv> *p2* (op <)"
   4.158 +
   4.159 +instance ..
   4.160 +
   4.161 +end
   4.162  
   4.163  lemmas star_class_defs [transfer_unfold] =
   4.164    star_zero_def     star_one_def      star_number_def
   4.165 @@ -220,14 +312,28 @@
   4.166  apply (transfer, erule (1) order_antisym)
   4.167  done
   4.168  
   4.169 -instance star :: (lower_semilattice) lower_semilattice
   4.170 +instantiation star :: (lower_semilattice) lower_semilattice
   4.171 +begin
   4.172 +
   4.173 +definition
   4.174    star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
   4.175 +
   4.176 +instance
   4.177    by default (transfer star_inf_def, auto)+
   4.178  
   4.179 -instance star :: (upper_semilattice) upper_semilattice
   4.180 +end
   4.181 +
   4.182 +instantiation star :: (upper_semilattice) upper_semilattice
   4.183 +begin
   4.184 +
   4.185 +definition
   4.186    star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
   4.187 +
   4.188 +instance
   4.189    by default (transfer star_sup_def, auto)+
   4.190  
   4.191 +end
   4.192 +
   4.193  instance star :: (lattice) lattice ..
   4.194  
   4.195  instance star :: (distrib_lattice) distrib_lattice
     5.1 --- a/src/HOL/IntDef.thy	Fri Dec 07 15:07:56 2007 +0100
     5.2 +++ b/src/HOL/IntDef.thy	Fri Dec 07 15:07:59 2007 +0100
     5.3 @@ -22,34 +22,48 @@
     5.4    int = "UNIV//intrel"
     5.5    by (auto simp add: quotient_def)
     5.6  
     5.7 -instance int :: zero
     5.8 -  Zero_int_def: "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" ..
     5.9 +instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}"
    5.10 +begin
    5.11 +
    5.12 +definition
    5.13 +  Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
    5.14 +
    5.15 +definition
    5.16 +  One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
    5.17  
    5.18 -instance int :: one
    5.19 -  One_int_def: "1 \<equiv> Abs_Integ (intrel `` {(1, 0)})" ..
    5.20 +definition
    5.21 +  add_int_def [code func del]: "z + w = Abs_Integ
    5.22 +    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    5.23 +      intrel `` {(x + u, y + v)})"
    5.24  
    5.25 -instance int :: plus
    5.26 -  add_int_def: "z + w \<equiv> Abs_Integ
    5.27 -    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    5.28 -      intrel `` {(x + u, y + v)})" ..
    5.29 +definition
    5.30 +  minus_int_def [code func del]:
    5.31 +    "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    5.32 +
    5.33 +definition
    5.34 +  diff_int_def [code func del]:  "z - w = z + (-w \<Colon> int)"
    5.35  
    5.36 -instance int :: minus
    5.37 -  minus_int_def:
    5.38 -    "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    5.39 -  diff_int_def:  "z - w \<equiv> z + (-w \<Colon> int)" ..
    5.40 -
    5.41 -instance int :: times
    5.42 -  mult_int_def: "z * w \<equiv>  Abs_Integ
    5.43 +definition
    5.44 +  mult_int_def [code func del]: "z * w = Abs_Integ
    5.45      (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    5.46 -      intrel `` {(x*u + y*v, x*v + y*u)})" ..
    5.47 +      intrel `` {(x*u + y*v, x*v + y*u)})"
    5.48 +
    5.49 +definition
    5.50 +  le_int_def [code func del]:
    5.51 +   "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
    5.52 +
    5.53 +definition
    5.54 +  less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
    5.55  
    5.56 -instance int :: ord
    5.57 -  le_int_def:
    5.58 -   "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
    5.59 -  less_int_def: "(z\<Colon>int) < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
    5.60 +definition
    5.61 +  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    5.62  
    5.63 -lemmas [code func del] = Zero_int_def One_int_def add_int_def
    5.64 -  minus_int_def mult_int_def le_int_def less_int_def
    5.65 +definition
    5.66 +  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    5.67 +
    5.68 +instance ..
    5.69 +
    5.70 +end
    5.71  
    5.72  
    5.73  subsection{*Construction of the Integers*}
    5.74 @@ -212,17 +226,21 @@
    5.75  apply (auto simp add: zmult_zless_mono2_lemma)
    5.76  done
    5.77  
    5.78 -instance int :: abs
    5.79 -  zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
    5.80 -instance int :: sgn
    5.81 -  zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
    5.82 +instantiation int :: distrib_lattice
    5.83 +begin
    5.84  
    5.85 -instance int :: distrib_lattice
    5.86 -  "inf \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> min"
    5.87 -  "sup \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> max"
    5.88 +definition
    5.89 +  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
    5.90 +
    5.91 +definition
    5.92 +  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
    5.93 +
    5.94 +instance
    5.95    by intro_classes
    5.96      (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
    5.97  
    5.98 +end
    5.99 +
   5.100  text{*The integers form an ordered integral domain*}
   5.101  instance int :: ordered_idom
   5.102  proof
   5.103 @@ -744,7 +762,7 @@
   5.104  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
   5.105  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   5.106  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
   5.107 -lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   5.108 +lemmas zless_le = less_int_def
   5.109  lemmas int_eq_of_nat = TrueI
   5.110  
   5.111  abbreviation
     6.1 --- a/src/HOL/IntDiv.thy	Fri Dec 07 15:07:56 2007 +0100
     6.2 +++ b/src/HOL/IntDiv.thy	Fri Dec 07 15:07:59 2007 +0100
     6.3 @@ -62,9 +62,18 @@
     6.4                    if 0<b then negDivAlg a b
     6.5                    else negateSnd (posDivAlg (-a) (-b))))"
     6.6  
     6.7 -instance int :: Divides.div
     6.8 -  div_def: "a div b == fst (divAlg (a, b))"
     6.9 -  mod_def: "a mod b == snd (divAlg (a, b))" ..
    6.10 +instantiation int :: Divides.div
    6.11 +begin
    6.12 +
    6.13 +definition
    6.14 +  div_def: "a div b = fst (divAlg (a, b))"
    6.15 +
    6.16 +definition
    6.17 +  mod_def: "a mod b = snd (divAlg (a, b))"
    6.18 +
    6.19 +instance ..
    6.20 +
    6.21 +end
    6.22  
    6.23  lemma divAlg_mod_div:
    6.24    "divAlg (p, q) = (p div q, p mod q)"
     7.1 --- a/src/HOL/Library/Multiset.thy	Fri Dec 07 15:07:56 2007 +0100
     7.2 +++ b/src/HOL/Library/Multiset.thy	Fri Dec 07 15:07:59 2007 +0100
     7.3 @@ -49,11 +49,24 @@
     7.4    set_of :: "'a multiset => 'a set" where
     7.5    "set_of M = {x. x :# M}"
     7.6  
     7.7 -instance multiset :: (type) "{plus, minus, zero, size}" 
     7.8 +instantiation multiset :: (type) "{plus, minus, zero, size}" 
     7.9 +begin
    7.10 +
    7.11 +definition
    7.12    union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
    7.13 +
    7.14 +definition
    7.15    diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
    7.16 +
    7.17 +definition
    7.18    Zero_multiset_def [simp]: "0 == {#}"
    7.19 -  size_def: "size M == setsum (count M) (set_of M)" ..
    7.20 +
    7.21 +definition
    7.22 +  size_def: "size M == setsum (count M) (set_of M)"
    7.23 +
    7.24 +instance ..
    7.25 +
    7.26 +end
    7.27  
    7.28  definition
    7.29    multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"  (infixl "#\<inter>" 70) where
     8.1 --- a/src/HOL/Library/Parity.thy	Fri Dec 07 15:07:56 2007 +0100
     8.2 +++ b/src/HOL/Library/Parity.thy	Fri Dec 07 15:07:59 2007 +0100
     8.3 @@ -16,11 +16,18 @@
     8.4    odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
     8.5    "odd x \<equiv> \<not> even x"
     8.6  
     8.7 -instance int :: even_odd
     8.8 -  even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" ..
     8.9 +instantiation int and nat :: even_odd
    8.10 +begin
    8.11 +
    8.12 +definition
    8.13 +  even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0"
    8.14  
    8.15 -instance nat :: even_odd
    8.16 -  even_nat_def[presburger]: "even x \<equiv> even (int x)" ..
    8.17 +definition
    8.18 +  even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)"
    8.19 +
    8.20 +instance ..
    8.21 +
    8.22 +end
    8.23  
    8.24  
    8.25  subsection {* Even and odd are mutually exclusive *}
     9.1 --- a/src/HOL/Library/Product_ord.thy	Fri Dec 07 15:07:56 2007 +0100
     9.2 +++ b/src/HOL/Library/Product_ord.thy	Fri Dec 07 15:07:59 2007 +0100
     9.3 @@ -9,9 +9,18 @@
     9.4  imports Main
     9.5  begin
     9.6  
     9.7 -instance "*" :: (ord, ord) ord
     9.8 +instantiation "*" :: (ord, ord) ord
     9.9 +begin
    9.10 +
    9.11 +definition
    9.12    prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
    9.13 -  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" ..
    9.14 +
    9.15 +definition
    9.16 +  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
    9.17 +
    9.18 +instance ..
    9.19 +
    9.20 +end
    9.21  
    9.22  lemma [code func]:
    9.23    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    9.24 @@ -29,10 +38,19 @@
    9.25  instance * :: (linorder, linorder) linorder
    9.26    by default (auto simp: prod_le_def)
    9.27  
    9.28 -instance * :: (linorder, linorder) distrib_lattice
    9.29 +instantiation * :: (linorder, linorder) distrib_lattice
    9.30 +begin
    9.31 +
    9.32 +definition
    9.33    inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    9.34 +
    9.35 +definition
    9.36    sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    9.37 +
    9.38 +instance
    9.39    by intro_classes
    9.40      (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    9.41  
    9.42  end
    9.43 +
    9.44 +end
    10.1 --- a/src/HOL/List.thy	Fri Dec 07 15:07:56 2007 +0100
    10.2 +++ b/src/HOL/List.thy	Fri Dec 07 15:07:59 2007 +0100
    10.3 @@ -109,7 +109,6 @@
    10.4  where
    10.5    append_Nil:"[] @ ys = ys"
    10.6    | append_Cons: "(x#xs) @ ys = x # xs @ ys"
    10.7 -declare append.simps [code]
    10.8  
    10.9  primrec
   10.10    "rev([]) = []"
   10.11 @@ -2691,9 +2690,16 @@
   10.12  
   10.13  text{* The integers are an instance of the above class: *}
   10.14  
   10.15 -instance int:: finite_intvl_succ
   10.16 -  successor_int_def: "successor == (%i\<Colon>int. i+1)"
   10.17 -by intro_classes (simp_all add: successor_int_def)
   10.18 +instantiation int:: finite_intvl_succ
   10.19 +begin
   10.20 +
   10.21 +definition
   10.22 +  successor_int_def: "successor = (%i\<Colon>int. i+1)"
   10.23 +
   10.24 +instance
   10.25 +  by intro_classes (simp_all add: successor_int_def)
   10.26 +
   10.27 +end
   10.28  
   10.29  text{* Now @{term"[i..j::int]"} is defined for integers. *}
   10.30  
   10.31 @@ -3178,7 +3184,6 @@
   10.32  where 
   10.33    "x mem [] \<longleftrightarrow> False"
   10.34    | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
   10.35 -declare member.simps [code]
   10.36  
   10.37  primrec
   10.38    "null [] = True"
    11.1 --- a/src/HOL/Nat.thy	Fri Dec 07 15:07:56 2007 +0100
    11.2 +++ b/src/HOL/Nat.thy	Fri Dec 07 15:07:59 2007 +0100
    11.3 @@ -139,20 +139,30 @@
    11.4  
    11.5  subsection {* Arithmetic operators *}
    11.6  
    11.7 -instance nat :: "{one, plus, minus, times}"
    11.8 -  One_nat_def [simp]: "1 == Suc 0" ..
    11.9 +instantiation nat :: "{one, plus, minus, times}"
   11.10 +begin
   11.11  
   11.12 -primrec
   11.13 -  add_0:    "0 + n = n"
   11.14 -  add_Suc:  "Suc m + n = Suc (m + n)"
   11.15 +definition
   11.16 +  One_nat_def [simp]: "1 = Suc 0"
   11.17 +
   11.18 +primrec plus_nat
   11.19 +where
   11.20 +  add_0:      "0 + n = (n\<Colon>nat)"
   11.21 +  | add_Suc:  "Suc m + n = Suc (m + n)"
   11.22  
   11.23 -primrec
   11.24 -  diff_0:   "m - 0 = m"
   11.25 -  diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
   11.26 +primrec minus_nat
   11.27 +where
   11.28 +  diff_0:     "m - 0 = (m\<Colon>nat)"
   11.29 +  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
   11.30  
   11.31 -primrec
   11.32 -  mult_0:   "0 * n = 0"
   11.33 -  mult_Suc: "Suc m * n = n + (m * n)"
   11.34 +primrec times_nat
   11.35 +where
   11.36 +  mult_0:     "0 * n = (0\<Colon>nat)"
   11.37 +  | mult_Suc: "Suc m * n = n + (m * n)"
   11.38 +
   11.39 +instance ..
   11.40 +
   11.41 +end
   11.42  
   11.43  
   11.44  subsection {* Orders on @{typ nat} *}
   11.45 @@ -341,9 +351,6 @@
   11.46    apply (blast dest: Suc_lessD)
   11.47    done
   11.48  
   11.49 -lemma [code]: "((n::nat) < 0) = False" by simp
   11.50 -lemma [code]: "(0 < Suc n) = True" by simp
   11.51 -
   11.52  text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
   11.53  lemma not_less_eq: "(~ m < n) = (n < Suc m)"
   11.54  by (induct m n rule: diff_induct) simp_all
   11.55 @@ -621,6 +628,13 @@
   11.56  
   11.57  declare diff_Suc [simp del, code del]
   11.58  
   11.59 +lemma [code]:
   11.60 +  "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
   11.61 +  "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
   11.62 +  "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
   11.63 +  "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
   11.64 +  using Suc_le_eq less_Suc_eq_le by simp_all
   11.65 +
   11.66  
   11.67  subsection {* Addition *}
   11.68  
   11.69 @@ -1141,16 +1155,6 @@
   11.70  declare "*.size" [noatp]
   11.71  
   11.72  
   11.73 -subsection {* Code generator setup *}
   11.74 -
   11.75 -lemma [code func]:
   11.76 -  "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
   11.77 -  "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
   11.78 -  "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
   11.79 -  "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
   11.80 -  using Suc_le_eq less_Suc_eq_le by simp_all
   11.81 -
   11.82 -
   11.83  subsection {* Embedding of the Naturals into any
   11.84    @{text semiring_1}: @{term of_nat} *}
   11.85  
   11.86 @@ -1162,7 +1166,6 @@
   11.87  where
   11.88    of_nat_0:     "of_nat 0 = 0"
   11.89    | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
   11.90 -declare of_nat.simps [code]
   11.91  
   11.92  lemma of_nat_1 [simp]: "of_nat 1 = 1"
   11.93    by simp
    12.1 --- a/src/HOL/NatBin.thy	Fri Dec 07 15:07:56 2007 +0100
    12.2 +++ b/src/HOL/NatBin.thy	Fri Dec 07 15:07:59 2007 +0100
    12.3 @@ -14,8 +14,15 @@
    12.4    Arithmetic for naturals is reduced to that for the non-negative integers.
    12.5  *}
    12.6  
    12.7 -instance nat :: number
    12.8 -  nat_number_of_def [code inline]: "number_of v == nat (number_of (v\<Colon>int))" ..
    12.9 +instantiation nat :: number
   12.10 +begin
   12.11 +
   12.12 +definition
   12.13 +  nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
   12.14 +
   12.15 +instance ..
   12.16 +
   12.17 +end
   12.18  
   12.19  abbreviation (xsymbols)
   12.20    square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
    13.1 --- a/src/HOL/Numeral.thy	Fri Dec 07 15:07:56 2007 +0100
    13.2 +++ b/src/HOL/Numeral.thy	Fri Dec 07 15:07:59 2007 +0100
    13.3 @@ -210,11 +210,16 @@
    13.4  
    13.5  text {* self-embedding of the integers *}
    13.6  
    13.7 -instance int :: number_ring
    13.8 -  int_number_of_def: "number_of w \<equiv> of_int w \<Colon> int"
    13.9 +instantiation int :: number_ring
   13.10 +begin
   13.11 +
   13.12 +definition
   13.13 +  int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
   13.14 +
   13.15 +instance
   13.16    by intro_classes (simp only: int_number_of_def)
   13.17  
   13.18 -lemmas [code func del] = int_number_of_def
   13.19 +end
   13.20  
   13.21  lemma number_of_is_id:
   13.22    "number_of (k::int) = k"
    14.1 --- a/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:56 2007 +0100
    14.2 +++ b/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:59 2007 +0100
    14.3 @@ -211,12 +211,20 @@
    14.4  instance preal :: linorder
    14.5    by intro_classes (rule preal_le_linear)
    14.6  
    14.7 -instance preal :: distrib_lattice
    14.8 -  "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
    14.9 -  "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal  \<equiv> max"
   14.10 +instantiation preal :: distrib_lattice
   14.11 +begin
   14.12 +
   14.13 +definition
   14.14 +  "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
   14.15 +
   14.16 +definition
   14.17 +  "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
   14.18 +
   14.19 +instance
   14.20    by intro_classes
   14.21      (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
   14.22  
   14.23 +end
   14.24  
   14.25  subsection{*Properties of Addition*}
   14.26  
    15.1 --- a/src/HOL/Real/Rational.thy	Fri Dec 07 15:07:56 2007 +0100
    15.2 +++ b/src/HOL/Real/Rational.thy	Fri Dec 07 15:07:59 2007 +0100
    15.3 @@ -163,60 +163,72 @@
    15.4  
    15.5  subsubsection {* Standard operations on rational numbers *}
    15.6  
    15.7 -instance rat :: zero
    15.8 -  Zero_rat_def: "0 == Fract 0 1" ..
    15.9 -lemmas [code func del] = Zero_rat_def
   15.10 +instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
   15.11 +begin
   15.12 +
   15.13 +definition
   15.14 +  Zero_rat_def [code func del]: "0 = Fract 0 1"
   15.15  
   15.16 -instance rat :: one
   15.17 -  One_rat_def: "1 == Fract 1 1" ..
   15.18 -lemmas [code func del] = One_rat_def
   15.19 +definition
   15.20 +  One_rat_def [code func del]: "1 = Fract 1 1"
   15.21  
   15.22 -instance rat :: plus
   15.23 -  add_rat_def:
   15.24 -   "q + r ==
   15.25 +definition
   15.26 +  add_rat_def [code func del]:
   15.27 +   "q + r =
   15.28         Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   15.29 -           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})" ..
   15.30 -lemmas [code func del] = add_rat_def
   15.31 +           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})"
   15.32  
   15.33 -instance rat :: minus
   15.34 -  minus_rat_def:
   15.35 -    "- q == Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
   15.36 -  diff_rat_def:  "q - r == q + - (r::rat)" ..
   15.37 -lemmas [code func del] = minus_rat_def diff_rat_def
   15.38 +definition
   15.39 +  minus_rat_def [code func del]:
   15.40 +    "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
   15.41 +
   15.42 +definition
   15.43 +  diff_rat_def [code func del]: "q - r = q + - (r::rat)"
   15.44  
   15.45 -instance rat :: times
   15.46 -  mult_rat_def:
   15.47 -   "q * r ==
   15.48 +definition
   15.49 +  mult_rat_def [code func del]:
   15.50 +   "q * r =
   15.51         Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   15.52 -           ratrel``{(fst x * fst y, snd x * snd y)})" ..
   15.53 -lemmas [code func del] = mult_rat_def
   15.54 +           ratrel``{(fst x * fst y, snd x * snd y)})"
   15.55  
   15.56 -instance rat :: inverse
   15.57 -  inverse_rat_def:
   15.58 -    "inverse q ==
   15.59 +definition
   15.60 +  inverse_rat_def [code func del]:
   15.61 +    "inverse q =
   15.62          Abs_Rat (\<Union>x \<in> Rep_Rat q.
   15.63              ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})"
   15.64 -  divide_rat_def:  "q / r == q * inverse (r::rat)" ..
   15.65 -lemmas [code func del] = inverse_rat_def divide_rat_def
   15.66 +
   15.67 +definition
   15.68 +  divide_rat_def [code func del]: "q / r = q * inverse (r::rat)"
   15.69  
   15.70 -instance rat :: ord
   15.71 -  le_rat_def:
   15.72 -   "q \<le> r == contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   15.73 +definition
   15.74 +  le_rat_def [code func del]:
   15.75 +   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   15.76        {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
   15.77 -  less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)" ..
   15.78 -lemmas [code func del] = le_rat_def less_rat_def
   15.79 +
   15.80 +definition
   15.81 +  less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   15.82 +
   15.83 +definition
   15.84 +  abs_rat_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
   15.85  
   15.86 -instance rat :: abs
   15.87 -  abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
   15.88 +definition
   15.89 +  sgn_rat_def: "sgn (q::rat) = (if q=0 then 0 else if 0<q then 1 else - 1)"
   15.90  
   15.91 -instance rat :: sgn
   15.92 -  sgn_rat_def: "sgn(q::rat) == (if q=0 then 0 else if 0<q then 1 else - 1)" ..
   15.93 +instance ..
   15.94 +
   15.95 +end
   15.96  
   15.97 -instance rat :: power ..
   15.98 +instantiation rat :: power
   15.99 +begin
  15.100  
  15.101 -primrec (rat)
  15.102 -  rat_power_0:   "q ^ 0       = 1"
  15.103 -  rat_power_Suc: "q ^ (Suc n) = (q::rat) * (q ^ n)"
  15.104 +primrec power_rat
  15.105 +where
  15.106 +  rat_power_0:     "q ^ 0       = (1\<Colon>rat)"
  15.107 +  | rat_power_Suc: "q ^ (Suc n) = (q\<Colon>rat) * (q ^ n)"
  15.108 +
  15.109 +instance ..
  15.110 +
  15.111 +end
  15.112  
  15.113  theorem eq_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
  15.114    (Fract a b = Fract c d) = (a * d = c * b)"
  15.115 @@ -361,11 +373,20 @@
  15.116    }
  15.117  qed
  15.118  
  15.119 -instance rat :: distrib_lattice
  15.120 -  "inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> min"
  15.121 -  "sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> max"
  15.122 +instantiation rat :: distrib_lattice
  15.123 +begin
  15.124 +
  15.125 +definition
  15.126 +  "(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min"
  15.127 +
  15.128 +definition
  15.129 +  "(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max"
  15.130 +
  15.131 +instance
  15.132    by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
  15.133  
  15.134 +end
  15.135 +
  15.136  instance rat :: ordered_field
  15.137  proof
  15.138    fix q r s :: rat
  15.139 @@ -474,11 +495,16 @@
  15.140  
  15.141  subsection {* Numerals and Arithmetic *}
  15.142  
  15.143 -instance rat :: number
  15.144 -  rat_number_of_def: "(number_of w :: rat) \<equiv> of_int w" ..
  15.145 +instantiation rat :: number_ring
  15.146 +begin
  15.147  
  15.148 -instance rat :: number_ring
  15.149 -  by default (simp add: rat_number_of_def) 
  15.150 +definition
  15.151 +  rat_number_of_def: "number_of w = (of_int w \<Colon> rat)"
  15.152 +
  15.153 +instance
  15.154 +  by default (simp add: rat_number_of_def)
  15.155 +
  15.156 +end 
  15.157  
  15.158  use "rat_arith.ML"
  15.159  declaration {* K rat_arith_setup *}
  15.160 @@ -488,7 +514,7 @@
  15.161  
  15.162  class field_char_0 = field + ring_char_0
  15.163  
  15.164 -instance ordered_field < field_char_0 ..
  15.165 +instance ordered_field < field_char_0 .. 
  15.166  
  15.167  definition
  15.168    of_rat :: "rat \<Rightarrow> 'a::field_char_0"
    16.1 --- a/src/HOL/Real/RealDef.thy	Fri Dec 07 15:07:56 2007 +0100
    16.2 +++ b/src/HOL/Real/RealDef.thy	Fri Dec 07 15:07:59 2007 +0100
    16.3 @@ -25,48 +25,54 @@
    16.4    real_of_preal :: "preal => real" where
    16.5    "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
    16.6  
    16.7 -instance real :: zero
    16.8 -  real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
    16.9 -lemmas [code func del] = real_zero_def
   16.10 +instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
   16.11 +begin
   16.12  
   16.13 -instance real :: one
   16.14 -  real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
   16.15 -lemmas [code func del] = real_one_def
   16.16 +definition
   16.17 +  real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
   16.18 +
   16.19 +definition
   16.20 +  real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
   16.21  
   16.22 -instance real :: plus
   16.23 -  real_add_def: "z + w ==
   16.24 +definition
   16.25 +  real_add_def [code func del]: "z + w =
   16.26         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   16.27 -		 { Abs_Real(realrel``{(x+u, y+v)}) })" ..
   16.28 -lemmas [code func del] = real_add_def
   16.29 +		 { Abs_Real(realrel``{(x+u, y+v)}) })"
   16.30  
   16.31 -instance real :: minus
   16.32 -  real_minus_def: "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   16.33 -  real_diff_def: "r - (s::real) == r + - s" ..
   16.34 -lemmas [code func del] = real_minus_def real_diff_def
   16.35 +definition
   16.36 +  real_minus_def [code func del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   16.37 +
   16.38 +definition
   16.39 +  real_diff_def [code func del]: "r - (s::real) = r + - s"
   16.40  
   16.41 -instance real :: times
   16.42 -  real_mult_def:
   16.43 -    "z * w ==
   16.44 +definition
   16.45 +  real_mult_def [code func del]:
   16.46 +    "z * w =
   16.47         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   16.48 -		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
   16.49 -lemmas [code func del] = real_mult_def
   16.50 +		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
   16.51  
   16.52 -instance real :: inverse
   16.53 -  real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
   16.54 -  real_divide_def: "R / (S::real) == R * inverse S" ..
   16.55 -lemmas [code func del] = real_inverse_def real_divide_def
   16.56 +definition
   16.57 +  real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
   16.58 +
   16.59 +definition
   16.60 +  real_divide_def [code func del]: "R / (S::real) = R * inverse S"
   16.61  
   16.62 -instance real :: ord
   16.63 -  real_le_def: "z \<le> (w::real) == 
   16.64 -    \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
   16.65 -  real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
   16.66 -lemmas [code func del] = real_le_def real_less_def
   16.67 +definition
   16.68 +  real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
   16.69 +    (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
   16.70 +
   16.71 +definition
   16.72 +  real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   16.73  
   16.74 -instance real :: abs
   16.75 -  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
   16.76 +definition
   16.77 +  real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
   16.78  
   16.79 -instance real :: sgn
   16.80 -  real_sgn_def: "sgn (x::real) == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
   16.81 +definition
   16.82 +  real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"
   16.83 +
   16.84 +instance ..
   16.85 +
   16.86 +end
   16.87  
   16.88  subsection {* Equivalence relation over positive reals *}
   16.89  
   16.90 @@ -400,11 +406,20 @@
   16.91  apply (simp add: right_distrib)
   16.92  done
   16.93  
   16.94 -instance real :: distrib_lattice
   16.95 -  "inf \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> min"
   16.96 -  "sup \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> max"
   16.97 +instantiation real :: distrib_lattice
   16.98 +begin
   16.99 +
  16.100 +definition
  16.101 +  "(inf \<Colon> real \<Rightarrow> real \<Rightarrow> real) = min"
  16.102 +
  16.103 +definition
  16.104 +  "(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
  16.105 +
  16.106 +instance
  16.107    by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
  16.108  
  16.109 +end
  16.110 +
  16.111  
  16.112  subsection{*The Reals Form an Ordered Field*}
  16.113  
  16.114 @@ -833,10 +848,17 @@
  16.115  
  16.116  subsection{*Numerals and Arithmetic*}
  16.117  
  16.118 -instance real :: number_ring
  16.119 -  real_number_of_def: "number_of w \<equiv> real_of_int w"
  16.120 +instantiation real :: number_ring
  16.121 +begin
  16.122 +
  16.123 +definition
  16.124 +  real_number_of_def: "number_of w = real_of_int w"
  16.125 +
  16.126 +instance
  16.127    by intro_classes (simp add: real_number_of_def)
  16.128  
  16.129 +end
  16.130 +
  16.131  lemma [code, code unfold]:
  16.132    "number_of k = real_of_int (number_of k)"
  16.133    unfolding number_of_is_id real_number_of_def ..
    17.1 --- a/src/HOL/Real/RealVector.thy	Fri Dec 07 15:07:56 2007 +0100
    17.2 +++ b/src/HOL/Real/RealVector.thy	Fri Dec 07 15:07:59 2007 +0100
    17.3 @@ -54,8 +54,15 @@
    17.4  
    17.5  end
    17.6  
    17.7 -instance real :: scaleR
    17.8 -  real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
    17.9 +instantiation real :: scaleR
   17.10 +begin
   17.11 +
   17.12 +definition
   17.13 +  real_scaleR_def [simp]: "scaleR a x = a * x"
   17.14 +
   17.15 +instance ..
   17.16 +
   17.17 +end
   17.18  
   17.19  class real_vector = scaleR + ab_group_add +
   17.20    assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
   17.21 @@ -371,8 +378,15 @@
   17.22  class norm = type +
   17.23    fixes norm :: "'a \<Rightarrow> real"
   17.24  
   17.25 -instance real :: norm
   17.26 -  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
   17.27 +instantiation real :: norm
   17.28 +begin
   17.29 +
   17.30 +definition
   17.31 +  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
   17.32 +
   17.33 +instance ..
   17.34 +
   17.35 +end
   17.36  
   17.37  class sgn_div_norm = scaleR + norm + sgn +
   17.38    assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"