# HG changeset patch
# User wenzelm
# Date 1082749564 -7200
# Node ID 65f8680c3f16f398db23b78c0de62a875ef1dcb0
# Parent  d2e5df3d120129495fcac7db9be1ea761f776049
improved notation;

diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/Bij.thy
--- a/src/HOL/Algebra/Bij.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Bij.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -3,41 +3,41 @@
     Author:     Florian Kammueller, with new proofs by L C Paulson
 *)
 
-
-header{*Bijections of a Set, Permutation Groups, Automorphism Groups*} 
+header {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
 
 theory Bij = Group:
 
 constdefs
-  Bij :: "'a set => (('a => 'a)set)" 
+  Bij :: "'a set => ('a => 'a) set"
     --{*Only extensional functions, since otherwise we get too many.*}
-    "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}"
+  "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}"
 
-   BijGroup ::  "'a set => (('a => 'a) monoid)"
-   "BijGroup S == (| carrier = Bij S, 
-		     mult  = %g: Bij S. %f: Bij S. compose S g f,
-		     one = %x: S. x |)"
+  BijGroup :: "'a set => ('a => 'a) monoid"
+  "BijGroup S ==
+    (| carrier = Bij S,
+      mult = %g: Bij S. %f: Bij S. compose S g f,
+      one = %x: S. x |)"
 
 
 declare Id_compose [simp] compose_Id [simp]
 
 lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
-by (simp add: Bij_def)
+  by (simp add: Bij_def)
 
 lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
-by (auto simp add: Bij_def Pi_def)
+  by (auto simp add: Bij_def Pi_def)
 
 lemma Bij_imp_apply: "f \<in> Bij S ==> f ` S = S"
-by (simp add: Bij_def)
+  by (simp add: Bij_def)
 
 lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S"
-by (simp add: Bij_def)
+  by (simp add: Bij_def)
 
 lemma BijI: "[| f \<in> extensional(S); f`S = S; inj_on f S |] ==> f \<in> Bij S"
-by (simp add: Bij_def)
+  by (simp add: Bij_def)
 
 
-subsection{*Bijections Form a Group*}
+subsection {*Bijections Form a Group *}
 
 lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
 apply (simp add: Bij_def)
@@ -60,7 +60,7 @@
 
 lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
 apply (rule BijI)
-  apply (simp add: compose_extensional) 
+  apply (simp add: compose_extensional)
  apply (blast del: equalityI
               intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on)
 apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on)
@@ -70,44 +70,44 @@
      "f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
 apply (rule compose_Inv_id)
  apply (simp add: Bij_imp_inj_on)
-apply (simp add: Bij_imp_apply) 
+apply (simp add: Bij_imp_apply)
 done
 
 theorem group_BijGroup: "group (BijGroup S)"
-apply (simp add: BijGroup_def) 
+apply (simp add: BijGroup_def)
 apply (rule groupI)
     apply (simp add: compose_Bij)
    apply (simp add: id_Bij)
   apply (simp add: compose_Bij)
   apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset)
  apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
-apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij) 
+apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
 done
 
 
 subsection{*Automorphisms Form a Group*}
 
 lemma Bij_Inv_mem: "[|  f \<in> Bij S;  x : S |] ==> Inv S f x : S"
-by (simp add: Bij_def Inv_mem) 
+by (simp add: Bij_def Inv_mem)
 
 lemma Bij_Inv_lemma:
  assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
- shows "[| h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S |]        
+ shows "[| h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S |]
         ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
-apply (simp add: Bij_def) 
+apply (simp add: Bij_def)
 apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'", clarify)
  apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
 done
 
 constdefs
- auto :: "('a,'b) monoid_scheme => ('a => 'a)set"
+  auto :: "('a, 'b) monoid_scheme => ('a => 'a) set"
   "auto G == hom G G \<inter> Bij (carrier G)"
 
-  AutoGroup :: "[('a,'c) monoid_scheme] => ('a=>'a) monoid"
+  AutoGroup :: "('a, 'c) monoid_scheme => ('a => 'a) monoid"
   "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
 
 lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
-  by (simp add: auto_def hom_def restrictI group.axioms id_Bij) 
+  by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
 
 lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G"
   by (simp add:  Pi_I group.axioms)
@@ -122,27 +122,26 @@
      "f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)"
 apply (rule group.inv_equality)
 apply (rule group_BijGroup)
-apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)  
+apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
 done
 
 lemma subgroup_auto:
       "group G ==> subgroup (auto G) (BijGroup (carrier G))"
-apply (rule group.subgroupI) 
-    apply (rule group_BijGroup) 
-   apply (force simp add: auto_def BijGroup_def) 
-  apply (blast intro: dest: id_in_auto) 
+apply (rule group.subgroupI)
+    apply (rule group_BijGroup)
+   apply (force simp add: auto_def BijGroup_def)
+  apply (blast intro: dest: id_in_auto)
  apply (simp del: restrict_apply
-	     add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom) 
+             add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
 apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij)
 done
 
 theorem AutoGroup: "group G ==> group (AutoGroup G)"
-apply (simp add: AutoGroup_def) 
+apply (simp add: AutoGroup_def)
 apply (rule Group.subgroup.groupI)
-apply (erule subgroup_auto)  
-apply (insert Bij.group_BijGroup [of "carrier G"]) 
-apply (simp_all add: group_def) 
+apply (erule subgroup_auto)
+apply (insert Bij.group_BijGroup [of "carrier G"])
+apply (simp_all add: group_def)
 done
 
 end
-
diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -189,13 +189,13 @@
 
 syntax
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
 syntax (xsymbols)
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
 syntax (HTML output)
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
   "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
 
diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -7,26 +7,26 @@
 
 theory Coset = Group + Exponent:
 
-declare (in group) l_inv [simp]  r_inv [simp] 
+declare (in group) l_inv [simp] and r_inv [simp]
 
 constdefs (structure G)
-  r_coset    :: "[_,'a set, 'a] => 'a set"    
-   "r_coset G H a == (% x. x \<otimes> a) ` H"
+  r_coset    :: "[_,'a set, 'a] => 'a set"
+  "r_coset G H a == (% x. x \<otimes> a) ` H"
 
   l_coset    :: "[_, 'a, 'a set] => 'a set"
-   "l_coset G a H == (% x. a \<otimes> x) ` H"
+  "l_coset G a H == (% x. a \<otimes> x) ` H"
 
   rcosets  :: "[_, 'a set] => ('a set)set"
-   "rcosets G H == r_coset G H ` (carrier G)"
+  "rcosets G H == r_coset G H ` (carrier G)"
 
   set_mult  :: "[_, 'a set ,'a set] => 'a set"
-   "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
+  "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
 
   set_inv   :: "[_,'a set] => 'a set"
-   "set_inv G H == m_inv G ` H"
+  "set_inv G H == m_inv G ` H"
 
   normal     :: "['a set, _] => bool"       (infixl "<|" 60)
