13813

1 
(*


2 
Title: HOL/Algebra/Group.thy


3 
Id: $Id$


4 
Author: Clemens Ballarin, started 4 February 2003


5 


6 
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.


7 
*)


8 


9 
header {* Algebraic Structures up to Abelian Groups *}


10 

13817

11 
theory Group = FuncSet + FoldSet:

13813

12 


13 
text {*


14 
Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with


15 
the exception of \emph{magma} which, following Bourbaki, is a set


16 
together with a binary, closed operation.


17 
*}


18 


19 
section {* From Magmas to Groups *}


20 


21 
subsection {* Definitions *}


22 

13817

23 
record 'a semigroup =

13813

24 
carrier :: "'a set"


25 
mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)


26 

13817

27 
record 'a monoid = "'a semigroup" +

13813

28 
one :: 'a ("\<one>\<index>")

13817

29 


30 
record 'a group = "'a monoid" +

13813

31 
m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)


32 


33 
locale magma = struct G +


34 
assumes m_closed [intro, simp]:


35 
"[ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y \<in> carrier G"


36 


37 
locale semigroup = magma +


38 
assumes m_assoc:


39 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==>


40 
(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"


41 

13817

42 
locale l_one = struct G +

13813

43 
assumes one_closed [intro, simp]: "\<one> \<in> carrier G"


44 
and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"

13817

45 


46 
locale group = semigroup + l_one +


47 
assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"

13813

48 
and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"


49 


50 
subsection {* Cancellation Laws and Basic Properties *}


51 


52 
lemma (in group) l_cancel [simp]:


53 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==>


54 
(x \<otimes> y = x \<otimes> z) = (y = z)"


55 
proof


56 
assume eq: "x \<otimes> y = x \<otimes> z"


57 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"


58 
then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc)


59 
with G show "y = z" by (simp add: l_inv)


60 
next


61 
assume eq: "y = z"


62 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"


63 
then show "x \<otimes> y = x \<otimes> z" by simp


64 
qed


65 


66 
lemma (in group) r_one [simp]:


67 
"x \<in> carrier G ==> x \<otimes> \<one> = x"


68 
proof 


69 
assume x: "x \<in> carrier G"


70 
then have "inv x \<otimes> (x \<otimes> \<one>) = inv x \<otimes> x"


71 
by (simp add: m_assoc [symmetric] l_inv)


72 
with x show ?thesis by simp


73 
qed


74 


75 
lemma (in group) r_inv:


76 
"x \<in> carrier G ==> x \<otimes> inv x = \<one>"


77 
proof 


78 
assume x: "x \<in> carrier G"


79 
then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"


80 
by (simp add: m_assoc [symmetric] l_inv)


81 
with x show ?thesis by (simp del: r_one)


82 
qed


83 


84 
lemma (in group) r_cancel [simp]:


85 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==>


86 
(y \<otimes> x = z \<otimes> x) = (y = z)"


87 
proof


88 
assume eq: "y \<otimes> x = z \<otimes> x"


89 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"


90 
then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"


91 
by (simp add: m_assoc [symmetric])


92 
with G show "y = z" by (simp add: r_inv)


93 
next


94 
assume eq: "y = z"


95 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"


96 
then show "y \<otimes> x = z \<otimes> x" by simp


97 
qed


98 


99 
lemma (in group) inv_inv [simp]:


100 
"x \<in> carrier G ==> inv (inv x) = x"


101 
proof 


102 
assume x: "x \<in> carrier G"


103 
then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by (simp add: l_inv r_inv)


104 
with x show ?thesis by simp


105 
qed


106 


107 
lemma (in group) inv_mult:


108 
"[ x \<in> carrier G; y \<in> carrier G ] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"


109 
proof 


110 
assume G: "x \<in> carrier G" "y \<in> carrier G"


111 
then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"


112 
by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)


113 
with G show ?thesis by simp


114 
qed


115 


116 
subsection {* Substructures *}


117 


118 
locale submagma = var H + struct G +


119 
assumes subset [intro, simp]: "H \<subseteq> carrier G"


120 
and m_closed [intro, simp]: "[ x \<in> H; y \<in> H ] ==> x \<otimes> y \<in> H"


121 


122 
declare (in submagma) magma.intro [intro] semigroup.intro [intro]


123 


