# HG changeset patch
# User haftmann
# Date 1268917020 -3600
# Node ID b766aad9136d58c0e6abe018ed9c04861d63b56e
# Parent  10e723e540760e41575aab8a5e95a25072673a77# Parent  bd26885af9f41e1b7bcb0416b6e7d69053491463
merged

diff -r 10e723e54076 -r b766aad9136d src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Mar 18 13:57:00 2010 +0100
@@ -9,13 +9,44 @@
 imports Plain
 begin
 
+subsection {* Generic monoid operation over a set *}
+
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
+
+locale comm_monoid_big = comm_monoid +
+  fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
+  assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)"
+
+sublocale comm_monoid_big < folding_image proof
+qed (simp add: F_eq)
+
+context comm_monoid_big
+begin
+
+lemma infinite [simp]:
+  "\<not> finite A \<Longrightarrow> F g A = 1"
+  by (simp add: F_eq)
+
+end
+
+text {* for ad-hoc proofs for @{const fold_image} *}
+
+lemma (in comm_monoid_add) comm_monoid_mult:
+  "comm_monoid_mult (op +) 0"
+proof qed (auto intro: add_assoc add_commute)
+
+notation times (infixl "*" 70)
+notation Groups.one ("1")
+
+
 subsection {* Generalized summation over a set *}
 
-interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add"
-  proof qed (auto intro: add_assoc add_commute)
+definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
+  "setsum f A = (if finite A then fold_image (op +) f 0 A else 0)"
 
-definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
-where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
+sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof
+qed (fact setsum_def)
 
 abbreviation
   Setsum  ("\<Sum>_" [1000] 999) where
@@ -63,26 +94,30 @@
 in [(@{const_syntax setsum}, setsum_tr')] end
 *}
 
-
-lemma setsum_empty [simp]: "setsum f {} = 0"
-by (simp add: setsum_def)
+lemma setsum_empty:
+  "setsum f {} = 0"
+  by (fact setsum.empty)
 
-lemma setsum_insert [simp]:
+lemma setsum_insert:
   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
-by (simp add: setsum_def)
+  by (fact setsum.insert)
+
+lemma setsum_infinite:
+  "~ finite A ==> setsum f A = 0"
+  by (fact setsum.infinite)
 
-lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
-by (simp add: setsum_def)
+lemma (in comm_monoid_add) setsum_reindex:
+  assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B"
+proof -
+  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+  from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD)
+qed
 
-lemma setsum_reindex:
-     "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
-by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
+lemma (in comm_monoid_add) setsum_reindex_id:
+  "inj_on f B ==> setsum f B = setsum id (f ` B)"
+  by (simp add: setsum_reindex)
 
-lemma setsum_reindex_id:
-     "inj_on f B ==> setsum f B = setsum id (f ` B)"
-by (auto simp add: setsum_reindex)
-
-lemma setsum_reindex_nonzero: 
+lemma (in comm_monoid_add) setsum_reindex_nonzero: 
   assumes fS: "finite S"
   and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
   shows "setsum h (f ` S) = setsum (h o f) S"
@@ -98,8 +133,8 @@
     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
     also have "\<dots> = setsum (h o f) (insert x F)" 
-      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
-      using h0 
+      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
+      using h0
       apply simp
       apply (rule "2.hyps"(3))
       apply (rule_tac y="y" in  "2.prems")
@@ -111,9 +146,9 @@
     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
       using fxF "2.hyps" by simp 
     also have "\<dots> = setsum (h o f) (insert x F)"
-      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
+      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
       apply simp
-      apply (rule cong[OF refl[of "op + (h (f x))"]])
+      apply (rule cong [OF refl [of "op + (h (f x))"]])
       apply (rule "2.hyps"(3))
       apply (rule_tac y="y" in  "2.prems")
       apply simp_all
@@ -122,40 +157,37 @@
   ultimately show ?case by blast
 qed
 
-lemma setsum_cong:
+lemma (in comm_monoid_add) setsum_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
-by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
+  by (cases "finite A") (auto intro: setsum.cong)
 
-lemma strong_setsum_cong[cong]:
+lemma (in comm_monoid_add) strong_setsum_cong [cong]:
   "A = B ==> (!!x. x:B =simp=> f x = g x)
    ==> setsum (%x. f x) A = setsum (%x. g x) B"
-by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
+  by (rule setsum_cong) (simp_all add: simp_implies_def)
 
-lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
-by (rule setsum_cong[OF refl], auto)
+lemma (in comm_monoid_add) setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
+  by (auto intro: setsum_cong)
 
-lemma setsum_reindex_cong:
+lemma (in comm_monoid_add) setsum_reindex_cong:
    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
     ==> setsum h B = setsum g A"
-by (simp add: setsum_reindex cong: setsum_cong)
+  by (simp add: setsum_reindex cong: setsum_cong)
 
+lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
+  by (cases "finite A") (erule finite_induct, auto)
 
-lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
-apply (clarsimp simp: setsum_def)
-apply (erule finite_induct, auto)
-done
+lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
+  by (simp add:setsum_cong)
 
-lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
-by(simp add:setsum_cong)
-
-lemma setsum_Un_Int: "finite A ==> finite B ==>
+lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
+  by (fact setsum.union_inter)
 
-lemma setsum_Un_disjoint: "finite A ==> finite B
+lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B
   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
-by (subst setsum_Un_Int [symmetric], auto)
+  by (fact setsum.union_disjoint)
 
 lemma setsum_mono_zero_left: 
   assumes fT: "finite T" and ST: "S \<subseteq> T"
@@ -250,11 +282,14 @@
 
 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   the lhs need not be, since UNION I A could still be finite.*)
-lemma setsum_UN_disjoint:
-    "finite I ==> (ALL i:I. finite (A i)) ==>
-        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
-      setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
-by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
+lemma (in comm_monoid_add) setsum_UN_disjoint:
+  assumes "finite I" and "ALL i:I. finite (A i)"
+    and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
+  shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
+proof -
+  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint cong: setsum_cong)
+qed
 
 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
@@ -270,9 +305,13 @@
 
 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   the rhs need not be, since SIGMA A B could still be finite.*)
-lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
-    (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
-by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
+lemma (in comm_monoid_add) setsum_Sigma:
+  assumes "finite A" and  "ALL x:A. finite (B x)"
+  shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
+proof -
+  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def cong: setsum_cong)
+qed
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
 lemma setsum_cartesian_product: 
@@ -286,8 +325,8 @@
             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
 done
 
-lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
-by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
+lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
+  by (cases "finite A") (simp_all add: setsum.distrib)
 
 
 subsubsection {* Properties in more restricted classes of structures *}
@@ -321,43 +360,34 @@
    setsum f A + setsum f B - setsum f (A Int B)"
 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
 
-lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
-  apply (induct set: finite)
-  apply simp by auto
-
-lemma (in comm_monoid_mult) fold_image_Un_one:
-  assumes fS: "finite S" and fT: "finite T"
-  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
-  shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
-proof-
-  have "fold_image op * f 1 (S \<inter> T) = 1" 
-    apply (rule fold_image_1)
-    using fS fT I0 by auto 
-  with fold_image_Un_Int[OF fS fT] show ?thesis by simp
-qed
-
-lemma setsum_eq_general_reverses:
+lemma (in comm_monoid_add) setsum_eq_general_reverses:
   assumes fS: "finite S" and fT: "finite T"
   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
   shows "setsum f S = setsum g T"