-   "normal H G == subgroup H G & 
+  "normal H G == subgroup H G &
                   (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
 
 syntax (xsymbols)
@@ -56,13 +56,13 @@
 apply (auto simp add: Pi_def)
 done
 
-lemma card_bij: 
-     "[|f \<in> A\<rightarrow>B; inj_on f A; 
+lemma card_bij:
+     "[|f \<in> A\<rightarrow>B; inj_on f A;
         g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
-by (blast intro: card_inj order_antisym) 
+by (blast intro: card_inj order_antisym)
 
 
-subsection{*Lemmas Using Locale Constants*}
+subsection {*Lemmas Using *}
 
 lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
 by (auto simp add: rcos_def r_coset_def)
@@ -77,7 +77,7 @@
 by (simp add: setmult_def set_mult_def image_def)
 
 lemma (in coset) coset_mult_assoc:
-     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]  
+     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
       ==> (M #> g) #> h = M #> (g \<otimes> h)"
 by (force simp add: r_coset_eq m_assoc)
 
@@ -85,14 +85,14 @@
 by (force simp add: r_coset_eq)
 
 lemma (in coset) coset_mult_inv1:
-     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G; 
+     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
          M <= carrier G |] ==> M #> x = M #> y"
 apply (erule subst [of concl: "%z. M #> x = z #> y"])
 apply (simp add: coset_mult_assoc m_assoc)
 done
 
 lemma (in coset) coset_mult_inv2:
-     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M <= carrier G |]  
+     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M <= carrier G |]
       ==> M #> (x \<otimes> (inv y)) = M "
 apply (simp add: coset_mult_assoc [symmetric])
 apply (simp add: coset_mult_assoc)
@@ -110,7 +110,7 @@
 lemma (in coset) solve_equation:
     "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
 apply (rule bexI [of _ "y \<otimes> (inv x)"])
-apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc 
+apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
                       subgroup.subset [THEN subsetD])
 done
 
@@ -133,30 +133,30 @@
 
 text{*Really needed?*}
 lemma (in coset) transpose_inv:
-     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]  
+     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
       ==> (inv x) \<otimes> z = y"
 by (force simp add: m_assoc [symmetric])
 
 lemma (in coset) repr_independence:
      "[| y \<in> H #> x;  x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
-by (auto simp add: r_coset_eq m_assoc [symmetric] 
+by (auto simp add: r_coset_eq m_assoc [symmetric]
                    subgroup.subset [THEN subsetD]
                    subgroup.m_closed solve_equation)
 
 lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
 apply (simp add: r_coset_eq)
-apply (blast intro: l_one subgroup.subset [THEN subsetD] 
+apply (blast intro: l_one subgroup.subset [THEN subsetD]
                     subgroup.one_closed)
 done
 
 
-subsection{*normal subgroups*}
+subsection {* Normal subgroups *}
 
 (*????????????????
 text "Allows use of theorems proved in the locale coset"
 lemma subgroup_imp_coset: "subgroup H G ==> coset G"
 apply (drule subgroup_imp_group)
-apply (simp add: group_def coset_def)  
+apply (simp add: group_def coset_def)
 done
 *)
 
@@ -180,7 +180,7 @@
 lemma (in coset) normal_inv_op_closed1:
      "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
 apply (auto simp add: l_coset_eq r_coset_eq normal_iff)
-apply (drule bspec, assumption) 
+apply (drule bspec, assumption)
 apply (drule equalityD1 [THEN subsetD], blast, clarify)
 apply (simp add: m_assoc subgroup.subset [THEN subsetD])
 apply (erule subst)
@@ -189,12 +189,12 @@
 
 lemma (in coset) normal_inv_op_closed2:
      "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
-apply (drule normal_inv_op_closed1 [of H "(inv x)"]) 
+apply (drule normal_inv_op_closed1 [of H "(inv x)"])
 apply auto
 done
 
 lemma (in coset) lcos_m_assoc:
-     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]  
+     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
       ==> g <# (h <# M) = (g \<otimes> h) <# M"
 by (force simp add: l_coset_eq m_assoc)
 
@@ -208,8 +208,8 @@
 lemma (in coset) l_coset_swap:
      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> y <# H"
 proof (simp add: l_coset_eq)
-  assume "\<exists>h\<in>H. x \<otimes> h = y" 
-    and x: "x \<in> carrier G" 
+  assume "\<exists>h\<in>H. x \<otimes> h = y"
+    and x: "x \<in> carrier G"
     and sb: "subgroup H G"
   then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
   show "\<exists>h\<in>H. y \<otimes> h = x"
@@ -223,28 +223,28 @@
 
 lemma (in coset) l_coset_carrier:
      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
-by (auto simp add: l_coset_eq m_assoc 
+by (auto simp add: l_coset_eq m_assoc
                    subgroup.subset [THEN subsetD] subgroup.m_closed)
 
 lemma (in coset) l_repr_imp_subset:
-  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G" 
+  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   shows "y <# H \<subseteq> x <# H"
 proof -
   from y
   obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_eq)
   thus ?thesis using x sb
-    by (auto simp add: l_coset_eq m_assoc 
+    by (auto simp add: l_coset_eq m_assoc
                        subgroup.subset [THEN subsetD] subgroup.m_closed)
 qed
 
 lemma (in coset) l_repr_independence:
-  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G" 
+  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   shows "x <# H = y <# H"
-proof 
+proof
   show "x <# H \<subseteq> y <# H"
-    by (rule l_repr_imp_subset, 
+    by (rule l_repr_imp_subset,
         (blast intro: l_coset_swap l_coset_carrier y x sb)+)
-  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb]) 
+  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
 qed
 
 lemma (in coset) setmult_subset_G:
@@ -255,29 +255,30 @@
 apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
 apply (rule_tac x = x in bexI)
 apply (rule bexI [of _ "\<one>"])
-apply (auto simp add: subgroup.m_closed subgroup.one_closed 
+apply (auto simp add: subgroup.m_closed subgroup.one_closed
                       r_one subgroup.subset [THEN subsetD])
 done
 
 
-(* set of inverses of an r_coset *)
+text {* Set of inverses of an @{text r_coset}. *}
+
 lemma (in coset) rcos_inv:
   assumes normalHG: "H <| G"
       and xinG:     "x \<in> carrier G"
   shows "set_inv G (H #> x) = H #> (inv x)"
 proof -
-  have H_subset: "H <= carrier G" 
+  have H_subset: "H <= carrier G"
     by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
   show ?thesis
   proof (auto simp add: r_coset_eq image_def set_inv_def)
     fix h
     assume "h \<in> H"
       hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
-	by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
-      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)" 
+        by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
+      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
        using prems
-	by (blast intro: normal_inv_op_closed1 normal_imp_subgroup 
-			 subgroup.m_inv_closed)
+        by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
+                         subgroup.m_inv_closed)
   next
     fix h
     assume "h \<in> H"
