# HG changeset patch # User haftmann # Date 1194335245 -3600 # Node ID 0699e20feabd0e6c933fed30bb2ce285e0e167ac # Parent 19b1729f1bd40e227b8a2c9dc55700cbb2152122 renamed lordered_*_* to lordered_*_add_*; further localization diff -r 19b1729f1bd4 -r 0699e20feabd src/HOL/Finite_Set.thy --- 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) \ 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 \ 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 (\a\A. abs(f a)) = (\a\A. abs(f a))" proof (cases "finite A") case True diff -r 19b1729f1bd4 -r 0699e20feabd src/HOL/Matrix/Matrix.thy --- 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 \ mult_matrix (op *) (op +) A B" .. -instance matrix :: (lordered_ab_group) abs +instance matrix :: (lordered_ab_group_add) abs abs_matrix_def: "abs A \ 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) \ f 0 = (0::'a) \ 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) \ f 0 = (0::'a) \ 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)" diff -r 19b1729f1bd4 -r 0699e20feabd src/HOL/Matrix/SparseMatrix.thy --- 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 \ 'a spvec" - add_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \ 'a spmat" + add_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \ 'a spvec" + add_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \ '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 \ bool" - le_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \ bool" + le_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \ bool" + le_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \ 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 \ disj_matrices C D \ disj_matrices A D \ disj_matrices B C \ - (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 \ - (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 \ - (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 \ disj_matrices B C \ - (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 \ disj_matrices B C \ - (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 \ sorted_spvec((j,y)#v) \ 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 \ disj_matrices A C \ disj_matrices (A::('a::lordered_ab_group) matrix) (B+C)" +lemma disj_matrices_x_add: "disj_matrices A B \ disj_matrices A C \ 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 \ disj_matrices A C \ disj_matrices (B+C) (A::('a::lordered_ab_group) matrix)" +lemma disj_matrices_add_x: "disj_matrices A B \ disj_matrices A C \ 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 \ u | i \ 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 \ 'a spvec" - nprt_spvec :: "('a::{lordered_ab_group}) spvec \ 'a spvec" - pprt_spmat :: "('a::{lordered_ab_group}) spmat \ 'a spmat" - nprt_spmat :: "('a::{lordered_ab_group}) spmat \ 'a spmat" + pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \ 'a spvec" + nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \ 'a spvec" + pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \ 'a spmat" + nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \ 'a spmat" primrec "pprt_spvec [] = []" diff -r 19b1729f1bd4 -r 0699e20feabd src/HOL/OrderedGroup.thy --- 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 \ 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 \ 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 \ a" and "0 \ b" + shows "0 \ a + b" +proof - + have "0 + 0 \ a + b" + using assms by (rule add_mono) + then show ?thesis by simp +qed + +lemma add_neg_nonpos: + assumes "a < 0" and "b \ 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 \ 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 \ 0" and "b \ 0" + shows "a + b \ 0" +proof - + have "a + b \ 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 \ 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 \ a \ 0 \ a" +proof + assume A: "- a \ a" show "0 \ a" + proof (rule classical) + assume "\ 0 \ 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 \ a" show "- a \ a" + proof (rule order_trans) + show "- a \ 0" using A by (simp add: minus_le_iff) + next + show "0 \ a" using A . + qed +qed + +lemma less_eq_neg_nonpos: + "a \ - a \ a \ 0" +proof + assume A: "a \ - a" show "a \ 0" + proof (rule classical) + assume "\ a \ 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 \ 0" show "a \ - a" + proof (rule order_trans) + show "0 \ - a" using A by (simp add: minus_le_iff) + next + show "a \ 0" using A . + qed +qed + +lemma equal_neg_zero: + "a = - a \ a = 0" +proof + assume "a = 0" then show "a = - a" by simp +next + assume A: "a = - a" show "a = 0" + proof (cases "0 \ a") + case True with A have "0 \ - a" by auto + with le_minus_iff have "a \ 0" by simp + with True show ?thesis by (auto intro: order_trans) + next + case False then have B: "a \ 0" by auto + with A have "- a \ 0" by auto + with B show ?thesis by (auto intro: order_trans) + qed +qed + +lemma neg_equal_zero: + "- a = a \ 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]: "\a\ \ 0" + and abs_ge_self: "a \ \a\" + and abs_of_nonneg [simp]: "0 \ a \ \a\ = a" + and abs_leI: "a \ b \ - a \ b \ \a\ \ b" + and abs_eq_0 [simp]: "\a\ = 0 \ a = 0" + and abs_minus_cancel [simp]: "\-a\ = \a\" + and abs_idempotent [simp]: "\\a\\ = \a\" + and abs_triangle_ineq: "\a + b\ \ \a\ + \b\" +begin + +lemma abs_zero [simp]: "\0\ = 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 = \a\ \ a = 0" +proof - + have "0 = \a\ \ \a\ = 0" by (simp only: eq_ac) + thus ?thesis by simp +qed + +lemma abs_le_zero_iff [simp]: "\a\ \ 0 \ a = 0" +proof + assume "\a\ \ 0" + then have "\a\ = 0" by (rule antisym) simp + thus "a = 0" by simp +next + assume "a = 0" + thus "\a\ \ 0" by simp +qed + +lemma zero_less_abs_iff [simp]: "0 < \a\ \ a \ 0" + by (simp add: less_le) + +lemma abs_not_less_zero [simp]: "\ \a\ < 0" +proof - + have a: "\x y. x \ y \ \ 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 \ \a\" +proof - + have "- a \ \-a\" by (rule abs_ge_self) + then show ?thesis by simp +qed + +lemma abs_minus_commute: + "\a - b\ = \b - a\" +proof - + have "\a - b\ = \- (a - b)\" by (simp only: abs_minus_cancel) + also have "... = \b - a\" by simp + finally show ?thesis . +qed + +lemma abs_of_pos: "0 < a \ \a\ = 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 \ 0" + shows "\a\ = - a" +proof - + let ?b = "- a" + have "- ?b \ 0 \ \- ?b\ = - (- ?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 \ \a\ = - a" + by (rule abs_of_nonpos, rule less_imp_le) + +lemma abs_le_D1: "\a\ \ b \ a \ b" + by (insert abs_ge_self, blast intro: order_trans) + +lemma abs_le_D2: "\a\ \ b \ - a \ b" + by (insert abs_le_D1 [of "uminus a"], simp) + +lemma abs_le_iff: "\a\ \ b \ a \ b \ - a \ b" + by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) + +lemma abs_triangle_ineq2: "\a\ - \b\ \ \a - b\" + 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: "\\a\ - \b\\ \ \a - b\" + 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: "\a - b\ \ \a\ + \b\" +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: "\a + b - (c + d)\ \ \a - c\ + \b - d\" +proof - + have "\a + b - (c+d)\ = \(a-c) + (b-d)\" by (simp add: diff_minus add_ac) + also have "... \ \a-c\ + \b-d\" 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]: + "\\a\ + \b\\ = \a\ + \b\" (is "?L = ?R") +proof (rule antisym) + show "?L \ ?R" by(rule abs_ge_self) +next + have "?L \ \\a\\ + \\b\\" by(rule abs_triangle_ineq) + also have "\ = ?R" by simp + finally show "?L \ ?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]: "\a\ \ 0" - and abs_ge_self: "a \ \a\" - and abs_of_nonneg [simp]: "0 \ a \ \a\ = a" - and abs_leI: "a \ b \ - a \ b \ \a\ \ b" - and abs_eq_0 [simp]: "\a\ = 0 \ a = 0" - and abs_minus_cancel [simp]: "\-a\ = \a\" - and abs_idempotent [simp]: "\\a\\ = \a\" - and abs_triangle_ineq: "\a + b\ \ \a\ + \b\" -begin - -lemma abs_zero [simp]: "\0\ = 0" - by simp - -lemma abs_0_eq [simp, noatp]: "0 = \a\ \ a = 0" -proof - - have "0 = \a\ \ \a\ = 0" by (simp only: eq_ac) - thus ?thesis by simp -qed - -lemma abs_le_zero_iff [simp]: "\a\ \ 0 \ a = 0" -proof - assume "\a\ \ 0" - then have "\a\ = 0" by (rule antisym) simp - thus "a = 0" by simp -next - assume "a = 0" - thus "\a\ \ 0" by simp -qed - -lemma zero_less_abs_iff [simp]: "0 < \a\ \ a \ 0" - by (simp add: less_le) - -lemma abs_not_less_zero [simp]: "\ \a\ < 0" -proof - - have a: "\x y. x \ y \ \ y < x" by auto - show ?thesis by (simp add: a) -qed - -lemma abs_ge_minus_self: "- a \ \a\" -proof - - have "- a \ \-a\" by (rule abs_ge_self) - then show ?thesis by simp -qed - -lemma abs_minus_commute: - "\a - b\ = \b - a\" -proof - - have "\a - b\ = \- (a - b)\" by (simp only: abs_minus_cancel) - also have "... = \b - a\" by simp - finally show ?thesis . -qed - -lemma abs_of_pos: "0 < a \ \a\ = a" - by (rule abs_of_nonneg, rule less_imp_le) - -lemma abs_of_nonpos [simp]: - assumes "a \ 0" - shows "\a\ = - a" -proof - - let ?b = "- a" - have "- ?b \ 0 \ \- ?b\ = - (- ?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 \ \a\ = - a" - by (rule abs_of_nonpos, rule less_imp_le) - -lemma abs_le_D1: "\a\ \ b \ a \ b" - by (insert abs_ge_self, blast intro: order_trans) - -lemma abs_le_D2: "\a\ \ b \ - a \ b" - by (insert abs_le_D1 [of "uminus a"], simp) - -lemma abs_le_iff: "\a\ \ b \ a \ b \ - a \ b" - by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) - -lemma abs_triangle_ineq2: "\a\ - \b\ \ \a - b\" - 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: "\\a\ - \b\\ \ \a - b\