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