
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 = (\<lambda>x. f x + g x)"
haftmann@25594: instance ..
haftmann@25594: 
haftmann@25594: end
haftmann@25594: 
haftmann@48173: lemma plus_fun_apply [simp]:
haftmann@48173:   "(f + g) x = f x + g x"
haftmann@48173:   by (simp add: plus_fun_def)
haftmann@48173: 
haftmann@38622: instantiation "fun" :: (type, zero) zero
haftmann@38622: begin
haftmann@38622: 
wenzelm@46575: definition "0 = (\<lambda>x. 0)"
haftmann@38622: instance ..
haftmann@38622: 
haftmann@38622: end
haftmann@25594: 
haftmann@48173: lemma zero_fun_apply [simp]:
haftmann@48173:   "0 x = 0"
haftmann@48173:   by (simp add: zero_fun_def)
haftmann@48173: 
haftmann@25594: instantiation "fun" :: (type, times) times
haftmann@25594: begin
haftmann@25594: 
wenzelm@46575: definition "f * g = (\<lambda>x. f x * g x)"
haftmann@25594: instance ..
haftmann@25594: 
haftmann@25594: end
haftmann@25594: 
haftmann@48173: lemma times_fun_apply [simp]:
haftmann@48173:   "(f * g) x = f x * g x"
haftmann@48173:   by (simp add: times_fun_def)
haftmann@48173: 
haftmann@25594: instantiation "fun" :: (type, one) one
haftmann@25594: begin
haftmann@25594: 
wenzelm@46575: definition "1 = (\<lambda>x. 1)"
haftmann@25594: instance ..
haftmann@25594: 
haftmann@25594: end
avigad@16908: 
haftmann@48173: lemma one_fun_apply [simp]:
haftmann@48173:   "1 x = 1"
haftmann@48173:   by (simp add: one_fun_def)
haftmann@48173: 
haftmann@38622: 
haftmann@38622: text {* Additive structures *}
haftmann@38622: 
wenzelm@46575: instance "fun" :: (type, semigroup_add) semigroup_add
haftmann@48173:   by default (simp add: fun_eq_iff add.assoc)
avigad@16908: 
wenzelm@46575: instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
haftmann@48173:   by default (simp_all add: fun_eq_iff)
avigad@16908: 
wenzelm@46575: instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
haftmann@48173:   by default (simp add: fun_eq_iff 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
haftmann@48173:   by default (simp_all add: fun_eq_iff)
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
haftmann@48173:     (simp_all add: fun_eq_iff 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
haftmann@48173:   by default (simp add: fun_eq_iff mult.assoc)
haftmann@38622: 
wenzelm@46575: instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
haftmann@48173:   by default (simp add: fun_eq_iff mult.commute)
avigad@16908: 
wenzelm@46575: instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
haftmann@48173:   by default (simp add: fun_eq_iff)
haftmann@38622: 
wenzelm@46575: instance "fun" :: (type, monoid_mult) monoid_mult
haftmann@48173:   by default (simp_all add: fun_eq_iff)
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
haftmann@48173:   by default (simp_all add: fun_eq_iff)
avigad@16908: 
wenzelm@46575: instance "fun" :: (type, zero_neq_one) zero_neq_one
haftmann@48173:   by default (simp add: fun_eq_iff)
wenzelm@19736: 
avigad@16908: 
haftmann@38622: text {* Ring structures *}
avigad@16908: 
wenzelm@46575: instance "fun" :: (type, semiring) semiring
haftmann@48173:   by default (simp_all add: fun_eq_iff algebra_simps)
avigad@16908: 
wenzelm@46575: instance "fun" :: (type, comm_semiring) comm_semiring
haftmann@48173:   by default (simp add: fun_eq_iff  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 = (\<lambda>x::'a. of_nat n)"
haftmann@38622: proof -
haftmann@38622:   have comp: "comp = (\<lambda>f g x. f (g x))"
haftmann@38622:     by (rule ext)+ simp
haftmann@38622:   have plus_fun: "plus = (\<lambda>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) (\<lambda>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) (\<lambda>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@48173: lemma of_nat_fun_apply [simp]:
haftmann@48173:   "of_nat n x = of_nat n"
haftmann@48173:   by (simp add: of_nat_fun)
haftmann@48173: 
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 (\<lambda>n (x::'a). of_nat n :: 'b)"
haftmann@38622:     by (rule inj_fun)
haftmann@38622:   then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
haftmann@38622:     by (simp add: of_nat_fun)
haftmann@38622:   then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> '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
haftmann@48173:   by default (auto simp add: 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
haftmann@48173:   by default (simp add: 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
haftmann@48173:     (auto simp add: 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
haftmann@48173: 




