# HG changeset patch
# User wenzelm
# Date 1083441717 -7200
# Node ID e1eedc8cad37fa3974482bcbe865dd3388470d7e
# Parent  f61ea8bfa81ed3353a799624a705fce75111f50a
tuned instance statements;

diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Complex/Complex.thy	Sat May 01 22:01:57 2004 +0200
@@ -11,13 +11,7 @@
 
 datatype complex = Complex real real
 
-instance complex :: zero ..
-instance complex :: one ..
-instance complex :: plus ..
-instance complex :: times ..
-instance complex :: minus ..
-instance complex :: inverse ..
-instance complex :: power ..
+instance complex :: "{zero, one, plus, times, minus, inverse, power}" ..
 
 consts
   "ii"    :: complex    ("\<i>")
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Sat May 01 22:01:57 2004 +0200
@@ -17,13 +17,7 @@
 typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
   by (auto simp add: quotient_def)
 
-instance hcomplex :: zero ..
-instance hcomplex :: one ..
-instance hcomplex :: plus ..
-instance hcomplex :: times ..
-instance hcomplex :: minus ..
-instance hcomplex :: inverse ..
-instance hcomplex :: power ..
+instance hcomplex :: "{zero, one, plus, times, minus, inverse, power}" ..
 
 defs (overloaded)
   hcomplex_zero_def:
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Sat May 01 22:01:57 2004 +0200
@@ -23,14 +23,7 @@
 typedef hypreal = "UNIV//hyprel" 
     by (auto simp add: quotient_def) 
 
-instance hypreal :: ord ..
-instance hypreal :: zero ..
-instance hypreal :: one ..
-instance hypreal :: plus ..
-instance hypreal :: times ..
-instance hypreal :: minus ..
-instance hypreal :: inverse ..
-
+instance hypreal :: "{ord, zero, one, plus, times, minus, inverse}" ..
 
 defs (overloaded)
 
@@ -58,10 +51,10 @@
   hypreal_of_real  :: "real => hypreal"
   "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
 
-  omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
+  omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
   "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
 
-  epsilon :: hypreal   (*an infinitesimal number = [<1,1/2,1/3,...>] *)
+  epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
   "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
 
 syntax (xsymbols)
@@ -341,9 +334,9 @@
 by (cases z, simp add: hypreal_zero_def hypreal_add)
 
 instance hypreal :: plus_ac0
