src/HOL/Library/Function_Algebras.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 39302 d7728f65b353
child 46575 f1e387195a56
permissions -rw-r--r--
Quotient_Info stores only relation maps
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
nipkow@39302
    60
qed (simp_all add: plus_fun_def fun_eq_iff)
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, zero_neq_one) zero_neq_one proof
nipkow@39302
   109
qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
wenzelm@19736
   110
avigad@16908
   111
haftmann@38622
   112
text {* Ring structures *}
avigad@16908
   113
haftmann@38622
   114
instance "fun" :: (type, semiring) semiring proof
haftmann@38622
   115
qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
avigad@16908
   116
haftmann@38622
   117
instance "fun" :: (type, comm_semiring) comm_semiring proof
haftmann@38622
   118
qed (simp add: plus_fun_def times_fun_def algebra_simps)
avigad@16908
   119
haftmann@38622
   120
instance "fun" :: (type, semiring_0) semiring_0 ..
haftmann@38622
   121
haftmann@38622
   122
instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
avigad@16908
   123
haftmann@38622
   124
instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
avigad@16908
   125
haftmann@38622
   126
instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
avigad@16908
   127
haftmann@38622
   128
instance "fun" :: (type, semiring_1) semiring_1 ..
avigad@16908
   129
haftmann@38622
   130
lemma of_nat_fun:
haftmann@38622
   131
  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
haftmann@38622
   132
proof -
haftmann@38622
   133
  have comp: "comp = (\<lambda>f g x. f (g x))"
haftmann@38622
   134
    by (rule ext)+ simp
haftmann@38622
   135
  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
haftmann@38622
   136
    by (rule ext, rule ext) (fact plus_fun_def)
haftmann@38622
   137
  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   138
    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
haftmann@38622
   139
  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
haftmann@38622
   140
    by (simp only: comp_funpow)
haftmann@38622
   141
  finally show ?thesis by (simp add: of_nat_def comp)
haftmann@38622
   142
qed
avigad@16908
   143
haftmann@38622
   144
instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
avigad@16908
   145
haftmann@38622
   146
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
avigad@16908
   147
haftmann@38622
   148
instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
avigad@16908
   149
haftmann@38622
   150
instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
haftmann@38622
   151
  from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
haftmann@38622
   152
    by (rule inj_fun)
haftmann@38622
   153
  then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
haftmann@38622
   154
    by (simp add: of_nat_fun)
haftmann@38622
   155
  then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
haftmann@38622
   156
qed
avigad@16908
   157
haftmann@38622
   158
instance "fun" :: (type, ring) ring ..
avigad@16908
   159
haftmann@38622
   160
instance "fun" :: (type, comm_ring) comm_ring ..
avigad@16908
   161
haftmann@38622
   162
instance "fun" :: (type, ring_1) ring_1 ..
avigad@16908
   163
haftmann@38622
   164
instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
avigad@16908
   165
haftmann@38622
   166
instance "fun" :: (type, ring_char_0) ring_char_0 ..
avigad@16908
   167
avigad@16908
   168
haftmann@38622
   169
text {* Ordereded structures *}
avigad@16908
   170
haftmann@38622
   171
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
haftmann@38622
   172
qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
avigad@16908
   173
haftmann@38622
   174
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
avigad@16908
   175
haftmann@38622
   176
instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
haftmann@38622
   177
qed (simp add: plus_fun_def le_fun_def)
avigad@16908
   178
haftmann@38622
   179
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
haftmann@38622
   180
haftmann@38622
   181
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
avigad@16908
   182
haftmann@38642
   183
instance "fun" :: (type, ordered_semiring) ordered_semiring proof
haftmann@38642
   184
qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
avigad@16908
   185
haftmann@38642
   186
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
haftmann@38642
   187
qed (fact mult_left_mono)
avigad@16908
   188
haftmann@38622
   189
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
avigad@16908
   190
haftmann@38622
   191
instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
haftmann@38622
   192
haftmann@38622
   193
instance "fun" :: (type, ordered_ring) ordered_ring ..
avigad@16908
   194
haftmann@38622
   195
instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
haftmann@38622
   196
avigad@16908
   197
haftmann@38622
   198
lemmas func_plus = plus_fun_def
haftmann@38622
   199
lemmas func_zero = zero_fun_def
haftmann@38622
   200
lemmas func_times = times_fun_def
haftmann@38622
   201
lemmas func_one = one_fun_def
wenzelm@19736
   202
avigad@16908
   203
end