src/HOL/OrderedGroup.thy
changeset 15580 900291ee0af8
parent 15539 333a88244569
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/OrderedGroup.thy	Mon Mar 07 16:55:36 2005 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon Mar 07 18:19:55 2005 +0100
     1.3 @@ -594,6 +594,21 @@
     1.4    from a b show ?thesis by blast
     1.5  qed
     1.6  
     1.7 +lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
     1.8 +lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
     1.9 +
    1.10 +lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"
    1.11 +  by (simp add: pprt_def le_def_join join_aci)
    1.12 +
    1.13 +lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
    1.14 +  by (simp add: nprt_def le_def_meet meet_aci)
    1.15 +
    1.16 +lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
    1.17 +  by (simp add: pprt_def le_def_join join_aci)
    1.18 +
    1.19 +lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
    1.20 +  by (simp add: nprt_def le_def_meet meet_aci)
    1.21 +
    1.22  lemma join_0_imp_0: "join a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
    1.23  proof -
    1.24    {
    1.25 @@ -776,6 +791,12 @@
    1.26  lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
    1.27  by (simp add: le_def_meet nprt_def meet_comm)
    1.28  
    1.29 +lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
    1.30 +  by (simp add: le_def_join pprt_def join_aci)
    1.31 +
    1.32 +lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
    1.33 +  by (simp add: le_def_meet nprt_def meet_aci)
    1.34 +
    1.35  lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
    1.36  by (simp)
    1.37