124 
(*


125 
alternative definition of submagma


126 


127 
locale submagma = var H + struct G +


128 
assumes subset [intro, simp]: "carrier H \<subseteq> carrier G"


129 
and m_equal [simp]: "mult H = mult G"


130 
and m_closed [intro, simp]:


131 
"[ x \<in> carrier H; y \<in> carrier H ] ==> x \<otimes> y \<in> carrier H"


132 
*)


133 


134 
lemma submagma_imp_subset:


135 
"submagma H G ==> H \<subseteq> carrier G"


136 
by (rule submagma.subset)


137 


138 
lemma (in submagma) subsetD [dest, simp]:


139 
"x \<in> H ==> x \<in> carrier G"


140 
using subset by blast


141 


142 
lemma (in submagma) magmaI [intro]:


143 
includes magma G


144 
shows "magma (G( carrier := H ))"


145 
by rule simp


146 


147 
lemma (in submagma) semigroup_axiomsI [intro]:


148 
includes semigroup G


149 
shows "semigroup_axioms (G( carrier := H ))"


150 
by rule (simp add: m_assoc)


151 


152 
lemma (in submagma) semigroupI [intro]:


153 
includes semigroup G


154 
shows "semigroup (G( carrier := H ))"


155 
using prems by fast


156 


157 
locale subgroup = submagma H G +


158 
assumes one_closed [intro, simp]: "\<one> \<in> H"


159 
and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"


160 


161 
declare (in subgroup) group.intro [intro]


162 

13817

163 
lemma (in subgroup) l_oneI [intro]:


164 
includes l_one G


165 
shows "l_one (G( carrier := H ))"


166 
by rule simp_all


167 

13813

168 
lemma (in subgroup) group_axiomsI [intro]:


169 
includes group G


170 
shows "group_axioms (G( carrier := H ))"


171 
by rule (simp_all add: l_inv)


172 


173 
lemma (in subgroup) groupI [intro]:


174 
includes group G


175 
shows "group (G( carrier := H ))"


176 
using prems by fast


177 


178 
text {*


179 
Since @{term H} is nonempty, it contains some element @{term x}. Since


180 
it is closed under inverse, it contains @{text "inv x"}. Since


181 
it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.


182 
*}


183 


184 
lemma (in group) one_in_subset:


185 
"[ H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H ]


186 
==> \<one> \<in> H"


187 
by (force simp add: l_inv)


188 


189 
text {* A characterization of subgroups: closed, nonempty subset. *}


190 


191 
lemma (in group) subgroupI:


192 
assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"


193 
and inv: "!!a. a \<in> H ==> inv a \<in> H"


194 
and mult: "!!a b. [a \<in> H; b \<in> H] ==> a \<otimes> b \<in> H"


195 
shows "subgroup H G"


196 
proof


197 
from subset and mult show "submagma H G" ..


198 
next


199 
have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)


200 
with inv show "subgroup_axioms H G"


201 
by (intro subgroup_axioms.intro) simp_all


202 
qed


203 


204 
text {*


205 
Repeat facts of submagmas for subgroups. Necessary???


206 
*}


207 


208 
lemma (in subgroup) subset:


209 
"H \<subseteq> carrier G"


210 
..


211 


212 
lemma (in subgroup) m_closed:


213 
"[ x \<in> H; y \<in> H ] ==> x \<otimes> y \<in> H"


214 
..


215 


216 
declare magma.m_closed [simp]


217 

13817

218 
declare l_one.one_closed [iff] group.inv_closed [simp]


219 
l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]

13813

220 


221 
lemma subgroup_nonempty:


222 
"~ subgroup {} G"


223 
by (blast dest: subgroup.one_closed)


224 


225 
lemma (in subgroup) finite_imp_card_positive:


226 
"finite (carrier G) ==> 0 < card H"


227 
proof (rule classical)


228 
have sub: "subgroup H G" using prems ..


229 
assume fin: "finite (carrier G)"


230 
and zero: "~ 0 < card H"


231 
then have "finite H" by (blast intro: finite_subset dest: subset)


232 
with zero sub have "subgroup {} G" by simp


233 
with subgroup_nonempty show ?thesis by contradiction


234 
qed


235 


236 
subsection {* Direct Products *}


237 


238 
constdefs

13817

239 
DirProdSemigroup ::


240 
"[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]


241 
=> ('a \<times> 'b) semigroup"


242 
(infixr "\<times>\<^sub>s" 80)


