1.1 --- a/src/HOL/FixedPoint.thy	Fri Mar 02 15:43:20 2007 +0100
     1.2 +++ b/src/HOL/FixedPoint.thy	Fri Mar 02 15:43:21 2007 +0100
     1.3 @@ -28,9 +28,9 @@
     1.4    bot :: "'a::order" where
     1.5    "bot == Sup {}"
     1.6  *)
     1.7 -axclass comp_lat < order
     1.8 -  Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x"
     1.9 -  Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z <= x) \<Longrightarrow> z <= Meet A"
    1.10 +class comp_lat = order +
    1.11 +  assumes Meet_lower: "x \<in> A \<Longrightarrow> Meet A \<sqsubseteq> x"
    1.12 +  assumes Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Meet A"
    1.13  
    1.14  theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
    1.15    by (auto simp: Sup_def intro: Meet_greatest)

     2.1 --- a/src/HOL/Library/Parity.thy	Fri Mar 02 15:43:20 2007 +0100
     2.2 +++ b/src/HOL/Library/Parity.thy	Fri Mar 02 15:43:21 2007 +0100
     2.3 @@ -9,21 +9,18 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -axclass even_odd < type
     2.8 -
     2.9 -consts
    2.10 -  even :: "'a::even_odd => bool"
    2.11 -
    2.12 -instance int :: even_odd ..
    2.13 -instance nat :: even_odd ..
    2.14 -
    2.15 -defs (overloaded)
    2.16 -  even_def: "even (x::int) == x mod 2 = 0"
    2.17 -  even_nat_def: "even (x::nat) == even (int x)"
    2.18 +class even_odd =
    2.19 +  fixes even :: "'a \<Rightarrow> bool"
    2.20  
    2.21  abbreviation
    2.22 -  odd :: "'a::even_odd => bool" where
    2.23 -  "odd x == \<not> even x"
    2.24 +  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
    2.25 +  "odd x \<equiv> \<not> even x"
    2.26 +
    2.27 +instance int :: even_odd
    2.28 +  even_def: "even x \<equiv> x mod 2 = 0" ..
    2.29 +
    2.30 +instance nat :: even_odd
    2.31 +  even_nat_def: "even x \<equiv> even (int x)" ..
    2.32  
    2.33  
    2.34  subsection {* Even and odd are mutually exclusive *}

     3.1 --- a/src/HOL/Library/Quotient.thy	Fri Mar 02 15:43:20 2007 +0100
     3.2 +++ b/src/HOL/Library/Quotient.thy	Fri Mar 02 15:43:21 2007 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5  text {*
     3.6   We introduce the notion of quotient types over equivalence relations
     3.7 - via axiomatic type classes.
     3.8 + via type classes.
     3.9  *}
    3.10  
    3.11  subsection {* Equivalence relations and quotient types *}
    3.12 @@ -21,14 +21,13 @@
    3.13   "\<sim> :: 'a => 'a => bool"}.
    3.14  *}
    3.15  
    3.16 -axclass eqv \<subseteq> type
    3.17 -consts
    3.18 -  eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
    3.19 +class eqv =
    3.20 +  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
    3.21  
    3.22 -axclass equiv \<subseteq> eqv
    3.23 -  equiv_refl [intro]: "x \<sim> x"
    3.24 -  equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    3.25 -  equiv_sym [sym]: "x \<sim> y ==> y \<sim> x"
    3.26 +class equiv = eqv +
    3.27 +  assumes equiv_refl [intro]: "x \<^loc>\<sim> x"
    3.28 +  assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z"
    3.29 +  assumes equiv_sym [sym]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> x"
    3.30  
    3.31  lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    3.32  proof -

     4.1 --- a/src/HOL/OrderedGroup.thy	Fri Mar 02 15:43:20 2007 +0100
     4.2 +++ b/src/HOL/OrderedGroup.thy	Fri Mar 02 15:43:21 2007 +0100
     4.3 @@ -25,73 +25,71 @@
     4.4  *}
     4.5  
     4.6  subsection {* Semigroups, Groups *}
     4.7 - 
     4.8 -axclass semigroup_add \<subseteq> plus
     4.9 -  add_assoc: "(a + b) + c = a + (b + c)"
    4.10  
    4.11 -axclass ab_semigroup_add \<subseteq> semigroup_add
    4.12 -  add_commute: "a + b = b + a"
    4.13 +class semigroup_add = plus +
    4.14 +  assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
    4.15 +
    4.16 +class ab_semigroup_add = semigroup_add +
    4.17 +  assumes add_commute: "a \<^loc>+ b = b \<^loc>+ a"
    4.18  
    4.19  lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))"
    4.20    by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
    4.21  
    4.22  theorems add_ac = add_assoc add_commute add_left_commute
    4.23  
    4.24 -axclass semigroup_mult \<subseteq> times
    4.25 -  mult_assoc: "(a * b) * c = a * (b * c)"
    4.26 +class semigroup_mult = times +
    4.27 +  assumes mult_assoc: "(a \<^loc>* b) \<^loc>* c = a \<^loc>* (b \<^loc>* c)"
    4.28  
    4.29 -axclass ab_semigroup_mult \<subseteq> semigroup_mult
    4.30 -  mult_commute: "a * b = b * a"
    4.31 +class ab_semigroup_mult = semigroup_mult +
    4.32 +  assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"
    4.33  
    4.34  lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ab_semigroup_mult))"
    4.35    by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
    4.36  
    4.37  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    4.38  
    4.39 -axclass comm_monoid_add \<subseteq> zero, ab_semigroup_add
    4.40 -  add_0[simp]: "0 + a = a"
    4.41 +class comm_monoid_add = zero + ab_semigroup_add +
    4.42 +  assumes add_0 [simp]: "\<^loc>0 \<^loc>+ a = a"
    4.43  
    4.44 -axclass monoid_mult \<subseteq> one, semigroup_mult
    4.45 -  mult_1_left[simp]: "1 * a  = a"
    4.46 -  mult_1_right[simp]: "a * 1 = a"
    4.47 +class monoid_mult = one + semigroup_mult +
    4.48 +  assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"
    4.49 +  assumes mult_1_right [simp]: "a \<^loc>* \<^loc>1 = a"
    4.50  
    4.51 -axclass comm_monoid_mult \<subseteq> one, ab_semigroup_mult
    4.52 -  mult_1: "1 * a = a"
    4.53 +class comm_monoid_mult = one + ab_semigroup_mult +
    4.54 +  assumes mult_1: "\<^loc>1 \<^loc>* a = a"
    4.55  
    4.56  instance comm_monoid_mult \<subseteq> monoid_mult
    4.57 -by (intro_classes, insert mult_1, simp_all add: mult_commute, auto)
    4.58 +  by intro_classes (insert mult_1, simp_all add: mult_commute, auto)
    4.59  
    4.60 -axclass cancel_semigroup_add \<subseteq> semigroup_add
    4.61 -  add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
    4.62 -  add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
    4.63 +class cancel_semigroup_add = semigroup_add +
    4.64 +  assumes add_left_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
    4.65 +  assumes add_right_imp_eq: "b \<^loc>+ a = c \<^loc>+ a \<Longrightarrow> b = c"
    4.66  
    4.67 -axclass cancel_ab_semigroup_add \<subseteq> ab_semigroup_add
    4.68 -  add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
    4.69 +class cancel_ab_semigroup_add = ab_semigroup_add +
    4.70 +  assumes add_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
    4.71  
    4.72  instance cancel_ab_semigroup_add \<subseteq> cancel_semigroup_add
    4.73 -proof
    4.74 -  {
    4.75 -    fix a b c :: 'a
    4.76 -    assume "a + b = a + c"
    4.77 -    thus "b = c" by (rule add_imp_eq)
    4.78 -  }
    4.79 -  note f = this
    4.80 +proof intro_classes
    4.81 +  fix a b c :: 'a
    4.82 +  assume "a + b = a + c" 
    4.83 +  then show "b = c" by (rule add_imp_eq)
    4.84 +next
    4.85    fix a b c :: 'a
    4.86    assume "b + a = c + a"
    4.87 -  hence "a + b = a + c" by (simp only: add_commute)
    4.88 -  thus "b = c" by (rule f)
    4.89 +  then have "a + b = a + c" by (simp only: add_commute)
    4.90 +  then show "b = c" by (rule add_imp_eq)
    4.91  qed
    4.92  
    4.93 -axclass ab_group_add \<subseteq> minus, comm_monoid_add
    4.94 -  left_minus[simp]: " - a + a = 0"
    4.95 -  diff_minus: "a - b = a + (-b)"
    4.96 +class ab_group_add = minus + comm_monoid_add +
    4.97 +  assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
    4.98 +  assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
    4.99  
   4.100  instance ab_group_add \<subseteq> cancel_ab_semigroup_add
   4.101 -proof 
   4.102 +proof intro_classes
   4.103    fix a b c :: 'a
   4.104    assume "a + b = a + c"
   4.105 -  hence "-a + a + b = -a + a + c" by (simp only: add_assoc)
   4.106 -  thus "b = c" by simp 
   4.107 +  then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
   4.108 +  then show "b = c" by simp 
   4.109  qed
   4.110  
   4.111  lemma add_0_right [simp]: "a + 0 = (a::'a::comm_monoid_add)"
   4.112 @@ -105,11 +103,11 @@
   4.113    and add_zero_right = add_0_right
   4.114  
   4.115  lemma add_left_cancel [simp]:
   4.116 -     "(a + b = a + c) = (b = (c::'a::cancel_semigroup_add))"
   4.117 -by (blast dest: add_left_imp_eq) 
   4.118 +  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
   4.119 +  by (blast dest: add_left_imp_eq) 
   4.120  
   4.121  lemma add_right_cancel [simp]:
   4.122 -     "(b + a = c + a) = (b = (c::'a::cancel_semigroup_add))"
   4.123 +  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
   4.124    by (blast dest: add_right_imp_eq)
   4.125  
   4.126  lemma right_minus [simp]: "a + -(a::'a::ab_group_add) = 0"
   4.127 @@ -196,17 +194,18 @@
   4.128  
   4.129  subsection {* (Partially) Ordered Groups *} 
   4.130  
   4.131 -axclass pordered_ab_semigroup_add \<subseteq> order, ab_semigroup_add
   4.132 -  add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   4.133 +class pordered_ab_semigroup_add = order + ab_semigroup_add +
   4.134 +  assumes add_left_mono: "a \<sqsubseteq> b \<Longrightarrow> c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b"
   4.135  
   4.136 -axclass pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add, cancel_ab_semigroup_add
   4.137 +class pordered_cancel_ab_semigroup_add =
   4.138 +  pordered_ab_semigroup_add + cancel_ab_semigroup_add
   4.139  
   4.140  instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
   4.141  
   4.142 -axclass pordered_ab_semigroup_add_imp_le \<subseteq> pordered_cancel_ab_semigroup_add
   4.143 -  add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   4.144 +class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
   4.145 +  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c + b \<Longrightarrow> a \<sqsubseteq> b"
   4.146  
   4.147 -axclass pordered_ab_group_add \<subseteq> ab_group_add, pordered_ab_semigroup_add
   4.148 +class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
   4.149  
   4.150  instance pordered_ab_group_add \<subseteq> pordered_ab_semigroup_add_imp_le
   4.151  proof
   4.152 @@ -217,7 +216,7 @@
   4.153    thus "a \<le> b" by simp
   4.154  qed
   4.155  
   4.156 -axclass ordered_cancel_ab_semigroup_add \<subseteq> pordered_cancel_ab_semigroup_add, linorder
   4.157 +class ordered_cancel_ab_semigroup_add = pordered_cancel_ab_semigroup_add + linorder
   4.158  
   4.159  instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le
   4.160  proof
   4.161 @@ -239,7 +238,7 @@
   4.162  qed
   4.163  
   4.164  lemma add_right_mono: "a \<le> (b::'a::pordered_ab_semigroup_add) ==> a + c \<le> b + c"
   4.165 -by (simp add: add_commute[of _ c] add_left_mono)
   4.166 +  by (simp add: add_commute [of _ c] add_left_mono)
   4.167  
   4.168  text {* non-strict, in both arguments *}
   4.169  lemma add_mono:

     5.1 --- a/src/HOL/Power.thy	Fri Mar 02 15:43:20 2007 +0100
     5.2 +++ b/src/HOL/Power.thy	Fri Mar 02 15:43:21 2007 +0100
     5.3 @@ -13,9 +13,9 @@
     5.4  
     5.5  subsection{*Powers for Arbitrary Monoids*}
     5.6  
     5.7 -axclass recpower \<subseteq> monoid_mult, power
     5.8 -  power_0 [simp]: "a ^ 0       = 1"
     5.9 -  power_Suc:      "a ^ (Suc n) = a * (a ^ n)"
    5.10 +class recpower = monoid_mult + power +
    5.11 +  assumes power_0 [simp]: "a \<^loc>^ 0       = \<^loc>1"
    5.12 +  assumes power_Suc:      "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)"
    5.13  
    5.14  lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
    5.15  by (simp add: power_Suc)

     6.1 --- a/src/HOL/Ring_and_Field.thy	Fri Mar 02 15:43:20 2007 +0100
     6.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Mar 02 15:43:21 2007 +0100
     6.3 @@ -23,17 +23,17 @@
     6.4    \end{itemize}
     6.5  *}
     6.6  
     6.7 -axclass semiring \<subseteq> ab_semigroup_add, semigroup_mult
     6.8 -  left_distrib: "(a + b) * c = a * c + b * c"
     6.9 -  right_distrib: "a * (b + c) = a * b + a * c"
    6.10 +class semiring = ab_semigroup_add + semigroup_mult +
    6.11 +  assumes left_distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
    6.12 +  assumes right_distrib: "a \<^loc>* (b \<^loc>+ c) = a \<^loc>* b \<^loc>+ a \<^loc>* c"
    6.13  
    6.14 -axclass mult_zero \<subseteq> times, zero
    6.15 -  mult_zero_left [simp]: "0 * a = 0"
    6.16 -  mult_zero_right [simp]: "a * 0 = 0"
    6.17 +class mult_zero = times + zero +
    6.18 +  assumes mult_zero_left [simp]: "\<^loc>0 \<^loc>* a = \<^loc>0"
    6.19 +  assumes mult_zero_right [simp]: "a \<^loc>* \<^loc>0 = \<^loc>0"
    6.20  
    6.21 -axclass semiring_0 \<subseteq> semiring, comm_monoid_add, mult_zero
    6.22 +class semiring_0 = semiring + comm_monoid_add + mult_zero
    6.23  
    6.24 -axclass semiring_0_cancel \<subseteq> semiring, comm_monoid_add, cancel_ab_semigroup_add
    6.25 +class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add
    6.26  
    6.27  instance semiring_0_cancel \<subseteq> semiring_0
    6.28  proof
    6.29 @@ -49,8 +49,8 @@
    6.30      by (simp only: add_left_cancel)
    6.31  qed
    6.32  
    6.33 -axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
    6.34 -  distrib: "(a + b) * c = a * c + b * c"
    6.35 +class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
    6.36 +  assumes distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
    6.37  
    6.38  instance comm_semiring \<subseteq> semiring
    6.39  proof
    6.40 @@ -62,37 +62,38 @@
    6.41    finally show "a * (b + c) = a * b + a * c" by blast
    6.42  qed
    6.43  
    6.44 -axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add, mult_zero
    6.45 +class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
    6.46  
    6.47  instance comm_semiring_0 \<subseteq> semiring_0 ..
    6.48  
    6.49 -axclass comm_semiring_0_cancel \<subseteq> comm_semiring, comm_monoid_add, cancel_ab_semigroup_add
    6.50 +class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
    6.51  
    6.52  instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
    6.53  
    6.54  instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
    6.55  
    6.56 -axclass zero_neq_one \<subseteq> zero, one
    6.57 -  zero_neq_one [simp]: "0 \<noteq> 1"
    6.58 +class zero_neq_one = zero + one +
    6.59 +  assumes zero_neq_one [simp]: "\<^loc>0 \<noteq> \<^loc>1"
    6.60  
    6.61 -axclass semiring_1 \<subseteq> zero_neq_one, semiring_0, monoid_mult
    6.62 +class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
    6.63  
    6.64 -axclass comm_semiring_1 \<subseteq> zero_neq_one, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)
    6.65 +class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
    6.66 +  (*previously almost_semiring*)
    6.67  
    6.68  instance comm_semiring_1 \<subseteq> semiring_1 ..
    6.69  
    6.70 -axclass no_zero_divisors \<subseteq> zero, times
    6.71 -  no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    6.72 +class no_zero_divisors = zero + times +
    6.73 +  assumes no_zero_divisors: "a \<noteq> \<^loc>0 \<Longrightarrow> b \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* b \<noteq> \<^loc>0"
    6.74  
    6.75 -axclass semiring_1_cancel \<subseteq> semiring, comm_monoid_add, zero_neq_one, cancel_ab_semigroup_add, monoid_mult
    6.76 +class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
    6.77 +  + cancel_ab_semigroup_add + monoid_mult
    6.78  
    6.79  instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
    6.80  
    6.81  instance semiring_1_cancel \<subseteq> semiring_1 ..
    6.82  
    6.83 -axclass comm_semiring_1_cancel \<subseteq> 
    6.84 -  comm_semiring, comm_monoid_add, comm_monoid_mult,
    6.85 -  zero_neq_one, cancel_ab_semigroup_add
    6.86 +class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
    6.87 +  + zero_neq_one + cancel_ab_semigroup_add
    6.88  
    6.89  instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
    6.90  
    6.91 @@ -100,38 +101,40 @@
    6.92  
    6.93  instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
    6.94  
    6.95 -axclass ring \<subseteq> semiring, ab_group_add
    6.96 +class ring = semiring + ab_group_add
    6.97  
    6.98  instance ring \<subseteq> semiring_0_cancel ..
    6.99  
   6.100 -axclass comm_ring \<subseteq> comm_semiring, ab_group_add
   6.101 +class comm_ring = comm_semiring + ab_group_add
   6.102  
   6.103  instance comm_ring \<subseteq> ring ..
   6.104  
   6.105  instance comm_ring \<subseteq> comm_semiring_0_cancel ..
   6.106  
   6.107 -axclass ring_1 \<subseteq> ring, zero_neq_one, monoid_mult
   6.108 +class ring_1 = ring + zero_neq_one + monoid_mult
   6.109  
   6.110  instance ring_1 \<subseteq> semiring_1_cancel ..
   6.111  
   6.112 -axclass comm_ring_1 \<subseteq> comm_ring, zero_neq_one, comm_monoid_mult (* previously ring *)
   6.113 +class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   6.114 +  (*previously ring*)
   6.115  
   6.116  instance comm_ring_1 \<subseteq> ring_1 ..
   6.117  
   6.118  instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
   6.119  
   6.120 -axclass idom \<subseteq> comm_ring_1, no_zero_divisors
   6.121 +class idom = comm_ring_1 + no_zero_divisors
   6.122  
   6.123 -axclass division_ring \<subseteq> ring_1, inverse
   6.124 -  left_inverse [simp]:  "a \<noteq> 0 ==> inverse a * a = 1"
   6.125 -  right_inverse [simp]: "a \<noteq> 0 ==> a * inverse a = 1"
   6.126 +class division_ring = ring_1 + inverse +
   6.127 +  assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
   6.128 +  assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
   6.129  
   6.130 -axclass field \<subseteq> comm_ring_1, inverse
   6.131 -  field_left_inverse: "a \<noteq> 0 ==> inverse a * a = 1"
   6.132 -  divide_inverse:     "a / b = a * inverse b"
   6.133 +class field = comm_ring_1 + inverse +
   6.134 +  assumes field_left_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
   6.135 +  assumes divide_inverse:     "a \<^loc>/ b = a \<^loc>* inverse b"
   6.136  
   6.137  lemma field_right_inverse:
   6.138 -      assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
   6.139 +  assumes not0: "a \<noteq> 0"
   6.140 +  shows "a * inverse (a::'a::field) = 1"
   6.141  proof -
   6.142    have "a * inverse a = inverse a * a" by (rule mult_commute)
   6.143    also have "... = 1" using not0 by (rule field_left_inverse)
   6.144 @@ -156,8 +159,8 @@
   6.145  instance field \<subseteq> idom
   6.146  by (intro_classes, simp)
   6.147  
   6.148 -axclass division_by_zero \<subseteq> zero, inverse
   6.149 -  inverse_zero [simp]: "inverse 0 = 0"
   6.150 +class division_by_zero = zero + inverse +
   6.151 +  assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
   6.152  
   6.153  subsection {* Distribution rules *}
   6.154  
   6.155 @@ -192,24 +195,23 @@
   6.156  by (simp add: left_distrib diff_minus 
   6.157                minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   6.158  
   6.159 -axclass mult_mono \<subseteq> times, zero, ord
   6.160 -  mult_left_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
   6.161 -  mult_right_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> a * c <= b * c"
   6.162 +class mult_mono = times + zero + ord +
   6.163 +  assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
   6.164 +  assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"
   6.165  
   6.166 -axclass pordered_semiring \<subseteq> mult_mono, semiring_0, pordered_ab_semigroup_add 
   6.167 +class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
   6.168  
   6.169 -axclass pordered_cancel_semiring \<subseteq> 
   6.170 -  mult_mono, pordered_ab_semigroup_add,
   6.171 -  semiring, comm_monoid_add, 
   6.172 -  pordered_ab_semigroup_add, cancel_ab_semigroup_add
   6.173 +class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   6.174 +  + semiring + comm_monoid_add + pordered_ab_semigroup_add
   6.175 +  + cancel_ab_semigroup_add
   6.176  
   6.177  instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
   6.178  
   6.179  instance pordered_cancel_semiring \<subseteq> pordered_semiring .. 
   6.180  
   6.181 -axclass ordered_semiring_strict \<subseteq> semiring, comm_monoid_add, ordered_cancel_ab_semigroup_add
   6.182 -  mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   6.183 -  mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   6.184 +class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   6.185 +  assumes mult_strict_left_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
   6.186 +  assumes mult_strict_right_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> a \<^loc>* c \<sqsubset> b \<^loc>* c"
   6.187  
   6.188  instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
   6.189  
   6.190 @@ -221,18 +223,19 @@
   6.191  apply (simp add: mult_strict_right_mono)
   6.192  done
   6.193  
   6.194 -axclass mult_mono1 \<subseteq> times, zero, ord
   6.195 -  mult_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
   6.196 +class mult_mono1 = times + zero + ord +
   6.197 +  assumes mult_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
   6.198  
   6.199 -axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add, mult_mono1
   6.200 +class pordered_comm_semiring = comm_semiring_0
   6.201 +  + pordered_ab_semigroup_add + mult_mono1
   6.202  
   6.203 -axclass pordered_cancel_comm_semiring \<subseteq> 
   6.204 -  comm_semiring_0_cancel, pordered_ab_semigroup_add, mult_mono1
   6.205 +class pordered_cancel_comm_semiring = comm_semiring_0_cancel
   6.206 +  + pordered_ab_semigroup_add + mult_mono1
   6.207    
   6.208  instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
   6.209  
   6.210 -axclass ordered_comm_semiring_strict \<subseteq> comm_semiring_0, ordered_cancel_ab_semigroup_add
   6.211 -  mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   6.212 +class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   6.213 +  assumes mult_strict_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
   6.214  
   6.215  instance pordered_comm_semiring \<subseteq> pordered_semiring
   6.216  proof
   6.217 @@ -258,7 +261,7 @@
   6.218  apply (auto simp add: mult_strict_left_mono order_le_less)
   6.219  done
   6.220  
   6.221 -axclass pordered_ring \<subseteq> ring, pordered_cancel_semiring 
   6.222 +class pordered_ring = ring + pordered_cancel_semiring 
   6.223  
   6.224  instance pordered_ring \<subseteq> pordered_ab_group_add ..
   6.225  
   6.226 @@ -268,26 +271,28 @@
   6.227  
   6.228  instance lordered_ring \<subseteq> lordered_ab_group_join ..
   6.229  
   6.230 -axclass abs_if \<subseteq> minus, ord, zero
   6.231 -  abs_if: "abs a = (if (a < 0) then (-a) else a)"
   6.232 +class abs_if = minus + ord + zero +
   6.233 +  assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
   6.234  
   6.235 -axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, abs_if
   6.236 +class ordered_ring_strict = ring + ordered_semiring_strict + abs_if
   6.237  
   6.238  instance ordered_ring_strict \<subseteq> lordered_ab_group ..
   6.239  
   6.240  instance ordered_ring_strict \<subseteq> lordered_ring
   6.241 -by (intro_classes, simp add: abs_if join_eq_if)
   6.242 +  by (intro_classes, simp add: abs_if join_eq_if)
   6.243  
   6.244 -axclass pordered_comm_ring \<subseteq> comm_ring, pordered_comm_semiring
   6.245 +class pordered_comm_ring = comm_ring + pordered_comm_semiring
   6.246  
   6.247 -axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)
   6.248 -  zero_less_one [simp]: "0 < 1"
   6.249 +class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   6.250 +  (*previously ordered_semiring*)
   6.251 +  assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
   6.252  
   6.253 -axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, abs_if (* previously ordered_ring *)
   6.254 +class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if
   6.255 +  (*previously ordered_ring*)
   6.256  
   6.257  instance ordered_idom \<subseteq> ordered_ring_strict ..
   6.258  
   6.259 -axclass ordered_field \<subseteq> field, ordered_idom
   6.260 +class ordered_field = field + ordered_idom
   6.261  
   6.262  lemmas linorder_neqE_ordered_idom =
   6.263   linorder_neqE[where 'a = "?'b::ordered_idom"]

     7.1 --- a/src/HOL/Wellfounded_Recursion.thy	Fri Mar 02 15:43:20 2007 +0100
     7.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Fri Mar 02 15:43:21 2007 +0100
     7.3 @@ -40,8 +40,8 @@
     7.4  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
     7.5    "acyclicP r == acyclic (Collect2 r)"
     7.6  
     7.7 -axclass wellorder \<subseteq> linorder
     7.8 -  wf: "wf {(x,y::'a::ord). x<y}"
     7.9 +class wellorder = linorder +
    7.10 +  assumes wf: "wf {(x, y). x \<sqsubset> y}"
    7.11  
    7.12  
    7.13  lemma wfP_wf_eq [pred_set_conv]: "wfP (member2 r) = wf r"