@@ -285,9 +286,9 @@
         by (simp add: xinG m_assoc H_subset [THEN subsetD])
       hence "(\<exists>j\<in>H. j \<otimes> x = inv  (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
        using prems
-	by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
-            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup 
-			 subgroup.m_inv_closed)
+        by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
+            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
+                         subgroup.m_inv_closed)
       thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
   qed
 qed
@@ -314,7 +315,7 @@
 apply (simp add: setrcos_eq, clarify)
 apply (subgoal_tac "x : carrier G")
  prefer 2
- apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup) 
+ apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
 apply (drule repr_independence)
   apply assumption
  apply (erule normal_imp_subgroup)
@@ -322,56 +323,57 @@
 done
 
 
-(* some rules for <#> with #> or <# *)
+text {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
+
 lemma (in coset) setmult_rcos_assoc:
-     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |] 
+     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
       ==> H <#> (K #> x) = (H <#> K) #> x"
 apply (auto simp add: rcos_def r_coset_def setmult_def set_mult_def)
 apply (force simp add: m_assoc)+
 done
 
 lemma (in coset) rcos_assoc_lcos:
-     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |] 
+     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
       ==> (H #> x) <#> K = H <#> (x <# K)"
-apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def 
+apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
                       setmult_def set_mult_def Sigma_def image_def)
 apply (force intro!: exI bexI simp add: m_assoc)+
 done
 
 lemma (in coset) rcos_mult_step1:
-     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
+     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
       ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
 by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
 
 lemma (in coset) rcos_mult_step2:
-     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
+     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
       ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
 by (simp add: normal_imp_rcos_eq_lcos)
 
 lemma (in coset) rcos_mult_step3:
-     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
+     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
       ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
 by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
               setmult_subset_G  subgroup_mult_id
               subgroup.subset normal_imp_subgroup)
 
 lemma (in coset) rcos_sum:
-     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
+     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
       ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
 
-(*generalizes subgroup_mult_id*)
 lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
-by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
-                   setmult_rcos_assoc subgroup_mult_id)
+  -- {* generalizes @{text subgroup_mult_id} *}
+  by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
+    setmult_rcos_assoc subgroup_mult_id)
 
 
-subsection{*Lemmas Leading to Lagrange's Theorem*}
+subsection {*Lemmas Leading to Lagrange's Theorem *}
 
-lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
+lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
 apply (rule equalityI)
-apply (force simp add: subgroup.subset [THEN subsetD] 
+apply (force simp add: subgroup.subset [THEN subsetD]
                        setrcos_eq r_coset_eq)
 apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
 done
@@ -398,13 +400,13 @@
 by (force simp add: inj_on_def subsetD)
 
 lemma (in coset) card_cosets_equal:
-     "[| c \<in> rcosets G H;  H <= carrier G; finite(carrier G) |] 
+     "[| c \<in> rcosets G H;  H <= carrier G; finite(carrier G) |]
       ==> card c = card H"
 apply (auto simp add: setrcos_eq)
 apply (rule card_bij_eq)
-     apply (rule inj_on_f, assumption+) 
+     apply (rule inj_on_f, assumption+)
     apply (force simp add: m_assoc subsetD r_coset_eq)
-   apply (rule inj_on_g, assumption+) 
+   apply (rule inj_on_g, assumption+)
   apply (force simp add: m_assoc subsetD r_coset_eq)
  txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
  apply (simp add: r_coset_subset_G [THEN finite_subset])
@@ -414,8 +416,8 @@
 subsection{*Two distinct right cosets are disjoint*}
 
 lemma (in coset) rcos_equation:
-     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;   
-        h \<in> H;  ha \<in> H;  hb \<in> H|]  
+     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
+        h \<in> H;  ha \<in> H;  hb \<in> H|]
       ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
 apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
 apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
@@ -439,16 +441,16 @@
 constdefs
   FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
      (infixl "Mod" 60)
-   "FactGroup G H ==
-      (| carrier = rcosets G H,
-	 mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
-	 one = H (*,
-	 m_inv = (%X: rcosets G H. set_inv G X) *) |)"
+  "FactGroup G H ==
+    (| carrier = rcosets G H,
+       mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
+       one = H (*,
+       m_inv = (%X: rcosets G H. set_inv G X) *) |)"
 
 lemma (in coset) setmult_closed:
-     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |] 
+     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
       ==> K1 <#> K2 \<in> rcosets G H"
-by (auto simp add: normal_imp_subgroup [THEN subgroup.subset] 
+by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
                    rcos_sum setrcos_eq)
 
 lemma (in group) setinv_closed:
@@ -467,9 +469,9 @@
 *)
 
 lemma (in coset) setrcos_assoc:
-     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]   
+     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
       ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
-by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup 
+by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
                    subgroup.subset m_assoc)
 
 lemma (in group) subgroup_in_rcosets:
@@ -486,10 +488,10 @@
 (*
 lemma subgroup_in_rcosets:
   "subgroup H G ==> H \<in> rcosets G H"
-apply (frule subgroup_imp_coset) 
-apply (frule subgroup_imp_group) 
+apply (frule subgroup_imp_coset)
+apply (frule subgroup_imp_group)
 apply (simp add: coset.setrcos_eq)
-apply (blast del: equalityI 
+apply (blast del: equalityI
              intro!: group.subgroup.one_closed group.one_closed
                      coset.coset_join2 [symmetric])
 done
@@ -497,7 +499,7 @@
 
 lemma (in coset) setrcos_inv_mult_group_eq:
      "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
-by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup 
+by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
                    subgroup.subset)
 (*
 lemma (in group) factorgroup_is_magma:
@@ -511,8 +513,8 @@
 *)
 theorem (in group) factorgroup_is_group:
   "H <| G ==> group (G Mod H)"
-apply (insert is_coset) 
-apply (simp add: FactGroup_def) 
+apply (insert is_coset)
+apply (simp add: FactGroup_def)
 apply (rule groupI)
     apply (simp add: coset.setmult_closed)
    apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -290,13 +290,13 @@
 
 syntax
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
 syntax (xsymbols)
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 syntax (HTML output)
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
   "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
 
diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -186,6 +186,7 @@
   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   by (unfold greatest_def) blast
 
+
 subsubsection {* Supremum *}
 
 lemma (in lattice) joinI:
@@ -212,7 +213,8 @@
   shows "x \<in> carrier L ==> \<Squnion> {x} = x"
   by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
 
-text {* Condition on A: supremum exists. *}
+
+text {* Condition on @{text A}: supremum exists. *}
 
 lemma (in lattice) sup_insertI:
   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -4,7 +4,7 @@
 
 See Florian Kamm\"uller and L. C. Paulson,
     A Formal Proof of Sylow's theorem:
-	An Experiment in Abstract Algebra with Isabelle HOL
+        An Experiment in Abstract Algebra with Isabelle HOL
     J. Automated Reasoning 23 (1999), 235-264
 *)
 