243 
"G \<times>\<^sub>s H == ( carrier = carrier G \<times> carrier H,


244 
mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) )"


245 


246 
DirProdMonoid ::


247 
"[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"

13813

248 
(infixr "\<times>\<^sub>m" 80)

13817

249 
"G \<times>\<^sub>m H == ( carrier = carrier (G \<times>\<^sub>s H),


250 
mult = mult (G \<times>\<^sub>s H),


251 
one = (one G, one H) )"

13813

252 


253 
DirProdGroup ::


254 
"[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"


255 
(infixr "\<times>\<^sub>g" 80)


256 
"G \<times>\<^sub>g H == ( carrier = carrier (G \<times>\<^sub>m H),


257 
mult = mult (G \<times>\<^sub>m H),

13817

258 
one = one (G \<times>\<^sub>m H),

13813

259 
m_inv = (%(g, h). (m_inv G g, m_inv H h)) )"


260 

13817

261 
lemma DirProdSemigroup_magma:

13813

262 
includes magma G + magma H

13817

263 
shows "magma (G \<times>\<^sub>s H)"


264 
by rule (auto simp add: DirProdSemigroup_def)

13813

265 

13817

266 
lemma DirProdSemigroup_semigroup_axioms:

13813

267 
includes semigroup G + semigroup H

13817

268 
shows "semigroup_axioms (G \<times>\<^sub>s H)"


269 
by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)

13813

270 

13817

271 
lemma DirProdSemigroup_semigroup:

13813

272 
includes semigroup G + semigroup H

13817

273 
shows "semigroup (G \<times>\<^sub>s H)"

13813

274 
using prems


275 
by (fast intro: semigroup.intro

13817

276 
DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)

13813

277 


278 
lemma DirProdGroup_magma:


279 
includes magma G + magma H


280 
shows "magma (G \<times>\<^sub>g H)"

13817

281 
by rule


282 
(auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)

13813

283 


284 
lemma DirProdGroup_semigroup_axioms:


285 
includes semigroup G + semigroup H


286 
shows "semigroup_axioms (G \<times>\<^sub>g H)"


287 
by rule

13817

288 
(auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def


289 
G.m_assoc H.m_assoc)

13813

290 


291 
lemma DirProdGroup_semigroup:


292 
includes semigroup G + semigroup H


293 
shows "semigroup (G \<times>\<^sub>g H)"


294 
using prems


295 
by (fast intro: semigroup.intro


296 
DirProdGroup_magma DirProdGroup_semigroup_axioms)


297 


298 
(* ... and further lemmas for group ... *)


299 

13817

300 
lemma DirProdGroup_group:

13813

301 
includes group G + group H


302 
shows "group (G \<times>\<^sub>g H)"


303 
by rule

13817

304 
(auto intro: magma.intro l_one.intro


305 
semigroup_axioms.intro group_axioms.intro


306 
simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def

13813

307 
G.m_assoc H.m_assoc G.l_inv H.l_inv)


308 


309 
subsection {* Homomorphisms *}


310 


311 
constdefs

13817

312 
hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]


313 
=> ('a => 'b)set"

13813

314 
"hom G H ==


315 
{h. h \<in> carrier G > carrier H &


316 
(\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"


317 


318 
lemma (in semigroup) hom:


319 
includes semigroup G


320 
shows "semigroup ( carrier = hom G G, mult = op o )"


321 
proof


322 
show "magma ( carrier = hom G G, mult = op o )"


323 
by rule (simp add: Pi_def hom_def)


324 
next


325 
show "semigroup_axioms ( carrier = hom G G, mult = op o )"


326 
by rule (simp add: o_assoc)


327 
qed


328 


329 
lemma hom_mult:


330 
"[ h \<in> hom G H; x \<in> carrier G; y \<in> carrier G ]


331 
==> h (mult G x y) = mult H (h x) (h y)"


332 
by (simp add: hom_def)


333 


334 
lemma hom_closed:


335 
"[ h \<in> hom G H; x \<in> carrier G ] ==> h x \<in> carrier H"


336 
by (auto simp add: hom_def funcset_mem)


337 


338 
locale group_hom = group G + group H + var h +


339 
assumes homh: "h \<in> hom G H"


340 
notes hom_mult [simp] = hom_mult [OF homh]


341 
and hom_closed [simp] = hom_closed [OF homh]


342 


343 
lemma (in group_hom) one_closed [simp]:


344 
"h \<one> \<in> carrier H"


345 
by simp


346 


347 
lemma (in group_hom) hom_one [simp]:


348 
"h \<one> = \<one>\<^sub>2"


349 
proof 


350 
have "h \<one> \<otimes>\<^sub>2 \<one>\<^sub>2 = h \<one> \<otimes>\<^sub>2 h \<one>"


351 
by (simp add: hom_mult [symmetric] del: hom_mult)


352 
then show ?thesis by (simp del: r_one)


353 
qed


354 


355 
lemma (in group_hom) inv_closed [simp]:


356 
"x \<in> carrier G ==> h (inv x) \<in> carrier H"


357 
by simp


358 


359 
lemma (in group_hom) hom_inv [simp]:


360 
"x \<in> carrier G ==> h (inv x) = inv\<^sub>2 (h x)"


361 
proof 


362 
assume x: "x \<in> carrier G"


363 
then have "h x \<otimes>\<^sub>2 h (inv x) = \<one>\<^sub>2"


364 
by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)


365 
also from x have "... = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)"


366 
by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)


