1.1 --- a/src/HOL/Finite_Set.thy Tue May 11 14:00:02 2004 +0200
1.2 +++ b/src/HOL/Finite_Set.thy Tue May 11 20:11:08 2004 +0200
1.3 @@ -742,15 +742,15 @@
1.4 subsection {* Generalized summation over a set *}
1.5
1.6 constdefs
1.7 - setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
1.8 + setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
1.9 "setsum f A == if finite A then fold (op + o f) 0 A else 0"
1.10
1.11 syntax
1.12 - "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("(3\<Sum>_:_. _)" [0, 51, 10] 10)
1.13 + "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_:_. _)" [0, 51, 10] 10)
1.14 syntax (xsymbols)
1.15 - "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
1.16 + "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
1.17 syntax (HTML output)
1.18 - "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
1.19 + "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
1.20 translations
1.21 "\<Sum>i:A. b" == "setsum (%i. b) A" -- {* Beware of argument permutation! *}
1.22
1.23 @@ -761,7 +761,7 @@
1.24 lemma setsum_insert [simp]:
1.25 "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
1.26 by (simp add: setsum_def
1.27 - LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
1.28 + LC.fold_insert [OF LC.intro] add_left_commute)
1.29
1.30 lemma setsum_reindex [rule_format]: "finite B ==>
1.31 inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
1.32 @@ -820,7 +820,7 @@
1.33 ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
1.34 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
1.35 apply (induct set: Finites, simp)
1.36 - apply (simp add: plus_ac0 Int_insert_left insert_absorb)
1.37 + apply (simp add: add_ac Int_insert_left insert_absorb)
1.38 done
1.39
1.40 lemma setsum_Un_disjoint: "finite A ==> finite B
1.41 @@ -874,7 +874,7 @@
1.42 apply (case_tac "finite A")
1.43 prefer 2 apply (simp add: setsum_def)
1.44 apply (erule finite_induct, auto)
1.45 - apply (simp add: plus_ac0)
1.46 + apply (simp add: add_ac)
1.47 done
1.48
1.49 subsubsection {* Properties in more restricted classes of structures *}
1.50 @@ -892,18 +892,18 @@
1.51
1.52 lemma setsum_constant_nat [simp]:
1.53 "finite A ==> (\<Sum>x: A. y) = (card A) * y"
1.54 - -- {* Later generalized to any semiring. *}
1.55 + -- {* Later generalized to any comm_semiring_1_cancel. *}
1.56 by (erule finite_induct, auto)
1.57
1.58 lemma setsum_Un: "finite A ==> finite B ==>
1.59 (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
1.60 -- {* For the natural numbers, we have subtraction. *}
1.61 - by (subst setsum_Un_Int [symmetric], auto)
1.62 + by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
1.63
1.64 lemma setsum_Un_ring: "finite A ==> finite B ==>
1.65 - (setsum f (A Un B) :: 'a :: ring) =
1.66 + (setsum f (A Un B) :: 'a :: comm_ring_1) =
1.67 setsum f A + setsum f B - setsum f (A Int B)"
1.68 - by (subst setsum_Un_Int [symmetric], auto)
1.69 + by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
1.70
1.71 lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
1.72 (if a:A then setsum f A - f a else setsum f A)"
1.73 @@ -914,16 +914,16 @@
1.74 apply (drule_tac a = a in mk_disjoint_insert, auto)
1.75 done
1.76
1.77 -lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
1.78 +lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::comm_ring_1) A =
1.79 - setsum f A"
1.80 by (induct set: Finites, auto)
1.81
1.82 -lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
1.83 +lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::comm_ring_1) - g x) A =
1.84 setsum f A - setsum g A"
1.85 by (simp add: diff_minus setsum_addf setsum_negf)
1.86
1.87 lemma setsum_nonneg: "[| finite A;
1.88 - \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
1.89 + \<forall>x \<in> A. (0::'a::ordered_semidom) \<le> f x |] ==>
1.90 0 \<le> setsum f A";
1.91 apply (induct set: Finites, auto)
1.92 apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
1.93 @@ -983,16 +983,16 @@
1.94 subsection {* Generalized product over a set *}
1.95
1.96 constdefs
1.97 - setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
1.98 + setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
1.99 "setprod f A == if finite A then fold (op * o f) 1 A else 1"
1.100
1.101 syntax
1.102 - "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1" ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
1.103 + "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
1.104
1.105 syntax (xsymbols)
1.106 - "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1.107 + "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1.108 syntax (HTML output)
1.109 - "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1.110 + "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1.111 translations
1.112 "\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *}
1.113
1.114 @@ -1002,7 +1002,7 @@
1.115 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
1.116 setprod f (insert a A) = f a * setprod f A"
1.117 by (auto simp add: setprod_def LC_def LC.fold_insert
1.118 - times_ac1_left_commute)
1.119 + mult_left_commute)
1.120
1.121 lemma setprod_reindex [rule_format]: "finite B ==>
1.122 inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
1.123 @@ -1043,7 +1043,7 @@
1.124
1.125 lemma setprod_1: "setprod (%i. 1) A = 1"
1.126 apply (case_tac "finite A")
1.127 - apply (erule finite_induct, auto simp add: times_ac1)
1.128 + apply (erule finite_induct, auto simp add: mult_ac)
1.129 apply (simp add: setprod_def)
1.130 done
1.131
1.132 @@ -1056,13 +1056,13 @@
1.133 lemma setprod_Un_Int: "finite A ==> finite B
1.134 ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
1.135 apply (induct set: Finites, simp)
1.136 - apply (simp add: times_ac1 insert_absorb)
1.137 - apply (simp add: times_ac1 Int_insert_left insert_absorb)
1.138 + apply (simp add: mult_ac insert_absorb)
1.139 + apply (simp add: mult_ac Int_insert_left insert_absorb)
1.140 done
1.141
1.142 lemma setprod_Un_disjoint: "finite A ==> finite B
1.143 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
1.144 - apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
1.145 + apply (subst setprod_Un_Int [symmetric], auto simp add: mult_ac)
1.146 done
1.147
1.148 lemma setprod_UN_disjoint:
1.149 @@ -1110,9 +1110,9 @@
1.150 lemma setprod_timesf: "setprod (%x. f x * g x) A =
1.151 (setprod f A * setprod g A)"
1.152 apply (case_tac "finite A")
1.153 - prefer 2 apply (simp add: setprod_def times_ac1)
1.154 + prefer 2 apply (simp add: setprod_def mult_ac)
1.155 apply (erule finite_induct, auto)
1.156 - apply (simp add: times_ac1)
1.157 + apply (simp add: mult_ac)
1.158 done
1.159
1.160 subsubsection {* Properties in more restricted classes of structures *}
1.161 @@ -1127,13 +1127,13 @@
1.162 apply (auto simp add: power_Suc)
1.163 done
1.164
1.165 -lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
1.166 +lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==>
1.167 setprod f A = 0"
1.168 apply (induct set: Finites, force, clarsimp)
1.169 apply (erule disjE, auto)
1.170 done
1.171
1.172 -lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
1.173 +lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_idom) \<le> f x)
1.174 --> 0 \<le> setprod f A"
1.175 apply (case_tac "finite A")
1.176 apply (induct set: Finites, force, clarsimp)
1.177 @@ -1142,7 +1142,7 @@
1.178 apply (auto simp add: setprod_def)
1.179 done
1.180
1.181 -lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
1.182 +lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
1.183 --> 0 < setprod f A"
1.184 apply (case_tac "finite A")
1.185 apply (induct set: Finites, force, clarsimp)
1.186 @@ -1152,13 +1152,13 @@
1.187 done
1.188
1.189 lemma setprod_nonzero [rule_format]:
1.190 - "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
1.191 + "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
1.192 finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
1.193 apply (erule finite_induct, auto)
1.194 done
1.195
1.196 lemma setprod_zero_eq:
1.197 - "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
1.198 + "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
1.199 finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
1.200 apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
1.201 done