dropped accidental duplication of "lin" prefix from cs. 108662d50512
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 08 14:22:22 2010 +0100
@@ -637,7 +637,7 @@
using eq_diff_eq[where a= x and b=t and c=0] by simp
-interpretation class_dense_linlinordered_field: constr_dense_linorder
+interpretation class_dense_linordered_field: constr_dense_linorder
"op <=" "op <"
"\<lambda> x y. 1/2 * ((x::'a::{linordered_field,number_ring}) + y)"
proof (unfold_locales, dlo, dlo, auto)
@@ -871,7 +871,7 @@
addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}]
in
-Ferrante_Rackoff_Data.funs @{thm "class_dense_linlinordered_field.ferrack_axiom"}
+Ferrante_Rackoff_Data.funs @{thm "class_dense_linordered_field.ferrack_axiom"}
{isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
end
*}
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 08 14:22:22 2010 +0100
@@ -836,7 +836,7 @@
lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector
lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector
lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector
-lemma dot_pos_le[simp]: "(0::'a\<Colon>linlinordered_ring_strict) <= x \<bullet> x"
+lemma dot_pos_le[simp]: "(0::'a\<Colon>linordered_ring_strict) <= x \<bullet> x"
by (simp add: dot_def setsum_nonneg)
lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"
@@ -852,10 +852,10 @@
show ?case by (simp add: h)
qed
-lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linlinordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"
+lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"
by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq)
-lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linlinordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
+lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
by (auto simp add: le_less)
subsection{* The collapse of the general concepts to dimension one. *}
--- a/src/HOL/NSA/HyperDef.thy Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/NSA/HyperDef.thy Mon Feb 08 14:22:22 2010 +0100
@@ -501,12 +501,12 @@
by transfer (rule power_mult_distrib)
lemma hyperpow_two_le [simp]:
- "(0::'a::{monoid_mult,linlinordered_ring_strict} star) \<le> r pow (1 + 1)"
+ "(0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow (1 + 1)"
by (auto simp add: hyperpow_two zero_le_mult_iff)
lemma hrabs_hyperpow_two [simp]:
"abs(x pow (1 + 1)) =
- (x::'a::{monoid_mult,linlinordered_ring_strict} star) pow (1 + 1)"
+ (x::'a::{monoid_mult,linordered_ring_strict} star) pow (1 + 1)"
by (simp only: abs_of_nonneg hyperpow_two_le)
lemma hyperpow_two_hrabs [simp]:
--- a/src/HOL/NSA/StarDef.thy Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy Mon Feb 08 14:22:22 2010 +0100
@@ -912,7 +912,7 @@
instance star :: (ordered_cancel_semiring) ordered_cancel_semiring ..
-instance star :: (linlinordered_semiring_strict) linlinordered_semiring_strict
+instance star :: (linordered_semiring_strict) linordered_semiring_strict
apply (intro_classes)
apply (transfer, erule (1) mult_strict_left_mono)
apply (transfer, erule (1) mult_strict_right_mono)
@@ -936,7 +936,7 @@
instance star :: (sgn_if) sgn_if
by (intro_classes, transfer, rule sgn_if)
-instance star :: (linlinordered_ring_strict) linlinordered_ring_strict ..
+instance star :: (linordered_ring_strict) linordered_ring_strict ..
instance star :: (ordered_comm_ring) ordered_comm_ring ..
instance star :: (linordered_semidom) linordered_semidom
--- a/src/HOL/Nat_Numeral.thy Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy Mon Feb 08 14:22:22 2010 +0100
@@ -113,7 +113,7 @@
end
-context linlinordered_ring_strict
+context linordered_ring_strict
begin
lemma sum_squares_ge_zero:
--- a/src/HOL/Parity.thy Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Parity.thy Mon Feb 08 14:22:22 2010 +0100
@@ -218,7 +218,7 @@
done
lemma zero_le_even_power: "even n ==>
- 0 <= (x::'a::{linlinordered_ring_strict,monoid_mult}) ^ n"
+ 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
apply (simp add: even_nat_equiv_def2)
apply (erule exE)
apply (erule ssubst)
--- a/src/HOL/Ring_and_Field.thy Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Feb 08 14:22:22 2010 +0100
@@ -767,9 +767,9 @@
end
-class linlinordered_semiring_1 = linordered_semiring + semiring_1
-
-class linlinordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
+class linordered_semiring_1 = linordered_semiring + semiring_1
+
+class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
begin
@@ -886,7 +886,7 @@
end
-class linlinlinordered_semiring_1_strict = linlinordered_semiring_strict + semiring_1
+class linlinordered_semiring_1_strict = linordered_semiring_strict + semiring_1
class mult_mono1 = times + zero + ord +
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
@@ -918,7 +918,7 @@
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
begin
-subclass linlinordered_semiring_strict
+subclass linordered_semiring_strict
proof
fix a b c :: 'a
assume "a < b" "0 < c"
@@ -1009,9 +1009,9 @@
end
(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
- Basically, linordered_ring + no_zero_divisors = linlinordered_ring_strict.
+ Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
*)
-class linlinordered_ring_strict = ring + linlinordered_semiring_strict
+class linordered_ring_strict = ring + linordered_semiring_strict
+ ordered_ab_group_add + abs_if
begin
@@ -1207,7 +1207,7 @@
(*previously linordered_ring*)
begin
-subclass linlinordered_ring_strict ..
+subclass linordered_ring_strict ..
subclass ordered_comm_ring ..
subclass idom ..
@@ -1502,7 +1502,7 @@
"(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))"
by (simp add: linorder_not_less [symmetric])
-lemma linlinordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
+lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
proof
fix x::'a
have m1: "- (1::'a) < 0" by simp
@@ -1511,7 +1511,7 @@
thus "\<exists>y. y < x" by blast
qed
-lemma linlinordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
+lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
proof
fix x::'a
have m1: " (1::'a) > 0" by simp
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Feb 08 14:22:22 2010 +0100
@@ -581,11 +581,11 @@
["(l::'a::idom) * m = n",
"(l::'a::idom) = m * n"],
K EqCancelFactor.proc),
- ("linlinordered_ring_le_cancel_factor",
+ ("linordered_ring_le_cancel_factor",
["(l::'a::linordered_ring) * m <= n",
"(l::'a::linordered_ring) <= m * n"],
K LeCancelFactor.proc),
- ("linlinordered_ring_less_cancel_factor",
+ ("linordered_ring_less_cancel_factor",
["(l::'a::linordered_ring) * m < n",
"(l::'a::linordered_ring) < m * n"],
K LessCancelFactor.proc),