Product operator added --- preliminary.
authorballarin
Fri Feb 14 17:35:56 2003 +0100 (2003-02-14)
changeset 138177e031a968443
parent 13816 cc228bd9c1fc
child 13818 274fda8cca4b
Product operator added --- preliminary.
src/HOL/Algebra/FoldSet.thy
src/HOL/Algebra/Group.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/FoldSet.thy	Fri Feb 14 17:35:56 2003 +0100
     1.3 @@ -0,0 +1,297 @@
     1.4 +(*  Title:      Summation Operator for Abelian Groups
     1.5 +    ID:         $Id$
     1.6 +    Author:     Clemens Ballarin, started 19 November 2002
     1.7 +
     1.8 +This file is largely based on HOL/Finite_Set.thy.
     1.9 +*)
    1.10 +
    1.11 +header {* Summation Operator *}
    1.12 +
    1.13 +theory FoldSet = Main:
    1.14 +
    1.15 +(* Instantiation of LC from Finite_Set.thy is not possible,
    1.16 +   because here we have explicit typing rules like x : carrier G.
    1.17 +   We introduce an explicit argument for the domain D *)
    1.18 +
    1.19 +consts
    1.20 +  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    1.21 +
    1.22 +inductive "foldSetD D f e"
    1.23 +  intros
    1.24 +    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
    1.25 +    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
    1.26 +                      (insert x A, f x y) : foldSetD D f e"
    1.27 +
    1.28 +inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
    1.29 +
    1.30 +constdefs
    1.31 +  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
    1.32 +  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
    1.33 +
    1.34 +lemma foldSetD_closed:
    1.35 +  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
    1.36 +      |] ==> z : D";
    1.37 +  by (erule foldSetD.elims) auto
    1.38 +
    1.39 +lemma Diff1_foldSetD:
    1.40 +  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
    1.41 +   (A, f x y) : foldSetD D f e"
    1.42 +  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    1.43 +   apply auto
    1.44 +  done
    1.45 +
    1.46 +lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
    1.47 +  by (induct set: foldSetD) auto
    1.48 +
    1.49 +lemma finite_imp_foldSetD:
    1.50 +  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
    1.51 +   EX x. (A, x) : foldSetD D f e"
    1.52 +proof (induct set: Finites)
    1.53 +  case empty then show ?case by auto
    1.54 +next
    1.55 +  case (insert F x)
    1.56 +  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    1.57 +  with insert have "y : D" by (auto dest: foldSetD_closed)
    1.58 +  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    1.59 +    by (intro foldSetD.intros) auto
    1.60 +  then show ?case ..
    1.61 +qed
    1.62 +
    1.63 +subsection {* Left-commutative operations *}
    1.64 +
    1.65 +locale LCD =
    1.66 +  fixes B :: "'b set"
    1.67 +  and D :: "'a set"
    1.68 +  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
    1.69 +  assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    1.70 +  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
    1.71 +
    1.72 +lemma (in LCD) foldSetD_closed [dest]:
    1.73 +  "(A, z) : foldSetD D f e ==> z : D";
    1.74 +  by (erule foldSetD.elims) auto
    1.75 +
    1.76 +lemma (in LCD) Diff1_foldSetD:
    1.77 +  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
    1.78 +   (A, f x y) : foldSetD D f e"
    1.79 +  apply (subgoal_tac "x : B")
    1.80 +  prefer 2 apply fast
    1.81 +  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    1.82 +   apply auto
    1.83 +  done
    1.84 +
    1.85 +lemma (in LCD) foldSetD_imp_finite [simp]:
    1.86 +  "(A, x) : foldSetD D f e ==> finite A"
    1.87 +  by (induct set: foldSetD) auto
    1.88 +
    1.89 +lemma (in LCD) finite_imp_foldSetD:
    1.90 +  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
    1.91 +proof (induct set: Finites)
    1.92 +  case empty then show ?case by auto
    1.93 +next
    1.94 +  case (insert F x)
    1.95 +  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    1.96 +  with insert have "y : D" by auto
    1.97 +  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    1.98 +    by (intro foldSetD.intros) auto
    1.99 +  then show ?case ..
   1.100 +qed
   1.101 +
   1.102 +lemma (in LCD) foldSetD_determ_aux:
   1.103 +  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
   1.104 +    (ALL y. (A, y) : foldSetD D f e --> y = x)"
   1.105 +  apply (induct n)
   1.106 +   apply (auto simp add: less_Suc_eq)
   1.107 +  apply (erule foldSetD.cases)
   1.108 +   apply blast
   1.109 +  apply (erule foldSetD.cases)
   1.110 +   apply blast
   1.111 +  apply clarify
   1.112 +  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   1.113 +  apply (erule rev_mp)
   1.114 +  apply (simp add: less_Suc_eq_le)
   1.115 +  apply (rule impI)
   1.116 +  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   1.117 +   apply (subgoal_tac "Aa = Ab")
   1.118 +    prefer 2 apply (blast elim!: equalityE)
   1.119 +   apply blast
   1.120 +  txt {* case @{prop "xa \<notin> xb"}. *}
   1.121 +  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   1.122 +   prefer 2 apply (blast elim!: equalityE)
   1.123 +  apply clarify
   1.124 +  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   1.125 +   prefer 2 apply blast
   1.126 +  apply (subgoal_tac "card Aa <= card Ab")
   1.127 +   prefer 2
   1.128 +   apply (rule Suc_le_mono [THEN subst])
   1.129 +   apply (simp add: card_Suc_Diff1)
   1.130 +  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
   1.131 +  apply (blast intro: foldSetD_imp_finite finite_Diff)
   1.132 +(* new subgoal from finite_imp_foldSetD *)
   1.133 +    apply best (* blast doesn't seem to solve this *)
   1.134 +   apply assumption
   1.135 +  apply (frule (1) Diff1_foldSetD)
   1.136 +(* new subgoal from Diff1_foldSetD *)
   1.137 +    apply best
   1.138 +(*
   1.139 +apply (best del: foldSetD_closed elim: foldSetD_closed)
   1.140 +    apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
   1.141 +    prefer 3 apply assumption apply (rule e_closed)
   1.142 +    apply (rule f_closed) apply force apply assumption
   1.143 +*)
   1.144 +  apply (subgoal_tac "ya = f xb x")
   1.145 +   prefer 2
   1.146 +(* new subgoal to make IH applicable *) 
   1.147 +  apply (subgoal_tac "Aa <= B")
   1.148 +   prefer 2 apply best
   1.149 +   apply (blast del: equalityCE)
   1.150 +  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
   1.151 +   prefer 2 apply simp
   1.152 +  apply (subgoal_tac "yb = f xa x")
   1.153 +   prefer 2 
   1.154 +(*   apply (drule_tac x = xa in Diff1_foldSetD)
   1.155 +     apply assumption
   1.156 +     apply (rule f_closed) apply best apply (rule foldSetD_closed)
   1.157 +     prefer 3 apply assumption apply (rule e_closed)
   1.158 +     apply (rule f_closed) apply best apply assumption
   1.159 +*)
   1.160 +   apply (blast del: equalityCE dest: Diff1_foldSetD)
   1.161 +   apply (simp (no_asm_simp))
   1.162 +   apply (rule left_commute)
   1.163 +   apply assumption apply best apply best
   1.164 + done
   1.165 +
   1.166 +lemma (in LCD) foldSetD_determ:
   1.167 +  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
   1.168 +   ==> y = x"
   1.169 +  by (blast intro: foldSetD_determ_aux [rule_format])
   1.170 +
   1.171 +lemma (in LCD) foldD_equality:
   1.172 +  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
   1.173 +  by (unfold foldD_def) (blast intro: foldSetD_determ)
   1.174 +
   1.175 +lemma foldD_empty [simp]:
   1.176 +  "e : D ==> foldD D f e {} = e"
   1.177 +  by (unfold foldD_def) blast
   1.178 +
   1.179 +lemma (in LCD) foldD_insert_aux:
   1.180 +  "[| x ~: A; x : B; e : D; A <= B |] ==>
   1.181 +    ((insert x A, v) : foldSetD D f e) =
   1.182 +    (EX y. (A, y) : foldSetD D f e & v = f x y)"
   1.183 +  apply auto
   1.184 +  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
   1.185 +   apply (fastsimp dest: foldSetD_imp_finite)
   1.186 +(* new subgoal by finite_imp_foldSetD *)
   1.187 +    apply assumption
   1.188 +    apply assumption
   1.189 +  apply (blast intro: foldSetD_determ)
   1.190 +  done
   1.191 +
   1.192 +lemma (in LCD) foldD_insert:
   1.193 +    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
   1.194 +     foldD D f e (insert x A) = f x (foldD D f e A)"
   1.195 +  apply (unfold foldD_def)
   1.196 +  apply (simp add: foldD_insert_aux)
   1.197 +  apply (rule the_equality)
   1.198 +  apply (auto intro: finite_imp_foldSetD
   1.199 +    cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
   1.200 +  done
   1.201 +
   1.202 +lemma (in LCD) foldD_closed [simp]:
   1.203 +  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
   1.204 +proof (induct set: Finites)
   1.205 +  case empty then show ?case by (simp add: foldD_empty)
   1.206 +next
   1.207 +  case insert then show ?case by (simp add: foldD_insert)
   1.208 +qed
   1.209 +
   1.210 +lemma (in LCD) foldD_commute:
   1.211 +  "[| finite A; x : B; e : D; A <= B |] ==>
   1.212 +   f x (foldD D f e A) = foldD D f (f x e) A"
   1.213 +  apply (induct set: Finites)
   1.214 +   apply simp
   1.215 +  apply (auto simp add: left_commute foldD_insert)
   1.216 +  done
   1.217 +
   1.218 +lemma Int_mono2:
   1.219 +  "[| A <= C; B <= C |] ==> A Int B <= C"
   1.220 +  by blast
   1.221 +
   1.222 +lemma (in LCD) foldD_nest_Un_Int:
   1.223 +  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
   1.224 +   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   1.225 +  apply (induct set: Finites)
   1.226 +   apply simp
   1.227 +  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
   1.228 +    Int_mono2 Un_subset_iff)
   1.229 +  done
   1.230 +
   1.231 +lemma (in LCD) foldD_nest_Un_disjoint:
   1.232 +  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
   1.233 +    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   1.234 +  by (simp add: foldD_nest_Un_Int)
   1.235 +
   1.236 +-- {* Delete rules to do with @{text foldSetD} relation. *}
   1.237 +
   1.238 +declare foldSetD_imp_finite [simp del]
   1.239 +  empty_foldSetDE [rule del]
   1.240 +  foldSetD.intros [rule del]
   1.241 +declare (in LCD)
   1.242 +  foldSetD_closed [rule del]
   1.243 +
   1.244 +subsection {* Commutative monoids *}
   1.245 +
   1.246 +text {*
   1.247 +  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   1.248 +  instead of @{text "'b => 'a => 'a"}.
   1.249 +*}
   1.250 +
   1.251 +locale ACeD =
   1.252 +  fixes D :: "'a set"
   1.253 +    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   1.254 +    and e :: 'a
   1.255 +  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
   1.256 +    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
   1.257 +    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   1.258 +    and e_closed [simp]: "e : D"
   1.259 +    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
   1.260 +
   1.261 +lemma (in ACeD) left_commute:
   1.262 +  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   1.263 +proof -
   1.264 +  assume D: "x : D" "y : D" "z : D"
   1.265 +  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   1.266 +  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   1.267 +  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
   1.268 +  finally show ?thesis .
   1.269 +qed
   1.270 +
   1.271 +lemmas (in ACeD) AC = assoc commute left_commute
   1.272 +
   1.273 +lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
   1.274 +proof -
   1.275 +  assume D: "x : D"
   1.276 +  have "x \<cdot> e = x" by (rule ident)
   1.277 +  with D show ?thesis by (simp add: commute)
   1.278 +qed
   1.279 +
   1.280 +lemma (in ACeD) foldD_Un_Int:
   1.281 +  "[| finite A; finite B; A <= D; B <= D |] ==>
   1.282 +    foldD D f e A \<cdot> foldD D f e B =
   1.283 +    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   1.284 +  apply (induct set: Finites)
   1.285 +   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
   1.286 +(* left_commute is required to show premise of LCD.intro *)
   1.287 +  apply (simp add: AC insert_absorb Int_insert_left
   1.288 +    LCD.foldD_insert [OF LCD.intro [of D]]
   1.289 +    LCD.foldD_closed [OF LCD.intro [of D]]
   1.290 +    Int_mono2 Un_subset_iff)
   1.291 +  done
   1.292 +
   1.293 +lemma (in ACeD) foldD_Un_disjoint:
   1.294 +  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
   1.295 +    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   1.296 +  by (simp add: foldD_Un_Int
   1.297 +    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
   1.298 +
   1.299 +end
   1.300 +
     2.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 12 17:55:05 2003 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Fri Feb 14 17:35:56 2003 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  
     2.5  header {* Algebraic Structures up to Abelian Groups *}
     2.6  
     2.7 -theory Group = FuncSet:
     2.8 +theory Group = FuncSet + FoldSet:
     2.9  
    2.10  text {*
    2.11    Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    2.12 @@ -20,12 +20,14 @@
    2.13  
    2.14  subsection {* Definitions *}
    2.15  
    2.16 -record 'a magma =
    2.17 +record 'a semigroup =
    2.18    carrier :: "'a set"
    2.19    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    2.20  
    2.21 -record 'a group = "'a magma" +
    2.22 +record 'a monoid = "'a semigroup" +
    2.23    one :: 'a ("\<one>\<index>")
    2.24 +
    2.25 +record 'a group = "'a monoid" +
    2.26    m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
    2.27  
    2.28  locale magma = struct G +
    2.29 @@ -37,10 +39,12 @@
    2.30      "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    2.31       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    2.32  
    2.33 -locale group = semigroup +
    2.34 +locale l_one = struct G +
    2.35    assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    2.36 -    and inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
    2.37      and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    2.38 +
    2.39 +locale group = semigroup + l_one +
    2.40 +  assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
    2.41      and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
    2.42  
    2.43  subsection {* Cancellation Laws and Basic Properties *}
    2.44 @@ -156,6 +160,11 @@
    2.45  
    2.46  declare (in subgroup) group.intro [intro]
    2.47  
    2.48 +lemma (in subgroup) l_oneI [intro]:
    2.49 +  includes l_one G
    2.50 +  shows "l_one (G(| carrier := H |))"
    2.51 +  by rule simp_all
    2.52 +
    2.53  lemma (in subgroup) group_axiomsI [intro]:
    2.54    includes group G
    2.55    shows "group_axioms (G(| carrier := H |))"
    2.56 @@ -206,8 +215,8 @@
    2.57  
    2.58  declare magma.m_closed [simp]
    2.59  
    2.60 -declare group.one_closed [iff] group.inv_closed [simp]
    2.61 -  group.l_one [simp] group.r_one [simp] group.inv_inv [simp]
    2.62 +declare l_one.one_closed [iff] group.inv_closed [simp]
    2.63 +  l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]
    2.64  
    2.65  lemma subgroup_nonempty:
    2.66    "~ subgroup {} G"
    2.67 @@ -227,47 +236,57 @@
    2.68  subsection {* Direct Products *}
    2.69  
    2.70  constdefs
    2.71 -  DirProdMagma ::
    2.72 -    "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a \<times> 'b) magma"
    2.73 +  DirProdSemigroup ::
    2.74 +    "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
    2.75 +    => ('a \<times> 'b) semigroup"
    2.76 +    (infixr "\<times>\<^sub>s" 80)
    2.77 +  "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
    2.78 +    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    2.79 +
    2.80 +  DirProdMonoid ::
    2.81 +    "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
    2.82      (infixr "\<times>\<^sub>m" 80)
    2.83 -  "G \<times>\<^sub>m H == (| carrier = carrier G \<times> carrier H,
    2.84 -    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    2.85 +  "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
    2.86 +    mult = mult (G \<times>\<^sub>s H),
    2.87 +    one = (one G, one H) |)"
    2.88  
    2.89    DirProdGroup ::
    2.90      "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
    2.91      (infixr "\<times>\<^sub>g" 80)
    2.92    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
    2.93      mult = mult (G \<times>\<^sub>m H),
    2.94 -    one = (one G, one H),
    2.95 +    one = one (G \<times>\<^sub>m H),
    2.96      m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
    2.97  
    2.98 -lemma DirProdMagma_magma:
    2.99 +lemma DirProdSemigroup_magma:
   2.100    includes magma G + magma H
   2.101 -  shows "magma (G \<times>\<^sub>m H)"
   2.102 -  by rule (auto simp add: DirProdMagma_def)
   2.103 +  shows "magma (G \<times>\<^sub>s H)"
   2.104 +  by rule (auto simp add: DirProdSemigroup_def)
   2.105  
   2.106 -lemma DirProdMagma_semigroup_axioms:
   2.107 +lemma DirProdSemigroup_semigroup_axioms:
   2.108    includes semigroup G + semigroup H
   2.109 -  shows "semigroup_axioms (G \<times>\<^sub>m H)"
   2.110 -  by rule (auto simp add: DirProdMagma_def G.m_assoc H.m_assoc)
   2.111 +  shows "semigroup_axioms (G \<times>\<^sub>s H)"
   2.112 +  by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
   2.113  
   2.114 -lemma DirProdMagma_semigroup:
   2.115 +lemma DirProdSemigroup_semigroup:
   2.116    includes semigroup G + semigroup H
   2.117 -  shows "semigroup (G \<times>\<^sub>m H)"
   2.118 +  shows "semigroup (G \<times>\<^sub>s H)"
   2.119    using prems
   2.120    by (fast intro: semigroup.intro
   2.121 -    DirProdMagma_magma DirProdMagma_semigroup_axioms)
   2.122 +    DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
   2.123  
   2.124  lemma DirProdGroup_magma:
   2.125    includes magma G + magma H
   2.126    shows "magma (G \<times>\<^sub>g H)"
   2.127 -  by rule (auto simp add: DirProdGroup_def DirProdMagma_def)
   2.128 +  by rule
   2.129 +    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)
   2.130  
   2.131  lemma DirProdGroup_semigroup_axioms:
   2.132    includes semigroup G + semigroup H
   2.133    shows "semigroup_axioms (G \<times>\<^sub>g H)"
   2.134    by rule
   2.135 -    (auto simp add: DirProdGroup_def DirProdMagma_def G.m_assoc H.m_assoc)
   2.136 +    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   2.137 +      G.m_assoc H.m_assoc)
   2.138  
   2.139  lemma DirProdGroup_semigroup:
   2.140    includes semigroup G + semigroup H
   2.141 @@ -278,18 +297,20 @@
   2.142  
   2.143  (* ... and further lemmas for group ... *)
   2.144  
   2.145 -lemma
   2.146 +lemma DirProdGroup_group:
   2.147    includes group G + group H
   2.148    shows "group (G \<times>\<^sub>g H)"
   2.149  by rule
   2.150 -  (auto intro: magma.intro semigroup_axioms.intro group_axioms.intro
   2.151 -    simp add: DirProdGroup_def DirProdMagma_def
   2.152 +  (auto intro: magma.intro l_one.intro
   2.153 +      semigroup_axioms.intro group_axioms.intro
   2.154 +    simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   2.155        G.m_assoc H.m_assoc G.l_inv H.l_inv)
   2.156  
   2.157  subsection {* Homomorphisms *}
   2.158  
   2.159  constdefs
   2.160 -  hom :: "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a => 'b)set"
   2.161 +  hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
   2.162 +    => ('a => 'b)set"
   2.163    "hom G H ==
   2.164      {h. h \<in> carrier G -> carrier H &
   2.165        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
   2.166 @@ -367,6 +388,291 @@
   2.167  
   2.168  lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
   2.169  
   2.170 -locale abelian_group = abelian_semigroup + group
   2.171 +locale abelian_monoid = abelian_semigroup + l_one
   2.172 +
   2.173 +lemma (in abelian_monoid) l_one [simp]:
   2.174 +  "x \<in> carrier G ==> x \<otimes> \<one> = x"
   2.175 +proof -
   2.176 +  assume G: "x \<in> carrier G"
   2.177 +  then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
   2.178 +  also from G have "... = x" by simp
   2.179 +  finally show ?thesis .
   2.180 +qed
   2.181 +
   2.182 +locale abelian_group = abelian_monoid + group
   2.183 +
   2.184 +subsection {* Products over Finite Sets *}
   2.185 +
   2.186 +locale finite_prod = abelian_monoid + var prod +
   2.187 +  defines "prod == (%f A. if finite A
   2.188 +      then foldD (carrier G) (op \<otimes> o f) \<one> A
   2.189 +      else arbitrary)"
   2.190 +
   2.191 +(* TODO: nice syntax for the summation operator inside the locale
   2.192 +   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
   2.193 +
   2.194 +ML_setup {* 
   2.195 +
   2.196 +Context.>> (fn thy => (simpset_ref_of thy :=
   2.197 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   2.198 +
   2.199 +lemma (in finite_prod) prod_empty [simp]: 
   2.200 +  "prod f {} = \<one>"
   2.201 +  by (simp add: prod_def)
   2.202 +
   2.203 +ML_setup {* 
   2.204 +
   2.205 +Context.>> (fn thy => (simpset_ref_of thy :=
   2.206 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   2.207 +
   2.208 +declare funcsetI [intro]
   2.209 +  funcset_mem [dest]
   2.210 +
   2.211 +lemma (in finite_prod) prod_insert [simp]:
   2.212 +  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
   2.213 +   prod f (insert a F) = f a \<otimes> prod f F"
   2.214 +  apply (rule trans)
   2.215 +  apply (simp add: prod_def)
   2.216 +  apply (rule trans)
   2.217 +  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
   2.218 +    apply simp
   2.219 +    apply (rule m_lcomm)
   2.220 +      apply fast apply fast apply assumption
   2.221 +    apply (fastsimp intro: m_closed)
   2.222 +    apply simp+ apply fast
   2.223 +  apply (auto simp add: prod_def)
   2.224 +  done
   2.225 +
   2.226 +lemma (in finite_prod) prod_one:
   2.227 +  "finite A ==> prod (%i. \<one>) A = \<one>"
   2.228 +proof (induct set: Finites)
   2.229 +  case empty show ?case by simp
   2.230 +next
   2.231 +  case (insert A a)
   2.232 +  have "(%i. \<one>) \<in> A -> carrier G" by auto
   2.233 +  with insert show ?case by simp
   2.234 +qed
   2.235 +
   2.236 +(*
   2.237 +lemma prod_eq_0_iff [simp]:
   2.238 +    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
   2.239 +  by (induct set: Finites) auto
   2.240 +
   2.241 +lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
   2.242 +  apply (case_tac "finite A")
   2.243 +   prefer 2 apply (simp add: prod_def)
   2.244 +  apply (erule rev_mp)
   2.245 +  apply (erule finite_induct)
   2.246 +   apply auto
   2.247 +  done
   2.248 +
   2.249 +lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
   2.250 +*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
   2.251 +(*
   2.252 +  by (induct set: Finites) auto
   2.253 +*)
   2.254 +
   2.255 +lemma (in finite_prod) prod_closed:
   2.256 +  fixes A
   2.257 +  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   2.258 +  shows "prod f A \<in> carrier G"
   2.259 +using fin f
   2.260 +proof induct
   2.261 +  case empty show ?case by simp
   2.262 +next
   2.263 +  case (insert A a)
   2.264 +  then have a: "f a \<in> carrier G" by fast
   2.265 +  from insert have A: "f \<in> A -> carrier G" by fast
   2.266 +  from insert A a show ?case by simp
   2.267 +qed
   2.268 +
   2.269 +lemma funcset_Int_left [simp, intro]:
   2.270 +  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
   2.271 +  by fast
   2.272 +
   2.273 +lemma funcset_Un_left [iff]:
   2.274 +  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   2.275 +  by fast
   2.276 +
   2.277 +lemma (in finite_prod) prod_Un_Int:
   2.278 +  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   2.279 +   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
   2.280 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   2.281 +proof (induct set: Finites)
   2.282 +  case empty then show ?case by (simp add: prod_closed)
   2.283 +next
   2.284 +  case (insert A a)
   2.285 +  then have a: "g a \<in> carrier G" by fast
   2.286 +  from insert have A: "g \<in> A -> carrier G" by fast
   2.287 +  from insert A a show ?case
   2.288 +    by (simp add: ac Int_insert_left insert_absorb prod_closed
   2.289 +          Int_mono2 Un_subset_iff) 
   2.290 +qed
   2.291 +
   2.292 +lemma (in finite_prod) prod_Un_disjoint:
   2.293 +  "[| finite A; finite B; A Int B = {};
   2.294 +      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   2.295 +   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
   2.296 +  apply (subst prod_Un_Int [symmetric])
   2.297 +    apply (auto simp add: prod_closed)
   2.298 +  done
   2.299 +
   2.300 +(*
   2.301 +lemma prod_UN_disjoint:
   2.302 +  fixes f :: "'a => 'b::plus_ac0"
   2.303 +  shows
   2.304 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   2.305 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.306 +      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
   2.307 +  apply (induct set: Finites)
   2.308 +   apply simp
   2.309 +  apply atomize
   2.310 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.311 +   prefer 2 apply blast
   2.312 +  apply (subgoal_tac "A x Int UNION F A = {}")
   2.313 +   prefer 2 apply blast
   2.314 +  apply (simp add: prod_Un_disjoint)
   2.315 +  done
   2.316 +*)
   2.317 +
   2.318 +lemma (in finite_prod) prod_addf:
   2.319 +  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   2.320 +   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
   2.321 +proof (induct set: Finites)
   2.322 +  case empty show ?case by simp
   2.323 +next
   2.324 +  case (insert A a) then
   2.325 +  have fA: "f : A -> carrier G" by fast
   2.326 +  from insert have fa: "f a : carrier G" by fast
   2.327 +  from insert have gA: "g : A -> carrier G" by fast
   2.328 +  from insert have ga: "g a : carrier G" by fast
   2.329 +  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
   2.330 +  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   2.331 +    by (simp add: Pi_def)
   2.332 +  show ?case  (* check if all simps are really necessary *)
   2.333 +    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
   2.334 +qed
   2.335 +
   2.336 +(*
   2.337 +lemma prod_Un: "finite A ==> finite B ==>
   2.338 +    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
   2.339 +  -- {* For the natural numbers, we have subtraction. *}
   2.340 +  apply (subst prod_Un_Int [symmetric])
   2.341 +    apply auto
   2.342 +  done
   2.343 +
   2.344 +lemma prod_diff1: "(prod f (A - {a}) :: nat) =
   2.345 +    (if a:A then prod f A - f a else prod f A)"
   2.346 +  apply (case_tac "finite A")
   2.347 +   prefer 2 apply (simp add: prod_def)
   2.348 +  apply (erule finite_induct)
   2.349 +   apply (auto simp add: insert_Diff_if)
   2.350 +  apply (drule_tac a = a in mk_disjoint_insert)
   2.351 +  apply auto
   2.352 +  done
   2.353 +*)
   2.354 +
   2.355 +lemma (in finite_prod) prod_cong:
   2.356 +  "[| A = B; g : B -> carrier G;
   2.357 +      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   2.358 +proof -
   2.359 +  assume prems: "A = B" "g : B -> carrier G"
   2.360 +    "!!i. i : B ==> f i = g i"
   2.361 +  show ?thesis
   2.362 +  proof (cases "finite B")
   2.363 +    case True
   2.364 +    then have "!!A. [| A = B; g : B -> carrier G;
   2.365 +      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   2.366 +    proof induct
   2.367 +      case empty thus ?case by simp
   2.368 +    next
   2.369 +      case (insert B x)
   2.370 +      then have "prod f A = prod f (insert x B)" by simp
   2.371 +      also from insert have "... = f x \<otimes> prod f B"
   2.372 +      proof (intro prod_insert)
   2.373 +	show "finite B" .
   2.374 +      next
   2.375 +	show "x ~: B" .
   2.376 +      next
   2.377 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   2.378 +	  "g \<in> insert x B \<rightarrow> carrier G"
   2.379 +	thus "f : B -> carrier G" by fastsimp
   2.380 +      next
   2.381 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   2.382 +	  "g \<in> insert x B \<rightarrow> carrier G"
   2.383 +	thus "f x \<in> carrier G" by fastsimp
   2.384 +      qed
   2.385 +      also from insert have "... = g x \<otimes> prod g B" by fastsimp
   2.386 +      also from insert have "... = prod g (insert x B)"
   2.387 +      by (intro prod_insert [THEN sym]) auto
   2.388 +      finally show ?case .
   2.389 +    qed
   2.390 +    with prems show ?thesis by simp
   2.391 +  next
   2.392 +    case False with prems show ?thesis by (simp add: prod_def)
   2.393 +  qed
   2.394 +qed
   2.395 +
   2.396 +lemma (in finite_prod) prod_cong1 [cong]:
   2.397 +  "[| A = B; !!i. i : B ==> f i = g i;
   2.398 +      g : B -> carrier G = True |] ==> prod f A = prod g B"
   2.399 +  by (rule prod_cong) fast+
   2.400 +
   2.401 +text {*Usually, if this rule causes a failed congruence proof error,
   2.402 +   the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
   2.403 +   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   2.404 +
   2.405 +declare funcsetI [rule del]
   2.406 +  funcset_mem [rule del]
   2.407 +
   2.408 +subsection {* Summation over the integer interval @{term "{..n}"} *}
   2.409 +
   2.410 +text {*
   2.411 +  For technical reasons (locales) a new locale where the index set is
   2.412 +  restricted to @{term "nat"} is necessary.
   2.413 +*}
   2.414 +
   2.415 +locale finite_prod_nat = finite_prod +
   2.416 +  assumes "False ==> prod f (A::nat set) = prod f A"
   2.417 +
   2.418 +lemma (in finite_prod_nat) natSum_0 [simp]:
   2.419 +  "f : {0::nat} -> carrier G ==> prod f {..0} = f 0"
   2.420 +by (simp add: Pi_def)
   2.421 +
   2.422 +lemma (in finite_prod_nat) natsum_Suc [simp]:
   2.423 +  "f : {..Suc n} -> carrier G ==>
   2.424 +   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
   2.425 +by (simp add: Pi_def atMost_Suc)
   2.426 +
   2.427 +lemma (in finite_prod_nat) natsum_Suc2:
   2.428 +  "f : {..Suc n} -> carrier G ==>
   2.429 +   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
   2.430 +proof (induct n)
   2.431 +  case 0 thus ?case by (simp add: Pi_def)
   2.432 +next
   2.433 +  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
   2.434 +qed
   2.435 +
   2.436 +lemma (in finite_prod_nat) natsum_zero [simp]:
   2.437 +  "prod (%i. \<one>) {..n::nat} = \<one>"
   2.438 +by (induct n) (simp_all add: Pi_def)
   2.439 +
   2.440 +lemma (in finite_prod_nat) natsum_add [simp]:
   2.441 +  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   2.442 +   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
   2.443 +by (induct n) (simp_all add: ac Pi_def prod_closed)
   2.444 +
   2.445 +thm setsum_cong
   2.446 +
   2.447 +ML_setup {* 
   2.448 +
   2.449 +Context.>> (fn thy => (simpset_ref_of thy :=
   2.450 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   2.451 +
   2.452 +lemma "(\<Sum>i\<in>{..10::nat}. if i<=10 then 0 else 1) = (0::nat)"
   2.453 +apply simp done
   2.454 +
   2.455 +lemma (in finite_prod_nat) "prod (%i. if i<=10 then \<one> else x) {..10} = \<one>"
   2.456 +apply (simp add: Pi_def)
   2.457  
   2.458  end