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