+proof -
+  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+  show ?thesis
   apply (simp add: setsum_def fS fT)
-  apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
+  apply (rule fold_image_eq_general_inverses)
+  apply (rule fS)
   apply (erule kh)
   apply (erule hk)
   done
-
+qed
 
-
-lemma setsum_Un_zero:  
+lemma (in comm_monoid_add) setsum_Un_zero:  
   assumes fS: "finite S" and fT: "finite T"
   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
+proof -
+  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+  show ?thesis
   using fS fT
   apply (simp add: setsum_def)
-  apply (rule comm_monoid_add.fold_image_Un_one)
+  apply (rule fold_image_Un_one)
   using I0 by auto
-
+qed
 
 lemma setsum_UNION_zero: 
   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
@@ -376,7 +406,6 @@
     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
 qed
 
-
 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   (if a:A then setsum f A - f a else setsum f A)"
 apply (case_tac "finite A")
@@ -651,7 +680,6 @@
   case False thus ?thesis by (simp add: setsum_def)
 qed
 
-
 lemma setsum_Plus:
   fixes A :: "'a set" and B :: "'b set"
   assumes fin: "finite A" "finite B"
@@ -668,14 +696,6 @@
 
 text {* Commuting outer and inner summation *}
 
-lemma swap_inj_on:
-  "inj_on (%(i, j). (j, i)) (A \<times> B)"
-  by (unfold inj_on_def) fast
-
-lemma swap_product:
-  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
-  by (simp add: split_def image_def) blast
-
 lemma setsum_commute:
   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
 proof (simp add: setsum_cartesian_product)
@@ -781,8 +801,11 @@
 
 subsection {* Generalized product over a set *}
 
-definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
-where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
+definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
+  "setprod f A = (if finite A then fold_image (op *) f 1 A else 1)"
+
+sublocale comm_monoid_add < setprod!: comm_monoid_big "op *" 1 setprod proof
+qed (fact setprod_def)
 
 abbreviation
   Setprod  ("\<Prod>_" [1000] 999) where
@@ -813,16 +836,15 @@
   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
 
-
-lemma setprod_empty [simp]: "setprod f {} = 1"
-by (auto simp add: setprod_def)
+lemma setprod_empty: "setprod f {} = 1"
+  by (fact setprod.empty)
 
-lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
+lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
     setprod f (insert a A) = f a * setprod f A"
-by (simp add: setprod_def)
+  by (fact setprod.insert)
 
-lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
-by (simp add: setprod_def)
+lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
+  by (fact setprod.infinite)
 
 lemma setprod_reindex:
    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
@@ -1123,17 +1145,63 @@
 qed
 
 
-subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
+subsection {* Versions of @{const inf} and @{const sup} on non-empty sets *}
+
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
+
+locale semilattice_big = semilattice +
+  fixes F :: "'a set \<Rightarrow> 'a"
+  assumes F_eq: "finite A \<Longrightarrow> F A = fold1 (op *) A"
+
+sublocale semilattice_big < folding_one_idem proof
+qed (simp_all add: F_eq)
+
+notation times (infixl "*" 70)
+notation Groups.one ("1")
 
-text{*
-  As an application of @{text fold1} we define infimum
-  and supremum in (not necessarily complete!) lattices
-  over (non-empty) sets by means of @{text fold1}.
-*}
+context lattice
+begin
+
+definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) where
+  "Inf_fin = fold1 inf"
+
+definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) where
+  "Sup_fin = fold1 sup"
+
+end
+
+sublocale lattice < Inf_fin!: semilattice_big inf Inf_fin proof
+qed (simp add: Inf_fin_def)
+
+sublocale lattice < Sup_fin!: semilattice_big sup Sup_fin proof
+qed (simp add: Sup_fin_def)
 
 context semilattice_inf
 begin
 
+lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+proof qed (rule inf_assoc inf_commute inf_idem)+
+
+lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
+by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
+
+lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
+by (induct pred: finite) (auto intro: le_infI1)
+
+lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
+proof(induct arbitrary: a pred:finite)
+  case empty thus ?case by simp
+next
+  case (insert x A)
+  show ?case
+  proof cases
+    assume "A = {}" thus ?thesis using insert by simp
+  next
+    assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
+  qed
+qed
+
 lemma below_fold1_iff:
   assumes "finite A" "A \<noteq> {}"
   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
@@ -1179,18 +1247,25 @@
 
 end
 
-context lattice
+context semilattice_sup
 begin
 
-definition
-  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
-where
-  "Inf_fin = fold1 inf"
+lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
+
+lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
+by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
 
-definition
-  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
-where
-  "Sup_fin = fold1 sup"
+lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
+by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
+
+lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
+by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
+
+end
+
+context lattice
+begin
 
 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
 apply(unfold Sup_fin_def Inf_fin_def)
@@ -1342,17 +1417,58 @@
 end
 
 
-subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
+subsection {* Versions of @{const min} and @{const max} on non-empty sets *}
+
+definition (in linorder) Min :: "'a set \<Rightarrow> 'a" where
+  "Min = fold1 min"
 
-text{*
-  As an application of @{text fold1} we define minimum
-  and maximum in (not necessarily complete!) linear orders
-  over (non-empty) sets by means of @{text fold1}.
-*}
+definition (in linorder) Max :: "'a set \<Rightarrow> 'a" where
+  "Max = fold1 max"
+
+sublocale linorder < Min!: semilattice_big min Min proof
+qed (simp add: Min_def)
+
+sublocale linorder < Max!: semilattice_big max Max proof
+qed (simp add: Max_def)
 
 context linorder
 begin
 
+lemmas Min_singleton = Min.singleton
+lemmas Max_singleton = Max.singleton
+
+lemma Min_insert:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Min (insert x A) = min x (Min A)"
+  using assms by simp
+
+lemma Max_insert:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Max (insert x A) = max x (Max A)"
+  using assms by simp
+
+lemma Min_Un:
+  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
+  shows "Min (A \<union> B) = min (Min A) (Min B)"
+  using assms by (rule Min.union_idem)
+
+lemma Max_Un:
+  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
+  shows "Max (A \<union> B) = max (Max A) (Max B)"
+  using assms by (rule Max.union_idem)
+
+lemma hom_Min_commute:
+  assumes "\<And>x y. h (min x y) = min (h x) (h y)"
+    and "finite N" and "N \<noteq> {}"
+  shows "h (Min N) = Min (h ` N)"
+  using assms by (rule Min.hom_commute)
+
+lemma hom_Max_commute:
+  assumes "\<And>x y. h (max x y) = max (h x) (h y)"
+    and "finite N" and "N \<noteq> {}"
+  shows "h (Max N) = Max (h ` N)"
+  using assms by (rule Max.hom_commute)
+
 lemma ab_semigroup_idem_mult_min:
   "ab_semigroup_idem_mult min"
   proof qed (auto simp add: min_def)
@@ -1429,37 +1545,6 @@
   finally show ?thesis .
 qed
 
