src/HOL/Hyperreal/StarClasses.thy
changeset 25304 7491c00f0915
parent 25230 022029099a83
child 25571 c9e39eafc7a0
     1.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 06 08:47:25 2007 +0100
     1.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 06 08:47:30 2007 +0100
     1.3 @@ -326,13 +326,19 @@
     1.4  instance star :: (pordered_ab_semigroup_add_imp_le) pordered_ab_semigroup_add_imp_le
     1.5  by (intro_classes, transfer, rule add_le_imp_le_left)
     1.6  
     1.7 +instance star :: (pordered_comm_monoid_add) pordered_comm_monoid_add ..
     1.8  instance star :: (pordered_ab_group_add) pordered_ab_group_add ..
     1.9 +
    1.10 +instance star :: (pordered_ab_group_add_abs) pordered_ab_group_add_abs 
    1.11 +  by intro_classes (transfer,
    1.12 +    simp add: abs_ge_self abs_leI abs_triangle_ineq)+
    1.13 +
    1.14  instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
    1.15 -instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
    1.16 -instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
    1.17 -instance star :: (lordered_ab_group) lordered_ab_group ..
    1.18 +instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
    1.19 +instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
    1.20 +instance star :: (lordered_ab_group_add) lordered_ab_group_add ..
    1.21  
    1.22 -instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
    1.23 +instance star :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs
    1.24  by (intro_classes, transfer, rule abs_lattice)
    1.25  
    1.26  subsection {* Ring and field classes *}
    1.27 @@ -411,6 +417,8 @@
    1.28  by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
    1.29  
    1.30  instance star :: (pordered_ring) pordered_ring ..
    1.31 +instance star :: (pordered_ring_abs) pordered_ring_abs
    1.32 +  by intro_classes  (transfer, rule abs_eq_mult)
    1.33  instance star :: (lordered_ring) lordered_ring ..
    1.34  
    1.35  instance star :: (abs_if) abs_if