--- a/src/HOL/Algebras.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Algebras.thy Wed Feb 10 14:12:04 2010 +0100
@@ -55,7 +55,7 @@
end
-subsection {* Generic algebraic operations *}
+subsection {* Generic syntactic operations *}
class zero =
fixes zero :: 'a ("0")
@@ -63,6 +63,13 @@
class one =
fixes one :: 'a ("1")
+hide (open) const zero one
+
+syntax
+ "_index1" :: index ("\<^sub>1")
+translations
+ (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
+
lemma Let_0 [simp]: "Let 0 f = f 0"
unfolding Let_def ..
@@ -89,8 +96,6 @@
in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
*} -- {* show types that are presumably too general *}
-hide (open) const zero one
-
class plus =
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
@@ -103,51 +108,4 @@
class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-class abs =
- fixes abs :: "'a \<Rightarrow> 'a"
-begin
-
-notation (xsymbols)
- abs ("\<bar>_\<bar>")
-
-notation (HTML output)
- abs ("\<bar>_\<bar>")
-
-end
-
-class sgn =
- fixes sgn :: "'a \<Rightarrow> 'a"
-
-class ord =
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-begin
-
-notation
- less_eq ("op <=") and
- less_eq ("(_/ <= _)" [51, 51] 50) and
- less ("op <") and
- less ("(_/ < _)" [51, 51] 50)
-
-notation (xsymbols)
- less_eq ("op \<le>") and
- less_eq ("(_/ \<le> _)" [51, 51] 50)
-
-notation (HTML output)
- less_eq ("op \<le>") and
- less_eq ("(_/ \<le> _)" [51, 51] 50)
-
-abbreviation (input)
- greater_eq (infix ">=" 50) where
- "x >= y \<equiv> y <= x"
-
-notation (input)
- greater_eq (infix "\<ge>" 50)
-
-abbreviation (input)
- greater (infix ">" 50) where
- "x > y \<equiv> y < x"
-
-end
-
end
\ No newline at end of file
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 14:12:04 2010 +0100
@@ -684,7 +684,7 @@
fun xnormalize_conv ctxt [] ct = reflexive ct
| xnormalize_conv ctxt (vs as (x::_)) ct =
case term_of ct of
- Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) =>
+ Const(@{const_name Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -727,7 +727,7 @@
| _ => reflexive ct)
-| Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
+| Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -816,7 +816,7 @@
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
in
fun field_isolate_conv phi ctxt vs ct = case term_of ct of
- Const(@{const_name Algebras.less},_)$a$b =>
+ Const(@{const_name Orderings.less},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -825,7 +825,7 @@
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const(@{const_name Algebras.less_eq},_)$a$b =>
+| Const(@{const_name Orderings.less_eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -856,11 +856,11 @@
else Ferrante_Rackoff_Data.Nox
| @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
- | Const(@{const_name Algebras.less},_)$y$z =>
+ | Const(@{const_name Orderings.less},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
else Ferrante_Rackoff_Data.Nox
- | Const (@{const_name Algebras.less_eq},_)$y$z =>
+ | Const (@{const_name Orderings.less_eq},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Le
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
else Ferrante_Rackoff_Data.Nox
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 14:12:04 2010 +0100
@@ -2958,8 +2958,8 @@
val disjt = @{term "op |"};
val impt = @{term "op -->"};
val ifft = @{term "op = :: bool => _"}
-fun llt rT = Const(@{const_name Algebras.less},rrT rT);
-fun lle rT = Const(@{const_name Algebras.less},rrT rT);
+fun llt rT = Const(@{const_name Orderings.less},rrT rT);
+fun lle rT = Const(@{const_name Orderings.less},rrT rT);
fun eqt rT = Const("op =",rrT rT);
fun rz rT = Const(@{const_name Algebras.zero},rT);
@@ -3024,9 +3024,9 @@
| Const("op =",ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
- | Const(@{const_name Algebras.less},_)$p$q =>
+ | Const(@{const_name Orderings.less},_)$p$q =>
@{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
- | Const(@{const_name Algebras.less_eq},_)$p$q =>
+ | Const(@{const_name Orderings.less_eq},_)$p$q =>
@{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const("Ex",_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
--- a/src/HOL/Groebner_Basis.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Groebner_Basis.thy Wed Feb 10 14:12:04 2010 +0100
@@ -556,14 +556,14 @@
fun proc3 phi ss ct =
(case term_of ct of
- Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -577,14 +577,14 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
--- a/src/HOL/Groups.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Groups.thy Wed Feb 10 14:12:04 2010 +0100
@@ -5,7 +5,7 @@
header {* Groups, also combined with orderings *}
theory Groups
-imports Lattices
+imports Orderings
uses "~~/src/Provers/Arith/abel_cancel.ML"
begin
@@ -40,6 +40,7 @@
Of course it also works for fields, but it knows nothing about multiplicative
inverses or division. This is catered for by @{text field_simps}. *}
+
subsection {* Semigroups and Monoids *}
class semigroup_add = plus +
@@ -884,6 +885,32 @@
shows "[|0\<le>a; b<c|] ==> b < a + c"
by (insert add_le_less_mono [of 0 a b c], simp)
+class abs =
+ fixes abs :: "'a \<Rightarrow> 'a"
+begin
+
+notation (xsymbols)
+ abs ("\<bar>_\<bar>")
+
+notation (HTML output)
+ abs ("\<bar>_\<bar>")
+
+end
+
+class sgn =
+ fixes sgn :: "'a \<Rightarrow> 'a"
+
+class abs_if = minus + uminus + ord + zero + abs +
+ assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
+
+class sgn_if = minus + uminus + zero + one + ord + sgn +
+ assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
+begin
+
+lemma sgn0 [simp]: "sgn 0 = 0"
+ by (simp add:sgn_if)
+
+end
class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
--- a/src/HOL/Hoare/hoare_tac.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Wed Feb 10 14:12:04 2010 +0100
@@ -58,7 +58,7 @@
let val T as Type ("fun",[t,_]) = fastype_of trm
in Collect_const t $ trm end;
-fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
fun Mset ctxt prop =
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed Feb 10 14:12:04 2010 +0100
@@ -166,7 +166,7 @@
import_theory prim_rec;
const_maps
- "<" > Algebras.less :: "[nat,nat]=>bool";
+ "<" > Orderings.less :: "[nat,nat]=>bool";
end_import;
@@ -181,7 +181,7 @@
">" > HOL4Compat.nat_gt
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
- "<=" > Algebras.less_eq :: "[nat,nat]=>bool"
+ "<=" > Orderings.less_eq :: "[nat,nat]=>bool"
"+" > Algebras.plus :: "[nat,nat]=>nat"
"*" > Algebras.times :: "[nat,nat]=>nat"
"-" > Algebras.minus :: "[nat,nat]=>nat"
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Wed Feb 10 14:12:04 2010 +0100
@@ -22,7 +22,7 @@
inv > Algebras.inverse :: "real => real"
real_add > Algebras.plus :: "[real,real] => real"
real_mul > Algebras.times :: "[real,real] => real"
- real_lt > Algebras.less :: "[real,real] => bool";
+ real_lt > Orderings.less :: "[real,real] => bool";
ignore_thms
real_TY_DEF
@@ -50,11 +50,11 @@
const_maps
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
- real_lte > Algebras.less_eq :: "[real,real] => bool"
+ real_lte > Orderings.less_eq :: "[real,real] => bool"
real_sub > Algebras.minus :: "[real,real] => real"
"/" > Algebras.divide :: "[real,real] => real"
pow > Power.power :: "[real,nat] => real"
- abs > Algebras.abs :: "real => real"
+ abs > Groups.abs :: "real => real"
real_of_num > RealDef.real :: "nat => real";
end_import;
--- a/src/HOL/Import/HOL/arithmetic.imp Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Wed Feb 10 14:12:04 2010 +0100
@@ -23,7 +23,7 @@
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
- "<=" > "Algebras.ord_class.less_eq" :: "nat => nat => bool"
+ "<=" > "Orderings.less_eq" :: "nat => nat => bool"
"-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
"+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
"*" > "Algebras.times_class.times" :: "nat => nat => nat"
--- a/src/HOL/Import/HOL/prim_rec.imp Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Import/HOL/prim_rec.imp Wed Feb 10 14:12:04 2010 +0100
@@ -18,7 +18,7 @@
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
"PRE" > "HOL4Base.prim_rec.PRE"
- "<" > "Algebras.less" :: "nat => nat => bool"
+ "<" > "Orderings.less" :: "nat => nat => bool"
thm_maps
"wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
--- a/src/HOL/Import/HOL/real.imp Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Import/HOL/real.imp Wed Feb 10 14:12:04 2010 +0100
@@ -12,11 +12,11 @@
"sum" > "HOL4Real.real.sum"
"real_sub" > "Algebras.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
- "real_lte" > "Algebras.less_eq" :: "real => real => bool"
+ "real_lte" > "Orderings.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"pow" > "Power.power_class.power" :: "real => nat => real"
- "abs" > "Algebras.abs" :: "real => real"
+ "abs" > "Groups.abs" :: "real => real"
"/" > "Ring.divide" :: "real => real => real"
thm_maps
--- a/src/HOL/Import/HOL/realax.imp Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Import/HOL/realax.imp Wed Feb 10 14:12:04 2010 +0100
@@ -29,7 +29,7 @@
"treal_0" > "HOL4Real.realax.treal_0"
"real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
"real_mul" > "Algebras.times_class.times" :: "real => real => real"
- "real_lt" > "Algebras.ord_class.less" :: "real => real => bool"
+ "real_lt" > "Orderings.less" :: "real => real => bool"
"real_add" > "Algebras.plus_class.plus" :: "real => real => real"
"real_1" > "Algebras.one_class.one" :: "real"
"real_0" > "Algebras.zero_class.zero" :: "real"
--- a/src/HOL/Mutabelle/Mutabelle.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Mutabelle/Mutabelle.thy Wed Feb 10 14:12:04 2010 +0100
@@ -16,7 +16,7 @@
(@{const_name dummy_pattern}, "'a::{}"),
(@{const_name Algebras.uminus}, "'a"),
(@{const_name Nat.size}, "'a"),
- (@{const_name Algebras.abs}, "'a")];
+ (@{const_name Groups.abs}, "'a")];
val forbidden_thms =
["finite_intvl_succ_class",
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Feb 10 14:12:04 2010 +0100
@@ -197,7 +197,7 @@
(@{const_name "dummy_pattern"}, "'a::{}") (*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
- (@{const_name "Algebras.abs"}, "'a") *)]
+ (@{const_name "Groups.abs"}, "'a") *)]
val forbidden_thms =
["finite_intvl_succ_class",
--- a/src/HOL/Orderings.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Orderings.thy Wed Feb 10 14:12:04 2010 +0100
@@ -11,6 +11,41 @@
"~~/src/Provers/quasi.ML" (* FIXME unused? *)
begin
+subsection {* Syntactic orders *}
+
+class ord =
+ fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+
+notation
+ less_eq ("op <=") and
+ less_eq ("(_/ <= _)" [51, 51] 50) and
+ less ("op <") and
+ less ("(_/ < _)" [51, 51] 50)
+
+notation (xsymbols)
+ less_eq ("op \<le>") and
+ less_eq ("(_/ \<le> _)" [51, 51] 50)
+
+notation (HTML output)
+ less_eq ("op \<le>") and
+ less_eq ("(_/ \<le> _)" [51, 51] 50)
+
+abbreviation (input)
+ greater_eq (infix ">=" 50) where
+ "x >= y \<equiv> y <= x"
+
+notation (input)
+ greater_eq (infix "\<ge>" 50)
+
+abbreviation (input)
+ greater (infix ">" 50) where
+ "x > y \<equiv> y < x"
+
+end
+
+
subsection {* Quasi orders *}
class preorder = ord +
--- a/src/HOL/Rings.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Rings.thy Wed Feb 10 14:12:04 2010 +0100
@@ -782,15 +782,6 @@
end
-class abs_if = minus + uminus + ord + zero + abs +
- assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
-
-class sgn_if = minus + uminus + zero + one + ord + sgn +
- assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
-
-lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
-by(simp add:sgn_if)
-
class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
begin
--- a/src/HOL/Tools/Function/lexicographic_order.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Wed Feb 10 14:12:04 2010 +0100
@@ -80,10 +80,10 @@
let
val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
in
- case try_proof (goals @{const_name Algebras.less}) solve_tac of
+ case try_proof (goals @{const_name Orderings.less}) solve_tac of
Solved thm => Less thm
| Stuck thm =>
- (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of
+ (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
--- a/src/HOL/Tools/Function/termination.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML Wed Feb 10 14:12:04 2010 +0100
@@ -203,10 +203,10 @@
HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
$ (m2 $ r) $ (m1 $ l)))))) tac
in
- case try @{const_name Algebras.less} of
+ case try @{const_name Orderings.less} of
Solved thm => Less thm
| Stuck thm =>
- (case try @{const_name Algebras.less_eq} of
+ (case try @{const_name Orderings.less_eq} of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 10 14:12:04 2010 +0100
@@ -223,7 +223,7 @@
@{const_name False},
@{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
@{const_name Nat.one_nat_inst.one_nat},
- @{const_name Algebras.ord_class.less}, @{const_name Algebras.ord_class.less_eq},
+ @{const_name Orderings.less}, @{const_name Orderings.less_eq},
@{const_name Algebras.zero},
@{const_name Algebras.one}, @{const_name Algebras.plus},
@{const_name Nat.ord_nat_inst.less_eq_nat},
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Feb 10 14:12:04 2010 +0100
@@ -73,10 +73,10 @@
| Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
-| Const (@{const_name Algebras.less}, _) $ y$ z =>
+| Const (@{const_name Orderings.less}, _) $ y$ z =>
if term_of x aconv y then Lt (Thm.dest_arg ct)
else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name Algebras.less_eq}, _) $ y $ z =>
+| Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
if term_of x aconv y then Le (Thm.dest_arg ct)
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
@@ -217,10 +217,10 @@
end
| _ => addC $ (mulC $ one $ tm) $ zero;
-fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) =
- lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s)
- | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) =
- lin vs (Const (@{const_name Algebras.less}, T) $ t $ s)
+fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) =
+ lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s)
+ | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) =
+ lin vs (Const (@{const_name Orderings.less}, T) $ t $ s)
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
| lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
@@ -295,11 +295,11 @@
case (term_of t) of
Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
- ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
+ ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
| Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
if x aconv y andalso member (op =)
- [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
+ [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
@@ -337,11 +337,11 @@
| Const (@{const_name Not},_)$_ => arg_conv unit_conv t
| Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
- ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
+ ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
| Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
if x=y andalso member (op =)
- [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
+ [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
| Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
if x=y then
@@ -560,8 +560,8 @@
fun qf_of_term ps vs t = case t
of Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
| Const(@{const_name Rings.dvd},_)$t1$t2 =>
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *)
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
--- a/src/HOL/Tools/inductive.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Feb 10 14:12:04 2010 +0100
@@ -184,7 +184,7 @@
case concl_of thm of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
| _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
- | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) =>
+ | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
| _ => thm
@@ -561,7 +561,7 @@
(list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
val ind_concl = HOLogic.mk_Trueprop
- (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred));
+ (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
--- a/src/HOL/Tools/int_arith.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/int_arith.ML Wed Feb 10 14:12:04 2010 +0100
@@ -55,7 +55,7 @@
@{const_name Algebras.times}, @{const_name Algebras.uminus},
@{const_name Algebras.minus}, @{const_name Algebras.plus},
@{const_name Algebras.zero},
- @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
+ @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
| check (a $ b) = check a andalso check b
| check _ = false;
--- a/src/HOL/Tools/lin_arith.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Wed Feb 10 14:12:04 2010 +0100
@@ -229,8 +229,8 @@
val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
in
case rel of
- @{const_name Algebras.less} => SOME (p, i, "<", q, j)
- | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j)
+ @{const_name Orderings.less} => SOME (p, i, "<", q, j)
+ | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
| "op =" => SOME (p, i, "=", q, j)
| _ => NONE
end handle Rat.DIVZERO => NONE;
@@ -292,7 +292,7 @@
case head_of lhs of
Const (a, _) => member (op =) [@{const_name Orderings.max},
@{const_name Orderings.min},
- @{const_name Algebras.abs},
+ @{const_name Groups.abs},
@{const_name Algebras.minus},
"Int.nat" (*DYNAMIC BINDING!*),
"Divides.div_class.mod" (*DYNAMIC BINDING!*),
@@ -372,7 +372,7 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const (@{const_name Algebras.less_eq},
+ val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -387,7 +387,7 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const (@{const_name Algebras.less_eq},
+ val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -397,16 +397,16 @@
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
(* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
- | (Const (@{const_name Algebras.abs}, _), [t1]) =>
+ | (Const (@{const_name Groups.abs}, _), [t1]) =>
let
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
split_type --> split_type) $ t1)]) rev_terms
val zero = Const (@{const_name Algebras.zero}, split_type)
- val zero_leq_t1 = Const (@{const_name Algebras.less_eq},
+ val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ t1
- val t1_lt_zero = Const (@{const_name Algebras.less},
+ val t1_lt_zero = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
@@ -427,7 +427,7 @@
(map (incr_boundvars 1) rev_terms)
val t1' = incr_boundvars 1 t1
val t2' = incr_boundvars 1 t2
- val t1_lt_t2 = Const (@{const_name Algebras.less},
+ val t1_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Algebras.plus},
@@ -451,7 +451,7 @@
val t1' = incr_boundvars 1 t1
val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
- val t1_lt_zero = Const (@{const_name Algebras.less},
+ val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
@@ -477,7 +477,7 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const (@{const_name Algebras.less},
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
@@ -509,7 +509,7 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const (@{const_name Algebras.less},
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
@@ -545,17 +545,17 @@
val t2' = incr_boundvars 2 t2
val t2_eq_zero = Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val zero_lt_t2 = Const (@{const_name Algebras.less},
+ val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
- val t2_lt_zero = Const (@{const_name Algebras.less},
+ val t2_lt_zero = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
- val zero_leq_j = Const (@{const_name Algebras.less_eq},
+ val zero_leq_j = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_leq_zero = Const (@{const_name Algebras.less_eq},
+ val j_leq_zero = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
- val j_lt_t2 = Const (@{const_name Algebras.less},
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t2_lt_j = Const (@{const_name Algebras.less},
+ val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
@@ -599,17 +599,17 @@
val t2' = incr_boundvars 2 t2
val t2_eq_zero = Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val zero_lt_t2 = Const (@{const_name Algebras.less},
+ val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
- val t2_lt_zero = Const (@{const_name Algebras.less},
+ val t2_lt_zero = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
- val zero_leq_j = Const (@{const_name Algebras.less_eq},
+ val zero_leq_j = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_leq_zero = Const (@{const_name Algebras.less_eq},
+ val j_leq_zero = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
- val j_lt_t2 = Const (@{const_name Algebras.less},
+ val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t2_lt_j = Const (@{const_name Algebras.less},
+ val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
--- a/src/HOL/Tools/nat_arith.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML Wed Feb 10 14:12:04 2010 +0100
@@ -69,16 +69,16 @@
structure LessCancelSums = CancelSumsFun
(struct
open CommonCancelSums;
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
end);
structure LeCancelSums = CancelSumsFun
(struct
open CommonCancelSums;
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
end);
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Wed Feb 10 14:12:04 2010 +0100
@@ -176,8 +176,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
val bal_add1 = @{thm nat_less_add_iff1} RS trans
val bal_add2 = @{thm nat_less_add_iff2} RS trans
);
@@ -185,8 +185,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
val bal_add1 = @{thm nat_le_add_iff1} RS trans
val bal_add2 = @{thm nat_le_add_iff2} RS trans
);
@@ -308,8 +308,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
val cancel = @{thm nat_mult_less_cancel1} RS trans
val neg_exchanges = true
)
@@ -317,8 +317,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
val cancel = @{thm nat_mult_le_cancel1} RS trans
val neg_exchanges = true
)
@@ -387,16 +387,16 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
);
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
);
--- a/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 14:12:04 2010 +0100
@@ -229,8 +229,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
val bal_add1 = @{thm less_add_iff1} RS trans
val bal_add2 = @{thm less_add_iff2} RS trans
);
@@ -238,8 +238,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
val bal_add1 = @{thm le_add_iff1} RS trans
val bal_add2 = @{thm le_add_iff2} RS trans
);
@@ -409,8 +409,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
val cancel = @{thm mult_less_cancel_left} RS trans
val neg_exchanges = true
)
@@ -418,8 +418,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
val cancel = @{thm mult_le_cancel_left} RS trans
val neg_exchanges = true
)
@@ -485,7 +485,7 @@
fun sign_conv pos_th neg_th ss t =
let val T = fastype_of t;
val zero = Const(@{const_name Algebras.zero}, T);
- val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT);
+ val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
fun prove p =
Option.map Eq_True_elim (Lin_Arith.simproc ss p)
@@ -524,8 +524,8 @@
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
val simp_conv = sign_conv
@{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
);
@@ -534,8 +534,8 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
val simp_conv = sign_conv
@{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
);
--- a/src/HOL/Tools/refute.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/refute.ML Wed Feb 10 14:12:04 2010 +0100
@@ -708,7 +708,7 @@
(* other optimizations *)
| Const (@{const_name Finite_Set.card}, _) => t
| Const (@{const_name Finite_Set.finite}, _) => t
- | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
| Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
@@ -883,7 +883,7 @@
| Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
| Const (@{const_name Finite_Set.finite}, T) =>
collect_type_axioms T axs
- | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
collect_type_axioms T axs
| Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
@@ -2771,7 +2771,7 @@
fun Nat_less_interpreter thy model args t =
case t of
- Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
--- a/src/HOL/Tools/res_clause.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/res_clause.ML Wed Feb 10 14:12:04 2010 +0100
@@ -99,7 +99,7 @@
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
Symtab.make [(@{const_name "op ="}, "equal"),
- (@{const_name Algebras.less_eq}, "lessequals"),
+ (@{const_name Orderings.less_eq}, "lessequals"),
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
(@{const_name "op -->"}, "implies"),
--- a/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 14:12:04 2010 +0100
@@ -95,8 +95,8 @@
| fm ((c as Const("True", _))) = c
| fm ((c as Const("False", _))) = c
| fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const(@{const_name Algebras.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
--- a/src/HOL/ex/svc_funcs.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML Wed Feb 10 14:12:04 2010 +0100
@@ -107,8 +107,8 @@
b1 orelse b2)
end
else (*might be numeric equality*) (t, is_intnat T)
- | Const(@{const_name Algebras.less}, Type ("fun", [T,_])) => (t, is_intnat T)
- | Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name Orderings.less}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
| _ => (t, false)
end
in #1 o tag end;
@@ -211,13 +211,13 @@
else fail t
end
(*inequalities: possible types are nat, int, real*)
- | fm pos (t as Const(@{const_name Algebras.less}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ x $ y) =
if not pos orelse T = HOLogic.realT then
Buildin("<", [tm x, tm y])
else if is_intnat T then
Buildin("<=", [suc (tm x), tm y])
else fail t
- | fm pos (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ x $ y) =
if pos orelse T = HOLogic.realT then
Buildin("<=", [tm x, tm y])
else if is_intnat T then