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