@@ -15,11 +15,11 @@
 subsection {*Order of a Group and Lagrange's Theorem*}
 
 constdefs
-  order     :: "('a,'b) semigroup_scheme => nat"
+  order :: "('a, 'b) semigroup_scheme => nat"
   "order S == card (carrier S)"
 
 theorem (in coset) lagrange:
-     "[| finite(carrier G); subgroup H G |] 
+     "[| finite(carrier G); subgroup H G |]
       ==> card(rcosets G H) * card(H) = order(G)"
 apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
 apply (subst mult_commute)
@@ -40,11 +40,11 @@
       and finite_G [iff]:  "finite (carrier G)"
   defines "calM == {s. s <= carrier(G) & card(s) = p^a}"
       and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
-		  	     (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
+                             (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
 
 lemma (in sylow) RelM_refl: "refl calM RelM"
-apply (auto simp add: refl_def RelM_def calM_def) 
-apply (blast intro!: coset_mult_one [symmetric]) 
+apply (auto simp add: refl_def RelM_def calM_def)
+apply (blast intro!: coset_mult_one [symmetric])
 done
 
 lemma (in sylow) RelM_sym: "sym RelM"
@@ -58,7 +58,7 @@
 qed
 
 lemma (in sylow) RelM_trans: "trans RelM"
-by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc) 
+by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
 
 lemma (in sylow) RelM_equiv: "equiv calM RelM"
 apply (unfold equiv_def)
@@ -91,9 +91,9 @@
 lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
 by force
 
-lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1" 
-apply (subgoal_tac "0 < card M1") 
- apply (blast dest: card_nonempty) 
+lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
+apply (subgoal_tac "0 < card M1")
+ apply (blast dest: card_nonempty)
 apply (cut_tac prime_p [THEN prime_imp_one_less])
 apply (simp (no_asm_simp) add: card_M1)
 done
@@ -112,18 +112,18 @@
     show ?thesis
     proof
       show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
-	by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
+        by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
       show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
       proof (rule restrictI)
-	fix z assume zH: "z \<in> H"
-	show "m1 \<otimes> z \<in> M1"
-	proof -
-	  from zH
-	  have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1" 
-	    by (auto simp add: H_def)
-	  show ?thesis
-	    by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
-	qed
+        fix z assume zH: "z \<in> H"
+        show "m1 \<otimes> z \<in> M1"
+        proof -
+          from zH
+          have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
+            by (auto simp add: H_def)
+          show ?thesis
+            by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
+        qed
       qed
     qed
   qed
@@ -135,8 +135,8 @@
 by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
 
 lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
-apply (subgoal_tac "M \<noteq> {}") 
- apply blast 
+apply (subgoal_tac "M \<noteq> {}")
+ apply blast
 apply (cut_tac EmptyNotInEquivSet, blast)
 done
 
@@ -245,7 +245,7 @@
 text{*Injections between @{term M} and @{term "rcosets G H"} show that
  their cardinalities are equal.*}
 
-lemma ElemClassEquiv: 
+lemma ElemClassEquiv:
      "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
 apply (unfold equiv_def quotient_def sym_def trans_def, blast)
 done
@@ -257,11 +257,11 @@
 apply (blast dest!: bspec)
 done
 
-lemmas (in sylow_central) M_elem_map_carrier = 
-	M_elem_map [THEN someI_ex, THEN conjunct1]
+lemmas (in sylow_central) M_elem_map_carrier =
+        M_elem_map [THEN someI_ex, THEN conjunct1]
 
 lemmas (in sylow_central) M_elem_map_eq =
-	M_elem_map [THEN someI_ex, THEN conjunct2]
+        M_elem_map [THEN someI_ex, THEN conjunct2]
 
 lemma (in sylow_central) M_funcset_setrcos_H:
      "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
@@ -293,14 +293,14 @@
      "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
 by (auto simp add: setrcos_eq)
 
-lemmas (in sylow_central) H_elem_map_carrier = 
-	H_elem_map [THEN someI_ex, THEN conjunct1]
+lemmas (in sylow_central) H_elem_map_carrier =
+        H_elem_map [THEN someI_ex, THEN conjunct1]
 
 lemmas (in sylow_central) H_elem_map_eq =
-	H_elem_map [THEN someI_ex, THEN conjunct2]
+        H_elem_map [THEN someI_ex, THEN conjunct2]
 
 
-lemma EquivElemClass: 
+lemma EquivElemClass:
      "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
 apply (unfold equiv_def quotient_def sym_def trans_def, blast)
 done
@@ -329,7 +329,7 @@
 apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
 apply (rule coset_join2)
 apply (blast intro: m_closed inv_closed H_elem_map_carrier)
-apply (rule H_is_subgroup) 
+apply (rule H_is_subgroup)
 apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier)
 done
 
@@ -344,9 +344,9 @@
 done
 
 lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
-apply (insert inj_M_GmodH inj_GmodH_M) 
-apply (blast intro: card_bij finite_M H_is_subgroup 
-             setrcos_subset_PowG [THEN finite_subset] 
+apply (insert inj_M_GmodH inj_GmodH_M)
+apply (blast intro: card_bij finite_M H_is_subgroup
+             setrcos_subset_PowG [THEN finite_subset]
              finite_Pow_iff [THEN iffD2])
 done
 
@@ -364,7 +364,7 @@
 lemma (in sylow_central) lemma_leq2: "card(H) <= p^a"
 apply (subst card_M1 [symmetric])
 apply (cut_tac M1_inj_H)
-apply (blast intro!: M1_subset_G intro: 
+apply (blast intro!: M1_subset_G intro:
              card_inj H_into_carrier_G finite_subset [OF _ finite_G])
 done
 
@@ -372,15 +372,15 @@
 by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
 
 lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
-apply (cut_tac lemma_A1, clarify) 
-apply (frule existsM1inM, clarify) 
+apply (cut_tac lemma_A1, clarify)
+apply (frule existsM1inM, clarify)
 apply (subgoal_tac "sylow_central G p a m M1 M")
  apply (blast dest:  sylow_central.H_is_subgroup sylow_central.card_H_eq)
-apply (simp add: sylow_central_def sylow_central_axioms_def prems) 
+apply (simp add: sylow_central_def sylow_central_axioms_def prems)
 done
 
 text{*Needed because the locale's automatic definition refers to
-   @{term "semigroup G"} and @{term "group_axioms G"} rather than 
+   @{term "semigroup G"} and @{term "group_axioms G"} rather than
   simply to @{term "group G"}.*}
 lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
 by (simp add: sylow_def group_def)
@@ -389,7 +389,7 @@
      "[|p \<in> prime;  group(G);  order(G) = (p^a) * m; finite (carrier G)|]
       ==> \<exists>H. subgroup H G & card(H) = p^a"
 apply (rule sylow.sylow_thm [of G p a m])
-apply (simp add: sylow_eq sylow_axioms_def) 
+apply (simp add: sylow_eq sylow_axioms_def)
 done
 
 end
diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -10,43 +10,32 @@
 theory UnivPoly = Module:
 
 text {*
-  Polynomials are formalised as modules with additional operations for 
-  extracting coefficients from polynomials and for obtaining monomials 
-  from coefficients and exponents (record @{text "up_ring"}).
-  The carrier set is 
-  a set of bounded functions from Nat to the coefficient domain.  
-  Bounded means that these functions return zero above a certain bound 
-  (the degree).  There is a chapter on the formalisation of polynomials 
-  in my PhD thesis (http://www4.in.tum.de/\~{}ballarin/publications/), 
-  which was implemented with axiomatic type classes.  This was later
-  ported to Locales.
+  Polynomials are formalised as modules with additional operations for
+  extracting coefficients from polynomials and for obtaining monomials
+  from coefficients and exponents (record @{text "up_ring"}).  The
+  carrier set is a set of bounded functions from Nat to the
+  coefficient domain.  Bounded means that these functions return zero
+  above a certain bound (the degree).  There is a chapter on the
+  formalisation of polynomials in my PhD thesis
+  (\url{http://www4.in.tum.de/~ballarin/publications/}), which was
+  implemented with axiomatic type classes.  This was later ported to
+  Locales.
 *}
 
+
 subsection {* The Constructor for Univariate Polynomials *}
 
-(* Could alternatively use locale ...
-locale bound = cring + var bound +
-  defines ...
-*)
-
-constdefs
-  bound  :: "['a, nat, nat => 'a] => bool"
-  "bound z n f == (ALL i. n < i --> f i = z)"
+locale bound =
+  fixes z :: 'a
+    and n :: nat
+    and f :: "nat => 'a"
+  assumes bound: "!!m. n < m \<Longrightarrow> f m = z"
 
-lemma boundI [intro!]:
-  "[| !! m. n < m ==> f m = z |] ==> bound z n f"
-  by (unfold bound_def) fast
-
-lemma boundE [elim?]:
-  "[| bound z n f; (!! m. n < m ==> f m = z) ==> P |] ==> P"
-  by (unfold bound_def) fast
-
-lemma boundD [dest]:
-  "[| bound z n f; n < m |] ==> f m = z"
-  by (unfold bound_def) fast
+declare bound.intro [intro!]
+  and bound.bound [dest]
 
 lemma bound_below:
-  assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m"
+  assumes bound: "bound z m f" and nonzero: "f n \<noteq> z" shows "n \<le> m"
 proof (rule classical)
   assume "~ ?thesis"
   then have "m < n" by arith
@@ -130,45 +119,45 @@
 
 lemma (in cring) up_mult_closed:
   "[| p \<in> up R; q \<in> up R |] ==>
-  (%n. finsum R (%i. p i \<otimes> q (n-i)) {..n}) \<in> up R"
+  (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
 proof
   fix n
   assume "p \<in> up R" "q \<in> up R"
-  then show "finsum R (%i. p i \<otimes> q (n-i)) {..n} \<in> carrier R"
+  then show "(\<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> carrier R"
     by (simp add: mem_upD  funcsetI)
 next
   assume UP: "p \<in> up R" "q \<in> up R"
-  show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
+  show "EX n. bound \<zero> n (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
   proof -
     from UP obtain n where boundn: "bound \<zero> n p" by fast
     from UP obtain m where boundm: "bound \<zero> m q" by fast
-    have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
+    have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
     proof
-      fix k
-      assume bound: "n + m < k"
+      fix k assume bound: "n + m < k"
       {
-	fix i
-	have "p i \<otimes> q (k-i) = \<zero>"
-	proof (cases "n < i")
-	  case True
-	  with boundn have "p i = \<zero>" by auto
+        fix i
+        have "p i \<otimes> q (k-i) = \<zero>"
+        proof (cases "n < i")
+          case True
+          with boundn have "p i = \<zero>" by auto
           moreover from UP have "q (k-i) \<in> carrier R" by auto
-	  ultimately show ?thesis by simp
-	next
-	  case False
-	  with bound have "m < k-i" by arith
-	  with boundm have "q (k-i) = \<zero>" by auto
-	  moreover from UP have "p i \<in> carrier R" by auto
-	  ultimately show ?thesis by simp
-	qed
+          ultimately show ?thesis by simp
+        next
+          case False
+          with bound have "m < k-i" by arith
+          with boundm have "q (k-i) = \<zero>" by auto
+          moreover from UP have "p i \<in> carrier R" by auto
+          ultimately show ?thesis by simp
+        qed
       }
-      then show "finsum R (%i. p i \<otimes> q (k-i)) {..k} = \<zero>"
-	by (simp add: Pi_def)
+      then show "(\<Oplus>i \<in> {..k}. p i \<otimes> q (k-i)) = \<zero>"
+        by (simp add: Pi_def)
     qed
     then show ?thesis by fast
   qed
 qed
 
+
 subsection {* Effect of operations on coefficients *}
 
 locale UP = struct R + struct P +
@@ -214,7 +203,7 @@
 
 lemma (in UP_cring) coeff_mult [simp]:
   "[| p \<in> carrier P; q \<in> carrier P |] ==>
-  coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (n-i)) {..n}"
+  coeff P (p \<otimes>\<^sub>2 q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
   by (simp add: UP_def up_mult_closed)
 
 lemma (in UP) up_eqI:
@@ -225,10 +214,10 @@
   fix x
   from prem and R show "p x = q x" by (simp add: UP_def)
 qed
-  
+
 subsection {* Polynomials form a commutative ring. *}
 
-text {* Operations are closed over @{term "P"}. *}
+text {* Operations are closed over @{term P}. *}
 
 lemma (in UP_cring) UP_mult_closed [simp]:
   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^sub>2 q \<in> carrier P"
@@ -307,9 +296,9 @@
     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
       "c \<in> UNIV -> carrier R"
     then have "k <= n ==>
-      finsum R (%j. finsum R (%i. a i \<otimes> b (j-i)) {..j} \<otimes> c (n-j)) {..k} =
-      finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (n-j-i)) {..k-j}) {..k}"
-      (is "_ ==> ?eq k")
+      (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
+      (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
+      (concl is "?eq k")
     proof (induct k)
       case 0 then show ?case by (simp add: Pi_def m_assoc)
     next
@@ -317,7 +306,7 @@
       then have "k <= n" by arith
       then have "?eq k" by (rule Suc)
       with R show ?case
-	by (simp cong: finsum_cong
+        by (simp cong: finsum_cong
              add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
           (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
     qed
@@ -353,19 +342,19 @@
   assumes R: "p \<in> carrier P" "q \<in> carrier P"
   shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p"
 proof (rule up_eqI)
-  fix n 
+  fix n
   {
     fix k and a b :: "nat=>'a"
     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
-    then have "k <= n ==> 
-      finsum R (%i. a i \<otimes> b (n-i)) {..k} =
-      finsum R (%i. a (k-i) \<otimes> b (i+n-k)) {..k}"
-      (is "_ ==> ?eq k")
+    then have "k <= n ==>
+      (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
+      (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
+      (concl is "?eq k")
     proof (induct k)
       case 0 then show ?case by (simp add: Pi_def)
     next
       case (Suc k) then show ?case
-	by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
+        by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
     qed
   }
   note l = this
@@ -557,6 +546,7 @@
 lemmas (in UP_cring) UP_finsum_rdistr =
   cring.finsum_rdistr [OF UP_cring]
 
+
 subsection {* Polynomials form an Algebra *}
 
 lemma (in UP_cring) UP_smult_l_distr:
@@ -658,64 +648,64 @@
   proof (cases "k = Suc n")
     case True show ?thesis
     proof -
-      from True have less_add_diff: 
-	"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
+      from True have less_add_diff:
+        "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
       from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
       also from True
-      have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
-	coeff P (monom P \<one> 1) (k - i)) ({..n(} Un {n})"
-	by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
-      also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
-	coeff P (monom P \<one> 1) (k - i)) {..n}"
-	by (simp only: ivl_disj_un_singleton)
-      also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
-	coeff P (monom P \<one> 1) (k - i)) ({..n} Un {)n..k})"
-	by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
-	  order_less_imp_not_eq Pi_def)
+      have "... = (\<Oplus>i \<in> {..n(} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
+        coeff P (monom P \<one> 1) (k - i))"
+        by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
+      also have "... = (\<Oplus>i \<in>  {..n}. coeff P (monom P \<one> n) i \<otimes>
+        coeff P (monom P \<one> 1) (k - i))"
+        by (simp only: ivl_disj_un_singleton)
+      also from True have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. coeff P (monom P \<one> n) i \<otimes>
+        coeff P (monom P \<one> 1) (k - i))"
+        by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
+          order_less_imp_not_eq Pi_def)
       also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
-	by (simp add: ivl_disj_un_one)
+        by (simp add: ivl_disj_un_one)
       finally show ?thesis .
     qed
   next
     case False
     note neq = False
     let ?s =
-      "(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>))"
+      "\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>)"
     from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
-    also have "... = finsum R ?s {..k}"
+    also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
     proof -
-      have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def)
-      from neq have f2: "finsum R ?s {n} = \<zero>"
-	by (simp cong: finsum_cong add: Pi_def) arith
-      have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>"
-	by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
+      have f1: "(\<Oplus>i \<in> {..n(}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
+      from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
+        by (simp cong: finsum_cong add: Pi_def) arith
+      have f3: "n < k ==> (\<Oplus>i \<in> {)n..k}. ?s i) = \<zero>"
+        by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
       show ?thesis
       proof (cases "k < n")
-	case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
+        case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
       next
-	case False then have n_le_k: "n <= k" by arith
-	show ?thesis
-	proof (cases "n = k")
-	  case True
-	  then have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
-	    by (simp cong: finsum_cong add: finsum_Un_disjoint
-	      ivl_disj_int_singleton Pi_def)
-	  also from True have "... = finsum R ?s {..k}"
-	    by (simp only: ivl_disj_un_singleton)
-	  finally show ?thesis .
-	next
-	  case False with n_le_k have n_less_k: "n < k" by arith
-	  with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
-	    by (simp add: finsum_Un_disjoint f1 f2
-	      ivl_disj_int_singleton Pi_def del: Un_insert_right)
-	  also have "... = finsum R ?s {..n}"
-	    by (simp only: ivl_disj_un_singleton)
-	  also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})"
-	    by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
-	  also from n_less_k have "... = finsum R ?s {..k}"
-	    by (simp only: ivl_disj_un_one)
-	  finally show ?thesis .
-	qed
+        case False then have n_le_k: "n <= k" by arith
+        show ?thesis
+        proof (cases "n = k")
+          case True
+          then have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
+            by (simp cong: finsum_cong add: finsum_Un_disjoint
+              ivl_disj_int_singleton Pi_def)
+          also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
+            by (simp only: ivl_disj_un_singleton)
+          finally show ?thesis .
+        next
+          case False with n_le_k have n_less_k: "n < k" by arith
+          with neq have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
+            by (simp add: finsum_Un_disjoint f1 f2
+              ivl_disj_int_singleton Pi_def del: Un_insert_right)
+          also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
+            by (simp only: ivl_disj_un_singleton)
+          also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. ?s i)"
+            by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
+          also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
+            by (simp only: ivl_disj_un_one)
+          finally show ?thesis .
+        qed
       qed
     qed
     also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp
