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