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