-definition
-  Min :: "'a set \<Rightarrow> 'a"
-where
-  "Min = fold1 min"
-
-definition
-  Max :: "'a set \<Rightarrow> 'a"
-where
-  "Max = fold1 max"
-
-lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
-lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
-
-lemma Min_insert [simp]:
-  assumes "finite A" and "A \<noteq> {}"
-  shows "Min (insert x A) = min x (Min A)"
-proof -
-  interpret ab_semigroup_idem_mult min
-    by (rule ab_semigroup_idem_mult_min)
-  from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
-qed
-
-lemma Max_insert [simp]:
-  assumes "finite A" and "A \<noteq> {}"
-  shows "Max (insert x A) = max x (Max A)"
-proof -
-  interpret ab_semigroup_idem_mult max
-    by (rule ab_semigroup_idem_mult_max)
-  from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
-qed
-
 lemma Min_in [simp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<in> A"
@@ -1478,48 +1563,6 @@
   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
 qed
 
-lemma Min_Un:
-  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
-  shows "Min (A \<union> B) = min (Min A) (Min B)"
-proof -
-  interpret ab_semigroup_idem_mult min
-    by (rule ab_semigroup_idem_mult_min)
-  from assms show ?thesis
-    by (simp add: Min_def fold1_Un2)
-qed
-
-lemma Max_Un:
-  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
-  shows "Max (A \<union> B) = max (Max A) (Max B)"
-proof -
-  interpret ab_semigroup_idem_mult max
-    by (rule ab_semigroup_idem_mult_max)
-  from assms show ?thesis
-    by (simp add: Max_def fold1_Un2)
-qed
-
-lemma hom_Min_commute:
-  assumes "\<And>x y. h (min x y) = min (h x) (h y)"
-    and "finite N" and "N \<noteq> {}"
-  shows "h (Min N) = Min (h ` N)"
-proof -
-  interpret ab_semigroup_idem_mult min
-    by (rule ab_semigroup_idem_mult_min)
-  from assms show ?thesis
-    by (simp add: Min_def hom_fold1_commute)
-qed
-
-lemma hom_Max_commute:
-  assumes "\<And>x y. h (max x y) = max (h x) (h y)"
-    and "finite N" and "N \<noteq> {}"
-  shows "h (Max N) = Max (h ` N)"
-proof -
-  interpret ab_semigroup_idem_mult max
-    by (rule ab_semigroup_idem_mult_max)
-  from assms show ?thesis
-    by (simp add: Max_def hom_fold1_commute [of h])
-qed
-
 lemma Min_le [simp]:
   assumes "finite A" and "x \<in> A"
   shows "Min A \<le> x"
diff -r 10e723e54076 -r b766aad9136d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 18 13:57:00 2010 +0100
@@ -9,7 +9,7 @@
 imports Power Option
 begin
 
-subsection {* Definition and basic properties *}
+subsection {* Predicate for finite sets *}
 
 inductive finite :: "'a set => bool"
   where
@@ -171,8 +171,7 @@
 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
 by(fastsimp simp: finite_conv_nat_seg_image)
 
-
-subsubsection{* Finiteness and set theoretic constructions *}
+text {* Finiteness and set theoretic constructions *}
 
 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
 by (induct set: finite) simp_all
@@ -567,7 +566,7 @@
 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
 
 
-subsection {* A fold functional for finite sets *}
+subsection {* A basic fold functional for finite sets *}
 
 text {* The intended behaviour is
 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
@@ -826,63 +825,122 @@
 
 end
 
-context ab_semigroup_idem_mult
-begin
+
+subsubsection {* Expressing set operations via @{const fold} *}
+
+lemma (in fun_left_comm) fun_left_comm_apply:
+  "fun_left_comm (\<lambda>x. f (g x))"
+proof
+qed (simp_all add: fun_left_comm)
+
+lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
+  "fun_left_comm_idem (\<lambda>x. f (g x))"
+  by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
+    (simp_all add: fun_left_idem)
+
+lemma fun_left_comm_idem_insert:
+  "fun_left_comm_idem insert"
+proof
+qed auto
+
+lemma fun_left_comm_idem_remove:
+  "fun_left_comm_idem (\<lambda>x A. A - {x})"
+proof
+qed auto
 
-lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
-apply unfold_locales
- apply (rule mult_left_commute)
-apply (rule mult_left_idem)
-done
+lemma (in semilattice_inf) fun_left_comm_idem_inf:
+  "fun_left_comm_idem inf"
+proof
+qed (auto simp add: inf_left_commute)
+
+lemma (in semilattice_sup) fun_left_comm_idem_sup:
+  "fun_left_comm_idem sup"
+proof
+qed (auto simp add: sup_left_commute)
 
-end
+lemma union_fold_insert:
+  assumes "finite A"
+  shows "A \<union> B = fold insert B A"
+proof -
+  interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
+  from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
+qed
 
-context semilattice_inf
+lemma minus_fold_remove:
+  assumes "finite A"
+  shows "B - A = fold (\<lambda>x A. A - {x}) B A"
+proof -
+  interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
+  from `finite A` show ?thesis by (induct A arbitrary: B) auto
+qed
+
+context complete_lattice
 begin
 
-lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
-proof qed (rule inf_assoc inf_commute inf_idem)+
-
-lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
-by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
-
-lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
-by (induct pred: finite) (auto intro: le_infI1)
+lemma inf_Inf_fold_inf:
+  assumes "finite A"
+  shows "inf B (Inf A) = fold inf B A"
+proof -
+  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+  from `finite A` show ?thesis by (induct A arbitrary: B)
+    (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
+qed
 
-lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
-proof(induct arbitrary: a pred:finite)
-  case empty thus ?case by simp
-next
-  case (insert x A)
-  show ?case
-  proof cases
-    assume "A = {}" thus ?thesis using insert by simp
-  next
-    assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
-  qed
+lemma sup_Sup_fold_sup:
+  assumes "finite A"
+  shows "sup B (Sup A) = fold sup B A"
+proof -
+  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+  from `finite A` show ?thesis by (induct A arbitrary: B)
+    (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
 qed
 
-end
+lemma Inf_fold_inf:
+  assumes "finite A"
+  shows "Inf A = fold inf top A"
+  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
+
+lemma Sup_fold_sup:
+  assumes "finite A"
+  shows "Sup A = fold sup bot A"
+  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
 
-context semilattice_sup
-begin
-
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
-by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
+lemma inf_INFI_fold_inf:
+  assumes "finite A"
+  shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
+proof (rule sym)
+  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+  interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
+  from `finite A` show "?fold = ?inf"
+  by (induct A arbitrary: B)
+    (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
+qed
 
-lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
-by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
+lemma sup_SUPR_fold_sup:
+  assumes "finite A"
+  shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
+proof (rule sym)
+  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+  interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
+  from `finite A` show "?fold = ?sup"
+  by (induct A arbitrary: B)
+    (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
+qed
 
-lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
-by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
+lemma INFI_fold_inf:
+  assumes "finite A"
+  shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
+  using assms inf_INFI_fold_inf [of A top] by simp
 
-lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
-by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
+lemma SUPR_fold_sup:
+  assumes "finite A"
+  shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
+  using assms sup_SUPR_fold_sup [of A bot] by simp
 
 end
 
 
-subsubsection{* The derived combinator @{text fold_image} *}
+subsection {* The derived combinator @{text fold_image} *}
 
 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
 where "fold_image f g = fold (%x y. f (g x) y)"
@@ -969,6 +1027,11 @@
 context comm_monoid_mult
 begin
 
+lemma fold_image_1:
+  "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
+  apply (induct set: finite)
+  apply simp by auto
+
 lemma fold_image_Un_Int:
   "finite A ==> finite B ==>
     fold_image times g 1 A * fold_image times g 1 B =
@@ -976,6 +1039,17 @@
 by (induct set: finite) 
    (auto simp add: mult_ac insert_absorb Int_insert_left)
 
+lemma fold_image_Un_one:
+  assumes fS: "finite S" and fT: "finite T"
+  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
+  shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
+proof-
+  have "fold_image op * f 1 (S \<inter> T) = 1" 
+    apply (rule fold_image_1)
+    using fS fT I0 by auto 
+  with fold_image_Un_Int[OF fS fT] show ?thesis by simp
+qed
+
 corollary fold_Un_disjoint:
   "finite A ==> finite B ==> A Int B = {} ==>
    fold_image times g 1 (A Un B) =
@@ -1061,7 +1135,7 @@
 end
 
 
-subsection{* A fold functional for non-empty sets *}
+subsection {* A fold functional for non-empty sets *}
 
 text{* Does not require start value. *}
 
@@ -1187,6 +1261,12 @@
 context ab_semigroup_idem_mult
 begin
 
+lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
+apply unfold_locales
+ apply (rule mult_left_commute)
+apply (rule mult_left_idem)
+done
+
 lemma fold1_insert_idem [simp]:
   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   shows "fold1 times (insert x A) = x * fold1 times A"
@@ -1354,138 +1434,17 @@
 qed
 
 
-subsection {* Expressing set operations via @{const fold} *}
-
-lemma (in fun_left_comm) fun_left_comm_apply:
-  "fun_left_comm (\<lambda>x. f (g x))"
-proof
-qed (simp_all add: fun_left_comm)
-
-lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
-  "fun_left_comm_idem (\<lambda>x. f (g x))"
-  by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
-    (simp_all add: fun_left_idem)
-
-lemma fun_left_comm_idem_insert:
-  "fun_left_comm_idem insert"
-proof
-qed auto
-
-lemma fun_left_comm_idem_remove:
-  "fun_left_comm_idem (\<lambda>x A. A - {x})"
-proof
-qed auto
-
-lemma (in semilattice_inf) fun_left_comm_idem_inf:
-  "fun_left_comm_idem inf"
-proof
-qed (auto simp add: inf_left_commute)
-
-lemma (in semilattice_sup) fun_left_comm_idem_sup:
-  "fun_left_comm_idem sup"
-proof
-qed (auto simp add: sup_left_commute)
-
-lemma union_fold_insert:
-  assumes "finite A"
-  shows "A \<union> B = fold insert B A"
-proof -
-  interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
-  from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
-qed
-
-lemma minus_fold_remove:
-  assumes "finite A"
-  shows "B - A = fold (\<lambda>x A. A - {x}) B A"
-proof -
-  interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
-  from `finite A` show ?thesis by (induct A arbitrary: B) auto
-qed
-
-context complete_lattice
-begin
+subsection {* Locales as mini-packages for fold operations *}
 
-lemma inf_Inf_fold_inf:
-  assumes "finite A"
-  shows "inf B (Inf A) = fold inf B A"
-proof -
-  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
-  from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
-qed
-
-lemma sup_Sup_fold_sup:
-  assumes "finite A"
-  shows "sup B (Sup A) = fold sup B A"
-proof -
-  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
-  from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
-qed
-
-lemma Inf_fold_inf:
-  assumes "finite A"
-  shows "Inf A = fold inf top A"
-  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
-
-lemma Sup_fold_sup:
-  assumes "finite A"
-  shows "Sup A = fold sup bot A"
-  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
-
-lemma inf_INFI_fold_inf:
-  assumes "finite A"
-  shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
-proof (rule sym)
-  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
-  interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
-  from `finite A` show "?fold = ?inf"
-  by (induct A arbitrary: B)
-    (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
-qed
-
-lemma sup_SUPR_fold_sup:
-  assumes "finite A"
-  shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
-proof (rule sym)
-  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
-  interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
-  from `finite A` show "?fold = ?sup"
-  by (induct A arbitrary: B)
-    (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
-qed
-
-lemma INFI_fold_inf:
-  assumes "finite A"
-  shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
-  using assms inf_INFI_fold_inf [of A top] by simp
-
-lemma SUPR_fold_sup:
-  assumes "finite A"
-  shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
-  using assms sup_SUPR_fold_sup [of A bot] by simp
-
-end
-
-
-subsection {* Locales as mini-packages *}
+subsubsection {* The natural case *}
 
 locale folding =
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b"
-  assumes commute_comp: "f x \<circ> f y = f y \<circ> f x"
+  assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
   assumes eq_fold: "finite A \<Longrightarrow> F A s = fold f s A"
 begin
 
-lemma fun_left_commute:
-  "f x (f y s) = f y (f x s)"
-  using commute_comp [of x y] by (simp add: expand_fun_eq)
-
-lemma fun_left_comm:
-  "fun_left_comm f"
-proof
-qed (fact fun_left_commute)
-
 lemma empty [simp]:
   "F {} = id"
   by (simp add: eq_fold expand_fun_eq)
@@ -1494,7 +1453,8 @@
   assumes "finite A" and "x \<notin> A"
   shows "F (insert x A) = F A \<circ> f x"
 proof -
-  interpret fun_left_comm f by (fact fun_left_comm)
+  interpret fun_left_comm f proof
+  qed (insert commute_comp, simp add: expand_fun_eq)
   from fold_insert2 assms
   have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
   with `finite A` show ?thesis by (simp add: eq_fold expand_fun_eq)
@@ -1515,89 +1475,112 @@
   shows "F (insert x A) = F (A - {x}) \<circ> f x"
   using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
 
+lemma commute_left_comp:
+  "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
+  by (simp add: o_assoc commute_comp)
+
 lemma commute_comp':
   assumes "finite A"
   shows "f x \<circ> F A = F A \<circ> f x"
-proof (rule ext)
-  fix s
-  from assms show "(f x \<circ> F A) s = (F A \<circ> f x) s"
-    by (induct A arbitrary: s) (simp_all add: fun_left_commute)
-qed
+  using assms by (induct A)
+    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] commute_comp)
+
+lemma commute_left_comp':
+  assumes "finite A"
+  shows "f x \<circ> (F A \<circ> g) = F A \<circ> (f x \<circ> g)"
+  using assms by (simp add: o_assoc commute_comp')
+
+lemma commute_comp'':
+  assumes "finite A" and "finite B"
+  shows "F B \<circ> F A = F A \<circ> F B"
+  using assms by (induct A)
+    (simp_all add: o_assoc, simp add: o_assoc [symmetric] commute_comp')
 
-lemma fun_left_commute':
-  assumes "finite A"
-  shows "f x (F A s) = F A (f x s)"
-  using commute_comp' assms by (simp add: expand_fun_eq)
+lemma commute_left_comp'':
+  assumes "finite A" and "finite B"
+  shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
+  using assms by (simp add: o_assoc commute_comp'')
+
+lemmas commute_comps = o_assoc [symmetric] commute_comp commute_left_comp
+  commute_comp' commute_left_comp' commute_comp'' commute_left_comp''
+
+lemma union_inter:
+  assumes "finite A" and "finite B"
+  shows "F (A \<union> B) \<circ> F (A \<inter> B) = F A \<circ> F B"
+  using assms by (induct A)
+    (simp_all del: o_apply add: insert_absorb Int_insert_left commute_comps,
+      simp add: o_assoc)
 
 lemma union:
   assumes "finite A" and "finite B"
   and "A \<inter> B = {}"
   shows "F (A \<union> B) = F A \<circ> F B"
-using `finite A` `A \<inter> B = {}` proof (induct A)
-  case empty show ?case by simp
-next
-  case (insert x A)
-  then have "A \<inter> B = {}" by auto
-  with insert(3) have "F (A \<union> B) = F A \<circ> F B" .
-  moreover from insert have "x \<notin> B" by simp
-  moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
-  moreover from `x \<notin> A` `x \<notin> B` have "x \<notin> A \<union> B" by simp
-  ultimately show ?case by (simp add: fun_left_commute')
+proof -
+  from union_inter `finite A` `finite B` have "F (A \<union> B) \<circ> F (A \<inter> B) = F A \<circ> F B" .
+  with `A \<inter> B = {}` show ?thesis by simp
 qed
 
 end
 
+
+subsubsection {* The natural case with idempotency *}
+
 locale folding_idem = folding +
   assumes idem_comp: "f x \<circ> f x = f x"
 begin
 
-declare insert [simp del]
+lemma idem_left_comp:
+  "f x \<circ> (f x \<circ> g) = f x \<circ> g"
+  by (simp add: o_assoc idem_comp)
+
+lemma in_comp_idem:
+  assumes "finite A" and "x \<in> A"
+  shows "F A \<circ> f x = F A"
+using assms by (induct A)
+  (auto simp add: commute_comps idem_comp, simp add: commute_left_comp' [symmetric] commute_comp')
 
-lemma fun_idem:
-  "f x (f x s) = f x s"
-  using idem_comp [of x] by (simp add: expand_fun_eq)
+lemma subset_comp_idem:
+  assumes "finite A" and "B \<subseteq> A"
+  shows "F A \<circ> F B = F A"
+proof -
+  from assms have "finite B" by (blast dest: finite_subset)
+  then show ?thesis using `B \<subseteq> A` by (induct B)
+    (simp_all add: o_assoc in_comp_idem `finite A`)
+qed
 
-lemma fun_left_comm_idem:
-  "fun_left_comm_idem f"
-proof
-qed (fact fun_left_commute fun_idem)+
+declare insert [simp del]
 
 lemma insert_idem [simp]:
   assumes "finite A"
   shows "F (insert x A) = F A \<circ> f x"
-proof -
-  interpret fun_left_comm_idem f by (fact fun_left_comm_idem)
-  from fold_insert_idem2 assms
-  have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
-  with assms show ?thesis by (simp add: eq_fold expand_fun_eq)
-qed
+  using assms by (cases "x \<in> A") (simp_all add: insert in_comp_idem insert_absorb)
 
 lemma union_idem:
   assumes "finite A" and "finite B"
   shows "F (A \<union> B) = F A \<circ> F B"
-using `finite A` proof (induct A)
-  case empty show ?case by simp
-next
-  case (insert x A)
-  from insert(3) have "F (A \<union> B) = F A \<circ> F B" .
-  moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
-  ultimately show ?case by (simp add: fun_left_commute')
+proof -
+  from assms have "finite (A \<union> B)" and "A \<inter> B \<subseteq> A \<union> B" by auto
+  then have "F (A \<union> B) \<circ> F (A \<inter> B) = F (A \<union> B)" by (rule subset_comp_idem)
+  with assms show ?thesis by (simp add: union_inter)
 qed
 
 end
 
+
+subsubsection {* The image case with fixed function *}
+
 no_notation times (infixl "*" 70)
 no_notation Groups.one ("1")
 
 locale folding_image_simple = comm_monoid +
   fixes g :: "('b \<Rightarrow> 'a)"
   fixes F :: "'b set \<Rightarrow> 'a"
-  assumes eq_fold: "finite A \<Longrightarrow> F A = fold_image f g 1 A"
+  assumes eq_fold_g: "finite A \<Longrightarrow> F A = fold_image f g 1 A"
 begin
 
 lemma empty [simp]:
   "F {} = 1"
-  by (simp add: eq_fold)
+  by (simp add: eq_fold_g)
 
 lemma insert [simp]:
   assumes "finite A" and "x \<notin> A"
@@ -1607,7 +1590,7 @@
   qed (simp add: ac_simps)
   with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
     by (simp add: fold_image_def)
-  with `finite A` show ?thesis by (simp add: eq_fold)
+  with `finite A` show ?thesis by (simp add: eq_fold_g)
 qed
 
 lemma remove:
@@ -1625,9 +1608,14 @@
   shows "F (insert x A) = g x * F (A - {x})"
   using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
 
+lemma neutral:
+  assumes "finite A" and "\<forall>x\<in>A. g x = 1"
+  shows "F A = 1"
+  using assms by (induct A) simp_all
+
 lemma union_inter:
   assumes "finite A" and "finite B"
-  shows "F A * F B = F (A \<union> B) * F (A \<inter> B)"
+  shows "F (A \<union> B) * F (A \<inter> B) = F A * F B"
 using assms proof (induct A)
   case empty then show ?case by simp
 next
@@ -1635,14 +1623,23 @@
     by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
 qed
 
+corollary union_inter_neutral:
+  assumes "finite A" and "finite B"
+  and I0: "\<forall>x \<in> A\<inter>B. g x = 1"
+  shows "F (A \<union> B) = F A * F B"
+  using assms by (simp add: union_inter [symmetric] neutral)
+
 corollary union_disjoint:
   assumes "finite A" and "finite B"
   assumes "A \<inter> B = {}"
   shows "F (A \<union> B) = F A * F B"
-  using assms by (simp add: union_inter)
+  using assms by (simp add: union_inter_neutral)
 
 end
 
+
+subsubsection {* The image case with flexible function *}
+
 locale folding_image = comm_monoid +
   fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   assumes eq_fold: "\<And>g. finite A \<Longrightarrow> F g A = fold_image f g 1 A"
@@ -1653,7 +1650,7 @@
 context folding_image
 begin
 
-lemma reindex:
+lemma reindex: (* FIXME polymorhism *)
   assumes "finite A" and "inj_on h A"
   shows "F g (h ` A) = F (g \<circ> h) A"
   using assms by (induct A) auto
@@ -1742,6 +1739,229 @@
 
 end
 
+
+subsubsection {* The image case with fixed function and idempotency *}
+
+locale folding_image_simple_idem = folding_image_simple +
+  assumes idem: "x * x = x"
+
+sublocale folding_image_simple_idem < semilattice proof
+qed (fact idem)
+
+context folding_image_simple_idem
+begin
+
+lemma in_idem:
+  assumes "finite A" and "x \<in> A"
+  shows "g x * F A = F A"
+  using assms by (induct A) (auto simp add: left_commute)
+
+lemma subset_idem:
+  assumes "finite A" and "B \<subseteq> A"
+  shows "F B * F A = F A"
+proof -
+  from assms have "finite B" by (blast dest: finite_subset)
+  then show ?thesis using `B \<subseteq> A` by (induct B)
+    (auto simp add: assoc in_idem `finite A`)
+qed
+
+declare insert [simp del]
+
+lemma insert_idem [simp]:
+  assumes "finite A"
+  shows "F (insert x A) = g x * F A"
+  using assms by (cases "x \<in> A") (simp_all add: insert in_idem insert_absorb)
+
+lemma union_idem:
+  assumes "finite A" and "finite B"
+  shows "F (A \<union> B) = F A * F B"
+proof -
+  from assms have "finite (A \<union> B)" and "A \<inter> B \<subseteq> A \<union> B" by auto
+  then have "F (A \<inter> B) * F (A \<union> B) = F (A \<union> B)" by (rule subset_idem)
+  with assms show ?thesis by (simp add: union_inter [of A B, symmetric] commute)
+qed
+
+end
+
+
+subsubsection {* The image case with flexible function and idempotency *}
+
+locale folding_image_idem = folding_image +
+  assumes idem: "x * x = x"
+
+sublocale folding_image_idem < folding_image_simple_idem "op *" 1 g "F g" proof
+qed (fact idem)
+
+
+subsubsection {* The neutral-less case *}
+
+locale folding_one = abel_semigroup +
+  fixes F :: "'a set \<Rightarrow> 'a"
+  assumes eq_fold: "finite A \<Longrightarrow> F A = fold1 f A"
+begin
+
+lemma singleton [simp]:
+  "F {x} = x"
+  by (simp add: eq_fold)
+
+lemma eq_fold':
+  assumes "finite A" and "x \<notin> A"
+  shows "F (insert x A) = fold (op *) x A"
+proof -
+  interpret ab_semigroup_mult "op *" proof qed (simp_all add: ac_simps)
+  with assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
+qed
+
+lemma insert [simp]:
+  assumes "finite A" and "x \<notin> A"
+  shows "F (insert x A) = (if A = {} then x else x * F A)"
+proof (cases "A = {}")
+  case True then show ?thesis by simp
+next
+  case False then obtain b where "b \<in> A" by blast
+  then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
+  with `finite A` have "finite B" by simp
+  interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
+  qed (simp_all add: expand_fun_eq ac_simps)
+  thm fold.commute_comp' [of B b, simplified expand_fun_eq, simplified]
+  from `finite B` fold.commute_comp' [of B x]
+    have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp
+  then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: expand_fun_eq commute)
+  from `finite B` * fold.insert [of B b]
+    have "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> op * b" by simp
+  then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: expand_fun_eq)
+  from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert)
+qed
+
+lemma remove:
+  assumes "finite A" and "x \<in> A"
+  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
+proof -
+  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
+  with assms show ?thesis by simp
+qed
+
+lemma insert_remove:
+  assumes "finite A"
+  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
+  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
+
+lemma union_disjoint:
+  assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}" and "A \<inter> B = {}"
+  shows "F (A \<union> B) = F A * F B"
+  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
+
+lemma union_inter:
+  assumes "finite A" and "finite B" and "A \<inter> B \<noteq> {}"
+  shows "F (A \<union> B) * F (A \<inter> B) = F A * F B"
+proof -
+  from assms have "A \<noteq> {}" and "B \<noteq> {}" by auto
+  from `finite A` `A \<noteq> {}` `A \<inter> B \<noteq> {}` show ?thesis proof (induct A rule: finite_ne_induct)
+    case (singleton x) then show ?case by (simp add: insert_absorb ac_simps)
+  next
+    case (insert x A) show ?case proof (cases "x \<in> B")
+      case True then have "B \<noteq> {}" by auto
+      with insert True `finite B` show ?thesis by (cases "A \<inter> B = {}")
+        (simp_all add: insert_absorb ac_simps union_disjoint)
+    next
+      case False with insert have "F (A \<union> B) * F (A \<inter> B) = F A * F B" by simp
+      moreover from False `finite B` insert have "finite (A \<union> B)" "x \<notin> A \<union> B" "A \<union> B \<noteq> {}"
+        by auto
+      ultimately show ?thesis using False `finite A` `x \<notin> A` `A \<noteq> {}` by (simp add: assoc)
+    qed
+  qed
+qed
+
+lemma closed:
+  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
+  shows "F A \<in> A"
+using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
+  case singleton then show ?case by simp
+next
+  case insert with elem show ?case by force
+qed
+
+end
+
+
+subsubsection {* The neutral-less case with idempotency *}
+
+locale folding_one_idem = folding_one +
+  assumes idem: "x * x = x"
+
+sublocale folding_one_idem < semilattice proof
+qed (fact idem)
+
+context folding_one_idem
+begin
+
+lemma in_idem:
+  assumes "finite A" and "x \<in> A"
+  shows "x * F A = F A"
+proof -
+  from assms have "A \<noteq> {}" by auto
+  with `finite A` show ?thesis using `x \<in> A` by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
+qed
+
+lemma subset_idem:
+  assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
+  shows "F B * F A = F A"
+proof -
+  from assms have "finite B" by (blast dest: finite_subset)
+  then show ?thesis using `B \<noteq> {}` `B \<subseteq> A` by (induct B rule: finite_ne_induct)
+    (simp_all add: assoc in_idem `finite A`)
+qed
+
+declare insert [simp del]
+
+lemma eq_fold_idem':
+  assumes "finite A"
+  shows "F (insert a A) = fold (op *) a A"
+proof -
+  interpret ab_semigroup_idem_mult "op *" proof qed (simp_all add: ac_simps)
+  with assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
+qed
+
+lemma insert_idem [simp]:
+  assumes "finite A"
+  shows "F (insert x A) = (if A = {} then x else x * F A)"
+proof (cases "x \<in> A")
+  case False with `finite A` show ?thesis by (rule insert)
+next
+  case True then have "A \<noteq> {}" by auto
+  with `finite A` show ?thesis by (simp add: in_idem insert_absorb True)
+qed
+  
+lemma union_idem:
+  assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
+  shows "F (A \<union> B) = F A * F B"
+proof (cases "A \<inter> B = {}")
+  case True with assms show ?thesis by (simp add: union_disjoint)
+next
+  case False
+  from assms have "finite (A \<union> B)" and "A \<inter> B \<subseteq> A \<union> B" by auto
+  with False have "F (A \<inter> B) * F (A \<union> B) = F (A \<union> B)" by (auto intro: subset_idem)
+  with assms False show ?thesis by (simp add: union_inter [of A B, symmetric] commute)
+qed
+
+lemma hom_commute:
+  assumes hom: "\<And>x y. h (x * y) = h x * h y"
+  and N: "finite N" "N \<noteq> {}" shows "h (F N) = F (h ` N)"
+using N proof (induct rule: finite_ne_induct)
+  case singleton thus ?case by simp
+next
+  case (insert n N)
+  then have "h (F (insert n N)) = h (n * F N)" by simp
+  also have "\<dots> = h n * h (F N)" by (rule hom)
+  also have "h (F N) = F (h ` N)" by(rule insert)
+  also have "h n * \<dots> = F (insert (h n) (h ` N))"
+    using insert by(simp)
+  also have "insert (h n) (h ` N) = h ` insert n N" by simp
+  finally show ?case .
+qed
+
+end
+
 notation times (infixl "*" 70)
 notation Groups.one ("1")
 
@@ -1854,7 +2074,7 @@
 
 lemma card_Un_Int: "finite A ==> finite B
     ==> card A + card B = card (A Un B) + card (A Int B)"
-  by (fact card.union_inter)
+  by (fact card.union_inter [symmetric])
 
 lemma card_Un_disjoint: "finite A ==> finite B
     ==> A Int B = {} ==> card (A Un B) = card A + card B"
diff -r 10e723e54076 -r b766aad9136d src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Thu Mar 18 13:57:00 2010 +0100
@@ -1015,7 +1015,7 @@
   apply (subst foldseq_almostzero[of _ j])
   apply (simp add: assms)+
   apply (auto)
-  apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
+  apply (metis add_0 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
   done
 
 lemma mult_matrix_ext:
diff -r 10e723e54076 -r b766aad9136d src/HOL/Multivariate_Analysis/Integration.cert
--- a/src/HOL/Multivariate_Analysis/Integration.cert	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.cert	Thu Mar 18 13:57:00 2010 +0100
@@ -3506,3 +3506,215 @@
 #328 := [unit-resolution #319 #327]: #300
 [th-lemma #326 #334 #195 #328 #187 #138]: false
 unsat
+WrIjxhfF5EcRCmS6xKG3XQ 211 0
+#2 := false
+#33 := 0::real
+decl uf_11 :: (-> T5 T6 real)
+decl uf_15 :: T6
+#28 := uf_15
+decl uf_16 :: T5
+#30 := uf_16
+#31 := (uf_11 uf_16 uf_15)
+decl uf_12 :: (-> T7 T8 T5)
+decl uf_14 :: T8
+#26 := uf_14
+decl uf_13 :: (-> T1 T7)
+decl uf_8 :: T1
+#16 := uf_8
+#25 := (uf_13 uf_8)
+#27 := (uf_12 #25 uf_14)
+#29 := (uf_11 #27 uf_15)
+#73 := -1::real
+#84 := (* -1::real #29)
+#85 := (+ #84 #31)
+#74 := (* -1::real #31)
+#75 := (+ #29 #74)
+#112 := (>= #75 0::real)
+#119 := (ite #112 #75 #85)
+#127 := (* -1::real #119)
+decl uf_17 :: T5
+#37 := uf_17
+#38 := (uf_11 uf_17 uf_15)
+#102 := -1/3::real
+#103 := (* -1/3::real #38)
+#128 := (+ #103 #127)
+#100 := 1/3::real
+#101 := (* 1/3::real #31)
+#129 := (+ #101 #128)
+#130 := (<= #129 0::real)
+#131 := (not #130)
+#40 := 3::real
+#39 := (- #31 #38)
+#41 := (/ #39 3::real)
+#32 := (- #29 #31)
+#35 := (- #32)
+#34 := (< #32 0::real)
+#36 := (ite #34 #35 #32)
+#42 := (< #36 #41)
+#136 := (iff #42 #131)
+#104 := (+ #101 #103)
+#78 := (< #75 0::real)
+#90 := (ite #78 #85 #75)
+#109 := (< #90 #104)
+#134 := (iff #109 #131)
+#124 := (< #119 #104)
+#132 := (iff #124 #131)
+#133 := [rewrite]: #132
+#125 := (iff #109 #124)
+#122 := (= #90 #119)
+#113 := (not #112)
+#116 := (ite #113 #85 #75)
+#120 := (= #116 #119)
+#121 := [rewrite]: #120
+#117 := (= #90 #116)
+#114 := (iff #78 #113)
+#115 := [rewrite]: #114
+#118 := [monotonicity #115]: #117
+#123 := [trans #118 #121]: #122
+#126 := [monotonicity #123]: #125
+#135 := [trans #126 #133]: #134
+#110 := (iff #42 #109)
+#107 := (= #41 #104)
+#93 := (* -1::real #38)
+#94 := (+ #31 #93)
+#97 := (/ #94 3::real)
+#105 := (= #97 #104)
+#106 := [rewrite]: #105
+#98 := (= #41 #97)
+#95 := (= #39 #94)
+#96 := [rewrite]: #95
+#99 := [monotonicity #96]: #98
+#108 := [trans #99 #106]: #107
+#91 := (= #36 #90)
+#76 := (= #32 #75)
+#77 := [rewrite]: #76
+#88 := (= #35 #85)
+#81 := (- #75)
+#86 := (= #81 #85)
+#87 := [rewrite]: #86
+#82 := (= #35 #81)
+#83 := [monotonicity #77]: #82
+#89 := [trans #83 #87]: #88
+#79 := (iff #34 #78)
+#80 := [monotonicity #77]: #79
+#92 := [monotonicity #80 #89 #77]: #91
+#111 := [monotonicity #92 #108]: #110
+#137 := [trans #111 #135]: #136
+#72 := [asserted]: #42
+#138 := [mp #72 #137]: #131
+decl uf_1 :: T1
+#4 := uf_1
+#43 := (uf_13 uf_1)
+#44 := (uf_12 #43 uf_14)
+#45 := (uf_11 #44 uf_15)
+#149 := (* -1::real #45)
+#150 := (+ #38 #149)
+#140 := (+ #93 #45)
+#161 := (<= #150 0::real)
+#168 := (ite #161 #140 #150)
+#176 := (* -1::real #168)
+#177 := (+ #103 #176)
+#178 := (+ #101 #177)
+#179 := (<= #178 0::real)
+#180 := (not #179)
+#46 := (- #45 #38)
+#48 := (- #46)
+#47 := (< #46 0::real)
+#49 := (ite #47 #48 #46)
+#50 := (< #49 #41)
+#185 := (iff #50 #180)
+#143 := (< #140 0::real)
+#155 := (ite #143 #150 #140)
+#158 := (< #155 #104)
+#183 := (iff #158 #180)
+#173 := (< #168 #104)
+#181 := (iff #173 #180)
+#182 := [rewrite]: #181
+#174 := (iff #158 #173)
+#171 := (= #155 #168)
+#162 := (not #161)
+#165 := (ite #162 #150 #140)
+#169 := (= #165 #168)
+#170 := [rewrite]: #169
+#166 := (= #155 #165)
+#163 := (iff #143 #162)
+#164 := [rewrite]: #163
+#167 := [monotonicity #164]: #166
+#172 := [trans #167 #170]: #171
+#175 := [monotonicity #172]: #174
+#184 := [trans #175 #182]: #183
+#159 := (iff #50 #158)
+#156 := (= #49 #155)
+#141 := (= #46 #140)
+#142 := [rewrite]: #141
+#153 := (= #48 #150)
+#146 := (- #140)
+#151 := (= #146 #150)
+#152 := [rewrite]: #151
+#147 := (= #48 #146)
+#148 := [monotonicity #142]: #147
+#154 := [trans #148 #152]: #153
+#144 := (iff #47 #143)
+#145 := [monotonicity #142]: #144
+#157 := [monotonicity #145 #154 #142]: #156
+#160 := [monotonicity #157 #108]: #159
+#186 := [trans #160 #184]: #185
+#139 := [asserted]: #50
+#187 := [mp #139 #186]: #180
+#299 := (+ #140 #176)
+#300 := (<= #299 0::real)
+#290 := (= #140 #168)
+#329 := [hypothesis]: #162
+#191 := (+ #29 #149)
+#192 := (<= #191 0::real)
+#51 := (<= #29 #45)
+#193 := (iff #51 #192)
+#194 := [rewrite]: #193
+#188 := [asserted]: #51
+#195 := [mp #188 #194]: #192
+#298 := (+ #75 #127)
+#301 := (<= #298 0::real)
+#284 := (= #75 #119)
+#302 := [hypothesis]: #113
+#296 := (+ #85 #127)
+#297 := (<= #296 0::real)
+#285 := (= #85 #119)
+#288 := (or #112 #285)
+#289 := [def-axiom]: #288
+#303 := [unit-resolution #289 #302]: #285
+#304 := (not #285)
+#305 := (or #304 #297)
+#306 := [th-lemma]: #305
+#307 := [unit-resolution #306 #303]: #297
+#315 := (not #290)
+#310 := (not #300)
+#311 := (or #310 #112)
+#308 := [hypothesis]: #300
+#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
+#312 := [lemma #309]: #311
+#322 := [unit-resolution #312 #302]: #310
+#316 := (or #315 #300)
+#313 := [hypothesis]: #310
+#314 := [hypothesis]: #290
+#317 := [th-lemma]: #316
+#318 := [unit-resolution #317 #314 #313]: false
+#319 := [lemma #318]: #316
+#323 := [unit-resolution #319 #322]: #315
+#292 := (or #162 #290)
+#293 := [def-axiom]: #292
+#324 := [unit-resolution #293 #323]: #162
+#325 := [th-lemma #324 #307 #138 #302 #195]: false
+#326 := [lemma #325]: #112
+#286 := (or #113 #284)
+#287 := [def-axiom]: #286
+#330 := [unit-resolution #287 #326]: #284
+#331 := (not #284)
+#332 := (or #331 #301)
+#333 := [th-lemma]: #332
+#334 := [unit-resolution #333 #330]: #301
+#335 := [th-lemma #326 #334 #195 #329 #138]: false
+#336 := [lemma #335]: #161
+#327 := [unit-resolution #293 #336]: #290
+#328 := [unit-resolution #319 #327]: #300
+[th-lemma #326 #334 #195 #328 #187 #138]: false
+unsat
diff -r 10e723e54076 -r b766aad9136d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Mar 18 13:57:00 2010 +0100
@@ -1459,7 +1459,7 @@
     { fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
       hence "f (a + x) \<in> S" using d
       apply(erule_tac x="x+a" in allE)
-      by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
+      by (auto simp add: add_commute dist_norm dist_commute)
     }
     hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
       using d(1) by auto
@@ -1476,7 +1476,7 @@
       unfolding Limits.eventually_at by fast
     { fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
       hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
-        by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
+        by(auto simp add: add_commute dist_norm dist_commute)
     }
     hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
     hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
@@ -2755,8 +2755,8 @@
   have "d>0" using `e>0` unfolding d_def e_def using zero_le_dist[of _ l', unfolded order_le_less] by auto
   obtain k where k:"f k \<noteq> l'"  "dist (f k) l' < d" using `d>0` and assms(3)[unfolded islimpt_approachable, THEN spec[where x="d"]] by auto
   have "k\<ge>N" using k(1)[unfolded dist_nz] using k(2)[unfolded d_def]
-    by force
-  hence "dist l' l < e" using N[THEN spec[where x=k]] using k(2)[unfolded d_def] and dist_triangle_half_r[of "f k" l' e l] by auto
+    by (force simp del: Min.insert_idem)
+  hence "dist l' l < e" using N[THEN spec[where x=k]] using k(2)[unfolded d_def] and dist_triangle_half_r[of "f k" l' e l] by (auto simp del: Min.insert_idem)
   thus False unfolding e_def by auto
 qed
 
diff -r 10e723e54076 -r b766aad9136d src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Nat_Transfer.thy	Thu Mar 18 13:57:00 2010 +0100
@@ -10,12 +10,13 @@
 
 subsection {* Generic transfer machinery *}
 
-definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
-  where "transfer_morphism f A \<longleftrightarrow> True"
+definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
+  where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
 
 lemma transfer_morphismI:
-  "transfer_morphism f A"
-  by (simp add: transfer_morphism_def)
+  assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
+  shows "transfer_morphism f A"
+  using assms by (auto simp add: transfer_morphism_def)
 
 use "Tools/transfer.ML"
 
@@ -27,7 +28,7 @@
 text {* set up transfer direction *}
 
 lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
-  by (fact transfer_morphismI)
+  by (rule transfer_morphismI) simp
 
 declare transfer_morphism_nat_int [transfer add
   mode: manual
@@ -266,7 +267,7 @@
 text {* set up transfer direction *}
 
 lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
-  by (fact transfer_morphismI)
+by (rule transfer_morphismI) simp
 
 declare transfer_morphism_int_nat [transfer add
   mode: manual
diff -r 10e723e54076 -r b766aad9136d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Product_Type.thy	Thu Mar 18 13:57:00 2010 +0100
@@ -998,6 +998,15 @@
 lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
   by (auto, rule_tac p = "f x" in PairE, auto)
 
+lemma swap_inj_on:
+  "inj_on (%(i, j). (j, i)) (A \<times> B)"
+  by (unfold inj_on_def) fast
+
+lemma swap_product:
+  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
+  by (simp add: split_def image_def) blast
+
+
 subsubsection {* Code generator setup *}
 
 lemma [code]:
diff -r 10e723e54076 -r b766aad9136d src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/SupInf.thy	Thu Mar 18 13:57:00 2010 +0100
@@ -355,13 +355,13 @@
 
 lemma Inf_greater:
   fixes z :: real
-  shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
+  shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
   by (metis Inf_real_iff mem_def not_leE)
 
 lemma Inf_close:
   fixes e :: real
   shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
-  by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
+  by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict)
 
 lemma Inf_finite_Min:
   fixes S :: "real set"
@@ -417,7 +417,7 @@
   also have "... \<le> e" 
     apply (rule Sup_asclose) 
     apply (auto simp add: S)
-    apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) 
+    apply (metis abs_minus_add_cancel b add_commute real_diff_def) 
     done
   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   thus ?thesis
diff -r 10e723e54076 -r b766aad9136d src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Tools/transfer.ML	Thu Mar 18 13:57:00 2010 +0100
@@ -23,11 +23,13 @@
 
 val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of;
 
+val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI});
+
 fun check_morphism_key ctxt key =
   let
-    val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key)
-      handle Pattern.MATCH => error
-        ("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI}));
+    val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key)
+      handle Pattern.MATCH => error ("Transfer: expected theorem of the form "
+        ^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key)));
   in direction_of key end;
 
 type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list,