-  by (intro_classes,
-      (assumption | 
-       rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+)
+  by intro_classes
+    (assumption | 
+      rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+
 
 lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
 by (simp add: hypreal_add_zero_left hypreal_add_commute)
@@ -502,9 +495,9 @@
 by (simp add: hypreal_less_def)
 
 instance hypreal :: order
-proof qed
- (assumption |
-  rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
+  by intro_classes
+    (assumption |
+      rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
 
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
@@ -514,7 +507,7 @@
 done
 
 instance hypreal :: linorder 
-  by (intro_classes, rule hypreal_le_linear)
+  by intro_classes (rule hypreal_le_linear)
 
 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
 by (auto simp add: order_less_irrefl)
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Sat May 01 22:01:57 2004 +0200
@@ -17,12 +17,7 @@
 typedef hypnat = "UNIV//hypnatrel"
     by (auto simp add: quotient_def)
 
-instance hypnat :: ord ..
-instance hypnat :: zero ..
-instance hypnat :: one ..
-instance hypnat :: plus ..
-instance hypnat :: times ..
-instance hypnat :: minus ..
+instance hypnat :: "{ord, zero, one, plus, times, minus}" ..
 
 consts whn :: hypnat
 
@@ -164,9 +159,9 @@
 done
 
 instance hypnat :: plus_ac0
-  by (intro_classes,
-      (assumption |
-       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
+  by intro_classes
+    (assumption |
+      rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
 
 
 subsection{*Subtraction inverse on @{typ hypreal}*}
@@ -332,9 +327,9 @@
 by (simp add: hypnat_less_def)
 
 instance hypnat :: order
-proof qed
- (assumption |
-  rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
+  by intro_classes
+    (assumption |
+      rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
@@ -343,7 +338,7 @@
 done
 
 instance hypnat :: linorder
-  by (intro_classes, rule hypnat_le_linear)
+  by intro_classes (rule hypnat_le_linear)
 
 lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
 apply (cases x, cases y, cases z)
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Sat May 01 22:01:57 2004 +0200
@@ -18,15 +18,9 @@
   int = "UNIV//intrel"
     by (auto simp add: quotient_def)
 
-instance int :: ord ..
-instance int :: zero ..
-instance int :: one ..
-instance int :: plus ..
-instance int :: times ..
-instance int :: minus ..
+instance int :: "{ord, zero, one, plus, times, minus}" ..
 
 constdefs
-
   int :: "nat => int"
   "int m == Abs_Integ(intrel `` {(m,0)})"
 
@@ -279,16 +273,16 @@
 by (simp add: less_int_def)
 
 instance int :: order
-proof qed
- (assumption |
-  rule zle_refl zle_trans zle_anti_sym zless_le)+
+  by intro_classes
+    (assumption |
+      rule zle_refl zle_trans zle_anti_sym zless_le)+
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma zle_linear: "(z::int) \<le> w | w \<le> z"
-by (cases z, cases w, simp add: le linorder_linear)
+by (cases z, cases w) (simp add: le linorder_linear)
 
 instance int :: linorder
-proof qed (rule zle_linear)
+  by intro_classes (rule zle_linear)
 
 
 lemmas zless_linear = linorder_less_linear [where 'a = int]
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat May 01 22:01:57 2004 +0200
@@ -46,9 +46,7 @@
   set_of :: "'a multiset => 'a set"
   "set_of M == {x. x :# M}"
 
-instance multiset :: (type) plus ..
-instance multiset :: (type) minus ..
-instance multiset :: (type) zero ..
+instance multiset :: (type) "{plus, minus, zero}" ..
 
 defs (overloaded)
   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Sat May 01 22:01:57 2004 +0200
@@ -21,8 +21,7 @@
 
 datatype inat = Fin nat | Infty
 
-instance inat :: ord ..
-instance inat :: zero ..
+instance inat :: "{ord, zero}" ..
 
 consts
   iSuc :: "inat => inat"
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Sat May 01 22:01:57 2004 +0200
@@ -20,11 +20,8 @@
 axclass matrix_element < almost_matrix_element
 matrix_add_0[simp]: "0+0 = 0"
 
-instance matrix :: (plus) plus
-by (intro_classes)
-
-instance matrix :: (times) times
-by (intro_classes)
+instance matrix :: (plus) plus ..
+instance matrix :: (times) times ..
 
 defs (overloaded)
 plus_matrix_def: "A + B == combine_matrix (op +) A B"
@@ -127,7 +124,7 @@
 g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
 
 instance g_almost_semiring < matrix_element
-by (intro_classes, simp)
+  by intro_classes simp
 
 instance semiring < g_semiring
 apply (intro_classes)
@@ -197,8 +194,7 @@
 apply (intro_classes)
 by (simp_all add: add_right_mono mult_right_mono mult_left_mono)
 
-instance matrix :: (pordered_g_semiring) pordered_g_semiring
-by (intro_classes)
+instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
 
 lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
 by (simp add: times_matrix_def mult_nrows)
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Sat May 01 22:01:57 2004 +0200
@@ -746,7 +746,7 @@
 qed
 
 
-instance matrix :: (zero)zero by intro_classes
+instance matrix :: (zero) zero ..
 
 defs(overloaded)
   zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"
@@ -1183,7 +1183,7 @@
   apply (rule ext)+
   by (simp! add: Rep_mult_matrix max_ac)
 
-instance matrix :: ("{ord,zero}") ord by intro_classes
+instance matrix :: ("{ord, zero}") ord ..
 
 defs (overloaded)
   le_matrix_def: "(A::('a::{ord,zero}) matrix) <= B == ! j i. (Rep_matrix A j i) <= (Rep_matrix B j i)"
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Nat.thy	Sat May 01 22:01:57 2004 +0200
@@ -41,9 +41,7 @@
 typedef (open Nat)
   nat = Nat by (rule exI, rule Nat.Zero_RepI)
 
-instance nat :: ord ..
-instance nat :: zero ..
-instance nat :: one ..
+instance nat :: "{ord, zero, one}" ..
 
 
 text {* Abstract constants and syntax *}
@@ -462,16 +460,14 @@
 
 text {* Type {@typ nat} is a wellfounded linear order *}
 
-instance nat :: order by (intro_classes,
-  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
-instance nat :: linorder by (intro_classes, rule nat_le_linear)
-instance nat :: wellorder by (intro_classes, rule wf_less)
-
+instance nat :: "{order, linorder, wellorder}"
+  by intro_classes
+    (assumption |
+      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
 
 lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   by (blast elim!: less_SucE)
 
-
 text {*
   Rewrite @{term "n < Suc m"} to @{term "n = m"}
   if @{term "~ n < m"} or @{term "m \<le> n"} hold.
@@ -506,10 +502,7 @@
 
 text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
 
-instance nat :: plus ..
-instance nat :: minus ..
-instance nat :: times ..
-instance nat :: power ..
+instance nat :: "{plus, minus, times, power}" ..
 
 text {* size of a datatype value; overloaded *}
 consts size :: "'a => nat"
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Real/PReal.thy	Sat May 01 22:01:57 2004 +0200
@@ -50,12 +50,7 @@
 typedef preal = "{A. cut A}"
   by (blast intro: cut_of_rat [OF zero_less_one])
 
-instance preal :: ord ..
-instance preal :: plus ..
-instance preal :: minus ..
-instance preal :: times ..
-instance preal :: inverse ..
-
+instance preal :: "{ord, plus, minus, times, inverse}" ..
 
 constdefs
   preal_of_rat :: "rat => preal"
@@ -211,9 +206,9 @@
 by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
 
 instance preal :: order
-proof qed
- (assumption |
-  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
+  by intro_classes
+    (assumption |
+      rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
 
 lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
 by (insert preal_imp_psubset_positives, blast)
@@ -226,7 +221,7 @@
 done
 
 instance preal :: linorder
-  by (intro_classes, rule preal_le_linear)
+  by intro_classes (rule preal_le_linear)
 
 
 
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Real/Rational.thy	Sat May 01 22:01:57 2004 +0200
@@ -4,10 +4,7 @@
     License: GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {*
-  \title{Rational numbers}
-  \author{Markus Wenzel}
-*}
+header {* Rational numbers *}
 
 theory Rational = Quotient + Main
 files ("rat_arith.ML"):
@@ -117,13 +114,7 @@
  to equivalence of fractions.
 *}
 
-instance fraction :: zero ..
-instance fraction :: one ..
-instance fraction :: plus ..
-instance fraction :: minus ..
-instance fraction :: times ..
-instance fraction :: inverse ..
-instance fraction :: ord ..
+instance fraction :: "{zero, one, plus, minus, times, inverse, ord}" ..
 
 defs (overloaded)
   zero_fraction_def: "0 == fract 0 1"
@@ -354,13 +345,7 @@
 
 subsubsection {* Standard operations on rational numbers *}
 
-instance rat :: zero ..
-instance rat :: one ..
-instance rat :: plus ..
-instance rat :: minus ..
-instance rat :: times ..
-instance rat :: inverse ..
-instance rat :: ord ..
+instance rat :: "{zero, one, plus, minus, times, inverse, ord}" ..
 
 defs (overloaded)
   zero_rat_def: "0 == rat_of 0"
@@ -369,7 +354,7 @@
   minus_rat_def: "-q == rat_of (-(fraction_of q))"
   diff_rat_def: "q - r == q + (-(r::rat))"
   mult_rat_def: "q * r == rat_of (fraction_of q * fraction_of r)"
-  inverse_rat_def: "inverse q == 
+  inverse_rat_def: "inverse q ==
                     if q=0 then 0 else rat_of (inverse (fraction_of q))"
   divide_rat_def: "q / r == q * inverse (r::rat)"
   le_rat_def: "q \<le> r == fraction_of q \<le> fraction_of r"
@@ -377,7 +362,7 @@
   abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
 
 theorem zero_rat: "0 = Fract 0 1"
-  by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)        
+  by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)
 
 theorem one_rat: "1 = Fract 1 1"
   by (simp add: one_rat_def one_fraction_def rat_of_def Fract_def)
@@ -470,14 +455,14 @@
 
 theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
-     (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less 
+     (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
                 split: abs_split)
 
 
 subsubsection {* The ordered field of rational numbers *}
 
 lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
-  by (induct q, induct r, induct s) 
+  by (induct q, induct r, induct s)
      (simp add: add_rat add_ac mult_ac int_distrib)
 
 lemma rat_add_0: "0 + q = (q::rat)"
@@ -507,14 +492,14 @@
   show "1 * q = q"
     by (induct q) (simp add: one_rat mult_rat)
   show "(q + r) * s = q * s + r * s"
-    by (induct q, induct r, induct s) 
+    by (induct q, induct r, induct s)
        (simp add: add_rat mult_rat eq_rat int_distrib)
   show "q \<noteq> 0 ==> inverse q * q = 1"
     by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
   show "q / r = q * inverse r"
-    by (simp add: divide_rat_def) 
+    by (simp add: divide_rat_def)
   show "0 \<noteq> (1::rat)"
-    by (simp add: zero_rat one_rat eq_rat) 
+    by (simp add: zero_rat one_rat eq_rat)
 qed
 
 instance rat :: linorder
@@ -638,7 +623,7 @@
 subsection {* Various Other Results *}
 
 lemma minus_rat_cancel [simp]: "b \<noteq> 0 ==> Fract (-a) (-b) = Fract a b"
-by (simp add: Fract_equality eq_fraction_iff) 
+by (simp add: Fract_equality eq_fraction_iff)
 
 theorem Rat_induct_pos [case_names Fract, induct type: rat]:
   assumes step: "!!a b. 0 < b ==> P (Fract a b)"
@@ -658,44 +643,43 @@
 
 lemma zero_less_Fract_iff:
      "0 < b ==> (0 < Fract a b) = (0 < a)"
-by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff) 
+by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
 
 lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
 apply (insert add_rat [of concl: m n 1 1])
-apply (simp add: one_rat  [symmetric]) 
+apply (simp add: one_rat  [symmetric])
 done
 
 lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
-apply (induct k) 
-apply (simp add: zero_rat) 
-apply (simp add: Fract_add_one) 
+apply (induct k)
+apply (simp add: zero_rat)
+apply (simp add: Fract_add_one)
 done
 
 lemma Fract_of_int_eq: "Fract k 1 = of_int k"
-proof (cases k rule: int_cases) 
+proof (cases k rule: int_cases)
   case (nonneg n)
     thus ?thesis by (simp add: int_eq_of_nat Fract_of_nat_eq)
-next 
+next
   case (neg n)
     hence "Fract k 1 = - (Fract (of_nat (Suc n)) 1)"
-      by (simp only: minus_rat int_eq_of_nat) 
+      by (simp only: minus_rat int_eq_of_nat)
     also have "... =  - (of_nat (Suc n))"
       by (simp only: Fract_of_nat_eq)
-    finally show ?thesis 
-      by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq) 
-qed 
+    finally show ?thesis
+      by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq)
+qed
 
 
-
-subsection{*Numerals and Arithmetic*}
+subsection {* Numerals and Arithmetic *}
 
 instance rat :: number ..
 
-primrec (*the type constraint is essential!*)
+primrec  -- {* the type constraint is essential! *}
   number_of_Pls: "number_of bin.Pls = 0"
   number_of_Min: "number_of bin.Min = - (1::rat)"
   number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
+                                       (number_of w) + (number_of w)"
 
 declare number_of_Pls [simp del]
         number_of_Min [simp del]
diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Sat May 01 22:01:57 2004 +0200
@@ -17,13 +17,7 @@
 typedef (Real)  real = "UNIV//realrel"
   by (auto simp add: quotient_def)
 
-instance real :: ord ..
-instance real :: zero ..
-instance real :: one ..
-instance real :: plus ..
-instance real :: times ..
-instance real :: minus ..
-instance real :: inverse ..
+instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
 
 constdefs
 
@@ -41,6 +35,9 @@
    (*overloaded constant for injecting other types into "real"*)
    real :: "'a => real"
 
+syntax (xsymbols)
+  Reals     :: "'a set"                   ("\<real>")
+
 
 defs (overloaded)
 
@@ -83,9 +80,6 @@
   real_abs_def:  "abs (r::real) == (if 0 \<le> r then r else -r)"
 
 
-syntax (xsymbols)
-  Reals     :: "'a set"                   ("\<real>")
-
 
 subsection{*Proving that realrel is an equivalence relation*}