# HG changeset patch # User haftmann # Date 1341219017 -7200 # Node ID c6a5a4336edfa17d37d83135e613caaae179686e # Parent 41222a78278019f03d2c3e768435467740818cde eta-expanded occurences of algebraic functionals are simplified by default diff -r 41222a782780 -r c6a5a4336edf src/HOL/Library/Function_Algebras.thy --- 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 +