src/HOL/Library/Function_Algebras.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62376 85f38d5f8807
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/Function_Algebras.thy
     2     Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
     3 *)
     4 
     5 section \<open>Pointwise instantiation of functions to algebra type classes\<close>
     6 
     7 theory Function_Algebras
     8 imports Main
     9 begin
    10 
    11 text \<open>Pointwise operations\<close>
    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 lemma plus_fun_apply [simp]:
    22   "(f + g) x = f x + g x"
    23   by (simp add: plus_fun_def)
    24 
    25 instantiation "fun" :: (type, zero) zero
    26 begin
    27 
    28 definition "0 = (\<lambda>x. 0)"
    29 instance ..
    30 
    31 end
    32 
    33 lemma zero_fun_apply [simp]:
    34   "0 x = 0"
    35   by (simp add: zero_fun_def)
    36 
    37 instantiation "fun" :: (type, times) times
    38 begin
    39 
    40 definition "f * g = (\<lambda>x. f x * g x)"
    41 instance ..
    42 
    43 end
    44 
    45 lemma times_fun_apply [simp]:
    46   "(f * g) x = f x * g x"
    47   by (simp add: times_fun_def)
    48 
    49 instantiation "fun" :: (type, one) one
    50 begin
    51 
    52 definition "1 = (\<lambda>x. 1)"
    53 instance ..
    54 
    55 end
    56 
    57 lemma one_fun_apply [simp]:
    58   "1 x = 1"
    59   by (simp add: one_fun_def)
    60 
    61 
    62 text \<open>Additive structures\<close>
    63 
    64 instance "fun" :: (type, semigroup_add) semigroup_add
    65   by standard (simp add: fun_eq_iff add.assoc)
    66 
    67 instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
    68   by standard (simp_all add: fun_eq_iff)
    69 
    70 instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
    71   by standard (simp add: fun_eq_iff add.commute)
    72 
    73 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    74   by standard (simp_all add: fun_eq_iff diff_diff_eq)
    75 
    76 instance "fun" :: (type, monoid_add) monoid_add
    77   by standard (simp_all add: fun_eq_iff)
    78 
    79 instance "fun" :: (type, comm_monoid_add) comm_monoid_add
    80   by standard simp
    81 
    82 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    83 
    84 instance "fun" :: (type, group_add) group_add
    85   by standard (simp_all add: fun_eq_iff)
    86 
    87 instance "fun" :: (type, ab_group_add) ab_group_add
    88   by standard simp_all
    89 
    90 
    91 text \<open>Multiplicative structures\<close>
    92 
    93 instance "fun" :: (type, semigroup_mult) semigroup_mult
    94   by standard (simp add: fun_eq_iff mult.assoc)
    95 
    96 instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
    97   by standard (simp add: fun_eq_iff mult.commute)
    98 
    99 instance "fun" :: (type, monoid_mult) monoid_mult
   100   by standard (simp_all add: fun_eq_iff)
   101 
   102 instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
   103   by standard simp
   104 
   105 
   106 text \<open>Misc\<close>
   107 
   108 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
   109 
   110 instance "fun" :: (type, mult_zero) mult_zero
   111   by standard (simp_all add: fun_eq_iff)
   112 
   113 instance "fun" :: (type, zero_neq_one) zero_neq_one
   114   by standard (simp add: fun_eq_iff)
   115 
   116 
   117 text \<open>Ring structures\<close>
   118 
   119 instance "fun" :: (type, semiring) semiring
   120   by standard (simp_all add: fun_eq_iff algebra_simps)
   121 
   122 instance "fun" :: (type, comm_semiring) comm_semiring
   123   by standard (simp add: fun_eq_iff  algebra_simps)
   124 
   125 instance "fun" :: (type, semiring_0) semiring_0 ..
   126 
   127 instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
   128 
   129 instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
   130 
   131 instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
   132 
   133 instance "fun" :: (type, semiring_1) semiring_1 ..
   134 
   135 lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
   136 proof -
   137   have comp: "comp = (\<lambda>f g x. f (g x))"
   138     by (rule ext)+ simp
   139   have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
   140     by (rule ext, rule ext) (fact plus_fun_def)
   141   have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
   142     by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
   143   also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
   144     by (simp only: comp_funpow)
   145   finally show ?thesis by (simp add: of_nat_def comp)
   146 qed
   147 
   148 lemma of_nat_fun_apply [simp]:
   149   "of_nat n x = of_nat n"
   150   by (simp add: of_nat_fun)
   151 
   152 instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
   153 
   154 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
   155 
   156 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel
   157   by standard (auto simp add: times_fun_def algebra_simps)
   158 
   159 instance "fun" :: (type, semiring_char_0) semiring_char_0
   160 proof
   161   from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
   162     by (rule inj_fun)
   163   then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
   164     by (simp add: of_nat_fun)
   165   then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
   166 qed
   167 
   168 instance "fun" :: (type, ring) ring ..
   169 
   170 instance "fun" :: (type, comm_ring) comm_ring ..
   171 
   172 instance "fun" :: (type, ring_1) ring_1 ..
   173 
   174 instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
   175 
   176 instance "fun" :: (type, ring_char_0) ring_char_0 ..
   177 
   178 
   179 text \<open>Ordered structures\<close>
   180 
   181 instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
   182   by standard (auto simp add: le_fun_def intro: add_left_mono)
   183 
   184 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   185 
   186 instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
   187   by standard (simp add: le_fun_def)
   188 
   189 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
   190 
   191 instance "fun" :: (type, ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
   192 
   193 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
   194 
   195 instance "fun" :: (type, ordered_semiring) ordered_semiring
   196   by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
   197 
   198 instance "fun" :: (type, dioid) dioid
   199 proof standard
   200   fix a b :: "'a \<Rightarrow> 'b"
   201   show "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
   202     unfolding le_fun_def plus_fun_def fun_eq_iff choice_iff[symmetric, of "\<lambda>x c. b x = a x + c"]
   203     by (intro arg_cong[where f=All] ext canonically_ordered_monoid_add_class.le_iff_add)
   204 qed
   205 
   206 instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
   207   by standard (fact mult_left_mono)
   208 
   209 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
   210 
   211 instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
   212 
   213 instance "fun" :: (type, ordered_ring) ordered_ring ..
   214 
   215 instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
   216 
   217 
   218 lemmas func_plus = plus_fun_def
   219 lemmas func_zero = zero_fun_def
   220 lemmas func_times = times_fun_def
   221 lemmas func_one = one_fun_def
   222 
   223 end
   224