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