splitted class uminus from class minus
authorhaftmann
Wed Jan 02 15:14:02 2008 +0100 (2008-01-02)
changeset 25762c03e9d04b3e4
parent 25761 466e714de2fc
child 25763 474f8ba9dfa9
splitted class uminus from class minus
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/PolyHomo.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/StarDef.thy
src/HOL/Import/HOL/realax.imp
src/HOL/IntDef.thy
src/HOL/OrderedGroup.thy
src/HOL/Real/HahnBanach/FunctionOrder.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Ring_and_Field.thy
src/HOL/Set.thy
src/HOL/Tools/Qelim/cooper_data.ML
src/HOL/Word/BinOperations.thy
src/HOL/Word/BitSyntax.thy
src/HOL/Word/WordArith.thy
src/HOL/Word/WordDefinition.thy
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Jan 02 12:22:38 2008 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Jan 02 15:14:02 2008 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  subsection {* Ring axioms *}
     1.6  
     1.7 -axclass ring < zero, one, plus, minus, times, inverse, power, Divides.div
     1.8 +axclass ring < zero, one, plus, minus, uminus, times, inverse, power, Divides.div
     1.9  
    1.10    a_assoc:      "(a + b) + c = a + (b + c)"
    1.11    l_zero:       "0 + a = a"
     2.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Wed Jan 02 12:22:38 2008 +0100
     2.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy	Wed Jan 02 15:14:02 2008 +0100
     2.3 @@ -181,6 +181,6 @@
     2.4    "EVAL (y::'a::domain)
     2.5      (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
     2.6     x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
     2.7 -  by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
     2.8 +  by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
     2.9  
    2.10  end
     3.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jan 02 12:22:38 2008 +0100
     3.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jan 02 15:14:02 2008 +0100
     3.3 @@ -77,32 +77,95 @@
     3.4  
     3.5  text {* Ring operations *}
     3.6  
     3.7 -instance up :: (zero) zero ..
     3.8 -instance up :: (one) one ..
     3.9 -instance up :: (plus) plus ..
    3.10 -instance up :: (minus) minus ..
    3.11 -instance up :: (times) times ..
    3.12 -instance up :: (Divides.div) Divides.div ..
    3.13 -instance up :: (inverse) inverse ..
    3.14 -instance up :: (power) power ..
    3.15 +instantiation up :: (zero) zero
    3.16 +begin
    3.17 +
    3.18 +definition
    3.19 +  up_zero_def: "0 = monom 0 0"
    3.20 +
    3.21 +instance ..
    3.22 +
    3.23 +end
    3.24 +
    3.25 +instantiation up :: ("{one, zero}") one
    3.26 +begin
    3.27 +
    3.28 +definition
    3.29 +  up_one_def: "1 = monom 1 0"
    3.30 +
    3.31 +instance ..
    3.32 +
    3.33 +end
    3.34 +
    3.35 +instantiation up :: ("{plus, zero}") plus
    3.36 +begin
    3.37 +
    3.38 +definition
    3.39 +  up_add_def:	"p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
    3.40 +
    3.41 +instance ..
    3.42  
    3.43 -defs
    3.44 -  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
    3.45 -  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
    3.46 +end
    3.47 +
    3.48 +instantiation up :: ("{one, times, uminus, zero}") uminus
    3.49 +begin
    3.50 +
    3.51 +definition
    3.52 +  (* note: - 1 is different from -1; latter is of class number *)
    3.53 +  up_uminus_def:"- p = (- 1) *s p"
    3.54 +  (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
    3.55 +
    3.56 +instance ..
    3.57 +
    3.58 +end
    3.59 +
    3.60 +instantiation up :: ("{one, plus, times, minus, uminus, zero}") minus
    3.61 +begin
    3.62 +
    3.63 +definition
    3.64 +  up_minus_def: "(a :: 'a up) - b = a + (-b)"
    3.65 +
    3.66 +instance ..
    3.67 +
    3.68 +end
    3.69 +
    3.70 +instantiation up :: ("{times, comm_monoid_add}") times
    3.71 +begin
    3.72 +
    3.73 +definition
    3.74 +  up_mult_def:  "p * q = Abs_UP (%n::nat. setsum
    3.75  		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
    3.76 -  up_zero_def:  "0 == monom 0 0"
    3.77 -  up_one_def:   "1 == monom 1 0"
    3.78 -  up_uminus_def:"- p == (- 1) *s p"
    3.79 -                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
    3.80 -                (* note: - 1 is different from -1; latter is of class number *)
    3.81 +
    3.82 +instance ..
    3.83 +
    3.84 +end
    3.85 +
    3.86 +instance up :: (type) Divides.div ..
    3.87 +
    3.88 +instantiation up :: ("{times, one, comm_monoid_add}") inverse
    3.89 +begin
    3.90 +
    3.91 +definition
    3.92 +  up_inverse_def: "inverse (a :: 'a up) = (if a dvd 1 then
    3.93 +                     THE x. a * x = 1 else 0)"
    3.94  
    3.95 -  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
    3.96 -  up_inverse_def: "inverse (a::'a::{zero, one, Divides.div, inverse} up) == 
    3.97 -                     (if a dvd 1 then THE x. a*x = 1 else 0)"
    3.98 -  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
    3.99 -  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
   3.100 -                     nat_rec 1 (%u b. b * a) n"
   3.101 +definition
   3.102 +  up_divide_def:  "(a :: 'a up) / b = a * inverse b"
   3.103 +
   3.104 +instance ..
   3.105 +
   3.106 +end
   3.107  
   3.108 +instantiation up :: ("{times, one, comm_monoid_add}") power
   3.109 +begin
   3.110 +
   3.111 +primrec power_up where
   3.112 +  "(a \<Colon> 'a up) ^ 0 = 1"
   3.113 +  | "(a \<Colon> 'a up) ^ Suc n = a ^ n * a"
   3.114 +
   3.115 +instance ..
   3.116 +
   3.117 +end
   3.118  
   3.119  subsection {* Effect of operations on coefficients *}
   3.120  
   3.121 @@ -294,7 +357,7 @@
   3.122      by (simp add: up_divide_def)
   3.123    fix n
   3.124    show "p ^ n = nat_rec 1 (%u b. b * p) n"
   3.125 -    by (simp add: up_power_def)
   3.126 +    by (induct n) simp_all
   3.127    qed
   3.128  
   3.129  (* Further properties of monom *)
     4.1 --- a/src/HOL/HOL.thy	Wed Jan 02 12:22:38 2008 +0100
     4.2 +++ b/src/HOL/HOL.thy	Wed Jan 02 15:14:02 2008 +0100
     4.3 @@ -221,8 +221,10 @@
     4.4    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
     4.5  
     4.6  class minus = type +
     4.7 +  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
     4.8 +
     4.9 +class uminus = type +
    4.10    fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    4.11 -    and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    4.12  
    4.13  class times = type +
    4.14    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
     5.1 --- a/src/HOL/Hyperreal/StarDef.thy	Wed Jan 02 12:22:38 2008 +0100
     5.2 +++ b/src/HOL/Hyperreal/StarDef.thy	Wed Jan 02 15:14:02 2008 +0100
     5.3 @@ -469,12 +469,19 @@
     5.4  
     5.5  end
     5.6  
     5.7 -instantiation star :: (minus) minus
     5.8 +instantiation star :: (uminus) uminus
     5.9  begin
    5.10  
    5.11  definition
    5.12    star_minus_def:   "uminus \<equiv> *f* uminus"
    5.13  
    5.14 +instance ..
    5.15 +
    5.16 +end
    5.17 +
    5.18 +instantiation star :: (minus) minus
    5.19 +begin
    5.20 +
    5.21  definition
    5.22    star_diff_def:    "(op -) \<equiv> *f2* (op -)"
    5.23  
     6.1 --- a/src/HOL/Import/HOL/realax.imp	Wed Jan 02 12:22:38 2008 +0100
     6.2 +++ b/src/HOL/Import/HOL/realax.imp	Wed Jan 02 15:14:02 2008 +0100
     6.3 @@ -27,7 +27,7 @@
     6.4    "treal_add" > "HOL4Real.realax.treal_add"
     6.5    "treal_1" > "HOL4Real.realax.treal_1"
     6.6    "treal_0" > "HOL4Real.realax.treal_0"
     6.7 -  "real_neg" > "HOL.minus_class.uminus" :: "real => real"
     6.8 +  "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
     6.9    "real_mul" > "HOL.times_class.times" :: "real => real => real"
    6.10    "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
    6.11    "real_add" > "HOL.plus_class.plus" :: "real => real => real"
     7.1 --- a/src/HOL/IntDef.thy	Wed Jan 02 12:22:38 2008 +0100
     7.2 +++ b/src/HOL/IntDef.thy	Wed Jan 02 15:14:02 2008 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4    int = "UNIV//intrel"
     7.5    by (auto simp add: quotient_def)
     7.6  
     7.7 -instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}"
     7.8 +instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
     7.9  begin
    7.10  
    7.11  definition
     8.1 --- a/src/HOL/OrderedGroup.thy	Wed Jan 02 12:22:38 2008 +0100
     8.2 +++ b/src/HOL/OrderedGroup.thy	Wed Jan 02 15:14:02 2008 +0100
     8.3 @@ -121,7 +121,7 @@
     8.4  
     8.5  subsection {* Groups *}
     8.6  
     8.7 -class group_add = minus + monoid_add +
     8.8 +class group_add = minus + uminus + monoid_add +
     8.9    assumes left_minus [simp]: "- a + a = 0"
    8.10    assumes diff_minus: "a - b = a + (- b)"
    8.11  begin
    8.12 @@ -219,7 +219,7 @@
    8.13  
    8.14  end
    8.15  
    8.16 -class ab_group_add = minus + comm_monoid_add +
    8.17 +class ab_group_add = minus + uminus + comm_monoid_add +
    8.18    assumes ab_left_minus: "- a + a = 0"
    8.19    assumes ab_diff_minus: "a - b = a + (- b)"
    8.20  begin
     9.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Wed Jan 02 12:22:38 2008 +0100
     9.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Wed Jan 02 15:14:02 2008 +0100
     9.3 @@ -104,7 +104,7 @@
     9.4  
     9.5  definition
     9.6    norm_pres_extensions ::
     9.7 -    "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
     9.8 +    "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
     9.9        \<Rightarrow> 'a graph set" where
    9.10      "norm_pres_extensions E p F f
    9.11        = {g. \<exists>H h. g = graph H h
    10.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Wed Jan 02 12:22:38 2008 +0100
    10.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Wed Jan 02 15:14:02 2008 +0100
    10.3 @@ -13,6 +13,7 @@
    10.4  *}
    10.5  
    10.6  locale linearform = var V + var f +
    10.7 +  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    10.8    assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
    10.9      and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
   10.10  
    11.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Wed Jan 02 12:22:38 2008 +0100
    11.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Wed Jan 02 15:14:02 2008 +0100
    11.3 @@ -19,6 +19,7 @@
    11.4    fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    11.5  
    11.6  locale seminorm = var V + norm_syntax +
    11.7 +  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    11.8    assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
    11.9      and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
   11.10      and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    12.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Jan 02 12:22:38 2008 +0100
    12.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Jan 02 15:14:02 2008 +0100
    12.3 @@ -17,6 +17,7 @@
    12.4  *}
    12.5  
    12.6  locale subspace = var U + var V +
    12.7 +  constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
    12.8    assumes non_empty [iff, intro]: "U \<noteq> {}"
    12.9      and subset [iff]: "U \<subseteq> V"
   12.10      and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
    13.1 --- a/src/HOL/Real/Rational.thy	Wed Jan 02 12:22:38 2008 +0100
    13.2 +++ b/src/HOL/Real/Rational.thy	Wed Jan 02 15:14:02 2008 +0100
    13.3 @@ -6,7 +6,7 @@
    13.4  header {* Rational numbers *}
    13.5  
    13.6  theory Rational
    13.7 -imports Abstract_Rat
    13.8 +imports "~~/src/HOL/Library/Abstract_Rat"
    13.9  uses ("rat_arith.ML")
   13.10  begin
   13.11  
   13.12 @@ -163,7 +163,7 @@
   13.13  
   13.14  subsubsection {* Standard operations on rational numbers *}
   13.15  
   13.16 -instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
   13.17 +instantiation rat :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
   13.18  begin
   13.19  
   13.20  definition
    14.1 --- a/src/HOL/Real/RealDef.thy	Wed Jan 02 12:22:38 2008 +0100
    14.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jan 02 15:14:02 2008 +0100
    14.3 @@ -25,7 +25,7 @@
    14.4    real_of_preal :: "preal => real" where
    14.5    "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
    14.6  
    14.7 -instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
    14.8 +instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
    14.9  begin
   14.10  
   14.11  definition
    15.1 --- a/src/HOL/Ring_and_Field.thy	Wed Jan 02 12:22:38 2008 +0100
    15.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Jan 02 15:14:02 2008 +0100
    15.3 @@ -516,10 +516,10 @@
    15.4  
    15.5  end
    15.6  
    15.7 -class abs_if = minus + ord + zero + abs +
    15.8 -  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
    15.9 -
   15.10 -class sgn_if = sgn + zero + one + minus + ord +
   15.11 +class abs_if = minus + uminus + ord + zero + abs +
   15.12 +  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
   15.13 +
   15.14 +class sgn_if = minus + uminus + zero + one + ord + sgn +
   15.15    assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   15.16  
   15.17  lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
    16.1 --- a/src/HOL/Set.thy	Wed Jan 02 12:22:38 2008 +0100
    16.2 +++ b/src/HOL/Set.thy	Wed Jan 02 15:14:02 2008 +0100
    16.3 @@ -352,10 +352,17 @@
    16.4  begin
    16.5  
    16.6  definition
    16.7 -  Compl_def [code func del]:    "- A   = {x. ~x:A}"
    16.8 +  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
    16.9 +
   16.10 +instance ..
   16.11 +
   16.12 +end
   16.13 +
   16.14 +instantiation set :: (type) uminus
   16.15 +begin
   16.16  
   16.17  definition
   16.18 -  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
   16.19 +  Compl_def [code func del]:    "- A   = {x. ~x:A}"
   16.20  
   16.21  instance ..
   16.22  
    17.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Wed Jan 02 12:22:38 2008 +0100
    17.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Wed Jan 02 15:14:02 2008 +0100
    17.3 @@ -19,28 +19,28 @@
    17.4  val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
    17.5                 addcongs [if_weak_cong, @{thm "let_weak_cong"}];*)
    17.6  val allowed_consts = 
    17.7 -  [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, 
    17.8 -   @{term "op - :: int => _"}, @{term "op - :: nat => _"}, 
    17.9 -   @{term "op * :: int => _"}, @{term "op * :: nat => _"}, 
   17.10 -   @{term "op div :: int => _"}, @{term "op div :: nat => _"}, 
   17.11 -   @{term "op mod :: int => _"}, @{term "op mod :: nat => _"}, 
   17.12 +  [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
   17.13 +   @{term "op - :: int => _"}, @{term "op - :: nat => _"},
   17.14 +   @{term "op * :: int => _"}, @{term "op * :: nat => _"},
   17.15 +   @{term "op div :: int => _"}, @{term "op div :: nat => _"},
   17.16 +   @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
   17.17     @{term "Numeral.Bit"},
   17.18     @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
   17.19 -   @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"}, 
   17.20 +   @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
   17.21     @{term "op < :: int => _"}, @{term "op < :: nat => _"},
   17.22     @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
   17.23 -   @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, 
   17.24 -   @{term "abs :: int => _"},  (*@ {term "abs :: nat => _"}, *)
   17.25 -   @{term "max :: int => _"},  @{term "max :: nat => _"}, 
   17.26 -   @{term "min :: int => _"},  @{term "min :: nat => _"}, 
   17.27 -   @{term "HOL.uminus :: int => _"}, @{term "HOL.uminus :: nat => _"}, 
   17.28 -   @{term "Not"}, @{term "Suc"}, 
   17.29 -   @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"}, 
   17.30 -   @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"}, 
   17.31 +   @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
   17.32 +   @{term "abs :: int => _"},
   17.33 +   @{term "max :: int => _"}, @{term "max :: nat => _"},
   17.34 +   @{term "min :: int => _"}, @{term "min :: nat => _"},
   17.35 +   @{term "HOL.uminus :: int => _"}, (*@ {term "HOL.uminus :: nat => _"},*)
   17.36 +   @{term "Not"}, @{term "Suc"},
   17.37 +   @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
   17.38 +   @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
   17.39     @{term "nat"}, @{term "int"},
   17.40     @{term "Numeral.bit.B0"},@{term "Numeral.bit.B1"}, 
   17.41     @{term "Numeral.Bit"}, @{term "Numeral.Pls"}, @{term "Numeral.Min"},
   17.42 -   @{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"}, 
   17.43 +   @{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"},
   17.44     @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
   17.45     @{term "True"}, @{term "False"}];
   17.46  
    18.1 --- a/src/HOL/Word/BinOperations.thy	Wed Jan 02 12:22:38 2008 +0100
    18.2 +++ b/src/HOL/Word/BinOperations.thy	Wed Jan 02 15:14:02 2008 +0100
    18.3 @@ -17,16 +17,28 @@
    18.4  
    18.5  text "bit-wise logical operations on the int type"
    18.6  
    18.7 -instance int :: bit
    18.8 -  int_not_def: "bitNOT \<equiv> bin_rec Numeral.Min Numeral.Pls 
    18.9 +instantiation int :: bit
   18.10 +begin
   18.11 +
   18.12 +definition
   18.13 +  int_not_def: "bitNOT = bin_rec Numeral.Min Numeral.Pls 
   18.14      (\<lambda>w b s. s BIT (NOT b))"
   18.15 -  int_and_def: "bitAND \<equiv> bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y) 
   18.16 +
   18.17 +definition
   18.18 +  int_and_def: "bitAND = bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y) 
   18.19      (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
   18.20 -  int_or_def: "bitOR \<equiv> bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min) 
   18.21 +
   18.22 +definition
   18.23 +  int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min) 
   18.24      (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
   18.25 -  int_xor_def: "bitXOR \<equiv> bin_rec (\<lambda>x. x) bitNOT 
   18.26 +
   18.27 +definition
   18.28 +  int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
   18.29      (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
   18.30 -  ..
   18.31 +
   18.32 +instance ..
   18.33 +
   18.34 +end
   18.35  
   18.36  lemma int_not_simps [simp]:
   18.37    "NOT Numeral.Pls = Numeral.Min"
    19.1 --- a/src/HOL/Word/BitSyntax.thy	Wed Jan 02 12:22:38 2008 +0100
    19.2 +++ b/src/HOL/Word/BitSyntax.thy	Wed Jan 02 15:14:02 2008 +0100
    19.3 @@ -45,12 +45,24 @@
    19.4  
    19.5  subsection {* Bitwise operations on type @{typ bit} *}
    19.6  
    19.7 -instance bit :: bit
    19.8 -  NOT_bit_def: "NOT x \<equiv> case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0"
    19.9 -  AND_bit_def: "x AND y \<equiv> case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y"
   19.10 -  OR_bit_def: "x OR y :: bit \<equiv> NOT (NOT x AND NOT y)"
   19.11 -  XOR_bit_def: "x XOR y :: bit \<equiv> (x AND NOT y) OR (NOT x AND y)"
   19.12 -  ..
   19.13 +instantiation bit :: bit
   19.14 +begin
   19.15 +
   19.16 +definition
   19.17 +  NOT_bit_def: "NOT x = (case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0)"
   19.18 +
   19.19 +definition
   19.20 +  AND_bit_def: "x AND y = (case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y)"
   19.21 +
   19.22 +definition
   19.23 +  OR_bit_def: "(x OR y \<Colon> bit) = NOT (NOT x AND NOT y)"
   19.24 +
   19.25 +definition
   19.26 +  XOR_bit_def: "(x XOR y \<Colon> bit) = (x AND NOT y) OR (NOT x AND y)"
   19.27 +
   19.28 +instance  ..
   19.29 +
   19.30 +end
   19.31  
   19.32  lemma bit_simps [simp]:
   19.33    "NOT bit.B0 = bit.B1"
    20.1 --- a/src/HOL/Word/WordArith.thy	Wed Jan 02 12:22:38 2008 +0100
    20.2 +++ b/src/HOL/Word/WordArith.thy	Wed Jan 02 15:14:02 2008 +0100
    20.3 @@ -25,7 +25,7 @@
    20.4  interpretation signed: linorder ["word_sle" "word_sless"] 
    20.5    by (rule signed_linorder)
    20.6  
    20.7 -lemmas word_arith_wis [THEN meta_eq_to_obj_eq] = 
    20.8 +lemmas word_arith_wis = 
    20.9    word_add_def word_mult_def word_minus_def 
   20.10    word_succ_def word_pred_def word_0_wi word_1_wi
   20.11  
   20.12 @@ -207,7 +207,7 @@
   20.13  (* now, to get the weaker results analogous to word_div/mod_def *)
   20.14  
   20.15  lemmas word_arith_alts = 
   20.16 -  word_sub_wi [unfolded succ_def pred_def, THEN meta_eq_to_obj_eq, standard]
   20.17 +  word_sub_wi [unfolded succ_def pred_def, standard]
   20.18    word_arith_wis [unfolded succ_def pred_def, standard]
   20.19  
   20.20  lemmas word_sub_alt = word_arith_alts (1)
   20.21 @@ -247,9 +247,9 @@
   20.22      len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
   20.23  
   20.24  lemmas uint_div_alt = word_div_def
   20.25 -  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
   20.26 +  [THEN trans [OF uint_cong int_word_uint], standard]
   20.27  lemmas uint_mod_alt = word_mod_def
   20.28 -  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
   20.29 +  [THEN trans [OF uint_cong int_word_uint], standard]
   20.30  
   20.31  lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
   20.32    unfolding word_pred_def number_of_eq
   20.33 @@ -791,7 +791,7 @@
   20.34  instance word :: (len0) order ..
   20.35  
   20.36  instance word :: (len) recpower
   20.37 -  by (intro_classes) (simp_all add: word_pow)
   20.38 +  by (intro_classes) simp_all
   20.39  
   20.40  (* note that iszero_def is only for class comm_semiring_1_cancel,
   20.41     which requires word length >= 1, ie 'a :: len word *) 
   20.42 @@ -990,7 +990,7 @@
   20.43  
   20.44  lemmas un_ui_le = trans 
   20.45    [OF word_le_nat_alt [symmetric] 
   20.46 -      word_le_def [THEN meta_eq_to_obj_eq], 
   20.47 +      word_le_def, 
   20.48     standard]
   20.49  
   20.50  lemma unat_sub_if_size:
    21.1 --- a/src/HOL/Word/WordDefinition.thy	Wed Jan 02 12:22:38 2008 +0100
    21.2 +++ b/src/HOL/Word/WordDefinition.thy	Wed Jan 02 15:14:02 2008 +0100
    21.3 @@ -13,28 +13,27 @@
    21.4  typedef (open word) 'a word
    21.5    = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
    21.6  
    21.7 -instance word :: (len0) number ..
    21.8 -instance word :: (type) minus ..
    21.9 -instance word :: (type) plus ..
   21.10 -instance word :: (type) one ..
   21.11 -instance word :: (type) zero ..
   21.12 -instance word :: (type) times ..
   21.13 -instance word :: (type) Divides.div ..
   21.14 -instance word :: (type) power ..
   21.15 -instance word :: (type) ord ..
   21.16 -instance word :: (type) size ..
   21.17 -instance word :: (type) inverse ..
   21.18 -instance word :: (type) bit ..
   21.19 +instantiation word :: (len0) size
   21.20 +begin
   21.21 +
   21.22 +definition
   21.23 +  word_size: "size (w :: 'a word) = len_of TYPE('a)"
   21.24 +
   21.25 +instance ..
   21.26 +
   21.27 +end
   21.28 +
   21.29 +definition
   21.30 +  -- {* representation of words using unsigned or signed bins, 
   21.31 +        only difference in these is the type class *}
   21.32 +  word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
   21.33 +where
   21.34 +  "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
   21.35  
   21.36  
   21.37  subsection "Type conversions and casting"
   21.38  
   21.39  constdefs
   21.40 -  -- {* representation of words using unsigned or signed bins, 
   21.41 -        only difference in these is the type class *}
   21.42 -  word_of_int :: "int => 'a :: len0 word"
   21.43 -  "word_of_int w == Abs_word (bintrunc (len_of TYPE ('a)) w)" 
   21.44 -
   21.45    -- {* uint and sint cast a word to an integer,
   21.46          uint treats the word as unsigned,
   21.47          sint treats the most-significant-bit as a sign bit *}
   21.48 @@ -81,10 +80,6 @@
   21.49    word_reverse :: "'a :: len0 word => 'a word"
   21.50    "word_reverse w == of_bl (rev (to_bl w))"
   21.51  
   21.52 -defs (overloaded)
   21.53 -  word_size: "size (w :: 'a :: len0 word) == len_of TYPE('a)"
   21.54 -  word_number_of_def: "number_of w == word_of_int w"
   21.55 -
   21.56  constdefs
   21.57    word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b"
   21.58    "word_int_case f w == f (uint w)"
   21.59 @@ -97,20 +92,82 @@
   21.60  
   21.61  subsection  "Arithmetic operations"
   21.62  
   21.63 -defs (overloaded)
   21.64 -  word_1_wi: "(1 :: ('a :: len0) word) == word_of_int 1"
   21.65 -  word_0_wi: "(0 :: ('a :: len0) word) == word_of_int 0"
   21.66 +instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
   21.67 +begin
   21.68 +
   21.69 +definition
   21.70 +  word_0_wi: "0 = word_of_int 0"
   21.71 +
   21.72 +definition
   21.73 +  word_1_wi: "1 = word_of_int 1"
   21.74 +
   21.75 +definition
   21.76 +  word_add_def: "a + b = word_of_int (uint a + uint b)"
   21.77 +
   21.78 +definition
   21.79 +  word_sub_wi: "a - b = word_of_int (uint a - uint b)"
   21.80 +
   21.81 +definition
   21.82 +  word_minus_def: "- a = word_of_int (- uint a)"
   21.83 +
   21.84 +definition
   21.85 +  word_mult_def: "a * b = word_of_int (uint a * uint b)"
   21.86 +
   21.87 +definition
   21.88 +  word_div_def: "a div b = word_of_int (uint a div uint b)"
   21.89 +
   21.90 +definition
   21.91 +  word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
   21.92 +
   21.93 +primrec power_word where
   21.94 +  "(a\<Colon>'a word) ^ 0 = 1"
   21.95 +  | "(a\<Colon>'a word) ^ Suc n = a * a ^ n"
   21.96 +
   21.97 +definition
   21.98 +  word_number_of_def: "number_of w = word_of_int w"
   21.99 +
  21.100 +definition
  21.101 +  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
  21.102  
  21.103 -  word_le_def: "a <= b == uint a <= uint b"
  21.104 -  word_less_def: "x < y == x <= y & x ~= (y :: 'a :: len0 word)"
  21.105 +definition
  21.106 +  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
  21.107 +
  21.108 +definition
  21.109 +  word_and_def: 
  21.110 +  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
  21.111 +
  21.112 +definition
  21.113 +  word_or_def:  
  21.114 +  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
  21.115 +
  21.116 +definition
  21.117 +  word_xor_def: 
  21.118 +  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
  21.119 +
  21.120 +definition
  21.121 +  word_not_def: 
  21.122 +  "NOT (a::'a word) = word_of_int (NOT (uint a))"
  21.123 +
  21.124 +instance ..
  21.125 +
  21.126 +end 
  21.127 +
  21.128 +abbreviation
  21.129 +  word_power :: "'a\<Colon>len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
  21.130 +where
  21.131 +  "word_power == op ^"
  21.132 +
  21.133 +definition
  21.134 +  word_succ :: "'a :: len0 word => 'a word"
  21.135 +where
  21.136 +  "word_succ a = word_of_int (Numeral.succ (uint a))"
  21.137 +
  21.138 +definition
  21.139 +  word_pred :: "'a :: len0 word => 'a word"
  21.140 +where
  21.141 +  "word_pred a = word_of_int (Numeral.pred (uint a))"
  21.142  
  21.143  constdefs
  21.144 -  word_succ :: "'a :: len0 word => 'a word"
  21.145 -  "word_succ a == word_of_int (Numeral.succ (uint a))"
  21.146 -
  21.147 -  word_pred :: "'a :: len0 word => 'a word"
  21.148 -  "word_pred a == word_of_int (Numeral.pred (uint a))"
  21.149 -
  21.150    udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
  21.151    "a udvd b == EX n>=0. uint b = n * uint a"
  21.152  
  21.153 @@ -120,37 +177,10 @@
  21.154    word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
  21.155    "(x <s y) == (x <=s y & x ~= y)"
  21.156  
  21.157 -consts
  21.158 -  word_power :: "'a :: len0 word => nat => 'a word"
  21.159 -primrec
  21.160 -  "word_power a 0 = 1"
  21.161 -  "word_power a (Suc n) = a * word_power a n"
  21.162 -
  21.163 -defs (overloaded)
  21.164 -  word_pow: "power == word_power"
  21.165 -  word_add_def: "a + b == word_of_int (uint a + uint b)"
  21.166 -  word_sub_wi: "a - b == word_of_int (uint a - uint b)"
  21.167 -  word_minus_def: "- a == word_of_int (- uint a)"
  21.168 -  word_mult_def: "a * b == word_of_int (uint a * uint b)"
  21.169 -  word_div_def: "a div b == word_of_int (uint a div uint b)"
  21.170 -  word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
  21.171 -
  21.172  
  21.173  subsection "Bit-wise operations"
  21.174  
  21.175  defs (overloaded)
  21.176 -  word_and_def: 
  21.177 -  "(a::'a::len0 word) AND b == word_of_int (uint a AND uint b)"
  21.178 -
  21.179 -  word_or_def:  
  21.180 -  "(a::'a::len0 word) OR b == word_of_int (uint a OR uint b)"
  21.181 -
  21.182 -  word_xor_def: 
  21.183 -  "(a::'a::len0 word) XOR b == word_of_int (uint a XOR uint b)"
  21.184 -
  21.185 -  word_not_def: 
  21.186 -  "NOT (a::'a::len0 word) == word_of_int (NOT (uint a))"
  21.187 -
  21.188    word_test_bit_def: 
  21.189    "test_bit (a::'a::len0 word) == bin_nth (uint a)"
  21.190  
  21.191 @@ -269,7 +299,7 @@
  21.192  lemmas of_nth_def = word_set_bits_def
  21.193  
  21.194  lemmas word_size_gt_0 [iff] = 
  21.195 -  xtr1 [OF word_size [THEN meta_eq_to_obj_eq] len_gt_0, standard]
  21.196 +  xtr1 [OF word_size len_gt_0, standard]
  21.197  lemmas lens_gt_0 = word_size_gt_0 len_gt_0
  21.198  lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
  21.199  
  21.200 @@ -701,9 +731,9 @@
  21.201    done
  21.202  
  21.203  lemmas num_abs_bintr = sym [THEN trans,
  21.204 -  OF num_of_bintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
  21.205 +  OF num_of_bintr word_number_of_def, standard]
  21.206  lemmas num_abs_sbintr = sym [THEN trans,
  21.207 -  OF num_of_sbintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
  21.208 +  OF num_of_sbintr word_number_of_def, standard]
  21.209    
  21.210  (** cast - note, no arg for new length, as it's determined by type of result,
  21.211    thus in "cast w = w, the type means cast to length of w! **)