# HG changeset patch
# User haftmann
# Date 1197036479 -3600
# Node ID c9e39eafc7a0318bb6b2f031d71d6c892c1afe34
# Parent  fdfbbb92dadf7642e3dfc573339290e8cdee6846
instantiation target rather than legacy instance

diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Complex/Complex.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -33,19 +33,24 @@
 
 subsection {* Addition and Subtraction *}
 
-instance complex :: zero
-  complex_zero_def:
-    "0 \<equiv> Complex 0 0" ..
+instantiation complex :: "{zero, plus, minus}"
+begin
+
+definition
+  complex_zero_def: "0 = Complex 0 0"
+
+definition
+  complex_add_def: "x + y = Complex (Re x + Re y) (Im x + Im y)"
 
-instance complex :: plus
-  complex_add_def:
-    "x + y \<equiv> Complex (Re x + Re y) (Im x + Im y)" ..
+definition
+  complex_minus_def: "- x = Complex (- Re x) (- Im x)"
 
-instance complex :: minus
-  complex_minus_def:
-    "- x \<equiv> Complex (- Re x) (- Im x)"
-  complex_diff_def:
-    "x - (y\<Colon>complex) \<equiv> x + - y" ..
+definition
+  complex_diff_def: "x - (y\<Colon>complex) = x + - y"
+
+instance ..
+
+end
 
 lemma Complex_eq_0 [simp]: "(Complex a b = 0) = (a = 0 \<and> b = 0)"
 by (simp add: complex_zero_def)
@@ -103,20 +108,26 @@
 
 subsection {* Multiplication and Division *}
 
-instance complex :: one
-  complex_one_def:
-    "1 \<equiv> Complex 1 0" ..
+instantiation complex :: "{one, times, inverse}"
+begin
+
+definition
+  complex_one_def: "1 = Complex 1 0"
+
+definition
+  complex_mult_def: "x * y =
+    Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)"
 
-instance complex :: times
-  complex_mult_def:
-    "x * y \<equiv> Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)" ..
+definition
+  complex_inverse_def: "inverse x =
+    Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
 
-instance complex :: inverse
-  complex_inverse_def:
-    "inverse x \<equiv>
-     Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
-  complex_divide_def:
-    "x / (y\<Colon>complex) \<equiv> x * inverse y" ..
+definition
+  complex_divide_def: "x / (y\<Colon>complex) = x * inverse y"
+
+instance ..
+
+end
 
 lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
 by (simp add: complex_one_def)
@@ -193,12 +204,16 @@
 
 subsection {* Numerals and Arithmetic *}
 
-instance complex :: number
-  complex_number_of_def:
-    "number_of w \<equiv> of_int w \<Colon> complex" ..
+instantiation complex :: number_ring
+begin
 
-instance complex :: number_ring
-by (intro_classes, simp only: complex_number_of_def)
+definition
+  complex_number_of_def: "number_of w = (of_int w \<Colon> complex)"
+
+instance
+  by (intro_classes, simp only: complex_number_of_def)
+
+end
 
 lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
 by (induct n) simp_all
@@ -225,9 +240,15 @@
 
 subsection {* Scalar Multiplication *}
 
-instance complex :: scaleR
-  complex_scaleR_def:
-    "scaleR r x \<equiv> Complex (r * Re x) (r * Im x)" ..
+instantiation complex :: scaleR
+begin
+
+definition
+  complex_scaleR_def: "scaleR r x = Complex (r * Re x) (r * Im x)"
+
+instance ..
+
+end
 
 lemma complex_scaleR [simp]:
   "scaleR r (Complex a b) = Complex (r * a) (r * b)"
@@ -291,16 +312,29 @@
 
 subsection {* Vector Norm *}
 
-instance complex :: norm
-  complex_norm_def:
-    "norm z \<equiv> sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)" ..
+instantiation complex :: norm
+begin
+
+definition
+  complex_norm_def: "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
+
+instance ..
+
+end
 
 abbreviation
   cmod :: "complex \<Rightarrow> real" where
     "cmod \<equiv> norm"
 
