author wenzelm Fri Apr 23 21:46:04 2004 +0200 (2004-04-23) changeset 14666 65f8680c3f16 parent 14665 d2e5df3d1201 child 14667 5a899cd54366
improved notation;
 src/HOL/Algebra/Bij.thy file | annotate | diff | revisions src/HOL/Algebra/CRing.thy file | annotate | diff | revisions src/HOL/Algebra/Coset.thy file | annotate | diff | revisions src/HOL/Algebra/FiniteProduct.thy file | annotate | diff | revisions src/HOL/Algebra/Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/Sylow.thy file | annotate | diff | revisions src/HOL/Algebra/UnivPoly.thy file | annotate | diff | revisions src/HOL/Algebra/document/root.tex file | annotate | diff | revisions
     1.1 --- a/src/HOL/Algebra/Bij.thy	Fri Apr 23 20:52:04 2004 +0200
1.2 +++ b/src/HOL/Algebra/Bij.thy	Fri Apr 23 21:46:04 2004 +0200
1.3 @@ -3,41 +3,41 @@
1.4      Author:     Florian Kammueller, with new proofs by L C Paulson
1.5  *)
1.6
1.7 -
1.8 -header{*Bijections of a Set, Permutation Groups, Automorphism Groups*}
1.9 +header {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
1.10
1.11  theory Bij = Group:
1.12
1.13  constdefs
1.14 -  Bij :: "'a set => (('a => 'a)set)"
1.15 +  Bij :: "'a set => ('a => 'a) set"
1.16      --{*Only extensional functions, since otherwise we get too many.*}
1.17 -    "Bij S == extensional S \<inter> {f. fS = S & inj_on f S}"
1.18 +  "Bij S == extensional S \<inter> {f. fS = S & inj_on f S}"
1.19
1.20 -   BijGroup ::  "'a set => (('a => 'a) monoid)"
1.21 -   "BijGroup S == (| carrier = Bij S,
1.22 -		     mult  = %g: Bij S. %f: Bij S. compose S g f,
1.23 -		     one = %x: S. x |)"
1.24 +  BijGroup :: "'a set => ('a => 'a) monoid"
1.25 +  "BijGroup S ==
1.26 +    (| carrier = Bij S,
1.27 +      mult = %g: Bij S. %f: Bij S. compose S g f,
1.28 +      one = %x: S. x |)"
1.29
1.30
1.31  declare Id_compose [simp] compose_Id [simp]
1.32
1.33  lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
1.34 -by (simp add: Bij_def)
1.35 +  by (simp add: Bij_def)
1.36
1.37  lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
1.38 -by (auto simp add: Bij_def Pi_def)
1.39 +  by (auto simp add: Bij_def Pi_def)
1.40
1.41  lemma Bij_imp_apply: "f \<in> Bij S ==> f  S = S"
1.42 -by (simp add: Bij_def)
1.43 +  by (simp add: Bij_def)
1.44
1.45  lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S"
1.46 -by (simp add: Bij_def)
1.47 +  by (simp add: Bij_def)
1.48
1.49  lemma BijI: "[| f \<in> extensional(S); fS = S; inj_on f S |] ==> f \<in> Bij S"
1.50 -by (simp add: Bij_def)
1.51 +  by (simp add: Bij_def)
1.52
1.53
1.54 -subsection{*Bijections Form a Group*}
1.55 +subsection {*Bijections Form a Group *}
1.56
1.57  lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
1.58  apply (simp add: Bij_def)
1.59 @@ -60,7 +60,7 @@
1.60
1.61  lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
1.62  apply (rule BijI)
1.63 -  apply (simp add: compose_extensional)
1.64 +  apply (simp add: compose_extensional)
1.65   apply (blast del: equalityI
1.66                intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on)
1.67  apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on)
1.68 @@ -70,44 +70,44 @@
1.69       "f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
1.70  apply (rule compose_Inv_id)
1.71   apply (simp add: Bij_imp_inj_on)
1.72 -apply (simp add: Bij_imp_apply)
1.73 +apply (simp add: Bij_imp_apply)
1.74  done
1.75
1.76  theorem group_BijGroup: "group (BijGroup S)"
1.77 -apply (simp add: BijGroup_def)
1.78 +apply (simp add: BijGroup_def)
1.79  apply (rule groupI)
1.80      apply (simp add: compose_Bij)
1.81     apply (simp add: id_Bij)
1.82    apply (simp add: compose_Bij)
1.83    apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset)
1.84   apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
1.85 -apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
1.86 +apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
1.87  done
1.88
1.89
1.90  subsection{*Automorphisms Form a Group*}
1.91
1.92  lemma Bij_Inv_mem: "[|  f \<in> Bij S;  x : S |] ==> Inv S f x : S"
1.93 -by (simp add: Bij_def Inv_mem)
1.94 +by (simp add: Bij_def Inv_mem)
1.95
1.96  lemma Bij_Inv_lemma:
1.97   assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
1.98 - shows "[| h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S |]
1.99 + shows "[| h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S |]
1.100          ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
1.101 -apply (simp add: Bij_def)
1.102 +apply (simp add: Bij_def)
1.103  apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'", clarify)
1.104   apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
1.105  done
1.106
1.107  constdefs
1.108 - auto :: "('a,'b) monoid_scheme => ('a => 'a)set"
1.109 +  auto :: "('a, 'b) monoid_scheme => ('a => 'a) set"
1.110    "auto G == hom G G \<inter> Bij (carrier G)"
1.111
1.112 -  AutoGroup :: "[('a,'c) monoid_scheme] => ('a=>'a) monoid"
1.113 +  AutoGroup :: "('a, 'c) monoid_scheme => ('a => 'a) monoid"
1.114    "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
1.115
1.116  lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
1.117 -  by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
1.118 +  by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
1.119
1.120  lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G"
1.121    by (simp add:  Pi_I group.axioms)
1.122 @@ -122,27 +122,26 @@
1.123       "f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)"
1.124  apply (rule group.inv_equality)
1.125  apply (rule group_BijGroup)
1.126 -apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
1.127 +apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
1.128  done
1.129
1.130  lemma subgroup_auto:
1.131        "group G ==> subgroup (auto G) (BijGroup (carrier G))"
1.132 -apply (rule group.subgroupI)
1.133 -    apply (rule group_BijGroup)
1.134 -   apply (force simp add: auto_def BijGroup_def)
1.135 -  apply (blast intro: dest: id_in_auto)
1.136 +apply (rule group.subgroupI)
1.137 +    apply (rule group_BijGroup)
1.138 +   apply (force simp add: auto_def BijGroup_def)
1.139 +  apply (blast intro: dest: id_in_auto)
1.140   apply (simp del: restrict_apply
1.141 -	     add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
1.142 +             add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
1.143  apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij)
1.144  done
1.145
1.146  theorem AutoGroup: "group G ==> group (AutoGroup G)"
1.147 -apply (simp add: AutoGroup_def)
1.148 +apply (simp add: AutoGroup_def)
1.149  apply (rule Group.subgroup.groupI)
1.150 -apply (erule subgroup_auto)
1.151 -apply (insert Bij.group_BijGroup [of "carrier G"])
1.152 -apply (simp_all add: group_def)
1.153 +apply (erule subgroup_auto)
1.154 +apply (insert Bij.group_BijGroup [of "carrier G"])
1.155 +apply (simp_all add: group_def)
1.156  done
1.157
1.158  end
1.159 -

     2.1 --- a/src/HOL/Algebra/CRing.thy	Fri Apr 23 20:52:04 2004 +0200
2.2 +++ b/src/HOL/Algebra/CRing.thy	Fri Apr 23 21:46:04 2004 +0200
2.3 @@ -189,13 +189,13 @@
2.4
2.5  syntax
2.6    "_finsum" :: "index => idt => 'a set => 'b => 'b"
2.7 -      ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
2.8 +      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
2.9  syntax (xsymbols)
2.10    "_finsum" :: "index => idt => 'a set => 'b => 'b"
2.11 -      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
2.12 +      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
2.13  syntax (HTML output)
2.14    "_finsum" :: "index => idt => 'a set => 'b => 'b"
2.15 -      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
2.16 +      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
2.17  translations
2.18    "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
2.19

     3.1 --- a/src/HOL/Algebra/Coset.thy	Fri Apr 23 20:52:04 2004 +0200
