src/HOL/Library/Function_Algebras.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 62376 85f38d5f8807
permissions -rw-r--r--
tuned equation
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
wenzelm@60500
     5
section \<open>Pointwise instantiation of functions to algebra type classes\<close>
avigad@16908
     6
haftmann@38622
     7
theory Function_Algebras
haftmann@30738
     8
imports Main
avigad@16908
     9
begin
avigad@16908
    10
wenzelm@60500
    11
text \<open>Pointwise operations\<close>
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
wenzelm@60500
    62
text \<open>Additive structures\<close>
haftmann@38622
    63
wenzelm@46575
    64
instance "fun" :: (type, semigroup_add) semigroup_add
wenzelm@60679
    65
  by standard (simp add: fun_eq_iff add.assoc)
avigad@16908
    66
wenzelm@46575
    67
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
wenzelm@60679
    68
  by standard (simp_all add: fun_eq_iff)
avigad@16908
    69
wenzelm@46575
    70
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
wenzelm@60679
    71
  by standard (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@60679
    74
  by standard (simp_all add: fun_eq_iff diff_diff_eq)
avigad@16908
    75
wenzelm@46575
    76
instance "fun" :: (type, monoid_add) monoid_add
wenzelm@60679
    77
  by standard (simp_all add: fun_eq_iff)
avigad@16908
    78
wenzelm@46575
    79
instance "fun" :: (type, comm_monoid_add) comm_monoid_add
wenzelm@60679
    80
  by standard 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@60679
    85
  by standard (simp_all add: fun_eq_iff)
avigad@16908
    86
wenzelm@46575
    87
instance "fun" :: (type, ab_group_add) ab_group_add
wenzelm@60679
    88
  by standard simp_all
haftmann@38622
    89
haftmann@38622
    90
wenzelm@60500
    91
text \<open>Multiplicative structures\<close>
avigad@16908
    92
wenzelm@46575
    93
instance "fun" :: (type, semigroup_mult) semigroup_mult
wenzelm@60679
    94
  by standard (simp add: fun_eq_iff mult.assoc)
haftmann@38622
    95
wenzelm@46575
    96
instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
wenzelm@60679
    97
  by standard (simp add: fun_eq_iff mult.commute)
avigad@16908
    98
wenzelm@46575
    99
instance "fun" :: (type, monoid_mult) monoid_mult
wenzelm@60679
   100
  by standard (simp_all add: fun_eq_iff)
haftmann@38622
   101
wenzelm@46575
   102
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
wenzelm@60679
   103
  by standard simp
haftmann@38622
   104
avigad@16908
   105
wenzelm@60500
   106
text \<open>Misc\<close>
haftmann@38622
   107
haftmann@38622
   108
instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
haftmann@38622
   109
wenzelm@46575
   110
instance "fun" :: (type, mult_zero) mult_zero
wenzelm@60679
   111
  by standard (simp_all add: fun_eq_iff)
avigad@16908
   112
wenzelm@46575
   113
instance "fun" :: (type, zero_neq_one) zero_neq_one
wenzelm@60679
   114
  by standard (simp add: fun_eq_iff)
wenzelm@19736
   115
avigad@16908
   116
wenzelm@60500
   117
text \<open>Ring structures\<close>
avigad@16908
   118
wenzelm@46575
   119
instance "fun" :: (type, semiring) semiring
wenzelm@60679
   120
  by standard (simp_all add: fun_eq_iff algebra_simps)
avigad@16908
   121
wenzelm@46575
   122
instance "fun" :: (type, comm_semiring) comm_semiring
wenzelm@60679
   123
  by standard (simp add: fun_eq_iff  algebra_simps)
avigad@16908
   124
haftmann@38622
   125
instance "fun" :: (type, semiring_0) semiring_0 ..
haftmann@38622
   126
haftmann@38622
   127
instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
avigad@16908
   128
haftmann@38622
   129
instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
avigad@16908
   130
haftmann@38622
   131
instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
avigad@16908
   132
haftmann@38622
   133
instance "fun" :: (type, semiring_1) semiring_1 ..
avigad@16908
   134
wenzelm@46575
   135
lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
haftmann@38622
   136
proof -
haftmann@38622
   137
  have comp: "comp = (\<lambda>f g x. f (g x))"
haftmann@38622
   138
    by (rule ext)+ simp
haftmann@38622
   139
  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
haftmann@38622
   140
    by (rule ext, rule ext) (fact plus_fun_def)
haftmann@38622
   141
  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   142
    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
haftmann@38622
   143
  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   144
    by (simp only: comp_funpow)
haftmann@38622
   145
  finally show ?thesis by (simp add: of_nat_def comp)
haftmann@38622
   146
qed
avigad@16908
   147
haftmann@48173
   148
lemma of_nat_fun_apply [simp]:
haftmann@48173
   149
  "of_nat n x = of_nat n"
haftmann@48173
   150
  by (simp add: of_nat_fun)
haftmann@48173
   151
haftmann@38622
   152
instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
avigad@16908
   153
haftmann@38622
   154
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
avigad@16908
   155
hoelzl@62376
   156
instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel
wenzelm@60679
   157
  by standard (auto simp add: times_fun_def algebra_simps)
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@60500
   179
text \<open>Ordered structures\<close>
avigad@16908
   180
wenzelm@46575
   181
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
wenzelm@60679
   182
  by standard (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
wenzelm@60679
   187
  by standard (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
hoelzl@62376
   191
instance "fun" :: (type, ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
hoelzl@62376
   192
haftmann@38622
   193
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
avigad@16908
   194
wenzelm@46575
   195
instance "fun" :: (type, ordered_semiring) ordered_semiring
wenzelm@60679
   196
  by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
avigad@16908
   197
hoelzl@62376
   198
instance "fun" :: (type, dioid) dioid
hoelzl@62376
   199
proof standard
hoelzl@62376
   200
  fix a b :: "'a \<Rightarrow> 'b"
hoelzl@62376
   201
  show "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
hoelzl@62376
   202
    unfolding le_fun_def plus_fun_def fun_eq_iff choice_iff[symmetric, of "\<lambda>x c. b x = a x + c"]
hoelzl@62376
   203
    by (intro arg_cong[where f=All] ext canonically_ordered_monoid_add_class.le_iff_add)
hoelzl@62376
   204
qed
hoelzl@62376
   205
wenzelm@46575
   206
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
wenzelm@60679
   207
  by standard (fact mult_left_mono)
avigad@16908
   208
haftmann@38622
   209
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
avigad@16908
   210
haftmann@38622
   211
instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
haftmann@38622
   212
haftmann@38622
   213
instance "fun" :: (type, ordered_ring) ordered_ring ..
avigad@16908
   214
haftmann@38622
   215
instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
haftmann@38622
   216
avigad@16908
   217
haftmann@38622
   218
lemmas func_plus = plus_fun_def
haftmann@38622
   219
lemmas func_zero = zero_fun_def
haftmann@38622
   220
lemmas func_times = times_fun_def
haftmann@38622
   221
lemmas func_one = one_fun_def
wenzelm@19736
   222
avigad@16908
   223
end
haftmann@48173
   224