add new theory Product_plus.thy to Library
authorhuffman
Fri Feb 20 07:41:41 2009 -0800 (2009-02-20)
changeset 30018690c65b8ad1a
parent 30014 03b46412760e
child 30019 a2f19e0a28b2
add new theory Product_plus.thy to Library
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Product_plus.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Feb 20 14:49:39 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Feb 20 07:41:41 2009 -0800
     1.3 @@ -339,6 +339,7 @@
     1.4    Library/Random.thy	Library/Quickcheck.thy	\
     1.5    Library/Poly_Deriv.thy \
     1.6    Library/Polynomial.thy \
     1.7 +  Library/Product_plus.thy \
     1.8    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
     1.9    Library/reify_data.ML Library/reflection.ML
    1.10  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
     2.1 --- a/src/HOL/Library/Library.thy	Fri Feb 20 14:49:39 2009 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Fri Feb 20 07:41:41 2009 -0800
     2.3 @@ -41,6 +41,7 @@
     2.4    Poly_Deriv
     2.5    Polynomial
     2.6    Primes
     2.7 +  Product_plus
     2.8    Quickcheck
     2.9    Quicksort
    2.10    Quotient
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Product_plus.thy	Fri Feb 20 07:41:41 2009 -0800
     3.3 @@ -0,0 +1,115 @@
     3.4 +(*  Title:      HOL/Library/Product_plus.thy
     3.5 +    Author:     Brian Huffman
     3.6 +*)
     3.7 +
     3.8 +header {* Additive group operations on product types *}
     3.9 +
    3.10 +theory Product_plus
    3.11 +imports Main
    3.12 +begin
    3.13 +
    3.14 +subsection {* Operations *}
    3.15 +
    3.16 +instantiation "*" :: (zero, zero) zero
    3.17 +begin
    3.18 +
    3.19 +definition zero_prod_def: "0 = (0, 0)"
    3.20 +
    3.21 +instance ..
    3.22 +end
    3.23 +
    3.24 +instantiation "*" :: (plus, plus) plus
    3.25 +begin
    3.26 +
    3.27 +definition plus_prod_def:
    3.28 +  "x + y = (fst x + fst y, snd x + snd y)"
    3.29 +
    3.30 +instance ..
    3.31 +end
    3.32 +
    3.33 +instantiation "*" :: (minus, minus) minus
    3.34 +begin
    3.35 +
    3.36 +definition minus_prod_def:
    3.37 +  "x - y = (fst x - fst y, snd x - snd y)"
    3.38 +
    3.39 +instance ..
    3.40 +end
    3.41 +
    3.42 +instantiation "*" :: (uminus, uminus) uminus
    3.43 +begin
    3.44 +
    3.45 +definition uminus_prod_def:
    3.46 +  "- x = (- fst x, - snd x)"
    3.47 +
    3.48 +instance ..
    3.49 +end
    3.50 +
    3.51 +lemma fst_zero [simp]: "fst 0 = 0"
    3.52 +  unfolding zero_prod_def by simp
    3.53 +
    3.54 +lemma snd_zero [simp]: "snd 0 = 0"
    3.55 +  unfolding zero_prod_def by simp
    3.56 +
    3.57 +lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
    3.58 +  unfolding plus_prod_def by simp
    3.59 +
    3.60 +lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
    3.61 +  unfolding plus_prod_def by simp
    3.62 +
    3.63 +lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
    3.64 +  unfolding minus_prod_def by simp
    3.65 +
    3.66 +lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
    3.67 +  unfolding minus_prod_def by simp
    3.68 +
    3.69 +lemma fst_uminus [simp]: "fst (- x) = - fst x"
    3.70 +  unfolding uminus_prod_def by simp
    3.71 +
    3.72 +lemma snd_uminus [simp]: "snd (- x) = - snd x"
    3.73 +  unfolding uminus_prod_def by simp
    3.74 +
    3.75 +lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
    3.76 +  unfolding plus_prod_def by simp
    3.77 +
    3.78 +lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
    3.79 +  unfolding minus_prod_def by simp
    3.80 +
    3.81 +lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
    3.82 +  unfolding uminus_prod_def by simp
    3.83 +
    3.84 +lemmas expand_prod_eq = Pair_fst_snd_eq
    3.85 +
    3.86 +
    3.87 +subsection {* Class instances *}
    3.88 +
    3.89 +instance "*" :: (semigroup_add, semigroup_add) semigroup_add
    3.90 +  by default (simp add: expand_prod_eq add_assoc)
    3.91 +
    3.92 +instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    3.93 +  by default (simp add: expand_prod_eq add_commute)
    3.94 +
    3.95 +instance "*" :: (monoid_add, monoid_add) monoid_add
    3.96 +  by default (simp_all add: expand_prod_eq)
    3.97 +
    3.98 +instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    3.99 +  by default (simp add: expand_prod_eq)
   3.100 +
   3.101 +instance "*" ::
   3.102 +  (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
   3.103 +    by default (simp_all add: expand_prod_eq)
   3.104 +
   3.105 +instance "*" ::
   3.106 +  (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   3.107 +    by default (simp add: expand_prod_eq)
   3.108 +
   3.109 +instance "*" ::
   3.110 +  (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   3.111 +
   3.112 +instance "*" :: (group_add, group_add) group_add
   3.113 +  by default (simp_all add: expand_prod_eq diff_minus)
   3.114 +
   3.115 +instance "*" :: (ab_group_add, ab_group_add) ab_group_add
   3.116 +  by default (simp_all add: expand_prod_eq)
   3.117 +
   3.118 +end