src/HOL/Big_Operators.thy
author wenzelm
Tue Sep 03 01:12:40 2013 +0200 (2013-09-03)
changeset 53374 a14d2a854c02
parent 53174 71a2702da5e0
child 54147 97a8ff4e4ac9
permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
     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 Option 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 proof (cases "finite A")
   700   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
   701 next
   702   case False thus ?thesis by simp
   703 qed
   704 
   705 lemma setsum_nonneg:
   706   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   707   shows "0 \<le> setsum f A"
   708 proof (cases "finite A")
   709   case True thus ?thesis using nn
   710   proof induct
   711     case empty then show ?case by simp
   712   next
   713     case (insert x F)
   714     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   715     with insert show ?case by simp
   716   qed
   717 next
   718   case False thus ?thesis by simp
   719 qed
   720 
   721 lemma setsum_nonpos:
   722   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   723   shows "setsum f A \<le> 0"
   724 proof (cases "finite A")
   725   case True thus ?thesis using np
   726   proof induct
   727     case empty then show ?case by simp
   728   next
   729     case (insert x F)
   730     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   731     with insert show ?case by simp
   732   qed
   733 next
   734   case False thus ?thesis by simp
   735 qed
   736 
   737 lemma setsum_nonneg_leq_bound:
   738   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   739   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   740   shows "f i \<le> B"
   741 proof -
   742   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   743     using assms by (auto intro!: setsum_nonneg)
   744   moreover
   745   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   746     using assms by (simp add: setsum_diff1)
   747   ultimately show ?thesis by auto
   748 qed
   749 
   750 lemma setsum_nonneg_0:
   751   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   752   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   753   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   754   shows "f i = 0"
   755   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   756 
   757 lemma setsum_mono2:
   758 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   759 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   760 shows "setsum f A \<le> setsum f B"
   761 proof -
   762   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   763     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   764   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   765     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   766   also have "A \<union> (B-A) = B" using sub by blast
   767   finally show ?thesis .
   768 qed
   769 
   770 lemma setsum_mono3: "finite B ==> A <= B ==> 
   771     ALL x: B - A. 
   772       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   773         setsum f A <= setsum f B"
   774   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   775   apply (erule ssubst)
   776   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   777   apply simp
   778   apply (rule add_left_mono)
   779   apply (erule setsum_nonneg)
   780   apply (subst setsum_Un_disjoint [THEN sym])
   781   apply (erule finite_subset, assumption)
   782   apply (rule finite_subset)
   783   prefer 2
   784   apply assumption
   785   apply (auto simp add: sup_absorb2)
   786 done
   787 
   788 lemma setsum_right_distrib: 
   789   fixes f :: "'a => ('b::semiring_0)"
   790   shows "r * setsum f A = setsum (%n. r * f n) A"
   791 proof (cases "finite A")
   792   case True
   793   thus ?thesis
   794   proof induct
   795     case empty thus ?case by simp
   796   next
   797     case (insert x A) thus ?case by (simp add: distrib_left)
   798   qed
   799 next
   800   case False thus ?thesis by simp
   801 qed
   802 
   803 lemma setsum_left_distrib:
   804   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   805 proof (cases "finite A")
   806   case True
   807   then show ?thesis
   808   proof induct
   809     case empty thus ?case by simp
   810   next
   811     case (insert x A) thus ?case by (simp add: distrib_right)
   812   qed
   813 next
   814   case False thus ?thesis by simp
   815 qed
   816 
   817 lemma setsum_divide_distrib:
   818   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   819 proof (cases "finite A")
   820   case True
   821   then show ?thesis
   822   proof induct
   823     case empty thus ?case by simp
   824   next
   825     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   826   qed
   827 next
   828   case False thus ?thesis by simp
   829 qed
   830 
   831 lemma setsum_abs[iff]: 
   832   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   833   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   834 proof (cases "finite A")
   835   case True
   836   thus ?thesis
   837   proof induct
   838     case empty thus ?case by simp
   839   next
   840     case (insert x A)
   841     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   842   qed
   843 next
   844   case False thus ?thesis by simp
   845 qed
   846 
   847 lemma setsum_abs_ge_zero[iff]: 
   848   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   849   shows "0 \<le> setsum (%i. abs(f i)) A"
   850 proof (cases "finite A")
   851   case True
   852   thus ?thesis
   853   proof induct
   854     case empty thus ?case by simp
   855   next
   856     case (insert x A) thus ?case by auto
   857   qed
   858 next
   859   case False thus ?thesis by simp
   860 qed
   861 
   862 lemma abs_setsum_abs[simp]: 
   863   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   864   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   865 proof (cases "finite A")
   866   case True
   867   thus ?thesis
   868   proof induct
   869     case empty thus ?case by simp
   870   next
   871     case (insert a A)
   872     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
   873     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   874     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   875       by (simp del: abs_of_nonneg)
   876     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   877     finally show ?case .
   878   qed
   879 next
   880   case False thus ?thesis by simp
   881 qed
   882 
   883 lemma setsum_diff1'[rule_format]:
   884   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   885 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))"])
   886 apply (auto simp add: insert_Diff_if add_ac)
   887 done
   888 
   889 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   890   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   891 unfolding setsum_diff1'[OF assms] by auto
   892 
   893 lemma setsum_product:
   894   fixes f :: "'a => ('b::semiring_0)"
   895   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   896   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   897 
   898 lemma setsum_mult_setsum_if_inj:
   899 fixes f :: "'a => ('b::semiring_0)"
   900 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   901   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   902 by(auto simp: setsum_product setsum_cartesian_product
   903         intro!:  setsum_reindex_cong[symmetric])
   904 
   905 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   906 apply (case_tac "finite A")
   907  prefer 2 apply simp
   908 apply (erule rev_mp)
   909 apply (erule finite_induct, auto)
   910 done
   911 
   912 lemma setsum_eq_0_iff [simp]:
   913   "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   914   by (induct set: finite) auto
   915 
   916 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   917   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   918 apply(erule finite_induct)
   919 apply (auto simp add:add_is_1)
   920 done
   921 
   922 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   923 
   924 lemma setsum_Un_nat: "finite A ==> finite B ==>
   925   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   926   -- {* For the natural numbers, we have subtraction. *}
   927 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   928 
   929 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   930   (if a:A then setsum f A - f a else setsum f A)"
   931 apply (case_tac "finite A")
   932  prefer 2 apply simp
   933 apply (erule finite_induct)
   934  apply (auto simp add: insert_Diff_if)
   935 apply (drule_tac a = a in mk_disjoint_insert, auto)
   936 done
   937 
   938 lemma setsum_diff_nat: 
   939 assumes "finite B" and "B \<subseteq> A"
   940 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   941 using assms
   942 proof induct
   943   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   944 next
   945   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   946     and xFinA: "insert x F \<subseteq> A"
   947     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   948   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   949   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   950     by (simp add: setsum_diff1_nat)
   951   from xFinA have "F \<subseteq> A" by simp
   952   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   953   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   954     by simp
   955   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   956   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   957     by simp
   958   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   959   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   960     by simp
   961   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   962 qed
   963 
   964 lemma setsum_comp_morphism:
   965   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   966   shows "setsum (h \<circ> g) A = h (setsum g A)"
   967 proof (cases "finite A")
   968   case False then show ?thesis by (simp add: assms)
   969 next
   970   case True then show ?thesis by (induct A) (simp_all add: assms)
   971 qed
   972 
   973 
   974 subsubsection {* Cardinality as special case of @{const setsum} *}
   975 
   976 lemma card_eq_setsum:
   977   "card A = setsum (\<lambda>x. 1) A"
   978 proof -
   979   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   980     by (simp add: fun_eq_iff)
   981   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   982     by (rule arg_cong)
   983   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   984     by (blast intro: fun_cong)
   985   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   986 qed
   987 
   988 lemma setsum_constant [simp]:
   989   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   990 apply (cases "finite A")
   991 apply (erule finite_induct)
   992 apply (auto simp add: algebra_simps)
   993 done
   994 
   995 lemma setsum_bounded:
   996   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   997   shows "setsum f A \<le> of_nat (card A) * K"
   998 proof (cases "finite A")
   999   case True
  1000   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  1001 next
  1002   case False thus ?thesis by simp
  1003 qed
  1004 
  1005 lemma card_UN_disjoint:
  1006   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
  1007     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
  1008   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1009 proof -
  1010   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
  1011   with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
  1012 qed
  1013 
  1014 lemma card_Union_disjoint:
  1015   "finite C ==> (ALL A:C. finite A) ==>
  1016    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  1017    ==> card (Union C) = setsum card C"
  1018 apply (frule card_UN_disjoint [of C id])
  1019 apply (simp_all add: SUP_def id_def)
  1020 done
  1021 
  1022 
  1023 subsubsection {* Cardinality of products *}
  1024 
  1025 lemma card_SigmaI [simp]:
  1026   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1027   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1028 by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
  1029 
  1030 (*
  1031 lemma SigmaI_insert: "y \<notin> A ==>
  1032   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1033   by auto
  1034 *)
  1035 
  1036 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1037   by (cases "finite A \<and> finite B")
  1038     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1039 
  1040 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1041 by (simp add: card_cartesian_product)
  1042 
  1043 
  1044 subsection {* Generalized product over a set *}
  1045 
  1046 context comm_monoid_mult
  1047 begin
  1048 
  1049 definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  1050 where
  1051   "setprod = comm_monoid_set.F times 1"
  1052 
  1053 sublocale setprod!: comm_monoid_set times 1
  1054 where
  1055   "comm_monoid_set.F times 1 = setprod"
  1056 proof -
  1057   show "comm_monoid_set times 1" ..
  1058   then interpret setprod!: comm_monoid_set times 1 .
  1059   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  1060 qed
  1061 
  1062 abbreviation
  1063   Setprod ("\<Prod>_" [1000] 999) where
  1064   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1065 
  1066 end
  1067 
  1068 syntax
  1069   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1070 syntax (xsymbols)
  1071   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1072 syntax (HTML output)
  1073   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1074 
  1075 translations -- {* Beware of argument permutation! *}
  1076   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1077   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1078 
  1079 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1080  @{text"\<Prod>x|P. e"}. *}
  1081 
  1082 syntax
  1083   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1084 syntax (xsymbols)
  1085   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1086 syntax (HTML output)
  1087   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1088 
  1089 translations
  1090   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1091   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1092 
  1093 text {* TODO These are candidates for generalization *}
  1094 
  1095 context comm_monoid_mult
  1096 begin
  1097 
  1098 lemma setprod_reindex_id:
  1099   "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1100   by (auto simp add: setprod.reindex)
  1101 
  1102 lemma setprod_reindex_cong:
  1103   "inj_on f A ==> B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1104   by (frule setprod.reindex, simp)
  1105 
  1106 lemma strong_setprod_reindex_cong:
  1107   assumes i: "inj_on f A"
  1108   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
  1109   shows "setprod h B = setprod g A"
  1110 proof-
  1111   have "setprod h B = setprod (h o f) A"
  1112     by (simp add: B setprod.reindex [OF i, of h])
  1113   then show ?thesis apply simp
  1114     apply (rule setprod.cong)
  1115     apply simp
  1116     by (simp add: eq)
  1117 qed
  1118 
  1119 lemma setprod_Union_disjoint:
  1120   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  1121   shows "setprod f (Union C) = setprod (setprod f) C"
  1122   using assms by (fact setprod.Union_disjoint)
  1123 
  1124 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1125 lemma setprod_cartesian_product:
  1126   "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1127   by (fact setprod.cartesian_product)
  1128 
  1129 lemma setprod_Un2:
  1130   assumes "finite (A \<union> B)"
  1131   shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
  1132 proof -
  1133   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
  1134     by auto
  1135   with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+
  1136 qed
  1137 
  1138 end
  1139 
  1140 text {* TODO These are legacy *}
  1141 
  1142 lemma setprod_empty: "setprod f {} = 1"
  1143   by (fact setprod.empty)
  1144 
  1145 lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
  1146     setprod f (insert a A) = f a * setprod f A"
  1147   by (fact setprod.insert)
  1148 
  1149 lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
  1150   by (fact setprod.infinite)
  1151 
  1152 lemma setprod_reindex:
  1153   "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1154   by (fact setprod.reindex)
  1155 
  1156 lemma setprod_cong:
  1157   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1158   by (fact setprod.cong)
  1159 
  1160 lemma strong_setprod_cong:
  1161   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1162   by (fact setprod.strong_cong)
  1163 
  1164 lemma setprod_Un_one:
  1165   "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
  1166   \<Longrightarrow> setprod f (S \<union> T) = setprod f S  * setprod f T"
  1167   by (fact setprod.union_inter_neutral)
  1168 
  1169 lemmas setprod_1 = setprod.neutral_const
  1170 lemmas setprod_1' = setprod.neutral
  1171 
  1172 lemma setprod_Un_Int: "finite A ==> finite B
  1173     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1174   by (fact setprod.union_inter)
  1175 
  1176 lemma setprod_Un_disjoint: "finite A ==> finite B
  1177   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1178   by (fact setprod.union_disjoint)
  1179 
  1180 lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
  1181     setprod f A = setprod f (A - B) * setprod f B"
  1182   by (fact setprod.subset_diff)
  1183 
  1184 lemma setprod_mono_one_left:
  1185   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
  1186   by (fact setprod.mono_neutral_left)
  1187 
  1188 lemmas setprod_mono_one_right = setprod.mono_neutral_right
  1189 
  1190 lemma setprod_mono_one_cong_left: 
  1191   "\<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>
  1192   \<Longrightarrow> setprod f S = setprod g T"
  1193   by (fact setprod.mono_neutral_cong_left)
  1194 
  1195 lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right
  1196 
  1197 lemma setprod_delta: "finite S \<Longrightarrow>
  1198   setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  1199   by (fact setprod.delta)
  1200 
  1201 lemma setprod_delta': "finite S \<Longrightarrow>
  1202   setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
  1203   by (fact setprod.delta')
  1204 
  1205 lemma setprod_UN_disjoint:
  1206     "finite I ==> (ALL i:I. finite (A i)) ==>
  1207         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1208       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1209   by (fact setprod.UNION_disjoint)
  1210 
  1211 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1212     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1213     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1214   by (fact setprod.Sigma)
  1215 
  1216 lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A = setprod f A * setprod g A"
  1217   by (fact setprod.distrib)
  1218 
  1219 
  1220 subsubsection {* Properties in more restricted classes of structures *}
  1221 
  1222 lemma setprod_zero:
  1223      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1224 apply (induct set: finite, force, clarsimp)
  1225 apply (erule disjE, auto)
  1226 done
  1227 
  1228 lemma setprod_zero_iff[simp]: "finite A ==> 
  1229   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1230   (EX x: A. f x = 0)"
  1231 by (erule finite_induct, auto simp:no_zero_divisors)
  1232 
  1233 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1234   (setprod f (A Un B) :: 'a ::{field})
  1235    = setprod f A * setprod f B / setprod f (A Int B)"
  1236 by (subst setprod_Un_Int [symmetric], auto)
  1237 
  1238 lemma setprod_nonneg [rule_format]:
  1239    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1240 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  1241 
  1242 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  1243   --> 0 < setprod f A"
  1244 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  1245 
  1246 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1247   (setprod f (A - {a}) :: 'a :: {field}) =
  1248   (if a:A then setprod f A / f a else setprod f A)"
  1249   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1250 
  1251 lemma setprod_inversef: 
  1252   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1253   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1254 by (erule finite_induct) auto
  1255 
  1256 lemma setprod_dividef:
  1257   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1258   shows "finite A
  1259     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1260 apply (subgoal_tac
  1261          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1262 apply (erule ssubst)
  1263 apply (subst divide_inverse)
  1264 apply (subst setprod_timesf)
  1265 apply (subst setprod_inversef, assumption+, rule refl)
  1266 apply (rule setprod_cong, rule refl)
  1267 apply (subst divide_inverse, auto)
  1268 done
  1269 
  1270 lemma setprod_dvd_setprod [rule_format]: 
  1271     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1272   apply (cases "finite A")
  1273   apply (induct set: finite)
  1274   apply (auto simp add: dvd_def)
  1275   apply (rule_tac x = "k * ka" in exI)
  1276   apply (simp add: algebra_simps)
  1277 done
  1278 
  1279 lemma setprod_dvd_setprod_subset:
  1280   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1281   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1282   apply (unfold dvd_def, blast)
  1283   apply (subst setprod_Un_disjoint [symmetric])
  1284   apply (auto elim: finite_subset intro: setprod_cong)
  1285 done
  1286 
  1287 lemma setprod_dvd_setprod_subset2:
  1288   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1289       setprod f A dvd setprod g B"
  1290   apply (rule dvd_trans)
  1291   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1292   apply (erule (1) setprod_dvd_setprod_subset)
  1293 done
  1294 
  1295 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1296     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1297 by (induct set: finite) (auto intro: dvd_mult)
  1298 
  1299 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1300     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1301   apply (cases "finite A")
  1302   apply (induct set: finite)
  1303   apply auto
  1304 done
  1305 
  1306 lemma setprod_mono:
  1307   fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  1308   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1309   shows "setprod f A \<le> setprod g A"
  1310 proof (cases "finite A")
  1311   case True
  1312   hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  1313   proof (induct A rule: finite_subset_induct)
  1314     case (insert a F)
  1315     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  1316       unfolding setprod_insert[OF insert(1,3)]
  1317       using assms[rule_format,OF insert(2)] insert
  1318       by (auto intro: mult_mono mult_nonneg_nonneg)
  1319   qed auto
  1320   thus ?thesis by simp
  1321 qed auto
  1322 
  1323 lemma abs_setprod:
  1324   fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  1325   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  1326 proof (cases "finite A")
  1327   case True thus ?thesis
  1328     by induct (auto simp add: field_simps abs_mult)
  1329 qed auto
  1330 
  1331 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  1332 apply (erule finite_induct)
  1333 apply auto
  1334 done
  1335 
  1336 lemma setprod_gen_delta:
  1337   assumes fS: "finite S"
  1338   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)"
  1339 proof-
  1340   let ?f = "(\<lambda>k. if k=a then b k else c)"
  1341   {assume a: "a \<notin> S"
  1342     hence "\<forall> k\<in> S. ?f k = c" by simp
  1343     hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
  1344   moreover 
  1345   {assume a: "a \<in> S"
  1346     let ?A = "S - {a}"
  1347     let ?B = "{a}"
  1348     have eq: "S = ?A \<union> ?B" using a by blast 
  1349     have dj: "?A \<inter> ?B = {}" by simp
  1350     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1351     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  1352       apply (rule setprod_cong) by auto
  1353     have cA: "card ?A = card S - 1" using fS a by auto
  1354     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  1355     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1356       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1357       by simp
  1358     then have ?thesis using a cA
  1359       by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
  1360   ultimately show ?thesis by blast
  1361 qed
  1362 
  1363 lemma setprod_eq_1_iff [simp]:
  1364   "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
  1365   by (induct set: finite) auto
  1366 
  1367 lemma setprod_pos_nat:
  1368   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1369 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1370 
  1371 lemma setprod_pos_nat_iff[simp]:
  1372   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1373 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1374 
  1375 
  1376 subsection {* Generic lattice operations over a set *}
  1377 
  1378 no_notation times (infixl "*" 70)
  1379 no_notation Groups.one ("1")
  1380 
  1381 
  1382 subsubsection {* Without neutral element *}
  1383 
  1384 locale semilattice_set = semilattice
  1385 begin
  1386 
  1387 interpretation comp_fun_idem f
  1388   by default (simp_all add: fun_eq_iff left_commute)
  1389 
  1390 definition F :: "'a set \<Rightarrow> 'a"
  1391 where
  1392   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)"
  1393 
  1394 lemma eq_fold:
  1395   assumes "finite A"
  1396   shows "F (insert x A) = Finite_Set.fold f x A"
  1397 proof (rule sym)
  1398   let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
  1399   interpret comp_fun_idem "?f"
  1400     by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
  1401   from assms show "Finite_Set.fold f x A = F (insert x A)"
  1402   proof induct
  1403     case empty then show ?case by (simp add: eq_fold')
  1404   next
  1405     case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
  1406   qed
  1407 qed
  1408 
  1409 lemma singleton [simp]:
  1410   "F {x} = x"
  1411   by (simp add: eq_fold)
  1412 
  1413 lemma insert_not_elem:
  1414   assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
  1415   shows "F (insert x A) = x * F A"
  1416 proof -
  1417   from `A \<noteq> {}` obtain b where "b \<in> A" by blast
  1418   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
  1419   with `finite A` and `x \<notin> A`
  1420     have "finite (insert x B)" and "b \<notin> insert x B" by auto
  1421   then have "F (insert b (insert x B)) = x * F (insert b B)"
  1422     by (simp add: eq_fold)
  1423   then show ?thesis by (simp add: * insert_commute)
  1424 qed
  1425 
  1426 lemma in_idem:
  1427   assumes "finite A" and "x \<in> A"
  1428   shows "x * F A = F A"
  1429 proof -
  1430   from assms have "A \<noteq> {}" by auto
  1431   with `finite A` show ?thesis using `x \<in> A`
  1432     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
  1433 qed
  1434 
  1435 lemma insert [simp]:
  1436   assumes "finite A" and "A \<noteq> {}"
  1437   shows "F (insert x A) = x * F A"
  1438   using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
  1439 
  1440 lemma union:
  1441   assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
  1442   shows "F (A \<union> B) = F A * F B"
  1443   using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
  1444 
  1445 lemma remove:
  1446   assumes "finite A" and "x \<in> A"
  1447   shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
  1448 proof -
  1449   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
  1450   with assms show ?thesis by simp
  1451 qed
  1452 
  1453 lemma insert_remove:
  1454   assumes "finite A"
  1455   shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
  1456   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
  1457 
  1458 lemma subset:
  1459   assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
  1460   shows "F B * F A = F A"
  1461 proof -
  1462   from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
  1463   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
  1464 qed
  1465 
  1466 lemma closed:
  1467   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
  1468   shows "F A \<in> A"
  1469 using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
  1470   case singleton then show ?case by simp
  1471 next
  1472   case insert with elem show ?case by force
  1473 qed
  1474 
  1475 lemma hom_commute:
  1476   assumes hom: "\<And>x y. h (x * y) = h x * h y"
  1477   and N: "finite N" "N \<noteq> {}"
  1478   shows "h (F N) = F (h ` N)"
  1479 using N proof (induct rule: finite_ne_induct)
  1480   case singleton thus ?case by simp
  1481 next
  1482   case (insert n N)
  1483   then have "h (F (insert n N)) = h (n * F N)" by simp
  1484   also have "\<dots> = h n * h (F N)" by (rule hom)
  1485   also have "h (F N) = F (h ` N)" by (rule insert)
  1486   also have "h n * \<dots> = F (insert (h n) (h ` N))"
  1487     using insert by simp
  1488   also have "insert (h n) (h ` N) = h ` insert n N" by simp
  1489   finally show ?case .
  1490 qed
  1491 
  1492 end
  1493 
  1494 locale semilattice_order_set = semilattice_order + semilattice_set
  1495 begin
  1496 
  1497 lemma bounded_iff:
  1498   assumes "finite A" and "A \<noteq> {}"
  1499   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
  1500   using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
  1501 
  1502 lemma boundedI:
  1503   assumes "finite A"
  1504   assumes "A \<noteq> {}"
  1505   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1506   shows "x \<preceq> F A"
  1507   using assms by (simp add: bounded_iff)
  1508 
  1509 lemma boundedE:
  1510   assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
  1511   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1512   using assms by (simp add: bounded_iff)
  1513 
  1514 lemma coboundedI:
  1515   assumes "finite A"
  1516     and "a \<in> A"
  1517   shows "F A \<preceq> a"
  1518 proof -
  1519   from assms have "A \<noteq> {}" by auto
  1520   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  1521   proof (induct rule: finite_ne_induct)
  1522     case singleton thus ?case by (simp add: refl)
  1523   next
  1524     case (insert x B)
  1525     from insert have "a = x \<or> a \<in> B" by simp
  1526     then show ?case using insert by (auto intro: coboundedI2)
  1527   qed
  1528 qed
  1529 
  1530 lemma antimono:
  1531   assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
  1532   shows "F B \<preceq> F A"
  1533 proof (cases "A = B")
  1534   case True then show ?thesis by (simp add: refl)
  1535 next
  1536   case False
  1537   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
  1538   then have "F B = F (A \<union> (B - A))" by simp
  1539   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  1540   also have "\<dots> \<preceq> F A" by simp
  1541   finally show ?thesis .
  1542 qed
  1543 
  1544 end
  1545 
  1546 
  1547 subsubsection {* With neutral element *}
  1548 
  1549 locale semilattice_neutr_set = semilattice_neutr
  1550 begin
  1551 
  1552 interpretation comp_fun_idem f
  1553   by default (simp_all add: fun_eq_iff left_commute)
  1554 
  1555 definition F :: "'a set \<Rightarrow> 'a"
  1556 where
  1557   eq_fold: "F A = Finite_Set.fold f 1 A"
  1558 
  1559 lemma infinite [simp]:
  1560   "\<not> finite A \<Longrightarrow> F A = 1"
  1561   by (simp add: eq_fold)
  1562 
  1563 lemma empty [simp]:
  1564   "F {} = 1"
  1565   by (simp add: eq_fold)
  1566 
  1567 lemma insert [simp]:
  1568   assumes "finite A"
  1569   shows "F (insert x A) = x * F A"
  1570   using assms by (simp add: eq_fold)
  1571 
  1572 lemma in_idem:
  1573   assumes "finite A" and "x \<in> A"
  1574   shows "x * F A = F A"
  1575 proof -
  1576   from assms have "A \<noteq> {}" by auto
  1577   with `finite A` show ?thesis using `x \<in> A`
  1578     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
  1579 qed
  1580 
  1581 lemma union:
  1582   assumes "finite A" and "finite B"
  1583   shows "F (A \<union> B) = F A * F B"
  1584   using assms by (induct A) (simp_all add: ac_simps)
  1585 
  1586 lemma remove:
  1587   assumes "finite A" and "x \<in> A"
  1588   shows "F A = x * F (A - {x})"
  1589 proof -
  1590   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
  1591   with assms show ?thesis by simp
  1592 qed
  1593 
  1594 lemma insert_remove:
  1595   assumes "finite A"
  1596   shows "F (insert x A) = x * F (A - {x})"
  1597   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
  1598 
  1599 lemma subset:
  1600   assumes "finite A" and "B \<subseteq> A"
  1601   shows "F B * F A = F A"
  1602 proof -
  1603   from assms have "finite B" by (auto dest: finite_subset)
  1604   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
  1605 qed
  1606 
  1607 lemma closed:
  1608   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
  1609   shows "F A \<in> A"
  1610 using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
  1611   case singleton then show ?case by simp
  1612 next
  1613   case insert with elem show ?case by force
  1614 qed
  1615 
  1616 end
  1617 
  1618 locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
  1619 begin
  1620 
  1621 lemma bounded_iff:
  1622   assumes "finite A"
  1623   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
  1624   using assms by (induct A) (simp_all add: bounded_iff)
  1625 
  1626 lemma boundedI:
  1627   assumes "finite A"
  1628   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1629   shows "x \<preceq> F A"
  1630   using assms by (simp add: bounded_iff)
  1631 
  1632 lemma boundedE:
  1633   assumes "finite A" and "x \<preceq> F A"
  1634   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  1635   using assms by (simp add: bounded_iff)
  1636 
  1637 lemma coboundedI:
  1638   assumes "finite A"
  1639     and "a \<in> A"
  1640   shows "F A \<preceq> a"
  1641 proof -
  1642   from assms have "A \<noteq> {}" by auto
  1643   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  1644   proof (induct rule: finite_ne_induct)
  1645     case singleton thus ?case by (simp add: refl)
  1646   next
  1647     case (insert x B)
  1648     from insert have "a = x \<or> a \<in> B" by simp
  1649     then show ?case using insert by (auto intro: coboundedI2)
  1650   qed
  1651 qed
  1652 
  1653 lemma antimono:
  1654   assumes "A \<subseteq> B" and "finite B"
  1655   shows "F B \<preceq> F A"
  1656 proof (cases "A = B")
  1657   case True then show ?thesis by (simp add: refl)
  1658 next
  1659   case False
  1660   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
  1661   then have "F B = F (A \<union> (B - A))" by simp
  1662   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  1663   also have "\<dots> \<preceq> F A" by simp
  1664   finally show ?thesis .
  1665 qed
  1666 
  1667 end
  1668 
  1669 notation times (infixl "*" 70)
  1670 notation Groups.one ("1")
  1671 
  1672 
  1673 subsection {* Lattice operations on finite sets *}
  1674 
  1675 text {*
  1676   For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
  1677   to @{class linorder}.  This is badly designed: both should depend on a common abstract
  1678   distributive lattice rather than having this non-subclass dependecy between two
  1679   classes.  But for the moment we have to live with it.  This forces us to setup
  1680   this sublocale dependency simultaneously with the lattice operations on finite
  1681   sets, to avoid garbage.
  1682 *}
  1683 
  1684 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
  1685 where
  1686   "Inf_fin = semilattice_set.F inf"
  1687 
  1688 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
  1689 where
  1690   "Sup_fin = semilattice_set.F sup"
  1691 
  1692 context linorder
  1693 begin
  1694 
  1695 definition Min :: "'a set \<Rightarrow> 'a"
  1696 where
  1697   "Min = semilattice_set.F min"
  1698 
  1699 definition Max :: "'a set \<Rightarrow> 'a"
  1700 where
  1701   "Max = semilattice_set.F max"
  1702 
  1703 sublocale Min!: semilattice_order_set min less_eq less
  1704   + Max!: semilattice_order_set max greater_eq greater
  1705 where
  1706   "semilattice_set.F min = Min"
  1707   and "semilattice_set.F max = Max"
  1708 proof -
  1709   show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
  1710   then interpret Min!: semilattice_order_set min less_eq less .
  1711   show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
  1712   then interpret Max!: semilattice_order_set max greater_eq greater .
  1713   from Min_def show "semilattice_set.F min = Min" by rule
  1714   from Max_def show "semilattice_set.F max = Max" by rule
  1715 qed
  1716 
  1717 
  1718 text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
  1719 
  1720 sublocale min_max!: distrib_lattice min less_eq less max
  1721 where
  1722   "semilattice_inf.Inf_fin min = Min"
  1723   and "semilattice_sup.Sup_fin max = Max"
  1724 proof -
  1725   show "class.distrib_lattice min less_eq less max"
  1726   proof
  1727     fix x y z
  1728     show "max x (min y z) = min (max x y) (max x z)"
  1729       by (auto simp add: min_def max_def)
  1730   qed (auto simp add: min_def max_def not_le less_imp_le)
  1731   then interpret min_max!: distrib_lattice min less_eq less max .
  1732   show "semilattice_inf.Inf_fin min = Min"
  1733     by (simp only: min_max.Inf_fin_def Min_def)
  1734   show "semilattice_sup.Sup_fin max = Max"
  1735     by (simp only: min_max.Sup_fin_def Max_def)
  1736 qed
  1737 
  1738 lemmas le_maxI1 = min_max.sup_ge1
  1739 lemmas le_maxI2 = min_max.sup_ge2
  1740  
  1741 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
  1742   min.left_commute
  1743 
  1744 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
  1745   max.left_commute
  1746 
  1747 end
  1748 
  1749 
  1750 text {* Lattice operations proper *}
  1751 
  1752 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
  1753 where
  1754   "semilattice_set.F inf = Inf_fin"
  1755 proof -
  1756   show "semilattice_order_set inf less_eq less" ..
  1757   then interpret Inf_fin!: semilattice_order_set inf less_eq less .
  1758   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
  1759 qed
  1760 
  1761 sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
  1762 where
  1763   "semilattice_set.F sup = Sup_fin"
  1764 proof -
  1765   show "semilattice_order_set sup greater_eq greater" ..
  1766   then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
  1767   from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
  1768 qed
  1769 
  1770 
  1771 text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
  1772 
  1773 lemma Inf_fin_Min:
  1774   "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
  1775   by (simp add: Inf_fin_def Min_def inf_min)
  1776 
  1777 lemma Sup_fin_Max:
  1778   "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
  1779   by (simp add: Sup_fin_def Max_def sup_max)
  1780 
  1781 
  1782 
  1783 subsection {* Infimum and Supremum over non-empty sets *}
  1784 
  1785 text {*
  1786   After this non-regular bootstrap, things continue canonically.
  1787 *}
  1788 
  1789 context lattice
  1790 begin
  1791 
  1792 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"
  1793 apply(subgoal_tac "EX a. a:A")
  1794 prefer 2 apply blast
  1795 apply(erule exE)
  1796 apply(rule order_trans)
  1797 apply(erule (1) Inf_fin.coboundedI)
  1798 apply(erule (1) Sup_fin.coboundedI)
  1799 done
  1800 
  1801 lemma sup_Inf_absorb [simp]:
  1802   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
  1803 apply(subst sup_commute)
  1804 apply(simp add: sup_absorb2 Inf_fin.coboundedI)
  1805 done
  1806 
  1807 lemma inf_Sup_absorb [simp]:
  1808   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
  1809 by (simp add: inf_absorb1 Sup_fin.coboundedI)
  1810 
  1811 end
  1812 
  1813 context distrib_lattice
  1814 begin
  1815 
  1816 lemma sup_Inf1_distrib:
  1817   assumes "finite A"
  1818     and "A \<noteq> {}"
  1819   shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
  1820 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
  1821   (rule arg_cong [where f="Inf_fin"], blast)
  1822 
  1823 lemma sup_Inf2_distrib:
  1824   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1825   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}"
  1826 using A proof (induct rule: finite_ne_induct)
  1827   case singleton then show ?case
  1828     by (simp add: sup_Inf1_distrib [OF B])
  1829 next
  1830   case (insert x A)
  1831   have finB: "finite {sup x b |b. b \<in> B}"
  1832     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
  1833   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  1834   proof -
  1835     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  1836       by blast
  1837     thus ?thesis by(simp add: insert(1) B(1))
  1838   qed
  1839   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1840   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)"
  1841     using insert by simp
  1842   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)
  1843   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})"
  1844     using insert by(simp add:sup_Inf1_distrib[OF B])
  1845   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})"
  1846     (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
  1847     using B insert
  1848     by (simp add: Inf_fin.union [OF finB _ finAB ne])
  1849   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1850     by blast
  1851   finally show ?case .
  1852 qed
  1853 
  1854 lemma inf_Sup1_distrib:
  1855   assumes "finite A" and "A \<noteq> {}"
  1856   shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
  1857 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
  1858   (rule arg_cong [where f="Sup_fin"], blast)
  1859 
  1860 lemma inf_Sup2_distrib:
  1861   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1862   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}"
  1863 using A proof (induct rule: finite_ne_induct)
  1864   case singleton thus ?case
  1865     by(simp add: inf_Sup1_distrib [OF B])
  1866 next
  1867   case (insert x A)
  1868   have finB: "finite {inf x b |b. b \<in> B}"
  1869     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  1870   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  1871   proof -
  1872     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  1873       by blast
  1874     thus ?thesis by(simp add: insert(1) B(1))
  1875   qed
  1876   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1877   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)"
  1878     using insert by simp
  1879   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)
  1880   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})"
  1881     using insert by(simp add:inf_Sup1_distrib[OF B])
  1882   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})"
  1883     (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
  1884     using B insert
  1885     by (simp add: Sup_fin.union [OF finB _ finAB ne])
  1886   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1887     by blast
  1888   finally show ?case .
  1889 qed
  1890 
  1891 end
  1892 
  1893 context complete_lattice
  1894 begin
  1895 
  1896 lemma Inf_fin_Inf:
  1897   assumes "finite A" and "A \<noteq> {}"
  1898   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
  1899 proof -
  1900   from assms obtain b B where "A = insert b B" and "finite B" by auto
  1901   then show ?thesis
  1902     by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
  1903 qed
  1904 
  1905 lemma Sup_fin_Sup:
  1906   assumes "finite A" and "A \<noteq> {}"
  1907   shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
  1908 proof -
  1909   from assms obtain b B where "A = insert b B" and "finite B" by auto
  1910   then show ?thesis
  1911     by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
  1912 qed
  1913 
  1914 end
  1915 
  1916 
  1917 subsection {* Minimum and Maximum over non-empty sets *}
  1918 
  1919 context linorder
  1920 begin
  1921 
  1922 lemma dual_min:
  1923   "ord.min greater_eq = max"
  1924   by (auto simp add: ord.min_def max_def fun_eq_iff)
  1925 
  1926 lemma dual_max:
  1927   "ord.max greater_eq = min"
  1928   by (auto simp add: ord.max_def min_def fun_eq_iff)
  1929 
  1930 lemma dual_Min:
  1931   "linorder.Min greater_eq = Max"
  1932 proof -
  1933   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
  1934   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
  1935 qed
  1936 
  1937 lemma dual_Max:
  1938   "linorder.Max greater_eq = Min"
  1939 proof -
  1940   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
  1941   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
  1942 qed
  1943 
  1944 lemmas Min_singleton = Min.singleton
  1945 lemmas Max_singleton = Max.singleton
  1946 lemmas Min_insert = Min.insert
  1947 lemmas Max_insert = Max.insert
  1948 lemmas Min_Un = Min.union
  1949 lemmas Max_Un = Max.union
  1950 lemmas hom_Min_commute = Min.hom_commute
  1951 lemmas hom_Max_commute = Max.hom_commute
  1952 
  1953 lemma Min_in [simp]:
  1954   assumes "finite A" and "A \<noteq> {}"
  1955   shows "Min A \<in> A"
  1956   using assms by (auto simp add: min_def Min.closed)
  1957 
  1958 lemma Max_in [simp]:
  1959   assumes "finite A" and "A \<noteq> {}"
  1960   shows "Max A \<in> A"
  1961   using assms by (auto simp add: max_def Max.closed)
  1962 
  1963 lemma Min_le [simp]:
  1964   assumes "finite A" and "x \<in> A"
  1965   shows "Min A \<le> x"
  1966   using assms by (fact Min.coboundedI)
  1967 
  1968 lemma Max_ge [simp]:
  1969   assumes "finite A" and "x \<in> A"
  1970   shows "x \<le> Max A"
  1971   using assms by (fact Max.coboundedI)
  1972 
  1973 lemma Min_eqI:
  1974   assumes "finite A"
  1975   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  1976     and "x \<in> A"
  1977   shows "Min A = x"
  1978 proof (rule antisym)
  1979   from `x \<in> A` have "A \<noteq> {}" by auto
  1980   with assms show "Min A \<ge> x" by simp
  1981 next
  1982   from assms show "x \<ge> Min A" by simp
  1983 qed
  1984 
  1985 lemma Max_eqI:
  1986   assumes "finite A"
  1987   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  1988     and "x \<in> A"
  1989   shows "Max A = x"
  1990 proof (rule antisym)
  1991   from `x \<in> A` have "A \<noteq> {}" by auto
  1992   with assms show "Max A \<le> x" by simp
  1993 next
  1994   from assms show "x \<le> Max A" by simp
  1995 qed
  1996 
  1997 context
  1998   fixes A :: "'a set"
  1999   assumes fin_nonempty: "finite A" "A \<noteq> {}"
  2000 begin
  2001 
  2002 lemma Min_ge_iff [simp, no_atp]:
  2003   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2004   using fin_nonempty by (fact Min.bounded_iff)
  2005 
  2006 lemma Max_le_iff [simp, no_atp]:
  2007   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2008   using fin_nonempty by (fact Max.bounded_iff)
  2009 
  2010 lemma Min_gr_iff [simp, no_atp]:
  2011   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2012   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
  2013 
  2014 lemma Max_less_iff [simp, no_atp]:
  2015   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  2016   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
  2017 
  2018 lemma Min_le_iff [no_atp]:
  2019   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2020   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
  2021 
  2022 lemma Max_ge_iff [no_atp]:
  2023   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  2024   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
  2025 
  2026 lemma Min_less_iff [no_atp]:
  2027   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2028   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
  2029 
  2030 lemma Max_gr_iff [no_atp]:
  2031   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  2032   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
  2033 
  2034 end
  2035 
  2036 lemma Min_antimono:
  2037   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2038   shows "Min N \<le> Min M"
  2039   using assms by (fact Min.antimono)
  2040 
  2041 lemma Max_mono:
  2042   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2043   shows "Max M \<le> Max N"
  2044   using assms by (fact Max.antimono)
  2045 
  2046 lemma mono_Min_commute:
  2047   assumes "mono f"
  2048   assumes "finite A" and "A \<noteq> {}"
  2049   shows "f (Min A) = Min (f ` A)"
  2050 proof (rule linorder_class.Min_eqI [symmetric])
  2051   from `finite A` show "finite (f ` A)" by simp
  2052   from assms show "f (Min A) \<in> f ` A" by simp
  2053   fix x
  2054   assume "x \<in> f ` A"
  2055   then obtain y where "y \<in> A" and "x = f y" ..
  2056   with assms have "Min A \<le> y" by auto
  2057   with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
  2058   with `x = f y` show "f (Min A) \<le> x" by simp
  2059 qed
  2060 
  2061 lemma mono_Max_commute:
  2062   assumes "mono f"
  2063   assumes "finite A" and "A \<noteq> {}"
  2064   shows "f (Max A) = Max (f ` A)"
  2065 proof (rule linorder_class.Max_eqI [symmetric])
  2066   from `finite A` show "finite (f ` A)" by simp
  2067   from assms show "f (Max A) \<in> f ` A" by simp
  2068   fix x
  2069   assume "x \<in> f ` A"
  2070   then obtain y where "y \<in> A" and "x = f y" ..
  2071   with assms have "y \<le> Max A" by auto
  2072   with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
  2073   with `x = f y` show "x \<le> f (Max A)" by simp
  2074 qed
  2075 
  2076 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
  2077   assumes fin: "finite A"
  2078   and empty: "P {}" 
  2079   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
  2080   shows "P A"
  2081 using fin empty insert
  2082 proof (induct rule: finite_psubset_induct)
  2083   case (psubset A)
  2084   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 
  2085   have fin: "finite A" by fact 
  2086   have empty: "P {}" by fact
  2087   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
  2088   show "P A"
  2089   proof (cases "A = {}")
  2090     assume "A = {}" 
  2091     then show "P A" using `P {}` by simp
  2092   next
  2093     let ?B = "A - {Max A}" 
  2094     let ?A = "insert (Max A) ?B"
  2095     have "finite ?B" using `finite A` by simp
  2096     assume "A \<noteq> {}"
  2097     with `finite A` have "Max A : A" by auto
  2098     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
  2099     then have "P ?B" using `P {}` step IH [of ?B] by blast
  2100     moreover 
  2101     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
  2102     ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
  2103   qed
  2104 qed
  2105 
  2106 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
  2107   "\<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"
  2108   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
  2109 
  2110 lemma Least_Min:
  2111   assumes "finite {a. P a}" and "\<exists>a. P a"
  2112   shows "(LEAST a. P a) = Min {a. P a}"
  2113 proof -
  2114   { fix A :: "'a set"
  2115     assume A: "finite A" "A \<noteq> {}"
  2116     have "(LEAST a. a \<in> A) = Min A"
  2117     using A proof (induct A rule: finite_ne_induct)
  2118       case singleton show ?case by (rule Least_equality) simp_all
  2119     next
  2120       case (insert a A)
  2121       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
  2122         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
  2123       with insert show ?case by simp
  2124     qed
  2125   } from this [of "{a. P a}"] assms show ?thesis by simp
  2126 qed
  2127 
  2128 end
  2129 
  2130 context linordered_ab_semigroup_add
  2131 begin
  2132 
  2133 lemma add_Min_commute:
  2134   fixes k
  2135   assumes "finite N" and "N \<noteq> {}"
  2136   shows "k + Min N = Min {k + m | m. m \<in> N}"
  2137 proof -
  2138   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  2139     by (simp add: min_def not_le)
  2140       (blast intro: antisym less_imp_le add_left_mono)
  2141   with assms show ?thesis
  2142     using hom_Min_commute [of "plus k" N]
  2143     by simp (blast intro: arg_cong [where f = Min])
  2144 qed
  2145 
  2146 lemma add_Max_commute:
  2147   fixes k
  2148   assumes "finite N" and "N \<noteq> {}"
  2149   shows "k + Max N = Max {k + m | m. m \<in> N}"
  2150 proof -
  2151   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  2152     by (simp add: max_def not_le)
  2153       (blast intro: antisym less_imp_le add_left_mono)
  2154   with assms show ?thesis
  2155     using hom_Max_commute [of "plus k" N]
  2156     by simp (blast intro: arg_cong [where f = Max])
  2157 qed
  2158 
  2159 end
  2160 
  2161 context linordered_ab_group_add
  2162 begin
  2163 
  2164 lemma minus_Max_eq_Min [simp]:
  2165   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
  2166   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  2167 
  2168 lemma minus_Min_eq_Max [simp]:
  2169   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
  2170   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  2171 
  2172 end
  2173 
  2174 context complete_linorder
  2175 begin
  2176 
  2177 lemma Min_Inf:
  2178   assumes "finite A" and "A \<noteq> {}"
  2179   shows "Min A = Inf A"
  2180 proof -
  2181   from assms obtain b B where "A = insert b B" and "finite B" by auto
  2182   then show ?thesis
  2183     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
  2184 qed
  2185 
  2186 lemma Max_Sup:
  2187   assumes "finite A" and "A \<noteq> {}"
  2188   shows "Max A = Sup A"
  2189 proof -
  2190   from assms obtain b B where "A = insert b B" and "finite B" by auto
  2191   then show ?thesis
  2192     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
  2193 qed
  2194 
  2195 end
  2196 
  2197 end