-instance complex :: sgn
-  complex_sgn_def: "sgn x == x /\<^sub>R cmod x" ..
+instantiation complex :: sgn
+begin
+
+definition
+  complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
+
+instance ..
+
+end
 
 lemmas cmod_def = complex_norm_def
 
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Divides.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -15,11 +15,20 @@
   fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
 
-instance nat :: Divides.div
+instantiation nat :: Divides.div
+begin
+
+definition
   div_def: "m div n == wfrec (pred_nat^+)
                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
+
+definition
   mod_def: "m mod n == wfrec (pred_nat^+)
-                          (%f j. if j<n | n=0 then j else f (j-n)) m" ..
+                          (%f j. if j<n | n=0 then j else f (j-n)) m"
+
+instance ..
+
+end
 
 definition (in div)
   dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -2665,32 +2665,48 @@
 lemma univ_unit [noatp]:
   "UNIV = {()}" by auto
 
-instance unit :: finite
-  "Finite_Set.itself \<equiv> TYPE(unit)"
-proof
+instantiation unit :: finite
+begin
+
+definition
+  "itself = TYPE(unit)"
+
+instance proof
   have "finite {()}" by simp
   also note univ_unit [symmetric]
   finally show "finite (UNIV :: unit set)" .
 qed
 
+end
+
 lemmas [code func] = univ_unit
 
 lemma univ_bool [noatp]:
   "UNIV = {False, True}" by auto
 
-instance bool :: finite
-  "itself \<equiv> TYPE(bool)"
-proof
+instantiation bool :: finite
+begin
+
+definition
+  "itself = TYPE(bool)"
+
+instance proof
   have "finite {False, True}" by simp
   also note univ_bool [symmetric]
   finally show "finite (UNIV :: bool set)" .
 qed
 
+end
+
 lemmas [code func] = univ_bool
 
-instance * :: (finite, finite) finite
-  "itself \<equiv> TYPE('a \<times> 'b)"
-proof
+instantiation * :: (finite, finite) finite
+begin
+
+definition
+  "itself = TYPE('a \<times> 'b)"
+
+instance proof
   show "finite (UNIV :: ('a \<times> 'b) set)"
   proof (rule finite_Prod_UNIV)
     show "finite (UNIV :: 'a set)" by (rule finite)
@@ -2698,13 +2714,19 @@
   qed
 qed
 
+end
+
 lemma univ_prod [noatp, code func]:
   "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
   unfolding UNIV_Times_UNIV ..
 
-instance "+" :: (finite, finite) finite
-  "itself \<equiv> TYPE('a + 'b)"
-proof
+instantiation "+" :: (finite, finite) finite
+begin
+
+definition
+  "itself = TYPE('a + 'b)"
+
+instance proof
   have a: "finite (UNIV :: 'a set)" by (rule finite)
   have b: "finite (UNIV :: 'b set)" by (rule finite)
   from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
@@ -2712,28 +2734,40 @@
   thus "finite (UNIV :: ('a + 'b) set)" by simp
 qed
 
+end
+
 lemma univ_sum [noatp, code func]:
   "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
   unfolding UNIV_Plus_UNIV ..
 
-instance set :: (finite) finite
-  "itself \<equiv> TYPE('a set)"
-proof
+instantiation set :: (finite) finite
+begin
+
+definition
+  "itself = TYPE('a set)"
+
+instance proof
   have "finite (UNIV :: 'a set)" by (rule finite)
   hence "finite (Pow (UNIV :: 'a set))"
     by (rule finite_Pow_iff [THEN iffD2])
   thus "finite (UNIV :: 'a set set)" by simp
 qed
 
+end
+
 lemma univ_set [noatp, code func]:
   "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
 
 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
 
-instance "fun" :: (finite, finite) finite
+instantiation "fun" :: (finite, finite) finite
+begin
+
+definition
   "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
-proof
+
+instance proof
   show "finite (UNIV :: ('a => 'b) set)"
   proof (rule finite_imageD)
     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
@@ -2742,6 +2776,8 @@
   qed
 qed
 
+end
+
 hide (open) const itself
 
 subsection {* Equality and order on functions *}
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -11,45 +11,137 @@
 
 subsection {* Syntactic classes *}
 
