src/HOL/Library/Product_plus.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 60679 ade12ef2773c
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Library/Product_plus.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Additive group operations on product types\<close>
     6 
     7 theory Product_plus
     8 imports Main
     9 begin
    10 
    11 subsection \<open>Operations\<close>
    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 \<open>Class instances\<close>
    82 
    83 instance prod :: (semigroup_add, semigroup_add) semigroup_add
    84   by standard (simp add: prod_eq_iff add.assoc)
    85 
    86 instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    87   by standard (simp add: prod_eq_iff add.commute)
    88 
    89 instance prod :: (monoid_add, monoid_add) monoid_add
    90   by standard (simp_all add: prod_eq_iff)
    91 
    92 instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    93   by standard (simp add: prod_eq_iff)
    94 
    95 instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
    96     by standard (simp_all add: prod_eq_iff)
    97 
    98 instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    99     by standard (simp_all add: prod_eq_iff diff_diff_eq)
   100 
   101 instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   102 
   103 instance prod :: (group_add, group_add) group_add
   104   by standard (simp_all add: prod_eq_iff)
   105 
   106 instance prod :: (ab_group_add, ab_group_add) ab_group_add
   107   by standard (simp_all add: prod_eq_iff)
   108 
   109 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
   110 proof (cases "finite A")
   111   case True
   112   then show ?thesis by induct simp_all
   113 next
   114   case False
   115   then show ?thesis by simp
   116 qed
   117 
   118 lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
   119 proof (cases "finite A")
   120   case True
   121   then show ?thesis by induct simp_all
   122 next
   123   case False
   124   then show ?thesis by simp
   125 qed
   126 
   127 lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
   128 proof (cases "finite A")
   129   case True
   130   then show ?thesis by induct (simp_all add: zero_prod_def)
   131 next
   132   case False
   133   then show ?thesis by (simp add: zero_prod_def)
   134 qed
   135 
   136 end