author ballarin Thu Jan 06 21:06:17 2011 +0100 (2011-01-06) changeset 41433 1b8ff770f02c parent 41432 3214c39777ab child 41434 710cdb9e0d17
Abelian group facts obtained from group facts via interpretation (sublocale).
 NEWS file | annotate | diff | revisions src/HOL/Algebra/FiniteProduct.thy file | annotate | diff | revisions src/HOL/Algebra/Ideal.thy file | annotate | diff | revisions src/HOL/Algebra/IntRing.thy file | annotate | diff | revisions src/HOL/Algebra/Ring.thy file | annotate | diff | revisions
```     1.1 --- a/NEWS	Thu Jan 06 17:51:56 2011 +0100
1.2 +++ b/NEWS	Thu Jan 06 21:06:17 2011 +0100
1.3 @@ -498,6 +498,14 @@
1.4  INCOMPATIBILITY.
1.5
1.6
1.7 +*** HOL-Algebra ***
1.8 +
1.9 +* Theorems for additive ring operations (locale abelian_monoid and
1.10 +descendants) are generated by interpretation from their multiplicative
1.11 +counterparts.  This causes slight differences in the simp and clasets.
1.12 +INCOMPATIBILITY.
1.13 +
1.14 +
1.15  *** HOLCF ***
1.16
1.17  * The domain package now runs in definitional mode by default: The
```
```     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Jan 06 17:51:56 2011 +0100
2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jan 06 21:06:17 2011 +0100
2.3 @@ -450,9 +450,9 @@
2.4
2.5  lemma finprod_cong:
2.6    "[| A = B; f \<in> B -> carrier G = True;
2.7 -      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
2.8 +      !!i. i \<in> B =simp=> f i = g i |] ==> finprod G f A = finprod G g B"
2.9    (* This order of prems is slightly faster (3%) than the last two swapped. *)
2.10 -  by (rule finprod_cong') force+
2.11 +  by (rule finprod_cong') (auto simp add: simp_implies_def)
2.12
2.13  text {*Usually, if this rule causes a failed congruence proof error,
2.14    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
```
```     3.1 --- a/src/HOL/Algebra/Ideal.thy	Thu Jan 06 17:51:56 2011 +0100
3.2 +++ b/src/HOL/Algebra/Ideal.thy	Thu Jan 06 21:06:17 2011 +0100
3.3 @@ -155,12 +155,7 @@
3.4
3.5  lemma (in ring) oneideal:
3.6    shows "ideal (carrier R) R"
3.7 -apply (intro idealI  subgroup.intro)
3.8 -      apply (rule is_ring)
3.9 -     apply simp+
3.10 -  apply (fold a_inv_def, simp)
3.11 - apply simp+
3.12 -done
3.13 +  by (rule idealI) (auto intro: is_ring add.subgroupI)
3.14
3.15  lemma (in "domain") zeroprimeideal:
3.16   shows "primeideal {\<zero>} R"
```
```     4.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Jan 06 17:51:56 2011 +0100
4.2 +++ b/src/HOL/Algebra/IntRing.thy	Thu Jan 06 21:06:17 2011 +0100
4.3 @@ -1,5 +1,6 @@
4.4  (*  Title:      HOL/Algebra/IntRing.thy
4.5      Author:     Stephan Hohe, TU Muenchen
4.6 +    Author:     Clemens Ballarin
4.7  *)
4.8
4.9  theory IntRing
4.10 @@ -20,17 +21,16 @@
4.11
4.12  subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
4.13
4.14 -definition
4.15 +abbreviation
4.16    int_ring :: "int ring" ("\<Z>") where
4.17 -  "int_ring = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
4.18 +  "int_ring == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
4.19
4.20  lemma int_Zcarr [intro!, simp]:
4.21    "k \<in> carrier \<Z>"
4.22 -  by (simp add: int_ring_def)
4.23 +  by simp
4.24
4.25  lemma int_is_cring:
4.26    "cring \<Z>"
4.27 -unfolding int_ring_def
4.28  apply (rule cringI)
4.29    apply (rule abelian_groupI, simp_all)
4.30    defer 1
4.31 @@ -62,30 +62,30 @@
4.32      and "pow \<Z> x n = x^n"
4.33  proof -
4.34    -- "Specification"
4.35 -  show "monoid \<Z>" proof qed (auto simp: int_ring_def)
4.36 +  show "monoid \<Z>" proof qed auto
4.37    then interpret int: monoid \<Z> .
4.38
4.39    -- "Carrier"
4.40 -  show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
4.41 +  show "carrier \<Z> = UNIV" by simp
4.42
4.43    -- "Operations"
4.44 -  { fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
4.45 +  { fix x y show "mult \<Z> x y = x * y" by simp }
4.46    note mult = this
4.47 -  show one: "one \<Z> = 1" by (simp add: int_ring_def)
4.48 -  show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
4.49 +  show one: "one \<Z> = 1" by simp
4.50 +  show "pow \<Z> x n = x^n" by (induct n) simp_all
4.51  qed
4.52
4.53  interpretation int: comm_monoid \<Z>
4.54    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
4.55  proof -
4.56    -- "Specification"
4.57 -  show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
4.58 +  show "comm_monoid \<Z>" proof qed auto
4.59    then interpret int: comm_monoid \<Z> .
4.60
4.61    -- "Operations"
4.62 -  { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
4.63 +  { fix x y have "mult \<Z> x y = x * y" by simp }
4.64    note mult = this
4.65 -  have one: "one \<Z> = 1" by (simp add: int_ring_def)
4.66 +  have one: "one \<Z> = 1" by simp
4.67    show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
4.68    proof (cases "finite A")
4.69      case True then show ?thesis proof induct
4.70 @@ -99,18 +99,22 @@
4.71  qed
4.72
4.73  interpretation int: abelian_monoid \<Z>
4.74 -  where "zero \<Z> = 0"
4.75 -    and "add \<Z> x y = x + y"
4.76 -    and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
4.77 +  where int_carrier_eq: "carrier \<Z> = UNIV"
4.78 +    and int_zero_eq: "zero \<Z> = 0"
4.79 +    and int_add_eq: "add \<Z> x y = x + y"
4.80 +    and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
4.81  proof -
4.82    -- "Specification"
4.83 -  show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
4.84 +  show "abelian_monoid \<Z>" proof qed auto
4.85    then interpret int: abelian_monoid \<Z> .
4.86
4.87 +  -- "Carrier"
4.88 +  show "carrier \<Z> = UNIV" by simp
4.89 +
4.90    -- "Operations"
4.91 -  { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
4.92 +  { fix x y show "add \<Z> x y = x + y" by simp }
4.94 -  show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
4.95 +  show zero: "zero \<Z> = 0" by simp
4.96    show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
4.97    proof (cases "finite A")
4.98      case True then show ?thesis proof induct
4.99 @@ -124,30 +128,46 @@
4.100  qed
4.101
4.102  interpretation int: abelian_group \<Z>
4.103 -  where "a_inv \<Z> x = - x"
4.104 -    and "a_minus \<Z> x y = x - y"
4.105 +  (* The equations from the interpretation of abelian_monoid need to be repeated.
4.106 +     Since the morphisms through which the abelian structures are interpreted are
4.107 +     not the identity, the equations of these interpretations are not inherited. *)
4.108 +  (* FIXME *)
4.109 +  where "carrier \<Z> = UNIV"
4.110 +    and "zero \<Z> = 0"
4.111 +    and "add \<Z> x y = x + y"
4.112 +    and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
4.113 +    and int_a_inv_eq: "a_inv \<Z> x = - x"
4.114 +    and int_a_minus_eq: "a_minus \<Z> x y = x - y"
4.115  proof -
4.116    -- "Specification"
4.117    show "abelian_group \<Z>"
4.118    proof (rule abelian_groupI)
4.119      show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
4.120 -      by (simp add: int_ring_def) arith
4.121 -  qed (auto simp: int_ring_def)
4.122 +      by simp arith
4.123 +  qed auto
4.124    then interpret int: abelian_group \<Z> .
4.125 -
4.126    -- "Operations"
4.127 -  { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
4.128 +  { fix x y have "add \<Z> x y = x + y" by simp }
4.130 -  have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
4.131 +  have zero: "zero \<Z> = 0" by simp
4.132    { fix x
4.134      then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
4.135    note a_inv = this
4.136    show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
4.137 -qed
4.139
4.140  interpretation int: "domain" \<Z>
4.141 -  proof qed (auto simp: int_ring_def left_distrib right_distrib)
4.142 +  where "carrier \<Z> = UNIV"
4.143 +    and "zero \<Z> = 0"
4.144 +    and "add \<Z> x y = x + y"
4.145 +    and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
4.146 +    and "a_inv \<Z> x = - x"
4.147 +    and "a_minus \<Z> x y = x - y"
4.148 +proof -
4.149 +  show "domain \<Z>" by unfold_locales (auto simp: left_distrib right_distrib)
4.150 +qed (simp
4.152
4.153
4.154  text {* Removal of occurrences of @{term UNIV} in interpretation result
4.155 @@ -213,8 +233,8 @@
4.156
4.157  lemma int_Idl:
4.158    "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
4.159 -  apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
4.160 -  apply (simp add: cgenideal_def int_ring_def)
4.161 +  apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
4.162 +  apply (simp add: cgenideal_def)
4.163    done
4.164
4.165  lemma multiples_principalideal:
4.166 @@ -232,10 +252,8 @@
4.167     apply (rule int.genideal_ideal, simp)
4.168    apply (rule int_is_cring)
4.169   apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
4.170 - apply (simp add: int_ring_def)
4.171   apply clarsimp defer 1
4.172   apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
4.173 - apply (simp add: int_ring_def)
4.174   apply (elim exE)
4.175  proof -
4.176    fix a b x
4.177 @@ -336,7 +354,7 @@
4.178    shows "EX x. k = x * l + r"
4.179  proof -
4.180    from kIl[unfolded ZMod_def]
4.181 -      have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
4.182 +      have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs)
4.183    from this obtain xl
4.184        where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
4.185        and k: "k = xl + r"
4.186 @@ -382,7 +400,6 @@
4.187        unfolding ZMod_def
4.188    apply (rule a_repr_independence'[symmetric])
4.189    apply (simp add: int_Idl a_r_coset_defs)
4.190 -  apply (simp add: int_ring_def)
4.191    proof -
4.192      have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
4.193      hence "a = (a div m) * m + (a mod m)" by simp
4.194 @@ -426,13 +443,13 @@
4.195  lemma ZFact_zero:
4.196    "carrier (ZFact 0) = (\<Union>a. {{a}})"
4.197  apply (insert int.genideal_zero)
4.198 -apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
4.199 +apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
4.200  done
4.201
4.202  lemma ZFact_one:
4.203    "carrier (ZFact 1) = {UNIV}"
4.204 -apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
4.205 -apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps])
4.206 +apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
4.207 +apply (subst int.genideal_one)
4.208  apply (rule, rule, clarsimp)
4.209   apply (rule, rule, clarsimp)
4.210   apply (rule, clarsimp, arith)
```
```     5.1 --- a/src/HOL/Algebra/Ring.thy	Thu Jan 06 17:51:56 2011 +0100
5.2 +++ b/src/HOL/Algebra/Ring.thy	Thu Jan 06 21:06:17 2011 +0100
5.3 @@ -31,10 +31,23 @@
5.4    assumes a_comm_monoid:
5.5       "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"
5.6
5.7 +definition
5.8 +  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
5.9 +  "finsum G = finprod (| carrier = carrier G, mult = add G, one = zero G |)"
5.10
5.11 -text {*
5.12 -  The following definition is redundant but simple to use.
5.13 -*}
5.14 +syntax
5.15 +  "_finsum" :: "index => idt => 'a set => 'b => 'b"
5.16 +      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
5.17 +syntax (xsymbols)
5.18 +  "_finsum" :: "index => idt => 'a set => 'b => 'b"
5.19 +      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
5.20 +syntax (HTML output)
5.21 +  "_finsum" :: "index => idt => 'a set => 'b => 'b"
5.22 +      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
5.23 +translations
5.24 +  "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
5.25 +  -- {* Beware of argument permutation! *}
5.26 +
5.27
5.28  locale abelian_group = abelian_monoid +
5.29    assumes a_comm_group:
5.30 @@ -85,248 +98,61 @@
5.31
5.32  lemmas monoid_record_simps = partial_object.simps monoid.simps
5.33
5.34 -lemma (in abelian_monoid) a_closed [intro, simp]:
5.35 -  "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier G"
5.36 -  by (rule monoid.m_closed [OF a_monoid, simplified monoid_record_simps])
5.37 -
5.38 -lemma (in abelian_monoid) zero_closed [intro, simp]:
5.39 -  "\<zero> \<in> carrier G"
5.40 -  by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps])
5.41 -
5.42 -lemma (in abelian_group) a_inv_closed [intro, simp]:
5.43 -  "x \<in> carrier G ==> \<ominus> x \<in> carrier G"
5.44 -  by (simp add: a_inv_def
5.45 -    group.inv_closed [OF a_group, simplified monoid_record_simps])
5.46 -
5.47 -lemma (in abelian_group) minus_closed [intro, simp]:
5.48 -  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
5.49 -  by (simp add: a_minus_def)
5.50 -
5.51 -lemma (in abelian_group) a_l_cancel [simp]:
5.52 -  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
5.53 -   (x \<oplus> y = x \<oplus> z) = (y = z)"
5.54 -  by (rule group.l_cancel [OF a_group, simplified monoid_record_simps])
5.55 -
5.56 -lemma (in abelian_group) a_r_cancel [simp]:
5.57 -  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
5.58 -   (y \<oplus> x = z \<oplus> x) = (y = z)"
5.59 -  by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
5.60 -
5.61 -lemma (in abelian_monoid) a_assoc:
5.62 -  "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
5.63 -  (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
5.64 -  by (rule monoid.m_assoc [OF a_monoid, simplified monoid_record_simps])
5.65 -
5.66 -lemma (in abelian_monoid) l_zero [simp]:
5.67 -  "x \<in> carrier G ==> \<zero> \<oplus> x = x"
5.68 -  by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps])
5.69 -
5.70 -lemma (in abelian_group) l_neg:
5.71 -  "x \<in> carrier G ==> \<ominus> x \<oplus> x = \<zero>"
5.72 -  by (simp add: a_inv_def
5.73 -    group.l_inv [OF a_group, simplified monoid_record_simps])
5.74 -
5.75 -lemma (in abelian_monoid) a_comm:
5.76 -  "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
5.77 -  by (rule comm_monoid.m_comm [OF a_comm_monoid,
5.78 -    simplified monoid_record_simps])
5.79 -
5.80 -lemma (in abelian_monoid) a_lcomm:
5.81 -  "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
5.82 -   x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
5.83 -  by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
5.84 -                                simplified monoid_record_simps])
5.85 -
5.86 -lemma (in abelian_monoid) r_zero [simp]:
5.87 -  "x \<in> carrier G ==> x \<oplus> \<zero> = x"
5.88 -  using monoid.r_one [OF a_monoid]
5.89 -  by simp
5.90 -
5.91 -lemma (in abelian_group) r_neg:
5.92 -  "x \<in> carrier G ==> x \<oplus> (\<ominus> x) = \<zero>"
5.93 -  using group.r_inv [OF a_group]
5.94 -  by (simp add: a_inv_def)
5.95 +text {* Transfer facts from multiplicative structures via interpretation. *}
5.96
5.97 -lemma (in abelian_group) minus_zero [simp]:
5.98 -  "\<ominus> \<zero> = \<zero>"
5.99 -  by (simp add: a_inv_def
5.100 -    group.inv_one [OF a_group, simplified monoid_record_simps])
5.101 -
5.102 -lemma (in abelian_group) minus_minus [simp]:
5.103 -  "x \<in> carrier G ==> \<ominus> (\<ominus> x) = x"
5.104 -  using group.inv_inv [OF a_group, simplified monoid_record_simps]
5.105 -  by (simp add: a_inv_def)
5.106 -
5.107 -lemma (in abelian_group) a_inv_inj:
5.108 -  "inj_on (a_inv G) (carrier G)"
5.109 -  using group.inv_inj [OF a_group, simplified monoid_record_simps]
5.110 -  by (simp add: a_inv_def)
5.111 -
5.113 -  "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
5.114 -  using comm_group.inv_mult [OF a_comm_group]
5.115 -  by (simp add: a_inv_def)
5.116 -
5.117 -lemma (in abelian_group) minus_equality:
5.118 -  "[| x \<in> carrier G; y \<in> carrier G; y \<oplus> x = \<zero> |] ==> \<ominus> x = y"
5.119 -  using group.inv_equality [OF a_group]
5.120 -  by (auto simp add: a_inv_def)
5.121 -
5.122 -lemma (in abelian_monoid) minus_unique:
5.123 -  "[| x \<in> carrier G; y \<in> carrier G; y' \<in> carrier G;
5.124 -      y \<oplus> x = \<zero>; x \<oplus> y' = \<zero> |] ==> y = y'"
5.125 -  using monoid.inv_unique [OF a_monoid]
5.126 -  by (simp add: a_inv_def)
5.127 -
5.128 -lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
5.129 -
5.130 -text {* Derive an @{text "abelian_group"} from a @{text "comm_group"} *}
5.131 -lemma comm_group_abelian_groupI:
5.132 -  fixes G (structure)
5.133 -  assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
5.134 -  shows "abelian_group G"
5.135 -proof -
5.136 -  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
5.137 -    by (rule cg)
5.138 -  show "abelian_group G" ..
5.139 -qed
5.140 -
5.141 -
5.142 -subsection {* Sums over Finite Sets *}
5.143 -
5.144 -text {*
5.145 -  This definition makes it easy to lift lemmas from @{term finprod}.
5.146 -*}
5.147 -
5.148 -definition
5.149 -  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
5.150 -  "finsum G f A = finprod (| carrier = carrier G, mult = add G, one = zero G |) f A"
5.151 -
5.152 -syntax
5.153 -  "_finsum" :: "index => idt => 'a set => 'b => 'b"
5.154 -      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
5.155 -syntax (xsymbols)
5.156 -  "_finsum" :: "index => idt => 'a set => 'b => 'b"
5.157 -      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
5.158 -syntax (HTML output)
5.159 -  "_finsum" :: "index => idt => 'a set => 'b => 'b"
5.160 -      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
5.161 -translations
5.162 -  "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
5.163 -  -- {* Beware of argument permutation! *}
5.164 +sublocale abelian_monoid <
5.165 +  add!: monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
5.166 +  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
5.167 +    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
5.168 +    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
5.169 +  by (rule a_monoid) auto
5.170
5.171  context abelian_monoid begin
5.172
5.173 -(*
5.174 -  lemmas finsum_empty [simp] =
5.175 -    comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
5.176 -  is dangeous, because attributes (like simplified) are applied upon opening
5.177 -  the locale, simplified refers to the simpset at that time!!!
5.184
5.185 -  lemmas finsum_empty [simp] =
5.186 -    abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
5.187 -      simplified monoid_record_simps]
5.188 -  makes the locale slow, because proofs are repeated for every
5.189 -  "lemma (in abelian_monoid)" command.
5.190 -  When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down
5.191 -  from 110 secs to 60 secs.
5.192 -*)
5.193 -
5.194 -lemma finsum_empty [simp]:
5.195 -  "finsum G f {} = \<zero>"
5.196 -  by (rule comm_monoid.finprod_empty [OF a_comm_monoid,
5.197 -    folded finsum_def, simplified monoid_record_simps])
5.198 +end
5.199
5.200 -lemma finsum_insert [simp]:
5.201 -  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |]
5.202 -  ==> finsum G f (insert a F) = f a \<oplus> finsum G f F"
5.203 -  by (rule comm_monoid.finprod_insert [OF a_comm_monoid,
5.204 -    folded finsum_def, simplified monoid_record_simps])
5.205 -
5.206 -lemma finsum_zero [simp]:
5.207 -  "finite A ==> (\<Oplus>i\<in>A. \<zero>) = \<zero>"
5.208 -  by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
5.209 -    simplified monoid_record_simps])
5.210 +sublocale abelian_monoid <
5.211 +  add!: comm_monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
5.212 +  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
5.213 +    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
5.214 +    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
5.215 +    and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
5.216 +  by (rule a_comm_monoid) (auto simp: finsum_def)
5.217
5.218 -lemma finsum_closed [simp]:
5.219 -  fixes A
5.220 -  assumes fin: "finite A" and f: "f \<in> A -> carrier G"
5.221 -  shows "finsum G f A \<in> carrier G"
5.222 -  apply (rule comm_monoid.finprod_closed [OF a_comm_monoid,
5.223 -    folded finsum_def, simplified monoid_record_simps])
5.224 -   apply (rule fin)
5.225 -  apply (rule f)
5.226 -  done
5.227 -
5.228 -lemma finsum_Un_Int:
5.229 -  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
5.230 -     finsum G g (A Un B) \<oplus> finsum G g (A Int B) =
5.231 -     finsum G g A \<oplus> finsum G g B"
5.232 -  by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid,
5.233 -    folded finsum_def, simplified monoid_record_simps])
5.234 +context abelian_monoid begin
5.235
5.236 -lemma finsum_Un_disjoint:
5.237 -  "[| finite A; finite B; A Int B = {};
5.238 -      g \<in> A -> carrier G; g \<in> B -> carrier G |]
5.239 -   ==> finsum G g (A Un B) = finsum G g A \<oplus> finsum G g B"
5.240 -  by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid,
5.241 -    folded finsum_def, simplified monoid_record_simps])
5.242 -
5.244 -  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
5.245 -   finsum G (%x. f x \<oplus> g x) A = (finsum G f A \<oplus> finsum G g A)"
5.246 -  by (rule comm_monoid.finprod_multf [OF a_comm_monoid,
5.247 -    folded finsum_def, simplified monoid_record_simps])
5.248 -
5.249 -lemma finsum_cong':
5.250 -  "[| A = B; g : B -> carrier G;
5.251 -      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
5.252 -  by (rule comm_monoid.finprod_cong' [OF a_comm_monoid,
5.253 -    folded finsum_def, simplified monoid_record_simps]) auto
5.254 -
5.255 -lemma finsum_0 [simp]:
5.256 -  "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0"
5.257 -  by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def,
5.258 -    simplified monoid_record_simps])
5.261 +lemmas a_ac = a_assoc a_comm a_lcomm
5.262
5.263 -lemma finsum_Suc [simp]:
5.264 -  "f : {..Suc n} -> carrier G ==>
5.265 -   finsum G f {..Suc n} = (f (Suc n) \<oplus> finsum G f {..n})"
5.266 -  by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def,
5.267 -    simplified monoid_record_simps])
5.268 -
5.269 -lemma finsum_Suc2:
5.270 -  "f : {..Suc n} -> carrier G ==>
5.271 -   finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \<oplus> f 0)"
5.272 -  by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def,
5.273 -    simplified monoid_record_simps])
5.286
5.288 -  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
5.289 -     finsum G (%i. f i \<oplus> g i) {..n::nat} =
5.290 -     finsum G f {..n} \<oplus> finsum G g {..n}"
5.291 -  by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def,
5.292 -    simplified monoid_record_simps])
5.293 -
5.294 -lemma finsum_cong:
5.295 -  "[| A = B; f : B -> carrier G;
5.296 -      !!i. i : B =simp=> f i = g i |] ==> finsum G f A = finsum G g B"
5.297 -  by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
5.298 -    simplified monoid_record_simps]) (auto simp add: simp_implies_def)
5.299 -
5.301  text {*Usually, if this rule causes a failed congruence proof error,
5.302     the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
5.303     Adding @{thm [source] Pi_def} to the simpset is often useful. *}
5.304
5.305 -lemma finsum_reindex:
5.306 -  assumes fin: "finite A"
5.307 -    shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow>
5.308 -        inj_on h A ==> finsum G f (h ` A) = finsum G (%x. f (h x)) A"
5.309 -  using fin apply induct
5.310 -  apply (auto simp add: finsum_insert Pi_def)
5.311 -done
5.313
5.314 -(* The following is wrong.  Needed is the equivalent of (^) for addition,
5.315 +(* The following would be wrong.  Needed is the equivalent of (^) for addition,
5.316    or indeed the canonical embedding from Nat into the monoid.
5.317
5.318  lemma finsum_const:
5.319 @@ -343,18 +169,60 @@
5.320  done
5.321  *)
5.322
5.323 -(* By Jesus Aransay. *)
5.324 -
5.325 -lemma finsum_singleton:
5.326 -  assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
5.327 -  shows "(\<Oplus>j\<in>A. if i = j then f j else \<zero>) = f i"
5.328 -  using i_in_A finsum_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<zero>)"]
5.329 -    fin_A f_Pi finsum_zero [of "A - {i}"]
5.330 -    finsum_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<zero>)" "(\<lambda>i. \<zero>)"]
5.331 -  unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
5.333
5.334  end
5.335
5.336 +sublocale abelian_group <
5.337 +  add!: group "(| carrier = carrier G, mult = add G, one = zero G |)"
5.338 +  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
5.339 +    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
5.340 +    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
5.341 +    and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
5.342 +  by (rule a_group) (auto simp: m_inv_def a_inv_def)
5.343 +
5.344 +context abelian_group begin
5.345 +
5.347 +
5.348 +lemma minus_closed [intro, simp]:
5.349 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
5.350 +  by (simp add: a_minus_def)
5.351 +
5.354 +lemmas l_neg = add.l_inv [simp del]
5.355 +lemmas r_neg = add.r_inv [simp del]
5.360 +
5.361 +end
5.362 +
5.363 +sublocale abelian_group <
5.364 +  add!: comm_group "(| carrier = carrier G, mult = add G, one = zero G |)"
5.365 +  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
5.366 +    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
5.367 +    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
5.368 +    and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
5.369 +    and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
5.370 +  by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def)
5.371 +
5.373 +
5.374 +text {* Derive an @{text "abelian_group"} from a @{text "comm_group"} *}
5.375 +
5.376 +lemma comm_group_abelian_groupI:
5.377 +  fixes G (structure)
5.378 +  assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
5.379 +  shows "abelian_group G"
5.380 +proof -
5.381 +  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
5.382 +    by (rule cg)
5.383 +  show "abelian_group G" ..
5.384 +qed
5.385 +
5.386
5.387  subsection {* Rings: Basic Definitions *}
5.388
5.389 @@ -389,18 +257,22 @@
5.390    by (auto intro: ring.intro
5.391      abelian_group.axioms ring_axioms.intro assms)
5.392
5.393 -lemma (in ring) is_abelian_group:
5.394 +context ring begin
5.395 +
5.396 +lemma is_abelian_group:
5.397    "abelian_group R"
5.398    ..
5.399
5.400 -lemma (in ring) is_monoid:
5.401 +lemma is_monoid:
5.402    "monoid R"
5.403    by (auto intro!: monoidI m_assoc)
5.404
5.405 -lemma (in ring) is_ring:
5.406 +lemma is_ring:
5.407    "ring R"
5.408    by (rule ring_axioms)
5.409
5.410 +end
5.411 +
5.412  lemmas ring_record_simps = monoid_record_simps ring.simps
5.413
5.414  lemma cringI:
5.415 @@ -449,7 +321,7 @@
5.416    assume G: "x \<in> carrier G" "y \<in> carrier G"
5.417    then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
5.418      by (simp only: r_neg l_zero)
5.419 -  with G show ?thesis
5.420 +  with G show ?thesis
5.422  qed
5.423
5.424 @@ -462,11 +334,13 @@
5.425    with G show ?thesis by (simp add: a_ac)
5.426  qed
5.427
5.428 +context ring begin
5.429 +
5.430  text {*
5.431 -  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
5.432 +  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89.
5.433  *}
5.434
5.435 -lemma (in ring) l_null [simp]:
5.436 +lemma l_null [simp]:
5.437    "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
5.438  proof -
5.439    assume R: "x \<in> carrier R"
5.440 @@ -477,7 +351,7 @@
5.441    with R show ?thesis by (simp del: r_zero)
5.442  qed
5.443
5.444 -lemma (in ring) r_null [simp]:
5.445 +lemma r_null [simp]:
5.446    "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
5.447  proof -
5.448    assume R: "x \<in> carrier R"
5.449 @@ -488,7 +362,7 @@
5.450    with R show ?thesis by (simp del: r_zero)
5.451  qed
5.452
5.453 -lemma (in ring) l_minus:
5.454 +lemma l_minus:
5.455    "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
5.456  proof -
5.457    assume R: "x \<in> carrier R" "y \<in> carrier R"
5.458 @@ -499,7 +373,7 @@
5.459    with R show ?thesis by (simp add: a_assoc r_neg)
5.460  qed
5.461
5.462 -lemma (in ring) r_minus:
5.463 +lemma r_minus:
5.464    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
5.465  proof -
5.466    assume R: "x \<in> carrier R" "y \<in> carrier R"
5.467 @@ -510,6 +384,8 @@
5.468    with R show ?thesis by (simp add: a_assoc r_neg )
5.469  qed
5.470
5.471 +end
5.472 +
5.473  lemma (in abelian_group) minus_eq:
5.474    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
5.475    by (simp only: a_minus_def)
5.476 @@ -539,12 +415,13 @@
5.477    r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
5.478    a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
5.479
5.480 -
5.481  lemma (in cring) nat_pow_zero:
5.482    "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
5.483    by (induct n) simp_all
5.484
5.485 -lemma (in ring) one_zeroD:
5.486 +context ring begin
5.487 +
5.488 +lemma one_zeroD:
5.489    assumes onezero: "\<one> = \<zero>"
5.490    shows "carrier R = {\<zero>}"
5.491  proof (rule, rule)
5.492 @@ -559,7 +436,7 @@
5.493    thus "x \<in> {\<zero>}" by fast
5.494  qed fast
5.495
5.496 -lemma (in ring) one_zeroI:
5.497 +lemma one_zeroI:
5.498    assumes carrzero: "carrier R = {\<zero>}"
5.499    shows "\<one> = \<zero>"
5.500  proof -
5.501 @@ -567,14 +444,16 @@
5.502        show "\<one> = \<zero>" by simp
5.503  qed
5.504
5.505 -lemma (in ring) carrier_one_zero:
5.506 +lemma carrier_one_zero:
5.507    shows "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
5.508    by (rule, erule one_zeroI, erule one_zeroD)
5.509
5.510 -lemma (in ring) carrier_one_not_zero:
5.511 +lemma carrier_one_not_zero:
5.512    shows "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
5.514
5.515 +end
5.516 +
5.517  text {* Two examples for use of method algebra *}
5.518
5.519  lemma
5.520 @@ -623,11 +502,13 @@
5.521
5.522  subsection {* Integral Domains *}
5.523
5.524 -lemma (in "domain") zero_not_one [simp]:
5.525 +context "domain" begin
5.526 +
5.527 +lemma zero_not_one [simp]:
5.528    "\<zero> ~= \<one>"
5.529    by (rule not_sym) simp
5.530
5.531 -lemma (in "domain") integral_iff: (* not by default a simp rule! *)
5.532 +lemma integral_iff: (* not by default a simp rule! *)
5.533    "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)"
5.534  proof
5.535    assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
5.536 @@ -637,7 +518,7 @@
5.537    then show "a \<otimes> b = \<zero>" by auto
5.538  qed
5.539
5.540 -lemma (in "domain") m_lcancel:
5.541 +lemma m_lcancel:
5.542    assumes prem: "a ~= \<zero>"
5.543      and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
5.544    shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
5.545 @@ -653,7 +534,7 @@
5.546    assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp
5.547  qed
5.548
5.549 -lemma (in "domain") m_rcancel:
5.550 +lemma m_rcancel:
5.551    assumes prem: "a ~= \<zero>"
5.552      and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
5.553    shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
5.554 @@ -662,6 +543,8 @@
5.555    with R show ?thesis by algebra
5.556  qed
5.557
5.558 +end
5.559 +
5.560
5.561  subsection {* Fields *}
5.562
```