-instance star :: (zero) zero
-  star_zero_def:    "0 \<equiv> star_of 0" ..
+instantiation star :: (zero) zero
+begin
+
+definition
+  star_zero_def:    "0 \<equiv> star_of 0"
+
+instance ..
+
+end
+
+instantiation star :: (one) one
+begin
+
+definition
+  star_one_def:     "1 \<equiv> star_of 1"
 
-instance star :: (one) one
-  star_one_def:     "1 \<equiv> star_of 1" ..
+instance ..
+
+end
+
+instantiation star :: (plus) plus
+begin
 
-instance star :: (plus) plus
-  star_add_def:     "(op +) \<equiv> *f2* (op +)" ..
+definition
+  star_add_def:     "(op +) \<equiv> *f2* (op +)"
+
+instance ..
+
+end
+
+instantiation star :: (times) times
+begin
 
-instance star :: (times) times
-  star_mult_def:    "(op *) \<equiv> *f2* (op *)" ..
+definition
+  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
+
+instance ..
 
-instance star :: (minus) minus
+end
+
+instantiation star :: (minus) minus
+begin
+
+definition
   star_minus_def:   "uminus \<equiv> *f* uminus"
-  star_diff_def:    "(op -) \<equiv> *f2* (op -)" ..
+
+definition
+  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
+
+instance ..
+
+end
 
-instance star :: (abs) abs
-  star_abs_def:     "abs \<equiv> *f* abs" ..
+instantiation star :: (abs) abs
+begin
+
+definition
+  star_abs_def:     "abs \<equiv> *f* abs"
+
+instance ..
+
+end
+
+instantiation star :: (sgn) sgn
+begin
 
-instance star :: (sgn) sgn
-  star_sgn_def:     "sgn \<equiv> *f* sgn" ..
+definition
+  star_sgn_def:     "sgn \<equiv> *f* sgn"
+
+instance ..
 
-instance star :: (inverse) inverse
+end
+
+instantiation star :: (inverse) inverse
+begin
+
+definition
   star_divide_def:  "(op /) \<equiv> *f2* (op /)"
-  star_inverse_def: "inverse \<equiv> *f* inverse" ..
+
+definition
+  star_inverse_def: "inverse \<equiv> *f* inverse"
+
+instance ..
+
+end
 
-instance star :: (number) number
-  star_number_def:  "number_of b \<equiv> star_of (number_of b)" ..
+instantiation star :: (number) number
+begin
+
+definition
+  star_number_def:  "number_of b \<equiv> star_of (number_of b)"
+
+instance ..
+
+end
+
+instantiation star :: (Divides.div) Divides.div
+begin
 
-instance star :: (Divides.div) Divides.div
+definition
   star_div_def:     "(op div) \<equiv> *f2* (op div)"
-  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)" ..
+
+definition
+  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
+
+instance ..
+
+end
+
+instantiation star :: (power) power
+begin
+
+definition
+  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
 
-instance star :: (power) power
-  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
+instance ..
+
+end
+
+instantiation star :: (ord) ord
+begin
 
-instance star :: (ord) ord
+definition
   star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
-  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
+
+definition
+  star_less_def:    "(op <) \<equiv> *p2* (op <)"
+
+instance ..
+
+end
 
 lemmas star_class_defs [transfer_unfold] =
   star_zero_def     star_one_def      star_number_def
@@ -220,14 +312,28 @@
 apply (transfer, erule (1) order_antisym)
 done
 
-instance star :: (lower_semilattice) lower_semilattice
+instantiation star :: (lower_semilattice) lower_semilattice
+begin
+
+definition
   star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
+
+instance
   by default (transfer star_inf_def, auto)+
 
-instance star :: (upper_semilattice) upper_semilattice
+end
+
+instantiation star :: (upper_semilattice) upper_semilattice
+begin
+
+definition
   star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
+
+instance
   by default (transfer star_sup_def, auto)+
 
+end
+
 instance star :: (lattice) lattice ..
 
 instance star :: (distrib_lattice) distrib_lattice
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/IntDef.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -22,34 +22,48 @@
   int = "UNIV//intrel"
   by (auto simp add: quotient_def)
 
-instance int :: zero
-  Zero_int_def: "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" ..
+instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}"
+begin
+
+definition
+  Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
+
+definition
+  One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
 