367 
finally have "h x \<otimes>\<^sub>2 h (inv x) = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" .


368 
with x show ?thesis by simp


369 
qed


370 


371 
section {* Abelian Structures *}


372 


373 
subsection {* Definition *}


374 


375 
locale abelian_semigroup = semigroup +


376 
assumes m_comm: "[ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y = y \<otimes> x"


377 


378 
lemma (in abelian_semigroup) m_lcomm:


379 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==>


380 
x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"


381 
proof 


382 
assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"


383 
from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)


384 
also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)


385 
also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)


386 
finally show ?thesis .


387 
qed


388 


389 
lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm


390 

13817

391 
locale abelian_monoid = abelian_semigroup + l_one


392 


393 
lemma (in abelian_monoid) l_one [simp]:


394 
"x \<in> carrier G ==> x \<otimes> \<one> = x"


395 
proof 


396 
assume G: "x \<in> carrier G"


397 
then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)


398 
also from G have "... = x" by simp


399 
finally show ?thesis .


400 
qed


401 


402 
locale abelian_group = abelian_monoid + group


403 


404 
subsection {* Products over Finite Sets *}


405 


406 
locale finite_prod = abelian_monoid + var prod +


407 
defines "prod == (%f A. if finite A


408 
then foldD (carrier G) (op \<otimes> o f) \<one> A


409 
else arbitrary)"


410 


411 
(* TODO: nice syntax for the summation operator inside the locale


412 
like \<Otimes>\<index> i\<in>A. f i, probably needs handcoded translation *)


413 


414 
ML_setup {*


415 


416 
Context.>> (fn thy => (simpset_ref_of thy :=


417 
simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}


418 


419 
lemma (in finite_prod) prod_empty [simp]:


420 
"prod f {} = \<one>"


421 
by (simp add: prod_def)


422 


423 
ML_setup {*


424 


425 
Context.>> (fn thy => (simpset_ref_of thy :=


426 
simpset_of thy setsubgoaler asm_simp_tac; thy)) *}


427 


428 
declare funcsetI [intro]


429 
funcset_mem [dest]


430 


431 
lemma (in finite_prod) prod_insert [simp]:


432 
"[ finite F; a \<notin> F; f \<in> F > carrier G; f a \<in> carrier G ] ==>


433 
prod f (insert a F) = f a \<otimes> prod f F"


434 
apply (rule trans)


435 
apply (simp add: prod_def)


436 
apply (rule trans)


437 
apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])


438 
apply simp


439 
apply (rule m_lcomm)


440 
apply fast apply fast apply assumption


441 
apply (fastsimp intro: m_closed)


442 
apply simp+ apply fast


443 
apply (auto simp add: prod_def)


444 
done


445 


446 
lemma (in finite_prod) prod_one:


447 
"finite A ==> prod (%i. \<one>) A = \<one>"


448 
proof (induct set: Finites)


449 
case empty show ?case by simp


450 
next


451 
case (insert A a)


452 
have "(%i. \<one>) \<in> A > carrier G" by auto


453 
with insert show ?case by simp


454 
qed


455 


