src/HOL/Library/Function_Algebras.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 62376 85f38d5f8807 permissions -rw-r--r--
executable domain membership checks
```     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
```