-instance int :: one
-  One_int_def: "1 \<equiv> Abs_Integ (intrel `` {(1, 0)})" ..
+definition
+  add_int_def [code func del]: "z + w = Abs_Integ
+    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
+      intrel `` {(x + u, y + v)})"
 
-instance int :: plus
-  add_int_def: "z + w \<equiv> Abs_Integ
-    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
-      intrel `` {(x + u, y + v)})" ..
+definition
+  minus_int_def [code func del]:
+    "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
+
+definition
+  diff_int_def [code func del]:  "z - w = z + (-w \<Colon> int)"
 
-instance int :: minus
-  minus_int_def:
-    "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
-  diff_int_def:  "z - w \<equiv> z + (-w \<Colon> int)" ..
-
-instance int :: times
-  mult_int_def: "z * w \<equiv>  Abs_Integ
+definition
+  mult_int_def [code func del]: "z * w = Abs_Integ
     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
-      intrel `` {(x*u + y*v, x*v + y*u)})" ..
+      intrel `` {(x*u + y*v, x*v + y*u)})"
+
+definition
+  le_int_def [code func del]:
+   "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)"
+
+definition
+  less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
 
-instance int :: ord
-  le_int_def:
-   "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"
-  less_int_def: "(z\<Colon>int) < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
+definition
+  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
 
-lemmas [code func del] = Zero_int_def One_int_def add_int_def
-  minus_int_def mult_int_def le_int_def less_int_def
+definition
+  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+
+instance ..
+
+end
 
 
 subsection{*Construction of the Integers*}
@@ -212,17 +226,21 @@
 apply (auto simp add: zmult_zless_mono2_lemma)
 done
 
-instance int :: abs
-  zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
-instance int :: sgn
-  zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
+instantiation int :: distrib_lattice
+begin
 
-instance int :: distrib_lattice
-  "inf \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> min"
-  "sup \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> max"
+definition
+  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
   by intro_classes
     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
 
+end
+
 text{*The integers form an ordered integral domain*}
 instance int :: ordered_idom
 proof
@@ -744,7 +762,7 @@
 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
-lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
+lemmas zless_le = less_int_def
 lemmas int_eq_of_nat = TrueI
 
 abbreviation
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/IntDiv.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -62,9 +62,18 @@
                   if 0<b then negDivAlg a b
                   else negateSnd (posDivAlg (-a) (-b))))"
 
-instance int :: Divides.div
-  div_def: "a div b == fst (divAlg (a, b))"
-  mod_def: "a mod b == snd (divAlg (a, b))" ..
+instantiation int :: Divides.div
+begin
+
+definition
+  div_def: "a div b = fst (divAlg (a, b))"
+
+definition
+  mod_def: "a mod b = snd (divAlg (a, b))"
+
+instance ..
+
+end
 
 lemma divAlg_mod_div:
   "divAlg (p, q) = (p div q, p mod q)"
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -49,11 +49,24 @@
   set_of :: "'a multiset => 'a set" where
   "set_of M = {x. x :# M}"
 
-instance multiset :: (type) "{plus, minus, zero, size}" 
+instantiation multiset :: (type) "{plus, minus, zero, size}" 
+begin
+
+definition
   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
+
+definition
   diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
+
+definition
   Zero_multiset_def [simp]: "0 == {#}"
-  size_def: "size M == setsum (count M) (set_of M)" ..
+
+definition
+  size_def: "size M == setsum (count M) (set_of M)"
+
+instance ..
+
+end
 
 definition
   multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"  (infixl "#\<inter>" 70) where
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Library/Parity.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -16,11 +16,18 @@
   odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
   "odd x \<equiv> \<not> even x"
 
-instance int :: even_odd
-  even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" ..
+instantiation int and nat :: even_odd
+begin
+
+definition
+  even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0"
 
-instance nat :: even_odd
-  even_nat_def[presburger]: "even x \<equiv> even (int x)" ..
+definition
+  even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)"
+
+instance ..
+
+end
 
 
 subsection {* Even and odd are mutually exclusive *}
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -9,9 +9,18 @@
 imports Main
 begin
 
-instance "*" :: (ord, ord) ord
+instantiation "*" :: (ord, ord) ord
+begin
+
+definition
   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"
