|
(* 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_sum: "fst (\x\A. f x) = (\x\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_sum: "snd (\x\A. f x) = (\x\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 sum_prod: "(\x\A. (f x, g x)) = (\x\A. f x, \x\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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
