src/HOL/Library/Function_Algebras.thy
author wenzelm
Fri May 02 19:28:32 2014 +0200 (2014-05-02)
changeset 56828 08041569357e
parent 54230 b1d955791529
child 58881 b9556a055632
permissions -rw-r--r--
tuned spelling;
haftmann@38622
     1
(*  Title:      HOL/Library/Function_Algebras.thy
haftmann@38622
     2
    Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
avigad@16908
     3
*)
avigad@16908
     4
haftmann@38622
     5
header {* Pointwise instantiation of functions to algebra type classes *}
avigad@16908
     6
haftmann@38622
     7
theory Function_Algebras
haftmann@30738
     8
imports Main
avigad@16908
     9
begin
avigad@16908
    10
haftmann@38622
    11
text {* Pointwise operations *}
haftmann@25594
    12
haftmann@25594
    13
instantiation "fun" :: (type, plus) plus
haftmann@25594
    14
begin
avigad@16908
    15
wenzelm@46575
    16
definition "f + g = (\<lambda>x. f x + g x)"
haftmann@25594
    17
instance ..
haftmann@25594
    18
haftmann@25594
    19
end
haftmann@25594
    20
haftmann@48173
    21
lemma plus_fun_apply [simp]:
haftmann@48173
    22
  "(f + g) x = f x + g x"
haftmann@48173
    23
  by (simp add: plus_fun_def)
haftmann@48173
    24
haftmann@38622
    25
instantiation "fun" :: (type, zero) zero
haftmann@38622
    26
begin
haftmann@38622
    27
wenzelm@46575
    28
definition "0 = (\<lambda>x. 0)"
haftmann@38622
    29
instance ..
haftmann@38622
    30
haftmann@38622
    31
end
haftmann@25594
    32
haftmann@48173
    33
lemma zero_fun_apply [simp]:
haftmann@48173
    34
  "0 x = 0"
haftmann@48173
    35
  by (simp add: zero_fun_def)
haftmann@48173
    36
haftmann@25594
    37
instantiation "fun" :: (type, times) times
haftmann@25594
    38
begin
haftmann@25594
    39
wenzelm@46575
    40
definition "f * g = (\<lambda>x. f x * g x)"
haftmann@25594
    41
instance ..
haftmann@25594
    42
haftmann@25594
    43
end
haftmann@25594
    44
haftmann@48173
    45
lemma times_fun_apply [simp]:
haftmann@48173
    46
  "(f * g) x = f x * g x"
haftmann@48173
    47
  by (simp add: times_fun_def)
haftmann@48173
    48
haftmann@25594
    49
instantiation "fun" :: (type, one) one
haftmann@25594
    50
begin
haftmann@25594
    51
wenzelm@46575
    52
definition "1 = (\<lambda>x. 1)"
haftmann@25594
    53
instance ..
haftmann@25594
    54
haftmann@25594
    55
end
avigad@16908
    56
haftmann@48173
    57
lemma one_fun_apply [simp]:
haftmann@48173
    58
  "1 x = 1"
haftmann@48173
    59
  by (simp add: one_fun_def)
haftmann@48173
    60
haftmann@38622
    61
haftmann@38622
    62
text {* Additive structures *}
haftmann@38622
    63
wenzelm@46575
    64
instance "fun" :: (type, semigroup_add) semigroup_add
haftmann@48173
    65
  by default (simp add: fun_eq_iff add.assoc)
avigad@16908
    66
wenzelm@46575
    67
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
haftmann@48173
    68
  by default (simp_all add: fun_eq_iff)
avigad@16908
    69
wenzelm@46575
    70
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
haftmann@48173
    71
  by default (simp add: fun_eq_iff add.commute)
avigad@16908
    72
wenzelm@46575
    73
instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
wenzelm@46575
    74
  by default simp
avigad@16908
    75
wenzelm@46575
    76
instance "fun" :: (type, monoid_add) monoid_add
haftmann@48173
    77
  by default (simp_all add: fun_eq_iff)
avigad@16908
    78
wenzelm@46575
    79
instance "fun" :: (type, comm_monoid_add) comm_monoid_add
wenzelm@46575
    80
  by default simp
haftmann@38622
    81
haftmann@38622
    82
instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
avigad@16908
    83
wenzelm@46575
    84
instance "fun" :: (type, group_add) group_add
wenzelm@46575
    85
  by default
haftmann@54230
    86
    (simp_all add: fun_eq_iff)
avigad@16908
    87
wenzelm@46575
    88
instance "fun" :: (type, ab_group_add) ab_group_add
haftmann@54230
    89
  by default simp_all
haftmann@38622
    90
haftmann@38622
    91
haftmann@38622
    92
text {* Multiplicative structures *}
avigad@16908
    93
wenzelm@46575
    94
instance "fun" :: (type, semigroup_mult) semigroup_mult
haftmann@48173
    95
  by default (simp add: fun_eq_iff mult.assoc)
haftmann@38622
    96
wenzelm@46575
    97
instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
haftmann@48173
    98
  by default (simp add: fun_eq_iff mult.commute)
avigad@16908
    99
wenzelm@46575
   100
instance "fun" :: (type, monoid_mult) monoid_mult
haftmann@48173
   101
  by default (simp_all add: fun_eq_iff)