456 
(*


457 
lemma prod_eq_0_iff [simp]:


458 
"finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"


459 
by (induct set: Finites) auto


460 


461 
lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"


462 
apply (case_tac "finite A")


463 
prefer 2 apply (simp add: prod_def)


464 
apply (erule rev_mp)


465 
apply (erule finite_induct)


466 
apply auto


467 
done


468 


469 
lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"


470 
*)  {* Could allow many @{text "card"} proofs to be simplified. *}


471 
(*


472 
by (induct set: Finites) auto


473 
*)


474 


475 
lemma (in finite_prod) prod_closed:


476 
fixes A


477 
assumes fin: "finite A" and f: "f \<in> A > carrier G"


478 
shows "prod f A \<in> carrier G"


479 
using fin f


480 
proof induct


481 
case empty show ?case by simp


482 
next


483 
case (insert A a)


484 
then have a: "f a \<in> carrier G" by fast


485 
from insert have A: "f \<in> A > carrier G" by fast


486 
from insert A a show ?case by simp


487 
qed


488 


489 
lemma funcset_Int_left [simp, intro]:


490 
"[ f \<in> A > C; f \<in> B > C ] ==> f \<in> A Int B > C"


491 
by fast


492 


493 
lemma funcset_Un_left [iff]:


494 
"(f \<in> A Un B > C) = (f \<in> A > C & f \<in> B > C)"


495 
by fast


496 


497 
lemma (in finite_prod) prod_Un_Int:


498 
"[ finite A; finite B; g \<in> A > carrier G; g \<in> B > carrier G ] ==>


499 
prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"


500 
 {* The reversed orientation looks more natural, but LOOPS as a simprule! *}


501 
proof (induct set: Finites)


502 
case empty then show ?case by (simp add: prod_closed)


503 
next


504 
case (insert A a)


505 
then have a: "g a \<in> carrier G" by fast


506 
from insert have A: "g \<in> A > carrier G" by fast


507 
from insert A a show ?case


508 
by (simp add: ac Int_insert_left insert_absorb prod_closed


509 
Int_mono2 Un_subset_iff)


510 
qed


511 


512 
lemma (in finite_prod) prod_Un_disjoint:


513 
"[ finite A; finite B; A Int B = {};


514 
g \<in> A > carrier G; g \<in> B > carrier G ]


515 
==> prod g (A Un B) = prod g A \<otimes> prod g B"


516 
apply (subst prod_Un_Int [symmetric])


517 
apply (auto simp add: prod_closed)


518 
done


519 


520 
(*


521 
lemma prod_UN_disjoint:


522 
fixes f :: "'a => 'b::plus_ac0"


523 
shows


524 
"finite I ==> (ALL i:I. finite (A i)) ==>


525 
(ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}) ==>


526 
prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"


527 
apply (induct set: Finites)


528 
apply simp


529 
apply atomize


530 
apply (subgoal_tac "ALL i:F. x \<noteq> i")


531 
prefer 2 apply blast


532 
apply (subgoal_tac "A x Int UNION F A = {}")


533 
prefer 2 apply blast


534 
apply (simp add: prod_Un_disjoint)


535 
done


536 
*)


537 


538 
lemma (in finite_prod) prod_addf:


539 
"[ finite A; f \<in> A > carrier G; g \<in> A > carrier G ] ==>


540 
prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"


541 
proof (induct set: Finites)


542 
case empty show ?case by simp


543 
next


544 
case (insert A a) then


545 
have fA: "f : A > carrier G" by fast


546 
from insert have fa: "f a : carrier G" by fast


547 
from insert have gA: "g : A > carrier G" by fast


548 
from insert have ga: "g a : carrier G" by fast


549 
from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)


550 
from insert have fgA: "(%x. f x \<otimes> g x) : A > carrier G"


551 
by (simp add: Pi_def)


552 
show ?case (* check if all simps are really necessary *)


553 
by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)


554 
qed


555 


556 
(*


557 
lemma prod_Un: "finite A ==> finite B ==>


558 
(prod f (A Un B) :: nat) = prod f A + prod f B  prod f (A Int B)"


559 
 {* For the natural numbers, we have subtraction. *}


560 
apply (subst prod_Un_Int [symmetric])


561 
apply auto


562 
done


563 


564 
lemma prod_diff1: "(prod f (A  {a}) :: nat) =


565 
(if a:A then prod f A  f a else prod f A)"


566 
apply (case_tac "finite A")


567 
prefer 2 apply (simp add: prod_def)


568 
apply (erule finite_induct)


569 
apply (auto simp add: insert_Diff_if)


570 
apply (drule_tac a = a in mk_disjoint_insert)


571 
apply auto


572 
done


573 
*)


