src/HOL/OrderedGroup.thy
changeset 22422 ee19cdb07528
parent 22390 378f34b1e380
child 22452 8a86fd2a1bf0
     1.1 --- a/src/HOL/OrderedGroup.thy	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  (*  Title:   HOL/OrderedGroup.thy
     1.6      ID:      $Id$
     1.7      Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
     1.8 @@ -570,97 +571,99 @@
     1.9  
    1.10  axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
    1.11  
    1.12 -lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
    1.13 +lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
    1.14  apply (rule order_antisym)
    1.15 -apply (simp_all add: le_meetI)
    1.16 +apply (simp_all add: le_infI)
    1.17  apply (rule add_le_imp_le_left [of "-a"])
    1.18  apply (simp only: add_assoc[symmetric], simp)
    1.19  apply rule
    1.20  apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
    1.21  done
    1.22  
    1.23 -lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
    1.24 +lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
    1.25  apply (rule order_antisym)
    1.26  apply (rule add_le_imp_le_left [of "-a"])
    1.27  apply (simp only: add_assoc[symmetric], simp)
    1.28  apply rule
    1.29  apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
    1.30 -apply (rule join_leI)
    1.31 +apply (rule le_supI)
    1.32  apply (simp_all)
    1.33  done
    1.34  
    1.35 -lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))"
    1.36 +lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
    1.37  apply (auto simp add: is_join_def)
    1.38 -apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
    1.39 -apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
    1.40 +apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
    1.41 +apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
    1.42  apply (subst neg_le_iff_le[symmetric]) 
    1.43 -apply (simp add: le_meetI)
    1.44 +apply (simp add: le_infI)
    1.45  done
    1.46  
    1.47 -lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))"
    1.48 +lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
    1.49  apply (auto simp add: is_meet_def)
    1.50 -apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
    1.51 -apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
    1.52 +apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
    1.53 +apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
    1.54  apply (subst neg_le_iff_le[symmetric]) 
    1.55 -apply (simp add: join_leI)
    1.56 +apply (simp add: le_supI)
    1.57  done
    1.58  
    1.59  axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
    1.60  
    1.61 -instance lordered_ab_group_meet \<subseteq> lordered_ab_group
    1.62 -proof 
    1.63 -  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_meet)
    1.64 -qed
    1.65 -
    1.66  instance lordered_ab_group_join \<subseteq> lordered_ab_group
    1.67  proof
    1.68 -  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_join)
    1.69 +  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
    1.70  qed
    1.71  
    1.72 -lemma add_join_distrib_right: "(join a b) + (c::'a::lordered_ab_group) = join (a+c) (b+c)"
    1.73 +instance lordered_ab_group_meet \<subseteq> lordered_ab_group
    1.74 +proof 
    1.75 +  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
    1.76 +qed
    1.77 +
    1.78 +lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
    1.79  proof -
    1.80 -  have "c + (join a b) = join (c+a) (c+b)" by (simp add: add_join_distrib_left)
    1.81 +  have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
    1.82    thus ?thesis by (simp add: add_commute)
    1.83  qed
    1.84  
    1.85 -lemma add_meet_distrib_right: "(meet a b) + (c::'a::lordered_ab_group) = meet (a+c) (b+c)"
    1.86 +lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
    1.87  proof -
    1.88 -  have "c + (meet a b) = meet (c+a) (c+b)" by (simp add: add_meet_distrib_left)
    1.89 +  have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
    1.90    thus ?thesis by (simp add: add_commute)
    1.91  qed
    1.92  
    1.93 -lemmas add_meet_join_distribs = add_meet_distrib_right add_meet_distrib_left add_join_distrib_right add_join_distrib_left
    1.94 +lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
    1.95  
    1.96 -lemma join_eq_neg_meet: "join a (b::'a::lordered_ab_group) = - meet (-a) (-b)"
    1.97 -by (simp add: is_join_unique[OF is_join_join is_join_neg_meet])
    1.98 +lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
    1.99 +by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
   1.100  
   1.101 -lemma meet_eq_neg_join: "meet a (b::'a::lordered_ab_group) = - join (-a) (-b)"
   1.102 -by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_join])
   1.103 +lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
   1.104 +by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
   1.105  
   1.106 -lemma add_eq_meet_join: "a + b = (join a b) + (meet a (b::'a::lordered_ab_group))"
   1.107 +lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
   1.108  proof -
   1.109 -  have "0 = - meet 0 (a-b) + meet (a-b) 0" by (simp add: meet_comm)
   1.110 -  hence "0 = join 0 (b-a) + meet (a-b) 0" by (simp add: meet_eq_neg_join)
   1.111 -  hence "0 = (-a + join a b) + (meet a b + (-b))"
   1.112 -    apply (simp add: add_join_distrib_left add_meet_distrib_right)
   1.113 +  have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
   1.114 +  hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
   1.115 +  hence "0 = (-a + sup a b) + (inf a b + (-b))"
   1.116 +    apply (simp add: add_sup_distrib_left add_inf_distrib_right)
   1.117      by (simp add: diff_minus add_commute)
   1.118    thus ?thesis
   1.119      apply (simp add: compare_rls)
   1.120 -    apply (subst add_left_cancel[symmetric, of "a+b" "join a b + meet a b" "-a"])
   1.121 +    apply (subst add_left_cancel[symmetric, of "a+b" "sup a b + inf a b" "-a"])
   1.122      apply (simp only: add_assoc, simp add: add_assoc[symmetric])
   1.123      done
   1.124  qed
   1.125  
   1.126  subsection {* Positive Part, Negative Part, Absolute Value *}
   1.127  
   1.128 -constdefs
   1.129 -  pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
   1.130 -  "pprt x == join x 0"
   1.131 -  nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
   1.132 -  "nprt x == meet x 0"
   1.133 +definition
   1.134 +  nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
   1.135 +  "nprt x = inf x 0"
   1.136 +
   1.137 +definition
   1.138 +  pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
   1.139 +  "pprt x = sup x 0"
   1.140  
   1.141  lemma prts: "a = pprt a + nprt a"
   1.142 -by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric])
   1.143 +by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
   1.144  
   1.145  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
   1.146  by (simp add: pprt_def)
   1.147 @@ -687,53 +690,53 @@
   1.148  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
   1.149  
   1.150  lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"
   1.151 -  by (simp add: pprt_def le_def_join join_aci)
   1.152 +  by (simp add: pprt_def le_iff_sup sup_aci)
   1.153  
   1.154  lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
   1.155 -  by (simp add: nprt_def le_def_meet meet_aci)
   1.156 +  by (simp add: nprt_def le_iff_inf inf_aci)
   1.157  
   1.158  lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
   1.159 -  by (simp add: pprt_def le_def_join join_aci)
   1.160 +  by (simp add: pprt_def le_iff_sup sup_aci)
   1.161  
   1.162  lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
   1.163 -  by (simp add: nprt_def le_def_meet meet_aci)
   1.164 +  by (simp add: nprt_def le_iff_inf inf_aci)
   1.165  
   1.166 -lemma join_0_imp_0: "join a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
   1.167 +lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
   1.168  proof -
   1.169    {
   1.170      fix a::'a
   1.171 -    assume hyp: "join a (-a) = 0"
   1.172 -    hence "join a (-a) + a = a" by (simp)
   1.173 -    hence "join (a+a) 0 = a" by (simp add: add_join_distrib_right) 
   1.174 -    hence "join (a+a) 0 <= a" by (simp)
   1.175 -    hence "0 <= a" by (blast intro: order_trans meet_join_le)
   1.176 +    assume hyp: "sup a (-a) = 0"
   1.177 +    hence "sup a (-a) + a = a" by (simp)
   1.178 +    hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) 
   1.179 +    hence "sup (a+a) 0 <= a" by (simp)
   1.180 +    hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
   1.181    }
   1.182    note p = this
   1.183 -  assume hyp:"join a (-a) = 0"
   1.184 -  hence hyp2:"join (-a) (-(-a)) = 0" by (simp add: join_comm)
   1.185 +  assume hyp:"sup a (-a) = 0"
   1.186 +  hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
   1.187    from p[OF hyp] p[OF hyp2] show "a = 0" by simp
   1.188  qed
   1.189  
   1.190 -lemma meet_0_imp_0: "meet a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
   1.191 -apply (simp add: meet_eq_neg_join)
   1.192 -apply (simp add: join_comm)
   1.193 -apply (erule join_0_imp_0)
   1.194 +lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
   1.195 +apply (simp add: inf_eq_neg_sup)
   1.196 +apply (simp add: sup_commute)
   1.197 +apply (erule sup_0_imp_0)
   1.198  done
   1.199  
   1.200 -lemma join_0_eq_0[simp]: "(join a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   1.201 -by (auto, erule join_0_imp_0)
   1.202 +lemma inf_0_eq_0[simp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   1.203 +by (auto, erule inf_0_imp_0)
   1.204  
   1.205 -lemma meet_0_eq_0[simp]: "(meet a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   1.206 -by (auto, erule meet_0_imp_0)
   1.207 +lemma sup_0_eq_0[simp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   1.208 +by (auto, erule sup_0_imp_0)
   1.209  
   1.210  lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
   1.211  proof
   1.212    assume "0 <= a + a"
   1.213 -  hence a:"meet (a+a) 0 = 0" by (simp add: le_def_meet meet_comm)
   1.214 -  have "(meet a 0)+(meet a 0) = meet (meet (a+a) 0) a" (is "?l=_") by (simp add: add_meet_join_distribs meet_aci)
   1.215 -  hence "?l = 0 + meet a 0" by (simp add: a, simp add: meet_comm)
   1.216 -  hence "meet a 0 = 0" by (simp only: add_right_cancel)
   1.217 -  then show "0 <= a" by (simp add: le_def_meet meet_comm)    
   1.218 +  hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
   1.219 +  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.220 +  hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
   1.221 +  hence "inf a 0 = 0" by (simp only: add_right_cancel)
   1.222 +  then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
   1.223  next  
   1.224    assume a: "0 <= a"
   1.225    show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
   1.226 @@ -759,7 +762,7 @@
   1.227  qed
   1.228  
   1.229  axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
   1.230 -  abs_lattice: "abs x = join x (-x)"
   1.231 +  abs_lattice: "abs x = sup x (-x)"
   1.232  
   1.233  lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
   1.234  by (simp add: abs_lattice)
   1.235 @@ -773,22 +776,22 @@
   1.236    thus ?thesis by simp
   1.237  qed
   1.238  
   1.239 -lemma neg_meet_eq_join[simp]: "- meet a (b::_::lordered_ab_group) = join (-a) (-b)"
   1.240 -by (simp add: meet_eq_neg_join)
   1.241 +lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"
   1.242 +by (simp add: inf_eq_neg_sup)
   1.243  
   1.244 -lemma neg_join_eq_meet[simp]: "- join a (b::_::lordered_ab_group) = meet (-a) (-b)"
   1.245 -by (simp del: neg_meet_eq_join add: join_eq_neg_meet)
   1.246 +lemma neg_sup_eq_inf[simp]: "- sup a (b::_::lordered_ab_group) = inf (-a) (-b)"
   1.247 +by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)
   1.248  
   1.249 -lemma join_eq_if: "join a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
   1.250 +lemma sup_eq_if: "sup a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
   1.251  proof -
   1.252    note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
   1.253    have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
   1.254 -  show ?thesis by (auto simp add: join_max max_def b linorder_not_less)
   1.255 +  show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
   1.256  qed
   1.257  
   1.258  lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
   1.259  proof -
   1.260 -  show ?thesis by (simp add: abs_lattice join_eq_if)
   1.261 +  show ?thesis by (simp add: abs_lattice sup_eq_if)
   1.262  qed
   1.263  
   1.264  lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
   1.265 @@ -824,16 +827,16 @@
   1.266  
   1.267  lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
   1.268  apply (simp add: pprt_def nprt_def diff_minus)
   1.269 -apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric])
   1.270 -apply (subst join_absorp2, auto)
   1.271 +apply (simp add: add_sup_inf_distribs sup_aci abs_lattice[symmetric])
   1.272 +apply (subst sup_absorb2, auto)
   1.273  done
   1.274  
   1.275  lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
   1.276 -by (simp add: abs_lattice join_comm)
   1.277 +by (simp add: abs_lattice sup_commute)
   1.278  
   1.279  lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
   1.280  apply (simp add: abs_lattice[of "abs a"])
   1.281 -apply (subst join_absorp1)
   1.282 +apply (subst sup_absorb1)
   1.283  apply (rule order_trans[of _ 0])
   1.284  by auto
   1.285  
   1.286 @@ -847,22 +850,22 @@
   1.287  qed
   1.288  
   1.289  lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"
   1.290 -by (simp add: le_def_meet nprt_def meet_comm)
   1.291 +by (simp add: le_iff_inf nprt_def inf_commute)
   1.292  
   1.293  lemma le_zero_iff_zero_pprt: "(a \<le> 0) = (pprt a = 0)"
   1.294 -by (simp add: le_def_join pprt_def join_comm)
   1.295 +by (simp add: le_iff_sup pprt_def sup_commute)
   1.296  
   1.297  lemma le_zero_iff_pprt_id: "(0 \<le> a) = (pprt a = a)"
   1.298 -by (simp add: le_def_join pprt_def join_comm)
   1.299 +by (simp add: le_iff_sup pprt_def sup_commute)
   1.300  
   1.301  lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
   1.302 -by (simp add: le_def_meet nprt_def meet_comm)
   1.303 +by (simp add: le_iff_inf nprt_def inf_commute)
   1.304  
   1.305  lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
   1.306 -  by (simp add: le_def_join pprt_def join_aci)
   1.307 +  by (simp add: le_iff_sup pprt_def sup_aci)
   1.308  
   1.309  lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
   1.310 -  by (simp add: le_def_meet nprt_def meet_aci)
   1.311 +  by (simp add: le_iff_inf nprt_def inf_aci)
   1.312  
   1.313  lemma pprt_neg: "pprt (-x) = - nprt x"
   1.314    by (simp add: pprt_def nprt_def)
   1.315 @@ -887,7 +890,7 @@
   1.316  by (rule abs_of_nonpos, rule order_less_imp_le)
   1.317  
   1.318  lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
   1.319 -by (simp add: abs_lattice join_leI)
   1.320 +by (simp add: abs_lattice le_supI)
   1.321  
   1.322  lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
   1.323  proof -
   1.324 @@ -914,14 +917,14 @@
   1.325  
   1.326  lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
   1.327  proof -
   1.328 -  have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
   1.329 -    by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
   1.330 -  have a:"a+b <= join ?m ?n" by (simp)
   1.331 +  have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
   1.332 +    by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
   1.333 +  have a:"a+b <= sup ?m ?n" by (simp)
   1.334    have b:"-a-b <= ?n" by (simp) 
   1.335 -  have c:"?n <= join ?m ?n" by (simp)
   1.336 -  from b c have d: "-a-b <= join ?m ?n" by(rule order_trans)
   1.337 +  have c:"?n <= sup ?m ?n" by (simp)
   1.338 +  from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
   1.339    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   1.340 -  from a d e have "abs(a+b) <= join ?m ?n" 
   1.341 +  from a d e have "abs(a+b) <= sup ?m ?n" 
   1.342      by (drule_tac abs_leI, auto)
   1.343    with g[symmetric] show ?thesis by simp
   1.344  qed
   1.345 @@ -1126,24 +1129,24 @@
   1.346  val compare_rls = thms "compare_rls";
   1.347  val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
   1.348  val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
   1.349 -val add_meet_distrib_left = thm "add_meet_distrib_left";
   1.350 -val add_join_distrib_left = thm "add_join_distrib_left";
   1.351 -val is_join_neg_meet = thm "is_join_neg_meet";
   1.352 -val is_meet_neg_join = thm "is_meet_neg_join";
   1.353 -val add_join_distrib_right = thm "add_join_distrib_right";
   1.354 -val add_meet_distrib_right = thm "add_meet_distrib_right";
   1.355 -val add_meet_join_distribs = thms "add_meet_join_distribs";
   1.356 -val join_eq_neg_meet = thm "join_eq_neg_meet";
   1.357 -val meet_eq_neg_join = thm "meet_eq_neg_join";
   1.358 -val add_eq_meet_join = thm "add_eq_meet_join";
   1.359 +val add_inf_distrib_left = thm "add_inf_distrib_left";
   1.360 +val add_sup_distrib_left = thm "add_sup_distrib_left";
   1.361 +val is_join_neg_inf = thm "is_join_neg_inf";
   1.362 +val is_meet_neg_sup = thm "is_meet_neg_sup";
   1.363 +val add_sup_distrib_right = thm "add_sup_distrib_right";
   1.364 +val add_inf_distrib_right = thm "add_inf_distrib_right";
   1.365 +val add_sup_inf_distribs = thms "add_sup_inf_distribs";
   1.366 +val sup_eq_neg_inf = thm "sup_eq_neg_inf";
   1.367 +val inf_eq_neg_sup = thm "inf_eq_neg_sup";
   1.368 +val add_eq_inf_sup = thm "add_eq_inf_sup";
   1.369  val prts = thm "prts";
   1.370  val zero_le_pprt = thm "zero_le_pprt";
   1.371  val nprt_le_zero = thm "nprt_le_zero";
   1.372  val le_eq_neg = thm "le_eq_neg";
   1.373 -val join_0_imp_0 = thm "join_0_imp_0";
   1.374 -val meet_0_imp_0 = thm "meet_0_imp_0";
   1.375 -val join_0_eq_0 = thm "join_0_eq_0";
   1.376 -val meet_0_eq_0 = thm "meet_0_eq_0";
   1.377 +val sup_0_imp_0 = thm "sup_0_imp_0";
   1.378 +val inf_0_imp_0 = thm "inf_0_imp_0";
   1.379 +val sup_0_eq_0 = thm "sup_0_eq_0";
   1.380 +val inf_0_eq_0 = thm "inf_0_eq_0";
   1.381  val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add";
   1.382  val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero";
   1.383  val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero";
   1.384 @@ -1151,9 +1154,9 @@
   1.385  val abs_zero = thm "abs_zero";
   1.386  val abs_eq_0 = thm "abs_eq_0";
   1.387  val abs_0_eq = thm "abs_0_eq";
   1.388 -val neg_meet_eq_join = thm "neg_meet_eq_join";
   1.389 -val neg_join_eq_meet = thm "neg_join_eq_meet";
   1.390 -val join_eq_if = thm "join_eq_if";
   1.391 +val neg_inf_eq_sup = thm "neg_inf_eq_sup";
   1.392 +val neg_sup_eq_inf = thm "neg_sup_eq_inf";
   1.393 +val sup_eq_if = thm "sup_eq_if";
   1.394  val abs_if_lattice = thm "abs_if_lattice";
   1.395  val abs_ge_zero = thm "abs_ge_zero";
   1.396  val abs_le_zero_iff = thm "abs_le_zero_iff";
   1.397 @@ -1161,10 +1164,10 @@
   1.398  val abs_not_less_zero = thm "abs_not_less_zero";
   1.399  val abs_ge_self = thm "abs_ge_self";
   1.400  val abs_ge_minus_self = thm "abs_ge_minus_self";
   1.401 -val le_imp_join_eq = thm "join_absorp2";
   1.402 -val ge_imp_join_eq = thm "join_absorp1";
   1.403 -val le_imp_meet_eq = thm "meet_absorp1";
   1.404 -val ge_imp_meet_eq = thm "meet_absorp2";
   1.405 +val le_imp_join_eq = thm "sup_absorb2";
   1.406 +val ge_imp_join_eq = thm "sup_absorb1";
   1.407 +val le_imp_meet_eq = thm "inf_absorb1";
   1.408 +val ge_imp_meet_eq = thm "inf_absorb2";
   1.409  val abs_prts = thm "abs_prts";
   1.410  val abs_minus_cancel = thm "abs_minus_cancel";
   1.411  val abs_idempotent = thm "abs_idempotent";
   1.412 @@ -1173,8 +1176,6 @@
   1.413  val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
   1.414  val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
   1.415  val iff2imp = thm "iff2imp";
   1.416 -(* val imp_abs_id = thm "imp_abs_id";
   1.417 -val imp_abs_neg_id = thm "imp_abs_neg_id"; *)
   1.418  val abs_leI = thm "abs_leI";
   1.419  val le_minus_self_iff = thm "le_minus_self_iff";
   1.420  val minus_le_self_iff = thm "minus_le_self_iff";