renamed lordered_*_* to lordered_*_add_*; further localization
authorhaftmann
Tue Nov 06 08:47:25 2007 +0100 (2007-11-06)
changeset 253030699e20feabd
parent 25302 19b1729f1bd4
child 25304 7491c00f0915
renamed lordered_*_* to lordered_*_add_*; further localization
src/HOL/Finite_Set.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/OrderedGroup.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Nov 05 23:17:03 2007 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 06 08:47:25 2007 +0100
     1.3 @@ -1199,7 +1199,7 @@
     1.4  qed
     1.5  
     1.6  lemma setsum_abs[iff]: 
     1.7 -  fixes f :: "'a => ('b::lordered_ab_group_abs)"
     1.8 +  fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
     1.9    shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
    1.10  proof (cases "finite A")
    1.11    case True
    1.12 @@ -1215,7 +1215,7 @@
    1.13  qed
    1.14  
    1.15  lemma setsum_abs_ge_zero[iff]: 
    1.16 -  fixes f :: "'a => ('b::lordered_ab_group_abs)"
    1.17 +  fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
    1.18    shows "0 \<le> setsum (%i. abs(f i)) A"
    1.19  proof (cases "finite A")
    1.20    case True
    1.21 @@ -1230,7 +1230,7 @@
    1.22  qed
    1.23  
    1.24  lemma abs_setsum_abs[simp]: 
    1.25 -  fixes f :: "'a => ('b::lordered_ab_group_abs)"
    1.26 +  fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
    1.27    shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
    1.28  proof (cases "finite A")
    1.29    case True
     2.1 --- a/src/HOL/Matrix/Matrix.thy	Mon Nov 05 23:17:03 2007 +0100
     2.2 +++ b/src/HOL/Matrix/Matrix.thy	Tue Nov 06 08:47:25 2007 +0100
     2.3 @@ -22,12 +22,12 @@
     2.4  instance matrix :: ("{plus, times, zero}") times
     2.5    times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
     2.6  
     2.7 -instance matrix :: (lordered_ab_group) abs
     2.8 +instance matrix :: (lordered_ab_group_add) abs
     2.9    abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
    2.10  
    2.11 -instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    2.12 +instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
    2.13  proof 
    2.14 -  fix A B C :: "('a::lordered_ab_group) matrix"
    2.15 +  fix A B C :: "('a::lordered_ab_group_add) matrix"
    2.16    show "A + B + C = A + (B + C)"    
    2.17      apply (simp add: plus_matrix_def)
    2.18      apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
    2.19 @@ -89,7 +89,8 @@
    2.20      done
    2.21  qed 
    2.22  
    2.23 -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)"
    2.24 +lemma Rep_matrix_add[simp]:
    2.25 +  "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
    2.26  by (simp add: plus_matrix_def)
    2.27  
    2.28  lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = 
    2.29 @@ -98,13 +99,13 @@
    2.30  apply (simp add: Rep_mult_matrix)
    2.31  done
    2.32  
    2.33 -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)"
    2.34 +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)"
    2.35  apply (subst Rep_matrix_inject[symmetric])
    2.36  apply (rule ext)+
    2.37  apply (simp)
    2.38  done
    2.39  
    2.40 -lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
    2.41 +lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
    2.42  apply (subst Rep_matrix_inject[symmetric])
    2.43  apply (rule ext)+
    2.44  apply (simp)
    2.45 @@ -162,10 +163,10 @@
    2.46  apply (simp_all add: mult_commute)
    2.47  done
    2.48  
    2.49 -lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B"
    2.50 +lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)+B) = transpose_matrix A + transpose_matrix B"
    2.51  by (simp add: plus_matrix_def transpose_combine_matrix)
    2.52  
    2.53 -lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B"
    2.54 +lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
    2.55  by (simp add: diff_matrix_def transpose_combine_matrix)
    2.56  
    2.57  lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
    2.58 @@ -252,7 +253,7 @@
    2.59  apply (simp add: max2)
    2.60  done
    2.61  
    2.62 -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)" 
    2.63 +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)" 
    2.64  apply (subst Rep_matrix_inject[symmetric])
    2.65  apply (rule ext)+
    2.66  apply (simp)
    2.67 @@ -280,7 +281,7 @@
    2.68  apply (auto)
    2.69  done
    2.70  
    2.71 -lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
    2.72 +lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group_add)) x y = - (Rep_matrix A x y)"
    2.73  by (simp add: minus_matrix_def)
    2.74  
    2.75  lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
     3.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Mon Nov 05 23:17:03 2007 +0100
     3.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Tue Nov 06 08:47:25 2007 +0100
     3.3 @@ -387,8 +387,8 @@
     3.4    done
     3.5  
     3.6  consts
     3.7 -  add_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> 'a spvec"
     3.8 -  add_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> 'a spmat"
     3.9 +  add_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> 'a spvec"
    3.10 +  add_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> 'a spmat"
    3.11  
    3.12  recdef add_spvec "measure (% (a, b). length a + (length b))"
    3.13    "add_spvec (arr, []) = arr"
    3.14 @@ -569,8 +569,8 @@
    3.15    done
    3.16  
    3.17  consts
    3.18 -  le_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> bool" 
    3.19 -  le_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> bool" 
    3.20 +  le_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> bool" 
    3.21 +  le_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> bool" 
    3.22  
    3.23  recdef le_spvec "measure (% (a,b). (length a) + (length b))" 
    3.24    "le_spvec ([], []) = True"
    3.25 @@ -610,7 +610,7 @@
    3.26  
    3.27  
    3.28  lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
    3.29 -  (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group) matrix))"
    3.30 +  (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group_add) matrix))"
    3.31    apply (auto)
    3.32    apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
    3.33    apply (intro strip)
    3.34 @@ -640,19 +640,19 @@
    3.35  by (auto simp add: disj_matrices_def)
    3.36  
    3.37  lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
    3.38 -  (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group) matrix) <= 0)"
    3.39 +  (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group_add) matrix) <= 0)"
    3.40  by (rule disj_matrices_add[of A B 0 0, simplified])
    3.41   
    3.42  lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
    3.43 -  (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group) matrix))"
    3.44 +  (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group_add) matrix))"
    3.45  by (rule disj_matrices_add[of 0 0 A B, simplified])
    3.46  
    3.47  lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
    3.48 -  (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group) matrix))"
    3.49 +  (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group_add) matrix))"
    3.50  by (auto simp add: disj_matrices_add[of 0 A B C, simplified])
    3.51  
    3.52  lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
    3.53 -  (B + A <= C) = (A <= C &  (B::('a::lordered_ab_group) matrix) <= 0)"
    3.54 +  (B + A <= C) = (A <= C &  (B::('a::lordered_ab_group_add) matrix) <= 0)"
    3.55  by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
    3.56  
    3.57  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)"
    3.58 @@ -668,7 +668,7 @@
    3.59    apply (simp_all)
    3.60    done 
    3.61  
    3.62 -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)"
    3.63 +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)"
    3.64    apply (simp add: disj_matrices_def)
    3.65    apply (auto)
    3.66    apply (drule_tac j=j and i=i in spec2)+
    3.67 @@ -677,7 +677,7 @@
    3.68    apply (simp_all)
    3.69    done
    3.70  
    3.71 -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)" 
    3.72 +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)" 
    3.73    by (simp add: disj_matrices_x_add disj_matrices_commute)
    3.74  
    3.75  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)" 
    3.76 @@ -897,10 +897,10 @@
    3.77  lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
    3.78  
    3.79  consts
    3.80 -  pprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
    3.81 -  nprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
    3.82 -  pprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
    3.83 -  nprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
    3.84 +  pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
    3.85 +  nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
    3.86 +  pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
    3.87 +  nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
    3.88  
    3.89  primrec
    3.90    "pprt_spvec [] = []"
     4.1 --- a/src/HOL/OrderedGroup.thy	Mon Nov 05 23:17:03 2007 +0100
     4.2 +++ b/src/HOL/OrderedGroup.thy	Tue Nov 06 08:47:25 2007 +0100
     4.3 @@ -394,6 +394,78 @@
     4.4  
     4.5  end
     4.6  
     4.7 +subsection {* Support for reasoning about signs *}
     4.8 +
     4.9 +class pordered_comm_monoid_add =
    4.10 +  pordered_cancel_ab_semigroup_add + comm_monoid_add
    4.11 +begin
    4.12 +
    4.13 +lemma add_pos_nonneg:
    4.14 +  assumes "0 < a" and "0 \<le> b"
    4.15 +    shows "0 < a + b"
    4.16 +proof -
    4.17 +  have "0 + 0 < a + b" 
    4.18 +    using assms by (rule add_less_le_mono)
    4.19 +  then show ?thesis by simp
    4.20 +qed
    4.21 +
    4.22 +lemma add_pos_pos:
    4.23 +  assumes "0 < a" and "0 < b"
    4.24 +    shows "0 < a + b"
    4.25 +  by (rule add_pos_nonneg) (insert assms, auto)
    4.26 +
    4.27 +lemma add_nonneg_pos:
    4.28 +  assumes "0 \<le> a" and "0 < b"
    4.29 +    shows "0 < a + b"
    4.30 +proof -
    4.31 +  have "0 + 0 < a + b" 
    4.32 +    using assms by (rule add_le_less_mono)
    4.33 +  then show ?thesis by simp
    4.34 +qed
    4.35 +
    4.36 +lemma add_nonneg_nonneg:
    4.37 +  assumes "0 \<le> a" and "0 \<le> b"
    4.38 +    shows "0 \<le> a + b"
    4.39 +proof -
    4.40 +  have "0 + 0 \<le> a + b" 
    4.41 +    using assms by (rule add_mono)
    4.42 +  then show ?thesis by simp
    4.43 +qed
    4.44 +
    4.45 +lemma add_neg_nonpos: 
    4.46 +  assumes "a < 0" and "b \<le> 0"
    4.47 +  shows "a + b < 0"
    4.48 +proof -
    4.49 +  have "a + b < 0 + 0"
    4.50 +    using assms by (rule add_less_le_mono)
    4.51 +  then show ?thesis by simp
    4.52 +qed
    4.53 +
    4.54 +lemma add_neg_neg: 
    4.55 +  assumes "a < 0" and "b < 0"
    4.56 +  shows "a + b < 0"
    4.57 +  by (rule add_neg_nonpos) (insert assms, auto)
    4.58 +
    4.59 +lemma add_nonpos_neg:
    4.60 +  assumes "a \<le> 0" and "b < 0"
    4.61 +  shows "a + b < 0"
    4.62 +proof -
    4.63 +  have "a + b < 0 + 0"
    4.64 +    using assms by (rule add_le_less_mono)
    4.65 +  then show ?thesis by simp
    4.66 +qed
    4.67 +
    4.68 +lemma add_nonpos_nonpos:
    4.69 +  assumes "a \<le> 0" and "b \<le> 0"
    4.70 +  shows "a + b \<le> 0"
    4.71 +proof -
    4.72 +  have "a + b \<le> 0 + 0"
    4.73 +    using assms by (rule add_mono)
    4.74 +  then show ?thesis by simp
    4.75 +qed
    4.76 +
    4.77 +end
    4.78 +
    4.79  class pordered_ab_group_add =
    4.80    ab_group_add + pordered_ab_semigroup_add
    4.81  begin
    4.82 @@ -410,6 +482,9 @@
    4.83    thus "a \<le> b" by simp
    4.84  qed
    4.85  
    4.86 +subclass pordered_comm_monoid_add
    4.87 +  by unfold_locales
    4.88 +
    4.89  lemma max_diff_distrib_left:
    4.90    shows "max x y - z = max (x - z) (y - z)"
    4.91    by (simp add: diff_minus, rule max_add_distrib_left) 
    4.92 @@ -584,6 +659,65 @@
    4.93  subclass ordered_cancel_ab_semigroup_add 
    4.94    by unfold_locales
    4.95  
    4.96 +lemma neg_less_eq_nonneg:
    4.97 +  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
    4.98 +proof
    4.99 +  assume A: "- a \<le> a" show "0 \<le> a"
   4.100 +  proof (rule classical)
   4.101 +    assume "\<not> 0 \<le> a"
   4.102 +    then have "a < 0" by auto
   4.103 +    with A have "- a < 0" by (rule le_less_trans)
   4.104 +    then show ?thesis by auto
   4.105 +  qed
   4.106 +next
   4.107 +  assume A: "0 \<le> a" show "- a \<le> a"
   4.108 +  proof (rule order_trans)
   4.109 +    show "- a \<le> 0" using A by (simp add: minus_le_iff)
   4.110 +  next
   4.111 +    show "0 \<le> a" using A .
   4.112 +  qed
   4.113 +qed
   4.114 +  
   4.115 +lemma less_eq_neg_nonpos:
   4.116 +  "a \<le> - a \<longleftrightarrow> a \<le> 0"
   4.117 +proof
   4.118 +  assume A: "a \<le> - a" show "a \<le> 0"
   4.119 +  proof (rule classical)
   4.120 +    assume "\<not> a \<le> 0"
   4.121 +    then have "0 < a" by auto
   4.122 +    then have "0 < - a" using A by (rule less_le_trans)
   4.123 +    then show ?thesis by auto
   4.124 +  qed
   4.125 +next
   4.126 +  assume A: "a \<le> 0" show "a \<le> - a"
   4.127 +  proof (rule order_trans)
   4.128 +    show "0 \<le> - a" using A by (simp add: minus_le_iff)
   4.129 +  next
   4.130 +    show "a \<le> 0" using A .
   4.131 +  qed
   4.132 +qed
   4.133 +
   4.134 +lemma equal_neg_zero:
   4.135 +  "a = - a \<longleftrightarrow> a = 0"
   4.136 +proof
   4.137 +  assume "a = 0" then show "a = - a" by simp
   4.138 +next
   4.139 +  assume A: "a = - a" show "a = 0"
   4.140 +  proof (cases "0 \<le> a")
   4.141 +    case True with A have "0 \<le> - a" by auto
   4.142 +    with le_minus_iff have "a \<le> 0" by simp
   4.143 +    with True show ?thesis by (auto intro: order_trans)
   4.144 +  next
   4.145 +    case False then have B: "a \<le> 0" by auto
   4.146 +    with A have "- a \<le> 0" by auto
   4.147 +    with B show ?thesis by (auto intro: order_trans)
   4.148 +  qed
   4.149 +qed
   4.150 +
   4.151 +lemma neg_equal_zero:
   4.152 +  "- a = a \<longleftrightarrow> a = 0"
   4.153 +  unfolding equal_neg_zero [symmetric] by auto
   4.154 +
   4.155  end
   4.156  
   4.157  -- {* FIXME localize the following *}
   4.158 @@ -609,77 +743,136 @@
   4.159  by (insert add_le_less_mono [of 0 a b c], simp)
   4.160  
   4.161  
   4.162 -subsection {* Support for reasoning about signs *}
   4.163 +class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
   4.164 +  assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
   4.165 +    and abs_ge_self: "a \<le> \<bar>a\<bar>"
   4.166 +    and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   4.167 +    and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   4.168 +    and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   4.169 +    and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   4.170 +    and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   4.171 +    and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   4.172 +begin
   4.173 +
   4.174 +lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   4.175 +  by simp
   4.176  
   4.177 -lemma add_pos_pos: "0 < 
   4.178 -    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   4.179 -      ==> 0 < y ==> 0 < x + y"
   4.180 -apply (subgoal_tac "0 + 0 < x + y")
   4.181 -apply simp
   4.182 -apply (erule add_less_le_mono)
   4.183 -apply (erule order_less_imp_le)
   4.184 -done
   4.185 +lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
   4.186 +proof -
   4.187 +  have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   4.188 +  thus ?thesis by simp
   4.189 +qed
   4.190 +
   4.191 +lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
   4.192 +proof
   4.193 +  assume "\<bar>a\<bar> \<le> 0"
   4.194 +  then have "\<bar>a\<bar> = 0" by (rule antisym) simp
   4.195 +  thus "a = 0" by simp
   4.196 +next
   4.197 +  assume "a = 0"
   4.198 +  thus "\<bar>a\<bar> \<le> 0" by simp
   4.199 +qed
   4.200 +
   4.201 +lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
   4.202 +  by (simp add: less_le)
   4.203 +
   4.204 +lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
   4.205 +proof -
   4.206 +  have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
   4.207 +  show ?thesis by (simp add: a)
   4.208 +qed
   4.209  
   4.210 -lemma add_pos_nonneg: "0 < 
   4.211 -    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   4.212 -      ==> 0 <= y ==> 0 < x + y"
   4.213 -apply (subgoal_tac "0 + 0 < x + y")
   4.214 -apply simp
   4.215 -apply (erule add_less_le_mono, assumption)
   4.216 -done
   4.217 +lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
   4.218 +proof -
   4.219 +  have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
   4.220 +  then show ?thesis by simp
   4.221 +qed
   4.222 +
   4.223 +lemma abs_minus_commute: 
   4.224 +  "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
   4.225 +proof -
   4.226 +  have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
   4.227 +  also have "... = \<bar>b - a\<bar>" by simp
   4.228 +  finally show ?thesis .
   4.229 +qed
   4.230 +
   4.231 +lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
   4.232 +  by (rule abs_of_nonneg, rule less_imp_le)
   4.233  
   4.234 -lemma add_nonneg_pos: "0 <= 
   4.235 -    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   4.236 -      ==> 0 < y ==> 0 < x + y"
   4.237 -apply (subgoal_tac "0 + 0 < x + y")
   4.238 -apply simp
   4.239 -apply (erule add_le_less_mono, assumption)
   4.240 +lemma abs_of_nonpos [simp]:
   4.241 +  assumes "a \<le> 0"
   4.242 +  shows "\<bar>a\<bar> = - a"
   4.243 +proof -
   4.244 +  let ?b = "- a"
   4.245 +  have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
   4.246 +  unfolding abs_minus_cancel [of "?b"]
   4.247 +  unfolding neg_le_0_iff_le [of "?b"]
   4.248 +  unfolding minus_minus by (erule abs_of_nonneg)
   4.249 +  then show ?thesis using assms by auto
   4.250 +qed
   4.251 +  
   4.252 +lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   4.253 +  by (rule abs_of_nonpos, rule less_imp_le)
   4.254 +
   4.255 +lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   4.256 +  by (insert abs_ge_self, blast intro: order_trans)
   4.257 +
   4.258 +lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
   4.259 +  by (insert abs_le_D1 [of "uminus a"], simp)
   4.260 +
   4.261 +lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   4.262 +  by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   4.263 +
   4.264 +lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
   4.265 +  apply (simp add: compare_rls)
   4.266 +  apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
   4.267 +  apply (erule ssubst)
   4.268 +  apply (rule abs_triangle_ineq)
   4.269 +  apply (rule arg_cong) back
   4.270 +  apply (simp add: compare_rls)
   4.271  done
   4.272  
   4.273 -lemma add_nonneg_nonneg: "0 <= 
   4.274 -    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   4.275 -      ==> 0 <= y ==> 0 <= x + y"
   4.276 -apply (subgoal_tac "0 + 0 <= x + y")
   4.277 -apply simp
   4.278 -apply (erule add_mono, assumption)
   4.279 -done
   4.280 -
   4.281 -lemma add_neg_neg: "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
   4.282 -    < 0 ==> y < 0 ==> x + y < 0"
   4.283 -apply (subgoal_tac "x + y < 0 + 0")
   4.284 -apply simp
   4.285 -apply (erule add_less_le_mono)
   4.286 -apply (erule order_less_imp_le)
   4.287 +lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
   4.288 +  apply (subst abs_le_iff)
   4.289 +  apply auto
   4.290 +  apply (rule abs_triangle_ineq2)
   4.291 +  apply (subst abs_minus_commute)
   4.292 +  apply (rule abs_triangle_ineq2)
   4.293  done
   4.294  
   4.295 -lemma add_neg_nonpos: 
   4.296 -    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) < 0 
   4.297 -      ==> y <= 0 ==> x + y < 0"
   4.298 -apply (subgoal_tac "x + y < 0 + 0")
   4.299 -apply simp
   4.300 -apply (erule add_less_le_mono, assumption)
   4.301 -done
   4.302 +lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   4.303 +proof -
   4.304 +  have "abs(a - b) = abs(a + - b)"
   4.305 +    by (subst diff_minus, rule refl)
   4.306 +  also have "... <= abs a + abs (- b)"
   4.307 +    by (rule abs_triangle_ineq)
   4.308 +  finally show ?thesis
   4.309 +    by simp
   4.310 +qed
   4.311  
   4.312 -lemma add_nonpos_neg: 
   4.313 -    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 
   4.314 -      ==> y < 0 ==> x + y < 0"
   4.315 -apply (subgoal_tac "x + y < 0 + 0")
   4.316 -apply simp
   4.317 -apply (erule add_le_less_mono, assumption)
   4.318 -done
   4.319 +lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
   4.320 +proof -
   4.321 +  have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
   4.322 +  also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
   4.323 +  finally show ?thesis .
   4.324 +qed
   4.325  
   4.326 -lemma add_nonpos_nonpos: 
   4.327 -    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 
   4.328 -      ==> y <= 0 ==> x + y <= 0"
   4.329 -apply (subgoal_tac "x + y <= 0 + 0")
   4.330 -apply simp
   4.331 -apply (erule add_mono, assumption)
   4.332 -done
   4.333 +lemma abs_add_abs [simp]:
   4.334 +  "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
   4.335 +proof (rule antisym)
   4.336 +  show "?L \<ge> ?R" by(rule abs_ge_self)
   4.337 +next
   4.338 +  have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
   4.339 +  also have "\<dots> = ?R" by simp
   4.340 +  finally show "?L \<le> ?R" .
   4.341 +qed
   4.342 +
   4.343 +end
   4.344  
   4.345  
   4.346  subsection {* Lattice Ordered (Abelian) Groups *}
   4.347  
   4.348 -class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
   4.349 +class lordered_ab_group_add_meet = pordered_ab_group_add + lower_semilattice
   4.350  begin
   4.351  
   4.352  lemma add_inf_distrib_left:
   4.353 @@ -701,7 +894,7 @@
   4.354  
   4.355  end
   4.356  
   4.357 -class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
   4.358 +class lordered_ab_group_add_join = pordered_ab_group_add + upper_semilattice
   4.359  begin
   4.360  
   4.361  lemma add_sup_distrib_left:
   4.362 @@ -724,11 +917,11 @@
   4.363  
   4.364  end
   4.365  
   4.366 -class lordered_ab_group = pordered_ab_group_add + lattice
   4.367 +class lordered_ab_group_add = pordered_ab_group_add + lattice
   4.368  begin
   4.369  
   4.370 -subclass lordered_ab_group_meet by unfold_locales
   4.371 -subclass lordered_ab_group_join by unfold_locales
   4.372 +subclass lordered_ab_group_add_meet by unfold_locales
   4.373 +subclass lordered_ab_group_add_join by unfold_locales
   4.374  
   4.375  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   4.376  
   4.377 @@ -982,134 +1175,7 @@
   4.378  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   4.379  
   4.380  
   4.381 -class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
   4.382 -  assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
   4.383 -    and abs_ge_self: "a \<le> \<bar>a\<bar>"
   4.384 -    and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   4.385 -    and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   4.386 -    and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   4.387 -    and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   4.388 -    and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   4.389 -    and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   4.390 -begin
   4.391 -
   4.392 -lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   4.393 -  by simp
   4.394 -
   4.395 -lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
   4.396 -proof -
   4.397 -  have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   4.398 -  thus ?thesis by simp
   4.399 -qed
   4.400 -
   4.401 -lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
   4.402 -proof
   4.403 -  assume "\<bar>a\<bar> \<le> 0"
   4.404 -  then have "\<bar>a\<bar> = 0" by (rule antisym) simp
   4.405 -  thus "a = 0" by simp
   4.406 -next
   4.407 -  assume "a = 0"
   4.408 -  thus "\<bar>a\<bar> \<le> 0" by simp
   4.409 -qed
   4.410 -
   4.411 -lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
   4.412 -  by (simp add: less_le)
   4.413 -
   4.414 -lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
   4.415 -proof -
   4.416 -  have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
   4.417 -  show ?thesis by (simp add: a)
   4.418 -qed
   4.419 -
   4.420 -lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
   4.421 -proof -
   4.422 -  have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
   4.423 -  then show ?thesis by simp
   4.424 -qed
   4.425 -
   4.426 -lemma abs_minus_commute: 
   4.427 -  "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
   4.428 -proof -
   4.429 -  have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
   4.430 -  also have "... = \<bar>b - a\<bar>" by simp
   4.431 -  finally show ?thesis .
   4.432 -qed
   4.433 -
   4.434 -lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
   4.435 -  by (rule abs_of_nonneg, rule less_imp_le)
   4.436 -
   4.437 -lemma abs_of_nonpos [simp]:
   4.438 -  assumes "a \<le> 0"
   4.439 -  shows "\<bar>a\<bar> = - a"
   4.440 -proof -
   4.441 -  let ?b = "- a"
   4.442 -  have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
   4.443 -  unfolding abs_minus_cancel [of "?b"]
   4.444 -  unfolding neg_le_0_iff_le [of "?b"]
   4.445 -  unfolding minus_minus by (erule abs_of_nonneg)
   4.446 -  then show ?thesis using assms by auto
   4.447 -qed
   4.448 -  
   4.449 -lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   4.450 -  by (rule abs_of_nonpos, rule less_imp_le)
   4.451 -
   4.452 -lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   4.453 -  by (insert abs_ge_self, blast intro: order_trans)
   4.454 -
   4.455 -lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
   4.456 -  by (insert abs_le_D1 [of "uminus a"], simp)
   4.457 -
   4.458 -lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   4.459 -  by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   4.460 -
   4.461 -lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
   4.462 -  apply (simp add: compare_rls)
   4.463 -  apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
   4.464 -  apply (erule ssubst)
   4.465 -  apply (rule abs_triangle_ineq)
   4.466 -  apply (rule arg_cong) back
   4.467 -  apply (simp add: compare_rls)
   4.468 -done
   4.469 -
   4.470 -lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
   4.471 -  apply (subst abs_le_iff)
   4.472 -  apply auto
   4.473 -  apply (rule abs_triangle_ineq2)
   4.474 -  apply (subst abs_minus_commute)
   4.475 -  apply (rule abs_triangle_ineq2)
   4.476 -done
   4.477 -
   4.478 -lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   4.479 -proof -
   4.480 -  have "abs(a - b) = abs(a + - b)"
   4.481 -    by (subst diff_minus, rule refl)
   4.482 -  also have "... <= abs a + abs (- b)"
   4.483 -    by (rule abs_triangle_ineq)
   4.484 -  finally show ?thesis
   4.485 -    by simp
   4.486 -qed
   4.487 -
   4.488 -lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
   4.489 -proof -
   4.490 -  have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
   4.491 -  also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
   4.492 -  finally show ?thesis .
   4.493 -qed
   4.494 -
   4.495 -lemma abs_add_abs [simp]:
   4.496 -  "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
   4.497 -proof (rule antisym)
   4.498 -  show "?L \<ge> ?R" by(rule abs_ge_self)
   4.499 -next
   4.500 -  have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
   4.501 -  also have "\<dots> = ?R" by simp
   4.502 -  finally show "?L \<le> ?R" .
   4.503 -qed
   4.504 -
   4.505 -end
   4.506 -
   4.507 -
   4.508 -class lordered_ab_group_abs = lordered_ab_group + abs +
   4.509 +class lordered_ab_group_add_abs = lordered_ab_group_add + abs +
   4.510    assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)"
   4.511  begin
   4.512  
   4.513 @@ -1190,7 +1256,7 @@
   4.514  end
   4.515  
   4.516  lemma sup_eq_if:
   4.517 -  fixes a :: "'a\<Colon>{lordered_ab_group, linorder}"
   4.518 +  fixes a :: "'a\<Colon>{lordered_ab_group_add, linorder}"
   4.519    shows "sup a (- a) = (if a < 0 then - a else a)"
   4.520  proof -
   4.521    note add_le_cancel_right [of a a "- a", symmetric, simplified]
   4.522 @@ -1199,7 +1265,7 @@
   4.523  qed
   4.524  
   4.525  lemma abs_if_lattice:
   4.526 -  fixes a :: "'a\<Colon>{lordered_ab_group_abs, linorder}"
   4.527 +  fixes a :: "'a\<Colon>{lordered_ab_group_add_abs, linorder}"
   4.528    shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
   4.529    by auto
   4.530  
   4.531 @@ -1244,7 +1310,7 @@
   4.532    done
   4.533  
   4.534  lemma estimate_by_abs:
   4.535 -  "a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b" 
   4.536 +  "a + b <= (c::'a::lordered_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
   4.537  proof -
   4.538    assume "a+b <= c"
   4.539    hence 2: "a <= c+(-b)" by (simp add: group_simps)
     5.1 --- a/src/HOL/Real/RealDef.thy	Mon Nov 05 23:17:03 2007 +0100
     5.2 +++ b/src/HOL/Real/RealDef.thy	Tue Nov 06 08:47:25 2007 +0100
     5.3 @@ -418,6 +418,8 @@
     5.4      by (simp only: real_sgn_def)
     5.5  qed
     5.6  
     5.7 +instance real :: lordered_ab_group_add ..
     5.8 +
     5.9  text{*The function @{term real_of_preal} requires many proofs, but it seems
    5.10  to be essential for proving completeness of the reals from that of the
    5.11  positive reals.*}