diff -r e4d1b5cbd429 -r 2449e026483d src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Wed Mar 17 09:14:43 2010 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Mar 18 13:56:31 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"