src/HOL/Algebra/FiniteProduct.thy

     Author:     Clemens Ballarin, started 19 November 2002
 
 This file is largely based on HOL/Finite_Set.thy.
 *)
 
-header {* Product Operator for Commutative Monoids *}
-
 theory FiniteProduct imports Group begin
+
+
+section {* Product Operator for Commutative Monoids *}
+
+
+subsection {* Inductive Definition of a Relation for Products over Sets *}
 
 text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
   possible, because here we have explicit typing rules like 
   @{text "x \<in> carrier G"}.  We introduce an explicit argument for the domain
   @{text D}. *}

   with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
     by (intro foldSetD.intros) auto
   then show ?case ..
 qed
 
-subsection {* Left-commutative operations *}
+
+subsection {* Left-Commutative Operations *}
 
 locale LCD =
   fixes B :: "'b set"
   and D :: "'a set"
   and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)

   empty_foldSetDE [rule del]
   foldSetD.intros [rule del]
 declare (in LCD)
   foldSetD_closed [rule del]
 
-subsection {* Commutative monoids *}
+
+subsection {* Commutative Monoids *}
 
 text {*
   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   instead of @{text "'b => 'a => 'a"}.
 *}

 lemma (in ACeD) foldD_Un_disjoint:
   "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
     foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   by (simp add: foldD_Un_Int
     left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
+
 
 subsection {* Products over Finite Sets *}
 
 constdefs (structure G)
   finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"