src/HOL/Library/Function_Algebras.thy
 author haftmann Tue Feb 19 19:44:10 2013 +0100 (2013-02-19) changeset 51188 9b5bf1a9a710 parent 48173 c6a5a4336edf child 51489 f738e6dbd844 permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
1 (*  Title:      HOL/Library/Function_Algebras.thy
2     Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
3 *)
5 header {* Pointwise instantiation of functions to algebra type classes *}
7 theory Function_Algebras
8 imports Main
9 begin
11 text {* Pointwise operations *}
13 instantiation "fun" :: (type, plus) plus
14 begin
16 definition "f + g = (\<lambda>x. f x + g x)"
17 instance ..
19 end
21 lemma plus_fun_apply [simp]:
22   "(f + g) x = f x + g x"
23   by (simp add: plus_fun_def)
25 instantiation "fun" :: (type, zero) zero
26 begin
28 definition "0 = (\<lambda>x. 0)"
29 instance ..
31 end
33 lemma zero_fun_apply [simp]:
34   "0 x = 0"
35   by (simp add: zero_fun_def)
37 instantiation "fun" :: (type, times) times
38 begin
40 definition "f * g = (\<lambda>x. f x * g x)"
41 instance ..
43 end
45 lemma times_fun_apply [simp]:
46   "(f * g) x = f x * g x"
47   by (simp add: times_fun_def)
49 instantiation "fun" :: (type, one) one
50 begin
52 definition "1 = (\<lambda>x. 1)"
53 instance ..
55 end
57 lemma one_fun_apply [simp]:
58   "1 x = 1"
59   by (simp add: one_fun_def)
62 text {* Additive structures *}
64 instance "fun" :: (type, semigroup_add) semigroup_add
65   by default (simp add: fun_eq_iff add.assoc)
67 instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
68   by default (simp_all add: fun_eq_iff)
70 instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
71   by default (simp add: fun_eq_iff add.commute)
73 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
74   by default simp
76 instance "fun" :: (type, monoid_add) monoid_add
77   by default (simp_all add: fun_eq_iff)
79 instance "fun" :: (type, comm_monoid_add) comm_monoid_add
80   by default simp
82 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
84 instance "fun" :: (type, group_add) group_add
85   by default
86     (simp_all add: fun_eq_iff diff_minus)
88 instance "fun" :: (type, ab_group_add) ab_group_add
89   by default (simp_all add: diff_minus)
92 text {* Multiplicative structures *}
94 instance "fun" :: (type, semigroup_mult) semigroup_mult
95   by default (simp add: fun_eq_iff mult.assoc)
97 instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
98   by default (simp add: fun_eq_iff mult.commute)
100 instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
101   by default (simp add: fun_eq_iff)
103 instance "fun" :: (type, monoid_mult) monoid_mult
104   by default (simp_all add: fun_eq_iff)
106 instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
107   by default simp
110 text {* Misc *}
112 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
114 instance "fun" :: (type, mult_zero) mult_zero
115   by default (simp_all add: fun_eq_iff)
117 instance "fun" :: (type, zero_neq_one) zero_neq_one
118   by default (simp add: fun_eq_iff)
121 text {* Ring structures *}
123 instance "fun" :: (type, semiring) semiring
124   by default (simp_all add: fun_eq_iff algebra_simps)
126 instance "fun" :: (type, comm_semiring) comm_semiring
127   by default (simp add: fun_eq_iff  algebra_simps)
129 instance "fun" :: (type, semiring_0) semiring_0 ..
131 instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
133 instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
135 instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
137 instance "fun" :: (type, semiring_1) semiring_1 ..
139 lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
140 proof -
141   have comp: "comp = (\<lambda>f g x. f (g x))"
142     by (rule ext)+ simp
143   have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
144     by (rule ext, rule ext) (fact plus_fun_def)
145   have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
146     by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
147   also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
148     by (simp only: comp_funpow)
149   finally show ?thesis by (simp add: of_nat_def comp)
150 qed
152 lemma of_nat_fun_apply [simp]:
153   "of_nat n x = of_nat n"
154   by (simp add: of_nat_fun)
156 instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
158 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
160 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
162 instance "fun" :: (type, semiring_char_0) semiring_char_0
163 proof
164   from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
165     by (rule inj_fun)
166   then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
167     by (simp add: of_nat_fun)
168   then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
169 qed
171 instance "fun" :: (type, ring) ring ..
173 instance "fun" :: (type, comm_ring) comm_ring ..
175 instance "fun" :: (type, ring_1) ring_1 ..
177 instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
179 instance "fun" :: (type, ring_char_0) ring_char_0 ..
182 text {* Ordereded structures *}
184 instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
185   by default (auto simp add: le_fun_def intro: add_left_mono)
187 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
189 instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
190   by default (simp add: le_fun_def)
192 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
194 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
196 instance "fun" :: (type, ordered_semiring) ordered_semiring
197   by default
198     (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
200 instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
201   by default (fact mult_left_mono)
203 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
205 instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
207 instance "fun" :: (type, ordered_ring) ordered_ring ..
209 instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
212 lemmas func_plus = plus_fun_def
213 lemmas func_zero = zero_fun_def
214 lemmas func_times = times_fun_def
215 lemmas func_one = one_fun_def
217 end