# HG changeset patch
# User haftmann
# Date 1196352506 -3600
# Node ID 9200b36280c012a012c4b471282b88a899231fba
# Parent  845883bd3a6bb4bf1c28261ce1476695d9856f02
instance command as rudimentary class target

diff -r 845883bd3a6b -r 9200b36280c0 NEWS
--- a/NEWS	Thu Nov 29 07:55:46 2007 +0100
+++ b/NEWS	Thu Nov 29 17:08:26 2007 +0100
@@ -4,6 +4,14 @@
 New in this Isabelle version
 ----------------------------
 
+*** Pure ***
+
+* Command "instance" now takes list of definitions in the same
+manner as the "definition" command.  Most notably, object equality is now
+possible.  Type inference is more canonical than it used to be.
+INCOMPATIBILITY: in some cases explicit type annotations are required.
+
+
 *** HOL ***
 
 * Constant "card" now with authentic syntax.
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Complex/Complex.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -45,7 +45,7 @@
   complex_minus_def:
     "- x \<equiv> Complex (- Re x) (- Im x)"
   complex_diff_def:
-    "x - y \<equiv> x + - y" ..
+    "x - (y\<Colon>complex) \<equiv> x + - y" ..
 
 lemma Complex_eq_0 [simp]: "(Complex a b = 0) = (a = 0 \<and> b = 0)"
 by (simp add: complex_zero_def)
@@ -116,7 +116,7 @@
     "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 \<equiv> x * inverse y" ..
+    "x / (y\<Colon>complex) \<equiv> x * inverse y" ..
 
 lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
 by (simp add: complex_one_def)
@@ -195,7 +195,7 @@
 
 instance complex :: number
   complex_number_of_def:
-    "number_of w \<equiv> of_int w" ..
+    "number_of w \<equiv> of_int w \<Colon> complex" ..
 
 instance complex :: number_ring
 by (intro_classes, simp only: complex_number_of_def)
@@ -213,10 +213,10 @@
 by (cases z rule: int_diff_cases) simp
 
 lemma complex_Re_number_of [simp]: "Re (number_of v) = number_of v"
-unfolding number_ring_class.axioms by (rule complex_Re_of_int)
+unfolding number_of_eq by (rule complex_Re_of_int)
 
 lemma complex_Im_number_of [simp]: "Im (number_of v) = 0"
-unfolding number_ring_class.axioms by (rule complex_Im_of_int)
+unfolding number_of_eq by (rule complex_Im_of_int)
 
 lemma Complex_eq_number_of [simp]:
   "(Complex a b = number_of w) = (a = number_of w \<and> b = 0)"
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -2689,7 +2689,7 @@
 lemmas [code func] = univ_bool
 
 instance * :: (finite, finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite)"
+  "itself \<equiv> TYPE('a \<times> 'b)"
 proof
   show "finite (UNIV :: ('a \<times> 'b) set)"
   proof (rule finite_Prod_UNIV)
