--- a/src/HOL/Finite_Set.thy Mon Nov 05 23:17:03 2007 +0100
+++ b/src/HOL/Finite_Set.thy Tue Nov 06 08:47:25 2007 +0100
@@ -1199,7 +1199,7 @@
qed
lemma setsum_abs[iff]:
- fixes f :: "'a => ('b::lordered_ab_group_abs)"
+ fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
proof (cases "finite A")
case True
@@ -1215,7 +1215,7 @@
qed
lemma setsum_abs_ge_zero[iff]:
- fixes f :: "'a => ('b::lordered_ab_group_abs)"
+ fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
shows "0 \<le> setsum (%i. abs(f i)) A"
proof (cases "finite A")
case True
@@ -1230,7 +1230,7 @@
qed
lemma abs_setsum_abs[simp]:
- fixes f :: "'a => ('b::lordered_ab_group_abs)"
+ fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
proof (cases "finite A")
case True
--- a/src/HOL/Matrix/Matrix.thy Mon Nov 05 23:17:03 2007 +0100
+++ b/src/HOL/Matrix/Matrix.thy Tue Nov 06 08:47:25 2007 +0100
@@ -22,12 +22,12 @@
instance matrix :: ("{plus, times, zero}") times
times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
-instance matrix :: (lordered_ab_group) abs
+instance matrix :: (lordered_ab_group_add) abs
abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
-instance matrix :: (lordered_ab_group) lordered_ab_group_meet
+instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
proof
- fix A B C :: "('a::lordered_ab_group) matrix"
+ fix A B C :: "('a::lordered_ab_group_add) matrix"
show "A + B + C = A + (B + C)"
apply (simp add: plus_matrix_def)
apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
@@ -89,7 +89,8 @@
done
qed
-lemma Rep_matrix_add[simp]: "Rep_matrix ((a::('a::lordered_ab_group)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)"
+lemma Rep_matrix_add[simp]:
+ "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)"
by (simp add: plus_matrix_def)
lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i =
@@ -98,13 +99,13 @@
apply (simp add: Rep_mult_matrix)
done
-lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
+lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
done
-lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
+lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
@@ -162,10 +163,10 @@
apply (simp_all add: mult_commute)
done
-lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B"
+lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)+B) = transpose_matrix A + transpose_matrix B"
by (simp add: plus_matrix_def transpose_combine_matrix)
-lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B"
+lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
by (simp add: diff_matrix_def transpose_combine_matrix)
lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
@@ -252,7 +253,7 @@
apply (simp add: max2)
done
-lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group) matrix)) = (move_matrix A j i) + (move_matrix B j i)"
+lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
@@ -280,7 +281,7 @@
apply (auto)
done
-lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
+lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group_add)) x y = - (Rep_matrix A x y)"
by (simp add: minus_matrix_def)
lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
--- a/src/HOL/Matrix/SparseMatrix.thy Mon Nov 05 23:17:03 2007 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy Tue Nov 06 08:47:25 2007 +0100
@@ -387,8 +387,8 @@
done
consts
- add_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> 'a spvec"
- add_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> 'a spmat"
+ add_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> 'a spvec"
+ add_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> 'a spmat"
recdef add_spvec "measure (% (a, b). length a + (length b))"
"add_spvec (arr, []) = arr"
@@ -569,8 +569,8 @@
done
consts
- le_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> bool"
- le_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> bool"
+ le_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> bool"
+ le_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> bool"
recdef le_spvec "measure (% (a,b). (length a) + (length b))"
"le_spvec ([], []) = True"
@@ -610,7 +610,7 @@
lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow>
- (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group) matrix))"
+ (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group_add) matrix))"
apply (auto)
apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
apply (intro strip)
@@ -640,19 +640,19 @@
by (auto simp add: disj_matrices_def)
lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
- (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group) matrix) <= 0)"
+ (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group_add) matrix) <= 0)"
by (rule disj_matrices_add[of A B 0 0, simplified])
lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
- (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group) matrix))"
+ (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group_add) matrix))"
by (rule disj_matrices_add[of 0 0 A B, simplified])
lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow>
- (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group) matrix))"
+ (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group_add) matrix))"
by (auto simp add: disj_matrices_add[of 0 A B C, simplified])
lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow>
- (B + A <= C) = (A <= C & (B::('a::lordered_ab_group) matrix) <= 0)"
+ (B + A <= C) = (A <= C & (B::('a::lordered_ab_group_add) matrix) <= 0)"
by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
lemma disj_sparse_row_singleton: "i <= j \<Longrightarrow> sorted_spvec((j,y)#v) \<Longrightarrow> disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)"
@@ -668,7 +668,7 @@
apply (simp_all)
done
-lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lordered_ab_group) matrix) (B+C)"
+lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lordered_ab_group_add) matrix) (B+C)"
apply (simp add: disj_matrices_def)
apply (auto)
apply (drule_tac j=j and i=i in spec2)+
@@ -677,7 +677,7 @@
apply (simp_all)
done
-lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lordered_ab_group) matrix)"
+lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lordered_ab_group_add) matrix)"
by (simp add: disj_matrices_x_add disj_matrices_commute)
lemma disj_singleton_matrices[simp]: "disj_matrices (singleton_matrix j i x) (singleton_matrix u v y) = (j \<noteq> u | i \<noteq> v | x = 0 | y = 0)"
@@ -897,10 +897,10 @@
lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
consts
- pprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
- nprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
- pprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
- nprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
+ pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
+ nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
+ pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
+ nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
primrec
"pprt_spvec [] = []"
--- a/src/HOL/OrderedGroup.thy Mon Nov 05 23:17:03 2007 +0100
+++ b/src/HOL/OrderedGroup.thy Tue Nov 06 08:47:25 2007 +0100
@@ -394,6 +394,78 @@
end
+subsection {* Support for reasoning about signs *}
+
+class pordered_comm_monoid_add =
+ pordered_cancel_ab_semigroup_add + comm_monoid_add
+begin
+
+lemma add_pos_nonneg:
+ assumes "0 < a" and "0 \<le> b"
+ shows "0 < a + b"
+proof -
+ have "0 + 0 < a + b"
+ using assms by (rule add_less_le_mono)
+ then show ?thesis by simp
+qed
+
+lemma add_pos_pos:
+ assumes "0 < a" and "0 < b"
+ shows "0 < a + b"
+ by (rule add_pos_nonneg) (insert assms, auto)
+
+lemma add_nonneg_pos:
+ assumes "0 \<le> a" and "0 < b"
+ shows "0 < a + b"
+proof -
+ have "0 + 0 < a + b"
+ using assms by (rule add_le_less_mono)
+ then show ?thesis by simp
+qed
+
+lemma add_nonneg_nonneg:
+ assumes "0 \<le> a" and "0 \<le> b"
+ shows "0 \<le> a + b"
+proof -
+ have "0 + 0 \<le> a + b"
+ using assms by (rule add_mono)
+ then show ?thesis by simp
+qed
+
+lemma add_neg_nonpos:
+ assumes "a < 0" and "b \<le> 0"
+ shows "a + b < 0"
+proof -
+ have "a + b < 0 + 0"
+ using assms by (rule add_less_le_mono)
+ then show ?thesis by simp
+qed
+
+lemma add_neg_neg:
+ assumes "a < 0" and "b < 0"
+ shows "a + b < 0"
+ by (rule add_neg_nonpos) (insert assms, auto)
+
+lemma add_nonpos_neg:
+ assumes "a \<le> 0" and "b < 0"
+ shows "a + b < 0"
+proof -
+ have "a + b < 0 + 0"
+ using assms by (rule add_le_less_mono)
+ then show ?thesis by simp
+qed
+
+lemma add_nonpos_nonpos:
+ assumes "a \<le> 0" and "b \<le> 0"
+ shows "a + b \<le> 0"
+proof -
+ have "a + b \<le> 0 + 0"
+ using assms by (rule add_mono)
+ then show ?thesis by simp
+qed
+
+end
+
class pordered_ab_group_add =
ab_group_add + pordered_ab_semigroup_add
begin
@@ -410,6 +482,9 @@
thus "a \<le> b" by simp
qed
+subclass pordered_comm_monoid_add
+ by unfold_locales
+
lemma max_diff_distrib_left:
shows "max x y - z = max (x - z) (y - z)"
by (simp add: diff_minus, rule max_add_distrib_left)
@@ -584,6 +659,65 @@
subclass ordered_cancel_ab_semigroup_add
by unfold_locales
+lemma neg_less_eq_nonneg:
+ "- a \<le> a \<longleftrightarrow> 0 \<le> a"
+proof
+ assume A: "- a \<le> a" show "0 \<le> a"
+ proof (rule classical)
+ assume "\<not> 0 \<le> a"
+ then have "a < 0" by auto
+ with A have "- a < 0" by (rule le_less_trans)
+ then show ?thesis by auto
+ qed
+next
+ assume A: "0 \<le> a" show "- a \<le> a"
+ proof (rule order_trans)
+ show "- a \<le> 0" using A by (simp add: minus_le_iff)
+ next
+ show "0 \<le> a" using A .
+ qed
+qed
+
+lemma less_eq_neg_nonpos:
+ "a \<le> - a \<longleftrightarrow> a \<le> 0"
+proof
+ assume A: "a \<le> - a" show "a \<le> 0"
+ proof (rule classical)
+ assume "\<not> a \<le> 0"
+ then have "0 < a" by auto
+ then have "0 < - a" using A by (rule less_le_trans)
+ then show ?thesis by auto
+ qed
+next
+ assume A: "a \<le> 0" show "a \<le> - a"
+ proof (rule order_trans)
+ show "0 \<le> - a" using A by (simp add: minus_le_iff)
+ next
+ show "a \<le> 0" using A .
+ qed
+qed
+
+lemma equal_neg_zero:
+ "a = - a \<longleftrightarrow> a = 0"
+proof
+ assume "a = 0" then show "a = - a" by simp
+next
+ assume A: "a = - a" show "a = 0"
+ proof (cases "0 \<le> a")
+ case True with A have "0 \<le> - a" by auto
+ with le_minus_iff have "a \<le> 0" by simp
+ with True show ?thesis by (auto intro: order_trans)
+ next
+ case False then have B: "a \<le> 0" by auto
+ with A have "- a \<le> 0" by auto
+ with B show ?thesis by (auto intro: order_trans)
+ qed
+qed
+
+lemma neg_equal_zero:
+ "- a = a \<longleftrightarrow> a = 0"
+ unfolding equal_neg_zero [symmetric] by auto
+
end
-- {* FIXME localize the following *}
@@ -609,77 +743,136 @@
by (insert add_le_less_mono [of 0 a b c], simp)
-subsection {* Support for reasoning about signs *}
+class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
+ assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
+ and abs_ge_self: "a \<le> \<bar>a\<bar>"
+ and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
+ and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
+ and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
+ and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
+ and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
+ and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
+begin
+
+lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
+ by simp
-lemma add_pos_pos: "0 <
- (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
- ==> 0 < y ==> 0 < x + y"
-apply (subgoal_tac "0 + 0 < x + y")
-apply simp
-apply (erule add_less_le_mono)
-apply (erule order_less_imp_le)
-done
+lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
+proof -
+ have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
+ thus ?thesis by simp
+qed
+
+lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
+proof
+ assume "\<bar>a\<bar> \<le> 0"
+ then have "\<bar>a\<bar> = 0" by (rule antisym) simp
+ thus "a = 0" by simp
+next
+ assume "a = 0"
+ thus "\<bar>a\<bar> \<le> 0" by simp
+qed
+
+lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
+ by (simp add: less_le)
+
+lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
+proof -
+ have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
+ show ?thesis by (simp add: a)
+qed
-lemma add_pos_nonneg: "0 <
- (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
- ==> 0 <= y ==> 0 < x + y"
-apply (subgoal_tac "0 + 0 < x + y")
-apply simp
-apply (erule add_less_le_mono, assumption)
-done
+lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
+proof -
+ have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
+ then show ?thesis by simp
+qed
+
+lemma abs_minus_commute:
+ "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
+proof -
+ have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
+ also have "... = \<bar>b - a\<bar>" by simp
+ finally show ?thesis .
+qed
+
+lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
+ by (rule abs_of_nonneg, rule less_imp_le)
-lemma add_nonneg_pos: "0 <=
- (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
- ==> 0 < y ==> 0 < x + y"
-apply (subgoal_tac "0 + 0 < x + y")
-apply simp
-apply (erule add_le_less_mono, assumption)
+lemma abs_of_nonpos [simp]:
+ assumes "a \<le> 0"
+ shows "\<bar>a\<bar> = - a"
+proof -
+ let ?b = "- a"
+ have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
+ unfolding abs_minus_cancel [of "?b"]
+ unfolding neg_le_0_iff_le [of "?b"]
+ unfolding minus_minus by (erule abs_of_nonneg)
+ then show ?thesis using assms by auto
+qed
+
+lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
+ by (rule abs_of_nonpos, rule less_imp_le)
+
+lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
+ by (insert abs_ge_self, blast intro: order_trans)
+
+lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
+ by (insert abs_le_D1 [of "uminus a"], simp)
+
+lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
+ by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
+
+lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
+ apply (simp add: compare_rls)
+ apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
+ apply (erule ssubst)
+ apply (rule abs_triangle_ineq)
+ apply (rule arg_cong) back
+ apply (simp add: compare_rls)
done
-lemma add_nonneg_nonneg: "0 <=
- (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
- ==> 0 <= y ==> 0 <= x + y"
-apply (subgoal_tac "0 + 0 <= x + y")
-apply simp
-apply (erule add_mono, assumption)
-done
-
-lemma add_neg_neg: "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
- < 0 ==> y < 0 ==> x + y < 0"
-apply (subgoal_tac "x + y < 0 + 0")
-apply simp
-apply (erule add_less_le_mono)
-apply (erule order_less_imp_le)
+lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
+ apply (subst abs_le_iff)
+ apply auto
+ apply (rule abs_triangle_ineq2)
+ apply (subst abs_minus_commute)
+ apply (rule abs_triangle_ineq2)
done
-lemma add_neg_nonpos:
- "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) < 0
- ==> y <= 0 ==> x + y < 0"
-apply (subgoal_tac "x + y < 0 + 0")
-apply simp
-apply (erule add_less_le_mono, assumption)
-done
+lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
+proof -
+ have "abs(a - b) = abs(a + - b)"
+ by (subst diff_minus, rule refl)
+ also have "... <= abs a + abs (- b)"
+ by (rule abs_triangle_ineq)
+ finally show ?thesis
+ by simp
+qed
-lemma add_nonpos_neg:
- "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0
- ==> y < 0 ==> x + y < 0"
-apply (subgoal_tac "x + y < 0 + 0")
-apply simp
-apply (erule add_le_less_mono, assumption)
-done
+lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
+proof -
+ have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
+ also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
+ finally show ?thesis .
+qed
-lemma add_nonpos_nonpos:
- "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0
- ==> y <= 0 ==> x + y <= 0"
-apply (subgoal_tac "x + y <= 0 + 0")
-apply simp
-apply (erule add_mono, assumption)
-done
+lemma abs_add_abs [simp]:
+ "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
+proof (rule antisym)
+ show "?L \<ge> ?R" by(rule abs_ge_self)
+next
+ have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
+ also have "\<dots> = ?R" by simp
+ finally show "?L \<le> ?R" .
+qed
+
+end
subsection {* Lattice Ordered (Abelian) Groups *}
-class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
+class lordered_ab_group_add_meet = pordered_ab_group_add + lower_semilattice
begin
lemma add_inf_distrib_left:
@@ -701,7 +894,7 @@
end
-class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
+class lordered_ab_group_add_join = pordered_ab_group_add + upper_semilattice
begin
lemma add_sup_distrib_left:
@@ -724,11 +917,11 @@
end
-class lordered_ab_group = pordered_ab_group_add + lattice
+class lordered_ab_group_add = pordered_ab_group_add + lattice
begin
-subclass lordered_ab_group_meet by unfold_locales
-subclass lordered_ab_group_join by unfold_locales
+subclass lordered_ab_group_add_meet by unfold_locales
+subclass lordered_ab_group_add_join by unfold_locales
lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
@@ -982,134 +1175,7 @@
lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
-class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
- assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
- and abs_ge_self: "a \<le> \<bar>a\<bar>"
- and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
- and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
- and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
- and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
- and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
- and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
-begin
-
-lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
- by simp
-
-lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
-proof -
- have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
- thus ?thesis by simp
-qed
-
-lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
-proof
- assume "\<bar>a\<bar> \<le> 0"
- then have "\<bar>a\<bar> = 0" by (rule antisym) simp
- thus "a = 0" by simp
-next
- assume "a = 0"
- thus "\<bar>a\<bar> \<le> 0" by simp
-qed
-
-lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
- by (simp add: less_le)
-
-lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
-proof -
- have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
- show ?thesis by (simp add: a)
-qed
-
-lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
-proof -
- have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
- then show ?thesis by simp
-qed
-
-lemma abs_minus_commute:
- "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
-proof -
- have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
- also have "... = \<bar>b - a\<bar>" by simp
- finally show ?thesis .
-qed
-
-lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
- by (rule abs_of_nonneg, rule less_imp_le)
-
-lemma abs_of_nonpos [simp]:
- assumes "a \<le> 0"
- shows "\<bar>a\<bar> = - a"
-proof -
- let ?b = "- a"
- have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
- unfolding abs_minus_cancel [of "?b"]
- unfolding neg_le_0_iff_le [of "?b"]
- unfolding minus_minus by (erule abs_of_nonneg)
- then show ?thesis using assms by auto
-qed
-
-lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
- by (rule abs_of_nonpos, rule less_imp_le)
-
-lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
- by (insert abs_ge_self, blast intro: order_trans)
-
-lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
- by (insert abs_le_D1 [of "uminus a"], simp)
-
-lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
- by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
-
-lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
- apply (simp add: compare_rls)
- apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
- apply (erule ssubst)
- apply (rule abs_triangle_ineq)
- apply (rule arg_cong) back
- apply (simp add: compare_rls)
-done
-
-lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
- apply (subst abs_le_iff)
- apply auto
- apply (rule abs_triangle_ineq2)
- apply (subst abs_minus_commute)
- apply (rule abs_triangle_ineq2)
-done
-
-lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
-proof -
- have "abs(a - b) = abs(a + - b)"
- by (subst diff_minus, rule refl)
- also have "... <= abs a + abs (- b)"
- by (rule abs_triangle_ineq)
- finally show ?thesis
- by simp
-qed
-
-lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
-proof -
- have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
- also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
- finally show ?thesis .
-qed
-
-lemma abs_add_abs [simp]:
- "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
-proof (rule antisym)
- show "?L \<ge> ?R" by(rule abs_ge_self)
-next
- have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
- also have "\<dots> = ?R" by simp
- finally show "?L \<le> ?R" .
-qed
-
-end
-
-
-class lordered_ab_group_abs = lordered_ab_group + abs +
+class lordered_ab_group_add_abs = lordered_ab_group_add + abs +
assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)"
begin
@@ -1190,7 +1256,7 @@
end
lemma sup_eq_if:
- fixes a :: "'a\<Colon>{lordered_ab_group, linorder}"
+ fixes a :: "'a\<Colon>{lordered_ab_group_add, linorder}"
shows "sup a (- a) = (if a < 0 then - a else a)"
proof -
note add_le_cancel_right [of a a "- a", symmetric, simplified]
@@ -1199,7 +1265,7 @@
qed
lemma abs_if_lattice:
- fixes a :: "'a\<Colon>{lordered_ab_group_abs, linorder}"
+ fixes a :: "'a\<Colon>{lordered_ab_group_add_abs, linorder}"
shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
by auto
@@ -1244,7 +1310,7 @@
done
lemma estimate_by_abs:
- "a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b"
+ "a + b <= (c::'a::lordered_ab_group_add_abs) \<Longrightarrow> a <= c + abs b"
proof -
assume "a+b <= c"
hence 2: "a <= c+(-b)" by (simp add: group_simps)
--- a/src/HOL/Real/RealDef.thy Mon Nov 05 23:17:03 2007 +0100
+++ b/src/HOL/Real/RealDef.thy Tue Nov 06 08:47:25 2007 +0100
@@ -418,6 +418,8 @@
by (simp only: real_sgn_def)
qed
+instance real :: lordered_ab_group_add ..
+
text{*The function @{term real_of_preal} requires many proofs, but it seems
to be essential for proving completeness of the reals from that of the
positive reals.*}