eta-expanded occurences of algebraic functionals are simplified by default

--- a/src/HOL/Library/Function_Algebras.thy	Sun Jul 01 02:32:03 2012 +0200
+++ b/src/HOL/Library/Function_Algebras.thy	Mon Jul 02 10:50:17 2012 +0200
@@ -18,6 +18,10 @@
 
 end
 
+lemma plus_fun_apply [simp]:
+  "(f + g) x = f x + g x"
+  by (simp add: plus_fun_def)
+
 instantiation "fun" :: (type, zero) zero
 begin
 
@@ -26,6 +30,10 @@
 
 end
 
+lemma zero_fun_apply [simp]:
+  "0 x = 0"
+  by (simp add: zero_fun_def)
+
 instantiation "fun" :: (type, times) times
 begin
 
@@ -34,6 +42,10 @@
 
 end
 
+lemma times_fun_apply [simp]:
+  "(f * g) x = f x * g x"
+  by (simp add: times_fun_def)
+
 instantiation "fun" :: (type, one) one
 begin
 
@@ -42,23 +54,27 @@
 
 end
 
+lemma one_fun_apply [simp]:
+  "1 x = 1"
+  by (simp add: one_fun_def)
+
 
 text {* Additive structures *}
 
 instance "fun" :: (type, semigroup_add) semigroup_add
-  by default (simp add: plus_fun_def add.assoc)
+  by default (simp add: fun_eq_iff add.assoc)
 
 instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
-  by default (simp_all add: plus_fun_def fun_eq_iff)
+  by default (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
-  by default (simp add: plus_fun_def add.commute)
+  by default (simp add: fun_eq_iff add.commute)
 
 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   by default simp
 
 instance "fun" :: (type, monoid_add) monoid_add
-  by default (simp_all add: plus_fun_def zero_fun_def)
+  by default (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, comm_monoid_add) comm_monoid_add
   by default simp
@@ -67,7 +83,7 @@
 
 instance "fun" :: (type, group_add) group_add
   by default
-    (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+    (simp_all add: fun_eq_iff diff_minus)
 
 instance "fun" :: (type, ab_group_add) ab_group_add
   by default (simp_all add: diff_minus)
@@ -76,16 +92,16 @@
 text {* Multiplicative structures *}
 
 instance "fun" :: (type, semigroup_mult) semigroup_mult
-  by default (simp add: times_fun_def mult.assoc)
+  by default (simp add: fun_eq_iff mult.assoc)
 
 instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
-  by default (simp add: times_fun_def mult.commute)
+  by default (simp add: fun_eq_iff mult.commute)
 
 instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
-  by default (simp add: times_fun_def)
+  by default (simp add: fun_eq_iff)
 
 instance "fun" :: (type, monoid_mult) monoid_mult
-  by default (simp_all add: times_fun_def one_fun_def)
+  by default (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
   by default simp
@@ -96,19 +112,19 @@
 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
 
 instance "fun" :: (type, mult_zero) mult_zero
-  by default (simp_all add: zero_fun_def times_fun_def)
+  by default (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, zero_neq_one) zero_neq_one
-  by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
+  by default (simp add: fun_eq_iff)
 
 
 text {* Ring structures *}
 
 instance "fun" :: (type, semiring) semiring
-  by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
+  by default (simp_all add: fun_eq_iff algebra_simps)
 
 instance "fun" :: (type, comm_semiring) comm_semiring
-  by default (simp add: plus_fun_def times_fun_def algebra_simps)
+  by default (simp add: fun_eq_iff  algebra_simps)
 
 instance "fun" :: (type, semiring_0) semiring_0 ..
 
@@ -133,6 +149,10 @@
   finally show ?thesis by (simp add: of_nat_def comp)
 qed
 
+lemma of_nat_fun_apply [simp]:
+  "of_nat n x = of_nat n"
+  by (simp add: of_nat_fun)
+
 instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
 
 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
@@ -162,12 +182,12 @@
 text {* Ordereded structures *}
 
 instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
-  by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+  by default (auto simp add: le_fun_def intro: add_left_mono)
 
 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
 
 instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
-  by default (simp add: plus_fun_def le_fun_def)
+  by default (simp add: le_fun_def)
 
 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
 
@@ -175,7 +195,7 @@
 
 instance "fun" :: (type, ordered_semiring) ordered_semiring
   by default
-    (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+    (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
 
 instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
   by default (fact mult_left_mono)
@@ -195,3 +215,4 @@
 lemmas func_one = one_fun_def
 
 end
+