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