src/HOL/Library/Function_Algebras.thy
 author haftmann Mon Aug 23 11:17:13 2010 +0200 (2010-08-23) changeset 38642 8fa437809c67 parent 38622 86fc906dcd86 child 39198 f967a16dfcdd permissions -rw-r--r--
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
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
17   "f + g = (\<lambda>x. f x + g x)"
19 instance ..
21 end
23 instantiation "fun" :: (type, zero) zero
24 begin
26 definition
27   "0 = (\<lambda>x. 0)"
29 instance ..
31 end
33 instantiation "fun" :: (type, times) times
34 begin
36 definition
37   "f * g = (\<lambda>x. f x * g x)"
39 instance ..
41 end
43 instantiation "fun" :: (type, one) one
44 begin
46 definition
47   "1 = (\<lambda>x. 1)"
49 instance ..
51 end
54 text {* Additive structures *}
56 instance "fun" :: (type, semigroup_add) semigroup_add proof
59 instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
60 qed (simp_all add: plus_fun_def expand_fun_eq)
62 instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
65 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
66 qed simp
68 instance "fun" :: (type, monoid_add) monoid_add proof
69 qed (simp_all add: plus_fun_def zero_fun_def)
71 instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
72 qed simp
74 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
76 instance "fun" :: (type, group_add) group_add proof
77 qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
79 instance "fun" :: (type, ab_group_add) ab_group_add proof
80 qed (simp_all add: diff_minus)
83 text {* Multiplicative structures *}
85 instance "fun" :: (type, semigroup_mult) semigroup_mult proof
86 qed (simp add: times_fun_def mult.assoc)
88 instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
89 qed (simp add: times_fun_def mult.commute)
91 instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
92 qed (simp add: times_fun_def)
94 instance "fun" :: (type, monoid_mult) monoid_mult proof
95 qed (simp_all add: times_fun_def one_fun_def)
97 instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
98 qed simp
101 text {* Misc *}
103 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
105 instance "fun" :: (type, mult_zero) mult_zero proof
106 qed (simp_all add: zero_fun_def times_fun_def)
108 instance "fun" :: (type, zero_neq_one) zero_neq_one proof
109 qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
112 text {* Ring structures *}
114 instance "fun" :: (type, semiring) semiring proof
115 qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
117 instance "fun" :: (type, comm_semiring) comm_semiring proof
118 qed (simp add: plus_fun_def times_fun_def algebra_simps)
120 instance "fun" :: (type, semiring_0) semiring_0 ..
122 instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
124 instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
126 instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
128 instance "fun" :: (type, semiring_1) semiring_1 ..
130 lemma of_nat_fun:
131   shows "of_nat n = (\<lambda>x::'a. of_nat n)"
132 proof -
133   have comp: "comp = (\<lambda>f g x. f (g x))"
134     by (rule ext)+ simp
135   have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
136     by (rule ext, rule ext) (fact plus_fun_def)
137   have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
138     by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
139   also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
140     by (simp only: comp_funpow)
141   finally show ?thesis by (simp add: of_nat_def comp)
142 qed
144 instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
146 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
148 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
150 instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
151   from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
152     by (rule inj_fun)
153   then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
154     by (simp add: of_nat_fun)
155   then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
156 qed
158 instance "fun" :: (type, ring) ring ..
160 instance "fun" :: (type, comm_ring) comm_ring ..
162 instance "fun" :: (type, ring_1) ring_1 ..
164 instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
166 instance "fun" :: (type, ring_char_0) ring_char_0 ..
169 text {* Ordereded structures *}
171 instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
172 qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
174 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
176 instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
177 qed (simp add: plus_fun_def le_fun_def)
179 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
181 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
183 instance "fun" :: (type, ordered_semiring) ordered_semiring proof
184 qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
186 instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
187 qed (fact mult_left_mono)
189 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
191 instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
193 instance "fun" :: (type, ordered_ring) ordered_ring ..
195 instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
198 lemmas func_plus = plus_fun_def
199 lemmas func_zero = zero_fun_def
200 lemmas func_times = times_fun_def
201 lemmas func_one = one_fun_def
203 end