src/HOL/Library/Function_Algebras.thy
author Christian Sternagel
Wed Aug 29 12:23:14 2012 +0900 (2012-08-29)
changeset 49083 01081bca31b6
parent 48173 c6a5a4336edf
child 51489 f738e6dbd844
permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
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@48173
    86
    (simp_all add: fun_eq_iff diff_minus)
avigad@16908
    87
wenzelm@46575
    88
instance "fun" :: (type, ab_group_add) ab_group_add
wenzelm@46575
    89
  by default (simp_all add: diff_minus)
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, ab_semigroup_idem_mult) ab_semigroup_idem_mult
haftmann@48173
   101
  by default (simp add: fun_eq_iff)
haftmann@38622
   102
wenzelm@46575
   103
instance "fun" :: (type, monoid_mult) monoid_mult
haftmann@48173
   104
  by default (simp_all add: fun_eq_iff)
haftmann@38622
   105
wenzelm@46575
   106
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
wenzelm@46575
   107
  by default simp
haftmann@38622
   108
avigad@16908
   109
haftmann@38622
   110
text {* Misc *}
haftmann@38622
   111
haftmann@38622
   112
instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
haftmann@38622
   113
wenzelm@46575
   114
instance "fun" :: (type, mult_zero) mult_zero
haftmann@48173
   115
  by default (simp_all add: fun_eq_iff)
avigad@16908
   116
wenzelm@46575
   117
instance "fun" :: (type, zero_neq_one) zero_neq_one
haftmann@48173
   118
  by default (simp add: fun_eq_iff)
wenzelm@19736
   119
avigad@16908
   120
haftmann@38622
   121
text {* Ring structures *}
avigad@16908
   122
wenzelm@46575
   123
instance "fun" :: (type, semiring) semiring
haftmann@48173
   124
  by default (simp_all add: fun_eq_iff algebra_simps)
avigad@16908
   125
wenzelm@46575
   126
instance "fun" :: (type, comm_semiring) comm_semiring
haftmann@48173
   127
  by default (simp add: fun_eq_iff  algebra_simps)
avigad@16908
   128
haftmann@38622
   129
instance "fun" :: (type, semiring_0) semiring_0 ..
haftmann@38622
   130
haftmann@38622
   131
instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
avigad@16908
   132
haftmann@38622
   133
instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
avigad@16908
   134
haftmann@38622
   135
instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
avigad@16908
   136
haftmann@38622
   137
instance "fun" :: (type, semiring_1) semiring_1 ..
avigad@16908
   138
wenzelm@46575
   139
lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
haftmann@38622
   140
proof -
haftmann@38622
   141
  have comp: "comp = (\<lambda>f g x. f (g x))"
haftmann@38622
   142
    by (rule ext)+ simp
haftmann@38622
   143
  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
haftmann@38622
   144
    by (rule ext, rule ext) (fact plus_fun_def)
haftmann@38622
   145
  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   146
    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
haftmann@38622
   147
  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   148
    by (simp only: comp_funpow)
haftmann@38622
   149
  finally show ?thesis by (simp add: of_nat_def comp)
haftmann@38622
   150
qed
avigad@16908
   151
haftmann@48173
   152
lemma of_nat_fun_apply [simp]:
haftmann@48173
   153
  "of_nat n x = of_nat n"
haftmann@48173
   154
  by (simp add: of_nat_fun)
haftmann@48173
   155
haftmann@38622
   156
instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
avigad@16908
   157
haftmann@38622
   158
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
avigad@16908
   159
haftmann@38622
   160
instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
avigad@16908
   161
wenzelm@46575
   162
instance "fun" :: (type, semiring_char_0) semiring_char_0
wenzelm@46575
   163
proof
haftmann@38622
   164
  from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
haftmann@38622
   165
    by (rule inj_fun)
haftmann@38622
   166
  then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
haftmann@38622
   167
    by (simp add: of_nat_fun)
haftmann@38622
   168
  then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
haftmann@38622
   169
qed
avigad@16908
   170
haftmann@38622
   171
instance "fun" :: (type, ring) ring ..
avigad@16908
   172
haftmann@38622
   173
instance "fun" :: (type, comm_ring) comm_ring ..
avigad@16908
   174
haftmann@38622
   175
instance "fun" :: (type, ring_1) ring_1 ..
avigad@16908
   176
haftmann@38622
   177
instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
avigad@16908
   178
haftmann@38622
   179
instance "fun" :: (type, ring_char_0) ring_char_0 ..
avigad@16908
   180
avigad@16908
   181
haftmann@38622
   182
text {* Ordereded structures *}
avigad@16908
   183
wenzelm@46575
   184
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
haftmann@48173
   185
  by default (auto simp add: le_fun_def intro: add_left_mono)
avigad@16908
   186
haftmann@38622
   187
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
avigad@16908
   188
wenzelm@46575
   189
instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
haftmann@48173
   190
  by default (simp add: le_fun_def)
avigad@16908
   191
haftmann@38622
   192
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
haftmann@38622
   193
haftmann@38622
   194
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
avigad@16908
   195
wenzelm@46575
   196
instance "fun" :: (type, ordered_semiring) ordered_semiring
wenzelm@46575
   197
  by default
haftmann@48173
   198
    (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
avigad@16908
   199
wenzelm@46575
   200
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
wenzelm@46575
   201
  by default (fact mult_left_mono)
avigad@16908
   202
haftmann@38622
   203
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
avigad@16908
   204
haftmann@38622
   205
instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
haftmann@38622
   206
haftmann@38622
   207
instance "fun" :: (type, ordered_ring) ordered_ring ..
avigad@16908
   208
haftmann@38622
   209
instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
haftmann@38622
   210
avigad@16908
   211
haftmann@38622
   212
lemmas func_plus = plus_fun_def
haftmann@38622
   213
lemmas func_zero = zero_fun_def
haftmann@38622
   214
lemmas func_times = times_fun_def
haftmann@38622
   215
lemmas func_one = one_fun_def
wenzelm@19736
   216
avigad@16908
   217
end
haftmann@48173
   218