src/HOL/Algebra/Group.thy
 changeset 13817 7e031a968443 parent 13813 722593f2f068 child 13835 12b2ffbe543a
```     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 12 17:55:05 2003 +0100
1.2 +++ b/src/HOL/Algebra/Group.thy	Fri Feb 14 17:35:56 2003 +0100
1.3 @@ -8,7 +8,7 @@
1.4
1.5  header {* Algebraic Structures up to Abelian Groups *}
1.6
1.7 -theory Group = FuncSet:
1.8 +theory Group = FuncSet + FoldSet:
1.9
1.10  text {*
1.11    Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
1.12 @@ -20,12 +20,14 @@
1.13
1.14  subsection {* Definitions *}
1.15
1.16 -record 'a magma =
1.17 +record 'a semigroup =
1.18    carrier :: "'a set"
1.19    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
1.20
1.21 -record 'a group = "'a magma" +
1.22 +record 'a monoid = "'a semigroup" +
1.23    one :: 'a ("\<one>\<index>")
1.24 +
1.25 +record 'a group = "'a monoid" +
1.26    m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
1.27
1.28  locale magma = struct G +
1.29 @@ -37,10 +39,12 @@
1.30      "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.31       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.32
1.33 -locale group = semigroup +
1.34 +locale l_one = struct G +
1.35    assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
1.36 -    and inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
1.37      and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
1.38 +
1.39 +locale group = semigroup + l_one +
1.40 +  assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
1.41      and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
1.42
1.43  subsection {* Cancellation Laws and Basic Properties *}
1.44 @@ -156,6 +160,11 @@
1.45
1.46  declare (in subgroup) group.intro [intro]
1.47
1.48 +lemma (in subgroup) l_oneI [intro]:
1.49 +  includes l_one G
1.50 +  shows "l_one (G(| carrier := H |))"
1.51 +  by rule simp_all
1.52 +
1.53  lemma (in subgroup) group_axiomsI [intro]:
1.54    includes group G
1.55    shows "group_axioms (G(| carrier := H |))"
1.56 @@ -206,8 +215,8 @@
1.57
1.58  declare magma.m_closed [simp]
1.59
1.60 -declare group.one_closed [iff] group.inv_closed [simp]
1.61 -  group.l_one [simp] group.r_one [simp] group.inv_inv [simp]
1.62 +declare l_one.one_closed [iff] group.inv_closed [simp]
1.63 +  l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]
1.64
1.65  lemma subgroup_nonempty:
1.66    "~ subgroup {} G"
1.67 @@ -227,47 +236,57 @@
1.68  subsection {* Direct Products *}
1.69
1.70  constdefs
1.71 -  DirProdMagma ::
1.72 -    "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a \<times> 'b) magma"
1.73 +  DirProdSemigroup ::
1.74 +    "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
1.75 +    => ('a \<times> 'b) semigroup"
1.76 +    (infixr "\<times>\<^sub>s" 80)
1.77 +  "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
1.78 +    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
1.79 +
1.80 +  DirProdMonoid ::
1.81 +    "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
1.82      (infixr "\<times>\<^sub>m" 80)
1.83 -  "G \<times>\<^sub>m H == (| carrier = carrier G \<times> carrier H,
1.84 -    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
1.85 +  "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
1.86 +    mult = mult (G \<times>\<^sub>s H),
1.87 +    one = (one G, one H) |)"
1.88
1.89    DirProdGroup ::
1.90      "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
1.91      (infixr "\<times>\<^sub>g" 80)
1.92    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
1.93      mult = mult (G \<times>\<^sub>m H),
1.94 -    one = (one G, one H),
1.95 +    one = one (G \<times>\<^sub>m H),
1.96      m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
1.97
1.98 -lemma DirProdMagma_magma:
1.99 +lemma DirProdSemigroup_magma:
1.100    includes magma G + magma H
1.101 -  shows "magma (G \<times>\<^sub>m H)"
1.102 -  by rule (auto simp add: DirProdMagma_def)
1.103 +  shows "magma (G \<times>\<^sub>s H)"
1.104 +  by rule (auto simp add: DirProdSemigroup_def)
1.105
1.106 -lemma DirProdMagma_semigroup_axioms:
1.107 +lemma DirProdSemigroup_semigroup_axioms:
1.108    includes semigroup G + semigroup H
1.109 -  shows "semigroup_axioms (G \<times>\<^sub>m H)"
1.110 -  by rule (auto simp add: DirProdMagma_def G.m_assoc H.m_assoc)
1.111 +  shows "semigroup_axioms (G \<times>\<^sub>s H)"
1.112 +  by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
1.113
1.114 -lemma DirProdMagma_semigroup:
1.115 +lemma DirProdSemigroup_semigroup:
1.116    includes semigroup G + semigroup H
1.117 -  shows "semigroup (G \<times>\<^sub>m H)"
1.118 +  shows "semigroup (G \<times>\<^sub>s H)"
1.119    using prems
1.120    by (fast intro: semigroup.intro
1.121 -    DirProdMagma_magma DirProdMagma_semigroup_axioms)
1.122 +    DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
1.123
1.124  lemma DirProdGroup_magma:
1.125    includes magma G + magma H
1.126    shows "magma (G \<times>\<^sub>g H)"
1.127 -  by rule (auto simp add: DirProdGroup_def DirProdMagma_def)
1.128 +  by rule
1.129 +    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)
1.130
1.131  lemma DirProdGroup_semigroup_axioms:
1.132    includes semigroup G + semigroup H
1.133    shows "semigroup_axioms (G \<times>\<^sub>g H)"
1.134    by rule
1.135 -    (auto simp add: DirProdGroup_def DirProdMagma_def G.m_assoc H.m_assoc)
1.136 +    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
1.137 +      G.m_assoc H.m_assoc)
1.138
1.139  lemma DirProdGroup_semigroup:
1.140    includes semigroup G + semigroup H
1.141 @@ -278,18 +297,20 @@
1.142
1.143  (* ... and further lemmas for group ... *)
1.144
1.145 -lemma
1.146 +lemma DirProdGroup_group:
1.147    includes group G + group H
1.148    shows "group (G \<times>\<^sub>g H)"
1.149  by rule
1.150 -  (auto intro: magma.intro semigroup_axioms.intro group_axioms.intro
1.151 -    simp add: DirProdGroup_def DirProdMagma_def
1.152 +  (auto intro: magma.intro l_one.intro
1.153 +      semigroup_axioms.intro group_axioms.intro
1.154 +    simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
1.155        G.m_assoc H.m_assoc G.l_inv H.l_inv)
1.156
1.157  subsection {* Homomorphisms *}
1.158
1.159  constdefs
1.160 -  hom :: "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a => 'b)set"
1.161 +  hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
1.162 +    => ('a => 'b)set"
1.163    "hom G H ==
1.164      {h. h \<in> carrier G -> carrier H &
1.165        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
1.166 @@ -367,6 +388,291 @@
1.167
1.168  lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
1.169
1.170 -locale abelian_group = abelian_semigroup + group
1.171 +locale abelian_monoid = abelian_semigroup + l_one
1.172 +
1.173 +lemma (in abelian_monoid) l_one [simp]:
1.174 +  "x \<in> carrier G ==> x \<otimes> \<one> = x"
1.175 +proof -
1.176 +  assume G: "x \<in> carrier G"
1.177 +  then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
1.178 +  also from G have "... = x" by simp
1.179 +  finally show ?thesis .
1.180 +qed
1.181 +
1.182 +locale abelian_group = abelian_monoid + group
1.183 +
1.184 +subsection {* Products over Finite Sets *}
1.185 +
1.186 +locale finite_prod = abelian_monoid + var prod +
1.187 +  defines "prod == (%f A. if finite A
1.188 +      then foldD (carrier G) (op \<otimes> o f) \<one> A
1.189 +      else arbitrary)"
1.190 +
1.191 +(* TODO: nice syntax for the summation operator inside the locale
1.192 +   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
1.193 +
1.194 +ML_setup {*
1.195 +
1.196 +Context.>> (fn thy => (simpset_ref_of thy :=
1.197 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
1.198 +
1.199 +lemma (in finite_prod) prod_empty [simp]:
1.200 +  "prod f {} = \<one>"
1.201 +  by (simp add: prod_def)
1.202 +
1.203 +ML_setup {*
1.204 +
1.205 +Context.>> (fn thy => (simpset_ref_of thy :=
1.206 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
1.207 +
1.208 +declare funcsetI [intro]
1.209 +  funcset_mem [dest]
1.210 +
1.211 +lemma (in finite_prod) prod_insert [simp]:
1.212 +  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
1.213 +   prod f (insert a F) = f a \<otimes> prod f F"
1.214 +  apply (rule trans)
1.215 +  apply (simp add: prod_def)
1.216 +  apply (rule trans)
1.217 +  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
1.218 +    apply simp
1.219 +    apply (rule m_lcomm)
1.220 +      apply fast apply fast apply assumption
1.221 +    apply (fastsimp intro: m_closed)
1.222 +    apply simp+ apply fast
1.223 +  apply (auto simp add: prod_def)
1.224 +  done
1.225 +
1.226 +lemma (in finite_prod) prod_one:
1.227 +  "finite A ==> prod (%i. \<one>) A = \<one>"
1.228 +proof (induct set: Finites)
1.229 +  case empty show ?case by simp
1.230 +next
1.231 +  case (insert A a)
1.232 +  have "(%i. \<one>) \<in> A -> carrier G" by auto
1.233 +  with insert show ?case by simp
1.234 +qed
1.235 +
1.236 +(*
1.237 +lemma prod_eq_0_iff [simp]:
1.238 +    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
1.239 +  by (induct set: Finites) auto
1.240 +
1.241 +lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
1.242 +  apply (case_tac "finite A")
1.243 +   prefer 2 apply (simp add: prod_def)
1.244 +  apply (erule rev_mp)
1.245 +  apply (erule finite_induct)
1.246 +   apply auto
1.247 +  done
1.248 +
1.249 +lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
1.250 +*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
1.251 +(*
1.252 +  by (induct set: Finites) auto
1.253 +*)
1.254 +
1.255 +lemma (in finite_prod) prod_closed:
1.256 +  fixes A
1.257 +  assumes fin: "finite A" and f: "f \<in> A -> carrier G"
1.258 +  shows "prod f A \<in> carrier G"
1.259 +using fin f
1.260 +proof induct
1.261 +  case empty show ?case by simp
1.262 +next
1.263 +  case (insert A a)
1.264 +  then have a: "f a \<in> carrier G" by fast
1.265 +  from insert have A: "f \<in> A -> carrier G" by fast
1.266 +  from insert A a show ?case by simp
1.267 +qed
1.268 +
1.269 +lemma funcset_Int_left [simp, intro]:
1.270 +  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
1.271 +  by fast
1.272 +
1.273 +lemma funcset_Un_left [iff]:
1.274 +  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
1.275 +  by fast
1.276 +
1.277 +lemma (in finite_prod) prod_Un_Int:
1.278 +  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
1.279 +   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
1.280 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
1.281 +proof (induct set: Finites)
1.282 +  case empty then show ?case by (simp add: prod_closed)
1.283 +next
1.284 +  case (insert A a)
1.285 +  then have a: "g a \<in> carrier G" by fast
1.286 +  from insert have A: "g \<in> A -> carrier G" by fast
1.287 +  from insert A a show ?case
1.288 +    by (simp add: ac Int_insert_left insert_absorb prod_closed
1.289 +          Int_mono2 Un_subset_iff)
1.290 +qed
1.291 +
1.292 +lemma (in finite_prod) prod_Un_disjoint:
1.293 +  "[| finite A; finite B; A Int B = {};
1.294 +      g \<in> A -> carrier G; g \<in> B -> carrier G |]
1.295 +   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
1.296 +  apply (subst prod_Un_Int [symmetric])
1.297 +    apply (auto simp add: prod_closed)
1.298 +  done
1.299 +
1.300 +(*
1.301 +lemma prod_UN_disjoint:
1.302 +  fixes f :: "'a => 'b::plus_ac0"
1.303 +  shows
1.304 +    "finite I ==> (ALL i:I. finite (A i)) ==>
1.305 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.306 +      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
1.307 +  apply (induct set: Finites)
1.308 +   apply simp
1.309 +  apply atomize
1.310 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
1.311 +   prefer 2 apply blast
1.312 +  apply (subgoal_tac "A x Int UNION F A = {}")
1.313 +   prefer 2 apply blast
1.314 +  apply (simp add: prod_Un_disjoint)
1.315 +  done
1.316 +*)
1.317 +
1.319 +  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
1.320 +   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
1.321 +proof (induct set: Finites)
1.322 +  case empty show ?case by simp
1.323 +next
1.324 +  case (insert A a) then
1.325 +  have fA: "f : A -> carrier G" by fast
1.326 +  from insert have fa: "f a : carrier G" by fast
1.327 +  from insert have gA: "g : A -> carrier G" by fast
1.328 +  from insert have ga: "g a : carrier G" by fast
1.329 +  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
1.330 +  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
1.331 +    by (simp add: Pi_def)
1.332 +  show ?case  (* check if all simps are really necessary *)
1.333 +    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
1.334 +qed
1.335 +
1.336 +(*
1.337 +lemma prod_Un: "finite A ==> finite B ==>
1.338 +    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
1.339 +  -- {* For the natural numbers, we have subtraction. *}
1.340 +  apply (subst prod_Un_Int [symmetric])
1.341 +    apply auto
1.342 +  done
1.343 +
1.344 +lemma prod_diff1: "(prod f (A - {a}) :: nat) =
1.345 +    (if a:A then prod f A - f a else prod f A)"
1.346 +  apply (case_tac "finite A")
1.347 +   prefer 2 apply (simp add: prod_def)
1.348 +  apply (erule finite_induct)
1.349 +   apply (auto simp add: insert_Diff_if)
1.350 +  apply (drule_tac a = a in mk_disjoint_insert)
1.351 +  apply auto
1.352 +  done
1.353 +*)
1.354 +
1.355 +lemma (in finite_prod) prod_cong:
1.356 +  "[| A = B; g : B -> carrier G;
1.357 +      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
1.358 +proof -
1.359 +  assume prems: "A = B" "g : B -> carrier G"
1.360 +    "!!i. i : B ==> f i = g i"
1.361 +  show ?thesis
1.362 +  proof (cases "finite B")
1.363 +    case True
1.364 +    then have "!!A. [| A = B; g : B -> carrier G;
1.365 +      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
1.366 +    proof induct
1.367 +      case empty thus ?case by simp
1.368 +    next
1.369 +      case (insert B x)
1.370 +      then have "prod f A = prod f (insert x B)" by simp
1.371 +      also from insert have "... = f x \<otimes> prod f B"
1.372 +      proof (intro prod_insert)
1.373 +	show "finite B" .
1.374 +      next
1.375 +	show "x ~: B" .
1.376 +      next
1.377 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.378 +	  "g \<in> insert x B \<rightarrow> carrier G"
1.379 +	thus "f : B -> carrier G" by fastsimp
1.380 +      next
1.381 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.382 +	  "g \<in> insert x B \<rightarrow> carrier G"
1.383 +	thus "f x \<in> carrier G" by fastsimp
1.384 +      qed
1.385 +      also from insert have "... = g x \<otimes> prod g B" by fastsimp
1.386 +      also from insert have "... = prod g (insert x B)"
1.387 +      by (intro prod_insert [THEN sym]) auto
1.388 +      finally show ?case .
1.389 +    qed
1.390 +    with prems show ?thesis by simp
1.391 +  next
1.392 +    case False with prems show ?thesis by (simp add: prod_def)
1.393 +  qed
1.394 +qed
1.395 +
1.396 +lemma (in finite_prod) prod_cong1 [cong]:
1.397 +  "[| A = B; !!i. i : B ==> f i = g i;
1.398 +      g : B -> carrier G = True |] ==> prod f A = prod g B"
1.399 +  by (rule prod_cong) fast+
1.400 +
1.401 +text {*Usually, if this rule causes a failed congruence proof error,
1.402 +   the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
1.403 +   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
1.404 +
1.405 +declare funcsetI [rule del]
1.406 +  funcset_mem [rule del]
1.407 +
1.408 +subsection {* Summation over the integer interval @{term "{..n}"} *}
1.409 +
1.410 +text {*
1.411 +  For technical reasons (locales) a new locale where the index set is
1.412 +  restricted to @{term "nat"} is necessary.
1.413 +*}
1.414 +
1.415 +locale finite_prod_nat = finite_prod +
1.416 +  assumes "False ==> prod f (A::nat set) = prod f A"
1.417 +
1.418 +lemma (in finite_prod_nat) natSum_0 [simp]:
1.419 +  "f : {0::nat} -> carrier G ==> prod f {..0} = f 0"
1.421 +
1.422 +lemma (in finite_prod_nat) natsum_Suc [simp]:
1.423 +  "f : {..Suc n} -> carrier G ==>
1.424 +   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
1.425 +by (simp add: Pi_def atMost_Suc)
1.426 +
1.427 +lemma (in finite_prod_nat) natsum_Suc2:
1.428 +  "f : {..Suc n} -> carrier G ==>
1.429 +   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
1.430 +proof (induct n)
1.431 +  case 0 thus ?case by (simp add: Pi_def)
1.432 +next
1.433 +  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
1.434 +qed
1.435 +
1.436 +lemma (in finite_prod_nat) natsum_zero [simp]:
1.437 +  "prod (%i. \<one>) {..n::nat} = \<one>"
1.438 +by (induct n) (simp_all add: Pi_def)
1.439 +
1.440 +lemma (in finite_prod_nat) natsum_add [simp]:
1.441 +  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
1.442 +   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
1.443 +by (induct n) (simp_all add: ac Pi_def prod_closed)
1.444 +
1.445 +thm setsum_cong
1.446 +
1.447 +ML_setup {*
1.448 +
1.449 +Context.>> (fn thy => (simpset_ref_of thy :=
1.450 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
1.451 +
1.452 +lemma "(\<Sum>i\<in>{..10::nat}. if i<=10 then 0 else 1) = (0::nat)"
1.453 +apply simp done
1.454 +
1.455 +lemma (in finite_prod_nat) "prod (%i. if i<=10 then \<one> else x) {..10} = \<one>"