author  nipkow 
Tue, 07 Sep 2010 10:05:19 +0200  
changeset 39198  f967a16dfcdd 
parent 38642  8fa437809c67 
child 39302  d7728f65b353 
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 

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

19 
instance .. 

20 

21 
end 

22 

38622  23 
instantiation "fun" :: (type, zero) zero 
24 
begin 

25 

25594  26 
definition 
38622  27 
"0 = (\<lambda>x. 0)" 
28 

29 
instance .. 

30 

31 
end 

25594  32 

33 
instantiation "fun" :: (type, times) times 

34 
begin 

35 

36 
definition 

38622  37 
"f * g = (\<lambda>x. f x * g x)" 
25594  38 

39 
instance .. 

40 

41 
end 

42 

43 
instantiation "fun" :: (type, one) one 

44 
begin 

45 

46 
definition 

38622  47 
"1 = (\<lambda>x. 1)" 
25594  48 

49 
instance .. 

50 

51 
end 

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

52 

38622  53 

54 
text {* Additive structures *} 

55 

56 
instance "fun" :: (type, semigroup_add) semigroup_add proof 

57 
qed (simp add: plus_fun_def add.assoc) 

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

58 

38622  59 
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof 
39198  60 
qed (simp_all add: plus_fun_def ext_iff) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

61 

38622  62 
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof 
63 
qed (simp add: plus_fun_def add.commute) 

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

64 

38622  65 
instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof 
66 
qed simp 

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

67 

38622  68 
instance "fun" :: (type, monoid_add) monoid_add proof 
69 
qed (simp_all add: plus_fun_def zero_fun_def) 

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

70 

38622  71 
instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof 
72 
qed simp 

73 

74 
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

75 

38622  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) 

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

78 

38622  79 
instance "fun" :: (type, ab_group_add) ab_group_add proof 
80 
qed (simp_all add: diff_minus) 

81 

82 

83 
text {* Multiplicative structures *} 

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

84 

38622  85 
instance "fun" :: (type, semigroup_mult) semigroup_mult proof 
86 
qed (simp add: times_fun_def mult.assoc) 

87 

88 
instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof 

89 
qed (simp add: times_fun_def mult.commute) 

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

90 

38622  91 
instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof 
92 
qed (simp add: times_fun_def) 

93 

94 
instance "fun" :: (type, monoid_mult) monoid_mult proof 

95 
qed (simp_all add: times_fun_def one_fun_def) 

96 

97 
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof 

98 
qed simp 

99 

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

100 

38622  101 
text {* Misc *} 
102 

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

104 

105 
instance "fun" :: (type, mult_zero) mult_zero proof 

106 
qed (simp_all add: zero_fun_def times_fun_def) 

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

107 

38622  108 
instance "fun" :: (type, zero_neq_one) zero_neq_one proof 
39198  109 
qed (simp add: zero_fun_def one_fun_def ext_iff) 
19736  110 

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

111 

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

113 

38622  114 
instance "fun" :: (type, semiring) semiring proof 
115 
qed (simp_all add: plus_fun_def times_fun_def algebra_simps) 

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

116 

38622  117 
instance "fun" :: (type, comm_semiring) comm_semiring proof 
118 
qed (simp add: plus_fun_def times_fun_def algebra_simps) 

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

119 

38622  120 
instance "fun" :: (type, semiring_0) semiring_0 .. 
121 

122 
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

123 

38622  124 
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

125 

38622  126 
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

127 

38622  128 
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

129 

38622  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 

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

143 

38622  144 
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

145 

38622  146 
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

147 

38622  148 
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

149 

38622  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 

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

157 

38622  158 
instance "fun" :: (type, ring) ring .. 
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_ring) comm_ring .. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

161 

38622  162 
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

163 

38622  164 
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

165 

38622  166 
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

167 

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

168 

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

170 

38622  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) 

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

173 

38622  174 
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

175 

38622  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) 

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

178 

38622  179 
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add .. 
180 

181 
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

182 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
38622
diff
changeset

183 
instance "fun" :: (type, ordered_semiring) ordered_semiring proof 
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
38622
diff
changeset

184 
qed (auto simp add: zero_fun_def times_fun_def 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

185 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
38622
diff
changeset

186 
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof 
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
38622
diff
changeset

187 
qed (fact mult_left_mono) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

188 

38622  189 
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

190 

38622  191 
instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring .. 
192 

193 
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

194 

38622  195 
instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring .. 
196 

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

197 

38622  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 

19736  202 

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

203 
end 