huffman@30018: (* Title: HOL/Library/Product_plus.thy huffman@30018: Author: Brian Huffman huffman@30018: *) huffman@30018: huffman@30018: header {* Additive group operations on product types *} huffman@30018: huffman@30018: theory Product_plus hoelzl@51002: imports "~~/src/HOL/Main" huffman@30018: begin huffman@30018: huffman@30018: subsection {* Operations *} huffman@30018: haftmann@37678: instantiation prod :: (zero, zero) zero huffman@30018: begin huffman@30018: huffman@30018: definition zero_prod_def: "0 = (0, 0)" huffman@30018: huffman@30018: instance .. huffman@30018: end huffman@30018: haftmann@37678: instantiation prod :: (plus, plus) plus huffman@30018: begin huffman@30018: huffman@30018: definition plus_prod_def: huffman@30018: "x + y = (fst x + fst y, snd x + snd y)" huffman@30018: huffman@30018: instance .. huffman@30018: end huffman@30018: haftmann@37678: instantiation prod :: (minus, minus) minus huffman@30018: begin huffman@30018: huffman@30018: definition minus_prod_def: huffman@30018: "x - y = (fst x - fst y, snd x - snd y)" huffman@30018: huffman@30018: instance .. huffman@30018: end huffman@30018: haftmann@37678: instantiation prod :: (uminus, uminus) uminus huffman@30018: begin huffman@30018: huffman@30018: definition uminus_prod_def: huffman@30018: "- x = (- fst x, - snd x)" huffman@30018: huffman@30018: instance .. huffman@30018: end huffman@30018: huffman@30018: lemma fst_zero [simp]: "fst 0 = 0" huffman@30018: unfolding zero_prod_def by simp huffman@30018: huffman@30018: lemma snd_zero [simp]: "snd 0 = 0" huffman@30018: unfolding zero_prod_def by simp huffman@30018: huffman@30018: lemma fst_add [simp]: "fst (x + y) = fst x + fst y" huffman@30018: unfolding plus_prod_def by simp huffman@30018: huffman@30018: lemma snd_add [simp]: "snd (x + y) = snd x + snd y" huffman@30018: unfolding plus_prod_def by simp huffman@30018: huffman@30018: lemma fst_diff [simp]: "fst (x - y) = fst x - fst y" huffman@30018: unfolding minus_prod_def by simp huffman@30018: huffman@30018: lemma snd_diff [simp]: "snd (x - y) = snd x - snd y" huffman@30018: unfolding minus_prod_def by simp huffman@30018: huffman@30018: lemma fst_uminus [simp]: "fst (- x) = - fst x" huffman@30018: unfolding uminus_prod_def by simp huffman@30018: huffman@30018: lemma snd_uminus [simp]: "snd (- x) = - snd x" huffman@30018: unfolding uminus_prod_def by simp huffman@30018: huffman@30018: lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)" huffman@30018: unfolding plus_prod_def by simp huffman@30018: huffman@30018: lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)" huffman@30018: unfolding minus_prod_def by simp huffman@30018: huffman@30018: lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)" huffman@30018: unfolding uminus_prod_def by simp huffman@30018: huffman@30018: subsection {* Class instances *} huffman@30018: haftmann@37678: instance prod :: (semigroup_add, semigroup_add) semigroup_add huffman@44066: by default (simp add: prod_eq_iff add_assoc) huffman@30018: haftmann@37678: instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add huffman@44066: by default (simp add: prod_eq_iff add_commute) huffman@30018: haftmann@37678: instance prod :: (monoid_add, monoid_add) monoid_add huffman@44066: by default (simp_all add: prod_eq_iff) huffman@30018: haftmann@37678: instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add huffman@44066: by default (simp add: prod_eq_iff) huffman@30018: haftmann@37678: instance prod :: huffman@30018: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add huffman@44066: by default (simp_all add: prod_eq_iff) huffman@30018: haftmann@37678: instance prod :: huffman@30018: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add huffman@44066: by default (simp add: prod_eq_iff) huffman@30018: haftmann@37678: instance prod :: huffman@30018: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add .. huffman@30018: haftmann@37678: instance prod :: (group_add, group_add) group_add huffman@44066: by default (simp_all add: prod_eq_iff diff_minus) huffman@30018: haftmann@37678: instance prod :: (ab_group_add, ab_group_add) ab_group_add huffman@44066: by default (simp_all add: prod_eq_iff) huffman@30018: huffman@36627: lemma fst_setsum: "fst (\x\A. f x) = (\x\A. fst (f x))" huffman@36627: by (cases "finite A", induct set: finite, simp_all) huffman@36627: huffman@36627: lemma snd_setsum: "snd (\x\A. f x) = (\x\A. snd (f x))" huffman@36627: by (cases "finite A", induct set: finite, simp_all) huffman@36627: hoelzl@37664: lemma setsum_prod: "(\x\A. (f x, g x)) = (\x\A. f x, \x\A. g x)" hoelzl@37664: by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def) hoelzl@37664: huffman@30018: end