src/HOL/Library/Function_Algebras.thy
changeset 38622 86fc906dcd86
parent 35267 8dfd816713c6
child 38642 8fa437809c67
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Fri Aug 20 17:48:30 2010 +0200
     1.3 @@ -0,0 +1,207 @@
     1.4 +(*  Title:      HOL/Library/Function_Algebras.thy
     1.5 +    Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
     1.6 +*)
     1.7 +
     1.8 +header {* Pointwise instantiation of functions to algebra type classes *}
     1.9 +
    1.10 +theory Function_Algebras
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +text {* Pointwise operations *}
    1.15 +
    1.16 +instantiation "fun" :: (type, plus) plus
    1.17 +begin
    1.18 +
    1.19 +definition
    1.20 +  "f + g = (\<lambda>x. f x + g x)"
    1.21 +
    1.22 +instance ..
    1.23 +
    1.24 +end
    1.25 +
    1.26 +instantiation "fun" :: (type, zero) zero
    1.27 +begin
    1.28 +
    1.29 +definition
    1.30 +  "0 = (\<lambda>x. 0)"
    1.31 +
    1.32 +instance ..
    1.33 +
    1.34 +end
    1.35 +
    1.36 +instantiation "fun" :: (type, times) times
    1.37 +begin
    1.38 +
    1.39 +definition
    1.40 +  "f * g = (\<lambda>x. f x * g x)"
    1.41 +
    1.42 +instance ..
    1.43 +
    1.44 +end
    1.45 +
    1.46 +instantiation "fun" :: (type, one) one
    1.47 +begin
    1.48 +
    1.49 +definition
    1.50 +  "1 = (\<lambda>x. 1)"
    1.51 +
    1.52 +instance ..
    1.53 +
    1.54 +end
    1.55 +
    1.56 +
    1.57 +text {* Additive structures *}
    1.58 +
    1.59 +instance "fun" :: (type, semigroup_add) semigroup_add proof
    1.60 +qed (simp add: plus_fun_def add.assoc)
    1.61 +
    1.62 +instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
    1.63 +qed (simp_all add: plus_fun_def expand_fun_eq)
    1.64 +
    1.65 +instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
    1.66 +qed (simp add: plus_fun_def add.commute)
    1.67 +
    1.68 +instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
    1.69 +qed simp
    1.70 +
    1.71 +instance "fun" :: (type, monoid_add) monoid_add proof
    1.72 +qed (simp_all add: plus_fun_def zero_fun_def)
    1.73 +
    1.74 +instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
    1.75 +qed simp
    1.76 +
    1.77 +instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    1.78 +
    1.79 +instance "fun" :: (type, group_add) group_add proof
    1.80 +qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
    1.81 +
    1.82 +instance "fun" :: (type, ab_group_add) ab_group_add proof
    1.83 +qed (simp_all add: diff_minus)
    1.84 +
    1.85 +
    1.86 +text {* Multiplicative structures *}
    1.87 +
    1.88 +instance "fun" :: (type, semigroup_mult) semigroup_mult proof
    1.89 +qed (simp add: times_fun_def mult.assoc)
    1.90 +
    1.91 +instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
    1.92 +qed (simp add: times_fun_def mult.commute)
    1.93 +
    1.94 +instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
    1.95 +qed (simp add: times_fun_def)
    1.96 +
    1.97 +instance "fun" :: (type, monoid_mult) monoid_mult proof
    1.98 +qed (simp_all add: times_fun_def one_fun_def)
    1.99 +
   1.100 +instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
   1.101 +qed simp
   1.102 +
   1.103 +
   1.104 +text {* Misc *}
   1.105 +
   1.106 +instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
   1.107 +
   1.108 +instance "fun" :: (type, mult_zero) mult_zero proof
   1.109 +qed (simp_all add: zero_fun_def times_fun_def)
   1.110 +
   1.111 +instance "fun" :: (type, mult_mono) mult_mono proof
   1.112 +qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
   1.113 +
   1.114 +instance "fun" :: (type, mult_mono1) mult_mono1 proof
   1.115 +qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
   1.116 +
   1.117 +instance "fun" :: (type, zero_neq_one) zero_neq_one proof
   1.118 +qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
   1.119 +
   1.120 +
   1.121 +text {* Ring structures *}
   1.122 +
   1.123 +instance "fun" :: (type, semiring) semiring proof
   1.124 +qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
   1.125 +
   1.126 +instance "fun" :: (type, comm_semiring) comm_semiring proof
   1.127 +qed (simp add: plus_fun_def times_fun_def algebra_simps)
   1.128 +
   1.129 +instance "fun" :: (type, semiring_0) semiring_0 ..
   1.130 +
   1.131 +instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
   1.132 +
   1.133 +instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
   1.134 +
   1.135 +instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
   1.136 +
   1.137 +instance "fun" :: (type, semiring_1) semiring_1 ..
   1.138 +
   1.139 +lemma of_nat_fun:
   1.140 +  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
   1.141 +proof -
   1.142 +  have comp: "comp = (\<lambda>f g x. f (g x))"
   1.143 +    by (rule ext)+ simp
   1.144 +  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
   1.145 +    by (rule ext, rule ext) (fact plus_fun_def)
   1.146 +  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
   1.147 +    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
   1.148 +  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
   1.149 +    by (simp only: comp_funpow)
   1.150 +  finally show ?thesis by (simp add: of_nat_def comp)
   1.151 +qed
   1.152 +
   1.153 +instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
   1.154 +
   1.155 +instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
   1.156 +
   1.157 +instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
   1.158 +
   1.159 +instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
   1.160 +  from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
   1.161 +    by (rule inj_fun)
   1.162 +  then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
   1.163 +    by (simp add: of_nat_fun)
   1.164 +  then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
   1.165 +qed
   1.166 +
   1.167 +instance "fun" :: (type, ring) ring ..
   1.168 +
   1.169 +instance "fun" :: (type, comm_ring) comm_ring ..
   1.170 +
   1.171 +instance "fun" :: (type, ring_1) ring_1 ..
   1.172 +
   1.173 +instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
   1.174 +
   1.175 +instance "fun" :: (type, ring_char_0) ring_char_0 ..
   1.176 +
   1.177 +
   1.178 +text {* Ordereded structures *}
   1.179 +
   1.180 +instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
   1.181 +qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
   1.182 +
   1.183 +instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   1.184 +
   1.185 +instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
   1.186 +qed (simp add: plus_fun_def le_fun_def)
   1.187 +
   1.188 +instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
   1.189 +
   1.190 +instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
   1.191 +
   1.192 +instance "fun" :: (type, ordered_semiring) ordered_semiring ..
   1.193 +
   1.194 +instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
   1.195 +
   1.196 +instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
   1.197 +
   1.198 +instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
   1.199 +
   1.200 +instance "fun" :: (type, ordered_ring) ordered_ring ..
   1.201 +
   1.202 +instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
   1.203 +
   1.204 +
   1.205 +lemmas func_plus = plus_fun_def
   1.206 +lemmas func_zero = zero_fun_def
   1.207 +lemmas func_times = times_fun_def
   1.208 +lemmas func_one = one_fun_def
   1.209 +
   1.210 +end