@@ -789,7 +779,7 @@
   "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
 
 lemma (in UP_cring) deg_aboveI:
-  "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n" 
+  "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
   by (unfold deg_def P_def) (fast intro: Least_le)
 (*
 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
@@ -798,7 +788,7 @@
   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   then show ?thesis ..
 qed
-  
+
 lemma bound_coeff_obtain:
   assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
 proof -
@@ -811,18 +801,18 @@
   "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
 proof -
   assume R: "p \<in> carrier P" and "deg R p < m"
-  from R obtain n where "bound \<zero> n (coeff P p)" 
+  from R obtain n where "bound \<zero> n (coeff P p)"
     by (auto simp add: UP_def P_def)
   then have "bound \<zero> (deg R p) (coeff P p)"
     by (auto simp: deg_def P_def dest: LeastI)
-  then show ?thesis by (rule boundD)
+  then show ?thesis ..
 qed
 
 lemma (in UP_cring) deg_belowI:
   assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
     and R: "p \<in> carrier P"
   shows "n <= deg R p"
--- {* Logically, this is a slightly stronger version of 
+-- {* Logically, this is a slightly stronger version of
   @{thm [source] deg_aboveD} *}
 proof (cases "n=0")
   case True then show ?thesis by simp
@@ -847,7 +837,7 @@
     then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
       by (unfold bound_def) fast
     then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
-    then show ?thesis by auto 
+    then show ?thesis by auto
   qed
   with deg_belowI R have "deg R p = m" by fastsimp
   with m_coeff show ?thesis by simp
@@ -890,7 +880,7 @@
   shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)"
 proof (cases "deg R p <= deg R q")
   case True show ?thesis
-    by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 
+    by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
 next
   case False show ?thesis
     by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
@@ -933,7 +923,7 @@
 proof (rule le_anti_sym)
   show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
 next
-  show "deg R p <= deg R (\<ominus>\<^sub>2 p)" 
+  show "deg R p <= deg R (\<ominus>\<^sub>2 p)"
     by (simp add: deg_belowI lcoeff_nonzero_deg
       inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
 qed
@@ -999,10 +989,10 @@
         deg_aboveD less_add_diff R Pi_def)
     also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
       by (simp only: ivl_disj_un_singleton)
-    also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 
+    also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
       by (simp cong: finsum_cong add: finsum_Un_disjoint
-	ivl_disj_int_singleton deg_aboveD R Pi_def)
-    finally have "finsum R ?s {.. deg R p + deg R q} 
+        ivl_disj_int_singleton deg_aboveD R Pi_def)
+    finally have "finsum R ?s {.. deg R p + deg R q}
       = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
     with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>"
       by (simp add: integral_iff lcoeff_nonzero R)
