Abelian group facts obtained from group facts via interpretation (sublocale).
authorballarin
Thu Jan 06 21:06:17 2011 +0100 (2011-01-06)
changeset 414331b8ff770f02c
parent 41432 3214c39777ab
child 41434 710cdb9e0d17
Abelian group facts obtained from group facts via interpretation (sublocale).
NEWS
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Ring.thy
     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.93    note add = this
    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.129    note add = this
   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.133      have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
   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.138 +qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
   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.151 +    add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
   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.112 -lemma (in abelian_group) minus_add:
   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.178 +lemmas a_closed = add.m_closed 
   5.179 +lemmas zero_closed = add.one_closed
   5.180 +lemmas a_assoc = add.m_assoc
   5.181 +lemmas l_zero = add.l_one
   5.182 +lemmas r_zero = add.r_one
   5.183 +lemmas minus_unique = add.inv_unique
   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.243 -lemma finsum_addf:
   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.259 +lemmas a_comm = add.m_comm
   5.260 +lemmas a_lcomm = add.m_lcomm
   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.274 +lemmas finsum_empty = add.finprod_empty
   5.275 +lemmas finsum_insert = add.finprod_insert
   5.276 +lemmas finsum_zero = add.finprod_one
   5.277 +lemmas finsum_closed = add.finprod_closed
   5.278 +lemmas finsum_Un_Int = add.finprod_Un_Int
   5.279 +lemmas finsum_Un_disjoint = add.finprod_Un_disjoint
   5.280 +lemmas finsum_addf = add.finprod_multf
   5.281 +lemmas finsum_cong' = add.finprod_cong'
   5.282 +lemmas finsum_0 = add.finprod_0
   5.283 +lemmas finsum_Suc = add.finprod_Suc
   5.284 +lemmas finsum_Suc2 = add.finprod_Suc2
   5.285 +lemmas finsum_add = add.finprod_mult
   5.286  
   5.287 -lemma finsum_add [simp]:
   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.300 +lemmas finsum_cong = add.finprod_cong
   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.312 +lemmas finsum_reindex = add.finprod_reindex
   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.332 +lemmas finsum_singleton = add.finprod_singleton
   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.346 +lemmas a_inv_closed = add.inv_closed
   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.352 +lemmas a_l_cancel = add.l_cancel
   5.353 +lemmas a_r_cancel = add.r_cancel
   5.354 +lemmas l_neg = add.l_inv [simp del]
   5.355 +lemmas r_neg = add.r_inv [simp del]
   5.356 +lemmas minus_zero = add.inv_one
   5.357 +lemmas minus_minus = add.inv_inv
   5.358 +lemmas a_inv_inj = add.inv_inj
   5.359 +lemmas minus_equality = add.inv_equality
   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.372 +lemmas (in abelian_group) minus_add = add.inv_mult
   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.421      by (simp add: a_ac)
   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.513    by (simp add: carrier_one_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