src/HOL/Library/Product_plus.thy
changeset 30018 690c65b8ad1a
child 36627 39b2516a1970
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Fri Feb 20 07:41:41 2009 -0800
     1.3 @@ -0,0 +1,115 @@
     1.4 +(*  Title:      HOL/Library/Product_plus.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Additive group operations on product types *}
     1.9 +
    1.10 +theory Product_plus
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +subsection {* Operations *}
    1.15 +
    1.16 +instantiation "*" :: (zero, zero) zero
    1.17 +begin
    1.18 +
    1.19 +definition zero_prod_def: "0 = (0, 0)"
    1.20 +
    1.21 +instance ..
    1.22 +end
    1.23 +
    1.24 +instantiation "*" :: (plus, plus) plus
    1.25 +begin
    1.26 +
    1.27 +definition plus_prod_def:
    1.28 +  "x + y = (fst x + fst y, snd x + snd y)"
    1.29 +
    1.30 +instance ..
    1.31 +end
    1.32 +
    1.33 +instantiation "*" :: (minus, minus) minus
    1.34 +begin
    1.35 +
    1.36 +definition minus_prod_def:
    1.37 +  "x - y = (fst x - fst y, snd x - snd y)"
    1.38 +
    1.39 +instance ..
    1.40 +end
    1.41 +
    1.42 +instantiation "*" :: (uminus, uminus) uminus
    1.43 +begin
    1.44 +
    1.45 +definition uminus_prod_def:
    1.46 +  "- x = (- fst x, - snd x)"
    1.47 +
    1.48 +instance ..
    1.49 +end
    1.50 +
    1.51 +lemma fst_zero [simp]: "fst 0 = 0"
    1.52 +  unfolding zero_prod_def by simp
    1.53 +
    1.54 +lemma snd_zero [simp]: "snd 0 = 0"
    1.55 +  unfolding zero_prod_def by simp
    1.56 +
    1.57 +lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
    1.58 +  unfolding plus_prod_def by simp
    1.59 +
    1.60 +lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
    1.61 +  unfolding plus_prod_def by simp
    1.62 +
    1.63 +lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
    1.64 +  unfolding minus_prod_def by simp
    1.65 +
    1.66 +lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
    1.67 +  unfolding minus_prod_def by simp
    1.68 +
    1.69 +lemma fst_uminus [simp]: "fst (- x) = - fst x"
    1.70 +  unfolding uminus_prod_def by simp
    1.71 +
    1.72 +lemma snd_uminus [simp]: "snd (- x) = - snd x"
    1.73 +  unfolding uminus_prod_def by simp
    1.74 +
    1.75 +lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
    1.76 +  unfolding plus_prod_def by simp
    1.77 +
    1.78 +lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
    1.79 +  unfolding minus_prod_def by simp
    1.80 +
    1.81 +lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
    1.82 +  unfolding uminus_prod_def by simp
    1.83 +
    1.84 +lemmas expand_prod_eq = Pair_fst_snd_eq
    1.85 +
    1.86 +
    1.87 +subsection {* Class instances *}
    1.88 +
    1.89 +instance "*" :: (semigroup_add, semigroup_add) semigroup_add
    1.90 +  by default (simp add: expand_prod_eq add_assoc)
    1.91 +
    1.92 +instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    1.93 +  by default (simp add: expand_prod_eq add_commute)
    1.94 +
    1.95 +instance "*" :: (monoid_add, monoid_add) monoid_add
    1.96 +  by default (simp_all add: expand_prod_eq)
    1.97 +
    1.98 +instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    1.99 +  by default (simp add: expand_prod_eq)
   1.100 +
   1.101 +instance "*" ::
   1.102 +  (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
   1.103 +    by default (simp_all add: expand_prod_eq)
   1.104 +
   1.105 +instance "*" ::
   1.106 +  (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   1.107 +    by default (simp add: expand_prod_eq)
   1.108 +
   1.109 +instance "*" ::
   1.110 +  (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   1.111 +
   1.112 +instance "*" :: (group_add, group_add) group_add
   1.113 +  by default (simp_all add: expand_prod_eq diff_minus)
   1.114 +
   1.115 +instance "*" :: (ab_group_add, ab_group_add) ab_group_add
   1.116 +  by default (simp_all add: expand_prod_eq)
   1.117 +
   1.118 +end