src/HOL/Algebra/Group.thy
changeset 13835 12b2ffbe543a
parent 13817 7e031a968443
child 13854 91c9ab25fece
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 26 14:26:18 2003 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Thu Feb 27 15:12:29 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 + FoldSet:
     1.8 +theory Group = FuncSet:
     1.9  
    1.10  text {*
    1.11    Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    1.12 @@ -20,6 +20,14 @@
    1.13  
    1.14  subsection {* Definitions *}
    1.15  
    1.16 +(* The following may be unnecessary. *)
    1.17 +text {*
    1.18 +  We write groups additively.  This simplifies notation for rings.
    1.19 +  All rings have an additive inverse, only fields have a
    1.20 +  multiplicative one.  This definitions reduces the need for
    1.21 +  qualifiers.
    1.22 +*}
    1.23 +
    1.24  record 'a semigroup =
    1.25    carrier :: "'a set"
    1.26    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    1.27 @@ -401,278 +409,4 @@
    1.28  
    1.29  locale abelian_group = abelian_monoid + group
    1.30  
    1.31 -subsection {* Products over Finite Sets *}
    1.32 -
    1.33 -locale finite_prod = abelian_monoid + var prod +
    1.34 -  defines "prod == (%f A. if finite A
    1.35 -      then foldD (carrier G) (op \<otimes> o f) \<one> A
    1.36 -      else arbitrary)"
    1.37 -
    1.38 -(* TODO: nice syntax for the summation operator inside the locale
    1.39 -   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
    1.40 -
    1.41 -ML_setup {* 
    1.42 -
    1.43 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.44 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    1.45 -
    1.46 -lemma (in finite_prod) prod_empty [simp]: 
    1.47 -  "prod f {} = \<one>"
    1.48 -  by (simp add: prod_def)
    1.49 -
    1.50 -ML_setup {* 
    1.51 -
    1.52 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.53 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    1.54 -
    1.55 -declare funcsetI [intro]
    1.56 -  funcset_mem [dest]
    1.57 -
    1.58 -lemma (in finite_prod) prod_insert [simp]:
    1.59 -  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
    1.60 -   prod f (insert a F) = f a \<otimes> prod f F"
    1.61 -  apply (rule trans)
    1.62 -  apply (simp add: prod_def)
    1.63 -  apply (rule trans)
    1.64 -  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
    1.65 -    apply simp
    1.66 -    apply (rule m_lcomm)
    1.67 -      apply fast apply fast apply assumption
    1.68 -    apply (fastsimp intro: m_closed)
    1.69 -    apply simp+ apply fast
    1.70 -  apply (auto simp add: prod_def)
    1.71 -  done
    1.72 -
    1.73 -lemma (in finite_prod) prod_one:
    1.74 -  "finite A ==> prod (%i. \<one>) A = \<one>"
    1.75 -proof (induct set: Finites)
    1.76 -  case empty show ?case by simp
    1.77 -next
    1.78 -  case (insert A a)
    1.79 -  have "(%i. \<one>) \<in> A -> carrier G" by auto
    1.80 -  with insert show ?case by simp
    1.81 -qed
    1.82 -
    1.83 -(*
    1.84 -lemma prod_eq_0_iff [simp]:
    1.85 -    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
    1.86 -  by (induct set: Finites) auto
    1.87 -
    1.88 -lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
    1.89 -  apply (case_tac "finite A")
    1.90 -   prefer 2 apply (simp add: prod_def)
    1.91 -  apply (erule rev_mp)
    1.92 -  apply (erule finite_induct)
    1.93 -   apply auto
    1.94 -  done
    1.95 -
    1.96 -lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
    1.97 -*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
    1.98 -(*
    1.99 -  by (induct set: Finites) auto
   1.100 -*)
   1.101 -
   1.102 -lemma (in finite_prod) prod_closed:
   1.103 -  fixes A
   1.104 -  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   1.105 -  shows "prod f A \<in> carrier G"
   1.106 -using fin f
   1.107 -proof induct
   1.108 -  case empty show ?case by simp
   1.109 -next
   1.110 -  case (insert A a)
   1.111 -  then have a: "f a \<in> carrier G" by fast
   1.112 -  from insert have A: "f \<in> A -> carrier G" by fast
   1.113 -  from insert A a show ?case by simp
   1.114 -qed
   1.115 -
   1.116 -lemma funcset_Int_left [simp, intro]:
   1.117 -  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
   1.118 -  by fast
   1.119 -
   1.120 -lemma funcset_Un_left [iff]:
   1.121 -  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   1.122 -  by fast
   1.123 -
   1.124 -lemma (in finite_prod) prod_Un_Int:
   1.125 -  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   1.126 -   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
   1.127 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   1.128 -proof (induct set: Finites)
   1.129 -  case empty then show ?case by (simp add: prod_closed)
   1.130 -next
   1.131 -  case (insert A a)
   1.132 -  then have a: "g a \<in> carrier G" by fast
   1.133 -  from insert have A: "g \<in> A -> carrier G" by fast
   1.134 -  from insert A a show ?case
   1.135 -    by (simp add: ac Int_insert_left insert_absorb prod_closed
   1.136 -          Int_mono2 Un_subset_iff) 
   1.137 -qed
   1.138 -
   1.139 -lemma (in finite_prod) prod_Un_disjoint:
   1.140 -  "[| finite A; finite B; A Int B = {};
   1.141 -      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   1.142 -   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
   1.143 -  apply (subst prod_Un_Int [symmetric])
   1.144 -    apply (auto simp add: prod_closed)
   1.145 -  done
   1.146 -
   1.147 -(*
   1.148 -lemma prod_UN_disjoint:
   1.149 -  fixes f :: "'a => 'b::plus_ac0"
   1.150 -  shows
   1.151 -    "finite I ==> (ALL i:I. finite (A i)) ==>
   1.152 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   1.153 -      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
   1.154 -  apply (induct set: Finites)
   1.155 -   apply simp
   1.156 -  apply atomize
   1.157 -  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   1.158 -   prefer 2 apply blast
   1.159 -  apply (subgoal_tac "A x Int UNION F A = {}")
   1.160 -   prefer 2 apply blast
   1.161 -  apply (simp add: prod_Un_disjoint)
   1.162 -  done
   1.163 -*)
   1.164 -
   1.165 -lemma (in finite_prod) prod_addf:
   1.166 -  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   1.167 -   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
   1.168 -proof (induct set: Finites)
   1.169 -  case empty show ?case by simp
   1.170 -next
   1.171 -  case (insert A a) then
   1.172 -  have fA: "f : A -> carrier G" by fast
   1.173 -  from insert have fa: "f a : carrier G" by fast
   1.174 -  from insert have gA: "g : A -> carrier G" by fast
   1.175 -  from insert have ga: "g a : carrier G" by fast
   1.176 -  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
   1.177 -  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   1.178 -    by (simp add: Pi_def)
   1.179 -  show ?case  (* check if all simps are really necessary *)
   1.180 -    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
   1.181 -qed
   1.182 -
   1.183 -(*
   1.184 -lemma prod_Un: "finite A ==> finite B ==>
   1.185 -    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
   1.186 -  -- {* For the natural numbers, we have subtraction. *}
   1.187 -  apply (subst prod_Un_Int [symmetric])
   1.188 -    apply auto
   1.189 -  done
   1.190 -
   1.191 -lemma prod_diff1: "(prod f (A - {a}) :: nat) =
   1.192 -    (if a:A then prod f A - f a else prod f A)"
   1.193 -  apply (case_tac "finite A")
   1.194 -   prefer 2 apply (simp add: prod_def)
   1.195 -  apply (erule finite_induct)
   1.196 -   apply (auto simp add: insert_Diff_if)
   1.197 -  apply (drule_tac a = a in mk_disjoint_insert)
   1.198 -  apply auto
   1.199 -  done
   1.200 -*)
   1.201 -
   1.202 -lemma (in finite_prod) prod_cong:
   1.203 -  "[| A = B; g : B -> carrier G;
   1.204 -      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   1.205 -proof -
   1.206 -  assume prems: "A = B" "g : B -> carrier G"
   1.207 -    "!!i. i : B ==> f i = g i"
   1.208 -  show ?thesis
   1.209 -  proof (cases "finite B")
   1.210 -    case True
   1.211 -    then have "!!A. [| A = B; g : B -> carrier G;
   1.212 -      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   1.213 -    proof induct
   1.214 -      case empty thus ?case by simp
   1.215 -    next
   1.216 -      case (insert B x)
   1.217 -      then have "prod f A = prod f (insert x B)" by simp
   1.218 -      also from insert have "... = f x \<otimes> prod f B"
   1.219 -      proof (intro prod_insert)
   1.220 -	show "finite B" .
   1.221 -      next
   1.222 -	show "x ~: B" .
   1.223 -      next
   1.224 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   1.225 -	  "g \<in> insert x B \<rightarrow> carrier G"
   1.226 -	thus "f : B -> carrier G" by fastsimp
   1.227 -      next
   1.228 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   1.229 -	  "g \<in> insert x B \<rightarrow> carrier G"
   1.230 -	thus "f x \<in> carrier G" by fastsimp
   1.231 -      qed
   1.232 -      also from insert have "... = g x \<otimes> prod g B" by fastsimp
   1.233 -      also from insert have "... = prod g (insert x B)"
   1.234 -      by (intro prod_insert [THEN sym]) auto
   1.235 -      finally show ?case .
   1.236 -    qed
   1.237 -    with prems show ?thesis by simp
   1.238 -  next
   1.239 -    case False with prems show ?thesis by (simp add: prod_def)
   1.240 -  qed
   1.241 -qed
   1.242 -
   1.243 -lemma (in finite_prod) prod_cong1 [cong]:
   1.244 -  "[| A = B; !!i. i : B ==> f i = g i;
   1.245 -      g : B -> carrier G = True |] ==> prod f A = prod g B"
   1.246 -  by (rule prod_cong) fast+
   1.247 -
   1.248 -text {*Usually, if this rule causes a failed congruence proof error,
   1.249 -   the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
   1.250 -   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   1.251 -
   1.252 -declare funcsetI [rule del]
   1.253 -  funcset_mem [rule del]
   1.254 -
   1.255 -subsection {* Summation over the integer interval @{term "{..n}"} *}
   1.256 -
   1.257 -text {*
   1.258 -  For technical reasons (locales) a new locale where the index set is
   1.259 -  restricted to @{term "nat"} is necessary.
   1.260 -*}
   1.261 -
   1.262 -locale finite_prod_nat = finite_prod +
   1.263 -  assumes "False ==> prod f (A::nat set) = prod f A"
   1.264 -
   1.265 -lemma (in finite_prod_nat) natSum_0 [simp]:
   1.266 -  "f : {0::nat} -> carrier G ==> prod f {..0} = f 0"
   1.267 -by (simp add: Pi_def)
   1.268 -
   1.269 -lemma (in finite_prod_nat) natsum_Suc [simp]:
   1.270 -  "f : {..Suc n} -> carrier G ==>
   1.271 -   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
   1.272 -by (simp add: Pi_def atMost_Suc)
   1.273 -
   1.274 -lemma (in finite_prod_nat) natsum_Suc2:
   1.275 -  "f : {..Suc n} -> carrier G ==>
   1.276 -   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
   1.277 -proof (induct n)
   1.278 -  case 0 thus ?case by (simp add: Pi_def)
   1.279 -next
   1.280 -  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
   1.281 -qed
   1.282 -
   1.283 -lemma (in finite_prod_nat) natsum_zero [simp]:
   1.284 -  "prod (%i. \<one>) {..n::nat} = \<one>"
   1.285 -by (induct n) (simp_all add: Pi_def)
   1.286 -
   1.287 -lemma (in finite_prod_nat) natsum_add [simp]:
   1.288 -  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   1.289 -   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
   1.290 -by (induct n) (simp_all add: ac Pi_def prod_closed)
   1.291 -
   1.292 -thm setsum_cong
   1.293 -
   1.294 -ML_setup {* 
   1.295 -
   1.296 -Context.>> (fn thy => (simpset_ref_of thy :=
   1.297 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.298 -
   1.299 -lemma "(\<Sum>i\<in>{..10::nat}. if i<=10 then 0 else 1) = (0::nat)"
   1.300 -apply simp done
   1.301 -
   1.302 -lemma (in finite_prod_nat) "prod (%i. if i<=10 then \<one> else x) {..10} = \<one>"
   1.303 -apply (simp add: Pi_def)
   1.304 -
   1.305  end