@@ -2703,7 +2703,7 @@
   unfolding UNIV_Times_UNIV ..
 
 instance "+" :: (finite, finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite + 'b\<Colon>finite)"
+  "itself \<equiv> TYPE('a + 'b)"
 proof
   have a: "finite (UNIV :: 'a set)" by (rule finite)
   have b: "finite (UNIV :: 'b set)" by (rule finite)
@@ -2717,7 +2717,7 @@
   unfolding UNIV_Plus_UNIV ..
 
 instance set :: (finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite set)"
+  "itself \<equiv> TYPE('a set)"
 proof
   have "finite (UNIV :: 'a set)" by (rule finite)
   hence "finite (Pow (UNIV :: 'a set))"
@@ -2732,7 +2732,7 @@
   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
 
 instance "fun" :: (finite, finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite \<Rightarrow> 'b\<Colon>finite)"
+  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
 proof
   show "finite (UNIV :: ('a => 'b) set)"
   proof (rule finite_imageD)
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/IntDef.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -36,7 +36,7 @@
 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)" ..
+  diff_int_def:  "z - w \<equiv> z + (-w \<Colon> int)" ..
 
 instance int :: times
   mult_int_def: "z * w \<equiv>  Abs_Integ
@@ -46,7 +46,7 @@
 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 < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
+  less_int_def: "(z\<Colon>int) < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
 
 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
@@ -218,8 +218,8 @@
   zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
 
 instance int :: distrib_lattice
-  "inf \<equiv> min"
-  "sup \<equiv> max"
+  "inf \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> min"
+  "sup \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> max"
   by intro_classes
     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Char_ord.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -39,8 +39,8 @@
 qed
 
 instance nibble :: distrib_lattice
-    "inf \<equiv> min"
-    "sup \<equiv> max"
+  "(inf \<Colon> nibble \<Rightarrow> _) = min"
+  "(sup \<Colon> nibble \<Rightarrow> _) = max"
   by default (auto simp add:
     inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
 
@@ -54,8 +54,8 @@
 lemmas [code func del] = char_less_eq_def char_less_def
 
 instance char :: distrib_lattice
-    "inf \<equiv> min"
-    "sup \<equiv> max"
+  "(inf \<Colon> char \<Rightarrow> _) = min"
+  "(sup \<Colon> char \<Rightarrow> _) = max"
   by default (auto simp add:
     inf_char_def sup_char_def min_max.sup_inf_distrib1)
 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Code_Index.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -143,7 +143,7 @@
   by simp
 
 instance index :: abs
-  "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
+  "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" ..
 
 lemma index_of_int [code func]:
   "index_of_int k = (if k = 0 then 0
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Eval.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -35,16 +35,16 @@
 *}
 
 instance "prop" :: typ_of
-  "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
+  "typ_of (T\<Colon>prop itself) \<equiv> STR ''prop'' {\<struct>} []" ..
 
 instance itself :: (typ_of) typ_of
-  "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
+  "typ_of (T\<Colon>'a itself itself) \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
 
 instance set :: (typ_of) typ_of
-  "typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
+  "typ_of (T\<Colon>'a set itself) \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
 
 instance int :: typ_of
-  "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
+  "typ_of (T\<Colon>int itself) \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
 
 setup {*
 let
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/List_lexord.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -10,13 +10,11 @@
 begin
 
 instance list :: (ord) ord
-  list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
-  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
-
-lemmas list_ord_defs [code func del] = list_less_def list_le_def
+  list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
+  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)" ..
 
 instance list :: (order) order
-  apply (intro_classes, unfold list_ord_defs)
+  apply (intro_classes, unfold list_less_def list_le_def)
   apply safe
   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
   apply simp
@@ -35,13 +33,11 @@
   done
 
 instance list :: (linorder) distrib_lattice
-  "inf \<equiv> min"
-  "sup \<equiv> max"
+  [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+  [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
   by intro_classes
     (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
 
-lemmas [code func del] = inf_list_def sup_list_def
-
 lemma not_less_Nil [simp]: "\<not> (x < [])"
   by (unfold list_less_def) simp
 
@@ -52,13 +48,13 @@
   by (unfold list_less_def) simp
 
 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
-  by (unfold list_ord_defs, cases x) auto
+  by (unfold list_le_def, cases x) auto
 
 lemma Nil_le_Cons [simp]: "[] \<le> x"
-  by (unfold list_ord_defs, cases x) auto
+  by (unfold list_le_def, cases x) auto
 
 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
-  by (unfold list_ord_defs) auto
+  by (unfold list_le_def) auto
 
 lemma less_code [code func]:
   "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Parity.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -17,7 +17,7 @@
   "odd x \<equiv> \<not> even x"
 
 instance int :: even_odd
-  even_def[presburger]: "even x \<equiv> x mod 2 = 0" ..
+  even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" ..
 
 instance nat :: even_odd
   even_nat_def[presburger]: "even x \<equiv> even (int x)" ..
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -10,30 +10,28 @@
 begin
 
 instance "*" :: (ord, ord) ord
-  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
-  prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
-
-lemmas prod_ord_defs [code func del] = prod_less_def prod_le_def
+  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" ..
 
 lemma [code func]:
   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
-  unfolding prod_ord_defs by simp_all
+  unfolding prod_le_def prod_less_def by simp_all
 
 lemma [code]:
   "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
-  unfolding prod_ord_defs by simp_all
+  unfolding prod_le_def prod_less_def by simp_all
 
 instance * :: (order, order) order
-  by default (auto simp: prod_ord_defs intro: order_less_trans)
+  by default (auto simp: prod_le_def prod_less_def intro: order_less_trans)
 
 instance * :: (linorder, linorder) linorder
   by default (auto simp: prod_le_def)
 
 instance * :: (linorder, linorder) distrib_lattice
-  inf_prod_def: "inf \<equiv> min"
-  sup_prod_def: "sup \<equiv> max"
+  inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+  sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
   by intro_classes
     (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/List.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -2691,7 +2691,7 @@
 text{* The integers are an instance of the above class: *}
 
 instance int:: finite_intvl_succ
-  successor_int_def: "successor == (%i. i+1)"
+  successor_int_def: "successor == (%i\<Colon>int. i+1)"
 by intro_classes (simp_all add: successor_int_def)
 
 text{* Now @{term"[i..j::int]"} is defined for integers. *}
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -23,7 +23,7 @@
   times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
 
 instance matrix :: (lordered_ab_group_add) abs
-  abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
+  abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" ..
 
 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
 proof 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -1281,7 +1281,7 @@
 
 instance matrix :: ("{ord, zero}") ord
   le_matrix_def: "A \<le> B \<equiv> \<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i"
-  less_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
+  less_def: "A < (B\<Colon>'a matrix) \<equiv> A \<le> B \<and> A \<noteq> B" ..
 
 instance matrix :: ("{order, zero}") order
 apply intro_classes
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Nat.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -1488,8 +1488,8 @@
 text {* the lattice order on @{typ nat} *}
 
 instance nat :: distrib_lattice
-  "inf \<equiv> min"
-  "sup \<equiv> max"
+  "inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> min"
+  "sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> max"
   by intro_classes
     (simp_all add: inf_nat_def sup_nat_def)
 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Numeral.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -203,16 +203,15 @@
   unfolding numeral_simps int_distrib by simp 
 
 
-
 subsection {* Converting Numerals to Rings: @{term number_of} *}
 
-axclass number_ring \<subseteq> number, comm_ring_1
-  number_of_eq: "number_of k = of_int k"
+class number_ring = number + comm_ring_1 +
+  assumes number_of_eq: "number_of k = of_int k"
 
 text {* self-embedding of the integers *}
 
 instance int :: number_ring
-  int_number_of_def: "number_of w \<equiv> of_int w"
+  int_number_of_def: "number_of w \<equiv> of_int w \<Colon> int"
   by intro_classes (simp only: int_number_of_def)
 
 lemmas [code func del] = int_number_of_def
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Orderings.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -930,7 +930,7 @@
 
 instance bool :: order 
   le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
-  less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
+  less_bool_def: "(P\<Colon>bool) < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
   by intro_classes (auto simp add: le_bool_def less_bool_def)
 lemmas [code func del] = le_bool_def less_bool_def
 
@@ -968,7 +968,7 @@
 
 instance "fun" :: (type, ord) ord
   le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
-  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
+  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
 
 lemmas [code func del] = le_fun_def less_fun_def
 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Real/PReal.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -212,8 +212,8 @@
   by intro_classes (rule preal_le_linear)
 
 instance preal :: distrib_lattice
-  "inf \<equiv> min"
-  "sup \<equiv> max"
+  "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
+  "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal  \<equiv> max"
   by intro_classes
     (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Real/Rational.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -362,8 +362,8 @@
 qed
 
 instance rat :: distrib_lattice
-  "inf r s \<equiv> min r s"
-  "sup r s \<equiv> max r s"
+  "inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> min"
+  "sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> max"
   by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
 
 instance rat :: ordered_field
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Real/RealDef.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -66,7 +66,7 @@
   real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
 
 instance real :: sgn
-  real_sgn_def: "sgn x == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
+  real_sgn_def: "sgn (x::real) == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
 
 subsection {* Equivalence relation over positive reals *}
 
@@ -401,8 +401,8 @@
 done
 
 instance real :: distrib_lattice
-  "inf x y \<equiv> min x y"
-  "sup x y \<equiv> max x y"
+  "inf \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> min"
+  "sup \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> max"
   by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
 
 
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Set.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -145,7 +145,7 @@
 
 instance set :: (type) ord
   subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
-  psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
+  psubset_def: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
 lemmas [code func del] = subset_def psubset_def
 
 abbreviation
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/SizeChange/Graphs.thy
--- a/src/HOL/SizeChange/Graphs.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/SizeChange/Graphs.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -79,7 +79,7 @@
   graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
   graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
   "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
-  "sup G H \<equiv> G + H"
+  "sup (G \<Colon> ('a, 'b) graph)  H \<equiv> G + H"
   Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
   Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))"
 proof
@@ -195,10 +195,10 @@
   "grpow 0 A = 1"
 | "grpow (Suc n) A = A * (grpow n A)"
 
-instance graph :: (type, monoid_mult) 
+instance graph :: (type, monoid_mult)
   "{semiring_1,idem_add,recpower,star}"
   graph_pow_def: "A ^ n == grpow n A"
-  graph_star_def: "star G == (SUP n. G ^ n)" 
+  graph_star_def: "star (G \<Colon> ('a, 'b) graph) == (SUP n. G ^ n)" 
 proof
   fix a b c :: "('a, 'b) graph"
   
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Nov 29 17:08:26 2007 +0100
@@ -544,7 +544,7 @@
         |> not (null arities) ? (
             f arities css
             #-> (fn defs =>
-              Class.prove_instance tac arities defs
+              Instance.prove_instance tac arities defs
             #-> (fn defs =>
               after_qed arities css defs)))
       end;
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Thu Nov 29 17:08:26 2007 +0100
@@ -38,7 +38,7 @@
     val n = Sign.arity_number thy tyco;
   in
     thy
-    |> Class.prove_instance (Class.intro_classes_tac [])
+    |> Instance.prove_instance (Class.intro_classes_tac [])
         [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
     |> snd
   end
diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -13,14 +13,14 @@
   assumes assoc: "x \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)"
 
 instance nat :: semigroup
-  "m \<otimes> n \<equiv> m + n"
+  "m \<otimes> n \<equiv> (m\<Colon>nat) + n"
 proof
   fix m n q :: nat 
   from mult_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
 qed
 
 instance int :: semigroup
-  "k \<otimes> l \<equiv> k + l"
+  "k \<otimes> l \<equiv> (k\<Colon>int) + l"
 proof
   fix k l j :: int
   from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
@@ -47,8 +47,8 @@
   assumes neutl: "\<one> \<otimes> x = x"
 
 instance nat :: monoidl and int :: monoidl
-  "\<one> \<equiv> 0"
-  "\<one> \<equiv> 0"
+  "\<one> \<equiv> (0\<Colon>nat)"
+  "\<one> \<equiv> (0\<Colon>int)"
 proof
   fix n :: nat
   from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp
diff -r 845883bd3a6b -r 9200b36280c0 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/Pure/Isar/class.ML	Thu Nov 29 17:08:26 2007 +0100
@@ -57,16 +57,7 @@
 
   (*old instance layer*)
   val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
-  val instance: arity list -> ((bstring * Attrib.src list) * term) list
-    -> (thm list -> theory -> theory)
-    -> theory -> Proof.state
-  val instance_cmd: (bstring * xstring list * xstring) list
-    -> ((bstring * Attrib.src list) * xstring) list
-    -> (thm list -> theory -> theory)
-    -> theory -> Proof.state
-  val prove_instance: tactic -> arity list
-    -> ((bstring * Attrib.src list) * term) list
-    -> theory -> thm list * theory
+  val instance_arity_cmd: (bstring * xstring list * xstring) list -> theory -> Proof.state
 end;
 
 structure Class : CLASS =
@@ -150,6 +141,8 @@
 
 val instance_arity =
   gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
+val instance_arity_cmd =
+  gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
 val classrel =
   gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
     AxClass.add_classrel I o single;
@@ -221,7 +214,7 @@
     val SOME class = AxClass.class_of_param thy c;
     val SOME tyco = inst_tyco thy (c, ty);
     val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
-    val c' = NameSpace.base c;
+    val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
     val ty' = Type.strip_sorts ty;
   in
     thy
@@ -253,137 +246,6 @@
   end;
 
 
-(* legacy *)
-
-fun add_inst_def (class, tyco) (c, ty) thy =
-  let
-    val tyco_base = Sign.base_name tyco;
-    val name_inst = Sign.base_name class ^ "_" ^ tyco_base ^ "_inst";
-    val c_inst_base = Sign.base_name c ^ "_" ^ tyco_base;
-  in
-    thy
-    |> Sign.sticky_prefix name_inst
-    |> Sign.declare_const [] (c_inst_base, ty, NoSyn)
-    |-> (fn const as Const (c_inst, _) =>
-      PureThy.add_defs_i false
-        [((Thm.def_name c_inst_base, Logic.mk_equals (const, Const (c, ty))), [])]
-      #-> (fn [thm] => add_inst (c, tyco) (c_inst, Thm.symmetric thm)))
-    |> Sign.restore_naming thy
-  end;
-
-fun add_inst_def' (class, tyco) (c, ty) thy =
-  if case Symtab.lookup (fst (InstData.get thy)) c
-   of NONE => true
-    | SOME tab => is_none (Symtab.lookup tab tyco)
-  then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy
-  else thy;
-
-fun add_def ((class, tyco), ((name, prop), atts)) thy =
-  let
-    val ((lhs as Const (c, ty), args), rhs) =
-      (apfst Term.strip_comb o Logic.dest_equals) prop;
-  in
-    thy
-    |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)]
-    |-> (fn [def] => add_inst_def (class, tyco) (c, ty) #> pair def)
-  end;
-
-
-(** instances with implicit parameter handling **)
-
-local
-
-fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) =
-  let
-    val ctxt = ProofContext.init thy;
-    val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
-    val ((c, ty), _) = Sign.cert_def ctxt t;
-    val atts = map (prep_att thy) raw_atts;
-    val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
-    val name = case raw_name
-     of "" => NONE
-      | _ => SOME raw_name;
-  in (c, (insts, ((name, t), atts))) end;
-
-fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop;
-fun read_def thy = gen_read_def thy (K I) (K I);
-
-fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
-  let
-    val arities = map (prep_arity theory) raw_arities;
-    val _ = if null arities then error "At least one arity must be given" else ();
-    val _ = case (duplicates (op =) o map #1) arities
-     of [] => ()
-      | dupl_tycos => error ("Type constructors occur more than once in arities: "
-          ^ commas_quote dupl_tycos);
-    fun get_consts_class tyco ty class =
-      let
-        val cs = (these o try (#params o AxClass.get_info theory)) class;
-        val subst_ty = map_type_tfree (K ty);
-      in
-        map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs
-      end;
-    fun get_consts_sort (tyco, asorts, sort) =
-      let
-        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
-          (Name.names Name.context Name.aT asorts))
-      in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
-    val cs = maps get_consts_sort arities;
-    fun mk_typnorm thy (ty, ty_sc) =
-      case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
-       of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT)
-        | NONE => NONE;
-    fun read_defs defs cs thy_read =
-      let
-        fun read raw_def cs =
-          let
-            val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
-            val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
-            val ((class, tyco), ty') = case AList.lookup (op =) cs c
-             of NONE => error ("Illegal definition for constant " ^ quote c)
-              | SOME class_ty => class_ty;
-            val name = case name_opt
-             of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
-              | SOME name => name;
-            val t' = case mk_typnorm thy_read (ty', ty)
-             of NONE => error ("Illegal definition for constant " ^
-                  quote (c ^ "::" ^ setmp show_sorts true
-                    (Sign.string_of_typ thy_read) ty))
-              | SOME norm => map_types norm t
-          in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
-      in fold_map read defs cs end;
-    val (defs, other_cs) = read_defs raw_defs cs
-      (fold Sign.primitive_arity arities (Theory.copy theory));
-    fun after_qed' cs defs =
-      fold Sign.add_const_constraint (map (apsnd SOME) cs)
-      #> after_qed defs;
-  in
-    theory
-    |> fold_map get_remove_global_constraint (map fst cs |> distinct (op =))
-    ||>> fold_map add_def defs
-    ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
-    |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
-  end;
-
-fun tactic_proof tac f arities defs =
-  fold (fn arity => AxClass.prove_arity arity tac) arities
-  #> f
-  #> pair defs;
-
-in
-
-val instance = gen_instance Sign.cert_arity read_def
-  (fn f => fn arities => fn defs => instance_arity f arities);
-val instance_cmd = gen_instance Sign.read_arity read_def_cmd
-  (fn f => fn arities => fn defs => instance_arity f arities);
-fun prove_instance tac arities defs =
-  gen_instance Sign.cert_arity read_def
-    (tactic_proof tac) arities defs (K I);
-
-end; (*local*)
-
-
-
 (** class data **)
 
 datatype class_data = ClassData of {
@@ -1008,7 +870,7 @@
 
     fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
-             of SOME (_, ty') => Type.typ_match tsig (ty, ty')
+             of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty')))
               | NONE => I)
           | NONE => I)
       | check_improve _ = I;
@@ -1057,6 +919,7 @@
      of [] => ()
       | dupl_tycos => error ("Type constructors occur more than once in arities: "
           ^ commas_quote dupl_tycos);
+    val _ = map (map (the_class_data thy) o #3) arities;
     val ty_insts = map (fn (tyco, sorts, _) =>
         (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
       arities;
@@ -1064,12 +927,11 @@
     fun type_name "*" = "prod"
       | type_name "+" = "sum"
       | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
-    fun get_param tyco sorts (param, (c, ty)) =
-      ((unoverload_const thy (c, ty), tyco),
-        (param ^ "_" ^ type_name tyco,
-          map_atyps (K (ty_inst tyco)) ty));
+    fun get_param tyco sorts (param, (c, ty)) = if can (inst thy) (c, tyco)
+      then NONE else SOME ((unoverload_const thy (c, ty), tyco),
+        (param ^ "_" ^ type_name tyco, map_atyps (K (ty_inst tyco)) ty));
     fun get_params (tyco, sorts, sort) =
-      map (get_param tyco sorts) (these_params thy sort)
+      map_filter (get_param tyco sorts) (these_params thy sort)
     val params = maps get_params arities;
   in
     thy
@@ -1099,8 +961,8 @@
   Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
 
 fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
-  fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
-    (fn {context, ...} => tac context)) lthy) I;
+  fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
+    (fn {context, ...} => tac context)) ts) lthy) I;
 
 fun conclude_instantiation lthy =
   let
