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;
huffman@30018
     1
(*  Title:      HOL/Library/Product_plus.thy
huffman@30018
     2
    Author:     Brian Huffman
huffman@30018
     3
*)
huffman@30018
     4
huffman@30018
     5
header {* Additive group operations on product types *}
huffman@30018
     6
huffman@30018
     7
theory Product_plus
huffman@30018
     8
imports Main
huffman@30018
     9
begin
huffman@30018
    10
huffman@30018
    11
subsection {* Operations *}
huffman@30018
    12
huffman@30018
    13
instantiation "*" :: (zero, zero) zero
huffman@30018
    14
begin
huffman@30018
    15
huffman@30018
    16
definition zero_prod_def: "0 = (0, 0)"
huffman@30018
    17
huffman@30018
    18
instance ..
huffman@30018
    19
end
huffman@30018
    20
huffman@30018
    21
instantiation "*" :: (plus, plus) plus
huffman@30018
    22
begin
huffman@30018
    23
huffman@30018
    24
definition plus_prod_def:
huffman@30018
    25
  "x + y = (fst x + fst y, snd x + snd y)"
huffman@30018
    26
huffman@30018
    27
instance ..
huffman@30018
    28
end
huffman@30018
    29
huffman@30018
    30
instantiation "*" :: (minus, minus) minus
huffman@30018
    31
begin
huffman@30018
    32
huffman@30018
    33
definition minus_prod_def:
huffman@30018
    34
  "x - y = (fst x - fst y, snd x - snd y)"
huffman@30018
    35
huffman@30018
    36
instance ..
huffman@30018
    37
end
huffman@30018
    38
huffman@30018
    39
instantiation "*" :: (uminus, uminus) uminus
huffman@30018
    40
begin
huffman@30018
    41
huffman@30018
    42
definition uminus_prod_def:
huffman@30018
    43
  "- x = (- fst x, - snd x)"
huffman@30018
    44
huffman@30018
    45
instance ..
huffman@30018
    46
end
huffman@30018
    47
huffman@30018
    48
lemma fst_zero [simp]: "fst 0 = 0"
huffman@30018
    49
  unfolding zero_prod_def by simp
huffman@30018
    50
huffman@30018
    51
lemma snd_zero [simp]: "snd 0 = 0"
huffman@30018
    52
  unfolding zero_prod_def by simp
huffman@30018
    53
huffman@30018
    54
lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
huffman@30018
    55
  unfolding plus_prod_def by simp
huffman@30018
    56
huffman@30018
    57
lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
huffman@30018
    58
  unfolding plus_prod_def by simp
huffman@30018
    59
huffman@30018
    60
lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
huffman@30018
    61
  unfolding minus_prod_def by simp
huffman@30018
    62
huffman@30018
    63
lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
huffman@30018
    64
  unfolding minus_prod_def by simp
huffman@30018
    65
huffman@30018
    66
lemma fst_uminus [simp]: "fst (- x) = - fst x"
huffman@30018
    67
  unfolding uminus_prod_def by simp
huffman@30018
    68
huffman@30018
    69
lemma snd_uminus [simp]: "snd (- x) = - snd x"
huffman@30018
    70
  unfolding uminus_prod_def by simp
huffman@30018
    71
huffman@30018
    72
lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
huffman@30018
    73
  unfolding plus_prod_def by simp
huffman@30018
    74
huffman@30018
    75
lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
huffman@30018
    76
  unfolding minus_prod_def by simp
huffman@30018
    77
huffman@30018
    78
lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
huffman@30018
    79
  unfolding uminus_prod_def by simp
huffman@30018
    80
huffman@30018
    81
lemmas expand_prod_eq = Pair_fst_snd_eq
huffman@30018
    82
huffman@30018
    83
huffman@30018
    84
subsection {* Class instances *}
huffman@30018
    85
huffman@30018
    86
instance "*" :: (semigroup_add, semigroup_add) semigroup_add
huffman@30018
    87
  by default (simp add: expand_prod_eq add_assoc)
huffman@30018
    88
huffman@30018
    89
instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
huffman@30018
    90
  by default (simp add: expand_prod_eq add_commute)
huffman@30018
    91
huffman@30018
    92
instance "*" :: (monoid_add, monoid_add) monoid_add
huffman@30018
    93
  by default (simp_all add: expand_prod_eq)
huffman@30018
    94
huffman@30018
    95
instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
huffman@30018
    96
  by default (simp add: expand_prod_eq)
huffman@30018
    97
huffman@30018
    98
instance "*" ::
huffman@30018
    99
  (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
huffman@30018
   100
    by default (simp_all add: expand_prod_eq)
huffman@30018
   101
huffman@30018
   102
instance "*" ::
huffman@30018
   103
  (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
huffman@30018
   104
    by default (simp add: expand_prod_eq)
huffman@30018
   105
huffman@30018
   106
instance "*" ::
huffman@30018
   107
  (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
huffman@30018
   108
huffman@30018
   109
instance "*" :: (group_add, group_add) group_add
huffman@30018
   110
  by default (simp_all add: expand_prod_eq diff_minus)
huffman@30018
   111
huffman@30018
   112
instance "*" :: (ab_group_add, ab_group_add) ab_group_add
huffman@30018
   113
  by default (simp_all add: expand_prod_eq)
huffman@30018
   114
huffman@30018
   115
end