574 


575 
lemma (in finite_prod) prod_cong:


576 
"[ A = B; g : B > carrier G;


577 
!!i. i : B ==> f i = g i ] ==> prod f A = prod g B"


578 
proof 


579 
assume prems: "A = B" "g : B > carrier G"


580 
"!!i. i : B ==> f i = g i"


581 
show ?thesis


582 
proof (cases "finite B")


583 
case True


584 
then have "!!A. [ A = B; g : B > carrier G;


585 
!!i. i : B ==> f i = g i ] ==> prod f A = prod g B"


586 
proof induct


587 
case empty thus ?case by simp


588 
next


589 
case (insert B x)


590 
then have "prod f A = prod f (insert x B)" by simp


591 
also from insert have "... = f x \<otimes> prod f B"


592 
proof (intro prod_insert)


593 
show "finite B" .


594 
next


595 
show "x ~: B" .


596 
next


597 
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"


598 
"g \<in> insert x B \<rightarrow> carrier G"


599 
thus "f : B > carrier G" by fastsimp


600 
next


601 
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"


602 
"g \<in> insert x B \<rightarrow> carrier G"


603 
thus "f x \<in> carrier G" by fastsimp


604 
qed


605 
also from insert have "... = g x \<otimes> prod g B" by fastsimp


606 
also from insert have "... = prod g (insert x B)"


607 
by (intro prod_insert [THEN sym]) auto


608 
finally show ?case .


609 
qed


610 
with prems show ?thesis by simp


611 
next


612 
case False with prems show ?thesis by (simp add: prod_def)


613 
qed


614 
qed


615 


616 
lemma (in finite_prod) prod_cong1 [cong]:


617 
"[ A = B; !!i. i : B ==> f i = g i;


618 
g : B > carrier G = True ] ==> prod f A = prod g B"


619 
by (rule prod_cong) fast+


620 


621 
text {*Usually, if this rule causes a failed congruence proof error,


622 
the reason is that the premise @{text "g : B > carrier G"} cannot be shown.


623 
Adding @{thm [source] Pi_def} to the simpset is often useful. *}


624 


625 
declare funcsetI [rule del]


626 
funcset_mem [rule del]


627 


628 
subsection {* Summation over the integer interval @{term "{..n}"} *}


629 


630 
text {*


631 
For technical reasons (locales) a new locale where the index set is


632 
restricted to @{term "nat"} is necessary.


633 
*}


634 


635 
locale finite_prod_nat = finite_prod +


636 
assumes "False ==> prod f (A::nat set) = prod f A"


637 


638 
lemma (in finite_prod_nat) natSum_0 [simp]:


639 
"f : {0::nat} > carrier G ==> prod f {..0} = f 0"


640 
by (simp add: Pi_def)


641 


642 
lemma (in finite_prod_nat) natsum_Suc [simp]:


643 
"f : {..Suc n} > carrier G ==>


644 
prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"


645 
by (simp add: Pi_def atMost_Suc)


646 


647 
lemma (in finite_prod_nat) natsum_Suc2:


648 
"f : {..Suc n} > carrier G ==>


649 
prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"


650 
proof (induct n)


651 
case 0 thus ?case by (simp add: Pi_def)


652 
next


653 
case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)


654 
qed


655 


656 
lemma (in finite_prod_nat) natsum_zero [simp]:


657 
"prod (%i. \<one>) {..n::nat} = \<one>"


658 
by (induct n) (simp_all add: Pi_def)


659 


660 
lemma (in finite_prod_nat) natsum_add [simp]:


661 
"[ f : {..n} > carrier G; g : {..n} > carrier G ] ==>


662 
prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"


663 
by (induct n) (simp_all add: ac Pi_def prod_closed)


664 


665 
thm setsum_cong


666 


667 
ML_setup {*


668 


669 
Context.>> (fn thy => (simpset_ref_of thy :=


670 
simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}


671 


672 
lemma "(\<Sum>i\<in>{..10::nat}. if i<=10 then 0 else 1) = (0::nat)"


673 
apply simp done


674 


675 
lemma (in finite_prod_nat) "prod (%i. if i<=10 then \<one> else x) {..10} = \<one>"


676 
apply (simp add: Pi_def)

13813

677 


678 
end