@@ -1121,7 +983,7 @@
       let
         val SOME class = AxClass.class_of_param thy c;
         val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
-        val c' = NameSpace.base c;
+        val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
         val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
         val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
       in
diff -r 845883bd3a6b -r 9200b36280c0 src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/Pure/Isar/instance.ML	Thu Nov 29 17:08:26 2007 +0100
@@ -10,7 +10,6 @@
   val instantiate: arity list -> (local_theory -> local_theory)
     -> (Proof.context -> tactic) -> theory -> theory
   val instance: arity list -> ((bstring * Attrib.src list) * term) list
-    -> (thm list -> theory -> theory)
     -> theory -> Proof.state
   val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list
     -> theory -> thm list * theory
@@ -18,7 +17,6 @@
   val instantiation_cmd: (xstring * sort * xstring) list
     -> theory -> local_theory
   val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list
-    -> (thm list -> theory -> theory)
     -> theory -> Proof.state
 end;
 
@@ -35,8 +33,9 @@
   #> LocalTheory.exit
   #> ProofContext.theory_of;
 
-fun gen_instance prep_arity prep_attr parse_term do_proof raw_arities defs after_qed thy =
+fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
   let
+    val arities = map (prep_arity thy) raw_arities;
     fun export_defs ctxt = 
       let
         val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
