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