diff -r 41701fce8ac7 -r f1e387195a56 src/HOL/Library/Function_Algebras.thy --- a/src/HOL/Library/Function_Algebras.thy Tue Feb 21 16:42:57 2012 +0100 +++ b/src/HOL/Library/Function_Algebras.thy Tue Feb 21 16:48:10 2012 +0100 @@ -13,9 +13,7 @@ instantiation "fun" :: (type, plus) plus begin -definition - "f + g = (\x. f x + g x)" - +definition "f + g = (\x. f x + g x)" instance .. end @@ -23,9 +21,7 @@ instantiation "fun" :: (type, zero) zero begin -definition - "0 = (\x. 0)" - +definition "0 = (\x. 0)" instance .. end @@ -33,9 +29,7 @@ instantiation "fun" :: (type, times) times begin -definition - "f * g = (\x. f x * g x)" - +definition "f * g = (\x. f x * g x)" instance .. end @@ -43,9 +37,7 @@ instantiation "fun" :: (type, one) one begin -definition - "1 = (\x. 1)" - +definition "1 = (\x. 1)" instance .. end @@ -53,69 +45,70 @@ text {* Additive structures *} -instance "fun" :: (type, semigroup_add) semigroup_add proof -qed (simp add: plus_fun_def add.assoc) +instance "fun" :: (type, semigroup_add) semigroup_add + by default (simp add: plus_fun_def add.assoc) -instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof -qed (simp_all add: plus_fun_def fun_eq_iff) +instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add + by default (simp_all add: plus_fun_def fun_eq_iff) -instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof -qed (simp add: plus_fun_def add.commute) +instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add + by default (simp add: plus_fun_def add.commute) -instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof -qed simp +instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add + by default simp -instance "fun" :: (type, monoid_add) monoid_add proof -qed (simp_all add: plus_fun_def zero_fun_def) +instance "fun" :: (type, monoid_add) monoid_add + by default (simp_all add: plus_fun_def zero_fun_def) -instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof -qed simp +instance "fun" :: (type, comm_monoid_add) comm_monoid_add + by default simp instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add .. -instance "fun" :: (type, group_add) group_add proof -qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus) +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) -instance "fun" :: (type, ab_group_add) ab_group_add proof -qed (simp_all add: diff_minus) +instance "fun" :: (type, ab_group_add) ab_group_add + by default (simp_all add: diff_minus) text {* Multiplicative structures *} -instance "fun" :: (type, semigroup_mult) semigroup_mult proof -qed (simp add: times_fun_def mult.assoc) +instance "fun" :: (type, semigroup_mult) semigroup_mult + by default (simp add: times_fun_def mult.assoc) -instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof -qed (simp add: times_fun_def mult.commute) +instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult + by default (simp add: times_fun_def mult.commute) -instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof -qed (simp add: times_fun_def) +instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult + by default (simp add: times_fun_def) -instance "fun" :: (type, monoid_mult) monoid_mult proof -qed (simp_all add: times_fun_def one_fun_def) +instance "fun" :: (type, monoid_mult) monoid_mult + by default (simp_all add: times_fun_def one_fun_def) -instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof -qed simp +instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult + by default simp text {* Misc *} instance "fun" :: (type, "Rings.dvd") "Rings.dvd" .. -instance "fun" :: (type, mult_zero) mult_zero proof -qed (simp_all add: zero_fun_def times_fun_def) +instance "fun" :: (type, mult_zero) mult_zero + by default (simp_all add: zero_fun_def times_fun_def) -instance "fun" :: (type, zero_neq_one) zero_neq_one proof -qed (simp add: zero_fun_def one_fun_def 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) text {* Ring structures *} -instance "fun" :: (type, semiring) semiring proof -qed (simp_all add: plus_fun_def times_fun_def algebra_simps) +instance "fun" :: (type, semiring) semiring + by default (simp_all add: plus_fun_def times_fun_def algebra_simps) -instance "fun" :: (type, comm_semiring) comm_semiring proof -qed (simp add: plus_fun_def times_fun_def algebra_simps) +instance "fun" :: (type, comm_semiring) comm_semiring + by default (simp add: plus_fun_def times_fun_def algebra_simps) instance "fun" :: (type, semiring_0) semiring_0 .. @@ -127,8 +120,7 @@ instance "fun" :: (type, semiring_1) semiring_1 .. -lemma of_nat_fun: - shows "of_nat n = (\x::'a. of_nat n)" +lemma of_nat_fun: "of_nat n = (\x::'a. of_nat n)" proof - have comp: "comp = (\f g x. f (g x))" by (rule ext)+ simp @@ -147,7 +139,8 @@ instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel .. -instance "fun" :: (type, semiring_char_0) semiring_char_0 proof +instance "fun" :: (type, semiring_char_0) semiring_char_0 +proof from inj_of_nat have "inj (\n (x::'a). of_nat n :: 'b)" by (rule inj_fun) then have "inj (\n. of_nat n :: 'a \ 'b)" @@ -168,23 +161,24 @@ text {* Ordereded structures *} -instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof -qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono) +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) 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 proof -qed (simp add: plus_fun_def le_fun_def) +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) instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add .. instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add .. -instance "fun" :: (type, ordered_semiring) ordered_semiring proof -qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono) +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) -instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof -qed (fact mult_left_mono) +instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring + by default (fact mult_left_mono) instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..