equal
deleted
inserted
replaced
197 class pordered_ab_semigroup_add = order + ab_semigroup_add + |
197 class pordered_ab_semigroup_add = order + ab_semigroup_add + |
198 assumes add_left_mono: "a \<sqsubseteq> b \<Longrightarrow> c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b" |
198 assumes add_left_mono: "a \<sqsubseteq> b \<Longrightarrow> c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b" |
199 |
199 |
200 class pordered_cancel_ab_semigroup_add = |
200 class pordered_cancel_ab_semigroup_add = |
201 pordered_ab_semigroup_add + cancel_ab_semigroup_add |
201 pordered_ab_semigroup_add + cancel_ab_semigroup_add |
202 |
|
203 instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add .. |
|
204 |
202 |
205 class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add + |
203 class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add + |
206 assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b" |
204 assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b" |
207 |
205 |
208 class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add |
206 class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add |