@@ -1021,7 +1011,7 @@
 
 lemma (in UP_cring) up_repr:
   assumes R: "p \<in> carrier P"
-  shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p"
+  shows "(\<Oplus>\<^sub>2 i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
 proof (rule up_eqI)
   let ?s = "(%i. monom P (coeff P p i) i)"
   fix k
@@ -1030,23 +1020,23 @@
   show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k"
   proof (cases "k <= deg R p")
     case True
-    hence "coeff P (finsum P ?s {..deg R p}) k = 
+    hence "coeff P (finsum P ?s {..deg R p}) k =
           coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
       by (simp only: ivl_disj_un_one)
     also from True
     have "... = coeff P (finsum P ?s {..k}) k"
       by (simp cong: finsum_cong add: finsum_Un_disjoint
-	ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
+        ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
     also
     have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff P p k"
       by (simp cong: finsum_cong add: setsum_Un_disjoint
-	ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
+        ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
     finally show ?thesis .
   next
     case False
-    hence "coeff P (finsum P ?s {..deg R p}) k = 
+    hence "coeff P (finsum P ?s {..deg R p}) k =
           coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
       by (simp only: ivl_disj_un_singleton)
     also from False have "... = coeff P p k"
@@ -1107,11 +1097,11 @@
     also from pq have "... = 0" by simp
     finally have "deg R p + deg R q = 0" .
     then have f1: "deg R p = 0 & deg R q = 0" by simp
-    from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}"
+    from f1 R have "p = (\<Oplus>\<^sub>2 i \<in> {..0}. monom P (coeff P p i) i)"
       by (simp only: up_repr_le)
     also from R have "... = monom P (coeff P p 0) 0" by simp
     finally have p: "p = monom P (coeff P p 0) 0" .
-    from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}"
+    from f1 R have "q = (\<Oplus>\<^sub>2 i \<in> {..0}. monom P (coeff P q i) i)"
       by (simp only: up_repr_le)
     also from R have "... = monom P (coeff P q 0) 0" by simp
     finally have q: "q = monom P (coeff P q 0) 0" .
