src/HOL/Library/Product_Plus.thy
 author wenzelm Wed Mar 08 10:50:59 2017 +0100 (2017-03-08) changeset 65151 a7394aa4d21c parent 64267 b9a1486e79be permissions -rw-r--r--
tuned proofs;
```     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_sum: "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_sum: "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 sum_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
```