equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Product_plus.thy |
1 (* Title: HOL/Library/Product_plus.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 section {* Additive group operations on product types *} |
5 section \<open>Additive group operations on product types\<close> |
6 |
6 |
7 theory Product_plus |
7 theory Product_plus |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Operations *} |
11 subsection \<open>Operations\<close> |
12 |
12 |
13 instantiation prod :: (zero, zero) zero |
13 instantiation prod :: (zero, zero) zero |
14 begin |
14 begin |
15 |
15 |
16 definition zero_prod_def: "0 = (0, 0)" |
16 definition zero_prod_def: "0 = (0, 0)" |
76 unfolding minus_prod_def by simp |
76 unfolding minus_prod_def by simp |
77 |
77 |
78 lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)" |
78 lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)" |
79 unfolding uminus_prod_def by simp |
79 unfolding uminus_prod_def by simp |
80 |
80 |
81 subsection {* Class instances *} |
81 subsection \<open>Class instances\<close> |
82 |
82 |
83 instance prod :: (semigroup_add, semigroup_add) semigroup_add |
83 instance prod :: (semigroup_add, semigroup_add) semigroup_add |
84 by default (simp add: prod_eq_iff add.assoc) |
84 by default (simp add: prod_eq_iff add.assoc) |
85 |
85 |
86 instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add |
86 instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add |