removed some legacy instantiations
authorhaftmann
Wed Jan 02 15:14:17 2008 +0100 (2008-01-02)
changeset 25764878c37886eed
parent 25763 474f8ba9dfa9
child 25765 49580bd58a21
removed some legacy instantiations
src/HOL/Library/Char_ord.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/SizeChange/Criterion.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/ZF/Games.thy
     1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Jan 02 15:14:15 2008 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Jan 02 15:14:17 2008 +0100
     1.3 @@ -9,10 +9,16 @@
     1.4  imports Product_ord Char_nat
     1.5  begin
     1.6  
     1.7 -instance nibble :: linorder
     1.8 -  nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
     1.9 -  nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
    1.10 -proof
    1.11 +instantiation nibble :: linorder
    1.12 +begin
    1.13 +
    1.14 +definition
    1.15 +  nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    1.16 +
    1.17 +definition
    1.18 +  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    1.19 +
    1.20 +instance proof
    1.21    fix n :: nibble
    1.22    show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    1.23  next
    1.24 @@ -38,27 +44,52 @@
    1.25      unfolding nibble_less_eq_def by auto
    1.26  qed
    1.27  
    1.28 -instance nibble :: distrib_lattice
    1.29 +end
    1.30 +
    1.31 +instantiation nibble :: distrib_lattice
    1.32 +begin
    1.33 +
    1.34 +definition
    1.35    "(inf \<Colon> nibble \<Rightarrow> _) = min"
    1.36 +
    1.37 +definition
    1.38    "(sup \<Colon> nibble \<Rightarrow> _) = max"
    1.39 -  by default (auto simp add:
    1.40 +
    1.41 +instance by default (auto simp add:
    1.42      inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    1.43  
    1.44 -instance char :: linorder
    1.45 -  char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.46 -    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    1.47 -  char_less_def:    "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.48 -    n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    1.49 +end
    1.50 +
    1.51 +instantiation char :: linorder
    1.52 +begin
    1.53 +
    1.54 +definition
    1.55 +  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>
    1.56 +    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
    1.57 +
    1.58 +definition
    1.59 +  char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.60 +    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
    1.61 +
    1.62 +instance
    1.63    by default (auto simp: char_less_eq_def char_less_def split: char.splits)
    1.64  
    1.65 -lemmas [code func del] = char_less_eq_def char_less_def
    1.66 +end
    1.67  
    1.68 -instance char :: distrib_lattice
    1.69 +instantiation char :: distrib_lattice
    1.70 +begin
    1.71 +
    1.72 +definition
    1.73    "(inf \<Colon> char \<Rightarrow> _) = min"
    1.74 +
    1.75 +definition
    1.76    "(sup \<Colon> char \<Rightarrow> _) = max"
    1.77 -  by default (auto simp add:
    1.78 +
    1.79 +instance   by default (auto simp add:
    1.80      inf_char_def sup_char_def min_max.sup_inf_distrib1)
    1.81  
    1.82 +end
    1.83 +
    1.84  lemma [simp, code func]:
    1.85    shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    1.86    and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
     2.1 --- a/src/HOL/Library/List_Prefix.thy	Wed Jan 02 15:14:15 2008 +0100
     2.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Jan 02 15:14:17 2008 +0100
     2.3 @@ -11,15 +11,20 @@
     2.4  
     2.5  subsection {* Prefix order on lists *}
     2.6  
     2.7 -instance list :: (type) ord ..
     2.8 +instantiation list :: (type) order
     2.9 +begin
    2.10 +
    2.11 +definition
    2.12 +  prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
    2.13  
    2.14 -defs (overloaded)
    2.15 -  prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
    2.16 -  strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    2.17 +definition
    2.18 +  strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
    2.19  
    2.20 -instance list :: (type) order
    2.21 +instance
    2.22    by intro_classes (auto simp add: prefix_def strict_prefix_def)
    2.23  
    2.24 +end
    2.25 +
    2.26  lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
    2.27    unfolding prefix_def by blast
    2.28  
     3.1 --- a/src/HOL/Library/List_lexord.thy	Wed Jan 02 15:14:15 2008 +0100
     3.2 +++ b/src/HOL/Library/List_lexord.thy	Wed Jan 02 15:14:17 2008 +0100
     3.3 @@ -9,9 +9,18 @@
     3.4  imports List
     3.5  begin
     3.6  
     3.7 -instance list :: (ord) ord
     3.8 +instantiation list :: (ord) ord
     3.9 +begin
    3.10 +
    3.11 +definition
    3.12    list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
    3.13 -  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)" ..
    3.14 +
    3.15 +definition
    3.16 +  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
    3.17 +
    3.18 +instance ..
    3.19 +
    3.20 +end
    3.21  
    3.22  instance list :: (order) order
    3.23    apply (intro_classes, unfold list_less_def list_le_def)
    3.24 @@ -32,12 +41,21 @@
    3.25    apply simp
    3.26    done
    3.27  
    3.28 -instance list :: (linorder) distrib_lattice
    3.29 +instantiation list :: (linorder) distrib_lattice
    3.30 +begin
    3.31 +
    3.32 +definition
    3.33    [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    3.34 +
    3.35 +definition
    3.36    [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    3.37 +
    3.38 +instance
    3.39    by intro_classes
    3.40      (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    3.41  
    3.42 +end
    3.43 +
    3.44  lemma not_less_Nil [simp]: "\<not> (x < [])"
    3.45    by (unfold list_less_def) simp
    3.46  
     4.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Wed Jan 02 15:14:15 2008 +0100
     4.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Wed Jan 02 15:14:17 2008 +0100
     4.3 @@ -61,15 +61,23 @@
     4.4  begin
     4.5  
     4.6  definition
     4.7 -  func_minus: "- f == (%x. - f x)"
     4.8 -
     4.9 -definition
    4.10    func_diff: "f - g == %x. f x - g x"
    4.11  
    4.12  instance ..
    4.13  
    4.14  end
    4.15  
    4.16 +instantiation "fun" :: (type, uminus) uminus
    4.17 +begin
    4.18 +
    4.19 +definition
    4.20 +  func_minus: "- f == (%x. - f x)"
    4.21 +
    4.22 +instance ..
    4.23 +
    4.24 +end
    4.25 +
    4.26 +
    4.27  instantiation set :: (zero) zero
    4.28  begin
    4.29  
     5.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Jan 02 15:14:15 2008 +0100
     5.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Jan 02 15:14:17 2008 +0100
     5.3 @@ -7,23 +7,69 @@
     5.4  imports MatrixGeneral
     5.5  begin
     5.6  
     5.7 -instance matrix :: ("{zero, lattice}") lattice
     5.8 -  "inf \<equiv> combine_matrix inf"
     5.9 -  "sup \<equiv> combine_matrix sup"
    5.10 +instantiation matrix :: ("{zero, lattice}") lattice
    5.11 +begin
    5.12 +
    5.13 +definition
    5.14 +  "inf = combine_matrix inf"
    5.15 +
    5.16 +definition
    5.17 +  "sup = combine_matrix sup"
    5.18 +
    5.19 +instance
    5.20    by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    5.21  
    5.22 -instance matrix :: ("{plus, zero}") plus
    5.23 -  plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
    5.24 +end
    5.25 +
    5.26 +instantiation matrix :: ("{plus, zero}") plus
    5.27 +begin
    5.28 +
    5.29 +definition
    5.30 +  plus_matrix_def: "A + B = combine_matrix (op +) A B"
    5.31 +
    5.32 +instance ..
    5.33 +
    5.34 +end
    5.35 +
    5.36 +instantiation matrix :: ("{uminus, zero}") uminus
    5.37 +begin
    5.38 +
    5.39 +definition
    5.40 +  minus_matrix_def: "- A = apply_matrix uminus A"
    5.41 +
    5.42 +instance ..
    5.43 +
    5.44 +end
    5.45 +
    5.46 +instantiation matrix :: ("{minus, zero}") minus
    5.47 +begin
    5.48  
    5.49 -instance matrix :: ("{minus, zero}") minus
    5.50 -  minus_matrix_def: "- A \<equiv> apply_matrix uminus A"
    5.51 -  diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" ..
    5.52 +definition
    5.53 +  diff_matrix_def: "A - B = combine_matrix (op -) A B"
    5.54 +
    5.55 +instance ..
    5.56 +
    5.57 +end
    5.58 +
    5.59 +instantiation matrix :: ("{plus, times, zero}") times
    5.60 +begin
    5.61 +
    5.62 +definition
    5.63 +  times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
    5.64  
    5.65 -instance matrix :: ("{plus, times, zero}") times
    5.66 -  times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
    5.67 +instance ..
    5.68 +
    5.69 +end
    5.70 +
    5.71 +instantiation matrix :: (lordered_ab_group_add) abs
    5.72 +begin
    5.73  
    5.74 -instance matrix :: (lordered_ab_group_add) abs
    5.75 -  abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" ..
    5.76 +definition
    5.77 +  abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
    5.78 +
    5.79 +instance ..
    5.80 +
    5.81 +end
    5.82  
    5.83  instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
    5.84  proof 
     6.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Jan 02 15:14:15 2008 +0100
     6.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Jan 02 15:14:17 2008 +0100
     6.3 @@ -1279,9 +1279,18 @@
     6.4  apply (rule ext)+
     6.5  by simp
     6.6  
     6.7 -instance matrix :: ("{ord, zero}") ord
     6.8 -  le_matrix_def: "A \<le> B \<equiv> \<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i"
     6.9 -  less_def: "A < (B\<Colon>'a matrix) \<equiv> A \<le> B \<and> A \<noteq> B" ..
    6.10 +instantiation matrix :: ("{ord, zero}") ord
    6.11 +begin
    6.12 +
    6.13 +definition
    6.14 +  le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
    6.15 +
    6.16 +definition
    6.17 +  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
    6.18 +
    6.19 +instance ..
    6.20 +
    6.21 +end
    6.22  
    6.23  instance matrix :: ("{order, zero}") order
    6.24  apply intro_classes
     7.1 --- a/src/HOL/SizeChange/Criterion.thy	Wed Jan 02 15:14:15 2008 +0100
     7.2 +++ b/src/HOL/SizeChange/Criterion.thy	Wed Jan 02 15:14:17 2008 +0100
     7.3 @@ -15,14 +15,16 @@
     7.4      LESS ("\<down>")
     7.5    | LEQ ("\<Down>")
     7.6  
     7.7 -instance sedge :: one
     7.8 -  one_sedge_def: "1 \<equiv> \<Down>" ..
     7.9 +instantiation sedge :: comm_monoid_mult
    7.10 +begin
    7.11  
    7.12 -instance sedge :: times
    7.13 -  mult_sedge_def:" a * b \<equiv> if a = \<down> then \<down> else b" ..
    7.14 +definition
    7.15 +  one_sedge_def: "1 = \<Down>"
    7.16  
    7.17 -instance sedge :: comm_monoid_mult
    7.18 -proof
    7.19 +definition
    7.20 +  mult_sedge_def:" a * b = (if a = \<down> then \<down> else b)"
    7.21 +
    7.22 +instance  proof
    7.23    fix a b c :: sedge
    7.24    show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def)
    7.25    show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def)
    7.26 @@ -30,6 +32,8 @@
    7.27      by (cases a, simp) (cases b, auto)
    7.28  qed
    7.29  
    7.30 +end
    7.31 +
    7.32  lemma sedge_UNIV:
    7.33    "UNIV = { LESS, LEQ }"
    7.34  proof (intro equalityI subsetI)
     8.1 --- a/src/HOL/SizeChange/Graphs.thy	Wed Jan 02 15:14:15 2008 +0100
     8.2 +++ b/src/HOL/SizeChange/Graphs.thy	Wed Jan 02 15:14:17 2008 +0100
     8.3 @@ -14,7 +14,7 @@
     8.4  datatype ('a, 'b) graph = 
     8.5    Graph "('a \<times> 'b \<times> 'a) set"
     8.6  
     8.7 -fun dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
     8.8 +primrec dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
     8.9    where "dest_graph (Graph G) = G"
    8.10  
    8.11  lemma graph_dest_graph[simp]:
    8.12 @@ -60,29 +60,47 @@
    8.13    by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
    8.14  
    8.15  
    8.16 -instance graph :: (type, type) "{comm_monoid_add}"
    8.17 -  graph_zero_def: "0 == Graph {}" 
    8.18 -  graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)"
    8.19 -proof
    8.20 +instantiation graph :: (type, type) comm_monoid_add
    8.21 +begin
    8.22 +
    8.23 +definition
    8.24 +  graph_zero_def: "0 = Graph {}" 
    8.25 +
    8.26 +definition
    8.27 +  graph_plus_def [code func del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
    8.28 +
    8.29 +instance proof
    8.30    fix x y z :: "('a,'b) graph"
    8.31 -
    8.32    show "x + y + z = x + (y + z)" 
    8.33     and "x + y = y + x" 
    8.34     and "0 + x = x"
    8.35 -  unfolding graph_plus_def graph_zero_def 
    8.36 -  by auto
    8.37 +  unfolding graph_plus_def graph_zero_def by auto
    8.38  qed
    8.39  
    8.40 -lemmas [code func del] = graph_plus_def
    8.41 +end
    8.42 +
    8.43 +instantiation graph :: (type, type) "{distrib_lattice, complete_lattice}"
    8.44 +begin
    8.45 +
    8.46 +definition
    8.47 +  graph_leq_def [code func del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
    8.48 +
    8.49 +definition
    8.50 +  graph_less_def [code func del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
    8.51  
    8.52 -instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
    8.53 -  graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
    8.54 -  graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
    8.55 -  "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
    8.56 -  "sup (G \<Colon> ('a, 'b) graph)  H \<equiv> G + H"
    8.57 -  Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
    8.58 -  Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))"
    8.59 -proof
    8.60 +definition
    8.61 +  [code func del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
    8.62 +
    8.63 +definition
    8.64 +  [code func del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
    8.65 +
    8.66 +definition
    8.67 +  Inf_graph_def [code func del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
    8.68 +
    8.69 +definition
    8.70 +  Sup_graph_def [code func del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
    8.71 +
    8.72 +instance proof
    8.73    fix x y z :: "('a,'b) graph"
    8.74    fix A :: "('a, 'b) graph set"
    8.75  
    8.76 @@ -130,8 +148,7 @@
    8.77      unfolding Sup_graph_def graph_leq_def by auto }
    8.78  qed
    8.79  
    8.80 -lemmas [code func del] = graph_leq_def graph_less_def
    8.81 -  inf_graph_def sup_graph_def Inf_graph_def Sup_graph_def
    8.82 +end
    8.83  
    8.84  lemma in_grplus:
    8.85    "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
    8.86 @@ -144,9 +161,13 @@
    8.87  
    8.88  subsubsection {* Multiplicative Structure *}
    8.89  
    8.90 -instance graph :: (type, times) mult_zero
    8.91 -  graph_mult_def: "G * H == grcomp G H" 
    8.92 -proof
    8.93 +instantiation graph :: (type, times) mult_zero
    8.94 +begin
    8.95 +
    8.96 +definition
    8.97 +  graph_mult_def [code func del]: "G * H = grcomp G H" 
    8.98 +
    8.99 +instance proof
   8.100    fix a :: "('a, 'b) graph"
   8.101  
   8.102    show "0 * a = 0" 
   8.103 @@ -157,10 +178,17 @@
   8.104      by (cases a) (simp add:grcomp.simps)
   8.105  qed
   8.106  
   8.107 -lemmas [code func del] = graph_mult_def
   8.108 +end
   8.109 +
   8.110 +instantiation graph :: (type, one) one 
   8.111 +begin
   8.112  
   8.113 -instance graph :: (type, one) one 
   8.114 -  graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
   8.115 +definition
   8.116 +  graph_one_def: "1 = Graph { (x, 1, x) |x. True}"
   8.117 +
   8.118 +instance ..
   8.119 +
   8.120 +end
   8.121  
   8.122  lemma in_grcomp:
   8.123    "has_edge (G * H) p b q
   8.124 @@ -190,16 +218,18 @@
   8.125    qed
   8.126  qed
   8.127  
   8.128 -fun grpow :: "nat \<Rightarrow> ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a, 'b) graph"
   8.129 -where
   8.130 -  "grpow 0 A = 1"
   8.131 -| "grpow (Suc n) A = A * (grpow n A)"
   8.132 +instantiation graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower, star}"
   8.133 +begin
   8.134  
   8.135 -instance graph :: (type, monoid_mult)
   8.136 -  "{semiring_1,idem_add,recpower,star}"
   8.137 -  graph_pow_def: "A ^ n == grpow n A"
   8.138 -  graph_star_def: "star (G \<Colon> ('a, 'b) graph) == (SUP n. G ^ n)" 
   8.139 -proof
   8.140 +primrec power_graph :: "('a\<Colon>type, 'b\<Colon>monoid_mult) graph \<Rightarrow> nat => ('a, 'b) graph"
   8.141 +where
   8.142 +  "(A \<Colon> ('a, 'b) graph) ^ 0 = 1"
   8.143 +| "(A \<Colon> ('a, 'b) graph) ^ Suc n = A * (A ^ n)"
   8.144 +
   8.145 +definition
   8.146 +  graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)" 
   8.147 +
   8.148 +instance proof
   8.149    fix a b c :: "('a, 'b) graph"
   8.150    
   8.151    show "1 * a = a" 
   8.152 @@ -219,9 +249,11 @@
   8.153    show "a + a = a" unfolding graph_plus_def by simp
   8.154    
   8.155    show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n"
   8.156 -    unfolding graph_pow_def by simp_all
   8.157 +    by simp_all
   8.158  qed
   8.159  
   8.160 +end
   8.161 +
   8.162  lemma graph_leqI:
   8.163    assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   8.164    shows "G \<le> H"
   8.165 @@ -309,7 +341,7 @@
   8.166  
   8.167  lemma in_tcl: 
   8.168    "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
   8.169 -  apply (auto simp: tcl_is_SUP in_SUP)
   8.170 +  apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps)
   8.171    apply (rule_tac x = "n - 1" in exI, auto)
   8.172    done
   8.173  
     9.1 --- a/src/HOL/ZF/Games.thy	Wed Jan 02 15:14:15 2008 +0100
     9.2 +++ b/src/HOL/ZF/Games.thy	Wed Jan 02 15:14:17 2008 +0100
     9.3 @@ -850,15 +850,30 @@
     9.4    by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def
     9.5      eq_game_sym intro: eq_game_refl eq_game_trans)
     9.6  
     9.7 -instance Pg :: "{ord,zero,plus,minus}" ..
     9.8 +instantiation Pg :: "{ord, zero, plus, minus, uminus}"
     9.9 +begin
    9.10 +
    9.11 +definition
    9.12 +  Pg_zero_def: "0 = Abs_Pg (eq_game_rel `` {zero_game})"
    9.13 +
    9.14 +definition
    9.15 +  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))"
    9.16 +
    9.17 +definition
    9.18 +  Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
    9.19  
    9.20 -defs (overloaded)
    9.21 -  Pg_zero_def: "0 \<equiv> Abs_Pg (eq_game_rel `` {zero_game})"
    9.22 -  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)"
    9.23 -  Pg_less_def: "G < H \<equiv> G \<le> H \<and> G \<noteq> (H::Pg)"
    9.24 -  Pg_minus_def: "- G \<equiv> contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
    9.25 -  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)})})"
    9.26 -  Pg_diff_def: "G - H \<equiv> G + (- (H::Pg))"
    9.27 +definition
    9.28 +  Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
    9.29 +
    9.30 +definition
    9.31 +  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)})})"
    9.32 +
    9.33 +definition
    9.34 +  Pg_diff_def: "G - H = G + (- (H::Pg))"
    9.35 +
    9.36 +instance ..
    9.37 +
    9.38 +end
    9.39  
    9.40  lemma Rep_Abs_eq_Pg[simp]: "Rep_Pg (Abs_Pg (eq_game_rel `` {g})) = eq_game_rel `` {g}"
    9.41    apply (subst Abs_Pg_inverse)