eta-expanded occurences of algebraic functionals are simplified by default
authorhaftmann
Mon Jul 02 10:50:17 2012 +0200 (2012-07-02)
changeset 48173c6a5a4336edf
parent 48172 41222a782780
child 48174 eb72f99737be
eta-expanded occurences of algebraic functionals are simplified by default
src/HOL/Library/Function_Algebras.thy
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Sun Jul 01 02:32:03 2012 +0200
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Mon Jul 02 10:50:17 2012 +0200
     1.3 @@ -18,6 +18,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma plus_fun_apply [simp]:
     1.8 +  "(f + g) x = f x + g x"
     1.9 +  by (simp add: plus_fun_def)
    1.10 +
    1.11  instantiation "fun" :: (type, zero) zero
    1.12  begin
    1.13  
    1.14 @@ -26,6 +30,10 @@
    1.15  
    1.16  end
    1.17  
    1.18 +lemma zero_fun_apply [simp]:
    1.19 +  "0 x = 0"
    1.20 +  by (simp add: zero_fun_def)
    1.21 +
    1.22  instantiation "fun" :: (type, times) times
    1.23  begin
    1.24  
    1.25 @@ -34,6 +42,10 @@
    1.26  
    1.27  end
    1.28  
    1.29 +lemma times_fun_apply [simp]:
    1.30 +  "(f * g) x = f x * g x"
    1.31 +  by (simp add: times_fun_def)
    1.32 +
    1.33  instantiation "fun" :: (type, one) one
    1.34  begin
    1.35  
    1.36 @@ -42,23 +54,27 @@
    1.37  
    1.38  end
    1.39  
    1.40 +lemma one_fun_apply [simp]:
    1.41 +  "1 x = 1"
    1.42 +  by (simp add: one_fun_def)
    1.43 +
    1.44  
    1.45  text {* Additive structures *}
    1.46  
    1.47  instance "fun" :: (type, semigroup_add) semigroup_add
    1.48 -  by default (simp add: plus_fun_def add.assoc)
    1.49 +  by default (simp add: fun_eq_iff add.assoc)
    1.50  
    1.51  instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
    1.52 -  by default (simp_all add: plus_fun_def fun_eq_iff)
    1.53 +  by default (simp_all add: fun_eq_iff)
    1.54  
    1.55  instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
    1.56 -  by default (simp add: plus_fun_def add.commute)
    1.57 +  by default (simp add: fun_eq_iff add.commute)
    1.58  
    1.59  instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    1.60    by default simp
    1.61  
    1.62  instance "fun" :: (type, monoid_add) monoid_add
    1.63 -  by default (simp_all add: plus_fun_def zero_fun_def)
    1.64 +  by default (simp_all add: fun_eq_iff)
    1.65  
    1.66  instance "fun" :: (type, comm_monoid_add) comm_monoid_add
    1.67    by default simp
    1.68 @@ -67,7 +83,7 @@
    1.69  
    1.70  instance "fun" :: (type, group_add) group_add
    1.71    by default
    1.72 -    (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
    1.73 +    (simp_all add: fun_eq_iff diff_minus)
    1.74  
    1.75  instance "fun" :: (type, ab_group_add) ab_group_add
    1.76    by default (simp_all add: diff_minus)
    1.77 @@ -76,16 +92,16 @@
    1.78  text {* Multiplicative structures *}
    1.79  
    1.80  instance "fun" :: (type, semigroup_mult) semigroup_mult
    1.81 -  by default (simp add: times_fun_def mult.assoc)
    1.82 +  by default (simp add: fun_eq_iff mult.assoc)
    1.83  
    1.84  instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
    1.85 -  by default (simp add: times_fun_def mult.commute)
    1.86 +  by default (simp add: fun_eq_iff mult.commute)
    1.87  
    1.88  instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
    1.89 -  by default (simp add: times_fun_def)
    1.90 +  by default (simp add: fun_eq_iff)
    1.91  
    1.92  instance "fun" :: (type, monoid_mult) monoid_mult
    1.93 -  by default (simp_all add: times_fun_def one_fun_def)
    1.94 +  by default (simp_all add: fun_eq_iff)
    1.95  
    1.96  instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
    1.97    by default simp
    1.98 @@ -96,19 +112,19 @@
    1.99  instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
   1.100  
   1.101  instance "fun" :: (type, mult_zero) mult_zero
   1.102 -  by default (simp_all add: zero_fun_def times_fun_def)
   1.103 +  by default (simp_all add: fun_eq_iff)
   1.104  
   1.105  instance "fun" :: (type, zero_neq_one) zero_neq_one
   1.106 -  by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
   1.107 +  by default (simp add: fun_eq_iff)
   1.108  
   1.109  
   1.110  text {* Ring structures *}
   1.111  
   1.112  instance "fun" :: (type, semiring) semiring
   1.113 -  by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
   1.114 +  by default (simp_all add: fun_eq_iff algebra_simps)
   1.115  
   1.116  instance "fun" :: (type, comm_semiring) comm_semiring
   1.117 -  by default (simp add: plus_fun_def times_fun_def algebra_simps)
   1.118 +  by default (simp add: fun_eq_iff  algebra_simps)
   1.119  
   1.120  instance "fun" :: (type, semiring_0) semiring_0 ..
   1.121  
   1.122 @@ -133,6 +149,10 @@
   1.123    finally show ?thesis by (simp add: of_nat_def comp)
   1.124  qed
   1.125  
   1.126 +lemma of_nat_fun_apply [simp]:
   1.127 +  "of_nat n x = of_nat n"
   1.128 +  by (simp add: of_nat_fun)
   1.129 +
   1.130  instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
   1.131  
   1.132  instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
   1.133 @@ -162,12 +182,12 @@
   1.134  text {* Ordereded structures *}
   1.135  
   1.136  instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
   1.137 -  by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
   1.138 +  by default (auto simp add: le_fun_def intro: add_left_mono)
   1.139  
   1.140  instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   1.141  
   1.142  instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
   1.143 -  by default (simp add: plus_fun_def le_fun_def)
   1.144 +  by default (simp add: le_fun_def)
   1.145  
   1.146  instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
   1.147  
   1.148 @@ -175,7 +195,7 @@
   1.149  
   1.150  instance "fun" :: (type, ordered_semiring) ordered_semiring
   1.151    by default
   1.152 -    (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
   1.153 +    (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
   1.154  
   1.155  instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
   1.156    by default (fact mult_left_mono)
   1.157 @@ -195,3 +215,4 @@
   1.158  lemmas func_one = one_fun_def
   1.159  
   1.160  end
   1.161 +