# HG changeset patch
# User hoelzl
# Date 1475242543 -7200
# Node ID c98d1dd7eba13cd7cd0e65add3765483b953aecf
# Parent  da89140186e2e42702e73912059d1ee0a6223b5e
Library: fix name Product_plus to Product_Plus

diff -r da89140186e2 -r c98d1dd7eba1 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Fri Sep 30 15:35:37 2016 +0200
+++ b/src/HOL/Analysis/Product_Vector.thy	Fri Sep 30 15:35:43 2016 +0200
@@ -7,7 +7,7 @@
 theory Product_Vector
 imports
   Inner_Product
-  "~~/src/HOL/Library/Product_plus"
+  "~~/src/HOL/Library/Product_Plus"
 begin
 
 subsection \<open>Product is a real vector space\<close>
diff -r da89140186e2 -r c98d1dd7eba1 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Sep 30 15:35:37 2016 +0200
+++ b/src/HOL/Library/Library.thy	Fri Sep 30 15:35:43 2016 +0200
@@ -61,7 +61,7 @@
   Polynomial
   Polynomial_FPS
   Preorder
-  Product_plus
+  Product_Plus
   Quadratic_Discriminant
   Quotient_List
   Quotient_Option
diff -r da89140186e2 -r c98d1dd7eba1 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Fri Sep 30 15:35:37 2016 +0200
+++ b/src/HOL/Library/Product_Order.thy	Fri Sep 30 15:35:43 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Pointwise order on product types\<close>
 
 theory Product_Order
-imports Product_plus
+imports Product_Plus
 begin
 
 subsection \<open>Pointwise ordering\<close>