-  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" ..
+
+definition
+  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+
+instance ..
+
+end
 
 lemma [code func]:
   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
@@ -29,10 +38,19 @@
 instance * :: (linorder, linorder) linorder
   by default (auto simp: prod_le_def)
 
-instance * :: (linorder, linorder) distrib_lattice
+instantiation * :: (linorder, linorder) distrib_lattice
+begin
+
+definition
   inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+
+definition
   sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
+
+instance
   by intro_classes
     (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
 
 end
+
+end
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/List.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -109,7 +109,6 @@
 where
   append_Nil:"[] @ ys = ys"
   | append_Cons: "(x#xs) @ ys = x # xs @ ys"
-declare append.simps [code]
 
 primrec
   "rev([]) = []"
@@ -2691,9 +2690,16 @@
 
 text{* The integers are an instance of the above class: *}
 
-instance int:: finite_intvl_succ
-  successor_int_def: "successor == (%i\<Colon>int. i+1)"
-by intro_classes (simp_all add: successor_int_def)
+instantiation int:: finite_intvl_succ
+begin
+
+definition
+  successor_int_def: "successor = (%i\<Colon>int. i+1)"
+
+instance
+  by intro_classes (simp_all add: successor_int_def)
+
+end
 
 text{* Now @{term"[i..j::int]"} is defined for integers. *}
 
@@ -3178,7 +3184,6 @@
 where 
   "x mem [] \<longleftrightarrow> False"
   | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
-declare member.simps [code]
 
 primrec
   "null [] = True"
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Nat.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -139,20 +139,30 @@
 
 subsection {* Arithmetic operators *}
 
-instance nat :: "{one, plus, minus, times}"
-  One_nat_def [simp]: "1 == Suc 0" ..
+instantiation nat :: "{one, plus, minus, times}"
+begin
 
-primrec
-  add_0:    "0 + n = n"
-  add_Suc:  "Suc m + n = Suc (m + n)"
+definition
+  One_nat_def [simp]: "1 = Suc 0"
+
+primrec plus_nat
+where
+  add_0:      "0 + n = (n\<Colon>nat)"
+  | add_Suc:  "Suc m + n = Suc (m + n)"
 
-primrec
-  diff_0:   "m - 0 = m"
-  diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+primrec minus_nat
+where
+  diff_0:     "m - 0 = (m\<Colon>nat)"
+  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
 
-primrec
-  mult_0:   "0 * n = 0"
-  mult_Suc: "Suc m * n = n + (m * n)"
+primrec times_nat
+where
+  mult_0:     "0 * n = (0\<Colon>nat)"
+  | mult_Suc: "Suc m * n = n + (m * n)"
+
+instance ..
+
+end
 
 
 subsection {* Orders on @{typ nat} *}
@@ -341,9 +351,6 @@
   apply (blast dest: Suc_lessD)
   done
 
-lemma [code]: "((n::nat) < 0) = False" by simp
-lemma [code]: "(0 < Suc n) = True" by simp
-
 text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
 lemma not_less_eq: "(~ m < n) = (n < Suc m)"
 by (induct m n rule: diff_induct) simp_all
@@ -621,6 +628,13 @@
 
 declare diff_Suc [simp del, code del]
 
+lemma [code]:
+  "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
+  "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
+  "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
+  "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
+  using Suc_le_eq less_Suc_eq_le by simp_all
+
 
 subsection {* Addition *}
 
@@ -1141,16 +1155,6 @@
 declare "*.size" [noatp]
 
 
-subsection {* Code generator setup *}
-
-lemma [code func]:
-  "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
-  "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
-  "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
-  "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
-  using Suc_le_eq less_Suc_eq_le by simp_all
-
-
 subsection {* Embedding of the Naturals into any
   @{text semiring_1}: @{term of_nat} *}
 
@@ -1162,7 +1166,6 @@
 where
   of_nat_0:     "of_nat 0 = 0"
   | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
-declare of_nat.simps [code]
 
 lemma of_nat_1 [simp]: "of_nat 1 = 1"
   by simp
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/NatBin.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -14,8 +14,15 @@
   Arithmetic for naturals is reduced to that for the non-negative integers.
 *}
 
