src/HOL/Library/Function_Algebras.thy
author wenzelm
Tue Feb 21 16:48:10 2012 +0100 (2012-02-21)
changeset 46575 f1e387195a56
parent 39302 d7728f65b353
child 48173 c6a5a4336edf
permissions -rw-r--r--
misc tuning;
more indentation;
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@38622
    21
instantiation "fun" :: (type, zero) zero
haftmann@38622
    22
begin
haftmann@38622
    23
wenzelm@46575
    24
definition "0 = (\<lambda>x. 0)"
haftmann@38622
    25
instance ..
haftmann@38622
    26
haftmann@38622
    27
end
haftmann@25594
    28
haftmann@25594
    29
instantiation "fun" :: (type, times) times
haftmann@25594
    30
begin
haftmann@25594
    31
wenzelm@46575
    32
definition "f * g = (\<lambda>x. f x * g x)"
haftmann@25594
    33
instance ..
haftmann@25594
    34
haftmann@25594
    35
end
haftmann@25594
    36
haftmann@25594
    37
instantiation "fun" :: (type, one) one
haftmann@25594
    38
begin
haftmann@25594
    39
wenzelm@46575
    40
definition "1 = (\<lambda>x. 1)"
haftmann@25594
    41
instance ..
haftmann@25594
    42
haftmann@25594
    43
end
avigad@16908
    44
haftmann@38622
    45
haftmann@38622
    46
text {* Additive structures *}
haftmann@38622
    47
wenzelm@46575
    48
instance "fun" :: (type, semigroup_add) semigroup_add
wenzelm@46575
    49
  by default (simp add: plus_fun_def add.assoc)
avigad@16908
    50
wenzelm@46575
    51
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
wenzelm@46575
    52
  by default (simp_all add: plus_fun_def fun_eq_iff)
avigad@16908
    53
wenzelm@46575
    54
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
wenzelm@46575
    55
  by default (simp add: plus_fun_def add.commute)
avigad@16908
    56
wenzelm@46575
    57
instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
wenzelm@46575
    58
  by default simp
avigad@16908
    59
wenzelm@46575
    60
instance "fun" :: (type, monoid_add) monoid_add
wenzelm@46575
    61
  by default (simp_all add: plus_fun_def zero_fun_def)
avigad@16908
    62
wenzelm@46575
    63
instance "fun" :: (type, comm_monoid_add) comm_monoid_add
wenzelm@46575
    64
  by default simp
haftmann@38622
    65
haftmann@38622
    66
instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
avigad@16908
    67
wenzelm@46575
    68
instance "fun" :: (type, group_add) group_add
wenzelm@46575
    69
  by default
