src/HOL/Library/Product_plus.thy
 author haftmann Thu Jul 01 16:54:44 2010 +0200 (2010-07-01) changeset 37678 0040bafffdef parent 37664 2946b8f057df child 44066 d74182c93f04 permissions -rw-r--r--
"prod" and "sum" replace "*" and "+" respectively
1 (*  Title:      HOL/Library/Product_plus.thy
2     Author:     Brian Huffman
3 *)
7 theory Product_plus
8 imports Main
9 begin
11 subsection {* Operations *}
13 instantiation prod :: (zero, zero) zero
14 begin
16 definition zero_prod_def: "0 = (0, 0)"
18 instance ..
19 end
21 instantiation prod :: (plus, plus) plus
22 begin
24 definition plus_prod_def:
25   "x + y = (fst x + fst y, snd x + snd y)"
27 instance ..
28 end
30 instantiation prod :: (minus, minus) minus
31 begin
33 definition minus_prod_def:
34   "x - y = (fst x - fst y, snd x - snd y)"
36 instance ..
37 end
39 instantiation prod :: (uminus, uminus) uminus
40 begin
42 definition uminus_prod_def:
43   "- x = (- fst x, - snd x)"
45 instance ..
46 end
48 lemma fst_zero [simp]: "fst 0 = 0"
49   unfolding zero_prod_def by simp
51 lemma snd_zero [simp]: "snd 0 = 0"
52   unfolding zero_prod_def by simp
54 lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
55   unfolding plus_prod_def by simp
57 lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
58   unfolding plus_prod_def by simp
60 lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
61   unfolding minus_prod_def by simp
63 lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
64   unfolding minus_prod_def by simp
66 lemma fst_uminus [simp]: "fst (- x) = - fst x"
67   unfolding uminus_prod_def by simp
69 lemma snd_uminus [simp]: "snd (- x) = - snd x"
70   unfolding uminus_prod_def by simp
72 lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
73   unfolding plus_prod_def by simp
75 lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
76   unfolding minus_prod_def by simp
78 lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
79   unfolding uminus_prod_def by simp
81 lemmas expand_prod_eq = Pair_fst_snd_eq
84 subsection {* Class instances *}
93   by default (simp_all add: expand_prod_eq)
96   by default (simp add: expand_prod_eq)
98 instance prod ::
100     by default (simp_all add: expand_prod_eq)
102 instance prod ::
104     by default (simp add: expand_prod_eq)
106 instance prod ::