# HG changeset patch
# User haftmann
# Date 1199283242 -3600
# Node ID c03e9d04b3e408b9e32f077a94f6fe1d63f80eb0
# Parent  466e714de2fcc70a1bb5fcf0e7fcfca8f698c7eb
splitted class uminus from class minus

diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -23,7 +23,7 @@
 
 subsection {* Ring axioms *}
 
-axclass ring < zero, one, plus, minus, times, inverse, power, Divides.div
+axclass ring < zero, one, plus, minus, uminus, times, inverse, power, Divides.div
 
   a_assoc:      "(a + b) + c = a + (b + c)"
   l_zero:       "0 + a = a"
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -181,6 +181,6 @@
   "EVAL (y::'a::domain)
     (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
    x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
-  by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
+  by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
 
 end
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -77,32 +77,95 @@
 
 text {* Ring operations *}
 
-instance up :: (zero) zero ..
-instance up :: (one) one ..
-instance up :: (plus) plus ..
-instance up :: (minus) minus ..
-instance up :: (times) times ..
-instance up :: (Divides.div) Divides.div ..
-instance up :: (inverse) inverse ..
-instance up :: (power) power ..
+instantiation up :: (zero) zero
+begin
+
+definition
+  up_zero_def: "0 = monom 0 0"
+
+instance ..
+
+end
+
+instantiation up :: ("{one, zero}") one
+begin
+
+definition
+  up_one_def: "1 = monom 1 0"
+
+instance ..
+
+end
+
+instantiation up :: ("{plus, zero}") plus
+begin
+
+definition
+  up_add_def:	"p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
+
+instance ..
 
-defs
-  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
-  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
+end
+
+instantiation up :: ("{one, times, uminus, zero}") uminus
+begin
+
+definition
+  (* note: - 1 is different from -1; latter is of class number *)
+  up_uminus_def:"- p = (- 1) *s p"
+  (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
+
+instance ..
+
+end
+
+instantiation up :: ("{one, plus, times, minus, uminus, zero}") minus
+begin
+
+definition
+  up_minus_def: "(a :: 'a up) - b = a + (-b)"
+
+instance ..
+
+end
+
+instantiation up :: ("{times, comm_monoid_add}") times
+begin
+
+definition
+  up_mult_def:  "p * q = Abs_UP (%n::nat. setsum
 		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
-  up_zero_def:  "0 == monom 0 0"
-  up_one_def:   "1 == monom 1 0"
-  up_uminus_def:"- p == (- 1) *s p"
-                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
-                (* note: - 1 is different from -1; latter is of class number *)
+
+instance ..
+
+end
+
+instance up :: (type) Divides.div ..
+
+instantiation up :: ("{times, one, comm_monoid_add}") inverse
+begin
+
+definition
+  up_inverse_def: "inverse (a :: 'a up) = (if a dvd 1 then
+                     THE x. a * x = 1 else 0)"
 
-  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
-  up_inverse_def: "inverse (a::'a::{zero, one, Divides.div, inverse} up) == 
-                     (if a dvd 1 then THE x. a*x = 1 else 0)"
-  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
-  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
-                     nat_rec 1 (%u b. b * a) n"
+definition
+  up_divide_def:  "(a :: 'a up) / b = a * inverse b"
+
+instance ..
+
+end
 
+instantiation up :: ("{times, one, comm_monoid_add}") power
+begin
+
+primrec power_up where
+  "(a \<Colon> 'a up) ^ 0 = 1"
+  | "(a \<Colon> 'a up) ^ Suc n = a ^ n * a"
+
+instance ..
+
+end
 
 subsection {* Effect of operations on coefficients *}
 
@@ -294,7 +357,7 @@
     by (simp add: up_divide_def)
   fix n
   show "p ^ n = nat_rec 1 (%u b. b * p) n"
-    by (simp add: up_power_def)
+    by (induct n) simp_all
   qed
 
 (* Further properties of monom *)
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/HOL.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -221,8 +221,10 @@
   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
 
 class minus = type +
+  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
+
+class uminus = type +
   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
-    and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
 
 class times = type +
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Hyperreal/StarDef.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -469,12 +469,19 @@
 
 end
 
-instantiation star :: (minus) minus
+instantiation star :: (uminus) uminus
 begin
 
 definition
   star_minus_def:   "uminus \<equiv> *f* uminus"
 
+instance ..
+
+end
+
+instantiation star :: (minus) minus
+begin
+
 definition
   star_diff_def:    "(op -) \<equiv> *f2* (op -)"
 
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Import/HOL/realax.imp
--- a/src/HOL/Import/HOL/realax.imp	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Import/HOL/realax.imp	Wed Jan 02 15:14:02 2008 +0100
@@ -27,7 +27,7 @@
   "treal_add" > "HOL4Real.realax.treal_add"
   "treal_1" > "HOL4Real.realax.treal_1"
   "treal_0" > "HOL4Real.realax.treal_0"
-  "real_neg" > "HOL.minus_class.uminus" :: "real => real"
+  "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
   "real_mul" > "HOL.times_class.times" :: "real => real => real"
   "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
   "real_add" > "HOL.plus_class.plus" :: "real => real => real"
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/IntDef.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -22,7 +22,7 @@
   int = "UNIV//intrel"
   by (auto simp add: quotient_def)
 
-instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}"
+instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
 
 definition
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/OrderedGroup.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -121,7 +121,7 @@
 
 subsection {* Groups *}
 
