src/HOL/Library/Function_Algebras.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 48173 c6a5a4336edf
child 51489 f738e6dbd844
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/Function_Algebras.thy
     2     Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
     3 *)
     4 
     5 header {* Pointwise instantiation of functions to algebra type classes *}
     6 
     7 theory Function_Algebras
     8 imports Main
     9 begin
    10 
    11 text {* Pointwise operations *}
    12 
    13 instantiation "fun" :: (type, plus) plus
    14 begin
    15 
    16 definition "f + g = (\<lambda>x. f x + g x)"
    17 instance ..
    18 
    19 end
    20 
    21 lemma plus_fun_apply [simp]:
    22   "(f + g) x = f x + g x"
    23   by (simp add: plus_fun_def)
    24 
    25 instantiation "fun" :: (type, zero) zero
    26 begin
    27 
    28 definition "0 = (\<lambda>x. 0)"
    29 instance ..
    30 
    31 end
    32 
    33 lemma zero_fun_apply [simp]:
    34   "0 x = 0"
    35   by (simp add: zero_fun_def)
    36 
    37 instantiation "fun" :: (type, times) times
    38 begin
    39 
    40 definition "f * g = (\<lambda>x. f x * g x)"
    41 instance ..
    42 
    43 end
    44 
    45 lemma times_fun_apply [simp]:
    46   "(f * g) x = f x * g x"
    47   by (simp add: times_fun_def)
    48 
    49 instantiation "fun" :: (type, one) one
    50 begin
    51 
    52 definition "1 = (\<lambda>x. 1)"
    53 instance ..
    54 
    55 end
    56 
    57 lemma one_fun_apply [simp]:
    58   "1 x = 1"
    59   by (simp add: one_fun_def)
    60 
    61 
    62 text {* Additive structures *}
    63 
    64 instance "fun" :: (type, semigroup_add) semigroup_add
    65   by default (simp add: fun_eq_iff add.assoc)
    66 
    67 instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
    68   by default (simp_all add: fun_eq_iff)
    69 
    70 instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
    71   by default (simp add: fun_eq_iff add.commute)
    72 
    73 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    74   by default simp
    75 
    76 instance "fun" :: (type, monoid_add) monoid_add
    77   by default (simp_all add: fun_eq_iff)
    78 
    79 instance "fun" :: (type, comm_monoid_add) comm_monoid_add
    80   by default simp
    81 
    82 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    83 
    84 instance "fun" :: (type, group_add) group_add
    85   by default
    86     (simp_all add: fun_eq_iff diff_minus)
    87 
    88 instance "fun" :: (type, ab_group_add) ab_group_add
    89   by default (simp_all add: diff_minus)
    90 
    91 
    92 text {* Multiplicative structures *}
    93 
    94 instance "fun" :: (type, semigroup_mult) semigroup_mult
    95   by default (simp add: fun_eq_iff mult.assoc)
    96 
    97 instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
    98   by default (simp add: fun_eq_iff mult.commute)
    99 
   100 instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
   101   by default (simp add: fun_eq_iff)
   102 
   103 instance "fun" :: (type, monoid_mult) monoid_mult
   104   by default (simp_all add: fun_eq_iff)
   105 
   106 instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
   107   by default simp
   108 
   109 
   110 text {* Misc *}
   111 
   112 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
   113 
   114 instance "fun" :: (type, mult_zero) mult_zero
   115   by default (simp_all add: fun_eq_iff)
   116 
   117 instance "fun" :: (type, zero_neq_one) zero_neq_one
   118   by default (simp add: fun_eq_iff)
   119 
   120 
   121 text {* Ring structures *}
   122 
   123 instance "fun" :: (type, semiring) semiring
   124   by default (simp_all add: fun_eq_iff algebra_simps)
   125 
   126 instance "fun" :: (type, comm_semiring) comm_semiring
   127   by default (simp add: fun_eq_iff  algebra_simps)
   128 
   129 instance "fun" :: (type, semiring_0) semiring_0 ..
   130 
   131 instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
   132 
   133 instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
   134 
   135 instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
   136 
   137 instance "fun" :: (type, semiring_1) semiring_1 ..
   138 
   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
   151 
   152 lemma of_nat_fun_apply [simp]:
   153   "of_nat n x = of_nat n"
   154   by (simp add: of_nat_fun)
   155 
   156 instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
   157 
   158 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
   159 
   160 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
   161 
   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
   170 
   171 instance "fun" :: (type, ring) ring ..
   172 
   173 instance "fun" :: (type, comm_ring) comm_ring ..
   174 
   175 instance "fun" :: (type, ring_1) ring_1 ..
   176 
   177 instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
   178 
   179 instance "fun" :: (type, ring_char_0) ring_char_0 ..
   180 
   181 
   182 text {* Ordereded structures *}
   183 
   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)
   186 
   187 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   188 
   189 instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
   190   by default (simp add: le_fun_def)
   191 
   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 ..
   195 
   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)
   199 
   200 instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
   201   by default (fact mult_left_mono)
   202 
   203 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
   204 
   205 instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
   206 
   207 instance "fun" :: (type, ordered_ring) ordered_ring ..
   208 
   209 instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
   210 
   211 
   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
   216 
   217 end
   218