src/HOL/Library/Product_plus.thy
author huffman
Mon Aug 08 10:32:55 2011 -0700 (2011-08-08)
changeset 44066 d74182c93f04
parent 37678 0040bafffdef
child 51002 496013a6eb38
permissions -rw-r--r--
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman@30018
     1
(*  Title:      HOL/Library/Product_plus.thy
huffman@30018
     2
    Author:     Brian Huffman
huffman@30018
     3
*)
huffman@30018
     4
huffman@30018
     5
header {* Additive group operations on product types *}
huffman@30018
     6
huffman@30018
     7
theory Product_plus
huffman@30018
     8
imports Main
huffman@30018
     9
begin
huffman@30018
    10
huffman@30018
    11
subsection {* Operations *}
huffman@30018
    12
haftmann@37678
    13
instantiation prod :: (zero, zero) zero
huffman@30018
    14
begin
huffman@30018
    15
huffman@30018
    16
definition zero_prod_def: "0 = (0, 0)"
huffman@30018
    17
huffman@30018
    18
instance ..
huffman@30018
    19
end
huffman@30018
    20
haftmann@37678
    21
instantiation prod :: (plus, plus) plus
huffman@30018
    22
begin
huffman@30018
    23
huffman@30018
    24
definition plus_prod_def:
huffman@30018
    25
  "x + y = (fst x + fst y, snd x + snd y)"
huffman@30018
    26
huffman@30018
    27
instance ..
huffman@30018
    28
end
huffman@30018
    29
haftmann@37678
    30
instantiation prod :: (minus, minus) minus
huffman@30018
    31
begin
huffman@30018
    32
huffman@30018
    33
definition minus_prod_def:
huffman@30018
    34
  "x - y = (fst x - fst y, snd x - snd y)"
huffman@30018
    35
huffman@30018
    36
instance ..
huffman@30018
    37
end
huffman@30018
    38
haftmann@37678
    39
instantiation prod :: (uminus, uminus) uminus
huffman@30018
    40
begin
huffman@30018
    41
huffman@30018
    42
definition uminus_prod_def:
huffman@30018
    43
  "- x = (- fst x, - snd x)"
huffman@30018
    44
huffman@30018
    45
instance ..
huffman@30018
    46
end
huffman@30018
    47
huffman@30018
    48
lemma fst_zero [simp]: "fst 0 = 0"
huffman@30018
    49
  unfolding zero_prod_def by simp
huffman@30018
    50
huffman@30018
    51
lemma snd_zero [simp]: "snd 0 = 0"
huffman@30018
    52
  unfolding zero_prod_def by simp
huffman@30018
    53
huffman@30018
    54
lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
huffman@30018
    55
  unfolding plus_prod_def by simp
huffman@30018
    56
huffman@30018
    57
lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
huffman@30018
    58
  unfolding plus_prod_def by simp
huffman@30018
    59
huffman@30018
    60
lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
huffman@30018
    61
  unfolding minus_prod_def by simp
huffman@30018
    62
huffman@30018
    63
lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
huffman@30018
    64
  unfolding minus_prod_def by simp
huffman@30018
    65
huffman@30018
    66
lemma fst_uminus [simp]: "fst (- x) = - fst x"
huffman@30018
    67
  unfolding uminus_prod_def by simp
huffman@30018
    68
huffman@30018
    69
lemma snd_uminus [simp]: "snd (- x) = - snd x"
huffman@30018
    70
  unfolding uminus_prod_def by simp
huffman@30018
    71
huffman@30018
    72
lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
huffman@30018
    73
  unfolding plus_prod_def by simp
huffman@30018
    74
huffman@30018
    75
lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
huffman@30018
    76
  unfolding minus_prod_def by simp
huffman@30018
    77
huffman@30018
    78
lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
huffman@30018
    79
  unfolding uminus_prod_def by simp
huffman@30018
    80
huffman@30018
    81
subsection {* Class instances *}
huffman@30018
    82
haftmann@37678
    83
instance prod :: (semigroup_add, semigroup_add) semigroup_add
huffman@44066
    84
  by default (simp add: prod_eq_iff add_assoc)
huffman@30018
    85
haftmann@37678
    86
instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
huffman@44066
    87
  by default (simp add: prod_eq_iff add_commute)
huffman@30018
    88
haftmann@37678
    89
instance prod :: (monoid_add, monoid_add) monoid_add
huffman@44066
    90
  by default (simp_all add: prod_eq_iff)
huffman@30018
    91
haftmann@37678
    92
instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
huffman@44066
    93
  by default (simp add: prod_eq_iff)
huffman@30018
    94
haftmann@37678
    95
instance prod ::
huffman@30018
    96
  (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
huffman@44066
    97
    by default (simp_all add: prod_eq_iff)
huffman@30018
    98
haftmann@37678
    99
instance prod ::
huffman@30018
   100
  (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
huffman@44066
   101
    by default (simp add: prod_eq_iff)
huffman@30018
   102
haftmann@37678
   103
instance prod ::
huffman@30018
   104
  (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
huffman@30018
   105
haftmann@37678
   106
instance prod :: (group_add, group_add) group_add
huffman@44066
   107
  by default (simp_all add: prod_eq_iff diff_minus)
huffman@30018
   108
haftmann@37678
   109
instance prod :: (ab_group_add, ab_group_add) ab_group_add
huffman@44066
   110
  by default (simp_all add: prod_eq_iff)
huffman@30018
   111
huffman@36627
   112
lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
huffman@36627
   113
by (cases "finite A", induct set: finite, simp_all)
huffman@36627
   114
huffman@36627
   115
lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
huffman@36627
   116
by (cases "finite A", induct set: finite, simp_all)
huffman@36627
   117
hoelzl@37664
   118
lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
hoelzl@37664
   119
by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def)
hoelzl@37664
   120
huffman@30018
   121
end