wenzelm@46575
    70
    (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
avigad@16908
    71
wenzelm@46575
    72
instance "fun" :: (type, ab_group_add) ab_group_add
wenzelm@46575
    73
  by default (simp_all add: diff_minus)
haftmann@38622
    74
haftmann@38622
    75
haftmann@38622
    76
text {* Multiplicative structures *}
avigad@16908
    77
wenzelm@46575
    78
instance "fun" :: (type, semigroup_mult) semigroup_mult
wenzelm@46575
    79
  by default (simp add: times_fun_def mult.assoc)
haftmann@38622
    80
wenzelm@46575
    81
instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
wenzelm@46575
    82
  by default (simp add: times_fun_def mult.commute)
avigad@16908
    83
wenzelm@46575
    84
instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
wenzelm@46575
    85
  by default (simp add: times_fun_def)
haftmann@38622
    86
wenzelm@46575
    87
instance "fun" :: (type, monoid_mult) monoid_mult
wenzelm@46575
    88
  by default (simp_all add: times_fun_def one_fun_def)
haftmann@38622
    89
wenzelm@46575
    90
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
wenzelm@46575
    91
  by default simp
haftmann@38622
    92
avigad@16908
    93
haftmann@38622
    94
text {* Misc *}
haftmann@38622
    95
haftmann@38622
    96
instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
haftmann@38622
    97
wenzelm@46575
    98
instance "fun" :: (type, mult_zero) mult_zero
wenzelm@46575
    99
  by default (simp_all add: zero_fun_def times_fun_def)
avigad@16908
   100
wenzelm@46575
   101
instance "fun" :: (type, zero_neq_one) zero_neq_one
wenzelm@46575
   102
  by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
wenzelm@19736
   103
avigad@16908
   104
haftmann@38622
   105
text {* Ring structures *}
avigad@16908
   106
wenzelm@46575
   107
instance "fun" :: (type, semiring) semiring
wenzelm@46575
   108
  by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
avigad@16908
   109
wenzelm@46575
   110
instance "fun" :: (type, comm_semiring) comm_semiring
wenzelm@46575
   111
  by default (simp add: plus_fun_def times_fun_def algebra_simps)
avigad@16908
   112
haftmann@38622
   113
instance "fun" :: (type, semiring_0) semiring_0 ..
haftmann@38622
   114
haftmann@38622
   115
instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
avigad@16908
   116
haftmann@38622
   117
instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
avigad@16908
   118
haftmann@38622
   119
instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
avigad@16908
   120
haftmann@38622
   121
instance "fun" :: (type, semiring_1) semiring_1 ..
avigad@16908
   122
wenzelm@46575
   123
lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
haftmann@38622
   124
proof -
haftmann@38622
   125
  have comp: "comp = (\<lambda>f g x. f (g x))"
haftmann@38622
   126
    by (rule ext)+ simp
haftmann@38622
   127
  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
haftmann@38622
   128
    by (rule ext, rule ext) (fact plus_fun_def)
haftmann@38622
   129
  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   130
    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
haftmann@38622
   131
  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   132
    by (simp only: comp_funpow)
haftmann@38622
   133
  finally show ?thesis by (simp add: of_nat_def comp)
haftmann@38622
   134
qed
avigad@16908
   135
haftmann@38622
   136
instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
avigad@16908
   137
haftmann@38622
   138
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
avigad@16908
   139
haftmann@38622
   140
instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
avigad@16908
   141
wenzelm@46575
   142
instance "fun" :: (type, semiring_char_0) semiring_char_0
wenzelm@46575
   143
proof
haftmann@38622
   144
  from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
haftmann@38622
   145
    by (rule inj_fun)
haftmann@38622
   146
  then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
haftmann@38622
   147
    by (simp add: of_nat_fun)
haftmann@38622
   148
  then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
haftmann@38622
   149
qed
avigad@16908
   150
haftmann@38622
   151
instance "fun" :: (type, ring) ring ..
avigad@16908
   152
haftmann@38622
   153
instance "fun" :: (type, comm_ring) comm_ring ..
avigad@16908
   154
haftmann@38622
   155
instance "fun" :: (type, ring_1) ring_1 ..
avigad@16908
   156
haftmann@38622
   157
instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
avigad@16908
   158
haftmann@38622
   159
instance "fun" :: (type, ring_char_0) ring_char_0 ..
avigad@16908
   160
avigad@16908
   161
haftmann@38622
   162
text {* Ordereded structures *}
avigad@16908
   163
wenzelm@46575
   164
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
wenzelm@46575
   165
  by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
avigad@16908
   166
haftmann@38622
   167
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
avigad@16908
   168
wenzelm@46575
   169
instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
wenzelm@46575
   170
  by default (simp add: plus_fun_def le_fun_def)
avigad@16908
   171
haftmann@38622
   172
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
haftmann@38622
   173
haftmann@38622
   174
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
avigad@16908
   175
wenzelm@46575
   176
instance "fun" :: (type, ordered_semiring) ordered_semiring
wenzelm@46575
   177
  by default
wenzelm@46575
   178
    (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
avigad@16908
   179
wenzelm@46575
   180
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
wenzelm@46575
   181
  by default (fact mult_left_mono)
avigad@16908
   182
haftmann@38622
   183
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
avigad@16908
   184
haftmann@38622
   185
instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
haftmann@38622
   186
haftmann@38622
   187
instance "fun" :: (type, ordered_ring) ordered_ring ..
avigad@16908
   188
haftmann@38622
   189
instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
haftmann@38622
   190
avigad@16908
   191
haftmann@38622
   192
lemmas func_plus = plus_fun_def
haftmann@38622
   193
lemmas func_zero = zero_fun_def
haftmann@38622
   194
lemmas func_times = times_fun_def
haftmann@38622
   195
lemmas func_one = one_fun_def
wenzelm@19736
   196
avigad@16908
   197
end