haftmann@38622: (* Title: HOL/Library/Function_Algebras.thy haftmann@38622: Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM avigad@16908: *) avigad@16908: haftmann@38622: header {* Pointwise instantiation of functions to algebra type classes *} avigad@16908: haftmann@38622: theory Function_Algebras haftmann@30738: imports Main avigad@16908: begin avigad@16908: haftmann@38622: text {* Pointwise operations *} haftmann@25594: haftmann@25594: instantiation "fun" :: (type, plus) plus haftmann@25594: begin avigad@16908: wenzelm@46575: definition "f + g = (\x. f x + g x)" haftmann@25594: instance .. haftmann@25594: haftmann@25594: end haftmann@25594: haftmann@38622: instantiation "fun" :: (type, zero) zero haftmann@38622: begin haftmann@38622: wenzelm@46575: definition "0 = (\x. 0)" haftmann@38622: instance .. haftmann@38622: haftmann@38622: end haftmann@25594: haftmann@25594: instantiation "fun" :: (type, times) times haftmann@25594: begin haftmann@25594: wenzelm@46575: definition "f * g = (\x. f x * g x)" haftmann@25594: instance .. haftmann@25594: haftmann@25594: end haftmann@25594: haftmann@25594: instantiation "fun" :: (type, one) one haftmann@25594: begin haftmann@25594: wenzelm@46575: definition "1 = (\x. 1)" haftmann@25594: instance .. haftmann@25594: haftmann@25594: end avigad@16908: haftmann@38622: haftmann@38622: text {* Additive structures *} haftmann@38622: wenzelm@46575: instance "fun" :: (type, semigroup_add) semigroup_add wenzelm@46575: by default (simp add: plus_fun_def add.assoc) avigad@16908: wenzelm@46575: instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add wenzelm@46575: by default (simp_all add: plus_fun_def fun_eq_iff) avigad@16908: wenzelm@46575: instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add wenzelm@46575: by default (simp add: plus_fun_def add.commute) avigad@16908: wenzelm@46575: instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add wenzelm@46575: by default simp avigad@16908: wenzelm@46575: instance "fun" :: (type, monoid_add) monoid_add wenzelm@46575: by default (simp_all add: plus_fun_def zero_fun_def) avigad@16908: wenzelm@46575: instance "fun" :: (type, comm_monoid_add) comm_monoid_add wenzelm@46575: by default simp haftmann@38622: haftmann@38622: instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add .. avigad@16908: wenzelm@46575: instance "fun" :: (type, group_add) group_add wenzelm@46575: by default wenzelm@46575: (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus) avigad@16908: wenzelm@46575: instance "fun" :: (type, ab_group_add) ab_group_add wenzelm@46575: by default (simp_all add: diff_minus) haftmann@38622: haftmann@38622: haftmann@38622: text {* Multiplicative structures *} avigad@16908: wenzelm@46575: instance "fun" :: (type, semigroup_mult) semigroup_mult wenzelm@46575: by default (simp add: times_fun_def mult.assoc) haftmann@38622: wenzelm@46575: instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult wenzelm@46575: by default (simp add: times_fun_def mult.commute) avigad@16908: wenzelm@46575: instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult wenzelm@46575: by default (simp add: times_fun_def) haftmann@38622: wenzelm@46575: instance "fun" :: (type, monoid_mult) monoid_mult wenzelm@46575: by default (simp_all add: times_fun_def one_fun_def) haftmann@38622: wenzelm@46575: instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult wenzelm@46575: by default simp haftmann@38622: avigad@16908: haftmann@38622: text {* Misc *} haftmann@38622: haftmann@38622: instance "fun" :: (type, "Rings.dvd") "Rings.dvd" .. haftmann@38622: wenzelm@46575: instance "fun" :: (type, mult_zero) mult_zero wenzelm@46575: by default (simp_all add: zero_fun_def times_fun_def) avigad@16908: wenzelm@46575: instance "fun" :: (type, zero_neq_one) zero_neq_one wenzelm@46575: by default (simp add: zero_fun_def one_fun_def fun_eq_iff) wenzelm@19736: avigad@16908: haftmann@38622: text {* Ring structures *} avigad@16908: wenzelm@46575: instance "fun" :: (type, semiring) semiring wenzelm@46575: by default (simp_all add: plus_fun_def times_fun_def algebra_simps) avigad@16908: wenzelm@46575: instance "fun" :: (type, comm_semiring) comm_semiring wenzelm@46575: by default (simp add: plus_fun_def times_fun_def algebra_simps) avigad@16908: haftmann@38622: instance "fun" :: (type, semiring_0) semiring_0 .. haftmann@38622: haftmann@38622: instance "fun" :: (type, comm_semiring_0) comm_semiring_0 .. avigad@16908: haftmann@38622: instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel .. avigad@16908: haftmann@38622: instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel .. avigad@16908: haftmann@38622: instance "fun" :: (type, semiring_1) semiring_1 .. avigad@16908: wenzelm@46575: lemma of_nat_fun: "of_nat n = (\x::'a. of_nat n)" haftmann@38622: proof - haftmann@38622: have comp: "comp = (\f g x. f (g x))" haftmann@38622: by (rule ext)+ simp haftmann@38622: have plus_fun: "plus = (\f g x. f x + g x)" haftmann@38622: by (rule ext, rule ext) (fact plus_fun_def) haftmann@38622: have "of_nat n = (comp (plus (1::'b)) ^^ n) (\x::'a. 0)" haftmann@38622: by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp) haftmann@38622: also have "... = comp ((plus 1) ^^ n) (\x::'a. 0)" haftmann@38622: by (simp only: comp_funpow) haftmann@38622: finally show ?thesis by (simp add: of_nat_def comp) haftmann@38622: qed avigad@16908: haftmann@38622: instance "fun" :: (type, comm_semiring_1) comm_semiring_1 .. avigad@16908: haftmann@38622: instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel .. avigad@16908: haftmann@38622: instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel .. avigad@16908: wenzelm@46575: instance "fun" :: (type, semiring_char_0) semiring_char_0 wenzelm@46575: proof haftmann@38622: from inj_of_nat have "inj (\n (x::'a). of_nat n :: 'b)" haftmann@38622: by (rule inj_fun) haftmann@38622: then have "inj (\n. of_nat n :: 'a \ 'b)" haftmann@38622: by (simp add: of_nat_fun) haftmann@38622: then show "inj (of_nat :: nat \ 'a \ 'b)" . haftmann@38622: qed avigad@16908: haftmann@38622: instance "fun" :: (type, ring) ring .. avigad@16908: haftmann@38622: instance "fun" :: (type, comm_ring) comm_ring .. avigad@16908: haftmann@38622: instance "fun" :: (type, ring_1) ring_1 .. avigad@16908: haftmann@38622: instance "fun" :: (type, comm_ring_1) comm_ring_1 .. avigad@16908: haftmann@38622: instance "fun" :: (type, ring_char_0) ring_char_0 .. avigad@16908: avigad@16908: haftmann@38622: text {* Ordereded structures *} avigad@16908: wenzelm@46575: instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add wenzelm@46575: by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono) avigad@16908: haftmann@38622: instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. avigad@16908: wenzelm@46575: instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le wenzelm@46575: by default (simp add: plus_fun_def le_fun_def) avigad@16908: haftmann@38622: instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add .. haftmann@38622: haftmann@38622: instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add .. avigad@16908: wenzelm@46575: instance "fun" :: (type, ordered_semiring) ordered_semiring wenzelm@46575: by default wenzelm@46575: (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono) avigad@16908: wenzelm@46575: instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring wenzelm@46575: by default (fact mult_left_mono) avigad@16908: haftmann@38622: instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring .. avigad@16908: haftmann@38622: instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring .. haftmann@38622: haftmann@38622: instance "fun" :: (type, ordered_ring) ordered_ring .. avigad@16908: haftmann@38622: instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring .. haftmann@38622: avigad@16908: haftmann@38622: lemmas func_plus = plus_fun_def haftmann@38622: lemmas func_zero = zero_fun_def haftmann@38622: lemmas func_times = times_fun_def haftmann@38622: lemmas func_one = one_fun_def wenzelm@19736: avigad@16908: end