1.1 --- a/src/HOL/Algebra/CRing.thy Fri Mar 14 12:03:23 2003 +0100
1.2 +++ b/src/HOL/Algebra/CRing.thy Fri Mar 14 18:00:16 2003 +0100
1.3 @@ -5,9 +5,7 @@
1.4 Copyright: Clemens Ballarin
1.5 *)
1.6
1.7 -header {* The algebraic hierarchy of rings as axiomatic classes *}
1.8 -
1.9 -theory CRing = Group
1.10 +theory CRing = Summation
1.11 files ("ringsimp.ML"):
1.12
1.13 section {* The Algebraic Hierarchy of Rings *}
1.14 @@ -37,7 +35,13 @@
1.15 divide_def: "a / b = a * inverse b"
1.16 power_def: "a ^ n = nat_rec 1 (%u b. b * a) n"
1.17 *)
1.18 -subsection {* Basic Facts *}
1.19 +
1.20 +locale "domain" = cring +
1.21 + assumes one_not_zero [simp]: "\<one> ~= \<zero>"
1.22 + and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
1.23 + a = \<zero> | b = \<zero>"
1.24 +
1.25 +subsection {* Basic Facts of Rings *}
1.26
1.27 lemma (in cring) a_magma [simp, intro]:
1.28 "magma (| carrier = carrier R,
1.29 @@ -73,39 +77,42 @@
1.30 mult = add R, one = zero R, m_inv = a_inv R |)"
1.31 by (simp add: abelian_semigroup_def)
1.32
1.33 -lemma (in cring) a_abelian_group:
1.34 - "abelian_group (| carrier = carrier R,
1.35 - mult = add R, one = zero R, m_inv = a_inv R |)"
1.36 - by (simp add: abelian_group_def)
1.37 +lemmas group_record_simps = semigroup.simps monoid.simps group.simps
1.38
1.39 lemmas (in cring) a_closed [intro, simp] =
1.40 - magma.m_closed [OF a_magma, simplified]
1.41 + magma.m_closed [OF a_magma, simplified group_record_simps]
1.42
1.43 lemmas (in cring) zero_closed [intro, simp] =
1.44 - l_one.one_closed [OF a_l_one, simplified]
1.45 + l_one.one_closed [OF a_l_one, simplified group_record_simps]
1.46
1.47 lemmas (in cring) a_inv_closed [intro, simp] =
1.48 - group.inv_closed [OF a_group, simplified]
1.49 + group.inv_closed [OF a_group, simplified group_record_simps]
1.50
1.51 lemma (in cring) minus_closed [intro, simp]:
1.52 "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
1.53 by (simp add: minus_def)
1.54
1.55 -lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified]
1.56 +lemmas (in cring) a_l_cancel [simp] =
1.57 + group.l_cancel [OF a_group, simplified group_record_simps]
1.58
1.59 -lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified]
1.60 +lemmas (in cring) a_r_cancel [simp] =
1.61 + group.r_cancel [OF a_group, simplified group_record_simps]
1.62
1.63 -lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified]
1.64 +lemmas (in cring) a_assoc =
1.65 + semigroup.m_assoc [OF a_semigroup, simplified group_record_simps]
1.66
1.67 -lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified]
1.68 +lemmas (in cring) l_zero [simp] =
1.69 + l_one.l_one [OF a_l_one, simplified group_record_simps]
1.70
1.71 -lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified]
1.72 +lemmas (in cring) l_neg =
1.73 + group.l_inv [OF a_group, simplified group_record_simps]
1.74
1.75 -lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup,
1.76 - simplified]
1.77 +lemmas (in cring) a_comm =
1.78 + abelian_semigroup.m_comm [OF a_abelian_semigroup,
1.79 + simplified group_record_simps]
1.80
1.81 lemmas (in cring) a_lcomm =
1.82 - abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified]
1.83 + abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified group_record_simps]
1.84
1.85 lemma (in cring) r_zero [simp]:
1.86 "x \<in> carrier R ==> x \<oplus> \<zero> = x"
1.87 @@ -117,11 +124,12 @@
1.88 using group.r_inv [OF a_group]
1.89 by simp
1.90
1.91 -lemmas (in cring) minus_zero [simp] = group.inv_one [OF a_group, simplified]
1.92 +lemmas (in cring) minus_zero [simp] =
1.93 + group.inv_one [OF a_group, simplified group_record_simps]
1.94
1.95 lemma (in cring) minus_minus [simp]:
1.96 "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
1.97 - using group.inv_inv [OF a_group, simplified]
1.98 + using group.inv_inv [OF a_group, simplified group_record_simps]
1.99 by simp
1.100
1.101 lemma (in cring) minus_add:
1.102 @@ -217,6 +225,8 @@
1.103 {* Method.ctxt_args cring_normalise *}
1.104 {* computes distributive normal form in commutative rings (locales version) *}
1.105
1.106 +text {* Two examples for use of method algebra *}
1.107 +
1.108 lemma
1.109 includes cring R + cring S
1.110 shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
1.111 @@ -228,4 +238,225 @@
1.112 shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
1.113 by algebra
1.114
1.115 +subsection {* Sums over Finite Sets *}
1.116 +
1.117 +text {*
1.118 + This definition makes it easy to lift lemmas from @{term finprod}.
1.119 +*}
1.120 +
1.121 +constdefs
1.122 + finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
1.123 + "finsum R f A == finprod (| carrier = carrier R,
1.124 + mult = add R, one = zero R, m_inv = a_inv R |) f A"
1.125 +
1.126 +lemma (in cring) a_abelian_monoid:
1.127 + "abelian_monoid (| carrier = carrier R,
1.128 + mult = add R, one = zero R, m_inv = a_inv R |)"
1.129 + by (simp add: abelian_monoid_def)
1.130 +
1.131 +(*
1.132 + lemmas (in cring) finsum_empty [simp] =
1.133 + abelian_monoid.finprod_empty [OF a_abelian_monoid, simplified]
1.134 + is dangeous, because attributes (like simplified) are applied upon opening
1.135 + the locale, simplified refers to the simpset at that time!!!
1.136 +*)
1.137 +
1.138 +lemmas (in cring) finsum_empty [simp] =
1.139 + abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
1.140 + simplified group_record_simps]
1.141 +
1.142 +lemmas (in cring) finsum_insert [simp] =
1.143 + abelian_monoid.finprod_insert [OF a_abelian_monoid, folded finsum_def,
1.144 + simplified group_record_simps]
1.145 +
1.146 +lemmas (in cring) finsum_zero =
1.147 + abelian_monoid.finprod_one [OF a_abelian_monoid, folded finsum_def,
1.148 + simplified group_record_simps]
1.149 +
1.150 +lemmas (in cring) finsum_closed [simp] =
1.151 + abelian_monoid.finprod_closed [OF a_abelian_monoid, folded finsum_def,
1.152 + simplified group_record_simps]
1.153 +
1.154 +lemmas (in cring) finsum_Un_Int =
1.155 + abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, folded finsum_def,
1.156 + simplified group_record_simps]
1.157 +
1.158 +lemmas (in cring) finsum_Un_disjoint =
1.159 + abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, folded finsum_def,
1.160 + simplified group_record_simps]
1.161 +
1.162 +lemmas (in cring) finsum_addf =
1.163 + abelian_monoid.finprod_multf [OF a_abelian_monoid, folded finsum_def,
1.164 + simplified group_record_simps]
1.165 +
1.166 +lemmas (in cring) finsum_cong =
1.167 + abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def,
1.168 + simplified group_record_simps]
1.169 +
1.170 +lemmas (in cring) finsum_0 [simp] =
1.171 + abelian_monoid.finprod_0 [OF a_abelian_monoid, folded finsum_def,
1.172 + simplified group_record_simps]
1.173 +
1.174 +lemmas (in cring) finsum_Suc [simp] =
1.175 + abelian_monoid.finprod_Suc [OF a_abelian_monoid, folded finsum_def,
1.176 + simplified group_record_simps]
1.177 +
1.178 +lemmas (in cring) finsum_Suc2 =
1.179 + abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, folded finsum_def,
1.180 + simplified group_record_simps]
1.181 +
1.182 +lemmas (in cring) finsum_add [simp] =
1.183 + abelian_monoid.finprod_mult [OF a_abelian_monoid, folded finsum_def,
1.184 + simplified group_record_simps]
1.185 +
1.186 +lemmas (in cring) finsum_cong' [cong] =
1.187 + abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def,
1.188 + simplified group_record_simps]
1.189 +
1.190 +(*
1.191 +lemma (in cring) finsum_empty [simp]:
1.192 + "finsum R f {} = \<zero>"
1.193 + by (simp add: finsum_def
1.194 + abelian_monoid.finprod_empty [OF a_abelian_monoid])
1.195 +
1.196 +lemma (in cring) finsum_insert [simp]:
1.197 + "[| finite F; a \<notin> F; f : F -> carrier R; f a \<in> carrier R |] ==>
1.198 + finsum R f (insert a F) = f a \<oplus> finsum R f F"
1.199 + by (simp add: finsum_def
1.200 + abelian_monoid.finprod_insert [OF a_abelian_monoid])
1.201 +
1.202 +lemma (in cring) finsum_zero:
1.203 + "finite A ==> finsum R (%i. \<zero>) A = \<zero>"
1.204 + by (simp add: finsum_def
1.205 + abelian_monoid.finprod_one [OF a_abelian_monoid, simplified])
1.206 +
1.207 +lemma (in cring) finsum_closed [simp]:
1.208 + "[| finite A; f : A -> carrier R |] ==> finsum R f A \<in> carrier R"
1.209 + by (simp only: finsum_def
1.210 + abelian_monoid.finprod_closed [OF a_abelian_monoid, simplified])
1.211 +
1.212 +lemma (in cring) finsum_Un_Int:
1.213 + "[| finite A; finite B; g \<in> A -> carrier R; g \<in> B -> carrier R |] ==>
1.214 + finsum R g (A Un B) \<oplus> finsum R g (A Int B) =
1.215 + finsum R g A \<oplus> finsum R g B"
1.216 + by (simp only: finsum_def
1.217 + abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, simplified])
1.218 +
1.219 +lemma (in cring) finsum_Un_disjoint:
1.220 + "[| finite A; finite B; A Int B = {};
1.221 + g \<in> A -> carrier R; g \<in> B -> carrier R |]
1.222 + ==> finsum R g (A Un B) = finsum R g A \<oplus> finsum R g B"
1.223 + by (simp only: finsum_def
1.224 + abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, simplified])
1.225 +
1.226 +lemma (in cring) finsum_addf:
1.227 + "[| finite A; f \<in> A -> carrier R; g \<in> A -> carrier R |] ==>
1.228 + finsum R (%x. f x \<oplus> g x) A = (finsum R f A \<oplus> finsum R g A)"
1.229 + by (simp only: finsum_def
1.230 + abelian_monoid.finprod_multf [OF a_abelian_monoid, simplified])
1.231 +
1.232 +lemma (in cring) finsum_cong:
1.233 + "[| A = B; g : B -> carrier R;
1.234 + !!i. i : B ==> f i = g i |] ==> finsum R f A = finsum R g B"
1.235 + apply (simp only: finsum_def)
1.236 + apply (rule abelian_monoid.finprod_cong [OF a_abelian_monoid, simplified])
1.237 + apply simp_all
1.238 + done
1.239 +
1.240 +lemma (in cring) finsum_0 [simp]:
1.241 + "f \<in> {0::nat} -> carrier R ==> finsum R f {..0} = f 0"
1.242 + by (simp add: finsum_def
1.243 + abelian_monoid.finprod_0 [OF a_abelian_monoid, simplified])
1.244 +
1.245 +lemma (in cring) finsum_Suc [simp]:
1.246 + "f \<in> {..Suc n} -> carrier R ==>
1.247 + finsum R f {..Suc n} = (f (Suc n) \<oplus> finsum R f {..n})"
1.248 + by (simp add: finsum_def
1.249 + abelian_monoid.finprod_Suc [OF a_abelian_monoid, simplified])
1.250 +
1.251 +lemma (in cring) finsum_Suc2:
1.252 + "f \<in> {..Suc n} -> carrier R ==>
1.253 + finsum R f {..Suc n} = (finsum R (%i. f (Suc i)) {..n} \<oplus> f 0)"
1.254 + by (simp only: finsum_def
1.255 + abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, simplified])
1.256 +
1.257 +lemma (in cring) finsum_add [simp]:
1.258 + "[| f : {..n} -> carrier R; g : {..n} -> carrier R |] ==>
1.259 + finsum R (%i. f i \<oplus> g i) {..n::nat} =
1.260 + finsum R f {..n} \<oplus> finsum R g {..n}"
1.261 + by (simp only: finsum_def
1.262 + abelian_monoid.finprod_mult [OF a_abelian_monoid, simplified])
1.263 +
1.264 +lemma (in cring) finsum_cong' [cong]:
1.265 + "[| A = B; !!i. i : B ==> f i = g i;
1.266 + g \<in> B -> carrier R = True |] ==> finsum R f A = finsum R g B"
1.267 + apply (simp only: finsum_def)
1.268 + apply (rule abelian_monoid.finprod_cong' [OF a_abelian_monoid, simplified])
1.269 + apply simp_all
1.270 + done
1.271 +*)
1.272 +
1.273 +text {*Usually, if this rule causes a failed congruence proof error,
1.274 + the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
1.275 + Adding @{thm [source] Pi_def} to the simpset is often useful. *}
1.276 +
1.277 +lemma (in cring) finsum_ldistr:
1.278 + "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
1.279 + finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
1.280 +proof (induct set: Finites)
1.281 + case empty then show ?case by simp
1.282 +next
1.283 + case (insert F x) then show ?case by (simp add: Pi_def l_distr)
1.284 +qed
1.285 +
1.286 +lemma (in cring) finsum_rdistr:
1.287 + "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
1.288 + a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
1.289 +proof (induct set: Finites)
1.290 + case empty then show ?case by simp
1.291 +next
1.292 + case (insert F x) then show ?case by (simp add: Pi_def r_distr)
1.293 +qed
1.294 +
1.295 +subsection {* Facts of Integral Domains *}
1.296 +
1.297 +lemma (in "domain") zero_not_one [simp]:
1.298 + "\<zero> ~= \<one>"
1.299 + by (rule not_sym) simp
1.300 +
1.301 +lemma (in "domain") integral_iff: (* not by default a simp rule! *)
1.302 + "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)"
1.303 +proof
1.304 + assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
1.305 + then show "a = \<zero> | b = \<zero>" by (simp add: integral)
1.306 +next
1.307 + assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> | b = \<zero>"
1.308 + then show "a \<otimes> b = \<zero>" by auto
1.309 +qed
1.310 +
1.311 +lemma (in "domain") m_lcancel:
1.312 + assumes prem: "a ~= \<zero>"
1.313 + and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
1.314 + shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
1.315 +proof
1.316 + assume eq: "a \<otimes> b = a \<otimes> c"
1.317 + with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
1.318 + with R have "a = \<zero> | (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
1.319 + with prem and R have "b \<ominus> c = \<zero>" by auto
1.320 + with R have "b = b \<ominus> (b \<ominus> c)" by algebra
1.321 + also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
1.322 + finally show "b = c" .
1.323 +next
1.324 + assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp
1.325 +qed
1.326 +
1.327 +lemma (in "domain") m_rcancel:
1.328 + assumes prem: "a ~= \<zero>"
1.329 + and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
1.330 + shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
1.331 +proof -
1.332 + from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel)
1.333 + with R show ?thesis by algebra
1.334 +qed
1.335 +
1.336 end
2.1 --- a/src/HOL/Algebra/Summation.thy Fri Mar 14 12:03:23 2003 +0100
2.2 +++ b/src/HOL/Algebra/Summation.thy Fri Mar 14 18:00:16 2003 +0100
2.3 @@ -5,9 +5,9 @@
2.4 This file is largely based on HOL/Finite_Set.thy.
2.5 *)
2.6
2.7 -theory FoldSet = Group:
2.8 +header {* Summation Operator *}
2.9
2.10 -section {* Summation operator *}
2.11 +theory Summation = Group:
2.12
2.13 (* Instantiation of LC from Finite_Set.thy is not possible,
2.14 because here we have explicit typing rules like x : carrier G.
2.15 @@ -293,18 +293,20 @@
2.16 by (simp add: foldD_Un_Int
2.17 left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
2.18
2.19 -subsection {* A Product Operator for Finite Sets *}
2.20 +subsection {* Products over Finite Sets *}
2.21
2.22 -text {*
2.23 - Definition of product (or summation, if the monoid is written addivitively)
2.24 - operator.
2.25 -*}
2.26 +constdefs
2.27 + finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
2.28 + "finprod G f A == if finite A
2.29 + then foldD (carrier G) (mult G o f) (one G) A
2.30 + else arbitrary"
2.31
2.32 +(*
2.33 locale finite_prod = abelian_monoid + var prod +
2.34 defines "prod == (%f A. if finite A
2.35 then foldD (carrier G) (op \<otimes> o f) \<one> A
2.36 else arbitrary)"
2.37 -
2.38 +*)
2.39 (* TODO: nice syntax for the summation operator inside the locale
2.40 like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
2.41
2.42 @@ -313,9 +315,9 @@
2.43 Context.>> (fn thy => (simpset_ref_of thy :=
2.44 simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
2.45
2.46 -lemma (in finite_prod) prod_empty [simp]:
2.47 - "prod f {} = \<one>"
2.48 - by (simp add: prod_def)
2.49 +lemma (in abelian_monoid) finprod_empty [simp]:
2.50 + "finprod G f {} = \<one>"
2.51 + by (simp add: finprod_def)
2.52
2.53 ML_setup {*
2.54
2.55 @@ -325,11 +327,11 @@
2.56 declare funcsetI [intro]
2.57 funcset_mem [dest]
2.58
2.59 -lemma (in finite_prod) prod_insert [simp]:
2.60 +lemma (in abelian_monoid) finprod_insert [simp]:
2.61 "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
2.62 - prod f (insert a F) = f a \<otimes> prod f F"
2.63 + finprod G f (insert a F) = f a \<otimes> finprod G f F"
2.64 apply (rule trans)
2.65 - apply (simp add: prod_def)
2.66 + apply (simp add: finprod_def)
2.67 apply (rule trans)
2.68 apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
2.69 apply simp
2.70 @@ -337,11 +339,11 @@
2.71 apply fast apply fast apply assumption
2.72 apply (fastsimp intro: m_closed)
2.73 apply simp+ apply fast
2.74 - apply (auto simp add: prod_def)
2.75 + apply (auto simp add: finprod_def)
2.76 done
2.77
2.78 -lemma (in finite_prod) prod_one:
2.79 - "finite A ==> prod (%i. \<one>) A = \<one>"
2.80 +lemma (in abelian_monoid) finprod_one:
2.81 + "finite A ==> finprod G (%i. \<one>) A = \<one>"
2.82 proof (induct set: Finites)
2.83 case empty show ?case by simp
2.84 next
2.85 @@ -350,29 +352,10 @@
2.86 with insert show ?case by simp
2.87 qed
2.88
2.89 -(*
2.90 -lemma prod_eq_0_iff [simp]:
2.91 - "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
2.92 - by (induct set: Finites) auto
2.93 -
2.94 -lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
2.95 - apply (case_tac "finite A")
2.96 - prefer 2 apply (simp add: prod_def)
2.97 - apply (erule rev_mp)
2.98 - apply (erule finite_induct)
2.99 - apply auto
2.100 - done
2.101 -
2.102 -lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
2.103 -*) -- {* Could allow many @{text "card"} proofs to be simplified. *}
2.104 -(*
2.105 - by (induct set: Finites) auto
2.106 -*)
2.107 -
2.108 -lemma (in finite_prod) prod_closed:
2.109 +lemma (in abelian_monoid) finprod_closed [simp]:
2.110 fixes A
2.111 assumes fin: "finite A" and f: "f \<in> A -> carrier G"
2.112 - shows "prod f A \<in> carrier G"
2.113 + shows "finprod G f A \<in> carrier G"
2.114 using fin f
2.115 proof induct
2.116 case empty show ?case by simp
2.117 @@ -391,50 +374,33 @@
2.118 "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
2.119 by fast
2.120
2.121 -lemma (in finite_prod) prod_Un_Int:
2.122 +lemma (in abelian_monoid) finprod_Un_Int:
2.123 "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
2.124 - prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
2.125 + finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
2.126 + finprod G g A \<otimes> finprod G g B"
2.127 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
2.128 proof (induct set: Finites)
2.129 - case empty then show ?case by (simp add: prod_closed)
2.130 + case empty then show ?case by (simp add: finprod_closed)
2.131 next
2.132 case (insert A a)
2.133 then have a: "g a \<in> carrier G" by fast
2.134 from insert have A: "g \<in> A -> carrier G" by fast
2.135 from insert A a show ?case
2.136 - by (simp add: ac Int_insert_left insert_absorb prod_closed
2.137 + by (simp add: ac Int_insert_left insert_absorb finprod_closed
2.138 Int_mono2 Un_subset_iff)
2.139 qed
2.140
2.141 -lemma (in finite_prod) prod_Un_disjoint:
2.142 +lemma (in abelian_monoid) finprod_Un_disjoint:
2.143 "[| finite A; finite B; A Int B = {};
2.144 g \<in> A -> carrier G; g \<in> B -> carrier G |]
2.145 - ==> prod g (A Un B) = prod g A \<otimes> prod g B"
2.146 - apply (subst prod_Un_Int [symmetric])
2.147 - apply (auto simp add: prod_closed)
2.148 + ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
2.149 + apply (subst finprod_Un_Int [symmetric])
2.150 + apply (auto simp add: finprod_closed)
2.151 done
2.152
2.153 -(*
2.154 -lemma prod_UN_disjoint:
2.155 - fixes f :: "'a => 'b::plus_ac0"
2.156 - shows
2.157 - "finite I ==> (ALL i:I. finite (A i)) ==>
2.158 - (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
2.159 - prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
2.160 - apply (induct set: Finites)
2.161 - apply simp
2.162 - apply atomize
2.163 - apply (subgoal_tac "ALL i:F. x \<noteq> i")
2.164 - prefer 2 apply blast
2.165 - apply (subgoal_tac "A x Int UNION F A = {}")
2.166 - prefer 2 apply blast
2.167 - apply (simp add: prod_Un_disjoint)
2.168 - done
2.169 -*)
2.170 -
2.171 -lemma (in finite_prod) prod_addf:
2.172 +lemma (in abelian_monoid) finprod_multf:
2.173 "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
2.174 - prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
2.175 + finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
2.176 proof (induct set: Finites)
2.177 case empty show ?case by simp
2.178 next
2.179 @@ -447,138 +413,85 @@
2.180 from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
2.181 by (simp add: Pi_def)
2.182 show ?case (* check if all simps are really necessary *)
2.183 - by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
2.184 + by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
2.185 qed
2.186
2.187 -(*
2.188 -lemma prod_Un: "finite A ==> finite B ==>
2.189 - (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
2.190 - apply (subst prod_Un_Int [symmetric])
2.191 - apply auto
2.192 - done
2.193 -
2.194 -lemma prod_diff1: "(prod f (A - {a}) :: nat) =
2.195 - (if a:A then prod f A - f a else prod f A)"
2.196 - apply (case_tac "finite A")
2.197 - prefer 2 apply (simp add: prod_def)
2.198 - apply (erule finite_induct)
2.199 - apply (auto simp add: insert_Diff_if)
2.200 - apply (drule_tac a = a in mk_disjoint_insert)
2.201 - apply auto
2.202 - done
2.203 -*)
2.204 -
2.205 -text {*
2.206 - Congruence rule. The simplifier requires the rule to be in this form.
2.207 -*}
2.208 -(*
2.209 -lemma (in finite_prod) prod_cong [cong]:
2.210 - "[| A = B; !!i. i \<in> B ==> f i = g i;
2.211 - g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
2.212 -*)
2.213 -lemma (in finite_prod) prod_cong:
2.214 - "[| A = B; g \<in> B -> carrier G;
2.215 - !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
2.216 -
2.217 +lemma (in abelian_monoid) finprod_cong:
2.218 + "[| A = B; g : B -> carrier G;
2.219 + !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
2.220 proof -
2.221 - assume prems: "A = B"
2.222 - "!!i. i \<in> B ==> f i = g i"
2.223 - "g \<in> B -> carrier G"
2.224 + assume prems: "A = B" "g : B -> carrier G"
2.225 + "!!i. i : B ==> f i = g i"
2.226 show ?thesis
2.227 proof (cases "finite B")
2.228 case True
2.229 - then have "!!A. [| A = B; g \<in> B -> carrier G;
2.230 - !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
2.231 + then have "!!A. [| A = B; g : B -> carrier G;
2.232 + !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
2.233 proof induct
2.234 case empty thus ?case by simp
2.235 next
2.236 case (insert B x)
2.237 - then have "prod f A = prod f (insert x B)" by simp
2.238 - also from insert have "... = f x \<otimes> prod f B"
2.239 - proof (intro prod_insert)
2.240 + then have "finprod G f A = finprod G f (insert x B)" by simp
2.241 + also from insert have "... = f x \<otimes> finprod G f B"
2.242 + proof (intro finprod_insert)
2.243 show "finite B" .
2.244 next
2.245 - show "x \<notin> B" .
2.246 + show "x ~: B" .
2.247 next
2.248 - assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
2.249 + assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
2.250 "g \<in> insert x B \<rightarrow> carrier G"
2.251 - thus "f \<in> B -> carrier G" by fastsimp
2.252 + thus "f : B -> carrier G" by fastsimp
2.253 next
2.254 assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
2.255 "g \<in> insert x B \<rightarrow> carrier G"
2.256 thus "f x \<in> carrier G" by fastsimp
2.257 qed
2.258 - also from insert have "... = g x \<otimes> prod g B" by fastsimp
2.259 - also from insert have "... = prod g (insert x B)"
2.260 - by (intro prod_insert [THEN sym]) auto
2.261 + also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
2.262 + also from insert have "... = finprod G g (insert x B)"
2.263 + by (intro finprod_insert [THEN sym]) auto
2.264 finally show ?case .
2.265 qed
2.266 with prems show ?thesis by simp
2.267 next
2.268 - case False with prems show ?thesis by (simp add: prod_def)
2.269 + case False with prems show ?thesis by (simp add: finprod_def)
2.270 qed
2.271 qed
2.272
2.273 -lemma (in finite_prod) prod_cong1 [cong]:
2.274 - "[| A = B; !!i. i \<in> B ==> f i = g i;
2.275 - g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
2.276 - by (rule prod_cong) fast+
2.277 +lemma (in abelian_monoid) finprod_cong' [cong]:
2.278 + "[| A = B; !!i. i : B ==> f i = g i;
2.279 + g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
2.280 + by (rule finprod_cong) fast+
2.281
2.282 -text {*
2.283 - Usually, if this rule causes a failed congruence proof error,
2.284 - the reason is that the premise @{text "g \<in> B -> carrier G"} could not
2.285 - be shown. Adding @{thm [source] Pi_def} to the simpset is often useful.
2.286 -*}
2.287 +text {*Usually, if this rule causes a failed congruence proof error,
2.288 + the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
2.289 + Adding @{thm [source] Pi_def} to the simpset is often useful. *}
2.290
2.291 declare funcsetI [rule del]
2.292 funcset_mem [rule del]
2.293
2.294 -subsection {* Summation over the integer interval @{term "{..n}"} *}
2.295 -
2.296 -text {*
2.297 - A new locale where the index set is restricted to @{term "nat"} is
2.298 - necessary, because currently locales demand types in theorems to be as
2.299 - general as in the locale's definition.
2.300 -*}
2.301 -
2.302 -locale finite_prod_nat = finite_prod +
2.303 - assumes "False ==> prod f (A::nat set) = prod f A"
2.304 -
2.305 -lemma (in finite_prod_nat) natSum_0 [simp]:
2.306 - "f \<in> {0::nat} -> carrier G ==> prod f {..0} = f 0"
2.307 +lemma (in abelian_monoid) finprod_0 [simp]:
2.308 + "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
2.309 by (simp add: Pi_def)
2.310
2.311 -lemma (in finite_prod_nat) natsum_Suc [simp]:
2.312 - "f \<in> {..Suc n} -> carrier G ==>
2.313 - prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
2.314 +lemma (in abelian_monoid) finprod_Suc [simp]:
2.315 + "f : {..Suc n} -> carrier G ==>
2.316 + finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
2.317 by (simp add: Pi_def atMost_Suc)
2.318
2.319 -lemma (in finite_prod_nat) natsum_Suc2:
2.320 - "f \<in> {..Suc n} -> carrier G ==>
2.321 - prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
2.322 +lemma (in abelian_monoid) finprod_Suc2:
2.323 + "f : {..Suc n} -> carrier G ==>
2.324 + finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
2.325 proof (induct n)
2.326 case 0 thus ?case by (simp add: Pi_def)
2.327 next
2.328 - case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
2.329 + case Suc thus ?case by (simp add: m_assoc Pi_def finprod_closed)
2.330 qed
2.331
2.332 -lemma (in finite_prod_nat) natsum_zero [simp]:
2.333 - "prod (%i. \<one>) {..n::nat} = \<one>"
2.334 -by (induct n) (simp_all add: Pi_def)
2.335 -
2.336 -lemma (in finite_prod_nat) natsum_add [simp]:
2.337 - "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
2.338 - prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
2.339 -by (induct n) (simp_all add: ac Pi_def prod_closed)
2.340 -
2.341 -ML_setup {*
2.342 -
2.343 -Context.>> (fn thy => (simpset_ref_of thy :=
2.344 - simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
2.345 -
2.346 -ML_setup {*
2.347 -
2.348 -Context.>> (fn thy => (simpset_ref_of thy :=
2.349 - simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
2.350 +lemma (in abelian_monoid) finprod_mult [simp]:
2.351 + "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
2.352 + finprod G (%i. f i \<otimes> g i) {..n::nat} =
2.353 + finprod G f {..n} \<otimes> finprod G g {..n}"
2.354 + by (induct n) (simp_all add: ac Pi_def finprod_closed)
2.355
2.356 end
2.357 +
3.1 --- a/src/HOL/Algebra/ringsimp.ML Fri Mar 14 12:03:23 2003 +0100
3.2 +++ b/src/HOL/Algebra/ringsimp.ML Fri Mar 14 18:00:16 2003 +0100
3.3 @@ -64,9 +64,9 @@
3.4 val cring_ss = HOL_ss settermless termless_ring;
3.5
3.6 fun cring_normalise ctxt = let
3.7 - fun filter t = case HOLogic.dest_Trueprop t of
3.8 + fun filter t = (case HOLogic.dest_Trueprop t of
3.9 Const ("CRing.cring_axioms", _) $ Free (s, _) => [s]
3.10 - | _ => []
3.11 + | _ => [])
3.12 handle TERM _ => [];
3.13 val insts = flat (map (filter o #prop o rep_thm)
3.14 (ProofContext.prems_of ctxt));