-class group_add = minus + monoid_add +
+class group_add = minus + uminus + monoid_add +
   assumes left_minus [simp]: "- a + a = 0"
   assumes diff_minus: "a - b = a + (- b)"
 begin
@@ -219,7 +219,7 @@
 
 end
 
-class ab_group_add = minus + comm_monoid_add +
+class ab_group_add = minus + uminus + comm_monoid_add +
   assumes ab_left_minus: "- a + a = 0"
   assumes ab_diff_minus: "a - b = a + (- b)"
 begin
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -104,7 +104,7 @@
 
 definition
   norm_pres_extensions ::
-    "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
+    "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
       \<Rightarrow> 'a graph set" where
     "norm_pres_extensions E p F f
       = {g. \<exists>H h. g = graph H h
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -13,6 +13,7 @@
 *}
 
 locale linearform = var V + var f +
+  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
   assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
     and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
 
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -19,6 +19,7 @@
   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
 
 locale seminorm = var V + norm_syntax +
+  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
   assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
     and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
     and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -17,6 +17,7 @@
 *}
 
 locale subspace = var U + var V +
+  constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
   assumes non_empty [iff, intro]: "U \<noteq> {}"
     and subset [iff]: "U \<subseteq> V"
     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/Rational.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -6,7 +6,7 @@
 header {* Rational numbers *}
 
 theory Rational
-imports Abstract_Rat
+imports "~~/src/HOL/Library/Abstract_Rat"
 uses ("rat_arith.ML")
 begin
 
@@ -163,7 +163,7 @@
 
 subsubsection {* Standard operations on rational numbers *}
 
-instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+instantiation rat :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
 begin
 
 definition
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/RealDef.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -25,7 +25,7 @@
   real_of_preal :: "preal => real" where
   "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
 
-instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
 begin
 
 definition
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Ring_and_Field.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -516,10 +516,10 @@
 
 end
 
-class abs_if = minus + ord + zero + abs +
-  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
-
-class sgn_if = sgn + zero + one + minus + ord +
+class abs_if = minus + uminus + ord + zero + abs +
+  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
+
+class sgn_if = minus + uminus + zero + one + ord + sgn +
   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
 
 lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Set.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -352,10 +352,17 @@
 begin
 
 definition
-  Compl_def [code func del]:    "- A   = {x. ~x:A}"
+  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
+
+instance ..
+
+end
+
+instantiation set :: (type) uminus
+begin
 
 definition
-  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
+  Compl_def [code func del]:    "- A   = {x. ~x:A}"
 
 instance ..
 
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Wed Jan 02 15:14:02 2008 +0100
@@ -19,28 +19,28 @@
 val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
                addcongs [if_weak_cong, @{thm "let_weak_cong"}];*)
 val allowed_consts = 
