# HG changeset patch
# User haftmann
# Date 1199283257 -3600
# Node ID 878c37886eed0cf4ff2d3a26d3f3c072fa8c2076
# Parent  474f8ba9dfa9bd0a2c6a7196ebf95e62e1c329d7
removed some legacy instantiations

diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/Library/Char_ord.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -9,10 +9,16 @@
 imports Product_ord Char_nat
 begin
 
-instance nibble :: linorder
-  nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
-  nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
-proof
+instantiation nibble :: linorder
+begin
+
+definition
+  nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+
+definition
+  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
+
+instance proof
   fix n :: nibble
   show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
 next
@@ -38,27 +44,52 @@
     unfolding nibble_less_eq_def by auto
 qed
 
-instance nibble :: distrib_lattice
+end
+
+instantiation nibble :: distrib_lattice
+begin
+
+definition
   "(inf \<Colon> nibble \<Rightarrow> _) = min"
+
+definition
   "(sup \<Colon> nibble \<Rightarrow> _) = max"
-  by default (auto simp add:
+
+instance by default (auto simp add:
     inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
 
-instance char :: linorder
-  char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
-    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
-  char_less_def:    "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
-    n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
+end
+
+instantiation char :: linorder
+begin
+
+definition
+  char_less_eq_def [code func del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
+
+definition
+  char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
+
+instance
   by default (auto simp: char_less_eq_def char_less_def split: char.splits)
 
-lemmas [code func del] = char_less_eq_def char_less_def
+end
 
-instance char :: distrib_lattice
+instantiation char :: distrib_lattice
+begin
+
+definition
   "(inf \<Colon> char \<Rightarrow> _) = min"
+
+definition
   "(sup \<Colon> char \<Rightarrow> _) = max"
-  by default (auto simp add:
+
+instance   by default (auto simp add:
     inf_char_def sup_char_def min_max.sup_inf_distrib1)
 
+end
+
 lemma [simp, code func]:
   shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
   and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -11,15 +11,20 @@
 
 subsection {* Prefix order on lists *}
 
-instance list :: (type) ord ..
+instantiation list :: (type) order
+begin
+
+definition
+  prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
 
-defs (overloaded)
-  prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
-  strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
+definition
+  strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
 
-instance list :: (type) order
+instance
   by intro_classes (auto simp add: prefix_def strict_prefix_def)
 
+end
+
 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
   unfolding prefix_def by blast
 
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/Library/List_lexord.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -9,9 +9,18 @@
 imports List
 begin
 
-instance list :: (ord) ord
+instantiation list :: (ord) ord
+begin
+
+definition
   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)" ..
+
+definition
+  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
+
+instance ..
+
+end
 
 instance list :: (order) order
   apply (intro_classes, unfold list_less_def list_le_def)
@@ -32,12 +41,21 @@
   apply simp
   done
 
-instance list :: (linorder) distrib_lattice
+instantiation list :: (linorder) distrib_lattice
+begin
+
+definition
   [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+
+definition
   [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
+
+instance
   by intro_classes
     (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
 
+end
+
 lemma not_less_Nil [simp]: "\<not> (x < [])"
   by (unfold list_less_def) simp
 
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -61,15 +61,23 @@
 begin
 
 definition
-  func_minus: "- f == (%x. - f x)"
-
-definition
   func_diff: "f - g == %x. f x - g x"
 
 instance ..
 
 end
 
+instantiation "fun" :: (type, uminus) uminus
+begin
+
+definition
+  func_minus: "- f == (%x. - f x)"
+
+instance ..
+
+end
+
+
 instantiation set :: (zero) zero
 begin
 
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -7,23 +7,69 @@
 imports MatrixGeneral
 begin
 
-instance matrix :: ("{zero, lattice}") lattice
-  "inf \<equiv> combine_matrix inf"
-  "sup \<equiv> combine_matrix sup"
+instantiation matrix :: ("{zero, lattice}") lattice
+begin
+
+definition
+  "inf = combine_matrix inf"
+
+definition
+  "sup = combine_matrix sup"
+
+instance
   by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
 
-instance matrix :: ("{plus, zero}") plus
-  plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
+end
+
+instantiation matrix :: ("{plus, zero}") plus
+begin
+
+definition
+  plus_matrix_def: "A + B = combine_matrix (op +) A B"
+
+instance ..
+
+end
+
+instantiation matrix :: ("{uminus, zero}") uminus
+begin
+
+definition
+  minus_matrix_def: "- A = apply_matrix uminus A"
+
+instance ..
+
+end
+
+instantiation matrix :: ("{minus, zero}") minus
+begin
 
-instance matrix :: ("{minus, zero}") minus
-  minus_matrix_def: "- A \<equiv> apply_matrix uminus A"
-  diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" ..
+definition
+  diff_matrix_def: "A - B = combine_matrix (op -) A B"
+
+instance ..
+
+end
+
+instantiation matrix :: ("{plus, times, zero}") times
+begin
+
+definition
+  times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
 
-instance matrix :: ("{plus, times, zero}") times
-  times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
+instance ..
+
+end
+
+instantiation matrix :: (lordered_ab_group_add) abs
+begin
 
-instance matrix :: (lordered_ab_group_add) abs
-  abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" ..
+definition
+  abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
+
+instance ..
+
+end
 
 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
 proof 
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -1279,9 +1279,18 @@
 apply (rule ext)+
 by simp
 
-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\<Colon>'a matrix) \<equiv> A \<le> B \<and> A \<noteq> B" ..
+instantiation matrix :: ("{ord, zero}") ord
+begin
+
+definition
+  le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
+
+definition
+  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
+
+instance ..
+
+end
 
 instance matrix :: ("{order, zero}") order
 apply intro_classes
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/SizeChange/Criterion.thy
--- a/src/HOL/SizeChange/Criterion.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/SizeChange/Criterion.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -15,14 +15,16 @@
     LESS ("\<down>")
   | LEQ ("\<Down>")
 
-instance sedge :: one
-  one_sedge_def: "1 \<equiv> \<Down>" ..
+instantiation sedge :: comm_monoid_mult
+begin
 
-instance sedge :: times
-  mult_sedge_def:" a * b \<equiv> if a = \<down> then \<down> else b" ..
+definition
+  one_sedge_def: "1 = \<Down>"
 
-instance sedge :: comm_monoid_mult
-proof
+definition
+  mult_sedge_def:" a * b = (if a = \<down> then \<down> else b)"
+
+instance  proof
   fix a b c :: sedge
   show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def)
   show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def)
@@ -30,6 +32,8 @@
     by (cases a, simp) (cases b, auto)
 qed
 
+end
+
 lemma sedge_UNIV:
   "UNIV = { LESS, LEQ }"
 proof (intro equalityI subsetI)
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/SizeChange/Graphs.thy
--- a/src/HOL/SizeChange/Graphs.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/SizeChange/Graphs.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -14,7 +14,7 @@
 datatype ('a, 'b) graph = 
   Graph "('a \<times> 'b \<times> 'a) set"
 
-fun dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
+primrec dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
   where "dest_graph (Graph G) = G"
 
 lemma graph_dest_graph[simp]:
@@ -60,29 +60,47 @@
   by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
 
 
-instance graph :: (type, type) "{comm_monoid_add}"
-  graph_zero_def: "0 == Graph {}" 
-  graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)"
-proof
+instantiation graph :: (type, type) comm_monoid_add
+begin
+
+definition
+  graph_zero_def: "0 = Graph {}" 
+
+definition
+  graph_plus_def [code func del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
+
+instance proof
   fix x y z :: "('a,'b) graph"
-
   show "x + y + z = x + (y + z)" 
    and "x + y = y + x" 
    and "0 + x = x"
-  unfolding graph_plus_def graph_zero_def 
-  by auto
+  unfolding graph_plus_def graph_zero_def by auto
 qed
 
-lemmas [code func del] = graph_plus_def
+end
+
+instantiation graph :: (type, type) "{distrib_lattice, complete_lattice}"
+begin
+
+definition
+  graph_leq_def [code func del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
+
+definition
+  graph_less_def [code func del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
 
-instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
-  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 \<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
+definition
+  [code func del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
+
+definition
+  [code func del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
+
+definition
+  Inf_graph_def [code func del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
+
+definition
+  Sup_graph_def [code func del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
+
+instance proof
   fix x y z :: "('a,'b) graph"
   fix A :: "('a, 'b) graph set"
 
@@ -130,8 +148,7 @@
     unfolding Sup_graph_def graph_leq_def by auto }
 qed
 
-lemmas [code func del] = graph_leq_def graph_less_def
-  inf_graph_def sup_graph_def Inf_graph_def Sup_graph_def
+end
 
 lemma in_grplus:
   "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
@@ -144,9 +161,13 @@
 
 subsubsection {* Multiplicative Structure *}
 
-instance graph :: (type, times) mult_zero
-  graph_mult_def: "G * H == grcomp G H" 
-proof
+instantiation graph :: (type, times) mult_zero
+begin
+
+definition
+  graph_mult_def [code func del]: "G * H = grcomp G H" 
+
+instance proof
   fix a :: "('a, 'b) graph"
 
   show "0 * a = 0" 
@@ -157,10 +178,17 @@
     by (cases a) (simp add:grcomp.simps)
 qed
 
-lemmas [code func del] = graph_mult_def
+end
+
+instantiation graph :: (type, one) one 
+begin
 
-instance graph :: (type, one) one 
-  graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
+definition
+  graph_one_def: "1 = Graph { (x, 1, x) |x. True}"
+
+instance ..
+
+end
 
 lemma in_grcomp:
   "has_edge (G * H) p b q
@@ -190,16 +218,18 @@
   qed
 qed
 
-fun grpow :: "nat \<Rightarrow> ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a, 'b) graph"
-where
-  "grpow 0 A = 1"
-| "grpow (Suc n) A = A * (grpow n A)"
+instantiation graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower, star}"
+begin
 
-instance graph :: (type, monoid_mult)
-  "{semiring_1,idem_add,recpower,star}"
-  graph_pow_def: "A ^ n == grpow n A"
-  graph_star_def: "star (G \<Colon> ('a, 'b) graph) == (SUP n. G ^ n)" 
-proof
+primrec power_graph :: "('a\<Colon>type, 'b\<Colon>monoid_mult) graph \<Rightarrow> nat => ('a, 'b) graph"
+where
+  "(A \<Colon> ('a, 'b) graph) ^ 0 = 1"
+| "(A \<Colon> ('a, 'b) graph) ^ Suc n = A * (A ^ n)"
+
+definition
+  graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)" 
+
+instance proof
   fix a b c :: "('a, 'b) graph"
   
   show "1 * a = a" 
@@ -219,9 +249,11 @@
   show "a + a = a" unfolding graph_plus_def by simp
   
   show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n"
-    unfolding graph_pow_def by simp_all
+    by simp_all
 qed
 
+end
+
 lemma graph_leqI:
   assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   shows "G \<le> H"
@@ -309,7 +341,7 @@
 
 lemma in_tcl: 
   "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
-  apply (auto simp: tcl_is_SUP in_SUP)
+  apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps)
   apply (rule_tac x = "n - 1" in exI, auto)
   done
 
diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/ZF/Games.thy	Wed Jan 02 15:14:17 2008 +0100
@@ -850,15 +850,30 @@
   by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def
     eq_game_sym intro: eq_game_refl eq_game_trans)
 
-instance Pg :: "{ord,zero,plus,minus}" ..
+instantiation Pg :: "{ord, zero, plus, minus, uminus}"
+begin
+
+definition
+  Pg_zero_def: "0 = Abs_Pg (eq_game_rel `` {zero_game})"
+
+definition
+  Pg_le_def: "G \<le> H \<longleftrightarrow> (\<exists> g h. g \<in> Rep_Pg G \<and> h \<in> Rep_Pg H \<and> ge_game (h, g))"
+
+definition
+  Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
 
-defs (overloaded)
-  Pg_zero_def: "0 \<equiv> Abs_Pg (eq_game_rel `` {zero_game})"
-  Pg_le_def: "G \<le> H \<equiv> \<exists> g h. g \<in> Rep_Pg G \<and> h \<in> Rep_Pg H \<and> ge_game (h, g)"
-  Pg_less_def: "G < H \<equiv> G \<le> H \<and> G \<noteq> (H::Pg)"
-  Pg_minus_def: "- G \<equiv> contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
-  Pg_plus_def: "G + H \<equiv> contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game (g,h)})})"
-  Pg_diff_def: "G - H \<equiv> G + (- (H::Pg))"
+definition
+  Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+
+definition
+  Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game (g,h)})})"
+
+definition
+  Pg_diff_def: "G - H = G + (- (H::Pg))"
+
+instance ..
+
+end
 
 lemma Rep_Abs_eq_Pg[simp]: "Rep_Pg (Abs_Pg (eq_game_rel `` {g})) = eq_game_rel `` {g}"
   apply (subst Abs_Pg_inverse)