src/HOL/OrderedGroup.thy
changeset 24286 7619080e49f0
parent 24137 8d7896398147
child 24380 c215e256beca
     1.1 --- a/src/HOL/OrderedGroup.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -711,16 +711,16 @@
     1.4  lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
     1.5  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
     1.6  
     1.7 -lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"
     1.8 +lemma pprt_eq_id[simp,noatp]: "0 <= x \<Longrightarrow> pprt x = x"
     1.9    by (simp add: pprt_def le_iff_sup sup_aci)
    1.10  
    1.11 -lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
    1.12 +lemma nprt_eq_id[simp,noatp]: "x <= 0 \<Longrightarrow> nprt x = x"
    1.13    by (simp add: nprt_def le_iff_inf inf_aci)
    1.14  
    1.15 -lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
    1.16 +lemma pprt_eq_0[simp,noatp]: "x <= 0 \<Longrightarrow> pprt x = 0"
    1.17    by (simp add: pprt_def le_iff_sup sup_aci)
    1.18  
    1.19 -lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
    1.20 +lemma nprt_eq_0[simp,noatp]: "0 <= x \<Longrightarrow> nprt x = 0"
    1.21    by (simp add: nprt_def le_iff_inf inf_aci)
    1.22  
    1.23  lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
    1.24 @@ -745,10 +745,10 @@
    1.25  apply (erule sup_0_imp_0)
    1.26  done
    1.27  
    1.28 -lemma inf_0_eq_0[simp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
    1.29 +lemma inf_0_eq_0[simp,noatp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
    1.30  by (auto, erule inf_0_imp_0)
    1.31  
    1.32 -lemma sup_0_eq_0[simp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
    1.33 +lemma sup_0_eq_0[simp,noatp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
    1.34  by (auto, erule sup_0_imp_0)
    1.35  
    1.36  lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
    1.37 @@ -798,6 +798,8 @@
    1.38    thus ?thesis by simp
    1.39  qed
    1.40  
    1.41 +declare abs_0_eq [noatp] (*essentially the same as the other one*)
    1.42 +
    1.43  lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"
    1.44  by (simp add: inf_eq_neg_sup)
    1.45  
    1.46 @@ -883,10 +885,10 @@
    1.47  lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
    1.48  by (simp add: le_iff_inf nprt_def inf_commute)
    1.49  
    1.50 -lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
    1.51 +lemma pprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
    1.52    by (simp add: le_iff_sup pprt_def sup_aci)
    1.53  
    1.54 -lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
    1.55 +lemma nprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
    1.56    by (simp add: le_iff_inf nprt_def inf_aci)
    1.57  
    1.58  lemma pprt_neg: "pprt (-x) = - nprt x"
    1.59 @@ -1063,7 +1065,7 @@
    1.60  lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
    1.61  lemmas diff_le_0_iff_le = le_iff_diff_le_0 [symmetric]
    1.62  declare diff_less_0_iff_less [simp]
    1.63 -declare diff_eq_0_iff_eq [simp]
    1.64 +declare diff_eq_0_iff_eq [simp,noatp]
    1.65  declare diff_le_0_iff_le [simp]
    1.66  
    1.67  ML {*