Library: fix name Product_plus to Product_Plus
authorhoelzl
Fri Sep 30 15:35:43 2016 +0200 (2016-09-30)
changeset 63972c98d1dd7eba1
parent 63971 da89140186e2
child 63973 b09f16aeb694
Library: fix name Product_plus to Product_Plus
src/HOL/Analysis/Product_Vector.thy
src/HOL/Library/Library.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/Product_Plus.thy
src/HOL/Library/Product_plus.thy
     1.1 --- a/src/HOL/Analysis/Product_Vector.thy	Fri Sep 30 15:35:37 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Fri Sep 30 15:35:43 2016 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  theory Product_Vector
     1.5  imports
     1.6    Inner_Product
     1.7 -  "~~/src/HOL/Library/Product_plus"
     1.8 +  "~~/src/HOL/Library/Product_Plus"
     1.9  begin
    1.10  
    1.11  subsection \<open>Product is a real vector space\<close>
     2.1 --- a/src/HOL/Library/Library.thy	Fri Sep 30 15:35:37 2016 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Fri Sep 30 15:35:43 2016 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4    Polynomial
     2.5    Polynomial_FPS
     2.6    Preorder
     2.7 -  Product_plus
     2.8 +  Product_Plus
     2.9    Quadratic_Discriminant
    2.10    Quotient_List
    2.11    Quotient_Option
     3.1 --- a/src/HOL/Library/Product_Order.thy	Fri Sep 30 15:35:37 2016 +0200
     3.2 +++ b/src/HOL/Library/Product_Order.thy	Fri Sep 30 15:35:43 2016 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  section \<open>Pointwise order on product types\<close>
     3.5  
     3.6  theory Product_Order
     3.7 -imports Product_plus
     3.8 +imports Product_Plus
     3.9  begin
    3.10  
    3.11  subsection \<open>Pointwise ordering\<close>
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Product_Plus.thy	Fri Sep 30 15:35:43 2016 +0200
     4.3 @@ -0,0 +1,136 @@
     4.4 +(*  Title:      HOL/Library/Product_Plus.thy
     4.5 +    Author:     Brian Huffman
     4.6 +*)
     4.7 +
     4.8 +section \<open>Additive group operations on product types\<close>
     4.9 +
    4.10 +theory Product_Plus
    4.11 +imports Main
    4.12 +begin
    4.13 +
    4.14 +subsection \<open>Operations\<close>
    4.15 +
    4.16 +instantiation prod :: (zero, zero) zero
    4.17 +begin
    4.18 +
    4.19 +definition zero_prod_def: "0 = (0, 0)"
    4.20 +
    4.21 +instance ..
    4.22 +end
    4.23 +
    4.24 +instantiation prod :: (plus, plus) plus
    4.25 +begin
    4.26 +
    4.27 +definition plus_prod_def:
    4.28 +  "x + y = (fst x + fst y, snd x + snd y)"
    4.29 +
    4.30 +instance ..
    4.31 +end
    4.32 +
    4.33 +instantiation prod :: (minus, minus) minus
    4.34 +begin
    4.35 +
    4.36 +definition minus_prod_def:
    4.37 +  "x - y = (fst x - fst y, snd x - snd y)"
    4.38 +
    4.39 +instance ..
    4.40 +end
    4.41 +
    4.42 +instantiation prod :: (uminus, uminus) uminus
    4.43 +begin
    4.44 +
    4.45 +definition uminus_prod_def:
    4.46 +  "- x = (- fst x, - snd x)"
    4.47 +
    4.48 +instance ..
    4.49 +end
    4.50 +
    4.51 +lemma fst_zero [simp]: "fst 0 = 0"
    4.52 +  unfolding zero_prod_def by simp
    4.53 +
    4.54 +lemma snd_zero [simp]: "snd 0 = 0"
    4.55 +  unfolding zero_prod_def by simp
    4.56 +
    4.57 +lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
    4.58 +  unfolding plus_prod_def by simp
    4.59 +
    4.60 +lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
    4.61 +  unfolding plus_prod_def by simp
    4.62 +
    4.63 +lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
    4.64 +  unfolding minus_prod_def by simp
    4.65 +
    4.66 +lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
    4.67 +  unfolding minus_prod_def by simp
    4.68 +
    4.69 +lemma fst_uminus [simp]: "fst (- x) = - fst x"
    4.70 +  unfolding uminus_prod_def by simp
    4.71 +
    4.72 +lemma snd_uminus [simp]: "snd (- x) = - snd x"
    4.73 +  unfolding uminus_prod_def by simp
    4.74 +
    4.75 +lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
    4.76 +  unfolding plus_prod_def by simp
    4.77 +
    4.78 +lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
    4.79 +  unfolding minus_prod_def by simp
    4.80 +
    4.81 +lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
    4.82 +  unfolding uminus_prod_def by simp
    4.83 +
    4.84 +subsection \<open>Class instances\<close>
    4.85 +
    4.86 +instance prod :: (semigroup_add, semigroup_add) semigroup_add
    4.87 +  by standard (simp add: prod_eq_iff add.assoc)
    4.88 +
    4.89 +instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    4.90 +  by standard (simp add: prod_eq_iff add.commute)
    4.91 +
    4.92 +instance prod :: (monoid_add, monoid_add) monoid_add
    4.93 +  by standard (simp_all add: prod_eq_iff)
    4.94 +
    4.95 +instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    4.96 +  by standard (simp add: prod_eq_iff)
    4.97 +
    4.98 +instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
    4.99 +    by standard (simp_all add: prod_eq_iff)
   4.100 +
   4.101 +instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   4.102 +    by standard (simp_all add: prod_eq_iff diff_diff_eq)
   4.103 +
   4.104 +instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   4.105 +
   4.106 +instance prod :: (group_add, group_add) group_add
   4.107 +  by standard (simp_all add: prod_eq_iff)
   4.108 +
   4.109 +instance prod :: (ab_group_add, ab_group_add) ab_group_add
   4.110 +  by standard (simp_all add: prod_eq_iff)
   4.111 +
   4.112 +lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
   4.113 +proof (cases "finite A")
   4.114 +  case True
   4.115 +  then show ?thesis by induct simp_all
   4.116 +next
   4.117 +  case False
   4.118 +  then show ?thesis by simp
   4.119 +qed
   4.120 +
   4.121 +lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
   4.122 +proof (cases "finite A")
   4.123 +  case True
   4.124 +  then show ?thesis by induct simp_all
   4.125 +next
   4.126 +  case False
   4.127 +  then show ?thesis by simp
   4.128 +qed
   4.129 +
   4.130 +lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
   4.131 +proof (cases "finite A")
   4.132 +  case True
   4.133 +  then show ?thesis by induct (simp_all add: zero_prod_def)
   4.134 +next
   4.135 +  case False
   4.136 +  then show ?thesis by (simp add: zero_prod_def)
   4.137 +qed
   4.138 +
   4.139 +end
     5.1 --- a/src/HOL/Library/Product_plus.thy	Fri Sep 30 15:35:37 2016 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,136 +0,0 @@
     5.4 -(*  Title:      HOL/Library/Product_plus.thy
     5.5 -    Author:     Brian Huffman
     5.6 -*)
     5.7 -
     5.8 -section \<open>Additive group operations on product types\<close>
     5.9 -
    5.10 -theory Product_plus
    5.11 -imports Main
    5.12 -begin
    5.13 -
    5.14 -subsection \<open>Operations\<close>
    5.15 -
    5.16 -instantiation prod :: (zero, zero) zero
    5.17 -begin
    5.18 -
    5.19 -definition zero_prod_def: "0 = (0, 0)"
    5.20 -
    5.21 -instance ..
    5.22 -end
    5.23 -
    5.24 -instantiation prod :: (plus, plus) plus
    5.25 -begin
    5.26 -
    5.27 -definition plus_prod_def:
    5.28 -  "x + y = (fst x + fst y, snd x + snd y)"
    5.29 -
    5.30 -instance ..
    5.31 -end
    5.32 -
    5.33 -instantiation prod :: (minus, minus) minus
    5.34 -begin
    5.35 -
    5.36 -definition minus_prod_def:
    5.37 -  "x - y = (fst x - fst y, snd x - snd y)"
    5.38 -
    5.39 -instance ..
    5.40 -end
    5.41 -
    5.42 -instantiation prod :: (uminus, uminus) uminus
    5.43 -begin
    5.44 -
    5.45 -definition uminus_prod_def:
    5.46 -  "- x = (- fst x, - snd x)"
    5.47 -
    5.48 -instance ..
    5.49 -end
    5.50 -
    5.51 -lemma fst_zero [simp]: "fst 0 = 0"
    5.52 -  unfolding zero_prod_def by simp
    5.53 -
    5.54 -lemma snd_zero [simp]: "snd 0 = 0"
    5.55 -  unfolding zero_prod_def by simp
    5.56 -
    5.57 -lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
    5.58 -  unfolding plus_prod_def by simp
    5.59 -
    5.60 -lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
    5.61 -  unfolding plus_prod_def by simp
    5.62 -
    5.63 -lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
    5.64 -  unfolding minus_prod_def by simp
    5.65 -
    5.66 -lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
    5.67 -  unfolding minus_prod_def by simp
    5.68 -
    5.69 -lemma fst_uminus [simp]: "fst (- x) = - fst x"
    5.70 -  unfolding uminus_prod_def by simp
    5.71 -
    5.72 -lemma snd_uminus [simp]: "snd (- x) = - snd x"
    5.73 -  unfolding uminus_prod_def by simp
    5.74 -
    5.75 -lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
    5.76 -  unfolding plus_prod_def by simp
    5.77 -
    5.78 -lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
    5.79 -  unfolding minus_prod_def by simp
    5.80 -
    5.81 -lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
    5.82 -  unfolding uminus_prod_def by simp
    5.83 -
    5.84 -subsection \<open>Class instances\<close>
    5.85 -
    5.86 -instance prod :: (semigroup_add, semigroup_add) semigroup_add
    5.87 -  by standard (simp add: prod_eq_iff add.assoc)
    5.88 -
    5.89 -instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    5.90 -  by standard (simp add: prod_eq_iff add.commute)
    5.91 -
    5.92 -instance prod :: (monoid_add, monoid_add) monoid_add
    5.93 -  by standard (simp_all add: prod_eq_iff)
    5.94 -
    5.95 -instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    5.96 -  by standard (simp add: prod_eq_iff)
    5.97 -
    5.98 -instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
    5.99 -    by standard (simp_all add: prod_eq_iff)
   5.100 -
   5.101 -instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   5.102 -    by standard (simp_all add: prod_eq_iff diff_diff_eq)
   5.103 -
   5.104 -instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   5.105 -
   5.106 -instance prod :: (group_add, group_add) group_add
   5.107 -  by standard (simp_all add: prod_eq_iff)
   5.108 -
   5.109 -instance prod :: (ab_group_add, ab_group_add) ab_group_add
   5.110 -  by standard (simp_all add: prod_eq_iff)
   5.111 -
   5.112 -lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
   5.113 -proof (cases "finite A")
   5.114 -  case True
   5.115 -  then show ?thesis by induct simp_all
   5.116 -next
   5.117 -  case False
   5.118 -  then show ?thesis by simp
   5.119 -qed
   5.120 -
   5.121 -lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
   5.122 -proof (cases "finite A")
   5.123 -  case True
   5.124 -  then show ?thesis by induct simp_all
   5.125 -next
   5.126 -  case False
   5.127 -  then show ?thesis by simp
   5.128 -qed
   5.129 -
   5.130 -lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
   5.131 -proof (cases "finite A")
   5.132 -  case True
   5.133 -  then show ?thesis by induct (simp_all add: zero_prod_def)
   5.134 -next
   5.135 -  case False
   5.136 -  then show ?thesis by (simp add: zero_prod_def)
   5.137 -qed
   5.138 -
   5.139 -end