-instance nat :: number
-  nat_number_of_def [code inline]: "number_of v == nat (number_of (v\<Colon>int))" ..
+instantiation nat :: number
+begin
+
+definition
+  nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
+
+instance ..
+
+end
 
 abbreviation (xsymbols)
   square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Numeral.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -210,11 +210,16 @@
 
 text {* self-embedding of the integers *}
 
-instance int :: number_ring
-  int_number_of_def: "number_of w \<equiv> of_int w \<Colon> int"
+instantiation int :: number_ring
+begin
+
+definition
+  int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
+
+instance
   by intro_classes (simp only: int_number_of_def)
 
-lemmas [code func del] = int_number_of_def
+end
 
 lemma number_of_is_id:
   "number_of (k::int) = k"
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -211,12 +211,20 @@
 instance preal :: linorder
   by intro_classes (rule preal_le_linear)
 
-instance preal :: distrib_lattice
-  "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
-  "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal  \<equiv> max"
+instantiation preal :: distrib_lattice
+begin
+
+definition
+  "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
+
+definition
+  "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
+
+instance
   by intro_classes
     (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
 
+end
 
 subsection{*Properties of Addition*}
 
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/Rational.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -163,60 +163,72 @@
 
 subsubsection {* Standard operations on rational numbers *}
 
-instance rat :: zero
-  Zero_rat_def: "0 == Fract 0 1" ..
-lemmas [code func del] = Zero_rat_def
+instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+begin
+
+definition
+  Zero_rat_def [code func del]: "0 = Fract 0 1"
 
-instance rat :: one
-  One_rat_def: "1 == Fract 1 1" ..
-lemmas [code func del] = One_rat_def
+definition
+  One_rat_def [code func del]: "1 = Fract 1 1"
 
-instance rat :: plus
-  add_rat_def:
-   "q + r ==
+definition
+  add_rat_def [code func del]:
+   "q + r =
        Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
-           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})" ..
-lemmas [code func del] = add_rat_def
+           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})"
 
-instance rat :: minus
-  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 diff_rat_def
+definition
+  minus_rat_def [code func del]:
+    "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
+
+definition
+  diff_rat_def [code func del]: "q - r = q + - (r::rat)"
 
-instance rat :: times
-  mult_rat_def:
-   "q * r ==
+definition
+  mult_rat_def [code func del]:
+   "q * r =
        Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
-           ratrel``{(fst x * fst y, snd x * snd y)})" ..
-lemmas [code func del] = mult_rat_def
+           ratrel``{(fst x * fst y, snd x * snd y)})"
 
-instance rat :: inverse
-  inverse_rat_def:
-    "inverse q ==
+definition
+  inverse_rat_def [code func del]:
+    "inverse q =
         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 divide_rat_def
+
+definition
+  divide_rat_def [code func del]: "q / r = q * inverse (r::rat)"
 
-instance rat :: ord
-  le_rat_def:
-   "q \<le> r == contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
+definition
+  le_rat_def [code func del]:
+   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
       {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
-  less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)" ..
-lemmas [code func del] = le_rat_def less_rat_def
+
+definition
+  less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+
+definition
+  abs_rat_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
 
-instance rat :: abs
-  abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
+definition
+  sgn_rat_def: "sgn (q::rat) = (if q=0 then 0 else if 0<q then 1 else - 1)"
 
-instance rat :: sgn
-  sgn_rat_def: "sgn(q::rat) == (if q=0 then 0 else if 0<q then 1 else - 1)" ..
+instance ..
+
+end
 
-instance rat :: power ..
+instantiation rat :: power
+begin
 
-primrec (rat)
-  rat_power_0:   "q ^ 0       = 1"
-  rat_power_Suc: "q ^ (Suc n) = (q::rat) * (q ^ n)"
+primrec power_rat
+where
+  rat_power_0:     "q ^ 0       = (1\<Colon>rat)"
+  | rat_power_Suc: "q ^ (Suc n) = (q\<Colon>rat) * (q ^ n)"
+
+instance ..
+
+end
 
 theorem eq_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   (Fract a b = Fract c d) = (a * d = c * b)"
@@ -361,11 +373,20 @@
   }
 qed
 