@@ -54,8 +53,9 @@
       let
         val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
       in Specification.definition def' ctxt end;
-    val arities = map (prep_arity thy) raw_arities;
-  in
+  in if not (null defs) orelse forall (fn (_, _, sort) =>
+      forall (Class.is_class thy) sort) arities
+  then
     thy
     |> TheoryTarget.instantiation arities
     |> `(fn ctxt => map (mk_def ctxt) defs)
@@ -64,15 +64,21 @@
     ||> LocalTheory.exit
     ||> ProofContext.theory_of
     ||> TheoryTarget.instantiation arities
-    |-> (fn defs => do_proof defs (LocalTheory.theory (after_qed defs)))
+    |-> (fn defs => do_proof defs)
+  else
+    thy
+    |> do_proof' arities
   end;
 
 val instance = gen_instance Sign.cert_arity (K I) (K I)
-  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
+  (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
 val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
-  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
+  (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
 fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
-  (fn defs => fn after_qed => Class.prove_instantiation_instance (K tac)
-    #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I);
+  (fn defs => Class.prove_instantiation_instance (K tac)
+    #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs)
+   (pair [] o ProofContext.theory_of o Proof.global_terminal_proof
+      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
+      oo Class.instance_arity I) arities defs;
 
 end;
diff -r 845883bd3a6b -r 9200b36280c0 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 29 17:08:26 2007 +0100
@@ -453,10 +453,8 @@
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.$$$ "advanced" |-- P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
-      >> (fn (arities, defs) => Instance.instance_cmd arities defs (K I)) ||
     P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
-      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
+      >> (fn (arities, defs) => Instance.instance_cmd arities defs))
     >> (Toplevel.print oo Toplevel.theory_to_proof)
   || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));