@@ -1149,49 +1139,49 @@
   by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
     inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
 
+
 subsection {* Evaluation Homomorphism and Universal Property*}
 
+(* alternative congruence rule (possibly more efficient)
+lemma (in abelian_monoid) finsum_cong2:
+  "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
+  !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
+  sorry*)
+
 ML_setup {*
   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
 *}
 
-(* alternative congruence rule (possibly more efficient)
-lemma (in abelian_monoid) finsum_cong2:
-  "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
-  !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
-  sorry
-*)
-
 theorem (in cring) diagonal_sum:
   "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
-  finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..n + m} =
-  finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
+  (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+  (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
 proof -
   assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
   {
     fix j
     have "j <= n + m ==>
-      finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..j} =
-      finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j - k}) {..j}"
+      (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+      (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..j - k}. f k \<otimes> g i)"
     proof (induct j)
       case 0 from Rf Rg show ?case by (simp add: Pi_def)
     next
-      case (Suc j) 
+      case (Suc j)
       (* The following could be simplified if there was a reasoner for
-	total orders integrated with simip. *)
+        total orders integrated with simip. *)
       have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
-	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
       have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
-	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
       have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
-	using Suc by (auto intro!: funcset_mem [OF Rf])
+        using Suc by (auto intro!: funcset_mem [OF Rf])
       have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
-	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
       have R11: "g 0 \<in> carrier R"
-	using Suc by (auto intro!: funcset_mem [OF Rg])
+        using Suc by (auto intro!: funcset_mem [OF Rg])
       from Suc show ?case
-	by (simp cong: finsum_cong add: Suc_diff_le a_ac
-	  Pi_def R6 R8 R9 R10 R11)
+        by (simp cong: finsum_cong add: Suc_diff_le a_ac
+          Pi_def R6 R8 R9 R10 R11)
     qed
   }
   then show ?thesis by fast
@@ -1204,9 +1194,8 @@
 theorem (in cring) cauchy_product:
   assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
     and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
-  shows "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
-    finsum R f {..n} \<otimes> finsum R g {..m}"
-(* State revese direction? *)
+  shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+    (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"        (* State revese direction? *)
 proof -
   have f: "!!x. f x \<in> carrier R"
   proof -
@@ -1220,24 +1209,20 @@
     show "g x \<in> carrier R"
       using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
   qed
-  from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
-    finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
+  from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+      (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
     by (simp add: diagonal_sum Pi_def)
-  also have "... = finsum R
-      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) ({..n} Un {)n..n + m})"
+  also have "... = (\<Oplus>k \<in> {..n} \<union> {)n..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
     by (simp only: ivl_disj_un_one)
-  also from f g have "... = finsum R
-      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n}"
+  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
     by (simp cong: finsum_cong
-      add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
-  also from f g have "... = finsum R
-      (%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m - k})) {..n}"
+      add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
+  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {)m..n + m - k}. f k \<otimes> g i)"
     by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
-  also from f g have "... = finsum R
-      (%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}"
+  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
     by (simp cong: finsum_cong
-      add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
-  also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}"
+      add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
+  also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"
     by (simp add: finsum_ldistr diagonal_sum Pi_def,
       simp cong: finsum_cong add: finsum_rdistr Pi_def)
   finally show ?thesis .
@@ -1256,13 +1241,13 @@
   then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
   else arbitrary"
 *)
-                                                         
+
 locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
 
 lemma (in ring_hom_UP_cring) eval_on_carrier:
   "p \<in> carrier P ==>
     eval R S phi s p =
-    finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}"
+    (\<Oplus>\<^sub>2 i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^sub>2 pow S s i)"
   by (unfold eval_def, fold P_def) simp
 
 lemma (in ring_hom_UP_cring) eval_extensional:
@@ -1282,31 +1267,29 @@
   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"
   proof (simp only: eval_on_carrier UP_mult_closed)
     from RS have
-      "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)} =
-      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)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})"
+      "(\<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) =
+      (\<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}.
+        h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp cong: finsum_cong
-	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
-	del: coeff_mult)
+        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
+        del: coeff_mult)
     also from RS have "... =
-      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}"
+      (\<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)"
       by (simp only: ivl_disj_un_one deg_mult_cring)
     also from RS have "... =
