98% localized
authorhaftmann
Fri Oct 19 07:48:25 2007 +0200 (2007-10-19)
changeset 250904a50b958391a
parent 25089 04b8456f7754
child 25091 a2ae7f71613d
98% localized
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Oct 19 07:48:23 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Oct 19 07:48:25 2007 +0200
     1.3 @@ -674,26 +674,34 @@
     1.4  subsection {* Lattice Ordered (Abelian) Groups *}
     1.5  
     1.6  class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
     1.7 -
     1.8 -class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
     1.9 -
    1.10 -class lordered_ab_group = pordered_ab_group_add + lattice
    1.11 +begin
    1.12  
    1.13 -instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default
    1.14 -instance lordered_ab_group \<subseteq> lordered_ab_group_join by default
    1.15 -
    1.16 -lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))"
    1.17 -apply (rule order_antisym)
    1.18 +lemma add_inf_distrib_left:
    1.19 +  "a + inf b c = inf (a + b) (a + c)"
    1.20 +apply (rule antisym)
    1.21  apply (simp_all add: le_infI)
    1.22 -apply (rule add_le_imp_le_left [of "-a"])
    1.23 -apply (simp only: add_assoc[symmetric], simp)
    1.24 +apply (rule add_le_imp_le_left [of "uminus a"])
    1.25 +apply (simp only: add_assoc [symmetric], simp)
    1.26  apply rule
    1.27  apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
    1.28  done
    1.29  
    1.30 -lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))" 
    1.31 -apply (rule order_antisym)
    1.32 -apply (rule add_le_imp_le_left [of "-a"])
    1.33 +lemma add_inf_distrib_right:
    1.34 +  "inf a b + c = inf (a + c) (b + c)"
    1.35 +proof -
    1.36 +  have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
    1.37 +  thus ?thesis by (simp add: add_commute)
    1.38 +qed
    1.39 +
    1.40 +end
    1.41 +
    1.42 +class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
    1.43 +begin
    1.44 +
    1.45 +lemma add_sup_distrib_left:
    1.46 +  "a + sup b c = sup (a + b) (a + c)" 
    1.47 +apply (rule antisym)
    1.48 +apply (rule add_le_imp_le_left [of "uminus a"])
    1.49  apply (simp only: add_assoc[symmetric], simp)
    1.50  apply rule
    1.51  apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
    1.52 @@ -701,29 +709,39 @@
    1.53  apply (simp_all)
    1.54  done
    1.55  
    1.56 -lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
    1.57 -proof -
    1.58 -  have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
    1.59 -  thus ?thesis by (simp add: add_commute)
    1.60 -qed
    1.61 -
    1.62 -lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
    1.63 +lemma add_sup_distrib_right:
    1.64 +  "sup a b + c = sup (a+c) (b+c)"
    1.65  proof -
    1.66    have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
    1.67    thus ?thesis by (simp add: add_commute)
    1.68  qed
    1.69  
    1.70 +end
    1.71 +
    1.72 +class lordered_ab_group = pordered_ab_group_add + lattice
    1.73 +begin
    1.74 +
    1.75 +subclass lordered_ab_group_meet by unfold_locales
    1.76 +subclass lordered_ab_group_join by unfold_locales
    1.77 +
    1.78 +end
    1.79 +
    1.80 +context lordered_ab_group
    1.81 +begin
    1.82 +
    1.83  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
    1.84  
    1.85 -lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)"
    1.86 +lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
    1.87  proof (rule inf_unique)
    1.88    fix a b :: 'a
    1.89 -  show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
    1.90 -    (simp, simp add: add_sup_distrib_left)
    1.91 +  show "- sup (-a) (-b) \<le> a"
    1.92 +    by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
    1.93 +      (simp, simp add: add_sup_distrib_left)
    1.94  next
    1.95    fix a b :: 'a
    1.96 -  show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
    1.97 -    (simp, simp add: add_sup_distrib_left)
    1.98 +  show "- sup (-a) (-b) \<le> b"
    1.99 +    by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
   1.100 +      (simp, simp add: add_sup_distrib_left)
   1.101  next
   1.102    fix a b c :: 'a
   1.103    assume "a \<le> b" "a \<le> c"
   1.104 @@ -731,15 +749,17 @@
   1.105      (simp add: le_supI)
   1.106  qed
   1.107    
   1.108 -lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)"
   1.109 +lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)"
   1.110  proof (rule sup_unique)
   1.111    fix a b :: 'a
   1.112 -  show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
   1.113 -    (simp, simp add: add_inf_distrib_left)
   1.114 +  show "a \<le> - inf (-a) (-b)"
   1.115 +    by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
   1.116 +      (simp, simp add: add_inf_distrib_left)
   1.117  next
   1.118    fix a b :: 'a
   1.119 -  show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
   1.120 -    (simp, simp add: add_inf_distrib_left)
   1.121 +  show "b \<le> - inf (-a) (-b)"
   1.122 +    by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
   1.123 +      (simp, simp add: add_inf_distrib_left)
   1.124  next
   1.125    fix a b c :: 'a
   1.126    assume "a \<le> c" "b \<le> c"
   1.127 @@ -747,7 +767,7 @@
   1.128      (simp add: le_infI)
   1.129  qed
   1.130  
   1.131 -lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)"
   1.132 +lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
   1.133  proof -
   1.134    have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
   1.135    hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
   1.136 @@ -756,7 +776,7 @@
   1.137      by (simp add: diff_minus add_commute)
   1.138    thus ?thesis
   1.139      apply (simp add: compare_rls)
   1.140 -    apply (subst add_left_cancel[symmetric, of "a+b" "sup a b + inf a b" "-a"])
   1.141 +    apply (subst add_left_cancel [symmetric, of "plus a b" "plus (sup a b) (inf a b)" "uminus a"])
   1.142      apply (simp only: add_assoc, simp add: add_assoc[symmetric])
   1.143      done
   1.144  qed
   1.145 @@ -764,27 +784,27 @@
   1.146  subsection {* Positive Part, Negative Part, Absolute Value *}
   1.147  
   1.148  definition
   1.149 -  nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
   1.150 +  nprt :: "'a \<Rightarrow> 'a" where
   1.151    "nprt x = inf x 0"
   1.152  
   1.153  definition
   1.154 -  pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
   1.155 +  pprt :: "'a \<Rightarrow> 'a" where
   1.156    "pprt x = sup x 0"
   1.157  
   1.158  lemma prts: "a = pprt a + nprt a"
   1.159 -by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
   1.160 +  by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
   1.161  
   1.162  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
   1.163 -by (simp add: pprt_def)
   1.164 +  by (simp add: pprt_def)
   1.165  
   1.166  lemma nprt_le_zero[simp]: "nprt a \<le> 0"
   1.167 -by (simp add: nprt_def)
   1.168 +  by (simp add: nprt_def)
   1.169  
   1.170 -lemma le_eq_neg: "(a \<le> -b) = (a + b \<le> (0::_::lordered_ab_group))" (is "?l = ?r")
   1.171 +lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r")
   1.172  proof -
   1.173    have a: "?l \<longrightarrow> ?r"
   1.174      apply (auto)
   1.175 -    apply (rule add_le_imp_le_right[of _ "-b" _])
   1.176 +    apply (rule add_le_imp_le_right[of _ "uminus b" _])
   1.177      apply (simp add: add_assoc)
   1.178      done
   1.179    have b: "?r \<longrightarrow> ?l"
   1.180 @@ -798,19 +818,19 @@
   1.181  lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
   1.182  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
   1.183  
   1.184 -lemma pprt_eq_id[simp,noatp]: "0 <= x \<Longrightarrow> pprt x = x"
   1.185 -  by (simp add: pprt_def le_iff_sup sup_aci)
   1.186 +lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
   1.187 +  by (simp add: pprt_def le_iff_sup sup_ACI)
   1.188  
   1.189 -lemma nprt_eq_id[simp,noatp]: "x <= 0 \<Longrightarrow> nprt x = x"
   1.190 -  by (simp add: nprt_def le_iff_inf inf_aci)
   1.191 +lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
   1.192 +  by (simp add: nprt_def le_iff_inf inf_ACI)
   1.193  
   1.194 -lemma pprt_eq_0[simp,noatp]: "x <= 0 \<Longrightarrow> pprt x = 0"
   1.195 -  by (simp add: pprt_def le_iff_sup sup_aci)
   1.196 +lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
   1.197 +  by (simp add: pprt_def le_iff_sup sup_ACI)
   1.198  
   1.199 -lemma nprt_eq_0[simp,noatp]: "0 <= x \<Longrightarrow> nprt x = 0"
   1.200 -  by (simp add: nprt_def le_iff_inf inf_aci)
   1.201 +lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
   1.202 +  by (simp add: nprt_def le_iff_inf inf_ACI)
   1.203  
   1.204 -lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
   1.205 +lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
   1.206  proof -
   1.207    {
   1.208      fix a::'a
   1.209 @@ -826,23 +846,25 @@
   1.210    from p[OF hyp] p[OF hyp2] show "a = 0" by simp
   1.211  qed
   1.212  
   1.213 -lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
   1.214 +lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0"
   1.215  apply (simp add: inf_eq_neg_sup)
   1.216  apply (simp add: sup_commute)
   1.217  apply (erule sup_0_imp_0)
   1.218  done
   1.219  
   1.220 -lemma inf_0_eq_0[simp,noatp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   1.221 -by (auto, erule inf_0_imp_0)
   1.222 +lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
   1.223 +  by (rule, erule inf_0_imp_0) simp
   1.224  
   1.225 -lemma sup_0_eq_0[simp,noatp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   1.226 -by (auto, erule sup_0_imp_0)
   1.227 +lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
   1.228 +  by (rule, erule sup_0_imp_0) simp
   1.229  
   1.230 -lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
   1.231 +lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   1.232 +  "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   1.233  proof
   1.234    assume "0 <= a + a"
   1.235    hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
   1.236 -  have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") by (simp add: add_sup_inf_distribs inf_aci)
   1.237 +  have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
   1.238 +    by (simp add: add_sup_inf_distribs inf_ACI)
   1.239    hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
   1.240    hence "inf a 0 = 0" by (simp only: add_right_cancel)
   1.241    then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
   1.242 @@ -851,182 +873,206 @@
   1.243    show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
   1.244  qed
   1.245  
   1.246 -lemma double_add_le_zero_iff_single_add_le_zero[simp]: "(a + a <= 0) = ((a::'a::lordered_ab_group) <= 0)" 
   1.247 +lemma double_zero: "a + a = 0 \<longleftrightarrow> a = 0"
   1.248 +proof
   1.249 +  assume assm: "a + a = 0"
   1.250 +  then have "a + a + - a = - a" by simp
   1.251 +  then have "a + (a + - a) = - a" by (simp only: add_assoc)
   1.252 +  then have a: "- a = a" by simp (*FIXME tune proof*)
   1.253 +  show "a = 0" apply rule
   1.254 +  apply (unfold neg_le_iff_le [symmetric, of a])
   1.255 +  unfolding a apply simp
   1.256 +  unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
   1.257 +  unfolding assm unfolding le_less apply simp_all done
   1.258 +next
   1.259 +  assume "a = 0" then show "a + a = 0" by simp
   1.260 +qed
   1.261 +
   1.262 +lemma zero_less_double_add_iff_zero_less_single_add:
   1.263 +  "0 < a + a \<longleftrightarrow> 0 < a"
   1.264 +proof (cases "a = 0")
   1.265 +  case True then show ?thesis by auto
   1.266 +next
   1.267 +  case False then show ?thesis (*FIXME tune proof*)
   1.268 +  unfolding less_le apply simp apply rule
   1.269 +  apply clarify
   1.270 +  apply rule
   1.271 +  apply assumption
   1.272 +  apply (rule notI)
   1.273 +  unfolding double_zero [symmetric, of a] apply simp
   1.274 +  done
   1.275 +qed
   1.276 +
   1.277 +lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   1.278 +  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
   1.279  proof -
   1.280 -  have "(a + a <= 0) = (0 <= -(a+a))" by (subst le_minus_iff, simp)
   1.281 -  moreover have "\<dots> = (a <= 0)" by (simp add: zero_le_double_add_iff_zero_le_single_add)
   1.282 +  have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
   1.283 +  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add)
   1.284    ultimately show ?thesis by blast
   1.285  qed
   1.286  
   1.287 -lemma double_add_less_zero_iff_single_less_zero[simp]: "(a+a<0) = ((a::'a::{pordered_ab_group_add,linorder}) < 0)" (is ?s)
   1.288 -proof cases
   1.289 -  assume a: "a < 0"
   1.290 -  thus ?s by (simp add:  add_strict_mono[OF a a, simplified])
   1.291 -next
   1.292 -  assume "~(a < 0)" 
   1.293 -  hence a:"0 <= a" by (simp)
   1.294 -  hence "0 <= a+a" by (simp add: add_mono[OF a a, simplified])
   1.295 -  hence "~(a+a < 0)" by simp
   1.296 -  with a show ?thesis by simp 
   1.297 +lemma double_add_less_zero_iff_single_less_zero [simp]:
   1.298 +  "a + a < 0 \<longleftrightarrow> a < 0"
   1.299 +proof -
   1.300 +  have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
   1.301 +  moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add)
   1.302 +  ultimately show ?thesis by blast
   1.303  qed
   1.304  
   1.305 +end
   1.306 +
   1.307 +lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   1.308 +
   1.309  class lordered_ab_group_abs = lordered_ab_group + abs +
   1.310 -  assumes abs_lattice: "abs x = sup x (uminus x)"
   1.311 +  assumes abs_lattice: "\<bar>x\<bar> = sup x (- x)"
   1.312 +begin
   1.313  
   1.314 -lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
   1.315 -by (simp add: abs_lattice)
   1.316 +lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   1.317 +  by (simp add: abs_lattice)
   1.318  
   1.319 -lemma abs_eq_0[simp]: "(abs a = 0) = (a = (0::'a::lordered_ab_group_abs))"
   1.320 -by (simp add: abs_lattice)
   1.321 +lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   1.322 +  by (simp add: abs_lattice)
   1.323  
   1.324 -lemma abs_0_eq[simp]: "(0 = abs a) = (a = (0::'a::lordered_ab_group_abs))"
   1.325 +lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
   1.326  proof -
   1.327    have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac)
   1.328    thus ?thesis by simp
   1.329  qed
   1.330  
   1.331 -declare abs_0_eq [noatp] (*essentially the same as the other one*)
   1.332 -
   1.333 -lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"
   1.334 -by (simp add: inf_eq_neg_sup)
   1.335 +lemma neg_inf_eq_sup [simp]: "- inf a b = sup (-a) (-b)"
   1.336 +  by (simp add: inf_eq_neg_sup)
   1.337  
   1.338 -lemma neg_sup_eq_inf[simp]: "- sup a (b::_::lordered_ab_group) = inf (-a) (-b)"
   1.339 -by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)
   1.340 +lemma neg_sup_eq_inf [simp]: "- sup a b = inf (-a) (-b)"
   1.341 +  by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)
   1.342  
   1.343 -lemma sup_eq_if: "sup a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
   1.344 +lemma abs_ge_zero [simp]: "0 \<le> \<bar>a\<bar>"
   1.345  proof -
   1.346 -  note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
   1.347 -  have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
   1.348 -  show ?thesis by (auto simp add: max_def b linorder_not_less sup_max)
   1.349 -qed
   1.350 -
   1.351 -lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
   1.352 -proof -
   1.353 -  show ?thesis by (simp add: abs_lattice sup_eq_if)
   1.354 -qed
   1.355 -
   1.356 -lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
   1.357 -proof -
   1.358 -  have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice)
   1.359 -  show ?thesis by (rule add_mono[OF a b, simplified])
   1.360 +  have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   1.361 +  show ?thesis by (rule add_mono [OF a b, simplified])
   1.362  qed
   1.363    
   1.364 -lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::lordered_ab_group_abs)) = (a = 0)" 
   1.365 +lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
   1.366  proof
   1.367 -  assume "abs a <= 0"
   1.368 -  hence "abs a = 0" by (auto dest: order_antisym)
   1.369 +  assume "\<bar>a\<bar> \<le> 0"
   1.370 +  then have "\<bar>a\<bar> = 0" by (rule antisym) simp
   1.371    thus "a = 0" by simp
   1.372  next
   1.373    assume "a = 0"
   1.374 -  thus "abs a <= 0" by simp
   1.375 +  thus "\<bar>a\<bar> \<le> 0" by simp
   1.376  qed
   1.377  
   1.378 -lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::lordered_ab_group_abs))"
   1.379 -by (simp add: order_less_le)
   1.380 +lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
   1.381 +  by (simp add: less_le)
   1.382  
   1.383 -lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::lordered_ab_group_abs)"
   1.384 +lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
   1.385  proof -
   1.386 -  have a:"!! x (y::_::order). x <= y \<Longrightarrow> ~(y < x)" by auto
   1.387 +  have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
   1.388    show ?thesis by (simp add: a)
   1.389  qed
   1.390  
   1.391 -lemma abs_ge_self: "a \<le> abs (a::'a::lordered_ab_group_abs)"
   1.392 -by (simp add: abs_lattice)
   1.393 +lemma abs_ge_self: "a \<le> \<bar>a\<bar>"
   1.394 +  by (auto simp add: abs_lattice)
   1.395  
   1.396 -lemma abs_ge_minus_self: "-a \<le> abs (a::'a::lordered_ab_group_abs)"
   1.397 -by (simp add: abs_lattice)
   1.398 +lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
   1.399 +  by (auto simp add: abs_lattice)
   1.400  
   1.401 -lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
   1.402 -apply (simp add: pprt_def nprt_def diff_minus)
   1.403 -apply (simp add: add_sup_inf_distribs sup_aci abs_lattice[symmetric])
   1.404 -apply (subst sup_absorb2, auto)
   1.405 -done
   1.406 +lemma abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   1.407 +  by (simp add: abs_lattice sup_commute)
   1.408  
   1.409 -lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
   1.410 -by (simp add: abs_lattice sup_commute)
   1.411 -
   1.412 -lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
   1.413 -apply (simp add: abs_lattice[of "abs a"])
   1.414 +lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   1.415 +apply (simp add: abs_lattice [of "abs a"])
   1.416  apply (subst sup_absorb1)
   1.417 -apply (rule order_trans[of _ 0])
   1.418 +apply (rule order_trans [of _ zero])
   1.419  by auto
   1.420  
   1.421  lemma abs_minus_commute: 
   1.422 -  fixes a :: "'a::lordered_ab_group_abs"
   1.423 -  shows "abs (a-b) = abs(b-a)"
   1.424 +  "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
   1.425  proof -
   1.426 -  have "abs (a-b) = abs (- (a-b))" by (simp only: abs_minus_cancel)
   1.427 -  also have "... = abs(b-a)" by simp
   1.428 +  have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
   1.429 +  also have "... = \<bar>b - a\<bar>" by simp
   1.430    finally show ?thesis .
   1.431  qed
   1.432  
   1.433 -lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"
   1.434 +lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
   1.435 +proof -
   1.436 +  have "0 \<le> \<bar>a\<bar>" by simp
   1.437 +  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   1.438 +  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   1.439 +  then show ?thesis
   1.440 +    by (simp add: add_sup_inf_distribs sup_ACI
   1.441 +      pprt_def nprt_def diff_minus abs_lattice)
   1.442 +qed
   1.443 +  
   1.444 +lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
   1.445 +  by (simp add: le_iff_inf nprt_def inf_commute)
   1.446 +
   1.447 +lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
   1.448 +  by (simp add: le_iff_sup pprt_def sup_commute)
   1.449 +
   1.450 +lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
   1.451 +  by (simp add: le_iff_sup pprt_def sup_commute)
   1.452 +
   1.453 +lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
   1.454  by (simp add: le_iff_inf nprt_def inf_commute)
   1.455  
   1.456 -lemma le_zero_iff_zero_pprt: "(a \<le> 0) = (pprt a = 0)"
   1.457 -by (simp add: le_iff_sup pprt_def sup_commute)
   1.458 -
   1.459 -lemma le_zero_iff_pprt_id: "(0 \<le> a) = (pprt a = a)"
   1.460 -by (simp add: le_iff_sup pprt_def sup_commute)
   1.461 +lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   1.462 +  by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
   1.463  
   1.464 -lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
   1.465 -by (simp add: le_iff_inf nprt_def inf_commute)
   1.466 +lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   1.467 +  by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
   1.468  
   1.469 -lemma pprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
   1.470 -  by (simp add: le_iff_sup pprt_def sup_aci)
   1.471 -
   1.472 -lemma nprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
   1.473 -  by (simp add: le_iff_inf nprt_def inf_aci)
   1.474 -
   1.475 -lemma pprt_neg: "pprt (-x) = - nprt x"
   1.476 +lemma pprt_neg: "pprt (- x) = - nprt x"
   1.477    by (simp add: pprt_def nprt_def)
   1.478  
   1.479 -lemma nprt_neg: "nprt (-x) = - pprt x"
   1.480 +lemma nprt_neg: "nprt (- x) = - pprt x"
   1.481    by (simp add: pprt_def nprt_def)
   1.482  
   1.483 -lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
   1.484 -by (simp add: iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_pprt_id] abs_prts)
   1.485 +lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   1.486 +  by (simp add: iffD1 [OF zero_le_iff_zero_nprt]
   1.487 +    iffD1[OF le_zero_iff_pprt_id] abs_prts)
   1.488  
   1.489 -lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x";
   1.490 -by (rule abs_of_nonneg, rule order_less_imp_le);
   1.491 +lemma abs_of_pos: "0 < x \<Longrightarrow> \<bar>x\<bar> = x"
   1.492 +  by (rule abs_of_nonneg, rule less_imp_le)
   1.493  
   1.494 -lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
   1.495 -by (simp add: iffD1[OF le_zero_iff_zero_pprt] iffD1[OF zero_le_iff_nprt_id] abs_prts)
   1.496 +lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   1.497 +  by (simp add: iffD1 [OF le_zero_iff_zero_pprt]
   1.498 +    iffD1 [OF zero_le_iff_nprt_id] abs_prts)
   1.499  
   1.500 -lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) <  0 ==> 
   1.501 -  abs x = - x"
   1.502 -by (rule abs_of_nonpos, rule order_less_imp_le)
   1.503 +lemma abs_of_neg: "x < 0 \<Longrightarrow> \<bar>x\<bar> = - x"
   1.504 +  by (rule abs_of_nonpos, rule less_imp_le)
   1.505  
   1.506 -lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
   1.507 -by (simp add: abs_lattice le_supI)
   1.508 +lemma abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   1.509 +  by (simp add: abs_lattice le_supI)
   1.510  
   1.511 -lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
   1.512 +lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
   1.513  proof -
   1.514 -  from add_le_cancel_left[of "-a" "a+a" "0"] have "(a <= -a) = (a+a <= 0)" 
   1.515 +  from add_le_cancel_left [of "uminus a" "plus a a" zero]
   1.516 +  have "(a <= -a) = (a+a <= 0)" 
   1.517      by (simp add: add_assoc[symmetric])
   1.518    thus ?thesis by simp
   1.519  qed
   1.520  
   1.521 -lemma minus_le_self_iff: "(-a \<le> a) = (0 \<le> (a::'a::lordered_ab_group))"
   1.522 +lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   1.523  proof -
   1.524 -  from add_le_cancel_left[of "-a" "0" "a+a"] have "(-a <= a) = (0 <= a+a)" 
   1.525 +  from add_le_cancel_left [of "uminus a" zero "plus a a"]
   1.526 +  have "(-a <= a) = (0 <= a+a)" 
   1.527      by (simp add: add_assoc[symmetric])
   1.528    thus ?thesis by simp
   1.529  qed
   1.530  
   1.531 -lemma abs_le_D1: "abs a \<le> b ==> a \<le> (b::'a::lordered_ab_group_abs)"
   1.532 -by (insert abs_ge_self, blast intro: order_trans)
   1.533 +lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   1.534 +  by (insert abs_ge_self, blast intro: order_trans)
   1.535  
   1.536 -lemma abs_le_D2: "abs a \<le> b ==> -a \<le> (b::'a::lordered_ab_group_abs)"
   1.537 -by (insert abs_le_D1 [of "-a"], simp)
   1.538 +lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
   1.539 +  by (insert abs_le_D1 [of "uminus a"], simp)
   1.540  
   1.541 -lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::lordered_ab_group_abs))"
   1.542 -by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   1.543 +lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   1.544 +  by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   1.545  
   1.546 -lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
   1.547 +lemma abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   1.548  proof -
   1.549    have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
   1.550 -    by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
   1.551 +    by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
   1.552    have a:"a+b <= sup ?m ?n" by (simp)
   1.553    have b:"-a-b <= ?n" by (simp) 
   1.554    have c:"?n <= sup ?m ?n" by (simp)
   1.555 @@ -1037,18 +1083,16 @@
   1.556    with g[symmetric] show ?thesis by simp
   1.557  qed
   1.558  
   1.559 -lemma abs_triangle_ineq2: "abs (a::'a::lordered_ab_group_abs) - 
   1.560 -    abs b <= abs (a - b)"
   1.561 +lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
   1.562    apply (simp add: compare_rls)
   1.563 -  apply (subgoal_tac "abs a = abs (a - b + b)")
   1.564 +  apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
   1.565    apply (erule ssubst)
   1.566    apply (rule abs_triangle_ineq)
   1.567 -  apply (rule arg_cong);back;
   1.568 +  apply (rule arg_cong) back
   1.569    apply (simp add: compare_rls)
   1.570  done
   1.571  
   1.572 -lemma abs_triangle_ineq3: 
   1.573 -    "abs(abs (a::'a::lordered_ab_group_abs) - abs b) <= abs (a - b)"
   1.574 +lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
   1.575    apply (subst abs_le_iff)
   1.576    apply auto
   1.577    apply (rule abs_triangle_ineq2)
   1.578 @@ -1056,9 +1100,8 @@
   1.579    apply (rule abs_triangle_ineq2)
   1.580  done
   1.581  
   1.582 -lemma abs_triangle_ineq4: "abs ((a::'a::lordered_ab_group_abs) - b) <= 
   1.583 -    abs a + abs b"
   1.584 -proof -;
   1.585 +lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   1.586 +proof -
   1.587    have "abs(a - b) = abs(a + - b)"
   1.588      by (subst diff_minus, rule refl)
   1.589    also have "... <= abs a + abs (- b)"
   1.590 @@ -1067,8 +1110,7 @@
   1.591      by simp
   1.592  qed
   1.593  
   1.594 -lemma abs_diff_triangle_ineq:
   1.595 -     "\<bar>(a::'a::lordered_ab_group_abs) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>"
   1.596 +lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
   1.597  proof -
   1.598    have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
   1.599    also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
   1.600 @@ -1076,9 +1118,8 @@
   1.601  qed
   1.602  
   1.603  lemma abs_add_abs[simp]:
   1.604 -fixes a:: "'a::{lordered_ab_group_abs}"
   1.605 -shows "abs(abs a + abs b) = abs a + abs b" (is "?L = ?R")
   1.606 -proof (rule order_antisym)
   1.607 +  "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
   1.608 +proof (rule antisym)
   1.609    show "?L \<ge> ?R" by(rule abs_ge_self)
   1.610  next
   1.611    have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
   1.612 @@ -1086,6 +1127,23 @@
   1.613    finally show "?L \<le> ?R" .
   1.614  qed
   1.615  
   1.616 +end
   1.617 +
   1.618 +lemma sup_eq_if:
   1.619 +  fixes a :: "'a\<Colon>{lordered_ab_group, linorder}"
   1.620 +  shows "sup a (- a) = (if a < 0 then - a else a)"
   1.621 +proof -
   1.622 +  note add_le_cancel_right [of a a "- a", symmetric, simplified]
   1.623 +  moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
   1.624 +  then show ?thesis by (auto simp: sup_max max_def)
   1.625 +qed
   1.626 +
   1.627 +lemma abs_if_lattice:
   1.628 +  fixes a :: "'a\<Colon>{lordered_ab_group_abs, linorder}"
   1.629 +  shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
   1.630 +  by auto
   1.631 +
   1.632 +
   1.633  text {* Needed for abelian cancellation simprocs: *}
   1.634  
   1.635  lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
   1.636 @@ -1116,7 +1174,7 @@
   1.637  lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"
   1.638  by (simp add: add_assoc[symmetric])
   1.639  
   1.640 -lemma  le_add_right_mono: 
   1.641 +lemma le_add_right_mono: 
   1.642    assumes 
   1.643    "a <= b + (c::'a::pordered_ab_group_add)"
   1.644    "c <= d"    
   1.645 @@ -1129,7 +1187,7 @@
   1.646    mult_ac
   1.647    add_ac
   1.648    add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.649 -  diff_eq_eq eq_diff_eq  diff_minus[symmetric] uminus_add_conv_diff
   1.650 +  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
   1.651    diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.652  
   1.653  lemma estimate_by_abs:
   1.654 @@ -1141,6 +1199,8 @@
   1.655    show ?thesis by (rule le_add_right_mono[OF 2 3])
   1.656  qed
   1.657  
   1.658 +subsection {* Tools setup *}
   1.659 +
   1.660  lemma add_mono_thms_ordered_semiring [noatp]:
   1.661    fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
   1.662    shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
   1.663 @@ -1159,9 +1219,6 @@
   1.664  by (auto intro: add_strict_right_mono add_strict_left_mono
   1.665    add_less_le_mono add_le_less_mono add_strict_mono)
   1.666  
   1.667 -
   1.668 -subsection {* Tools setup *}
   1.669 -
   1.670  text{*Simplification of @{term "x-y < 0"}, etc.*}
   1.671  lemmas diff_less_0_iff_less [simp] = less_iff_diff_less_0 [symmetric]
   1.672  lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]