-instance rat :: distrib_lattice
-  "inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> min"
-  "sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> max"
+instantiation rat :: distrib_lattice
+begin
+
+definition
+  "(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min"
+
+definition
+  "(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max"
+
+instance
   by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
 
+end
+
 instance rat :: ordered_field
 proof
   fix q r s :: rat
@@ -474,11 +495,16 @@
 
 subsection {* Numerals and Arithmetic *}
 
-instance rat :: number
-  rat_number_of_def: "(number_of w :: rat) \<equiv> of_int w" ..
+instantiation rat :: number_ring
+begin
 
-instance rat :: number_ring
-  by default (simp add: rat_number_of_def) 
+definition
+  rat_number_of_def: "number_of w = (of_int w \<Colon> rat)"
+
+instance
+  by default (simp add: rat_number_of_def)
+
+end 
 
 use "rat_arith.ML"
 declaration {* K rat_arith_setup *}
@@ -488,7 +514,7 @@
 
 class field_char_0 = field + ring_char_0
 
-instance ordered_field < field_char_0 ..
+instance ordered_field < field_char_0 .. 
 
 definition
   of_rat :: "rat \<Rightarrow> 'a::field_char_0"
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/RealDef.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -25,48 +25,54 @@
   real_of_preal :: "preal => real" where
   "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
 
-instance real :: zero
-  real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
-lemmas [code func del] = real_zero_def
+instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+begin
 
-instance real :: one
-  real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
-lemmas [code func del] = real_one_def
+definition
+  real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
+
+definition
+  real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
 
-instance real :: plus
-  real_add_def: "z + w ==
+definition
+  real_add_def [code func del]: "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
+		 { Abs_Real(realrel``{(x+u, y+v)}) })"
 
-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
+definition
+  real_minus_def [code func del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+
+definition
+  real_diff_def [code func del]: "r - (s::real) = r + - s"
 
-instance real :: times
-  real_mult_def:
-    "z * w ==
+definition
+  real_mult_def [code func del]:
+    "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
+		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
 
-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
+definition
+  real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
+
+definition
+  real_divide_def [code func del]: "R / (S::real) = R * inverse S"
 
-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
+definition
+  real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
+    (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
+
+definition
+  real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
 
-instance real :: abs
-  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
+definition
+  real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
 
-instance real :: sgn
-  real_sgn_def: "sgn (x::real) == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
+definition
+  real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"
+
+instance ..
+
+end
 
 subsection {* Equivalence relation over positive reals *}
 
@@ -400,11 +406,20 @@
 apply (simp add: right_distrib)
 done
 
-instance real :: distrib_lattice
-  "inf \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> min"
-  "sup \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> max"
+instantiation real :: distrib_lattice
+begin
+
+definition
+  "(inf \<Colon> real \<Rightarrow> real \<Rightarrow> real) = min"
+
+definition
+  "(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
+
+instance
   by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
 
+end
+
 
 subsection{*The Reals Form an Ordered Field*}
 
@@ -833,10 +848,17 @@
 
 subsection{*Numerals and Arithmetic*}
 
-instance real :: number_ring
-  real_number_of_def: "number_of w \<equiv> real_of_int w"
+instantiation real :: number_ring
+begin
+
+definition
+  real_number_of_def: "number_of w = real_of_int w"
+
+instance
   by intro_classes (simp add: real_number_of_def)
 
+end
+
 lemma [code, code unfold]:
   "number_of k = real_of_int (number_of k)"
   unfolding number_of_is_id real_number_of_def ..
diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/RealVector.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -54,8 +54,15 @@
 
 end
 
-instance real :: scaleR
-  real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
+instantiation real :: scaleR
+begin
+
+definition
+  real_scaleR_def [simp]: "scaleR a x = a * x"
+
+instance ..
+
+end
 
 class real_vector = scaleR + ab_group_add +
   assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
@@ -371,8 +378,15 @@
 class norm = type +
   fixes norm :: "'a \<Rightarrow> real"
 
-instance real :: norm
-  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
+instantiation real :: norm
+begin
+
+definition
+  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
+
+instance ..
+
+end
 
 class sgn_div_norm = scaleR + norm + sgn +
   assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"