src/HOL/Library/Product_plus.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 57512 cc97b347b301 child 58881 b9556a055632 permissions -rw-r--r--
simpler proof
```     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 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)
```
```   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
```