diff -r da89140186e2 -r c98d1dd7eba1 src/HOL/Library/Product_Plus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Product_Plus.thy	Fri Sep 30 15:35:43 2016 +0200
@@ -0,0 +1,136 @@
+(*  Title:      HOL/Library/Product_Plus.thy
+    Author:     Brian Huffman
+*)
+
+section \<open>Additive group operations on product types\<close>
+
+theory Product_Plus
+imports Main
+begin
+
+subsection \<open>Operations\<close>
+
+instantiation prod :: (zero, zero) zero
+begin
+
+definition zero_prod_def: "0 = (0, 0)"
+
+instance ..
+end
+
+instantiation prod :: (plus, plus) plus
+begin
+
+definition plus_prod_def:
+  "x + y = (fst x + fst y, snd x + snd y)"
+
+instance ..
+end
+
+instantiation prod :: (minus, minus) minus
+begin
+
+definition minus_prod_def:
+  "x - y = (fst x - fst y, snd x - snd y)"
+
+instance ..
+end
+
+instantiation prod :: (uminus, uminus) uminus
+begin
+
+definition uminus_prod_def:
+  "- x = (- fst x, - snd x)"
+
+instance ..
+end
+
+lemma fst_zero [simp]: "fst 0 = 0"
+  unfolding zero_prod_def by simp
+
+lemma snd_zero [simp]: "snd 0 = 0"
+  unfolding zero_prod_def by simp
+
+lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
+  unfolding plus_prod_def by simp
+
+lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
+  unfolding plus_prod_def by simp
+
+lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
+  unfolding minus_prod_def by simp
+
+lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
+  unfolding minus_prod_def by simp
+
+lemma fst_uminus [simp]: "fst (- x) = - fst x"
+  unfolding uminus_prod_def by simp
+
+lemma snd_uminus [simp]: "snd (- x) = - snd x"
+  unfolding uminus_prod_def by simp
+
+lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
+  unfolding plus_prod_def by simp
+
+lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
+  unfolding minus_prod_def by simp
+
+lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
+  unfolding uminus_prod_def by simp
+
+subsection \<open>Class instances\<close>
+
+instance prod :: (semigroup_add, semigroup_add) semigroup_add
+  by standard (simp add: prod_eq_iff add.assoc)
+
+instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
+  by standard (simp add: prod_eq_iff add.commute)
+
+instance prod :: (monoid_add, monoid_add) monoid_add
+  by standard (simp_all add: prod_eq_iff)
+
+instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
+  by standard (simp add: prod_eq_iff)
+
+instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
+    by standard (simp_all add: prod_eq_iff)
+
+instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
+    by standard (simp_all add: prod_eq_iff diff_diff_eq)
+
+instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
+
+instance prod :: (group_add, group_add) group_add
+  by standard (simp_all add: prod_eq_iff)
+
+instance prod :: (ab_group_add, ab_group_add) ab_group_add
+  by standard (simp_all add: prod_eq_iff)
+
+lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
+proof (cases "finite A")
+  case True
+  then show ?thesis by induct simp_all
+next
+  case False
+  then show ?thesis by simp
+qed
+
+lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
+proof (cases "finite A")
+  case True
+  then show ?thesis by induct simp_all
+next
+  case False
+  then show ?thesis by simp
+qed
+
+lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
+proof (cases "finite A")
+  case True
+  then show ?thesis by induct (simp_all add: zero_prod_def)
+next
+  case False
+  then show ?thesis by (simp add: zero_prod_def)
+qed
+
+end
diff -r da89140186e2 -r c98d1dd7eba1 src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Fri Sep 30 15:35:37 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,136 +0,0 @@
-(*  Title:      HOL/Library/Product_plus.thy
-    Author:     Brian Huffman
-*)
-
-section \<open>Additive group operations on product types\<close>
-
-theory Product_plus
-imports Main
-begin
-
-subsection \<open>Operations\<close>
-
-instantiation prod :: (zero, zero) zero
-begin
-
-definition zero_prod_def: "0 = (0, 0)"
-
-instance ..
-end
-
-instantiation prod :: (plus, plus) plus
-begin
-
-definition plus_prod_def:
-  "x + y = (fst x + fst y, snd x + snd y)"
-
-instance ..
-end
-
-instantiation prod :: (minus, minus) minus
-begin
-
-definition minus_prod_def:
-  "x - y = (fst x - fst y, snd x - snd y)"
-
-instance ..
-end
-
-instantiation prod :: (uminus, uminus) uminus
-begin
-
-definition uminus_prod_def:
-  "- x = (- fst x, - snd x)"
-
-instance ..
-end
-
-lemma fst_zero [simp]: "fst 0 = 0"
-  unfolding zero_prod_def by simp
-
-lemma snd_zero [simp]: "snd 0 = 0"
-  unfolding zero_prod_def by simp
-
-lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
-  unfolding plus_prod_def by simp
-
-lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
-  unfolding plus_prod_def by simp
-
-lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
-  unfolding minus_prod_def by simp
-
-lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
-  unfolding minus_prod_def by simp
-
-lemma fst_uminus [simp]: "fst (- x) = - fst x"
-  unfolding uminus_prod_def by simp
-
-lemma snd_uminus [simp]: "snd (- x) = - snd x"
-  unfolding uminus_prod_def by simp
-
-lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
-  unfolding plus_prod_def by simp
-
-lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
-  unfolding minus_prod_def by simp
-
-lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
-  unfolding uminus_prod_def by simp
-
-subsection \<open>Class instances\<close>
-
-instance prod :: (semigroup_add, semigroup_add) semigroup_add
-  by standard (simp add: prod_eq_iff add.assoc)
-
-instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
-  by standard (simp add: prod_eq_iff add.commute)
-
-instance prod :: (monoid_add, monoid_add) monoid_add
-  by standard (simp_all add: prod_eq_iff)
-
-instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
-  by standard (simp add: prod_eq_iff)
-
-instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
-    by standard (simp_all add: prod_eq_iff)
-
-instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
-    by standard (simp_all add: prod_eq_iff diff_diff_eq)
-
-instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
-
-instance prod :: (group_add, group_add) group_add
-  by standard (simp_all add: prod_eq_iff)
-
-instance prod :: (ab_group_add, ab_group_add) ab_group_add
-  by standard (simp_all add: prod_eq_iff)
-
-lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-proof (cases "finite A")
-  case True
-  then show ?thesis by induct simp_all
-next
-  case False
-  then show ?thesis by simp
-qed
-
-lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-proof (cases "finite A")
-  case True
-  then show ?thesis by induct simp_all
-next
-  case False
-  then show ?thesis by simp
-qed
-
-lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
-proof (cases "finite A")
-  case True
-  then show ?thesis by induct (simp_all add: zero_prod_def)
-next
-  case False
-  then show ?thesis by (simp add: zero_prod_def)
-qed
-
-end