improved notation;
authorwenzelm
Fri Apr 23 21:46:04 2004 +0200 (2004-04-23)
changeset 1466665f8680c3f16
parent 14665 d2e5df3d1201
child 14667 5a899cd54366
improved notation;
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/document/root.tex
     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. f`S = S & inj_on f S}"
    1.18 +  "Bij S == extensional S \<inter> {f. f`S = 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); f`S = 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}