moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
authorhaftmann
Wed Feb 10 14:12:04 2010 +0100 (2010-02-10)
changeset 35092cfe605c54e50
parent 35091 59b41ba431b5
child 35093 5acba118b02a
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
src/HOL/Algebras.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Groebner_Basis.thy
src/HOL/Groups.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/prim_rec.imp
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOL/realax.imp
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Orderings.thy
src/HOL/Rings.thy
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_clause.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
     1.1 --- a/src/HOL/Algebras.thy	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Algebras.thy	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection {* Generic algebraic operations *}
     1.8 +subsection {* Generic syntactic operations *}
     1.9  
    1.10  class zero = 
    1.11    fixes zero :: 'a  ("0")
    1.12 @@ -63,6 +63,13 @@
    1.13  class one =
    1.14    fixes one  :: 'a  ("1")
    1.15  
    1.16 +hide (open) const zero one
    1.17 +
    1.18 +syntax
    1.19 +  "_index1"  :: index    ("\<^sub>1")
    1.20 +translations
    1.21 +  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    1.22 +
    1.23  lemma Let_0 [simp]: "Let 0 f = f 0"
    1.24    unfolding Let_def ..
    1.25  
    1.26 @@ -89,8 +96,6 @@
    1.27  in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
    1.28  *} -- {* show types that are presumably too general *}
    1.29  
    1.30 -hide (open) const zero one
    1.31 -
    1.32  class plus =
    1.33    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    1.34  
    1.35 @@ -103,51 +108,4 @@
    1.36  class times =
    1.37    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    1.38  
    1.39 -class abs =
    1.40 -  fixes abs :: "'a \<Rightarrow> 'a"
    1.41 -begin
    1.42 -
    1.43 -notation (xsymbols)
    1.44 -  abs  ("\<bar>_\<bar>")
    1.45 -
    1.46 -notation (HTML output)
    1.47 -  abs  ("\<bar>_\<bar>")
    1.48 -
    1.49 -end
    1.50 -
    1.51 -class sgn =
    1.52 -  fixes sgn :: "'a \<Rightarrow> 'a"
    1.53 -
    1.54 -class ord =
    1.55 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.56 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.57 -begin
    1.58 -
    1.59 -notation
    1.60 -  less_eq  ("op <=") and
    1.61 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
    1.62 -  less  ("op <") and
    1.63 -  less  ("(_/ < _)"  [51, 51] 50)
    1.64 -  
    1.65 -notation (xsymbols)
    1.66 -  less_eq  ("op \<le>") and
    1.67 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.68 -
    1.69 -notation (HTML output)
    1.70 -  less_eq  ("op \<le>") and
    1.71 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.72 -
    1.73 -abbreviation (input)
    1.74 -  greater_eq  (infix ">=" 50) where
    1.75 -  "x >= y \<equiv> y <= x"
    1.76 -
    1.77 -notation (input)
    1.78 -  greater_eq  (infix "\<ge>" 50)
    1.79 -
    1.80 -abbreviation (input)
    1.81 -  greater  (infix ">" 50) where
    1.82 -  "x > y \<equiv> y < x"
    1.83 -
    1.84 -end
    1.85 -
    1.86  end
    1.87 \ No newline at end of file
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 14:12:02 2010 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 14:12:04 2010 +0100
     2.3 @@ -684,7 +684,7 @@
     2.4  fun xnormalize_conv ctxt [] ct = reflexive ct
     2.5  | xnormalize_conv ctxt (vs as (x::_)) ct =
     2.6     case term_of ct of
     2.7 -   Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) =>
     2.8 +   Const(@{const_name Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) =>
     2.9      (case whatis x (Thm.dest_arg1 ct) of
    2.10      ("c*x+t",[c,t]) =>
    2.11         let
    2.12 @@ -727,7 +727,7 @@
    2.13      | _ => reflexive ct)
    2.14  
    2.15  
    2.16 -|  Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    2.17 +|  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    2.18     (case whatis x (Thm.dest_arg1 ct) of
    2.19      ("c*x+t",[c,t]) =>
    2.20         let
    2.21 @@ -816,7 +816,7 @@
    2.22    val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
    2.23  in
    2.24  fun field_isolate_conv phi ctxt vs ct = case term_of ct of
    2.25 -  Const(@{const_name Algebras.less},_)$a$b =>
    2.26 +  Const(@{const_name Orderings.less},_)$a$b =>
    2.27     let val (ca,cb) = Thm.dest_binop ct
    2.28         val T = ctyp_of_term ca
    2.29         val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
    2.30 @@ -825,7 +825,7 @@
    2.31                (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    2.32         val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    2.33     in rth end
    2.34 -| Const(@{const_name Algebras.less_eq},_)$a$b =>
    2.35 +| Const(@{const_name Orderings.less_eq},_)$a$b =>
    2.36     let val (ca,cb) = Thm.dest_binop ct
    2.37         val T = ctyp_of_term ca
    2.38         val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
    2.39 @@ -856,11 +856,11 @@
    2.40                              else Ferrante_Rackoff_Data.Nox
    2.41     | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    2.42                              else Ferrante_Rackoff_Data.Nox
    2.43 -   | Const(@{const_name Algebras.less},_)$y$z =>
    2.44 +   | Const(@{const_name Orderings.less},_)$y$z =>
    2.45         if term_of x aconv y then Ferrante_Rackoff_Data.Lt
    2.46          else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
    2.47          else Ferrante_Rackoff_Data.Nox
    2.48 -   | Const (@{const_name Algebras.less_eq},_)$y$z =>
    2.49 +   | Const (@{const_name Orderings.less_eq},_)$y$z =>
    2.50           if term_of x aconv y then Ferrante_Rackoff_Data.Le
    2.51           else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
    2.52           else Ferrante_Rackoff_Data.Nox
     3.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 14:12:02 2010 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 14:12:04 2010 +0100
     3.3 @@ -2958,8 +2958,8 @@
     3.4  val disjt = @{term "op |"};
     3.5  val impt = @{term "op -->"};
     3.6  val ifft = @{term "op = :: bool => _"}
     3.7 -fun llt rT = Const(@{const_name Algebras.less},rrT rT);
     3.8 -fun lle rT = Const(@{const_name Algebras.less},rrT rT);
     3.9 +fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    3.10 +fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    3.11  fun eqt rT = Const("op =",rrT rT);
    3.12  fun rz rT = Const(@{const_name Algebras.zero},rT);
    3.13  
    3.14 @@ -3024,9 +3024,9 @@
    3.15    | Const("op =",ty)$p$q => 
    3.16         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
    3.17         else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    3.18 -  | Const(@{const_name Algebras.less},_)$p$q => 
    3.19 +  | Const(@{const_name Orderings.less},_)$p$q => 
    3.20          @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    3.21 -  | Const(@{const_name Algebras.less_eq},_)$p$q => 
    3.22 +  | Const(@{const_name Orderings.less_eq},_)$p$q => 
    3.23          @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    3.24    | Const("Ex",_)$Abs(xn,xT,p) => 
    3.25       let val (xn', p') =  variant_abs (xn,xT,p)
     4.1 --- a/src/HOL/Groebner_Basis.thy	Wed Feb 10 14:12:02 2010 +0100
     4.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Feb 10 14:12:04 2010 +0100
     4.3 @@ -556,14 +556,14 @@
     4.4  
     4.5   fun proc3 phi ss ct =
     4.6    (case term_of ct of
     4.7 -    Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
     4.8 +    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
     4.9        let
    4.10          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    4.11          val _ = map is_number [a,b,c]
    4.12          val T = ctyp_of_term c
    4.13          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    4.14        in SOME (mk_meta_eq th) end
    4.15 -  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    4.16 +  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    4.17        let
    4.18          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    4.19          val _ = map is_number [a,b,c]
    4.20 @@ -577,14 +577,14 @@
    4.21          val T = ctyp_of_term c
    4.22          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    4.23        in SOME (mk_meta_eq th) end
    4.24 -  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    4.25 +  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    4.26      let
    4.27        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    4.28          val _ = map is_number [a,b,c]
    4.29          val T = ctyp_of_term c
    4.30          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    4.31        in SOME (mk_meta_eq th) end
    4.32 -  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    4.33 +  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    4.34      let
    4.35        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    4.36          val _ = map is_number [a,b,c]
     5.1 --- a/src/HOL/Groups.thy	Wed Feb 10 14:12:02 2010 +0100
     5.2 +++ b/src/HOL/Groups.thy	Wed Feb 10 14:12:04 2010 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Groups, also combined with orderings *}
     5.5  
     5.6  theory Groups
     5.7 -imports Lattices
     5.8 +imports Orderings
     5.9  uses "~~/src/Provers/Arith/abel_cancel.ML"
    5.10  begin
    5.11  
    5.12 @@ -40,6 +40,7 @@
    5.13  Of course it also works for fields, but it knows nothing about multiplicative
    5.14  inverses or division. This is catered for by @{text field_simps}. *}
    5.15  
    5.16 +
    5.17  subsection {* Semigroups and Monoids *}
    5.18  
    5.19  class semigroup_add = plus +
    5.20 @@ -884,6 +885,32 @@
    5.21    shows "[|0\<le>a; b<c|] ==> b < a + c"
    5.22  by (insert add_le_less_mono [of 0 a b c], simp)
    5.23  
    5.24 +class abs =
    5.25 +  fixes abs :: "'a \<Rightarrow> 'a"
    5.26 +begin
    5.27 +
    5.28 +notation (xsymbols)
    5.29 +  abs  ("\<bar>_\<bar>")
    5.30 +
    5.31 +notation (HTML output)
    5.32 +  abs  ("\<bar>_\<bar>")
    5.33 +
    5.34 +end
    5.35 +
    5.36 +class sgn =
    5.37 +  fixes sgn :: "'a \<Rightarrow> 'a"
    5.38 +
    5.39 +class abs_if = minus + uminus + ord + zero + abs +
    5.40 +  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
    5.41 +
    5.42 +class sgn_if = minus + uminus + zero + one + ord + sgn +
    5.43 +  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    5.44 +begin
    5.45 +
    5.46 +lemma sgn0 [simp]: "sgn 0 = 0"
    5.47 +  by (simp add:sgn_if)
    5.48 +
    5.49 +end
    5.50  
    5.51  class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
    5.52    assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
     6.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed Feb 10 14:12:02 2010 +0100
     6.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed Feb 10 14:12:04 2010 +0100
     6.3 @@ -58,7 +58,7 @@
     6.4    let val T as Type ("fun",[t,_]) = fastype_of trm
     6.5    in Collect_const t $ trm end;
     6.6  
     6.7 -fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT);
     6.8 +fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
     6.9  
    6.10  
    6.11  fun Mset ctxt prop =
     7.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Feb 10 14:12:02 2010 +0100
     7.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Feb 10 14:12:04 2010 +0100
     7.3 @@ -166,7 +166,7 @@
     7.4  import_theory prim_rec;
     7.5  
     7.6  const_maps
     7.7 -    "<" > Algebras.less :: "[nat,nat]=>bool";
     7.8 +    "<" > Orderings.less :: "[nat,nat]=>bool";
     7.9  
    7.10  end_import;
    7.11  
    7.12 @@ -181,7 +181,7 @@
    7.13    ">"          > HOL4Compat.nat_gt
    7.14    ">="         > HOL4Compat.nat_ge
    7.15    FUNPOW       > HOL4Compat.FUNPOW
    7.16 -  "<="         > Algebras.less_eq :: "[nat,nat]=>bool"
    7.17 +  "<="         > Orderings.less_eq :: "[nat,nat]=>bool"
    7.18    "+"          > Algebras.plus :: "[nat,nat]=>nat"
    7.19    "*"          > Algebras.times :: "[nat,nat]=>nat"
    7.20    "-"          > Algebras.minus :: "[nat,nat]=>nat"
     8.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Feb 10 14:12:02 2010 +0100
     8.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Feb 10 14:12:04 2010 +0100
     8.3 @@ -22,7 +22,7 @@
     8.4    inv      > Algebras.inverse   :: "real => real"
     8.5    real_add > Algebras.plus      :: "[real,real] => real"
     8.6    real_mul > Algebras.times     :: "[real,real] => real"
     8.7 -  real_lt  > Algebras.less      :: "[real,real] => bool";
     8.8 +  real_lt  > Orderings.less      :: "[real,real] => bool";
     8.9  
    8.10  ignore_thms
    8.11      real_TY_DEF
    8.12 @@ -50,11 +50,11 @@
    8.13  const_maps
    8.14    real_gt     > HOL4Compat.real_gt
    8.15    real_ge     > HOL4Compat.real_ge
    8.16 -  real_lte    > Algebras.less_eq :: "[real,real] => bool"
    8.17 +  real_lte    > Orderings.less_eq :: "[real,real] => bool"
    8.18    real_sub    > Algebras.minus :: "[real,real] => real"
    8.19    "/"         > Algebras.divide :: "[real,real] => real"
    8.20    pow         > Power.power :: "[real,nat] => real"
    8.21 -  abs         > Algebras.abs :: "real => real"
    8.22 +  abs         > Groups.abs :: "real => real"
    8.23    real_of_num > RealDef.real :: "nat => real";
    8.24  
    8.25  end_import;
     9.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Wed Feb 10 14:12:02 2010 +0100
     9.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Feb 10 14:12:04 2010 +0100
     9.3 @@ -23,7 +23,7 @@
     9.4    "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
     9.5    ">=" > "HOL4Compat.nat_ge"
     9.6    ">" > "HOL4Compat.nat_gt"
     9.7 -  "<=" > "Algebras.ord_class.less_eq" :: "nat => nat => bool"
     9.8 +  "<=" > "Orderings.less_eq" :: "nat => nat => bool"
     9.9    "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
    9.10    "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
    9.11    "*" > "Algebras.times_class.times" :: "nat => nat => nat"
    10.1 --- a/src/HOL/Import/HOL/prim_rec.imp	Wed Feb 10 14:12:02 2010 +0100
    10.2 +++ b/src/HOL/Import/HOL/prim_rec.imp	Wed Feb 10 14:12:04 2010 +0100
    10.3 @@ -18,7 +18,7 @@
    10.4    "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
    10.5    "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
    10.6    "PRE" > "HOL4Base.prim_rec.PRE"
    10.7 -  "<" > "Algebras.less" :: "nat => nat => bool"
    10.8 +  "<" > "Orderings.less" :: "nat => nat => bool"
    10.9  
   10.10  thm_maps
   10.11    "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
    11.1 --- a/src/HOL/Import/HOL/real.imp	Wed Feb 10 14:12:02 2010 +0100
    11.2 +++ b/src/HOL/Import/HOL/real.imp	Wed Feb 10 14:12:04 2010 +0100
    11.3 @@ -12,11 +12,11 @@
    11.4    "sum" > "HOL4Real.real.sum"
    11.5    "real_sub" > "Algebras.minus" :: "real => real => real"
    11.6    "real_of_num" > "RealDef.real" :: "nat => real"
    11.7 -  "real_lte" > "Algebras.less_eq" :: "real => real => bool"
    11.8 +  "real_lte" > "Orderings.less_eq" :: "real => real => bool"
    11.9    "real_gt" > "HOL4Compat.real_gt"
   11.10    "real_ge" > "HOL4Compat.real_ge"
   11.11    "pow" > "Power.power_class.power" :: "real => nat => real"
   11.12 -  "abs" > "Algebras.abs" :: "real => real"
   11.13 +  "abs" > "Groups.abs" :: "real => real"
   11.14    "/" > "Ring.divide" :: "real => real => real"
   11.15  
   11.16  thm_maps
    12.1 --- a/src/HOL/Import/HOL/realax.imp	Wed Feb 10 14:12:02 2010 +0100
    12.2 +++ b/src/HOL/Import/HOL/realax.imp	Wed Feb 10 14:12:04 2010 +0100
    12.3 @@ -29,7 +29,7 @@
    12.4    "treal_0" > "HOL4Real.realax.treal_0"
    12.5    "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
    12.6    "real_mul" > "Algebras.times_class.times" :: "real => real => real"
    12.7 -  "real_lt" > "Algebras.ord_class.less" :: "real => real => bool"
    12.8 +  "real_lt" > "Orderings.less" :: "real => real => bool"
    12.9    "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
   12.10    "real_1" > "Algebras.one_class.one" :: "real"
   12.11    "real_0" > "Algebras.zero_class.zero" :: "real"
    13.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Wed Feb 10 14:12:02 2010 +0100
    13.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Wed Feb 10 14:12:04 2010 +0100
    13.3 @@ -16,7 +16,7 @@
    13.4    (@{const_name dummy_pattern}, "'a::{}"),
    13.5    (@{const_name Algebras.uminus}, "'a"),
    13.6    (@{const_name Nat.size}, "'a"),
    13.7 -  (@{const_name Algebras.abs}, "'a")];
    13.8 +  (@{const_name Groups.abs}, "'a")];
    13.9  
   13.10  val forbidden_thms =
   13.11   ["finite_intvl_succ_class",
    14.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Feb 10 14:12:02 2010 +0100
    14.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Feb 10 14:12:04 2010 +0100
    14.3 @@ -197,7 +197,7 @@
    14.4    (@{const_name "dummy_pattern"}, "'a::{}") (*,
    14.5    (@{const_name "uminus"}, "'a"),
    14.6    (@{const_name "Nat.size"}, "'a"),
    14.7 -  (@{const_name "Algebras.abs"}, "'a") *)]
    14.8 +  (@{const_name "Groups.abs"}, "'a") *)]
    14.9  
   14.10  val forbidden_thms =
   14.11   ["finite_intvl_succ_class",
    15.1 --- a/src/HOL/Orderings.thy	Wed Feb 10 14:12:02 2010 +0100
    15.2 +++ b/src/HOL/Orderings.thy	Wed Feb 10 14:12:04 2010 +0100
    15.3 @@ -11,6 +11,41 @@
    15.4    "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    15.5  begin
    15.6  
    15.7 +subsection {* Syntactic orders *}
    15.8 +
    15.9 +class ord =
   15.10 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   15.11 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   15.12 +begin
   15.13 +
   15.14 +notation
   15.15 +  less_eq  ("op <=") and
   15.16 +  less_eq  ("(_/ <= _)" [51, 51] 50) and
   15.17 +  less  ("op <") and
   15.18 +  less  ("(_/ < _)"  [51, 51] 50)
   15.19 +  
   15.20 +notation (xsymbols)
   15.21 +  less_eq  ("op \<le>") and
   15.22 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   15.23 +
   15.24 +notation (HTML output)
   15.25 +  less_eq  ("op \<le>") and
   15.26 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   15.27 +
   15.28 +abbreviation (input)
   15.29 +  greater_eq  (infix ">=" 50) where
   15.30 +  "x >= y \<equiv> y <= x"
   15.31 +
   15.32 +notation (input)
   15.33 +  greater_eq  (infix "\<ge>" 50)
   15.34 +
   15.35 +abbreviation (input)
   15.36 +  greater  (infix ">" 50) where
   15.37 +  "x > y \<equiv> y < x"
   15.38 +
   15.39 +end
   15.40 +
   15.41 +
   15.42  subsection {* Quasi orders *}
   15.43  
   15.44  class preorder = ord +
    16.1 --- a/src/HOL/Rings.thy	Wed Feb 10 14:12:02 2010 +0100
    16.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 14:12:04 2010 +0100
    16.3 @@ -782,15 +782,6 @@
    16.4  
    16.5  end
    16.6  
    16.7 -class abs_if = minus + uminus + ord + zero + abs +
    16.8 -  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
    16.9 -
   16.10 -class sgn_if = minus + uminus + zero + one + ord + sgn +
   16.11 -  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   16.12 -
   16.13 -lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
   16.14 -by(simp add:sgn_if)
   16.15 -
   16.16  class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   16.17  begin
   16.18  
    17.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Feb 10 14:12:02 2010 +0100
    17.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Feb 10 14:12:04 2010 +0100
    17.3 @@ -80,10 +80,10 @@
    17.4    let
    17.5      val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
    17.6    in
    17.7 -    case try_proof (goals @{const_name Algebras.less}) solve_tac of
    17.8 +    case try_proof (goals @{const_name Orderings.less}) solve_tac of
    17.9        Solved thm => Less thm
   17.10      | Stuck thm =>
   17.11 -      (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of
   17.12 +      (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
   17.13           Solved thm2 => LessEq (thm2, thm)
   17.14         | Stuck thm2 =>
   17.15           if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
    18.1 --- a/src/HOL/Tools/Function/termination.ML	Wed Feb 10 14:12:02 2010 +0100
    18.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Feb 10 14:12:04 2010 +0100
    18.3 @@ -203,10 +203,10 @@
    18.4               HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
    18.5                 $ (m2 $ r) $ (m1 $ l)))))) tac
    18.6    in
    18.7 -    case try @{const_name Algebras.less} of
    18.8 +    case try @{const_name Orderings.less} of
    18.9         Solved thm => Less thm
   18.10       | Stuck thm =>
   18.11 -       (case try @{const_name Algebras.less_eq} of
   18.12 +       (case try @{const_name Orderings.less_eq} of
   18.13            Solved thm2 => LessEq (thm2, thm)
   18.14          | Stuck thm2 =>
   18.15            if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
    19.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 10 14:12:02 2010 +0100
    19.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 10 14:12:04 2010 +0100
    19.3 @@ -223,7 +223,7 @@
    19.4    @{const_name False},
    19.5    @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
    19.6    @{const_name Nat.one_nat_inst.one_nat},
    19.7 -  @{const_name Algebras.ord_class.less}, @{const_name Algebras.ord_class.less_eq},
    19.8 +  @{const_name Orderings.less}, @{const_name Orderings.less_eq},
    19.9    @{const_name Algebras.zero},
   19.10    @{const_name Algebras.one},  @{const_name Algebras.plus},
   19.11    @{const_name Nat.ord_nat_inst.less_eq_nat},
    20.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 10 14:12:02 2010 +0100
    20.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 10 14:12:04 2010 +0100
    20.3 @@ -73,10 +73,10 @@
    20.4  | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
    20.5  | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
    20.6    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
    20.7 -| Const (@{const_name Algebras.less}, _) $ y$ z =>
    20.8 +| Const (@{const_name Orderings.less}, _) $ y$ z =>
    20.9     if term_of x aconv y then Lt (Thm.dest_arg ct)
   20.10     else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
   20.11 -| Const (@{const_name Algebras.less_eq}, _) $ y $ z =>
   20.12 +| Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
   20.13     if term_of x aconv y then Le (Thm.dest_arg ct)
   20.14     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
   20.15  | Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
   20.16 @@ -217,10 +217,10 @@
   20.17    end
   20.18   | _ => addC $ (mulC $ one $ tm) $ zero;
   20.19  
   20.20 -fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) =
   20.21 -    lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s)
   20.22 -  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) =
   20.23 -    lin vs (Const (@{const_name Algebras.less}, T) $ t $ s)
   20.24 +fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) =
   20.25 +    lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s)
   20.26 +  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) =
   20.27 +    lin vs (Const (@{const_name Orderings.less}, T) $ t $ s)
   20.28    | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   20.29    | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
   20.30      HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
   20.31 @@ -295,11 +295,11 @@
   20.32     case (term_of t) of
   20.33      Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
   20.34      if x aconv y andalso member (op =)
   20.35 -      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   20.36 +      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   20.37      then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   20.38    | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
   20.39      if x aconv y andalso member (op =)
   20.40 -       [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   20.41 +       [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   20.42      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   20.43    | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
   20.44      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   20.45 @@ -337,11 +337,11 @@
   20.46    | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
   20.47    | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
   20.48      if x=y andalso member (op =)
   20.49 -      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   20.50 +      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   20.51      then cv (l div dest_numeral c) t else Thm.reflexive t
   20.52    | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
   20.53      if x=y andalso member (op =)
   20.54 -      [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   20.55 +      [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   20.56      then cv (l div dest_numeral c) t else Thm.reflexive t
   20.57    | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
   20.58      if x=y then
   20.59 @@ -560,8 +560,8 @@
   20.60  fun qf_of_term ps vs t =  case t
   20.61   of Const("True",_) => T
   20.62    | Const("False",_) => F
   20.63 -  | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   20.64 -  | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   20.65 +  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   20.66 +  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   20.67    | Const(@{const_name Rings.dvd},_)$t1$t2 =>
   20.68        (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
   20.69    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    21.1 --- a/src/HOL/Tools/inductive.ML	Wed Feb 10 14:12:02 2010 +0100
    21.2 +++ b/src/HOL/Tools/inductive.ML	Wed Feb 10 14:12:04 2010 +0100
    21.3 @@ -184,7 +184,7 @@
    21.4      case concl_of thm of
    21.5        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    21.6      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    21.7 -    | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) =>
    21.8 +    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
    21.9        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   21.10          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
   21.11      | _ => thm
   21.12 @@ -561,7 +561,7 @@
   21.13           (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
   21.14  
   21.15      val ind_concl = HOLogic.mk_Trueprop
   21.16 -      (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred));
   21.17 +      (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
   21.18  
   21.19      val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
   21.20  
    22.1 --- a/src/HOL/Tools/int_arith.ML	Wed Feb 10 14:12:02 2010 +0100
    22.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Feb 10 14:12:04 2010 +0100
    22.3 @@ -55,7 +55,7 @@
    22.4        @{const_name Algebras.times}, @{const_name Algebras.uminus},
    22.5        @{const_name Algebras.minus}, @{const_name Algebras.plus},
    22.6        @{const_name Algebras.zero},
    22.7 -      @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
    22.8 +      @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    22.9    | check (a $ b) = check a andalso check b
   22.10    | check _ = false;
   22.11  
    23.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Feb 10 14:12:02 2010 +0100
    23.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 10 14:12:04 2010 +0100
    23.3 @@ -229,8 +229,8 @@
    23.4    val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
    23.5  in
    23.6    case rel of
    23.7 -    @{const_name Algebras.less}    => SOME (p, i, "<", q, j)
    23.8 -  | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j)
    23.9 +    @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
   23.10 +  | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
   23.11    | "op ="              => SOME (p, i, "=", q, j)
   23.12    | _                   => NONE
   23.13  end handle Rat.DIVZERO => NONE;
   23.14 @@ -292,7 +292,7 @@
   23.15      case head_of lhs of
   23.16        Const (a, _) => member (op =) [@{const_name Orderings.max},
   23.17                                      @{const_name Orderings.min},
   23.18 -                                    @{const_name Algebras.abs},
   23.19 +                                    @{const_name Groups.abs},
   23.20                                      @{const_name Algebras.minus},
   23.21                                      "Int.nat" (*DYNAMIC BINDING!*),
   23.22                                      "Divides.div_class.mod" (*DYNAMIC BINDING!*),
   23.23 @@ -372,7 +372,7 @@
   23.24          val rev_terms     = rev terms
   23.25          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   23.26          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   23.27 -        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
   23.28 +        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   23.29                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   23.30          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   23.31          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   23.32 @@ -387,7 +387,7 @@
   23.33          val rev_terms     = rev terms
   23.34          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   23.35          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   23.36 -        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
   23.37 +        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   23.38                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   23.39          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   23.40          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   23.41 @@ -397,16 +397,16 @@
   23.42          SOME [(Ts, subgoal1), (Ts, subgoal2)]
   23.43        end
   23.44      (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
   23.45 -    | (Const (@{const_name Algebras.abs}, _), [t1]) =>
   23.46 +    | (Const (@{const_name Groups.abs}, _), [t1]) =>
   23.47        let
   23.48          val rev_terms   = rev terms
   23.49          val terms1      = map (subst_term [(split_term, t1)]) rev_terms
   23.50          val terms2      = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
   23.51                              split_type --> split_type) $ t1)]) rev_terms
   23.52          val zero        = Const (@{const_name Algebras.zero}, split_type)
   23.53 -        val zero_leq_t1 = Const (@{const_name Algebras.less_eq},
   23.54 +        val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
   23.55                              split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   23.56 -        val t1_lt_zero  = Const (@{const_name Algebras.less},
   23.57 +        val t1_lt_zero  = Const (@{const_name Orderings.less},
   23.58                              split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
   23.59          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   23.60          val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
   23.61 @@ -427,7 +427,7 @@
   23.62                                  (map (incr_boundvars 1) rev_terms)
   23.63          val t1'             = incr_boundvars 1 t1
   23.64          val t2'             = incr_boundvars 1 t2
   23.65 -        val t1_lt_t2        = Const (@{const_name Algebras.less},
   23.66 +        val t1_lt_t2        = Const (@{const_name Orderings.less},
   23.67                                  split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   23.68          val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   23.69                                  (Const (@{const_name Algebras.plus},
   23.70 @@ -451,7 +451,7 @@
   23.71          val t1'         = incr_boundvars 1 t1
   23.72          val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   23.73                              (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
   23.74 -        val t1_lt_zero  = Const (@{const_name Algebras.less},
   23.75 +        val t1_lt_zero  = Const (@{const_name Orderings.less},
   23.76                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   23.77          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   23.78          val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
   23.79 @@ -477,7 +477,7 @@
   23.80                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   23.81          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   23.82                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   23.83 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
   23.84 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
   23.85                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   23.86          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   23.87                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
   23.88 @@ -509,7 +509,7 @@
   23.89                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   23.90          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   23.91                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   23.92 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
   23.93 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
   23.94                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   23.95          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   23.96                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
   23.97 @@ -545,17 +545,17 @@
   23.98          val t2'                     = incr_boundvars 2 t2
   23.99          val t2_eq_zero              = Const ("op =",
  23.100                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  23.101 -        val zero_lt_t2              = Const (@{const_name Algebras.less},
  23.102 +        val zero_lt_t2              = Const (@{const_name Orderings.less},
  23.103                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  23.104 -        val t2_lt_zero              = Const (@{const_name Algebras.less},
  23.105 +        val t2_lt_zero              = Const (@{const_name Orderings.less},
  23.106                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
  23.107 -        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
  23.108 +        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
  23.109                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  23.110 -        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
  23.111 +        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
  23.112                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  23.113 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
  23.114 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
  23.115                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  23.116 -        val t2_lt_j                 = Const (@{const_name Algebras.less},
  23.117 +        val t2_lt_j                 = Const (@{const_name Orderings.less},
  23.118                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  23.119          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  23.120                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  23.121 @@ -599,17 +599,17 @@
  23.122          val t2'                     = incr_boundvars 2 t2
  23.123          val t2_eq_zero              = Const ("op =",
  23.124                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  23.125 -        val zero_lt_t2              = Const (@{const_name Algebras.less},
  23.126 +        val zero_lt_t2              = Const (@{const_name Orderings.less},
  23.127                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  23.128 -        val t2_lt_zero              = Const (@{const_name Algebras.less},
  23.129 +        val t2_lt_zero              = Const (@{const_name Orderings.less},
  23.130                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
  23.131 -        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
  23.132 +        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
  23.133                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  23.134 -        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
  23.135 +        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
  23.136                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  23.137 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
  23.138 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
  23.139                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  23.140 -        val t2_lt_j                 = Const (@{const_name Algebras.less},
  23.141 +        val t2_lt_j                 = Const (@{const_name Orderings.less},
  23.142                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  23.143          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  23.144                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
    24.1 --- a/src/HOL/Tools/nat_arith.ML	Wed Feb 10 14:12:02 2010 +0100
    24.2 +++ b/src/HOL/Tools/nat_arith.ML	Wed Feb 10 14:12:04 2010 +0100
    24.3 @@ -69,16 +69,16 @@
    24.4  structure LessCancelSums = CancelSumsFun
    24.5  (struct
    24.6    open CommonCancelSums;
    24.7 -  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
    24.8 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
    24.9 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
   24.10 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
   24.11    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   24.12  end);
   24.13  
   24.14  structure LeCancelSums = CancelSumsFun
   24.15  (struct
   24.16    open CommonCancelSums;
   24.17 -  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
   24.18 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
   24.19 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
   24.20 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
   24.21    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   24.22  end);
   24.23  
    25.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Feb 10 14:12:02 2010 +0100
    25.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Feb 10 14:12:04 2010 +0100
    25.3 @@ -176,8 +176,8 @@
    25.4  structure LessCancelNumerals = CancelNumeralsFun
    25.5   (open CancelNumeralsCommon
    25.6    val prove_conv = Arith_Data.prove_conv
    25.7 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
    25.8 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
    25.9 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   25.10 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   25.11    val bal_add1 = @{thm nat_less_add_iff1} RS trans
   25.12    val bal_add2 = @{thm nat_less_add_iff2} RS trans
   25.13  );
   25.14 @@ -185,8 +185,8 @@
   25.15  structure LeCancelNumerals = CancelNumeralsFun
   25.16   (open CancelNumeralsCommon
   25.17    val prove_conv = Arith_Data.prove_conv
   25.18 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   25.19 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   25.20 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   25.21 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   25.22    val bal_add1 = @{thm nat_le_add_iff1} RS trans
   25.23    val bal_add2 = @{thm nat_le_add_iff2} RS trans
   25.24  );
   25.25 @@ -308,8 +308,8 @@
   25.26  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   25.27   (open CancelNumeralFactorCommon
   25.28    val prove_conv = Arith_Data.prove_conv
   25.29 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   25.30 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   25.31 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   25.32 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   25.33    val cancel = @{thm nat_mult_less_cancel1} RS trans
   25.34    val neg_exchanges = true
   25.35  )
   25.36 @@ -317,8 +317,8 @@
   25.37  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   25.38   (open CancelNumeralFactorCommon
   25.39    val prove_conv = Arith_Data.prove_conv
   25.40 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   25.41 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   25.42 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   25.43 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   25.44    val cancel = @{thm nat_mult_le_cancel1} RS trans
   25.45    val neg_exchanges = true
   25.46  )
   25.47 @@ -387,16 +387,16 @@
   25.48  structure LessCancelFactor = ExtractCommonTermFun
   25.49   (open CancelFactorCommon
   25.50    val prove_conv = Arith_Data.prove_conv
   25.51 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   25.52 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   25.53 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   25.54 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   25.55    fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
   25.56  );
   25.57  
   25.58  structure LeCancelFactor = ExtractCommonTermFun
   25.59   (open CancelFactorCommon
   25.60    val prove_conv = Arith_Data.prove_conv
   25.61 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   25.62 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   25.63 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   25.64 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   25.65    fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
   25.66  );
   25.67  
    26.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 14:12:02 2010 +0100
    26.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 14:12:04 2010 +0100
    26.3 @@ -229,8 +229,8 @@
    26.4  structure LessCancelNumerals = CancelNumeralsFun
    26.5   (open CancelNumeralsCommon
    26.6    val prove_conv = Arith_Data.prove_conv
    26.7 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
    26.8 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
    26.9 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   26.10 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   26.11    val bal_add1 = @{thm less_add_iff1} RS trans
   26.12    val bal_add2 = @{thm less_add_iff2} RS trans
   26.13  );
   26.14 @@ -238,8 +238,8 @@
   26.15  structure LeCancelNumerals = CancelNumeralsFun
   26.16   (open CancelNumeralsCommon
   26.17    val prove_conv = Arith_Data.prove_conv
   26.18 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   26.19 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   26.20 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   26.21 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   26.22    val bal_add1 = @{thm le_add_iff1} RS trans
   26.23    val bal_add2 = @{thm le_add_iff2} RS trans
   26.24  );
   26.25 @@ -409,8 +409,8 @@
   26.26  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   26.27   (open CancelNumeralFactorCommon
   26.28    val prove_conv = Arith_Data.prove_conv
   26.29 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   26.30 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   26.31 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   26.32 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   26.33    val cancel = @{thm mult_less_cancel_left} RS trans
   26.34    val neg_exchanges = true
   26.35  )
   26.36 @@ -418,8 +418,8 @@
   26.37  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   26.38   (open CancelNumeralFactorCommon
   26.39    val prove_conv = Arith_Data.prove_conv
   26.40 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   26.41 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   26.42 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   26.43 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   26.44    val cancel = @{thm mult_le_cancel_left} RS trans
   26.45    val neg_exchanges = true
   26.46  )
   26.47 @@ -485,7 +485,7 @@
   26.48  fun sign_conv pos_th neg_th ss t =
   26.49    let val T = fastype_of t;
   26.50        val zero = Const(@{const_name Algebras.zero}, T);
   26.51 -      val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT);
   26.52 +      val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
   26.53        val pos = less $ zero $ t and neg = less $ t $ zero
   26.54        fun prove p =
   26.55          Option.map Eq_True_elim (Lin_Arith.simproc ss p)
   26.56 @@ -524,8 +524,8 @@
   26.57  structure LeCancelFactor = ExtractCommonTermFun
   26.58   (open CancelFactorCommon
   26.59    val prove_conv = Arith_Data.prove_conv
   26.60 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   26.61 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   26.62 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   26.63 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   26.64    val simp_conv = sign_conv
   26.65      @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
   26.66  );
   26.67 @@ -534,8 +534,8 @@
   26.68  structure LessCancelFactor = ExtractCommonTermFun
   26.69   (open CancelFactorCommon
   26.70    val prove_conv = Arith_Data.prove_conv
   26.71 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   26.72 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   26.73 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   26.74 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   26.75    val simp_conv = sign_conv
   26.76      @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
   26.77  );
    27.1 --- a/src/HOL/Tools/refute.ML	Wed Feb 10 14:12:02 2010 +0100
    27.2 +++ b/src/HOL/Tools/refute.ML	Wed Feb 10 14:12:04 2010 +0100
    27.3 @@ -708,7 +708,7 @@
    27.4        (* other optimizations *)
    27.5        | Const (@{const_name Finite_Set.card}, _) => t
    27.6        | Const (@{const_name Finite_Set.finite}, _) => t
    27.7 -      | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
    27.8 +      | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
    27.9          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
   27.10        | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
   27.11          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   27.12 @@ -883,7 +883,7 @@
   27.13        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
   27.14        | Const (@{const_name Finite_Set.finite}, T) =>
   27.15          collect_type_axioms T axs
   27.16 -      | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
   27.17 +      | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
   27.18          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   27.19            collect_type_axioms T axs
   27.20        | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
   27.21 @@ -2771,7 +2771,7 @@
   27.22  
   27.23    fun Nat_less_interpreter thy model args t =
   27.24      case t of
   27.25 -      Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
   27.26 +      Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
   27.27          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   27.28        let
   27.29          val size_of_nat = size_of_type thy model (Type ("nat", []))
    28.1 --- a/src/HOL/Tools/res_clause.ML	Wed Feb 10 14:12:02 2010 +0100
    28.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Feb 10 14:12:04 2010 +0100
    28.3 @@ -99,7 +99,7 @@
    28.4  (*Provide readable names for the more common symbolic functions*)
    28.5  val const_trans_table =
    28.6        Symtab.make [(@{const_name "op ="}, "equal"),
    28.7 -                   (@{const_name Algebras.less_eq}, "lessequals"),
    28.8 +                   (@{const_name Orderings.less_eq}, "lessequals"),
    28.9                     (@{const_name "op &"}, "and"),
   28.10                     (@{const_name "op |"}, "or"),
   28.11                     (@{const_name "op -->"}, "implies"),
    29.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 14:12:02 2010 +0100
    29.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 14:12:04 2010 +0100
    29.3 @@ -95,8 +95,8 @@
    29.4        | fm ((c as Const("True", _))) = c
    29.5        | fm ((c as Const("False", _))) = c
    29.6        | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    29.7 -      | fm (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    29.8 -      | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    29.9 +      | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   29.10 +      | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   29.11        | fm t = replace t
   29.12      (*entry point, and abstraction of a meta-formula*)
   29.13      fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    30.1 --- a/src/HOL/ex/svc_funcs.ML	Wed Feb 10 14:12:02 2010 +0100
    30.2 +++ b/src/HOL/ex/svc_funcs.ML	Wed Feb 10 14:12:04 2010 +0100
    30.3 @@ -107,8 +107,8 @@
    30.4                           b1 orelse b2)
    30.5                       end
    30.6                   else (*might be numeric equality*) (t, is_intnat T)
    30.7 -           | Const(@{const_name Algebras.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
    30.8 -           | Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
    30.9 +           | Const(@{const_name Orderings.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
   30.10 +           | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
   30.11             | _ => (t, false)
   30.12           end
   30.13     in #1 o tag end;
   30.14 @@ -211,13 +211,13 @@
   30.15                     else fail t
   30.16              end
   30.17          (*inequalities: possible types are nat, int, real*)
   30.18 -      | fm pos (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ x $ y) =
   30.19 +      | fm pos (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ x $ y) =
   30.20              if not pos orelse T = HOLogic.realT then
   30.21                  Buildin("<", [tm x, tm y])
   30.22              else if is_intnat T then
   30.23                  Buildin("<=", [suc (tm x), tm y])
   30.24              else fail t
   30.25 -      | fm pos (t as Const(@{const_name Algebras.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   30.26 +      | fm pos (t as Const(@{const_name Orderings.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   30.27              if pos orelse T = HOLogic.realT then
   30.28                  Buildin("<=", [tm x, tm y])
   30.29              else if is_intnat T then