3.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Apr 23 21:46:04 2004 +0200
3.3 @@ -7,26 +7,26 @@
3.4
3.5  theory Coset = Group + Exponent:
3.6
3.7 -declare (in group) l_inv [simp]  r_inv [simp]
3.8 +declare (in group) l_inv [simp] and r_inv [simp]
3.9
3.10  constdefs (structure G)
3.11 -  r_coset    :: "[_,'a set, 'a] => 'a set"
3.12 -   "r_coset G H a == (% x. x \<otimes> a)  H"
3.13 +  r_coset    :: "[_,'a set, 'a] => 'a set"
3.14 +  "r_coset G H a == (% x. x \<otimes> a)  H"
3.15
3.16    l_coset    :: "[_, 'a, 'a set] => 'a set"
3.17 -   "l_coset G a H == (% x. a \<otimes> x)  H"
3.18 +  "l_coset G a H == (% x. a \<otimes> x)  H"
3.19
3.20    rcosets  :: "[_, 'a set] => ('a set)set"
3.21 -   "rcosets G H == r_coset G H  (carrier G)"
3.22 +  "rcosets G H == r_coset G H  (carrier G)"
3.23
3.24    set_mult  :: "[_, 'a set ,'a set] => 'a set"
3.25 -   "set_mult G H K == (%(x,y). x \<otimes> y)  (H \<times> K)"
3.26 +  "set_mult G H K == (%(x,y). x \<otimes> y)  (H \<times> K)"
3.27
3.28    set_inv   :: "[_,'a set] => 'a set"
3.29 -   "set_inv G H == m_inv G  H"
3.30 +  "set_inv G H == m_inv G  H"
3.31
3.32    normal     :: "['a set, _] => bool"       (infixl "<|" 60)
3.33 -   "normal H G == subgroup H G &
3.34 +  "normal H G == subgroup H G &
3.35                    (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
3.36
3.37  syntax (xsymbols)
3.38 @@ -56,13 +56,13 @@
3.39  apply (auto simp add: Pi_def)
3.40  done
3.41
3.42 -lemma card_bij:
3.43 -     "[|f \<in> A\<rightarrow>B; inj_on f A;
3.44 +lemma card_bij:
3.45 +     "[|f \<in> A\<rightarrow>B; inj_on f A;
3.46          g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
3.47 -by (blast intro: card_inj order_antisym)
3.48 +by (blast intro: card_inj order_antisym)
3.49
3.50
3.51 -subsection{*Lemmas Using Locale Constants*}
3.52 +subsection {*Lemmas Using *}
3.53
3.54  lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
3.55  by (auto simp add: rcos_def r_coset_def)
3.56 @@ -77,7 +77,7 @@
3.57  by (simp add: setmult_def set_mult_def image_def)
3.58
3.59  lemma (in coset) coset_mult_assoc:
3.60 -     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
3.61 +     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
3.62        ==> (M #> g) #> h = M #> (g \<otimes> h)"
3.63  by (force simp add: r_coset_eq m_assoc)
3.64
3.65 @@ -85,14 +85,14 @@
3.66  by (force simp add: r_coset_eq)
3.67
3.68  lemma (in coset) coset_mult_inv1:
3.69 -     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
3.70 +     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
3.71           M <= carrier G |] ==> M #> x = M #> y"
3.72  apply (erule subst [of concl: "%z. M #> x = z #> y"])
3.73  apply (simp add: coset_mult_assoc m_assoc)
3.74  done
3.75
3.76  lemma (in coset) coset_mult_inv2:
3.77 -     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M <= carrier G |]
3.78 +     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M <= carrier G |]
3.79        ==> M #> (x \<otimes> (inv y)) = M "
3.80  apply (simp add: coset_mult_assoc [symmetric])
3.81  apply (simp add: coset_mult_assoc)
3.82 @@ -110,7 +110,7 @@
3.83  lemma (in coset) solve_equation:
3.84      "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
3.85  apply (rule bexI [of _ "y \<otimes> (inv x)"])
3.86 -apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
3.87 +apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
3.88                        subgroup.subset [THEN subsetD])
3.89  done
3.90
3.91 @@ -133,30 +133,30 @@
3.92
3.93  text{*Really needed?*}
3.94  lemma (in coset) transpose_inv:
3.95 -     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
3.96 +     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
3.97        ==> (inv x) \<otimes> z = y"
3.98  by (force simp add: m_assoc [symmetric])
3.99
3.100  lemma (in coset) repr_independence:
3.101       "[| y \<in> H #> x;  x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
3.102 -by (auto simp add: r_coset_eq m_assoc [symmetric]
3.103 +by (auto simp add: r_coset_eq m_assoc [symmetric]
3.104                     subgroup.subset [THEN subsetD]
3.105                     subgroup.m_closed solve_equation)
3.106
3.107  lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
3.108  apply (simp add: r_coset_eq)
3.109 -apply (blast intro: l_one subgroup.subset [THEN subsetD]
3.110 +apply (blast intro: l_one subgroup.subset [THEN subsetD]
3.111                      subgroup.one_closed)
3.112  done
3.113
3.114
3.115 -subsection{*normal subgroups*}
3.116 +subsection {* Normal subgroups *}
3.117
3.118  (*????????????????
3.119  text "Allows use of theorems proved in the locale coset"
3.120  lemma subgroup_imp_coset: "subgroup H G ==> coset G"
3.121  apply (drule subgroup_imp_group)
3.122 -apply (simp add: group_def coset_def)
3.123 +apply (simp add: group_def coset_def)
3.124  done
3.125  *)
3.126
3.127 @@ -180,7 +180,7 @@
3.128  lemma (in coset) normal_inv_op_closed1:
3.129       "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
3.130  apply (auto simp add: l_coset_eq r_coset_eq normal_iff)
3.131 -apply (drule bspec, assumption)
3.132 +apply (drule bspec, assumption)
3.133  apply (drule equalityD1 [THEN subsetD], blast, clarify)
3.134  apply (simp add: m_assoc subgroup.subset [THEN subsetD])
3.135  apply (erule subst)
3.136 @@ -189,12 +189,12 @@
3.137
3.138  lemma (in coset) normal_inv_op_closed2:
3.139       "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
3.140 -apply (drule normal_inv_op_closed1 [of H "(inv x)"])
3.141 +apply (drule normal_inv_op_closed1 [of H "(inv x)"])
3.142  apply auto
3.143  done
3.144
3.145  lemma (in coset) lcos_m_assoc:
3.146 -     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
3.147 +     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
3.148        ==> g <# (h <# M) = (g \<otimes> h) <# M"
3.149  by (force simp add: l_coset_eq m_assoc)
3.150
3.151 @@ -208,8 +208,8 @@
3.152  lemma (in coset) l_coset_swap:
3.153       "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> y <# H"
3.154  proof (simp add: l_coset_eq)
3.155 -  assume "\<exists>h\<in>H. x \<otimes> h = y"
3.156 -    and x: "x \<in> carrier G"
3.157 +  assume "\<exists>h\<in>H. x \<otimes> h = y"
3.158 +    and x: "x \<in> carrier G"
3.159      and sb: "subgroup H G"
3.160    then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
3.161    show "\<exists>h\<in>H. y \<otimes> h = x"
3.162 @@ -223,28 +223,28 @@
3.163
3.164  lemma (in coset) l_coset_carrier:
3.165       "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
3.166 -by (auto simp add: l_coset_eq m_assoc
3.167 +by (auto simp add: l_coset_eq m_assoc
3.168                     subgroup.subset [THEN subsetD] subgroup.m_closed)
3.169
3.170  lemma (in coset) l_repr_imp_subset:
3.171 -  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
3.172 +  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
3.173    shows "y <# H \<subseteq> x <# H"
3.174  proof -
3.175    from y
3.176    obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_eq)
3.177    thus ?thesis using x sb
3.178 -    by (auto simp add: l_coset_eq m_assoc
3.179 +    by (auto simp add: l_coset_eq m_assoc
3.180                         subgroup.subset [THEN subsetD] subgroup.m_closed)
3.181  qed
3.182
3.183  lemma (in coset) l_repr_independence:
3.184 -  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
3.185 +  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
3.186    shows "x <# H = y <# H"
3.187 -proof
3.188 +proof
3.189    show "x <# H \<subseteq> y <# H"
3.190 -    by (rule l_repr_imp_subset,
3.191 +    by (rule l_repr_imp_subset,
3.192          (blast intro: l_coset_swap l_coset_carrier y x sb)+)
3.193 -  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
3.194 +  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
3.195  qed
3.196
3.197  lemma (in coset) setmult_subset_G:
3.198 @@ -255,29 +255,30 @@
3.199  apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
3.200  apply (rule_tac x = x in bexI)
3.201  apply (rule bexI [of _ "\<one>"])
3.202 -apply (auto simp add: subgroup.m_closed subgroup.one_closed
3.203 +apply (auto simp add: subgroup.m_closed subgroup.one_closed
3.204                        r_one subgroup.subset [THEN subsetD])
3.205  done
3.206
3.207
3.208 -(* set of inverses of an r_coset *)
3.209 +text {* Set of inverses of an @{text r_coset}. *}
3.210 +
3.211  lemma (in coset) rcos_inv:
3.212    assumes normalHG: "H <| G"
3.213        and xinG:     "x \<in> carrier G"
3.214    shows "set_inv G (H #> x) = H #> (inv x)"
3.215  proof -
3.216 -  have H_subset: "H <= carrier G"
3.217 +  have H_subset: "H <= carrier G"
3.218      by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
3.219    show ?thesis
3.220    proof (auto simp add: r_coset_eq image_def set_inv_def)
3.221      fix h
3.222      assume "h \<in> H"
3.223        hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
3.224 -	by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
3.225 -      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
3.226 +        by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
3.227 +      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
3.228         using prems
3.229 -	by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
3.230 -			 subgroup.m_inv_closed)
3.231 +        by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
3.232 +                         subgroup.m_inv_closed)
3.233    next
3.234      fix h
3.235      assume "h \<in> H"
3.236 @@ -285,9 +286,9 @@
3.237          by (simp add: xinG m_assoc H_subset [THEN subsetD])
3.238        hence "(\<exists>j\<in>H. j \<otimes> x = inv  (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
3.239         using prems
3.240 -	by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
3.241 -            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
3.242 -			 subgroup.m_inv_closed)
3.243 +        by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
3.244 +            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
3.245 +                         subgroup.m_inv_closed)
3.246        thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
3.247    qed
3.248  qed
3.249 @@ -314,7 +315,7 @@
3.250  apply (simp add: setrcos_eq, clarify)
3.251  apply (subgoal_tac "x : carrier G")
3.252   prefer 2
3.253 - apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
3.254 + apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
3.255  apply (drule repr_independence)
3.256    apply assumption
3.257   apply (erule normal_imp_subgroup)
3.258 @@ -322,56 +323,57 @@
3.259  done
3.260
3.261
3.262 -(* some rules for <#> with #> or <# *)
3.263 +text {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
3.264 +
3.265  lemma (in coset) setmult_rcos_assoc:
3.266 -     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
3.267 +     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
3.268        ==> H <#> (K #> x) = (H <#> K) #> x"
3.269  apply (auto simp add: rcos_def r_coset_def setmult_def set_mult_def)
3.270  apply (force simp add: m_assoc)+
3.271  done
3.272
3.273  lemma (in coset) rcos_assoc_lcos:
3.274 -     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
3.275 +     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
3.276        ==> (H #> x) <#> K = H <#> (x <# K)"
3.277 -apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
3.278 +apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
3.279                        setmult_def set_mult_def Sigma_def image_def)
3.280  apply (force intro!: exI bexI simp add: m_assoc)+
3.281  done
3.282
3.283  lemma (in coset) rcos_mult_step1:
3.284 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.285 +     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.286        ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
3.287  by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
3.288                r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
3.289
3.290  lemma (in coset) rcos_mult_step2:
3.291 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.292 +     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.293        ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
3.294  by (simp add: normal_imp_rcos_eq_lcos)
3.295
3.296  lemma (in coset) rcos_mult_step3:
3.297 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.298 +     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.299        ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
3.300  by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
3.301                setmult_subset_G  subgroup_mult_id
3.302                subgroup.subset normal_imp_subgroup)
3.303
3.304  lemma (in coset) rcos_sum:
3.305 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.306 +     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
3.307        ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
3.308  by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
3.309
3.310 -(*generalizes subgroup_mult_id*)
3.311  lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
3.312 -by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
3.313 -                   setmult_rcos_assoc subgroup_mult_id)
3.314 +  -- {* generalizes @{text subgroup_mult_id} *}
3.315 +  by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
3.316 +    setmult_rcos_assoc subgroup_mult_id)
3.317
3.318
3.319 -subsection{*Lemmas Leading to Lagrange's Theorem*}
3.320 +subsection {*Lemmas Leading to Lagrange's Theorem *}
3.321
3.322 -lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
3.323 +lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
3.324  apply (rule equalityI)
3.325 -apply (force simp add: subgroup.subset [THEN subsetD]
3.326 +apply (force simp add: subgroup.subset [THEN subsetD]
3.327                         setrcos_eq r_coset_eq)
3.328  apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
3.329  done
3.330 @@ -398,13 +400,13 @@
3.331  by (force simp add: inj_on_def subsetD)
3.332
3.333  lemma (in coset) card_cosets_equal:
3.334 -     "[| c \<in> rcosets G H;  H <= carrier G; finite(carrier G) |]
3.335 +     "[| c \<in> rcosets G H;  H <= carrier G; finite(carrier G) |]
3.336        ==> card c = card H"
3.337  apply (auto simp add: setrcos_eq)
3.338  apply (rule card_bij_eq)
3.339 -     apply (rule inj_on_f, assumption+)
3.340 +     apply (rule inj_on_f, assumption+)
3.341      apply (force simp add: m_assoc subsetD r_coset_eq)
3.342 -   apply (rule inj_on_g, assumption+)
3.343 +   apply (rule inj_on_g, assumption+)
3.344    apply (force simp add: m_assoc subsetD r_coset_eq)
3.345   txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
3.346   apply (simp add: r_coset_subset_G [THEN finite_subset])
3.347 @@ -414,8 +416,8 @@
3.348  subsection{*Two distinct right cosets are disjoint*}
3.349
3.350  lemma (in coset) rcos_equation:
3.351 -     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
3.352 -        h \<in> H;  ha \<in> H;  hb \<in> H|]
3.353 +     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
3.354 +        h \<in> H;  ha \<in> H;  hb \<in> H|]
3.355        ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
3.356  apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
3.357  apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
3.358 @@ -439,16 +441,16 @@
3.359  constdefs
3.360    FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
3.361       (infixl "Mod" 60)
3.362 -   "FactGroup G H ==
3.363 -      (| carrier = rcosets G H,
3.364 -	 mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
3.365 -	 one = H (*,
3.366 -	 m_inv = (%X: rcosets G H. set_inv G X) *) |)"
3.367 +  "FactGroup G H ==
3.368 +    (| carrier = rcosets G H,
3.369 +       mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
3.370 +       one = H (*,
3.371 +       m_inv = (%X: rcosets G H. set_inv G X) *) |)"
3.372
3.373  lemma (in coset) setmult_closed:
3.374 -     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
3.375 +     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
3.376        ==> K1 <#> K2 \<in> rcosets G H"
3.377 -by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
3.378 +by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
3.379                     rcos_sum setrcos_eq)
3.380
3.381  lemma (in group) setinv_closed:
3.382 @@ -467,9 +469,9 @@
3.383  *)
3.384
3.385  lemma (in coset) setrcos_assoc:
3.386 -     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
3.387 +     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
3.388        ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
3.389 -by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
3.390 +by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
3.391                     subgroup.subset m_assoc)
3.392
3.393  lemma (in group) subgroup_in_rcosets:
3.394 @@ -486,10 +488,10 @@
3.395  (*
3.396  lemma subgroup_in_rcosets:
3.397    "subgroup H G ==> H \<in> rcosets G H"
3.398 -apply (frule subgroup_imp_coset)
3.399 -apply (frule subgroup_imp_group)
3.400 +apply (frule subgroup_imp_coset)
3.401 +apply (frule subgroup_imp_group)
3.402  apply (simp add: coset.setrcos_eq)
3.403 -apply (blast del: equalityI
3.404 +apply (blast del: equalityI
3.405               intro!: group.subgroup.one_closed group.one_closed
3.406                       coset.coset_join2 [symmetric])
3.407  done
3.408 @@ -497,7 +499,7 @@
3.409
3.410  lemma (in coset) setrcos_inv_mult_group_eq:
3.411       "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
3.412 -by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
3.413 +by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
3.414                     subgroup.subset)
3.415  (*
3.416  lemma (in group) factorgroup_is_magma:
3.417 @@ -511,8 +513,8 @@
3.418  *)
3.419  theorem (in group) factorgroup_is_group:
3.420    "H <| G ==> group (G Mod H)"
3.421 -apply (insert is_coset)
3.422 -apply (simp add: FactGroup_def)
3.423 +apply (insert is_coset)
3.424 +apply (simp add: FactGroup_def)
3.425  apply (rule groupI)
3.426      apply (simp add: coset.setmult_closed)
3.427     apply (simp add: normal_imp_subgroup subgroup_in_rcosets)

     4.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 23 20:52:04 2004 +0200
4.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 23 21:46:04 2004 +0200
4.3 @@ -290,13 +290,13 @@
4.4
4.5  syntax
4.6    "_finprod" :: "index => idt => 'a set => 'b => 'b"
4.7 -      ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
4.8 +      ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
4.9  syntax (xsymbols)
4.10    "_finprod" :: "index => idt => 'a set => 'b => 'b"
4.11 -      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
4.12 +      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
4.13  syntax (HTML output)
4.14    "_finprod" :: "index => idt => 'a set => 'b => 'b"
4.15 -      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
4.16 +      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
4.17  translations
4.18    "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
4.19

     5.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Apr 23 20:52:04 2004 +0200
5.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Apr 23 21:46:04 2004 +0200
5.3 @@ -186,6 +186,7 @@
5.4    shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
5.5    by (unfold greatest_def) blast
5.6
5.7 +
5.8  subsubsection {* Supremum *}
5.9
5.10  lemma (in lattice) joinI:
5.11 @@ -212,7 +213,8 @@
5.12    shows "x \<in> carrier L ==> \<Squnion> {x} = x"
5.13    by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
5.14
5.15 -text {* Condition on A: supremum exists. *}
5.16 +
5.17 +text {* Condition on @{text A}: supremum exists. *}
5.18
5.19  lemma (in lattice) sup_insertI:
5.20    "[| !!s. least L s (Upper L (insert x A)) ==> P s;

     6.1 --- a/src/HOL/Algebra/Sylow.thy	Fri Apr 23 20:52:04 2004 +0200
6.2 +++ b/src/HOL/Algebra/Sylow.thy	Fri Apr 23 21:46:04 2004 +0200
6.3 @@ -4,7 +4,7 @@
6.4
6.5  See Florian Kamm\"uller and L. C. Paulson,
6.6      A Formal Proof of Sylow's theorem:
6.7 -	An Experiment in Abstract Algebra with Isabelle HOL
6.8 +        An Experiment in Abstract Algebra with Isabelle HOL
6.9      J. Automated Reasoning 23 (1999), 235-264
6.10  *)
6.11
6.12 @@ -15,11 +15,11 @@
6.13  subsection {*Order of a Group and Lagrange's Theorem*}
6.14
6.15  constdefs
6.16 -  order     :: "('a,'b) semigroup_scheme => nat"
6.17 +  order :: "('a, 'b) semigroup_scheme => nat"
6.18    "order S == card (carrier S)"
6.19
6.20  theorem (in coset) lagrange:
6.21 -     "[| finite(carrier G); subgroup H G |]
6.22 +     "[| finite(carrier G); subgroup H G |]
6.23        ==> card(rcosets G H) * card(H) = order(G)"
6.24  apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
6.25  apply (subst mult_commute)
6.26 @@ -40,11 +40,11 @@
6.27        and finite_G [iff]:  "finite (carrier G)"
6.28    defines "calM == {s. s <= carrier(G) & card(s) = p^a}"
6.29        and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
6.30 -		  	     (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
6.31 +                             (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
6.32
6.33  lemma (in sylow) RelM_refl: "refl calM RelM"
6.34 -apply (auto simp add: refl_def RelM_def calM_def)
6.35 -apply (blast intro!: coset_mult_one [symmetric])
6.36 +apply (auto simp add: refl_def RelM_def calM_def)
6.37 +apply (blast intro!: coset_mult_one [symmetric])
6.38  done
6.39
6.40  lemma (in sylow) RelM_sym: "sym RelM"
6.41 @@ -58,7 +58,7 @@
6.42  qed
6.43
6.44  lemma (in sylow) RelM_trans: "trans RelM"
6.45 -by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
6.46 +by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
6.47
6.48  lemma (in sylow) RelM_equiv: "equiv calM RelM"
6.49  apply (unfold equiv_def)
6.50 @@ -91,9 +91,9 @@
6.51  lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
6.52  by force
6.53
6.54 -lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
6.55 -apply (subgoal_tac "0 < card M1")
6.56 - apply (blast dest: card_nonempty)
6.57 +lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
6.58 +apply (subgoal_tac "0 < card M1")
6.59 + apply (blast dest: card_nonempty)
6.60  apply (cut_tac prime_p [THEN prime_imp_one_less])
6.61  apply (simp (no_asm_simp) add: card_M1)
6.62  done
6.63 @@ -112,18 +112,18 @@
6.64      show ?thesis
6.65      proof
6.66        show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
6.67 -	by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
6.68 +        by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
6.69        show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
6.70        proof (rule restrictI)
6.71 -	fix z assume zH: "z \<in> H"
6.72 -	show "m1 \<otimes> z \<in> M1"
6.73 -	proof -
6.74 -	  from zH
6.75 -	  have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
6.76 -	    by (auto simp add: H_def)
6.77 -	  show ?thesis
6.78 -	    by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
6.79 -	qed
6.80 +        fix z assume zH: "z \<in> H"
6.81 +        show "m1 \<otimes> z \<in> M1"
6.82 +        proof -
6.83 +          from zH
6.84 +          have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
6.85 +            by (auto simp add: H_def)
6.86 +          show ?thesis
6.87 +            by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
6.88 +        qed
6.89        qed
6.90      qed
6.91    qed
6.92 @@ -135,8 +135,8 @@
6.93  by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
6.94
6.95  lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
6.96 -apply (subgoal_tac "M \<noteq> {}")
6.97 - apply blast
6.98 +apply (subgoal_tac "M \<noteq> {}")
6.99 + apply blast
6.100  apply (cut_tac EmptyNotInEquivSet, blast)
6.101  done
6.102
6.103 @@ -245,7 +245,7 @@
6.104  text{*Injections between @{term M} and @{term "rcosets G H"} show that
6.105   their cardinalities are equal.*}
6.106
6.107 -lemma ElemClassEquiv:
6.108 +lemma ElemClassEquiv:
6.109       "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
6.110  apply (unfold equiv_def quotient_def sym_def trans_def, blast)
6.111  done
6.112 @@ -257,11 +257,11 @@
6.113  apply (blast dest!: bspec)
6.114  done
6.115
6.116 -lemmas (in sylow_central) M_elem_map_carrier =
6.117 -	M_elem_map [THEN someI_ex, THEN conjunct1]
6.118 +lemmas (in sylow_central) M_elem_map_carrier =
6.119 +        M_elem_map [THEN someI_ex, THEN conjunct1]
6.120
6.121  lemmas (in sylow_central) M_elem_map_eq =
6.122 -	M_elem_map [THEN someI_ex, THEN conjunct2]
6.123 +        M_elem_map [THEN someI_ex, THEN conjunct2]
6.124
6.125  lemma (in sylow_central) M_funcset_setrcos_H:
6.126       "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
6.127 @@ -293,14 +293,14 @@
6.128       "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
6.129  by (auto simp add: setrcos_eq)
6.130
6.131 -lemmas (in sylow_central) H_elem_map_carrier =
6.132 -	H_elem_map [THEN someI_ex, THEN conjunct1]
6.133 +lemmas (in sylow_central) H_elem_map_carrier =
6.134 +        H_elem_map [THEN someI_ex, THEN conjunct1]
6.135
6.136  lemmas (in sylow_central) H_elem_map_eq =
6.137 -	H_elem_map [THEN someI_ex, THEN conjunct2]
6.138 +        H_elem_map [THEN someI_ex, THEN conjunct2]
6.139
6.140
6.141 -lemma EquivElemClass:
6.142 +lemma EquivElemClass:
6.143       "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
6.144  apply (unfold equiv_def quotient_def sym_def trans_def, blast)
6.145  done
6.146 @@ -329,7 +329,7 @@
6.147  apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
6.148  apply (rule coset_join2)
6.149  apply (blast intro: m_closed inv_closed H_elem_map_carrier)
6.150 -apply (rule H_is_subgroup)
6.151 +apply (rule H_is_subgroup)
6.152  apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier)
6.153  done
6.154
6.155 @@ -344,9 +344,9 @@
6.156  done
6.157
6.158  lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
6.159 -apply (insert inj_M_GmodH inj_GmodH_M)
6.160 -apply (blast intro: card_bij finite_M H_is_subgroup
6.161 -             setrcos_subset_PowG [THEN finite_subset]
6.162 +apply (insert inj_M_GmodH inj_GmodH_M)
6.163 +apply (blast intro: card_bij finite_M H_is_subgroup
6.164 +             setrcos_subset_PowG [THEN finite_subset]
6.165               finite_Pow_iff [THEN iffD2])
6.166  done
6.167
6.168 @@ -364,7 +364,7 @@
6.169  lemma (in sylow_central) lemma_leq2: "card(H) <= p^a"
6.170  apply (subst card_M1 [symmetric])
6.171  apply (cut_tac M1_inj_H)
6.172 -apply (blast intro!: M1_subset_G intro:
6.173 +apply (blast intro!: M1_subset_G intro:
6.174               card_inj H_into_carrier_G finite_subset [OF _ finite_G])
6.175  done
6.176
6.177 @@ -372,15 +372,15 @@
6.178  by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
6.179
6.180  lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
6.181 -apply (cut_tac lemma_A1, clarify)
6.182 -apply (frule existsM1inM, clarify)
6.183 +apply (cut_tac lemma_A1, clarify)
6.184 +apply (frule existsM1inM, clarify)
6.185  apply (subgoal_tac "sylow_central G p a m M1 M")
6.186   apply (blast dest:  sylow_central.H_is_subgroup sylow_central.card_H_eq)
6.187 -apply (simp add: sylow_central_def sylow_central_axioms_def prems)
6.188 +apply (simp add: sylow_central_def sylow_central_axioms_def prems)
6.189  done
6.190
6.191  text{*Needed because the locale's automatic definition refers to
6.192 -   @{term "semigroup G"} and @{term "group_axioms G"} rather than
6.193 +   @{term "semigroup G"} and @{term "group_axioms G"} rather than
6.194    simply to @{term "group G"}.*}
6.195  lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
6.196  by (simp add: sylow_def group_def)
6.197 @@ -389,7 +389,7 @@
6.198       "[|p \<in> prime;  group(G);  order(G) = (p^a) * m; finite (carrier G)|]
6.199        ==> \<exists>H. subgroup H G & card(H) = p^a"
6.200  apply (rule sylow.sylow_thm [of G p a m])
6.201 -apply (simp add: sylow_eq sylow_axioms_def)
6.202 +apply (simp add: sylow_eq sylow_axioms_def)
6.203  done
6.204
6.205  end

     7.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 23 20:52:04 2004 +0200
7.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 23 21:46:04 2004 +0200
7.3 @@ -10,43 +10,32 @@
7.4  theory UnivPoly = Module:
7.5
7.6  text {*
7.7 -  Polynomials are formalised as modules with additional operations for
7.8 -  extracting coefficients from polynomials and for obtaining monomials
7.9 -  from coefficients and exponents (record @{text "up_ring"}).
7.10 -  The carrier set is
7.11 -  a set of bounded functions from Nat to the coefficient domain.
7.12 -  Bounded means that these functions return zero above a certain bound
7.13 -  (the degree).  There is a chapter on the formalisation of polynomials
7.14 -  in my PhD thesis (http://www4.in.tum.de/\~{}ballarin/publications/),
7.15 -  which was implemented with axiomatic type classes.  This was later
7.16 -  ported to Locales.
7.17 +  Polynomials are formalised as modules with additional operations for
7.18 +  extracting coefficients from polynomials and for obtaining monomials
7.19 +  from coefficients and exponents (record @{text "up_ring"}).  The
7.20 +  carrier set is a set of bounded functions from Nat to the
7.21 +  coefficient domain.  Bounded means that these functions return zero
7.22 +  above a certain bound (the degree).  There is a chapter on the
7.23 +  formalisation of polynomials in my PhD thesis
7.24 +  (\url{http://www4.in.tum.de/~ballarin/publications/}), which was
7.25 +  implemented with axiomatic type classes.  This was later ported to
7.26 +  Locales.
7.27  *}
7.28
7.29 +
7.30  subsection {* The Constructor for Univariate Polynomials *}
7.31
7.32 -(* Could alternatively use locale ...
7.33 -locale bound = cring + var bound +
7.34 -  defines ...
7.35 -*)
7.36 -
7.37 -constdefs
7.38 -  bound  :: "['a, nat, nat => 'a] => bool"
7.39 -  "bound z n f == (ALL i. n < i --> f i = z)"
7.40 +locale bound =
7.41 +  fixes z :: 'a
7.42 +    and n :: nat
7.43 +    and f :: "nat => 'a"
7.44 +  assumes bound: "!!m. n < m \<Longrightarrow> f m = z"
7.45
7.46 -lemma boundI [intro!]:
7.47 -  "[| !! m. n < m ==> f m = z |] ==> bound z n f"
7.48 -  by (unfold bound_def) fast
7.49 -
7.50 -lemma boundE [elim?]:
7.51 -  "[| bound z n f; (!! m. n < m ==> f m = z) ==> P |] ==> P"
7.52 -  by (unfold bound_def) fast
7.53 -
7.54 -lemma boundD [dest]:
7.55 -  "[| bound z n f; n < m |] ==> f m = z"
7.56 -  by (unfold bound_def) fast
7.57 +declare bound.intro [intro!]
7.58 +  and bound.bound [dest]
7.59
7.60  lemma bound_below:
7.61 -  assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m"
7.62 +  assumes bound: "bound z m f" and nonzero: "f n \<noteq> z" shows "n \<le> m"
7.63  proof (rule classical)
7.64    assume "~ ?thesis"
7.65    then have "m < n" by arith
7.66 @@ -130,45 +119,45 @@
7.67
7.68  lemma (in cring) up_mult_closed:
7.69    "[| p \<in> up R; q \<in> up R |] ==>
7.70 -  (%n. finsum R (%i. p i \<otimes> q (n-i)) {..n}) \<in> up R"
7.71 +  (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
7.72  proof
7.73    fix n
7.74    assume "p \<in> up R" "q \<in> up R"
7.75 -  then show "finsum R (%i. p i \<otimes> q (n-i)) {..n} \<in> carrier R"
7.76 +  then show "(\<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> carrier R"
7.77      by (simp add: mem_upD  funcsetI)
7.78  next
7.79    assume UP: "p \<in> up R" "q \<in> up R"
7.80 -  show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
7.81 +  show "EX n. bound \<zero> n (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
7.82    proof -
7.83      from UP obtain n where boundn: "bound \<zero> n p" by fast
7.84      from UP obtain m where boundm: "bound \<zero> m q" by fast
7.85 -    have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
7.86 +    have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
7.87      proof
7.88 -      fix k
7.89 -      assume bound: "n + m < k"
7.90 +      fix k assume bound: "n + m < k"
7.91        {
7.92 -	fix i
7.93 -	have "p i \<otimes> q (k-i) = \<zero>"
7.94 -	proof (cases "n < i")
7.95 -	  case True
7.96 -	  with boundn have "p i = \<zero>" by auto
7.97 +        fix i
7.98 +        have "p i \<otimes> q (k-i) = \<zero>"
7.99 +        proof (cases "n < i")
7.100 +          case True
7.101 +          with boundn have "p i = \<zero>" by auto
7.102            moreover from UP have "q (k-i) \<in> carrier R" by auto
7.103 -	  ultimately show ?thesis by simp
7.104 -	next
7.105 -	  case False
7.106 -	  with bound have "m < k-i" by arith
7.107 -	  with boundm have "q (k-i) = \<zero>" by auto
7.108 -	  moreover from UP have "p i \<in> carrier R" by auto
7.109 -	  ultimately show ?thesis by simp
7.110 -	qed
7.111 +          ultimately show ?thesis by simp
7.112 +        next
7.113 +          case False
7.114 +          with bound have "m < k-i" by arith
7.115 +          with boundm have "q (k-i) = \<zero>" by auto
7.116 +          moreover from UP have "p i \<in> carrier R" by auto
7.117 +          ultimately show ?thesis by simp
7.118 +        qed
7.119        }
7.120 -      then show "finsum R (%i. p i \<otimes> q (k-i)) {..k} = \<zero>"
7.121 -	by (simp add: Pi_def)
7.122 +      then show "(\<Oplus>i \<in> {..k}. p i \<otimes> q (k-i)) = \<zero>"
7.123 +        by (simp add: Pi_def)
7.124      qed
7.125      then show ?thesis by fast
7.126    qed
7.127  qed
7.128
7.129 +
7.130  subsection {* Effect of operations on coefficients *}
7.131
7.132  locale UP = struct R + struct P +
7.133 @@ -214,7 +203,7 @@
7.134
7.135  lemma (in UP_cring) coeff_mult [simp]:
7.136    "[| p \<in> carrier P; q \<in> carrier P |] ==>
7.137 -  coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (n-i)) {..n}"
7.138 +  coeff P (p \<otimes>\<^sub>2 q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
7.139    by (simp add: UP_def up_mult_closed)
7.140
7.141  lemma (in UP) up_eqI:
7.142 @@ -225,10 +214,10 @@
7.143    fix x
7.144    from prem and R show "p x = q x" by (simp add: UP_def)
7.145  qed
7.146 -
7.147 +
7.148  subsection {* Polynomials form a commutative ring. *}
7.149
7.150 -text {* Operations are closed over @{term "P"}. *}
7.151 +text {* Operations are closed over @{term P}. *}
7.152
7.153  lemma (in UP_cring) UP_mult_closed [simp]:
7.154    "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^sub>2 q \<in> carrier P"
7.155 @@ -307,9 +296,9 @@
7.156      assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
7.157        "c \<in> UNIV -> carrier R"
7.158      then have "k <= n ==>
7.159 -      finsum R (%j. finsum R (%i. a i \<otimes> b (j-i)) {..j} \<otimes> c (n-j)) {..k} =
7.160 -      finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (n-j-i)) {..k-j}) {..k}"
7.161 -      (is "_ ==> ?eq k")
7.162 +      (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
7.163 +      (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
7.164 +      (concl is "?eq k")
7.165      proof (induct k)
7.166        case 0 then show ?case by (simp add: Pi_def m_assoc)
7.167      next
7.168 @@ -317,7 +306,7 @@
7.169        then have "k <= n" by arith
7.170        then have "?eq k" by (rule Suc)
7.171        with R show ?case
7.172 -	by (simp cong: finsum_cong
7.173 +        by (simp cong: finsum_cong
7.174               add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
7.175            (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
7.176      qed
7.177 @@ -353,19 +342,19 @@
7.178    assumes R: "p \<in> carrier P" "q \<in> carrier P"
7.179    shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p"
7.180  proof (rule up_eqI)
7.181 -  fix n
7.182 +  fix n
7.183    {
7.184      fix k and a b :: "nat=>'a"
7.185      assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
7.186 -    then have "k <= n ==>
7.187 -      finsum R (%i. a i \<otimes> b (n-i)) {..k} =
7.188 -      finsum R (%i. a (k-i) \<otimes> b (i+n-k)) {..k}"
7.189 -      (is "_ ==> ?eq k")
7.190 +    then have "k <= n ==>
7.191 +      (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
7.192 +      (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
7.193 +      (concl is "?eq k")
7.194      proof (induct k)
7.195        case 0 then show ?case by (simp add: Pi_def)
7.196      next
7.197        case (Suc k) then show ?case
7.198 -	by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
7.199 +        by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
7.200      qed
7.201    }
7.202    note l = this
7.203 @@ -557,6 +546,7 @@
7.204  lemmas (in UP_cring) UP_finsum_rdistr =
7.205    cring.finsum_rdistr [OF UP_cring]
7.206
7.207 +
7.208  subsection {* Polynomials form an Algebra *}
7.209
7.210  lemma (in UP_cring) UP_smult_l_distr:
7.211 @@ -658,64 +648,64 @@
7.212    proof (cases "k = Suc n")
7.213      case True show ?thesis
7.214      proof -
7.215 -      from True have less_add_diff:
7.216 -	"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
7.217 +      from True have less_add_diff:
7.218 +        "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
7.219        from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
7.220        also from True
7.221 -      have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
7.222 -	coeff P (monom P \<one> 1) (k - i)) ({..n(} Un {n})"
7.223 -	by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
7.224 -      also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
7.225 -	coeff P (monom P \<one> 1) (k - i)) {..n}"
7.226 -	by (simp only: ivl_disj_un_singleton)
7.227 -      also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
7.228 -	coeff P (monom P \<one> 1) (k - i)) ({..n} Un {)n..k})"
7.229 -	by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
7.230 -	  order_less_imp_not_eq Pi_def)
7.231 +      have "... = (\<Oplus>i \<in> {..n(} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
7.232 +        coeff P (monom P \<one> 1) (k - i))"
7.233 +        by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
7.234 +      also have "... = (\<Oplus>i \<in>  {..n}. coeff P (monom P \<one> n) i \<otimes>
7.235 +        coeff P (monom P \<one> 1) (k - i))"
7.236 +        by (simp only: ivl_disj_un_singleton)
7.237 +      also from True have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. coeff P (monom P \<one> n) i \<otimes>
7.238 +        coeff P (monom P \<one> 1) (k - i))"
7.239 +        by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
7.240 +          order_less_imp_not_eq Pi_def)
7.241        also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
7.242 -	by (simp add: ivl_disj_un_one)
7.243 +        by (simp add: ivl_disj_un_one)
7.244        finally show ?thesis .
7.245      qed
7.246    next
7.247      case False
7.248      note neq = False
7.249      let ?s =
7.250 -      "(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>))"
7.251 +      "\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>)"
7.252      from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
7.253 -    also have "... = finsum R ?s {..k}"
7.254 +    also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
7.255      proof -
7.256 -      have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def)
7.257 -      from neq have f2: "finsum R ?s {n} = \<zero>"
7.258 -	by (simp cong: finsum_cong add: Pi_def) arith
7.259 -      have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>"
7.260 -	by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
7.261 +      have f1: "(\<Oplus>i \<in> {..n(}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
7.262 +      from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
7.263 +        by (simp cong: finsum_cong add: Pi_def) arith
7.264 +      have f3: "n < k ==> (\<Oplus>i \<in> {)n..k}. ?s i) = \<zero>"
7.265 +        by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
7.266        show ?thesis
7.267        proof (cases "k < n")
7.268 -	case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
7.269 +        case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
7.270        next
7.271 -	case False then have n_le_k: "n <= k" by arith
7.272 -	show ?thesis
7.273 -	proof (cases "n = k")
7.274 -	  case True
7.275 -	  then have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
7.276 -	    by (simp cong: finsum_cong add: finsum_Un_disjoint
7.277 -	      ivl_disj_int_singleton Pi_def)
7.278 -	  also from True have "... = finsum R ?s {..k}"
7.279 -	    by (simp only: ivl_disj_un_singleton)
7.280 -	  finally show ?thesis .
7.281 -	next
7.282 -	  case False with n_le_k have n_less_k: "n < k" by arith
7.283 -	  with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
7.284 -	    by (simp add: finsum_Un_disjoint f1 f2
7.285 -	      ivl_disj_int_singleton Pi_def del: Un_insert_right)
7.286 -	  also have "... = finsum R ?s {..n}"
7.287 -	    by (simp only: ivl_disj_un_singleton)
7.288 -	  also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})"
7.289 -	    by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
7.290 -	  also from n_less_k have "... = finsum R ?s {..k}"
7.291 -	    by (simp only: ivl_disj_un_one)
7.292 -	  finally show ?thesis .
7.293 -	qed
7.294 +        case False then have n_le_k: "n <= k" by arith
7.295 +        show ?thesis
7.296 +        proof (cases "n = k")
7.297 +          case True
7.298 +          then have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
7.299 +            by (simp cong: finsum_cong add: finsum_Un_disjoint
7.300 +              ivl_disj_int_singleton Pi_def)
7.301 +          also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
7.302 +            by (simp only: ivl_disj_un_singleton)
7.303 +          finally show ?thesis .
7.304 +        next
7.305 +          case False with n_le_k have n_less_k: "n < k" by arith
7.306 +          with neq have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
7.307 +            by (simp add: finsum_Un_disjoint f1 f2
7.308 +              ivl_disj_int_singleton Pi_def del: Un_insert_right)
7.309 +          also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
7.310 +            by (simp only: ivl_disj_un_singleton)
7.311 +          also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. ?s i)"
7.312 +            by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
7.313 +          also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
7.314 +            by (simp only: ivl_disj_un_one)
7.315 +          finally show ?thesis .
7.316 +        qed
7.317        qed
7.318      qed
7.319      also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp
7.320 @@ -789,7 +779,7 @@
7.321    "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
7.322
7.323  lemma (in UP_cring) deg_aboveI:
7.324 -  "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
7.325 +  "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
7.326    by (unfold deg_def P_def) (fast intro: Least_le)
7.327  (*
7.328  lemma coeff_bound_ex: "EX n. bound n (coeff p)"
7.329 @@ -798,7 +788,7 @@
7.330    then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
7.331    then show ?thesis ..
7.332  qed
7.333 -
7.334 +
7.335  lemma bound_coeff_obtain:
7.336    assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
7.337  proof -
7.338 @@ -811,18 +801,18 @@
7.339    "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
7.340  proof -
7.341    assume R: "p \<in> carrier P" and "deg R p < m"
7.342 -  from R obtain n where "bound \<zero> n (coeff P p)"
7.343 +  from R obtain n where "bound \<zero> n (coeff P p)"
7.344      by (auto simp add: UP_def P_def)
7.345    then have "bound \<zero> (deg R p) (coeff P p)"
7.346      by (auto simp: deg_def P_def dest: LeastI)
7.347 -  then show ?thesis by (rule boundD)
7.348 +  then show ?thesis ..
7.349  qed
7.350
7.351  lemma (in UP_cring) deg_belowI:
7.352    assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
7.353      and R: "p \<in> carrier P"
7.354    shows "n <= deg R p"
7.355 --- {* Logically, this is a slightly stronger version of
7.356 +-- {* Logically, this is a slightly stronger version of
7.357    @{thm [source] deg_aboveD} *}
7.358  proof (cases "n=0")
7.359    case True then show ?thesis by simp
7.360 @@ -847,7 +837,7 @@
7.361      then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
7.362        by (unfold bound_def) fast
7.363      then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
7.364 -    then show ?thesis by auto
7.365 +    then show ?thesis by auto
7.366    qed
7.367    with deg_belowI R have "deg R p = m" by fastsimp
7.368    with m_coeff show ?thesis by simp
7.369 @@ -890,7 +880,7 @@
7.370    shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)"
7.371  proof (cases "deg R p <= deg R q")
7.372    case True show ?thesis
7.373 -    by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
7.374 +    by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
7.375  next
7.376    case False show ?thesis
7.377      by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
7.378 @@ -933,7 +923,7 @@
7.379  proof (rule le_anti_sym)
7.380    show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
7.381  next
7.382 -  show "deg R p <= deg R (\<ominus>\<^sub>2 p)"
7.383 +  show "deg R p <= deg R (\<ominus>\<^sub>2 p)"
7.384      by (simp add: deg_belowI lcoeff_nonzero_deg
7.385        inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
7.386  qed
7.387 @@ -999,10 +989,10 @@
7.388          deg_aboveD less_add_diff R Pi_def)
7.389      also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
7.390        by (simp only: ivl_disj_un_singleton)
7.391 -    also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
7.392 +    also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
7.393        by (simp cong: finsum_cong add: finsum_Un_disjoint
7.394 -	ivl_disj_int_singleton deg_aboveD R Pi_def)
7.395 -    finally have "finsum R ?s {.. deg R p + deg R q}
7.396 +        ivl_disj_int_singleton deg_aboveD R Pi_def)
7.397 +    finally have "finsum R ?s {.. deg R p + deg R q}
7.398        = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
7.399      with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>"
7.400        by (simp add: integral_iff lcoeff_nonzero R)
7.401 @@ -1021,7 +1011,7 @@
7.402
7.403  lemma (in UP_cring) up_repr:
7.404    assumes R: "p \<in> carrier P"
7.405 -  shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p"
7.406 +  shows "(\<Oplus>\<^sub>2 i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
7.407  proof (rule up_eqI)
7.408    let ?s = "(%i. monom P (coeff P p i) i)"
7.409    fix k
7.410 @@ -1030,23 +1020,23 @@
7.411    show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k"
7.412    proof (cases "k <= deg R p")
7.413      case True
7.414 -    hence "coeff P (finsum P ?s {..deg R p}) k =
7.415 +    hence "coeff P (finsum P ?s {..deg R p}) k =
7.416            coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
7.417        by (simp only: ivl_disj_un_one)
7.418      also from True
7.419      have "... = coeff P (finsum P ?s {..k}) k"
7.420        by (simp cong: finsum_cong add: finsum_Un_disjoint
7.421 -	ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
7.422 +        ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
7.423      also
7.424      have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
7.425        by (simp only: ivl_disj_un_singleton)
7.426      also have "... = coeff P p k"
7.427        by (simp cong: finsum_cong add: setsum_Un_disjoint
7.428 -	ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
7.429 +        ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
7.430      finally show ?thesis .
7.431    next
7.432      case False
7.433 -    hence "coeff P (finsum P ?s {..deg R p}) k =
7.434 +    hence "coeff P (finsum P ?s {..deg R p}) k =
7.435            coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
7.436        by (simp only: ivl_disj_un_singleton)
7.437      also from False have "... = coeff P p k"
7.438 @@ -1107,11 +1097,11 @@
7.439      also from pq have "... = 0" by simp
7.440      finally have "deg R p + deg R q = 0" .
7.441      then have f1: "deg R p = 0 & deg R q = 0" by simp
7.442 -    from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}"
7.443 +    from f1 R have "p = (\<Oplus>\<^sub>2 i \<in> {..0}. monom P (coeff P p i) i)"
7.444        by (simp only: up_repr_le)
7.445      also from R have "... = monom P (coeff P p 0) 0" by simp
7.446      finally have p: "p = monom P (coeff P p 0) 0" .
7.447 -    from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}"
7.448 +    from f1 R have "q = (\<Oplus>\<^sub>2 i \<in> {..0}. monom P (coeff P q i) i)"
7.449        by (simp only: up_repr_le)
7.450      also from R have "... = monom P (coeff P q 0) 0" by simp
7.451      finally have q: "q = monom P (coeff P q 0) 0" .
7.452 @@ -1149,49 +1139,49 @@
7.453    by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
7.454      inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
7.455
7.456 +
7.457  subsection {* Evaluation Homomorphism and Universal Property*}
7.458
7.459 +(* alternative congruence rule (possibly more efficient)
7.460 +lemma (in abelian_monoid) finsum_cong2:
7.461 +  "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
7.462 +  !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
7.463 +  sorry*)
7.464 +
7.465  ML_setup {*
7.466    simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
7.467  *}
7.468
7.469 -(* alternative congruence rule (possibly more efficient)
7.470 -lemma (in abelian_monoid) finsum_cong2:
7.471 -  "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
7.472 -  !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
7.473 -  sorry
7.474 -*)
7.475 -
7.476  theorem (in cring) diagonal_sum:
7.477    "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
7.478 -  finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..n + m} =
7.479 -  finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
7.480 +  (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
7.481 +  (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
7.482  proof -
7.483    assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
7.484    {
7.485      fix j
7.486      have "j <= n + m ==>
7.487 -      finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..j} =
7.488 -      finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j - k}) {..j}"
7.489 +      (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
7.490 +      (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..j - k}. f k \<otimes> g i)"
7.491      proof (induct j)
7.492        case 0 from Rf Rg show ?case by (simp add: Pi_def)
7.493      next
7.494 -      case (Suc j)
7.495 +      case (Suc j)
7.496        (* The following could be simplified if there was a reasoner for
7.497 -	total orders integrated with simip. *)
7.498 +        total orders integrated with simip. *)
7.499        have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
7.500 -	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
7.501 +        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
7.502        have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
7.503 -	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
7.504 +        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
7.505        have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
7.506 -	using Suc by (auto intro!: funcset_mem [OF Rf])
7.507 +        using Suc by (auto intro!: funcset_mem [OF Rf])
7.508        have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
7.509 -	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
7.510 +        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
7.511        have R11: "g 0 \<in> carrier R"
7.512 -	using Suc by (auto intro!: funcset_mem [OF Rg])
7.513 +        using Suc by (auto intro!: funcset_mem [OF Rg])
7.514        from Suc show ?case
7.515 -	by (simp cong: finsum_cong add: Suc_diff_le a_ac
7.516 -	  Pi_def R6 R8 R9 R10 R11)
7.517 +        by (simp cong: finsum_cong add: Suc_diff_le a_ac
7.518 +          Pi_def R6 R8 R9 R10 R11)
7.519      qed
7.520    }
7.521    then show ?thesis by fast
7.522 @@ -1204,9 +1194,8 @@
7.523  theorem (in cring) cauchy_product:
7.524    assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
7.525      and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
7.526 -  shows "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
7.527 -    finsum R f {..n} \<otimes> finsum R g {..m}"
7.528 -(* State revese direction? *)
7.529 +  shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
7.530 +    (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"        (* State revese direction? *)
7.531  proof -
7.532    have f: "!!x. f x \<in> carrier R"
7.533    proof -
7.534 @@ -1220,24 +1209,20 @@
7.535      show "g x \<in> carrier R"
7.536        using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
7.537    qed
7.538 -  from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
7.539 -    finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
7.540 +  from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
7.541 +      (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
7.542      by (simp add: diagonal_sum Pi_def)
7.543 -  also have "... = finsum R
7.544 -      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) ({..n} Un {)n..n + m})"
7.545 +  also have "... = (\<Oplus>k \<in> {..n} \<union> {)n..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
7.546      by (simp only: ivl_disj_un_one)
7.547 -  also from f g have "... = finsum R
7.548 -      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n}"
7.549 +  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
7.550      by (simp cong: finsum_cong
7.551 -      add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.552 -  also from f g have "... = finsum R
7.553 -      (%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m - k})) {..n}"
7.554 +      add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.555 +  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {)m..n + m - k}. f k \<otimes> g i)"
7.556      by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
7.557 -  also from f g have "... = finsum R
7.558 -      (%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}"
7.559 +  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
7.560      by (simp cong: finsum_cong
7.561 -      add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.562 -  also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}"
7.563 +      add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.564 +  also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"
7.565      by (simp add: finsum_ldistr diagonal_sum Pi_def,
7.566        simp cong: finsum_cong add: finsum_rdistr Pi_def)
7.567    finally show ?thesis .
7.568 @@ -1256,13 +1241,13 @@
7.569    then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
7.570    else arbitrary"
7.571  *)
7.572 -
7.573 +
7.574  locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
7.575
7.576  lemma (in ring_hom_UP_cring) eval_on_carrier:
7.577    "p \<in> carrier P ==>
7.578      eval R S phi s p =
7.579 -    finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}"
7.580 +    (\<Oplus>\<^sub>2 i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^sub>2 pow S s i)"
7.581    by (unfold eval_def, fold P_def) simp
7.582
7.583  lemma (in ring_hom_UP_cring) eval_extensional:
7.584 @@ -1282,31 +1267,29 @@
7.585    then show "eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q"
7.586    proof (simp only: eval_on_carrier UP_mult_closed)
7.587      from RS have
7.588 -      "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
7.589 -      finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.590 -        ({..deg R (p \<otimes>\<^sub>3 q)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})"
7.591 +      "(\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
7.592 +      (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q}.
7.593 +        h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.594        by (simp cong: finsum_cong
7.595 -	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
7.596 -	del: coeff_mult)
7.597 +        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
7.598 +        del: coeff_mult)
7.599      also from RS have "... =
7.600 -      finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p + deg R q}"
7.601 +      (\<Oplus>\<^sub>2 i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.602        by (simp only: ivl_disj_un_one deg_mult_cring)
7.603      also from RS have "... =
7.604 -      finsum S (%i.
7.605 -        finsum S (%k.
7.606 -        (h (coeff P p k) \<otimes>\<^sub>2 h (coeff P q (i-k))) \<otimes>\<^sub>2 (s (^)\<^sub>2 k \<otimes>\<^sub>2 s (^)\<^sub>2 (i-k)))
7.607 -      {..i}) {..deg R p + deg R q}"
7.608 +      (\<Oplus>\<^sub>2 i \<in> {..deg R p + deg R q}.
7.609 +       \<Oplus>\<^sub>2 k \<in> {..i}. h (coeff P p k) \<otimes>\<^sub>2 h (coeff P q (i - k)) \<otimes>\<^sub>2 (s (^)\<^sub>2 k \<otimes>\<^sub>2 s (^)\<^sub>2 (i - k)))"
7.610        by (simp cong: finsum_cong add: nat_pow_mult Pi_def
7.611 -	S.m_ac S.finsum_rdistr)
7.612 +        S.m_ac S.finsum_rdistr)
7.613      also from RS have "... =
7.614 -      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
7.615 -      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
7.616 -      by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac
7.617 -	Pi_def)
7.618 +      (\<Oplus>\<^sub>2i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<otimes>\<^sub>2
7.619 +      (\<Oplus>\<^sub>2i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.620 +      by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
7.621 +        Pi_def)
7.622      finally show
7.623 -      "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
7.624 -      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
7.625 -      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" .
7.626 +      "(\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
7.627 +      (\<Oplus>\<^sub>2 i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<otimes>\<^sub>2
7.628 +      (\<Oplus>\<^sub>2 i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)" .
7.629    qed
7.630  next
7.631    fix p q
7.632 @@ -1314,36 +1297,35 @@
7.633    then show "eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q"
7.634    proof (simp only: eval_on_carrier UP_a_closed)
7.635      from RS have
7.636 -      "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
7.637 -      finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.638 -        ({..deg R (p \<oplus>\<^sub>3 q)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})"
7.639 +      "(\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
7.640 +      (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)}.
7.641 +        h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.642        by (simp cong: finsum_cong
7.643 -	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
7.644 -	del: coeff_add)
7.645 +        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
7.646 +        del: coeff_add)
7.647      also from RS have "... =
7.648 -      finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.649 -        {..max (deg R p) (deg R q)}"
7.650 +        (\<Oplus>\<^sub>2 i \<in> {..max (deg R p) (deg R q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.651        by (simp add: ivl_disj_un_one)
7.652      also from RS have "... =
7.653 -      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)} \<oplus>\<^sub>2
7.654 -      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}"
7.655 +      (\<Oplus>\<^sub>2i\<in>{..max (deg R p) (deg R q)}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
7.656 +      (\<Oplus>\<^sub>2i\<in>{..max (deg R p) (deg R q)}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.657        by (simp cong: finsum_cong
7.658 -	add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.659 +        add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.660      also have "... =
7.661 -      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.662 -        ({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2
7.663 -      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.664 -        ({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})"
7.665 +        (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {)deg R p..max (deg R p) (deg R q)}.
7.666 +          h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
7.667 +        (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {)deg R q..max (deg R p) (deg R q)}.
7.668 +          h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.669        by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
7.670      also from RS have "... =
7.671 -      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
7.672 -      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
7.673 +      (\<Oplus>\<^sub>2 i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
7.674 +      (\<Oplus>\<^sub>2 i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.675        by (simp cong: finsum_cong
7.676 -	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.677 +        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.678      finally show
7.679 -      "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
7.680 -      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
7.681 -      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
7.682 +      "(\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
7.683 +      (\<Oplus>\<^sub>2i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
7.684 +      (\<Oplus>\<^sub>2i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.685        .
7.686    qed
7.687  next
7.688 @@ -1414,14 +1396,14 @@
7.689    "s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
7.690  proof (simp only: eval_on_carrier monom_closed R.one_closed)
7.691    assume S: "s \<in> carrier S"
7.692 -  then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.693 -      {..deg R (monom P \<one> 1)} =
7.694 -    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.695 -      ({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})"
7.696 +  then have
7.697 +    "(\<Oplus>\<^sub>2 i \<in> {..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
7.698 +    (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {)deg R (monom P \<one> 1)..1}.
7.699 +      h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.700      by (simp cong: finsum_cong del: coeff_monom
7.701        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
7.702 -  also have "... =
7.703 -    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}"
7.704 +  also have "... =
7.705 +    (\<Oplus>\<^sub>2 i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
7.706      by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
7.707    also have "... = s"
7.708    proof (cases "s = \<zero>\<^sub>2")
7.709 @@ -1429,8 +1411,8 @@
7.710    next
7.711      case False with S show ?thesis by (simp add: Pi_def)
7.712    qed
7.713 -  finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
7.714 -      {..deg R (monom P \<one> 1)} = s" .
7.715 +  finally show "(\<Oplus>\<^sub>2 i \<in> {..deg R (monom P \<one> 1)}.
7.716 +    h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) = s" .
7.717  qed
7.718
7.719  lemma (in UP_cring) monom_pow:
7.720 @@ -1491,15 +1473,13 @@
7.721      by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
7.722    have Psi_hom: "ring_hom_cring P S Psi"
7.723      by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
7.724 -  have "Phi p = Phi (finsum P
7.725 -    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
7.726 +  have "Phi p = Phi (\<Oplus>\<^sub>3i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^sub>3 monom P \<one> 1 (^)\<^sub>3 i)"
7.727      by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
7.728 -  also have "... = Psi (finsum P
7.729 -    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
7.730 -    by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
7.731 +  also have "... = Psi (\<Oplus>\<^sub>3i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^sub>3 monom P \<one> 1 (^)\<^sub>3 i)"
7.732 +    by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
7.733        ring_hom_cring.hom_mult [OF Phi_hom]
7.734        ring_hom_cring.hom_pow [OF Phi_hom] Phi
7.735 -      ring_hom_cring.hom_finsum [OF Psi_hom]
7.736 +      ring_hom_cring.hom_finsum [OF Psi_hom]
7.737        ring_hom_cring.hom_mult [OF Psi_hom]
7.738        ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
7.739    also have "... = Psi p"
7.740 @@ -1511,13 +1491,13 @@
7.741  theorem (in ring_hom_UP_cring) UP_universal_property:
7.742    "s \<in> carrier S ==>
7.743    EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
7.744 -    Phi (monom P \<one> 1) = s &
7.745 +    Phi (monom P \<one> 1) = s &
7.746      (ALL r : carrier R. Phi (monom P r 0) = h r)"
7.747 -  using eval_monom1
7.748 +  using eval_monom1
7.749    apply (auto intro: eval_ring_hom eval_const eval_extensional)
7.750 -  apply (rule extensionalityI)
7.751 -  apply (auto intro: UP_hom_unique)
7.752 -  done
7.753 +  apply (rule extensionalityI)
7.754 +  apply (auto intro: UP_hom_unique)
7.755 +  done
7.756
7.757  subsection {* Sample application of evaluation homomorphism *}
7.758
7.759 @@ -1545,7 +1525,8 @@
7.760  text {*
7.761    An instantiation mechanism would now import all theorems and lemmas
7.762    valid in the context of homomorphisms between @{term INTEG} and @{term
7.763 -  "UP INTEG"}.  *}
7.764 +  "UP INTEG"}.
7.765 +*}
7.766
7.767  lemma INTEG_closed [intro, simp]:
7.768    "z \<in> carrier INTEG"
7.769 @@ -1562,6 +1543,4 @@
7.770  lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
7.771    by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id])
7.772
7.773 --- {* Calculates @{term "x = 500"} *}
7.774 -
7.775  end

     8.1 --- a/src/HOL/Algebra/document/root.tex	Fri Apr 23 20:52:04 2004 +0200
8.2 +++ b/src/HOL/Algebra/document/root.tex	Fri Apr 23 21:46:04 2004 +0200
8.3 @@ -2,6 +2,17 @@
8.4  \documentclass[11pt,a4paper]{article}
8.5  \usepackage{graphicx}
8.6  \usepackage{isabelle,isabellesym}
8.7 +\usepackage{amssymb}
8.8 +\usepackage[latin1]{inputenc}
8.9 +\usepackage[only,bigsqcap]{stmaryrd}
8.10 +%\usepackage{masmath}
8.11 +
8.12 +% this should be the last package used
8.13 +\usepackage{pdfsetup}
8.14 +
8.15 +% proper setup for best-style documents
8.16 +\urlstyle{rm}
8.17 +\isabellestyle{it}
8.18
8.19  %\usepackage{substr}
8.20
8.21 @@ -10,33 +21,6 @@
8.22  %    \chapter{\BehindSubString{Chapter: }{#1}}}{%
8.23  %  \section{#1}}}
8.24
8.25 -% further packages required for unusual symbols (see also isabellesym.sty)
8.26 -
8.27 -%\usepackage{latexsym}                 % for \<leadsto>, \<box>, \<diamond>,
8.28 -                                       %   \<sqsupset>, \<mho>, \<Join>
8.29 -                                       %   and \<lhd> and others!
8.30 -\usepackage{amssymb}                  % for \<lesssim>, \<greatersim>,
8.31 -                                       %   \<lessapprox>, \<greaterapprox>,
8.32 -                                       %   \<triangleq>, \<yen>, \<lozenge>
8.33 -%\usepackage[english]{babel}           % for \<guillemotleft> \<guillemotright>
8.34 -\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
8.35 -                                       %   \<twosuperior>, \<onehalf>,
8.36 -                                       %   \<threesuperior>, \<threequarters>
8.37 -                                       %   \<degree>
8.38 -\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
8.39 -%\usepackage{wasysym}
8.40 -%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
8.41 -%\usepackage{textcomp}                  % for \<zero> ... \<nine>, \<cent>
8.42 -                                       %   \<currency>
8.43 -%\usepackage{marvosym}                 % for \<euro>
8.44 -
8.45 -% this should be the last package used
8.46 -\usepackage{pdfsetup}
8.47 -
8.48 -% proper setup for best-style documents
8.49 -\urlstyle{rm}
8.50 -\isabellestyle{it}
8.51 -
8.52
8.53  \begin{document}
8.54
8.55 @@ -53,10 +37,6 @@
8.56
8.57  \parindent 0pt\parskip 0.5ex
8.58
8.59 -% include generated text of all theories
8.60  \input{session}
8.61
8.62 -%\bibliographystyle{abbrv}
8.63 -%\bibliography{root}
8.64 -
8.65  \end{document}