src/HOL/Library/Product_plus.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 30018 690c65b8ad1a
child 36627 39b2516a1970
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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 "*" :: (zero, zero) zero
    14 begin
    15 
    16 definition zero_prod_def: "0 = (0, 0)"
    17 
    18 instance ..
    19 end
    20 
    21 instantiation "*" :: (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 "*" :: (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 "*" :: (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 lemmas expand_prod_eq = Pair_fst_snd_eq
    82 
    83 
    84 subsection {* Class instances *}
    85 
    86 instance "*" :: (semigroup_add, semigroup_add) semigroup_add
    87   by default (simp add: expand_prod_eq add_assoc)
    88 
    89 instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    90   by default (simp add: expand_prod_eq add_commute)
    91 
    92 instance "*" :: (monoid_add, monoid_add) monoid_add
    93   by default (simp_all add: expand_prod_eq)
    94 
    95 instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    96   by default (simp add: expand_prod_eq)
    97 
    98 instance "*" ::
    99   (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
   100     by default (simp_all add: expand_prod_eq)
   101 
   102 instance "*" ::
   103   (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   104     by default (simp add: expand_prod_eq)
   105 
   106 instance "*" ::
   107   (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   108 
   109 instance "*" :: (group_add, group_add) group_add
   110   by default (simp_all add: expand_prod_eq diff_minus)
   111 
   112 instance "*" :: (ab_group_add, ab_group_add) ab_group_add
   113   by default (simp_all add: expand_prod_eq)
   114 
   115 end