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