src/HOL/Library/Function_Algebras.thy
changeset 60679 ade12ef2773c
parent 60562 24af00b010cf
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -62,46 +62,45 @@
     1.4  text \<open>Additive structures\<close>
     1.5  
     1.6  instance "fun" :: (type, semigroup_add) semigroup_add
     1.7 -  by default (simp add: fun_eq_iff add.assoc)
     1.8 +  by standard (simp add: fun_eq_iff add.assoc)
     1.9  
    1.10  instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
    1.11 -  by default (simp_all add: fun_eq_iff)
    1.12 +  by standard (simp_all add: fun_eq_iff)
    1.13  
    1.14  instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
    1.15 -  by default (simp add: fun_eq_iff add.commute)
    1.16 +  by standard (simp add: fun_eq_iff add.commute)
    1.17  
    1.18  instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    1.19 -  by default (simp_all add: fun_eq_iff diff_diff_eq)
    1.20 +  by standard (simp_all add: fun_eq_iff diff_diff_eq)
    1.21  
    1.22  instance "fun" :: (type, monoid_add) monoid_add
    1.23 -  by default (simp_all add: fun_eq_iff)
    1.24 +  by standard (simp_all add: fun_eq_iff)
    1.25  
    1.26  instance "fun" :: (type, comm_monoid_add) comm_monoid_add
    1.27 -  by default simp
    1.28 +  by standard simp
    1.29  
    1.30  instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    1.31  
    1.32  instance "fun" :: (type, group_add) group_add
    1.33 -  by default
    1.34 -    (simp_all add: fun_eq_iff)
    1.35 +  by standard (simp_all add: fun_eq_iff)
    1.36  
    1.37  instance "fun" :: (type, ab_group_add) ab_group_add
    1.38 -  by default simp_all
    1.39 +  by standard simp_all
    1.40  
    1.41  
    1.42  text \<open>Multiplicative structures\<close>
    1.43  
    1.44  instance "fun" :: (type, semigroup_mult) semigroup_mult
    1.45 -  by default (simp add: fun_eq_iff mult.assoc)
    1.46 +  by standard (simp add: fun_eq_iff mult.assoc)
    1.47  
    1.48  instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
    1.49 -  by default (simp add: fun_eq_iff mult.commute)
    1.50 +  by standard (simp add: fun_eq_iff mult.commute)
    1.51  
    1.52  instance "fun" :: (type, monoid_mult) monoid_mult
    1.53 -  by default (simp_all add: fun_eq_iff)
    1.54 +  by standard (simp_all add: fun_eq_iff)
    1.55  
    1.56  instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
    1.57 -  by default simp
    1.58 +  by standard simp
    1.59  
    1.60  
    1.61  text \<open>Misc\<close>
    1.62 @@ -109,19 +108,19 @@
    1.63  instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
    1.64  
    1.65  instance "fun" :: (type, mult_zero) mult_zero
    1.66 -  by default (simp_all add: fun_eq_iff)
    1.67 +  by standard (simp_all add: fun_eq_iff)
    1.68  
    1.69  instance "fun" :: (type, zero_neq_one) zero_neq_one
    1.70 -  by default (simp add: fun_eq_iff)
    1.71 +  by standard (simp add: fun_eq_iff)
    1.72  
    1.73  
    1.74  text \<open>Ring structures\<close>
    1.75  
    1.76  instance "fun" :: (type, semiring) semiring
    1.77 -  by default (simp_all add: fun_eq_iff algebra_simps)
    1.78 +  by standard (simp_all add: fun_eq_iff algebra_simps)
    1.79  
    1.80  instance "fun" :: (type, comm_semiring) comm_semiring
    1.81 -  by default (simp add: fun_eq_iff  algebra_simps)
    1.82 +  by standard (simp add: fun_eq_iff  algebra_simps)
    1.83  
    1.84  instance "fun" :: (type, semiring_0) semiring_0 ..
    1.85  
    1.86 @@ -155,7 +154,7 @@
    1.87  instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
    1.88  
    1.89  instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
    1.90 -  by default (auto simp add: times_fun_def algebra_simps)
    1.91 +  by standard (auto simp add: times_fun_def algebra_simps)
    1.92  
    1.93  instance "fun" :: (type, semiring_char_0) semiring_char_0
    1.94  proof
    1.95 @@ -180,23 +179,22 @@
    1.96  text \<open>Ordered structures\<close>
    1.97  
    1.98  instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
    1.99 -  by default (auto simp add: le_fun_def intro: add_left_mono)
   1.100 +  by standard (auto simp add: le_fun_def intro: add_left_mono)
   1.101  
   1.102  instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   1.103  
   1.104  instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
   1.105 -  by default (simp add: le_fun_def)
   1.106 +  by standard (simp add: le_fun_def)
   1.107  
   1.108  instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
   1.109  
   1.110  instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
   1.111  
   1.112  instance "fun" :: (type, ordered_semiring) ordered_semiring
   1.113 -  by default
   1.114 -    (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
   1.115 +  by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
   1.116  
   1.117  instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
   1.118 -  by default (fact mult_left_mono)
   1.119 +  by standard (fact mult_left_mono)
   1.120  
   1.121  instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
   1.122