author  haftmann 
Mon, 02 Jul 2012 10:50:17 +0200  
changeset 48173  c6a5a4336edf 
parent 46575  f1e387195a56 
child 51489  f738e6dbd844 
permissions  rwrr 
38622  1 
(* Title: HOL/Library/Function_Algebras.thy 
2 
Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

3 
*) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

4 

38622  5 
header {* Pointwise instantiation of functions to algebra type classes *} 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

6 

38622  7 
theory Function_Algebras 
30738  8 
imports Main 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

9 
begin 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

10 

38622  11 
text {* Pointwise operations *} 
25594  12 

13 
instantiation "fun" :: (type, plus) plus 

14 
begin 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

15 

46575  16 
definition "f + g = (\<lambda>x. f x + g x)" 
25594  17 
instance .. 
18 

19 
end 

20 

48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

21 
lemma plus_fun_apply [simp]: 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

22 
"(f + g) x = f x + g x" 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

23 
by (simp add: plus_fun_def) 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

24 

38622  25 
instantiation "fun" :: (type, zero) zero 
26 
begin 

27 

46575  28 
definition "0 = (\<lambda>x. 0)" 
38622  29 
instance .. 
30 

31 
end 

25594  32 

48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

33 
lemma zero_fun_apply [simp]: 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

34 
"0 x = 0" 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

35 
by (simp add: zero_fun_def) 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

36 

25594  37 
instantiation "fun" :: (type, times) times 
38 
begin 

39 

46575  40 
definition "f * g = (\<lambda>x. f x * g x)" 
25594  41 
instance .. 
42 

43 
end 

44 

48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

45 
lemma times_fun_apply [simp]: 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

46 
"(f * g) x = f x * g x" 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

47 
by (simp add: times_fun_def) 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

48 

25594  49 
instantiation "fun" :: (type, one) one 
50 
begin 

51 

46575  52 
definition "1 = (\<lambda>x. 1)" 
25594  53 
instance .. 
54 

55 
end 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

56 

48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

57 
lemma one_fun_apply [simp]: 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

58 
"1 x = 1" 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

59 
by (simp add: one_fun_def) 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

60 

38622  61 

62 
text {* Additive structures *} 

63 

46575  64 
instance "fun" :: (type, semigroup_add) semigroup_add 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

65 
by default (simp add: fun_eq_iff add.assoc) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

66 

46575  67 
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

68 
by default (simp_all add: fun_eq_iff) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

69 

46575  70 
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

71 
by default (simp add: fun_eq_iff add.commute) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

72 

46575  73 
instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add 
74 
by default simp 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

75 

46575  76 
instance "fun" :: (type, monoid_add) monoid_add 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

77 
by default (simp_all add: fun_eq_iff) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

78 

46575  79 
instance "fun" :: (type, comm_monoid_add) comm_monoid_add 
80 
by default simp 

38622  81 

82 
instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add .. 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

83 

46575  84 
instance "fun" :: (type, group_add) group_add 
85 
by default 

48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

86 
(simp_all add: fun_eq_iff diff_minus) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

87 

46575  88 
instance "fun" :: (type, ab_group_add) ab_group_add 
89 
by default (simp_all add: diff_minus) 

38622  90 

91 

92 
text {* Multiplicative structures *} 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

93 

46575  94 
instance "fun" :: (type, semigroup_mult) semigroup_mult 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

95 
by default (simp add: fun_eq_iff mult.assoc) 
38622  96 

46575  97 
instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

98 
by default (simp add: fun_eq_iff mult.commute) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

99 

46575  100 
instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

101 
by default (simp add: fun_eq_iff) 
38622  102 

46575  103 
instance "fun" :: (type, monoid_mult) monoid_mult 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

104 
by default (simp_all add: fun_eq_iff) 
38622  105 

46575  106 
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult 
107 
by default simp 

38622  108 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

109 

38622  110 
text {* Misc *} 
111 

112 
instance "fun" :: (type, "Rings.dvd") "Rings.dvd" .. 

113 

46575  114 
instance "fun" :: (type, mult_zero) mult_zero 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

115 
by default (simp_all add: fun_eq_iff) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

116 

46575  117 
instance "fun" :: (type, zero_neq_one) zero_neq_one 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

118 
by default (simp add: fun_eq_iff) 
19736  119 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

120 

38622  121 
text {* Ring structures *} 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

122 

46575  123 
instance "fun" :: (type, semiring) semiring 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

124 
by default (simp_all add: fun_eq_iff algebra_simps) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

125 

46575  126 
instance "fun" :: (type, comm_semiring) comm_semiring 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

127 
by default (simp add: fun_eq_iff algebra_simps) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

128 

38622  129 
instance "fun" :: (type, semiring_0) semiring_0 .. 
130 

131 
instance "fun" :: (type, comm_semiring_0) comm_semiring_0 .. 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

132 

38622  133 
instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

134 

38622  135 
instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

136 

38622  137 
instance "fun" :: (type, semiring_1) semiring_1 .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

138 

46575  139 
lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)" 
38622  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 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

151 

48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

152 
lemma of_nat_fun_apply [simp]: 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

153 
"of_nat n x = of_nat n" 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

154 
by (simp add: of_nat_fun) 
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

155 

38622  156 
instance "fun" :: (type, comm_semiring_1) comm_semiring_1 .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

157 

38622  158 
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

159 

38622  160 
instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

161 

46575  162 
instance "fun" :: (type, semiring_char_0) semiring_char_0 
163 
proof 

38622  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 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

170 

38622  171 
instance "fun" :: (type, ring) ring .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

172 

38622  173 
instance "fun" :: (type, comm_ring) comm_ring .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

174 

38622  175 
instance "fun" :: (type, ring_1) ring_1 .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

176 

38622  177 
instance "fun" :: (type, comm_ring_1) comm_ring_1 .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

178 

38622  179 
instance "fun" :: (type, ring_char_0) ring_char_0 .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

180 

d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

181 

38622  182 
text {* Ordereded structures *} 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

183 

46575  184 
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

185 
by default (auto simp add: le_fun_def intro: add_left_mono) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

186 

38622  187 
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

188 

46575  189 
instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

190 
by default (simp add: le_fun_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

191 

38622  192 
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add .. 
193 

194 
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add .. 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

195 

46575  196 
instance "fun" :: (type, ordered_semiring) ordered_semiring 
197 
by default 

48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

198 
(auto simp add: le_fun_def intro: mult_left_mono mult_right_mono) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

199 

46575  200 
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring 
201 
by default (fact mult_left_mono) 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

202 

38622  203 
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

204 

38622  205 
instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring .. 
206 

207 
instance "fun" :: (type, ordered_ring) ordered_ring .. 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

208 

38622  209 
instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring .. 
210 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

211 

38622  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 

19736  216 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

217 
end 
48173
c6a5a4336edf
etaexpanded occurences of algebraic functionals are simplified by default
haftmann
parents:
46575
diff
changeset

218 