src/HOL/Big_Operators.thy
author blanchet
Thu Nov 21 21:33:34 2013 +0100 (2013-11-21)
changeset 54555 e8c5e95d338b
parent 54230 b1d955791529
permissions -rw-r--r--
rationalize imports
     1 (*  Title:      HOL/Big_Operators.thy
     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3                 with contributions by Jeremy Avigad
     4 *)
     5 
     6 header {* Big operators and finite (non-empty) sets *}
     7 
     8 theory Big_Operators
     9 imports Finite_Set Metis
    10 begin
    11 
    12 subsection {* Generic monoid operation over a set *}
    13 
    14 no_notation times (infixl "*" 70)
    15 no_notation Groups.one ("1")
    16 
    17 locale comm_monoid_set = comm_monoid
    18 begin
    19 
    20 interpretation comp_fun_commute f
    21   by default (simp add: fun_eq_iff left_commute)
    22 
    23 interpretation comp_fun_commute "f \<circ> g"
    24   by (rule comp_comp_fun_commute)
    25 
    26 definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    27 where
    28   eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
    29 
    30 lemma infinite [simp]:
    31   "\<not> finite A \<Longrightarrow> F g A = 1"
    32   by (simp add: eq_fold)
    33 
    34 lemma empty [simp]:
    35   "F g {} = 1"
    36   by (simp add: eq_fold)
    37 
    38 lemma insert [simp]:
    39   assumes "finite A" and "x \<notin> A"
    40   shows "F g (insert x A) = g x * F g A"
    41   using assms by (simp add: eq_fold)
    42 
    43 lemma remove:
    44   assumes "finite A" and "x \<in> A"
    45   shows "F g A = g x * F g (A - {x})"
    46 proof -
    47   from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
    48     by (auto dest: mk_disjoint_insert)
    49   moreover from `finite A` A have "finite B" by simp
    50   ultimately show ?thesis by simp
    51 qed
    52 
    53 lemma insert_remove:
    54   assumes "finite A"
    55   shows "F g (insert x A) = g x * F g (A - {x})"
    56   using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
    57 
    58 lemma neutral:
    59   assumes "\<forall>x\<in>A. g x = 1"
    60   shows "F g A = 1"
    61   using assms by (induct A rule: infinite_finite_induct) simp_all
    62 
    63 lemma neutral_const [simp]:
    64   "F (\<lambda>_. 1) A = 1"
    65   by (simp add: neutral)
    66 
    67 lemma union_inter:
    68   assumes "finite A" and "finite B"
    69   shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
    70   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    71 using assms proof (induct A)
    72   case empty then show ?case by simp
    73 next
    74   case (insert x A) then show ?case
    75     by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
    76 qed
    77 
    78 corollary union_inter_neutral:
    79   assumes "finite A" and "finite B"
    80   and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
    81   shows "F g (A \<union> B) = F g A * F g B"
    82   using assms by (simp add: union_inter [symmetric] neutral)
    83 
    84 corollary union_disjoint:
    85   assumes "finite A" and "finite B"
    86   assumes "A \<inter> B = {}"
    87   shows "F g (A \<union> B) = F g A * F g B"
    88   using assms by (simp add: union_inter_neutral)
    89 
    90 lemma subset_diff:
    91   "B \<subseteq> A \<Longrightarrow> finite A \<Longrightarrow> F g A = F g (A - B) * F g B"
    92   by (metis Diff_partition union_disjoint Diff_disjoint finite_Un inf_commute sup_commute)
    93 
    94 lemma reindex:
    95   assumes "inj_on h A"
    96   shows "F g (h ` A) = F (g \<circ> h) A"
    97 proof (cases "finite A")
    98   case True
    99   with assms show ?thesis by (simp add: eq_fold fold_image comp_assoc)
   100 next
   101   case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
   102   with False show ?thesis by simp
   103 qed
   104 
   105 lemma cong:
   106   assumes "A = B"
   107   assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   108   shows "F g A = F h B"
   109 proof (cases "finite A")
   110   case True
   111   then have "\<And>C. C \<subseteq> A \<longrightarrow> (\<forall>x\<in>C. g x = h x) \<longrightarrow> F g C = F h C"
   112   proof induct
   113     case empty then show ?case by simp
   114   next
   115     case (insert x F) then show ?case apply -
   116     apply (simp add: subset_insert_iff, clarify)
   117     apply (subgoal_tac "finite C")
   118       prefer 2 apply (blast dest: finite_subset [rotated])
   119     apply (subgoal_tac "C = insert x (C - {x})")
   120       prefer 2 apply blast
   121     apply (erule ssubst)
   122     apply (simp add: Ball_def del: insert_Diff_single)
   123     done
   124   qed
   125   with `A = B` g_h show ?thesis by simp
   126 next
   127   case False
   128   with `A = B` show ?thesis by simp
   129 qed
   130 
   131 lemma strong_cong [cong]:
   132   assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
   133   shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
   134   by (rule cong) (insert assms, simp_all add: simp_implies_def)
   135 
   136 lemma UNION_disjoint:
   137   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   138   and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   139   shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
   140 apply (insert assms)
   141 apply (induct rule: finite_induct)
   142 apply simp
   143 apply atomize
   144 apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
   145  prefer 2 apply blast
   146 apply (subgoal_tac "A x Int UNION Fa A = {}")
   147  prefer 2 apply blast
   148 apply (simp add: union_disjoint)
   149 done
   150 
   151 lemma Union_disjoint:
   152   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
   153   shows "F g (Union C) = F (F g) C"
   154 proof cases
   155   assume "finite C"
   156   from UNION_disjoint [OF this assms]
   157   show ?thesis
   158     by (simp add: SUP_def)
   159 qed (auto dest: finite_UnionD intro: infinite)
   160 
   161 lemma distrib:
   162   "F (\<lambda>x. g x * h x) A = F g A * F h A"
   163   using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
   164 
   165 lemma Sigma:
   166   "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
   167 apply (subst Sigma_def)
   168 apply (subst UNION_disjoint, assumption, simp)
   169  apply blast
   170 apply (rule cong)
   171 apply rule
   172 apply (simp add: fun_eq_iff)
   173 apply (subst UNION_disjoint, simp, simp)
   174  apply blast
   175 apply (simp add: comp_def)
   176 done
   177 
   178 lemma related: 
   179   assumes Re: "R 1 1" 
   180   and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   181   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   182   shows "R (F h S) (F g S)"
   183   using fS by (rule finite_subset_induct) (insert assms, auto)
   184 
   185 lemma eq_general:
   186   assumes h: "\<forall>y\<in>S'. \<exists>!x. x \<in> S \<and> h x = y" 
   187   and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2 (h x) = f1 x"
   188   shows "F f1 S = F f2 S'"
   189 proof-
   190   from h f12 have hS: "h ` S = S'" by blast
   191   {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
   192     from f12 h H  have "x = y" by auto }
   193   hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
   194   from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
   195   from hS have "F f2 S' = F f2 (h ` S)" by simp
   196   also have "\<dots> = F (f2 o h) S" using reindex [OF hinj, of f2] .
   197   also have "\<dots> = F f1 S " using th cong [of _ _ "f2 o h" f1]
   198     by blast
   199   finally show ?thesis ..
   200 qed
   201 
   202 lemma eq_general_reverses:
   203   assumes kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   204   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = j x"
   205   shows "F j S = F g T"
   206   (* metis solves it, but not yet available here *)
   207   apply (rule eq_general [of T S h g j])
   208   apply (rule ballI)
   209   apply (frule kh)
   210   apply (rule ex1I[])
   211   apply blast
   212   apply clarsimp
   213   apply (drule hk) apply simp
   214   apply (rule sym)
   215   apply (erule conjunct1[OF conjunct2[OF hk]])
   216   apply (rule ballI)
   217   apply (drule hk)
   218   apply blast
   219   done
   220 
   221 lemma mono_neutral_cong_left:
   222   assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
   223   and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
   224 proof-
   225   have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
   226   have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
   227   from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
   228     by (auto intro: finite_subset)
   229   show ?thesis using assms(4)
   230     by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
   231 qed
   232 
   233 lemma mono_neutral_cong_right:
   234   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
   235    \<Longrightarrow> F g T = F h S"
   236   by (auto intro!: mono_neutral_cong_left [symmetric])
   237 
   238 lemma mono_neutral_left:
   239   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   240   by (blast intro: mono_neutral_cong_left)
   241 
   242 lemma mono_neutral_right:
   243   "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   244   by (blast intro!: mono_neutral_left [symmetric])
   245 
   246 lemma delta: 
   247   assumes fS: "finite S"
   248   shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
   249 proof-
   250   let ?f = "(\<lambda>k. if k=a then b k else 1)"
   251   { assume a: "a \<notin> S"
   252     hence "\<forall>k\<in>S. ?f k = 1" by simp
   253     hence ?thesis  using a by simp }
   254   moreover
   255   { assume a: "a \<in> S"
   256     let ?A = "S - {a}"
   257     let ?B = "{a}"
   258     have eq: "S = ?A \<union> ?B" using a by blast 
   259     have dj: "?A \<inter> ?B = {}" by simp
   260     from fS have fAB: "finite ?A" "finite ?B" by auto  
   261     have "F ?f S = F ?f ?A * F ?f ?B"
   262       using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
   263       by simp
   264     then have ?thesis using a by simp }
   265   ultimately show ?thesis by blast
   266 qed
   267 
   268 lemma delta': 
   269   assumes fS: "finite S"
   270   shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
   271   using delta [OF fS, of a b, symmetric] by (auto intro: cong)
   272 
   273 lemma If_cases:
   274   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   275   assumes fA: "finite A"
   276   shows "F (\<lambda>x. if P x then h x else g x) A =
   277     F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
   278 proof -
   279   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
   280           "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
   281     by blast+
   282   from fA 
   283   have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   284   let ?g = "\<lambda>x. if P x then h x else g x"
   285   from union_disjoint [OF f a(2), of ?g] a(1)
   286   show ?thesis
   287     by (subst (1 2) cong) simp_all
   288 qed
   289 
   290 lemma cartesian_product:
   291    "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
   292 apply (rule sym)
   293 apply (cases "finite A") 
   294  apply (cases "finite B") 
   295   apply (simp add: Sigma)
   296  apply (cases "A={}", simp)
   297  apply simp
   298 apply (auto intro: infinite dest: finite_cartesian_productD2)
   299 apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
   300 done
   301 
   302 end
   303 
   304 notation times (infixl "*" 70)
   305 notation Groups.one ("1")
   306 
   307 
   308 subsection {* Generalized summation over a set *}
   309 
   310 context comm_monoid_add
   311 begin
   312 
   313 definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   314 where
   315   "setsum = comm_monoid_set.F plus 0"
   316 
   317 sublocale setsum!: comm_monoid_set plus 0
   318 where
   319   "comm_monoid_set.F plus 0 = setsum"
   320 proof -
   321   show "comm_monoid_set plus 0" ..
   322   then interpret setsum!: comm_monoid_set plus 0 .
   323   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   324 qed
   325 
   326 abbreviation
   327   Setsum ("\<Sum>_" [1000] 999) where
   328   "\<Sum>A \<equiv> setsum (%x. x) A"
   329 
   330 end
   331 
   332 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   333 written @{text"\<Sum>x\<in>A. e"}. *}
   334 
   335 syntax
   336   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   337 syntax (xsymbols)
   338   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   339 syntax (HTML output)
   340   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   341 
   342 translations -- {* Beware of argument permutation! *}
   343   "SUM i:A. b" == "CONST setsum (%i. b) A"
   344   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   345 
   346 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   347  @{text"\<Sum>x|P. e"}. *}
   348 
   349 syntax
   350   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   351 syntax (xsymbols)
   352   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   353 syntax (HTML output)
   354   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   355 
   356 translations
   357   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   358   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   359 
   360 print_translation {*
   361 let
   362   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   363         if x <> y then raise Match
   364         else
   365           let
   366             val x' = Syntax_Trans.mark_bound_body (x, Tx);
   367             val t' = subst_bound (x', t);
   368             val P' = subst_bound (x', P);
   369           in
   370             Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   371           end
   372     | setsum_tr' _ = raise Match;
   373 in [(@{const_syntax setsum}, K setsum_tr')] end
   374 *}
   375 
   376 text {* TODO These are candidates for generalization *}
   377 
   378 context comm_monoid_add
   379 begin
   380 
   381 lemma setsum_reindex_id: 
   382   "inj_on f B ==> setsum f B = setsum id (f ` B)"
   383   by (simp add: setsum.reindex)
   384 
   385 lemma setsum_reindex_nonzero:
   386   assumes fS: "finite S"
   387   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"
   388   shows "setsum h (f ` S) = setsum (h \<circ> f) S"
   389 using nz proof (induct rule: finite_induct [OF fS])
   390   case 1 thus ?case by simp
   391 next
   392   case (2 x F) 
   393   { assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
   394     then obtain y where y: "y \<in> F" "f x = f y" by auto 
   395     from "2.hyps" y have xy: "x \<noteq> y" by auto
   396     from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
   397     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
   398     also have "\<dots> = setsum (h o f) (insert x F)" 
   399       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   400       using h0
   401       apply (simp cong del: setsum.strong_cong)
   402       apply (rule "2.hyps"(3))
   403       apply (rule_tac y="y" in  "2.prems")
   404       apply simp_all
   405       done
   406     finally have ?case . }
   407   moreover
   408   { assume fxF: "f x \<notin> f ` F"
   409     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
   410       using fxF "2.hyps" by simp 
   411     also have "\<dots> = setsum (h o f) (insert x F)"
   412       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   413       apply (simp cong del: setsum.strong_cong)
   414       apply (rule cong [OF refl [of "op + (h (f x))"]])
   415       apply (rule "2.hyps"(3))
   416       apply (rule_tac y="y" in  "2.prems")
   417       apply simp_all
   418       done
   419     finally have ?case . }
   420   ultimately show ?case by blast
   421 qed
   422 
   423 lemma setsum_cong2:
   424   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
   425   by (auto intro: setsum.cong)
   426 
   427 lemma setsum_reindex_cong:
   428    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   429     ==> setsum h B = setsum g A"
   430   by (simp add: setsum.reindex)
   431 
   432 lemma setsum_restrict_set:
   433   assumes fA: "finite A"
   434   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   435 proof-
   436   from fA have fab: "finite (A \<inter> B)" by auto
   437   have aba: "A \<inter> B \<subseteq> A" by blast
   438   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   439   from setsum.mono_neutral_left [OF fA aba, of ?g]
   440   show ?thesis by simp
   441 qed
   442 
   443 lemma setsum_Union_disjoint:
   444   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
   445   shows "setsum f (Union C) = setsum (setsum f) C"
   446   using assms by (fact setsum.Union_disjoint)
   447 
   448 lemma setsum_cartesian_product:
   449   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   450   by (fact setsum.cartesian_product)
   451 
   452 lemma setsum_UNION_zero:
   453   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   454   and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
   455   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   456   using fSS f0
   457 proof(induct rule: finite_induct[OF fS])
   458   case 1 thus ?case by simp
   459 next
   460   case (2 T F)
   461   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   462     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
   463   from fTF have fUF: "finite (\<Union>F)" by auto
   464   from "2.prems" TF fTF
   465   show ?case 
   466     by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f])
   467 qed
   468 
   469 text {* Commuting outer and inner summation *}
   470 
   471 lemma setsum_commute:
   472   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   473 proof (simp add: setsum_cartesian_product)
   474   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
   475     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
   476     (is "?s = _")
   477     apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on)
   478     apply (simp add: split_def)
   479     done
   480   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
   481     (is "_ = ?t")
   482     apply (simp add: swap_product)
   483     done
   484   finally show "?s = ?t" .
   485 qed
   486 
   487 lemma setsum_Plus:
   488   fixes A :: "'a set" and B :: "'b set"
   489   assumes fin: "finite A" "finite B"
   490   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   491 proof -
   492   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   493   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   494     by auto
   495   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   496   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   497   ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex)
   498 qed
   499 
   500 end
   501 
   502 text {* TODO These are legacy *}
   503 
   504 lemma setsum_empty:
   505   "setsum f {} = 0"
   506   by (fact setsum.empty)
   507 
   508 lemma setsum_insert:
   509   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   510   by (fact setsum.insert)
   511 
   512 lemma setsum_infinite:
   513   "~ finite A ==> setsum f A = 0"
   514   by (fact setsum.infinite)
   515 
   516 lemma setsum_reindex:
   517   "inj_on f B \<Longrightarrow> setsum h (f ` B) = setsum (h \<circ> f) B"
   518   by (fact setsum.reindex)
   519 
   520 lemma setsum_cong:
   521   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   522   by (fact setsum.cong)
   523 
   524 lemma strong_setsum_cong:
   525   "A = B ==> (!!x. x:B =simp=> f x = g x)
   526    ==> setsum (%x. f x) A = setsum (%x. g x) B"
   527   by (fact setsum.strong_cong)
   528 
   529 lemmas setsum_0 = setsum.neutral_const
   530 lemmas setsum_0' = setsum.neutral
   531 
   532 lemma setsum_Un_Int: "finite A ==> finite B ==>
   533   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   534   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   535   by (fact setsum.union_inter)
   536 
   537 lemma setsum_Un_disjoint: "finite A ==> finite B
   538   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   539   by (fact setsum.union_disjoint)
   540 
   541 lemma setsum_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
   542     setsum f A = setsum f (A - B) + setsum f B"
   543   by (fact setsum.subset_diff)
   544 
   545 lemma setsum_mono_zero_left: 
   546   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 0 \<rbrakk> \<Longrightarrow> setsum f S = setsum f T"
   547   by (fact setsum.mono_neutral_left)
   548 
   549 lemmas setsum_mono_zero_right = setsum.mono_neutral_right
   550 
   551 lemma setsum_mono_zero_cong_left: 
   552   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
   553   \<Longrightarrow> setsum f S = setsum g T"
   554   by (fact setsum.mono_neutral_cong_left)
   555 
   556 lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right
   557 
   558 lemma setsum_delta: "finite S \<Longrightarrow>
   559   setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
   560   by (fact setsum.delta)
   561 
   562 lemma setsum_delta': "finite S \<Longrightarrow>
   563   setsum (\<lambda>k. if a = k then b k else 0) S = (if a\<in> S then b a else 0)"
   564   by (fact setsum.delta')
   565 
   566 lemma setsum_cases:
   567   assumes "finite A"
   568   shows "setsum (\<lambda>x. if P x then f x else g x) A =
   569          setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
   570   using assms by (fact setsum.If_cases)
   571 
   572 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   573   the lhs need not be, since UNION I A could still be finite.*)
   574 lemma setsum_UN_disjoint:
   575   assumes "finite I" and "ALL i:I. finite (A i)"
   576     and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
   577   shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   578   using assms by (fact setsum.UNION_disjoint)
   579 
   580 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   581   the rhs need not be, since SIGMA A B could still be finite.*)
   582 lemma setsum_Sigma:
   583   assumes "finite A" and  "ALL x:A. finite (B x)"
   584   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)"
   585   using assms by (fact setsum.Sigma)
   586 
   587 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   588   by (fact setsum.distrib)
   589 
   590 lemma setsum_Un_zero:  
   591   "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 0 \<rbrakk> \<Longrightarrow>
   592   setsum f (S \<union> T) = setsum f S + setsum f T"
   593   by (fact setsum.union_inter_neutral)
   594 
   595 lemma setsum_eq_general_reverses:
   596   assumes fS: "finite S" and fT: "finite T"
   597   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   598   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
   599   shows "setsum f S = setsum g T"
   600   using kh hk by (fact setsum.eq_general_reverses)
   601 
   602 
   603 subsubsection {* Properties in more restricted classes of structures *}
   604 
   605 lemma setsum_Un: "finite A ==> finite B ==>
   606   (setsum f (A Un B) :: 'a :: ab_group_add) =
   607    setsum f A + setsum f B - setsum f (A Int B)"
   608 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   609 
   610 lemma setsum_Un2:
   611   assumes "finite (A \<union> B)"
   612   shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
   613 proof -
   614   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   615     by auto
   616   with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
   617 qed
   618 
   619 lemma setsum_diff1: "finite A \<Longrightarrow>
   620   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   621   (if a:A then setsum f A - f a else setsum f A)"
   622 by (erule finite_induct) (auto simp add: insert_Diff_if)
   623 
   624 lemma setsum_diff:
   625   assumes le: "finite A" "B \<subseteq> A"
   626   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   627 proof -
   628   from le have finiteB: "finite B" using finite_subset by auto
   629   show ?thesis using finiteB le
   630   proof induct
   631     case empty
   632     thus ?case by auto
   633   next
   634     case (insert x F)
   635     thus ?case using le finiteB 
   636       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   637   qed
   638 qed
   639 
   640 lemma setsum_mono:
   641   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   642   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   643 proof (cases "finite K")
   644   case True
   645   thus ?thesis using le
   646   proof induct
   647     case empty
   648     thus ?case by simp
   649   next
   650     case insert
   651     thus ?case using add_mono by fastforce
   652   qed
   653 next
   654   case False then show ?thesis by simp
   655 qed
   656 
   657 lemma setsum_strict_mono:
   658   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   659   assumes "finite A"  "A \<noteq> {}"
   660     and "!!x. x:A \<Longrightarrow> f x < g x"
   661   shows "setsum f A < setsum g A"
   662   using assms
   663 proof (induct rule: finite_ne_induct)
   664   case singleton thus ?case by simp
   665 next
   666   case insert thus ?case by (auto simp: add_strict_mono)
   667 qed
   668 
   669 lemma setsum_strict_mono_ex1:
   670 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   671 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   672 shows "setsum f A < setsum g A"
   673 proof-
   674   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   675   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   676     by(simp add:insert_absorb[OF `a:A`])
   677   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   678     using `finite A` by(subst setsum_Un_disjoint) auto
   679   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   680     by(rule setsum_mono)(simp add: assms(2))
   681   also have "setsum f {a} < setsum g {a}" using a by simp
   682   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   683     using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
   684   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   685   finally show ?thesis by (metis add_right_mono add_strict_left_mono)
   686 qed
   687 
   688 lemma setsum_negf:
   689   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   690 proof (cases "finite A")
   691   case True thus ?thesis by (induct set: finite) auto
   692 next
   693   case False thus ?thesis by simp
   694 qed
   695 
   696 lemma setsum_subtractf:
   697   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   698     setsum f A - setsum g A"
   699   using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
   700 
   701 lemma setsum_nonneg:
   702   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   703   shows "0 \<le> setsum f A"
   704 proof (cases "finite A")
   705   case True thus ?thesis using nn
   706   proof induct
   707     case empty then show ?case by simp
   708   next
   709     case (insert x F)
   710     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   711     with insert show ?case by simp
   712   qed
   713 next
   714   case False thus ?thesis by simp
   715 qed
   716 
   717 lemma setsum_nonpos:
   718   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   719   shows "setsum f A \<le> 0"
   720 proof (cases "finite A")
   721   case True thus ?thesis using np
   722   proof induct
   723     case empty then show ?case by simp
   724   next
   725     case (insert x F)
   726     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   727     with insert show ?case by simp
   728   qed
   729 next
   730   case False thus ?thesis by simp
   731 qed
   732 
   733 lemma setsum_nonneg_leq_bound:
   734   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   735   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   736   shows "f i \<le> B"
   737 proof -
   738   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   739     using assms by (auto intro!: setsum_nonneg)
   740   moreover
   741   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   742     using assms by (simp add: setsum_diff1)
   743   ultimately show ?thesis by auto
   744 qed
   745 
   746 lemma setsum_nonneg_0:
   747   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   748   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   749   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   750   shows "f i = 0"
   751   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   752 
   753 lemma setsum_mono2:
   754 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   755 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   756 shows "setsum f A \<le> setsum f B"
   757 proof -
   758   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   759     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   760   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   761     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   762   also have "A \<union> (B-A) = B" using sub by blast
   763   finally show ?thesis .
   764 qed
   765 
   766 lemma setsum_mono3: "finite B ==> A <= B ==> 
   767     ALL x: B - A. 
   768       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   769         setsum f A <= setsum f B"
   770   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   771   apply (erule ssubst)
   772   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   773   apply simp
   774   apply (rule add_left_mono)
   775   apply (erule setsum_nonneg)
   776   apply (subst setsum_Un_disjoint [THEN sym])
   777   apply (erule finite_subset, assumption)
   778   apply (rule finite_subset)
   779   prefer 2
   780   apply assumption
   781   apply (auto simp add: sup_absorb2)
   782 done
   783 
   784 lemma setsum_right_distrib: 
   785   fixes f :: "'a => ('b::semiring_0)"
   786   shows "r * setsum f A = setsum (%n. r * f n) A"
   787 proof (cases "finite A")
   788   case True
   789   thus ?thesis
   790   proof induct
   791     case empty thus ?case by simp
   792   next
   793     case (insert x A) thus ?case by (simp add: distrib_left)
   794   qed
   795 next
   796   case False thus ?thesis by simp
   797 qed
   798 
   799 lemma setsum_left_distrib:
   800   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   801 proof (cases "finite A")
   802   case True
   803   then show ?thesis
   804   proof induct
   805     case empty thus ?case by simp
   806   next
   807     case (insert x A) thus ?case by (simp add: distrib_right)
   808   qed
   809 next
   810   case False thus ?thesis by simp
   811 qed
   812 
   813 lemma setsum_divide_distrib:
   814   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   815 proof (cases "finite A")
   816   case True
   817   then show ?thesis
   818   proof induct
   819     case empty thus ?case by simp
   820   next
   821     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   822   qed
   823 next
   824   case False thus ?thesis by simp
   825 qed
   826 
   827 lemma setsum_abs[iff]: 
   828   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   829   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   830 proof (cases "finite A")
   831   case True
   832   thus ?thesis
   833   proof induct
   834     case empty thus ?case by simp
   835   next
   836     case (insert x A)
   837     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   838   qed
   839 next
   840   case False thus ?thesis by simp
   841 qed
   842 
   843 lemma setsum_abs_ge_zero[iff]: 
   844   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   845   shows "0 \<le> setsum (%i. abs(f i)) A"
   846 proof (cases "finite A")
   847   case True
   848   thus ?thesis
   849   proof induct
   850     case empty thus ?case by simp
   851   next
   852     case (insert x A) thus ?case by auto
   853   qed
   854 next
   855   case False thus ?thesis by simp
   856 qed
   857 
   858 lemma abs_setsum_abs[simp]: 
   859   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   860   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   861 proof (cases "finite A")
   862   case True
   863   thus ?thesis
   864   proof induct
   865     case empty thus ?case by simp
   866   next
   867     case (insert a A)
   868     hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
   869     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   870     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   871       by (simp del: abs_of_nonneg)
   872     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   873     finally show ?case .
   874   qed
   875 next
   876   case False thus ?thesis by simp
   877 qed
   878 
   879 lemma setsum_diff1'[rule_format]:
   880   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   881 apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
   882 apply (auto simp add: insert_Diff_if add_ac)
   883 done
   884 
   885 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   886   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   887 unfolding setsum_diff1'[OF assms] by auto
   888 
   889 lemma setsum_product:
   890   fixes f :: "'a => ('b::semiring_0)"
   891   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   892   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   893 
   894 lemma setsum_mult_setsum_if_inj:
   895 fixes f :: "'a => ('b::semiring_0)"
   896 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   897   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   898 by(auto simp: setsum_product setsum_cartesian_product
   899         intro!:  setsum_reindex_cong[symmetric])
   900 
   901 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   902 apply (case_tac "finite A")
   903  prefer 2 apply simp
   904 apply (erule rev_mp)
   905 apply (erule finite_induct, auto)
   906 done
   907 
   908 lemma setsum_eq_0_iff [simp]:
   909   "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   910   by (induct set: finite) auto
   911 
   912 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   913   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   914 apply(erule finite_induct)
   915 apply (auto simp add:add_is_1)
   916 done
   917 
   918 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   919 
   920 lemma setsum_Un_nat: "finite A ==> finite B ==>
   921   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   922   -- {* For the natural numbers, we have subtraction. *}
   923 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   924 
   925 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   926   (if a:A then setsum f A - f a else setsum f A)"
   927 apply (case_tac "finite A")
   928  prefer 2 apply simp
   929 apply (erule finite_induct)
   930  apply (auto simp add: insert_Diff_if)
   931 apply (drule_tac a = a in mk_disjoint_insert, auto)
   932 done
   933 
   934 lemma setsum_diff_nat: 
   935 assumes "finite B" and "B \<subseteq> A"
   936 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   937 using assms
   938 proof induct
   939   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   940 next
   941   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   942     and xFinA: "insert x F \<subseteq> A"
   943     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   944   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   945   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   946     by (simp add: setsum_diff1_nat)
   947   from xFinA have "F \<subseteq> A" by simp
   948   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   949   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   950     by simp
   951   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   952   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   953     by simp
   954   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   955   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   956     by simp
   957   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   958 qed
   959 
   960 lemma setsum_comp_morphism:
   961   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   962   shows "setsum (h \<circ> g) A = h (setsum g A)"
   963 proof (cases "finite A")
   964   case False then show ?thesis by (simp add: assms)
   965 next
   966   case True then show ?thesis by (induct A) (simp_all add: assms)
   967 qed
   968 
   969 
   970 subsubsection {* Cardinality as special case of @{const setsum} *}
   971 
   972 lemma card_eq_setsum:
   973   "card A = setsum (\<lambda>x. 1) A"
   974 proof -
   975   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   976     by (simp add: fun_eq_iff)
   977   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   978     by (rule arg_cong)
   979   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   980     by (blast intro: fun_cong)
   981   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   982 qed
   983 
   984 lemma setsum_constant [simp]:
   985   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   986 apply (cases "finite A")
   987 apply (erule finite_induct)
   988 apply (auto simp add: algebra_simps)
   989 done
   990 
   991 lemma setsum_bounded:
   992   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   993   shows "setsum f A \<le> of_nat (card A) * K"
   994 proof (cases "finite A")
   995   case True
   996   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   997 next
   998   case False thus ?thesis by simp
   999 qed
  1000 
  1001 lemma card_UN_disjoint:
  1002   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
  1003     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
  1004   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1005 proof -
  1006   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
  1007   with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
  1008 qed
  1009 
  1010 lemma card_Union_disjoint:
  1011   "finite C ==> (ALL A:C. finite A) ==>
  1012    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  1013    ==> card (Union C) = setsum card C"
  1014 apply (frule card_UN_disjoint [of C id])
  1015 apply (simp_all add: SUP_def id_def)
  1016 done
  1017 
  1018 
  1019 subsubsection {* Cardinality of products *}
  1020 
  1021 lemma card_SigmaI [simp]:
  1022   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1023   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1024 by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
  1025 
  1026 (*
  1027 lemma SigmaI_insert: "y \<notin> A ==>
  1028   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1029   by auto
  1030 *)
  1031 
  1032 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1033   by (cases "finite A \<and> finite B")
  1034     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1035 
  1036 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1037 by (simp add: card_cartesian_product)
  1038 
  1039 
  1040 subsection {* Generalized product over a set *}
  1041 
  1042 context comm_monoid_mult
  1043 begin
  1044 
  1045 definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  1046 where
  1047   "setprod = comm_monoid_set.F times 1"
  1048 
  1049 sublocale setprod!: comm_monoid_set times 1
  1050 where
  1051   "comm_monoid_set.F times 1 = setprod"
  1052 proof -
  1053   show "comm_monoid_set times 1" ..
  1054   then interpret setprod!: comm_monoid_set times 1 .
  1055   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  1056 qed
  1057 
  1058 abbreviation
  1059   Setprod ("\<Prod>_" [1000] 999) where
  1060   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1061 
  1062 end
  1063 
  1064 syntax
  1065   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1066 syntax (xsymbols)
  1067   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1068 syntax (HTML output)
  1069   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1070 
  1071 translations -- {* Beware of argument permutation! *}
  1072   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1073   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1074 
  1075 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1076  @{text"\<Prod>x|P. e"}. *}
  1077 
  1078 syntax
  1079   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1080 syntax (xsymbols)
  1081   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1082 syntax (HTML output)
  1083   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1084 
  1085 translations
  1086   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1087   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1088 
  1089 text {* TODO These are candidates for generalization *}
  1090 
  1091 context comm_monoid_mult
  1092 begin
  1093 
  1094 lemma setprod_reindex_id:
  1095   "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1096   by (auto simp add: setprod.reindex)
  1097 
  1098 lemma setprod_reindex_cong:
  1099   "inj_on f A ==> B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1100   by (frule setprod.reindex, simp)
  1101 
  1102 lemma strong_setprod_reindex_cong:
  1103   assumes i: "inj_on f A"
  1104   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
  1105   shows "setprod h B = setprod g A"
  1106 proof-
  1107   have "setprod h B = setprod (h o f) A"
  1108     by (simp add: B setprod.reindex [OF i, of h])
  1109   then show ?thesis apply simp
  1110     apply (rule setprod.cong)
  1111     apply simp
  1112     by (simp add: eq)
  1113 qed
  1114 
  1115 lemma setprod_Union_disjoint:
  1116   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  1117   shows "setprod f (Union C) = setprod (setprod f) C"
  1118   using assms by (fact setprod.Union_disjoint)
  1119 
  1120 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1121 lemma setprod_cartesian_product:
  1122   "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1123   by (fact setprod.cartesian_product)
  1124 
  1125 lemma setprod_Un2:
  1126   assumes "finite (A \<union> B)"
  1127   shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
  1128 proof -
  1129   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
  1130     by auto
  1131   with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+
  1132 qed
  1133 
  1134 end
  1135 
  1136 text {* TODO These are legacy *}
  1137 
  1138 lemma setprod_empty: "setprod f {} = 1"
  1139   by (fact setprod.empty)
  1140 
  1141 lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
  1142     setprod f (insert a A) = f a * setprod f A"
  1143   by (fact setprod.insert)
  1144 
  1145 lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
  1146   by (fact setprod.infinite)
  1147 
  1148 lemma setprod_reindex:
  1149   "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1150   by (fact setprod.reindex)
  1151 
  1152 lemma setprod_cong:
  1153   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1154   by (fact setprod.cong)
  1155 
  1156 lemma strong_setprod_cong:
  1157   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1158   by (fact setprod.strong_cong)
  1159 
  1160 lemma setprod_Un_one:
  1161   "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
  1162   \<Longrightarrow> setprod f (S \<union> T) = setprod f S  * setprod f T"
  1163   by (fact setprod.union_inter_neutral)
  1164 
  1165 lemmas setprod_1 = setprod.neutral_const
  1166 lemmas setprod_1' = setprod.neutral
  1167 
  1168 lemma setprod_Un_Int: "finite A ==> finite B
  1169     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1170   by (fact setprod.union_inter)
  1171 
  1172 lemma setprod_Un_disjoint: "finite A ==> finite B
  1173   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1174   by (fact setprod.union_disjoint)
  1175 
  1176 lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
  1177     setprod f A = setprod f (A - B) * setprod f B"
  1178   by (fact setprod.subset_diff)
  1179 
  1180 lemma setprod_mono_one_left:
  1181   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
  1182   by (fact setprod.mono_neutral_left)
  1183 
  1184 lemmas setprod_mono_one_right = setprod.mono_neutral_right
  1185 
  1186 lemma setprod_mono_one_cong_left: 
  1187   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
  1188   \<Longrightarrow> setprod f S = setprod g T"
  1189   by (fact setprod.mono_neutral_cong_left)
  1190 
  1191 lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right
  1192 
  1193 lemma setprod_delta: "finite S \<Longrightarrow>
  1194   setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  1195   by (fact setprod.delta)
  1196 
  1197 lemma setprod_delta': "finite S \<Longrightarrow>
  1198   setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
  1199   by (fact setprod.delta')
  1200 
  1201 lemma setprod_UN_disjoint:
  1202     "finite I ==> (ALL i:I. finite (A i)) ==>
  1203         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1204       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1205   by (fact setprod.UNION_disjoint)
  1206 
  1207 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1208     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1209     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1210   by (fact setprod.Sigma)
  1211 
  1212 lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A = setprod f A * setprod g A"
  1213   by (fact setprod.distrib)
  1214 
  1215 
  1216 subsubsection {* Properties in more restricted classes of structures *}
  1217 
  1218 lemma setprod_zero:
  1219      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1220 apply (induct set: finite, force, clarsimp)
  1221 apply (erule disjE, auto)
  1222 done
  1223 
  1224 lemma setprod_zero_iff[simp]: "finite A ==> 
  1225   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1226   (EX x: A. f x = 0)"
  1227 by (erule finite_induct, auto simp:no_zero_divisors)
  1228 
  1229 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1230   (setprod f (A Un B) :: 'a ::{field})
  1231    = setprod f A * setprod f B / setprod f (A Int B)"
  1232 by (subst setprod_Un_Int [symmetric], auto)
  1233 
  1234 lemma setprod_nonneg [rule_format]:
  1235    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1236 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  1237 
  1238 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  1239   --> 0 < setprod f A"
  1240 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  1241 
  1242 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1243   (setprod f (A - {a}) :: 'a :: {field}) =
  1244   (if a:A then setprod f A / f a else setprod f A)"
  1245   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1246 
  1247 lemma setprod_inversef: 
  1248   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1249   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1250 by (erule finite_induct) auto
  1251 
  1252 lemma setprod_dividef:
  1253   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1254   shows "finite A
  1255     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1256 apply (subgoal_tac
  1257          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1258 apply (erule ssubst)
  1259 apply (subst divide_inverse)
  1260 apply (subst setprod_timesf)
  1261 apply (subst setprod_inversef, assumption+, rule refl)
  1262 apply (rule setprod_cong, rule refl)
  1263 apply (subst divide_inverse, auto)
  1264 done
  1265 
  1266 lemma setprod_dvd_setprod [rule_format]: 
  1267     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1268   apply (cases "finite A")
  1269   apply (induct set: finite)
  1270   apply (auto simp add: dvd_def)
  1271   apply (rule_tac x = "k * ka" in exI)
  1272   apply (simp add: algebra_simps)
  1273 done
  1274 
  1275 lemma setprod_dvd_setprod_subset:
  1276   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1277   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1278   apply (unfold dvd_def, blast)
  1279   apply (subst setprod_Un_disjoint [symmetric])
  1280   apply (auto elim: finite_subset intro: setprod_cong)
  1281 done
  1282 
  1283 lemma setprod_dvd_setprod_subset2:
  1284   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1285       setprod f A dvd setprod g B"
  1286   apply (rule dvd_trans)
  1287   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1288   apply (erule (1) setprod_dvd_setprod_subset)
  1289 done
  1290 
  1291 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1292     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1293 by (induct set: finite) (auto intro: dvd_mult)
  1294 
  1295 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1296     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1297   apply (cases "finite A")
  1298   apply (induct set: finite)
  1299   apply auto
  1300 done
  1301 
  1302 lemma setprod_mono:
  1303   fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  1304   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1305   shows "setprod f A \<le> setprod g A"
  1306 proof (cases "finite A")
  1307   case True
  1308   hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  1309   proof (induct A rule: finite_subset_induct)
  1310     case (insert a F)
  1311     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  1312       unfolding setprod_insert[OF insert(1,3)]
  1313       using assms[rule_format,OF insert(2)] insert
  1314       by (auto intro: mult_mono mult_nonneg_nonneg)
  1315   qed auto
  1316   thus ?thesis by simp
  1317 qed auto
  1318 
  1319 lemma abs_setprod:
  1320   fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  1321   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  1322 proof (cases "finite A")
  1323   case True thus ?thesis
  1324     by induct (auto simp add: field_simps abs_mult)
  1325 qed auto
  1326 
  1327 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  1328 apply (erule finite_induct)
  1329 apply auto
  1330 done
  1331 
  1332 lemma setprod_gen_delta:
  1333   assumes fS: "finite S"
  1334   shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
  1335 proof-
  1336   let ?f = "(\<lambda>k. if k=a then b k else c)"
  1337   {assume a: "a \<notin> S"
  1338     hence "\<forall> k\<in> S. ?f k = c" by simp
  1339     hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
  1340   moreover 
  1341   {assume a: "a \<in> S"
  1342     let ?A = "S - {a}"
  1343     let ?B = "{a}"
  1344     have eq: "S = ?A \<union> ?B" using a by blast 
  1345     have dj: "?A \<inter> ?B = {}" by simp
  1346     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1347     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  1348       apply (rule setprod_cong) by auto
  1349     have cA: "card ?A = card S - 1" using fS a by auto
  1350     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  1351     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1352       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1353       by simp
  1354     then have ?thesis using a cA
  1355       by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
  1356   ultimately show ?thesis by blast
  1357 qed
  1358 
  1359 lemma setprod_eq_1_iff [simp]:
  1360   "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
  1361   by (induct set: finite) auto
  1362 
  1363 lemma setprod_pos_nat:
  1364   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1365 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1366 
  1367 lemma setprod_pos_nat_iff[simp]:
  1368   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1369 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1370 
  1371 
  1372 subsection {* Generic lattice operations over a set *}
  1373 
  1374 no_notation times (infixl "*" 70)
  1375 no_notation Groups.one ("1")
  1376 
  1377 
  1378 subsubsection {* Without neutral element *}
  1379 
  1380 locale semilattice_set = semilattice
  1381 begin
  1382 
  1383 interpretation comp_fun_idem f
  1384   by default (simp_all add: fun_eq_iff left_commute)
  1385 
  1386 definition F :: "'a set \<Rightarrow> 'a"
  1387 where
  1388   eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
  1389 
  1390 lemma eq_fold:
  1391   assumes "finite A"
  1392   shows "F (insert x A) = Finite_Set.fold f x A"
  1393 proof (rule sym)
  1394   let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
  1395   interpret comp_fun_idem "?f"
  1396     by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
  1397   from assms show "Finite_Set.fold f x A = F (insert x A)"
  1398   proof induct
  1399     case empty then show ?case by (simp add: eq_fold')
  1400   next
  1401     case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
  1402   qed
  1403 qed
  1404 
  1405 lemma singleton [simp]:
  1406   "F {x} = x"
  1407   by (simp add: eq_fold)
  1408 
  1409 lemma insert_not_elem:
  1410   assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
  1411   shows "F (insert x A) = x * F A"
  1412 proof -
  1413   from `A \<noteq> {}` obtain b where "b \<in> A" by blast
  1414   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
  1415   with `finite A` and `x \<notin> A`
  1416     have "finite (insert x B)" and "b \<notin> insert x B" by auto
  1417   then have "F (insert b (insert x B)) = x * F (insert b B)"
  1418     by (simp add: eq_fold)
  1419   then show ?thesis by (simp add: * insert_commute)
  1420 qed
  1421 
  1422 lemma in_idem:
  1423   assumes "finite A" and "x \<in> A"
  1424   shows "x * F A = F A"
  1425 proof -
  1426   from assms have "A \<noteq> {}" by auto
  1427   with `finite A` show ?thesis using `x \<in> A`
  1428     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
  1429 qed
  1430 
  1431 lemma insert [simp]:
  1432   assumes "finite A" and "A \<noteq> {}"
  1433   shows "F (insert x A) = x * F A"
  1434   using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
  1435 
  1436 lemma union:
  1437   assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
  1438   shows "F (A \<union> B) = F A * F B"
  1439   using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
  1440 
  1441 lemma remove:
  1442   assumes "finite A" and "x \<in> A"
  1443   shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
  1444 proof -
  1445   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
  1446   with assms show ?thesis by simp
  1447 qed
  1448 
  1449 lemma insert_remove:
  1450   assumes "finite A"
  1451   shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
  1452   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
  1453 
  1454 lemma subset:
  1455   assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
  1456   shows "F B * F A = F A"
  1457 proof -
  1458   from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
  1459   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
  1460 qed
  1461 
  1462 lemma closed:
  1463   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
  1464   shows "F A \<in> A"
  1465 using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
  1466   case singleton then show ?case by simp
  1467 next
  1468   case insert with elem show ?case by force
  1469 qed
  1470 
  1471 lemma hom_commute:
  1472   assumes hom: "\<And>x y. h (x * y) = h x * h y"
  1473   and N: "finite N" "N \<noteq> {}"
  1474   shows "h (F N) = F (h ` N)"
  1475 using N proof (induct rule: finite_ne_induct)
  1476   case singleton thus ?case by simp
  1477 next
  1478   case (insert n N)
  1479   then have "h (F (insert n N)) = h (n * F N)" by simp
  1480   also have "\<dots> = h n * h (F N)" by (rule hom)
  1481   also have "h (F N) = F (h ` N)" by (rule insert)
  1482   also have "h n * \<dots> = F (insert (h n) (h ` N))"
  1483     using insert by simp
  1484   also have "insert (h n) (h ` N) = h ` insert n N" by simp
  1485   finally show ?case .
  1486 qed
  1487 
  1488 end
  1489 
  1490 locale semilattice_order_set = semilattice_order + semilattice_set
  1491 begin
  1492 
  1493 lemma bounded_iff:
  1494   assumes "finite A" and "A \<noteq> {}"
  1495   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
  1496   using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
  1497 
  1498 lemma boundedI:
  1499   assumes "finite A"
  1500   assumes "A \<noteq> {}"
  1501   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1502   shows "x \<preceq> F A"
  1503   using assms by (simp add: bounded_iff)
  1504 
  1505 lemma boundedE:
  1506   assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
  1507   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1508   using assms by (simp add: bounded_iff)
  1509 
  1510 lemma coboundedI:
  1511   assumes "finite A"
  1512     and "a \<in> A"
  1513   shows "F A \<preceq> a"
  1514 proof -
  1515   from assms have "A \<noteq> {}" by auto
  1516   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  1517   proof (induct rule: finite_ne_induct)
  1518     case singleton thus ?case by (simp add: refl)
  1519   next
  1520     case (insert x B)
  1521     from insert have "a = x \<or> a \<in> B" by simp
  1522     then show ?case using insert by (auto intro: coboundedI2)
  1523   qed
  1524 qed
  1525 
  1526 lemma antimono:
  1527   assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
  1528   shows "F B \<preceq> F A"
  1529 proof (cases "A = B")
  1530   case True then show ?thesis by (simp add: refl)
  1531 next
  1532   case False
  1533   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
  1534   then have "F B = F (A \<union> (B - A))" by simp
  1535   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  1536   also have "\<dots> \<preceq> F A" by simp
  1537   finally show ?thesis .
  1538 qed
  1539 
  1540 end
  1541 
  1542 
  1543 subsubsection {* With neutral element *}
  1544 
  1545 locale semilattice_neutr_set = semilattice_neutr
  1546 begin
  1547 
  1548 interpretation comp_fun_idem f
  1549   by default (simp_all add: fun_eq_iff left_commute)
  1550 
  1551 definition F :: "'a set \<Rightarrow> 'a"
  1552 where
  1553   eq_fold: "F A = Finite_Set.fold f 1 A"
  1554 
  1555 lemma infinite [simp]:
  1556   "\<not> finite A \<Longrightarrow> F A = 1"
  1557   by (simp add: eq_fold)
  1558 
  1559 lemma empty [simp]:
  1560   "F {} = 1"
  1561   by (simp add: eq_fold)
  1562 
  1563 lemma insert [simp]:
  1564   assumes "finite A"
  1565   shows "F (insert x A) = x * F A"
  1566   using assms by (simp add: eq_fold)
  1567 
  1568 lemma in_idem:
  1569   assumes "finite A" and "x \<in> A"
  1570   shows "x * F A = F A"
  1571 proof -
  1572   from assms have "A \<noteq> {}" by auto
  1573   with `finite A` show ?thesis using `x \<in> A`
  1574     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
  1575 qed
  1576 
  1577 lemma union:
  1578   assumes "finite A" and "finite B"
  1579   shows "F (A \<union> B) = F A * F B"
  1580   using assms by (induct A) (simp_all add: ac_simps)
  1581 
  1582 lemma remove:
  1583   assumes "finite A" and "x \<in> A"
  1584   shows "F A = x * F (A - {x})"
  1585 proof -
  1586   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
  1587   with assms show ?thesis by simp
  1588 qed
  1589 
  1590 lemma insert_remove:
  1591   assumes "finite A"
  1592   shows "F (insert x A) = x * F (A - {x})"
  1593   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
  1594 
  1595 lemma subset:
  1596   assumes "finite A" and "B \<subseteq> A"
  1597   shows "F B * F A = F A"
  1598 proof -
  1599   from assms have "finite B" by (auto dest: finite_subset)
  1600   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
  1601 qed
  1602 
  1603 lemma closed:
  1604   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
  1605   shows "F A \<in> A"
  1606 using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
  1607   case singleton then show ?case by simp
  1608 next
  1609   case insert with elem show ?case by force
  1610 qed
  1611 
  1612 end
  1613 
  1614 locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
  1615 begin
  1616 
  1617 lemma bounded_iff:
  1618   assumes "finite A"
  1619   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
  1620   using assms by (induct A) (simp_all add: bounded_iff)
  1621 
  1622 lemma boundedI:
  1623   assumes "finite A"
  1624   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1625   shows "x \<preceq> F A"
  1626   using assms by (simp add: bounded_iff)
  1627 
  1628 lemma boundedE:
  1629   assumes "finite A" and "x \<preceq> F A"
  1630   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1631   using assms by (simp add: bounded_iff)
  1632 
  1633 lemma coboundedI:
  1634   assumes "finite A"
  1635     and "a \<in> A"
  1636   shows "F A \<preceq> a"
  1637 proof -
  1638   from assms have "A \<noteq> {}" by auto
  1639   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  1640   proof (induct rule: finite_ne_induct)
  1641     case singleton thus ?case by (simp add: refl)
  1642   next
  1643     case (insert x B)
  1644     from insert have "a = x \<or> a \<in> B" by simp
  1645     then show ?case using insert by (auto intro: coboundedI2)
  1646   qed
  1647 qed
  1648 
  1649 lemma antimono:
  1650   assumes "A \<subseteq> B" and "finite B"
  1651   shows "F B \<preceq> F A"
  1652 proof (cases "A = B")
  1653   case True then show ?thesis by (simp add: refl)
  1654 next
  1655   case False
  1656   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
  1657   then have "F B = F (A \<union> (B - A))" by simp
  1658   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  1659   also have "\<dots> \<preceq> F A" by simp
  1660   finally show ?thesis .
  1661 qed
  1662 
  1663 end
  1664 
  1665 notation times (infixl "*" 70)
  1666 notation Groups.one ("1")
  1667 
  1668 
  1669 subsection {* Lattice operations on finite sets *}
  1670 
  1671 text {*
  1672   For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
  1673   to @{class linorder}.  This is badly designed: both should depend on a common abstract
  1674   distributive lattice rather than having this non-subclass dependecy between two
  1675   classes.  But for the moment we have to live with it.  This forces us to setup
  1676   this sublocale dependency simultaneously with the lattice operations on finite
  1677   sets, to avoid garbage.
  1678 *}
  1679 
  1680 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
  1681 where
  1682   "Inf_fin = semilattice_set.F inf"
  1683 
  1684 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
  1685 where
  1686   "Sup_fin = semilattice_set.F sup"
  1687 
  1688 context linorder
  1689 begin
  1690 
  1691 definition Min :: "'a set \<Rightarrow> 'a"
  1692 where
  1693   "Min = semilattice_set.F min"
  1694 
  1695 definition Max :: "'a set \<Rightarrow> 'a"
  1696 where
  1697   "Max = semilattice_set.F max"
  1698 
  1699 sublocale Min!: semilattice_order_set min less_eq less
  1700   + Max!: semilattice_order_set max greater_eq greater
  1701 where
  1702   "semilattice_set.F min = Min"
  1703   and "semilattice_set.F max = Max"
  1704 proof -
  1705   show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
  1706   then interpret Min!: semilattice_order_set min less_eq less .
  1707   show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
  1708   then interpret Max!: semilattice_order_set max greater_eq greater .
  1709   from Min_def show "semilattice_set.F min = Min" by rule
  1710   from Max_def show "semilattice_set.F max = Max" by rule
  1711 qed
  1712 
  1713 
  1714 text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
  1715 
  1716 sublocale min_max!: distrib_lattice min less_eq less max
  1717 where
  1718   "semilattice_inf.Inf_fin min = Min"
  1719   and "semilattice_sup.Sup_fin max = Max"
  1720 proof -
  1721   show "class.distrib_lattice min less_eq less max"
  1722   proof
  1723     fix x y z
  1724     show "max x (min y z) = min (max x y) (max x z)"
  1725       by (auto simp add: min_def max_def)
  1726   qed (auto simp add: min_def max_def not_le less_imp_le)
  1727   then interpret min_max!: distrib_lattice min less_eq less max .
  1728   show "semilattice_inf.Inf_fin min = Min"
  1729     by (simp only: min_max.Inf_fin_def Min_def)
  1730   show "semilattice_sup.Sup_fin max = Max"
  1731     by (simp only: min_max.Sup_fin_def Max_def)
  1732 qed
  1733 
  1734 lemmas le_maxI1 = min_max.sup_ge1
  1735 lemmas le_maxI2 = min_max.sup_ge2
  1736  
  1737 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
  1738   min.left_commute
  1739 
  1740 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
  1741   max.left_commute
  1742 
  1743 end
  1744 
  1745 
  1746 text {* Lattice operations proper *}
  1747 
  1748 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
  1749 where
  1750   "semilattice_set.F inf = Inf_fin"
  1751 proof -
  1752   show "semilattice_order_set inf less_eq less" ..
  1753   then interpret Inf_fin!: semilattice_order_set inf less_eq less .
  1754   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
  1755 qed
  1756 
  1757 sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
  1758 where
  1759   "semilattice_set.F sup = Sup_fin"
  1760 proof -
  1761   show "semilattice_order_set sup greater_eq greater" ..
  1762   then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
  1763   from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
  1764 qed
  1765 
  1766 
  1767 text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
  1768 
  1769 lemma Inf_fin_Min:
  1770   "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
  1771   by (simp add: Inf_fin_def Min_def inf_min)
  1772 
  1773 lemma Sup_fin_Max:
  1774   "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
  1775   by (simp add: Sup_fin_def Max_def sup_max)
  1776 
  1777 
  1778 
  1779 subsection {* Infimum and Supremum over non-empty sets *}
  1780 
  1781 text {*
  1782   After this non-regular bootstrap, things continue canonically.
  1783 *}
  1784 
  1785 context lattice
  1786 begin
  1787 
  1788 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
  1789 apply(subgoal_tac "EX a. a:A")
  1790 prefer 2 apply blast
  1791 apply(erule exE)
  1792 apply(rule order_trans)
  1793 apply(erule (1) Inf_fin.coboundedI)
  1794 apply(erule (1) Sup_fin.coboundedI)
  1795 done
  1796 
  1797 lemma sup_Inf_absorb [simp]:
  1798   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
  1799 apply(subst sup_commute)
  1800 apply(simp add: sup_absorb2 Inf_fin.coboundedI)
  1801 done
  1802 
  1803 lemma inf_Sup_absorb [simp]:
  1804   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
  1805 by (simp add: inf_absorb1 Sup_fin.coboundedI)
  1806 
  1807 end
  1808 
  1809 context distrib_lattice
  1810 begin
  1811 
  1812 lemma sup_Inf1_distrib:
  1813   assumes "finite A"
  1814     and "A \<noteq> {}"
  1815   shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
  1816 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
  1817   (rule arg_cong [where f="Inf_fin"], blast)
  1818 
  1819 lemma sup_Inf2_distrib:
  1820   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1821   shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B}"
  1822 using A proof (induct rule: finite_ne_induct)
  1823   case singleton then show ?case
  1824     by (simp add: sup_Inf1_distrib [OF B])
  1825 next
  1826   case (insert x A)
  1827   have finB: "finite {sup x b |b. b \<in> B}"
  1828     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
  1829   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  1830   proof -
  1831     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  1832       by blast
  1833     thus ?thesis by(simp add: insert(1) B(1))
  1834   qed
  1835   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1836   have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)"
  1837     using insert by simp
  1838   also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
  1839   also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})"
  1840     using insert by(simp add:sup_Inf1_distrib[OF B])
  1841   also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
  1842     (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
  1843     using B insert
  1844     by (simp add: Inf_fin.union [OF finB _ finAB ne])
  1845   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1846     by blast
  1847   finally show ?case .
  1848 qed
  1849 
  1850 lemma inf_Sup1_distrib:
  1851   assumes "finite A" and "A \<noteq> {}"
  1852   shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
  1853 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
  1854   (rule arg_cong [where f="Sup_fin"], blast)
  1855 
  1856 lemma inf_Sup2_distrib:
  1857   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1858   shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B}"
  1859 using A proof (induct rule: finite_ne_induct)
  1860   case singleton thus ?case
  1861     by(simp add: inf_Sup1_distrib [OF B])
  1862 next
  1863   case (insert x A)
  1864   have finB: "finite {inf x b |b. b \<in> B}"
  1865     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  1866   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  1867   proof -
  1868     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  1869       by blast
  1870     thus ?thesis by(simp add: insert(1) B(1))
  1871   qed
  1872   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1873   have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)"
  1874     using insert by simp
  1875   also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
  1876   also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})"
  1877     using insert by(simp add:inf_Sup1_distrib[OF B])
  1878   also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
  1879     (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
  1880     using B insert
  1881     by (simp add: Sup_fin.union [OF finB _ finAB ne])
  1882   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1883     by blast
  1884   finally show ?case .
  1885 qed
  1886 
  1887 end
  1888 
  1889 context complete_lattice
  1890 begin
  1891 
  1892 lemma Inf_fin_Inf:
  1893   assumes "finite A" and "A \<noteq> {}"
  1894   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
  1895 proof -
  1896   from assms obtain b B where "A = insert b B" and "finite B" by auto
  1897   then show ?thesis
  1898     by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
  1899 qed
  1900 
  1901 lemma Sup_fin_Sup:
  1902   assumes "finite A" and "A \<noteq> {}"
  1903   shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
  1904 proof -
  1905   from assms obtain b B where "A = insert b B" and "finite B" by auto
  1906   then show ?thesis
  1907     by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
  1908 qed
  1909 
  1910 end
  1911 
  1912 
  1913 subsection {* Minimum and Maximum over non-empty sets *}
  1914 
  1915 context linorder
  1916 begin
  1917 
  1918 lemma dual_min:
  1919   "ord.min greater_eq = max"
  1920   by (auto simp add: ord.min_def max_def fun_eq_iff)
  1921 
  1922 lemma dual_max:
  1923   "ord.max greater_eq = min"
  1924   by (auto simp add: ord.max_def min_def fun_eq_iff)
  1925 
  1926 lemma dual_Min:
  1927   "linorder.Min greater_eq = Max"
  1928 proof -
  1929   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
  1930   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
  1931 qed
  1932 
  1933 lemma dual_Max:
  1934   "linorder.Max greater_eq = Min"
  1935 proof -
  1936   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
  1937   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
  1938 qed
  1939 
  1940 lemmas Min_singleton = Min.singleton
  1941 lemmas Max_singleton = Max.singleton
  1942 lemmas Min_insert = Min.insert
  1943 lemmas Max_insert = Max.insert
  1944 lemmas Min_Un = Min.union
  1945 lemmas Max_Un = Max.union
  1946 lemmas hom_Min_commute = Min.hom_commute
  1947 lemmas hom_Max_commute = Max.hom_commute
  1948 
  1949 lemma Min_in [simp]:
  1950   assumes "finite A" and "A \<noteq> {}"
  1951   shows "Min A \<in> A"
  1952   using assms by (auto simp add: min_def Min.closed)
  1953 
  1954 lemma Max_in [simp]:
  1955   assumes "finite A" and "A \<noteq> {}"
  1956   shows "Max A \<in> A"
  1957   using assms by (auto simp add: max_def Max.closed)
  1958 
  1959 lemma Min_le [simp]:
  1960   assumes "finite A" and "x \<in> A"
  1961   shows "Min A \<le> x"
  1962   using assms by (fact Min.coboundedI)
  1963 
  1964 lemma Max_ge [simp]:
  1965   assumes "finite A" and "x \<in> A"
  1966   shows "x \<le> Max A"
  1967   using assms by (fact Max.coboundedI)
  1968 
  1969 lemma Min_eqI:
  1970   assumes "finite A"
  1971   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  1972     and "x \<in> A"
  1973   shows "Min A = x"
  1974 proof (rule antisym)
  1975   from `x \<in> A` have "A \<noteq> {}" by auto
  1976   with assms show "Min A \<ge> x" by simp
  1977 next
  1978   from assms show "x \<ge> Min A" by simp
  1979 qed
  1980 
  1981 lemma Max_eqI:
  1982   assumes "finite A"
  1983   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  1984     and "x \<in> A"
  1985   shows "Max A = x"
  1986 proof (rule antisym)
  1987   from `x \<in> A` have "A \<noteq> {}" by auto
  1988   with assms show "Max A \<le> x" by simp
  1989 next
  1990   from assms show "x \<le> Max A" by simp
  1991 qed
  1992 
  1993 context
  1994   fixes A :: "'a set"
  1995   assumes fin_nonempty: "finite A" "A \<noteq> {}"
  1996 begin
  1997 
  1998 lemma Min_ge_iff [simp]:
  1999   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2000   using fin_nonempty by (fact Min.bounded_iff)
  2001 
  2002 lemma Max_le_iff [simp]:
  2003   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2004   using fin_nonempty by (fact Max.bounded_iff)
  2005 
  2006 lemma Min_gr_iff [simp]:
  2007   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2008   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
  2009 
  2010 lemma Max_less_iff [simp]:
  2011   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  2012   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
  2013 
  2014 lemma Min_le_iff:
  2015   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2016   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
  2017 
  2018 lemma Max_ge_iff:
  2019   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  2020   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
  2021 
  2022 lemma Min_less_iff:
  2023   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2024   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
  2025 
  2026 lemma Max_gr_iff:
  2027   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  2028   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
  2029 
  2030 end
  2031 
  2032 lemma Min_antimono:
  2033   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2034   shows "Min N \<le> Min M"
  2035   using assms by (fact Min.antimono)
  2036 
  2037 lemma Max_mono:
  2038   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2039   shows "Max M \<le> Max N"
  2040   using assms by (fact Max.antimono)
  2041 
  2042 lemma mono_Min_commute:
  2043   assumes "mono f"
  2044   assumes "finite A" and "A \<noteq> {}"
  2045   shows "f (Min A) = Min (f ` A)"
  2046 proof (rule linorder_class.Min_eqI [symmetric])
  2047   from `finite A` show "finite (f ` A)" by simp
  2048   from assms show "f (Min A) \<in> f ` A" by simp
  2049   fix x
  2050   assume "x \<in> f ` A"
  2051   then obtain y where "y \<in> A" and "x = f y" ..
  2052   with assms have "Min A \<le> y" by auto
  2053   with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
  2054   with `x = f y` show "f (Min A) \<le> x" by simp
  2055 qed
  2056 
  2057 lemma mono_Max_commute:
  2058   assumes "mono f"
  2059   assumes "finite A" and "A \<noteq> {}"
  2060   shows "f (Max A) = Max (f ` A)"
  2061 proof (rule linorder_class.Max_eqI [symmetric])
  2062   from `finite A` show "finite (f ` A)" by simp
  2063   from assms show "f (Max A) \<in> f ` A" by simp
  2064   fix x
  2065   assume "x \<in> f ` A"
  2066   then obtain y where "y \<in> A" and "x = f y" ..
  2067   with assms have "y \<le> Max A" by auto
  2068   with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
  2069   with `x = f y` show "x \<le> f (Max A)" by simp
  2070 qed
  2071 
  2072 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
  2073   assumes fin: "finite A"
  2074   and empty: "P {}" 
  2075   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
  2076   shows "P A"
  2077 using fin empty insert
  2078 proof (induct rule: finite_psubset_induct)
  2079   case (psubset A)
  2080   have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
  2081   have fin: "finite A" by fact 
  2082   have empty: "P {}" by fact
  2083   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
  2084   show "P A"
  2085   proof (cases "A = {}")
  2086     assume "A = {}" 
  2087     then show "P A" using `P {}` by simp
  2088   next
  2089     let ?B = "A - {Max A}" 
  2090     let ?A = "insert (Max A) ?B"
  2091     have "finite ?B" using `finite A` by simp
  2092     assume "A \<noteq> {}"
  2093     with `finite A` have "Max A : A" by auto
  2094     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
  2095     then have "P ?B" using `P {}` step IH [of ?B] by blast
  2096     moreover 
  2097     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
  2098     ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
  2099   qed
  2100 qed
  2101 
  2102 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
  2103   "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
  2104   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
  2105 
  2106 lemma Least_Min:
  2107   assumes "finite {a. P a}" and "\<exists>a. P a"
  2108   shows "(LEAST a. P a) = Min {a. P a}"
  2109 proof -
  2110   { fix A :: "'a set"
  2111     assume A: "finite A" "A \<noteq> {}"
  2112     have "(LEAST a. a \<in> A) = Min A"
  2113     using A proof (induct A rule: finite_ne_induct)
  2114       case singleton show ?case by (rule Least_equality) simp_all
  2115     next
  2116       case (insert a A)
  2117       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
  2118         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
  2119       with insert show ?case by simp
  2120     qed
  2121   } from this [of "{a. P a}"] assms show ?thesis by simp
  2122 qed
  2123 
  2124 end
  2125 
  2126 context linordered_ab_semigroup_add
  2127 begin
  2128 
  2129 lemma add_Min_commute:
  2130   fixes k
  2131   assumes "finite N" and "N \<noteq> {}"
  2132   shows "k + Min N = Min {k + m | m. m \<in> N}"
  2133 proof -
  2134   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  2135     by (simp add: min_def not_le)
  2136       (blast intro: antisym less_imp_le add_left_mono)
  2137   with assms show ?thesis
  2138     using hom_Min_commute [of "plus k" N]
  2139     by simp (blast intro: arg_cong [where f = Min])
  2140 qed
  2141 
  2142 lemma add_Max_commute:
  2143   fixes k
  2144   assumes "finite N" and "N \<noteq> {}"
  2145   shows "k + Max N = Max {k + m | m. m \<in> N}"
  2146 proof -
  2147   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  2148     by (simp add: max_def not_le)
  2149       (blast intro: antisym less_imp_le add_left_mono)
  2150   with assms show ?thesis
  2151     using hom_Max_commute [of "plus k" N]
  2152     by simp (blast intro: arg_cong [where f = Max])
  2153 qed
  2154 
  2155 end
  2156 
  2157 context linordered_ab_group_add
  2158 begin
  2159 
  2160 lemma minus_Max_eq_Min [simp]:
  2161   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
  2162   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  2163 
  2164 lemma minus_Min_eq_Max [simp]:
  2165   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
  2166   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  2167 
  2168 end
  2169 
  2170 context complete_linorder
  2171 begin
  2172 
  2173 lemma Min_Inf:
  2174   assumes "finite A" and "A \<noteq> {}"
  2175   shows "Min A = Inf A"
  2176 proof -
  2177   from assms obtain b B where "A = insert b B" and "finite B" by auto
  2178   then show ?thesis
  2179     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
  2180 qed
  2181 
  2182 lemma Max_Sup:
  2183   assumes "finite A" and "A \<noteq> {}"
  2184   shows "Max A = Sup A"
  2185 proof -
  2186   from assms obtain b B where "A = insert b B" and "finite B" by auto
  2187   then show ?thesis
  2188     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
  2189 qed
  2190 
  2191 end
  2192 
  2193 end