-  [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, 
-   @{term "op - :: int => _"}, @{term "op - :: nat => _"}, 
-   @{term "op * :: int => _"}, @{term "op * :: nat => _"}, 
-   @{term "op div :: int => _"}, @{term "op div :: nat => _"}, 
-   @{term "op mod :: int => _"}, @{term "op mod :: nat => _"}, 
+  [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
+   @{term "op - :: int => _"}, @{term "op - :: nat => _"},
+   @{term "op * :: int => _"}, @{term "op * :: nat => _"},
+   @{term "op div :: int => _"}, @{term "op div :: nat => _"},
+   @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
    @{term "Numeral.Bit"},
    @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
-   @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"}, 
+   @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
-   @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, 
-   @{term "abs :: int => _"},  (*@ {term "abs :: nat => _"}, *)
-   @{term "max :: int => _"},  @{term "max :: nat => _"}, 
-   @{term "min :: int => _"},  @{term "min :: nat => _"}, 
-   @{term "HOL.uminus :: int => _"}, @{term "HOL.uminus :: nat => _"}, 
-   @{term "Not"}, @{term "Suc"}, 
-   @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"}, 
-   @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"}, 
+   @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
+   @{term "abs :: int => _"},
+   @{term "max :: int => _"}, @{term "max :: nat => _"},
+   @{term "min :: int => _"}, @{term "min :: nat => _"},
+   @{term "HOL.uminus :: int => _"}, (*@ {term "HOL.uminus :: nat => _"},*)
+   @{term "Not"}, @{term "Suc"},
+   @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
+   @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
    @{term "nat"}, @{term "int"},
    @{term "Numeral.bit.B0"},@{term "Numeral.bit.B1"}, 
    @{term "Numeral.Bit"}, @{term "Numeral.Pls"}, @{term "Numeral.Min"},
-   @{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"}, 
+   @{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"},
    @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    @{term "True"}, @{term "False"}];
 
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/BinOperations.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -17,16 +17,28 @@
 
 text "bit-wise logical operations on the int type"
 
-instance int :: bit
-  int_not_def: "bitNOT \<equiv> bin_rec Numeral.Min Numeral.Pls 
+instantiation int :: bit
+begin
+
+definition
+  int_not_def: "bitNOT = bin_rec Numeral.Min Numeral.Pls 
     (\<lambda>w b s. s BIT (NOT b))"
-  int_and_def: "bitAND \<equiv> bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y) 
+
+definition
+  int_and_def: "bitAND = bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y) 
     (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
-  int_or_def: "bitOR \<equiv> bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min) 
+
+definition
+  int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min) 
     (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
-  int_xor_def: "bitXOR \<equiv> bin_rec (\<lambda>x. x) bitNOT 
+
+definition
+  int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
     (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
-  ..
+
+instance ..
+
+end
 
 lemma int_not_simps [simp]:
   "NOT Numeral.Pls = Numeral.Min"
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Word/BitSyntax.thy
--- a/src/HOL/Word/BitSyntax.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/BitSyntax.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -45,12 +45,24 @@
 
 subsection {* Bitwise operations on type @{typ bit} *}
 
-instance bit :: bit
-  NOT_bit_def: "NOT x \<equiv> case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0"
-  AND_bit_def: "x AND y \<equiv> case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y"
-  OR_bit_def: "x OR y :: bit \<equiv> NOT (NOT x AND NOT y)"
-  XOR_bit_def: "x XOR y :: bit \<equiv> (x AND NOT y) OR (NOT x AND y)"
-  ..
+instantiation bit :: bit
+begin
+
+definition
+  NOT_bit_def: "NOT x = (case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0)"
+
+definition
+  AND_bit_def: "x AND y = (case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y)"
+
+definition
+  OR_bit_def: "(x OR y \<Colon> bit) = NOT (NOT x AND NOT y)"
+
+definition
+  XOR_bit_def: "(x XOR y \<Colon> bit) = (x AND NOT y) OR (NOT x AND y)"
+
+instance  ..
+
+end
 
 lemma bit_simps [simp]:
   "NOT bit.B0 = bit.B1"
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/WordArith.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -25,7 +25,7 @@
 interpretation signed: linorder ["word_sle" "word_sless"] 
   by (rule signed_linorder)
 
-lemmas word_arith_wis [THEN meta_eq_to_obj_eq] = 
+lemmas word_arith_wis = 
   word_add_def word_mult_def word_minus_def 
   word_succ_def word_pred_def word_0_wi word_1_wi
 
@@ -207,7 +207,7 @@
 (* now, to get the weaker results analogous to word_div/mod_def *)
 
 lemmas word_arith_alts = 
-  word_sub_wi [unfolded succ_def pred_def, THEN meta_eq_to_obj_eq, standard]
+  word_sub_wi [unfolded succ_def pred_def, standard]
   word_arith_wis [unfolded succ_def pred_def, standard]
 
 lemmas word_sub_alt = word_arith_alts (1)
@@ -247,9 +247,9 @@
     len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
 
 lemmas uint_div_alt = word_div_def
-  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
+  [THEN trans [OF uint_cong int_word_uint], standard]
 lemmas uint_mod_alt = word_mod_def
-  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
+  [THEN trans [OF uint_cong int_word_uint], standard]
 
 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
   unfolding word_pred_def number_of_eq
@@ -791,7 +791,7 @@
 instance word :: (len0) order ..
 
 instance word :: (len) recpower
-  by (intro_classes) (simp_all add: word_pow)
+  by (intro_classes) simp_all
 
 (* note that iszero_def is only for class comm_semiring_1_cancel,
    which requires word length >= 1, ie 'a :: len word *) 
@@ -990,7 +990,7 @@
 
 lemmas un_ui_le = trans 
   [OF word_le_nat_alt [symmetric] 
-      word_le_def [THEN meta_eq_to_obj_eq], 
+      word_le_def, 
    standard]
 
 lemma unat_sub_if_size:
diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/WordDefinition.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -13,28 +13,27 @@
 typedef (open word) 'a word
   = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
 
-instance word :: (len0) number ..
-instance word :: (type) minus ..
-instance word :: (type) plus ..
-instance word :: (type) one ..
-instance word :: (type) zero ..
-instance word :: (type) times ..
-instance word :: (type) Divides.div ..
-instance word :: (type) power ..
-instance word :: (type) ord ..
-instance word :: (type) size ..
-instance word :: (type) inverse ..
-instance word :: (type) bit ..
+instantiation word :: (len0) size
+begin
+
+definition
+  word_size: "size (w :: 'a word) = len_of TYPE('a)"
+
+instance ..
+
+end
+
+definition
+  -- {* representation of words using unsigned or signed bins, 
+        only difference in these is the type class *}
+  word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
+where
+  "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
 
 
 subsection "Type conversions and casting"
 
 constdefs
-  -- {* representation of words using unsigned or signed bins, 
-        only difference in these is the type class *}
-  word_of_int :: "int => 'a :: len0 word"
-  "word_of_int w == Abs_word (bintrunc (len_of TYPE ('a)) w)" 
-
   -- {* uint and sint cast a word to an integer,
         uint treats the word as unsigned,
         sint treats the most-significant-bit as a sign bit *}
@@ -81,10 +80,6 @@
   word_reverse :: "'a :: len0 word => 'a word"
   "word_reverse w == of_bl (rev (to_bl w))"
 
-defs (overloaded)
-  word_size: "size (w :: 'a :: len0 word) == len_of TYPE('a)"
-  word_number_of_def: "number_of w == word_of_int w"
-
 constdefs
   word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b"
   "word_int_case f w == f (uint w)"
@@ -97,20 +92,82 @@
 
 subsection  "Arithmetic operations"
 
-defs (overloaded)
-  word_1_wi: "(1 :: ('a :: len0) word) == word_of_int 1"
-  word_0_wi: "(0 :: ('a :: len0) word) == word_of_int 0"
+instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
+begin
+
+definition
+  word_0_wi: "0 = word_of_int 0"
+
+definition
+  word_1_wi: "1 = word_of_int 1"
+
+definition
+  word_add_def: "a + b = word_of_int (uint a + uint b)"
+
+definition
+  word_sub_wi: "a - b = word_of_int (uint a - uint b)"
+
+definition
+  word_minus_def: "- a = word_of_int (- uint a)"
+
+definition
+  word_mult_def: "a * b = word_of_int (uint a * uint b)"
+
+definition
+  word_div_def: "a div b = word_of_int (uint a div uint b)"
+
+definition
+  word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
+
+primrec power_word where
+  "(a\<Colon>'a word) ^ 0 = 1"
+  | "(a\<Colon>'a word) ^ Suc n = a * a ^ n"
+
+definition
+  word_number_of_def: "number_of w = word_of_int w"
+
+definition
+  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
 
-  word_le_def: "a <= b == uint a <= uint b"
-  word_less_def: "x < y == x <= y & x ~= (y :: 'a :: len0 word)"
+definition
+  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
+
+definition
+  word_and_def: 
+  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
+
+definition
+  word_or_def:  
+  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
+
+definition
+  word_xor_def: 
+  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
+
+definition
+  word_not_def: 
+  "NOT (a::'a word) = word_of_int (NOT (uint a))"
+
+instance ..
+
+end 
+
+abbreviation
+  word_power :: "'a\<Colon>len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
+where
+  "word_power == op ^"
+
+definition
+  word_succ :: "'a :: len0 word => 'a word"
+where
+  "word_succ a = word_of_int (Numeral.succ (uint a))"
+
+definition
+  word_pred :: "'a :: len0 word => 'a word"
+where
+  "word_pred a = word_of_int (Numeral.pred (uint a))"
 
 constdefs
-  word_succ :: "'a :: len0 word => 'a word"
-  "word_succ a == word_of_int (Numeral.succ (uint a))"
-
-  word_pred :: "'a :: len0 word => 'a word"
-  "word_pred a == word_of_int (Numeral.pred (uint a))"
-
   udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
   "a udvd b == EX n>=0. uint b = n * uint a"
 
@@ -120,37 +177,10 @@
   word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
   "(x <s y) == (x <=s y & x ~= y)"
 
-consts
-  word_power :: "'a :: len0 word => nat => 'a word"
-primrec
-  "word_power a 0 = 1"
-  "word_power a (Suc n) = a * word_power a n"
-
-defs (overloaded)
-  word_pow: "power == word_power"
-  word_add_def: "a + b == word_of_int (uint a + uint b)"
-  word_sub_wi: "a - b == word_of_int (uint a - uint b)"
-  word_minus_def: "- a == word_of_int (- uint a)"
-  word_mult_def: "a * b == word_of_int (uint a * uint b)"
-  word_div_def: "a div b == word_of_int (uint a div uint b)"
-  word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
-
 
 subsection "Bit-wise operations"
 
 defs (overloaded)
-  word_and_def: 
-  "(a::'a::len0 word) AND b == word_of_int (uint a AND uint b)"
-
-  word_or_def:  
-  "(a::'a::len0 word) OR b == word_of_int (uint a OR uint b)"
-
-  word_xor_def: 
-  "(a::'a::len0 word) XOR b == word_of_int (uint a XOR uint b)"
-
-  word_not_def: 
-  "NOT (a::'a::len0 word) == word_of_int (NOT (uint a))"
-
   word_test_bit_def: 
   "test_bit (a::'a::len0 word) == bin_nth (uint a)"
 
@@ -269,7 +299,7 @@
 lemmas of_nth_def = word_set_bits_def
 
 lemmas word_size_gt_0 [iff] = 
-  xtr1 [OF word_size [THEN meta_eq_to_obj_eq] len_gt_0, standard]
+  xtr1 [OF word_size len_gt_0, standard]
 lemmas lens_gt_0 = word_size_gt_0 len_gt_0
 lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
 
@@ -701,9 +731,9 @@
   done
 
 lemmas num_abs_bintr = sym [THEN trans,
-  OF num_of_bintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
+  OF num_of_bintr word_number_of_def, standard]
 lemmas num_abs_sbintr = sym [THEN trans,
-  OF num_of_sbintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
+  OF num_of_sbintr word_number_of_def, standard]
   
 (** cast - note, no arg for new length, as it's determined by type of result,
   thus in "cast w = w, the type means cast to length of w! **)