src/HOL/Library/Function_Algebras.thy
changeset 62376 85f38d5f8807
parent 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Tue Feb 09 09:21:10 2016 +0100
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Wed Feb 10 18:43:19 2016 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  
     1.5  instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
     1.6  
     1.7 -instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
     1.8 +instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel
     1.9    by standard (auto simp add: times_fun_def algebra_simps)
    1.10  
    1.11  instance "fun" :: (type, semiring_char_0) semiring_char_0
    1.12 @@ -188,11 +188,21 @@
    1.13  
    1.14  instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
    1.15  
    1.16 +instance "fun" :: (type, ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
    1.17 +
    1.18  instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
    1.19  
    1.20  instance "fun" :: (type, ordered_semiring) ordered_semiring
    1.21    by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
    1.22  
    1.23 +instance "fun" :: (type, dioid) dioid
    1.24 +proof standard
    1.25 +  fix a b :: "'a \<Rightarrow> 'b"
    1.26 +  show "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
    1.27 +    unfolding le_fun_def plus_fun_def fun_eq_iff choice_iff[symmetric, of "\<lambda>x c. b x = a x + c"]
    1.28 +    by (intro arg_cong[where f=All] ext canonically_ordered_monoid_add_class.le_iff_add)
    1.29 +qed
    1.30 +
    1.31  instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
    1.32    by standard (fact mult_left_mono)
    1.33