haftmann@38622
   102
wenzelm@46575
   103
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
wenzelm@46575
   104
  by default simp
haftmann@38622
   105
avigad@16908
   106
haftmann@38622
   107
text {* Misc *}
haftmann@38622
   108
haftmann@38622
   109
instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
haftmann@38622
   110
wenzelm@46575
   111
instance "fun" :: (type, mult_zero) mult_zero
haftmann@48173
   112
  by default (simp_all add: fun_eq_iff)
avigad@16908
   113
wenzelm@46575
   114
instance "fun" :: (type, zero_neq_one) zero_neq_one
haftmann@48173
   115
  by default (simp add: fun_eq_iff)
wenzelm@19736
   116
avigad@16908
   117
haftmann@38622
   118
text {* Ring structures *}
avigad@16908
   119
wenzelm@46575
   120
instance "fun" :: (type, semiring) semiring
haftmann@48173
   121
  by default (simp_all add: fun_eq_iff algebra_simps)
avigad@16908
   122
wenzelm@46575
   123
instance "fun" :: (type, comm_semiring) comm_semiring
haftmann@48173
   124
  by default (simp add: fun_eq_iff  algebra_simps)
avigad@16908
   125
haftmann@38622
   126
instance "fun" :: (type, semiring_0) semiring_0 ..
haftmann@38622
   127
haftmann@38622
   128
instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
avigad@16908
   129
haftmann@38622
   130
instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
avigad@16908
   131
haftmann@38622
   132
instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
avigad@16908
   133
haftmann@38622
   134
instance "fun" :: (type, semiring_1) semiring_1 ..
avigad@16908
   135
wenzelm@46575
   136
lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
haftmann@38622
   137
proof -
haftmann@38622
   138
  have comp: "comp = (\<lambda>f g x. f (g x))"
haftmann@38622
   139
    by (rule ext)+ simp
haftmann@38622
   140
  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
haftmann@38622
   141
    by (rule ext, rule ext) (fact plus_fun_def)
haftmann@38622
   142
  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   143
    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
haftmann@38622
   144
  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   145
    by (simp only: comp_funpow)
haftmann@38622
   146
  finally show ?thesis by (simp add: of_nat_def comp)
haftmann@38622
   147
qed
avigad@16908
   148
haftmann@48173
   149
lemma of_nat_fun_apply [simp]:
haftmann@48173
   150
  "of_nat n x = of_nat n"
haftmann@48173
   151
  by (simp add: of_nat_fun)
haftmann@48173
   152
haftmann@38622
   153
instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
avigad@16908
   154
haftmann@38622
   155
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
avigad@16908
   156
haftmann@38622
   157
instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
avigad@16908
   158
wenzelm@46575
   159
instance "fun" :: (type, semiring_char_0) semiring_char_0
wenzelm@46575
   160
proof
haftmann@38622
   161
  from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
haftmann@38622
   162
    by (rule inj_fun)
haftmann@38622
   163
  then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
haftmann@38622
   164
    by (simp add: of_nat_fun)
haftmann@38622
   165
  then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
haftmann@38622
   166
qed
avigad@16908
   167
haftmann@38622
   168
instance "fun" :: (type, ring) ring ..
avigad@16908
   169
haftmann@38622
   170
instance "fun" :: (type, comm_ring) comm_ring ..
avigad@16908
   171
haftmann@38622
   172
instance "fun" :: (type, ring_1) ring_1 ..
avigad@16908
   173
haftmann@38622
   174
instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
avigad@16908
   175
haftmann@38622
   176
instance "fun" :: (type, ring_char_0) ring_char_0 ..
avigad@16908
   177
avigad@16908
   178
wenzelm@56828
   179
text {* Ordered structures *}
avigad@16908
   180
wenzelm@46575
   181
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
haftmann@48173
   182
  by default (auto simp add: le_fun_def intro: add_left_mono)
avigad@16908
   183
haftmann@38622
   184
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
avigad@16908
   185
wenzelm@46575
   186
instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
haftmann@48173
   187
  by default (simp add: le_fun_def)
avigad@16908
   188
haftmann@38622
   189
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
haftmann@38622
   190
haftmann@38622
   191
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
avigad@16908
   192
wenzelm@46575
   193
instance "fun" :: (type, ordered_semiring) ordered_semiring
wenzelm@46575
   194
  by default
haftmann@48173
   195
    (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
avigad@16908
   196
wenzelm@46575
   197
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
wenzelm@46575
   198
  by default (fact mult_left_mono)
avigad@16908
   199
haftmann@38622
   200
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
avigad@16908
   201
haftmann@38622
   202
instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
haftmann@38622
   203
haftmann@38622
   204
instance "fun" :: (type, ordered_ring) ordered_ring ..
avigad@16908
   205
haftmann@38622
   206
instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
haftmann@38622
   207
avigad@16908
   208
haftmann@38622
   209
lemmas func_plus = plus_fun_def
haftmann@38622
   210
lemmas func_zero = zero_fun_def
haftmann@38622
   211
lemmas func_times = times_fun_def
haftmann@38622
   212
lemmas func_one = one_fun_def
wenzelm@19736
   213
avigad@16908
   214
end
haftmann@48173
   215