src/HOL/Library/Product_Plus.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 64267 b9a1486e79be
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
hoelzl@63972
     1
(*  Title:      HOL/Library/Product_Plus.thy
huffman@30018
     2
    Author:     Brian Huffman
huffman@30018
     3
*)
huffman@30018
     4
wenzelm@60500
     5
section \<open>Additive group operations on product types\<close>
huffman@30018
     6
hoelzl@63972
     7
theory Product_Plus
wenzelm@51301
     8
imports Main
huffman@30018
     9
begin
huffman@30018
    10
wenzelm@60500
    11
subsection \<open>Operations\<close>
huffman@30018
    12
haftmann@37678
    13
instantiation prod :: (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
haftmann@37678
    21
instantiation prod :: (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
haftmann@37678
    30
instantiation prod :: (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
haftmann@37678
    39
instantiation prod :: (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
wenzelm@60500
    81
subsection \<open>Class instances\<close>
huffman@30018
    82
haftmann@37678
    83
instance prod :: (semigroup_add, semigroup_add) semigroup_add
wenzelm@60679
    84
  by standard (simp add: prod_eq_iff add.assoc)
huffman@30018
    85
haftmann@37678
    86
instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
wenzelm@60679
    87
  by standard (simp add: prod_eq_iff add.commute)
huffman@30018
    88
haftmann@37678
    89
instance prod :: (monoid_add, monoid_add) monoid_add
wenzelm@60679
    90
  by standard (simp_all add: prod_eq_iff)
huffman@30018
    91
haftmann@37678
    92
instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
wenzelm@60679
    93
  by standard (simp add: prod_eq_iff)
huffman@30018
    94
wenzelm@60679
    95
instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
wenzelm@60679
    96
    by standard (simp_all add: prod_eq_iff)
huffman@30018
    97
wenzelm@60679
    98
instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
wenzelm@60679
    99
    by standard (simp_all add: prod_eq_iff diff_diff_eq)
huffman@30018
   100
wenzelm@60679
   101
instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
huffman@30018
   102
haftmann@37678
   103
instance prod :: (group_add, group_add) group_add
wenzelm@60679
   104
  by standard (simp_all add: prod_eq_iff)
huffman@30018
   105
haftmann@37678
   106
instance prod :: (ab_group_add, ab_group_add) ab_group_add
wenzelm@60679
   107
  by standard (simp_all add: prod_eq_iff)
huffman@30018
   108
nipkow@64267
   109
lemma fst_sum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
wenzelm@60679
   110
proof (cases "finite A")
wenzelm@60679
   111
  case True
wenzelm@60679
   112
  then show ?thesis by induct simp_all
wenzelm@60679
   113
next
wenzelm@60679
   114
  case False
wenzelm@60679
   115
  then show ?thesis by simp
wenzelm@60679
   116
qed
huffman@36627
   117
nipkow@64267
   118
lemma snd_sum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
wenzelm@60679
   119
proof (cases "finite A")
wenzelm@60679
   120
  case True
wenzelm@60679
   121
  then show ?thesis by induct simp_all
wenzelm@60679
   122
next
wenzelm@60679
   123
  case False
wenzelm@60679
   124
  then show ?thesis by simp
wenzelm@60679
   125
qed
huffman@36627
   126
nipkow@64267
   127
lemma sum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
wenzelm@60679
   128
proof (cases "finite A")
wenzelm@60679
   129
  case True
wenzelm@60679
   130
  then show ?thesis by induct (simp_all add: zero_prod_def)
wenzelm@60679
   131
next
wenzelm@60679
   132
  case False
wenzelm@60679
   133
  then show ?thesis by (simp add: zero_prod_def)
wenzelm@60679
   134
qed
hoelzl@37664
   135
huffman@30018
   136
end