-      finsum S (%i.
-        finsum S (%k. 
-        (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)))
-      {..i}) {..deg R p + deg R q}"
+      (\<Oplus>\<^sub>2 i \<in> {..deg R p + deg R q}.
+       \<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)))"
       by (simp cong: finsum_cong add: nat_pow_mult Pi_def
-	S.m_ac S.finsum_rdistr)
+        S.m_ac S.finsum_rdistr)
     also from RS have "... =
-      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
-      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
-      by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac
-	Pi_def)
+      (\<Oplus>\<^sub>2i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<otimes>\<^sub>2
+      (\<Oplus>\<^sub>2i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
+      by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
+        Pi_def)
     finally show
-      "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)} =
-      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
-      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" .
+      "(\<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) =
+      (\<Oplus>\<^sub>2 i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<otimes>\<^sub>2
+      (\<Oplus>\<^sub>2 i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)" .
   qed
 next
   fix p q
@@ -1314,36 +1297,35 @@
   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"
   proof (simp only: eval_on_carrier UP_a_closed)
     from RS have
-      "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)} =
-      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)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})"
+      "(\<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) =
+      (\<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)}.
+        h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp cong: finsum_cong
-	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
-	del: coeff_add)
+        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
+        del: coeff_add)
     also from RS have "... =
-      finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
-        {..max (deg R p) (deg R q)}"
+        (\<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)"
       by (simp add: ivl_disj_un_one)
     also from RS have "... =
-      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
-      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}"
+      (\<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
+      (\<Oplus>\<^sub>2i\<in>{..max (deg R p) (deg R q)}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp cong: finsum_cong
-	add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
+        add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
     also have "... =
-      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
-        ({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2
-      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
-        ({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})"
+        (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {)deg R p..max (deg R p) (deg R q)}.
+          h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
+        (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {)deg R q..max (deg R p) (deg R q)}.
+          h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
     also from RS have "... =
-      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
-      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
+      (\<Oplus>\<^sub>2 i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
+      (\<Oplus>\<^sub>2 i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp cong: finsum_cong
-	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
+        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
     finally show
-      "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)} =
-      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
-      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
+      "(\<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) =
+      (\<Oplus>\<^sub>2i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
+      (\<Oplus>\<^sub>2i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       .
   qed
 next
@@ -1414,14 +1396,14 @@
   "s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
 proof (simp only: eval_on_carrier monom_closed R.one_closed)
   assume S: "s \<in> carrier S"
-  then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
-      {..deg R (monom P \<one> 1)} =
-    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
-      ({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})"
+  then have
+    "(\<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) =
+    (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {)deg R (monom P \<one> 1)..1}.
+      h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
     by (simp cong: finsum_cong del: coeff_monom
       add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
-  also have "... = 
-    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}"
+  also have "... =
+    (\<Oplus>\<^sub>2 i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
     by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
   also have "... = s"
   proof (cases "s = \<zero>\<^sub>2")
@@ -1429,8 +1411,8 @@
   next
     case False with S show ?thesis by (simp add: Pi_def)
   qed
-  finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
-      {..deg R (monom P \<one> 1)} = s" .
+  finally show "(\<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) = s" .
 qed
 
 lemma (in UP_cring) monom_pow:
@@ -1491,15 +1473,13 @@
     by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
   have Psi_hom: "ring_hom_cring P S Psi"
     by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
-  have "Phi p = Phi (finsum P
-    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
+  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)"
     by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
-  also have "... = Psi (finsum P
-    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
-    by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom] 
+  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)"
+    by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
       ring_hom_cring.hom_mult [OF Phi_hom]
       ring_hom_cring.hom_pow [OF Phi_hom] Phi
-      ring_hom_cring.hom_finsum [OF Psi_hom] 
+      ring_hom_cring.hom_finsum [OF Psi_hom]
       ring_hom_cring.hom_mult [OF Psi_hom]
       ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
   also have "... = Psi p"
@@ -1511,13 +1491,13 @@
 theorem (in ring_hom_UP_cring) UP_universal_property:
   "s \<in> carrier S ==>
   EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
-    Phi (monom P \<one> 1) = s & 
+    Phi (monom P \<one> 1) = s &
     (ALL r : carrier R. Phi (monom P r 0) = h r)"
-  using eval_monom1                              
+  using eval_monom1
   apply (auto intro: eval_ring_hom eval_const eval_extensional)
-  apply (rule extensionalityI)                                 
-  apply (auto intro: UP_hom_unique)                            
-  done                                                         
+  apply (rule extensionalityI)
+  apply (auto intro: UP_hom_unique)
+  done
 
 subsection {* Sample application of evaluation homomorphism *}
 
@@ -1545,7 +1525,8 @@
 text {*
   An instantiation mechanism would now import all theorems and lemmas
   valid in the context of homomorphisms between @{term INTEG} and @{term
-  "UP INTEG"}.  *}
+  "UP INTEG"}.
+*}
 
 lemma INTEG_closed [intro, simp]:
   "z \<in> carrier INTEG"
@@ -1562,6 +1543,4 @@
 lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
   by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id])
 
--- {* Calculates @{term "x = 500"} *}
-
 end
diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/document/root.tex
--- a/src/HOL/Algebra/document/root.tex	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/document/root.tex	Fri Apr 23 21:46:04 2004 +0200
@@ -2,6 +2,17 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
+\usepackage{amssymb}
+\usepackage[latin1]{inputenc}
+\usepackage[only,bigsqcap]{stmaryrd}
+%\usepackage{masmath}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% proper setup for best-style documents
+\urlstyle{rm}
+\isabellestyle{it}
 
 %\usepackage{substr}
 
@@ -10,33 +21,6 @@
 %    \chapter{\BehindSubString{Chapter: }{#1}}}{%
 %  \section{#1}}}
 
-% further packages required for unusual symbols (see also isabellesym.sty)
-
-%\usepackage{latexsym}                 % for \<leadsto>, \<box>, \<diamond>,
-                                       %   \<sqsupset>, \<mho>, \<Join>
-                                       %   and \<lhd> and others!
-\usepackage{amssymb}                  % for \<lesssim>, \<greatersim>,
-                                       %   \<lessapprox>, \<greaterapprox>,
-                                       %   \<triangleq>, \<yen>, \<lozenge>
-%\usepackage[english]{babel}           % for \<guillemotleft> \<guillemotright>
-\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
-                                       %   \<twosuperior>, \<onehalf>,
-                                       %   \<threesuperior>, \<threequarters>
-                                       %   \<degree>
-\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
-%\usepackage{wasysym}
-%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
-%\usepackage{textcomp}                  % for \<zero> ... \<nine>, \<cent>
-                                       %   \<currency>
-%\usepackage{marvosym}                 % for \<euro>
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% proper setup for best-style documents
-\urlstyle{rm}
-\isabellestyle{it}
-
 
 \begin{document}
 
@@ -53,10 +37,6 @@
 
 \parindent 0pt\parskip 0.5ex
 
-% include generated text of all theories
 \input{session}
 
-%\bibliographystyle{abbrv}
-%\bibliography{root}
-
 \end{document}