--- a/src/HOL/Hyperreal/StarClasses.thy Tue Nov 06 08:47:25 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy Tue Nov 06 08:47:30 2007 +0100
@@ -326,13 +326,19 @@
instance star :: (pordered_ab_semigroup_add_imp_le) pordered_ab_semigroup_add_imp_le
by (intro_classes, transfer, rule add_le_imp_le_left)
+instance star :: (pordered_comm_monoid_add) pordered_comm_monoid_add ..
instance star :: (pordered_ab_group_add) pordered_ab_group_add ..
+
+instance star :: (pordered_ab_group_add_abs) pordered_ab_group_add_abs
+ by intro_classes (transfer,
+ simp add: abs_ge_self abs_leI abs_triangle_ineq)+
+
instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
-instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
-instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
-instance star :: (lordered_ab_group) lordered_ab_group ..
+instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
+instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
+instance star :: (lordered_ab_group_add) lordered_ab_group_add ..
-instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
+instance star :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs
by (intro_classes, transfer, rule abs_lattice)
subsection {* Ring and field classes *}
@@ -411,6 +417,8 @@
by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
instance star :: (pordered_ring) pordered_ring ..
+instance star :: (pordered_ring_abs) pordered_ring_abs
+ by intro_classes (transfer, rule abs_eq_mult)
instance star :: (lordered_ring) lordered_ring ..
instance star :: (abs_if) abs_if
--- a/src/HOL/MetisExamples/BigO.thy Tue Nov 06 08:47:25 2007 +0100
+++ b/src/HOL/MetisExamples/BigO.thy Tue Nov 06 08:47:30 2007 +0100
@@ -25,8 +25,8 @@
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto);
- apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_le_mult)
+ apply (rule_tac x = "abs c" in exI, auto)
+ apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
done
(*** Now various verions with an increasing modulus ***)
@@ -858,11 +858,12 @@
apply (simp add: bigo_def abs_mult)
proof (neg_clausify)
fix x
-assume 0: "\<And>xa. \<not> \<bar>c\<bar> * \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. \<not> \<bar>c * f (x X2)\<bar> \<le> X2 * \<bar>f (x X2)\<bar>"
- by (metis 0 abs_mult)
+assume 0: "\<And>xa\<Colon>'b\<Colon>ordered_idom.
+ \<not> \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> *
+ \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
+ \<le> xa * \<bar>f (x xa)\<bar>"
show "False"
- by (metis 1 abs_le_mult)
+ by (metis linorder_neq_iff linorder_antisym_conv1 0)
qed
lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
--- a/src/HOL/Ring_and_Field.thy Tue Nov 06 08:47:25 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy Tue Nov 06 08:47:30 2007 +0100
@@ -353,6 +353,8 @@
subclass pordered_cancel_semiring by unfold_locales
+subclass pordered_comm_monoid_add by unfold_locales
+
lemma mult_left_less_imp_less:
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
by (force simp add: mult_left_mono not_le [symmetric])
@@ -514,14 +516,6 @@
end
-class lordered_ring = pordered_ring + lordered_ab_group_abs
-begin
-
-subclass lordered_ab_group_meet by unfold_locales
-subclass lordered_ab_group_join by unfold_locales
-
-end
-
class abs_if = minus + ord + zero + abs +
assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
@@ -529,30 +523,32 @@
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
class ordered_ring = ring + ordered_semiring
- + lordered_ab_group + abs_if
- -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
- @{text lordered_ab_group}*}
-
-instance ordered_ring \<subseteq> lordered_ring
-proof
- fix x :: 'a
- show "\<bar>x\<bar> = sup x (- x)"
- by (simp only: abs_if sup_eq_if)
-qed
+ + ordered_ab_group_add + abs_if
+begin
+
+subclass pordered_ring by unfold_locales
+
+subclass pordered_ab_group_add_abs
+proof unfold_locales
+ fix a b
+ show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
+ by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
+ (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
+ neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
+ auto intro!: less_imp_le add_neg_neg)
+qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
+
+end
(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
*)
class ordered_ring_strict = ring + ordered_semiring_strict
- + lordered_ab_group + abs_if
- -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
- @{text lordered_ab_group}*}
-
-instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes
-
-context ordered_ring_strict
+ + ordered_ab_group_add + abs_if
begin
+subclass ordered_ring by unfold_locales
+
lemma mult_strict_left_mono_neg:
"b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
apply (drule mult_strict_left_mono [of _ _ "uminus c"])
@@ -571,6 +567,12 @@
end
+instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
+apply intro_classes
+apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
+apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
+done
+
lemma zero_less_mult_iff:
fixes a :: "'a::ordered_ring_strict"
shows "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
@@ -579,12 +581,6 @@
apply (blast dest: zero_less_mult_pos2)
done
-instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
-apply intro_classes
-apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
-apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
-done
-
lemma zero_le_mult_iff:
"((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
@@ -637,7 +633,7 @@
class ordered_idom =
comm_ring_1 +
ordered_comm_semiring_strict +
- lordered_ab_group +
+ ordered_ab_group_add +
abs_if + sgn_if
(*previously ordered_ring*)
@@ -652,8 +648,6 @@
assumes "x \<noteq> y" obtains "x < y" | "y < x"
using assms by (rule linorder_neqE)
--- {* FIXME continue localization here *}
-
text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}
theorems available to members of @{term ordered_idom} *}
@@ -2006,12 +2000,29 @@
subsection {* Absolute Value *}
-lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
-using less_linear[of x 0]
-by(auto simp: sgn_if abs_if)
+context ordered_idom
+begin
+
+lemma mult_sgn_abs: "sgn x * abs x = x"
+ unfolding abs_if sgn_if by auto
+
+end
lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
-by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
+ by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
+
+class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
+ assumes abs_eq_mult:
+ "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
+
+
+class lordered_ring = pordered_ring + lordered_ab_group_add_abs
+begin
+
+subclass lordered_ab_group_add_meet by unfold_locales
+subclass lordered_ab_group_add_join by unfold_locales
+
+end
lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
proof -
@@ -2054,9 +2065,11 @@
done
qed
-lemma abs_eq_mult:
- assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
- shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"
+instance lordered_ring \<subseteq> pordered_ring_abs
+proof
+ fix a b :: "'a\<Colon> lordered_ring"
+ assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
+ show "abs (a*b) = abs a * abs b"
proof -
have s: "(0 <= a*b) | (a*b <= 0)"
apply (auto)
@@ -2094,12 +2107,17 @@
done
qed
qed
+qed
+
+instance ordered_idom \<subseteq> pordered_ring_abs
+by default (auto simp add: abs_if not_less
+ equal_neg_zero neg_equal_zero mult_less_0_iff)
lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)"
-by (simp add: abs_eq_mult linorder_linear)
+ by (simp add: abs_eq_mult linorder_linear)
lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
-by (simp add: abs_if)
+ by (simp add: abs_if)
lemma nonzero_abs_inverse:
"a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
@@ -2134,29 +2152,27 @@
thus ?thesis by (simp add: ac cpos mult_strict_mono)
qed
-lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"
-by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
+lemmas eq_minus_self_iff = equal_neg_zero
lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
-by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
+ unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))"
apply (simp add: order_less_le abs_le_iff)
-apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
-apply (simp add: le_minus_self_iff linorder_neq_iff)
+apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
done
lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==>
- (abs y) * x = abs (y * x)";
- apply (subst abs_mult);
- apply simp;
-done;
+ (abs y) * x = abs (y * x)"
+ apply (subst abs_mult)
+ apply simp
+done
lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==>
- abs x / y = abs (x / y)";
- apply (subst abs_divide);
- apply (simp add: order_less_imp_le);
-done;
+ abs x / y = abs (x / y)"
+ apply (subst abs_divide)
+ apply (simp add: order_less_imp_le)
+done
subsection {* Bounds of products via negative and positive Part *}