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