src/HOL/Finite_Set.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35034 8103ea95b142
child 35171 28f824c7addc
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/Finite_Set.thy
     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3                 with contributions by Jeremy Avigad
     4 *)
     5 
     6 header {* Finite sets *}
     7 
     8 theory Finite_Set
     9 imports Power Product_Type Sum_Type
    10 begin
    11 
    12 subsection {* Definition and basic properties *}
    13 
    14 inductive finite :: "'a set => bool"
    15   where
    16     emptyI [simp, intro!]: "finite {}"
    17   | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
    18 
    19 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    20   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    21   shows "\<exists>a::'a. a \<notin> A"
    22 proof -
    23   from assms have "A \<noteq> UNIV" by blast
    24   thus ?thesis by blast
    25 qed
    26 
    27 lemma finite_induct [case_names empty insert, induct set: finite]:
    28   "finite F ==>
    29     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    30   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    31 proof -
    32   assume "P {}" and
    33     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    34   assume "finite F"
    35   thus "P F"
    36   proof induct
    37     show "P {}" by fact
    38     fix x F assume F: "finite F" and P: "P F"
    39     show "P (insert x F)"
    40     proof cases
    41       assume "x \<in> F"
    42       hence "insert x F = F" by (rule insert_absorb)
    43       with P show ?thesis by (simp only:)
    44     next
    45       assume "x \<notin> F"
    46       from F this P show ?thesis by (rule insert)
    47     qed
    48   qed
    49 qed
    50 
    51 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
    52 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
    53  \<lbrakk> \<And>x. P{x};
    54    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
    55  \<Longrightarrow> P F"
    56 using fin
    57 proof induct
    58   case empty thus ?case by simp
    59 next
    60   case (insert x F)
    61   show ?case
    62   proof cases
    63     assume "F = {}"
    64     thus ?thesis using `P {x}` by simp
    65   next
    66     assume "F \<noteq> {}"
    67     thus ?thesis using insert by blast
    68   qed
    69 qed
    70 
    71 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    72   assumes "finite F" and "F \<subseteq> A"
    73     and empty: "P {}"
    74     and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    75   shows "P F"
    76 proof -
    77   from `finite F` and `F \<subseteq> A`
    78   show ?thesis
    79   proof induct
    80     show "P {}" by fact
    81   next
    82     fix x F
    83     assume "finite F" and "x \<notin> F" and
    84       P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    85     show "P (insert x F)"
    86     proof (rule insert)
    87       from i show "x \<in> A" by blast
    88       from i have "F \<subseteq> A" by blast
    89       with P show "P F" .
    90       show "finite F" by fact
    91       show "x \<notin> F" by fact
    92     qed
    93   qed
    94 qed
    95 
    96 
    97 text{* A finite choice principle. Does not need the SOME choice operator. *}
    98 lemma finite_set_choice:
    99   "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
   100 proof (induct set: finite)
   101   case empty thus ?case by simp
   102 next
   103   case (insert a A)
   104   then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
   105   show ?case (is "EX f. ?P f")
   106   proof
   107     show "?P(%x. if x = a then b else f x)" using f ab by auto
   108   qed
   109 qed
   110 
   111 
   112 text{* Finite sets are the images of initial segments of natural numbers: *}
   113 
   114 lemma finite_imp_nat_seg_image_inj_on:
   115   assumes fin: "finite A" 
   116   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
   117 using fin
   118 proof induct
   119   case empty
   120   show ?case  
   121   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 
   122   qed
   123 next
   124   case (insert a A)
   125   have notinA: "a \<notin> A" by fact
   126   from insert.hyps obtain n f
   127     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
   128   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
   129         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
   130     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
   131   thus ?case by blast
   132 qed
   133 
   134 lemma nat_seg_image_imp_finite:
   135   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
   136 proof (induct n)
   137   case 0 thus ?case by simp
   138 next
   139   case (Suc n)
   140   let ?B = "f ` {i. i < n}"
   141   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
   142   show ?case
   143   proof cases
   144     assume "\<exists>k<n. f n = f k"
   145     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
   146     thus ?thesis using finB by simp
   147   next
   148     assume "\<not>(\<exists> k<n. f n = f k)"
   149     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
   150     thus ?thesis using finB by simp
   151   qed
   152 qed
   153 
   154 lemma finite_conv_nat_seg_image:
   155   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
   156 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
   157 
   158 lemma finite_imp_inj_to_nat_seg:
   159 assumes "finite A"
   160 shows "EX f n::nat. f`A = {i. i<n} & inj_on f A"
   161 proof -
   162   from finite_imp_nat_seg_image_inj_on[OF `finite A`]
   163   obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
   164     by (auto simp:bij_betw_def)
   165   let ?f = "the_inv_into {i. i<n} f"
   166   have "inj_on ?f A & ?f ` A = {i. i<n}"
   167     by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
   168   thus ?thesis by blast
   169 qed
   170 
   171 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
   172 by(fastsimp simp: finite_conv_nat_seg_image)
   173 
   174 
   175 subsubsection{* Finiteness and set theoretic constructions *}
   176 
   177 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
   178 by (induct set: finite) simp_all
   179 
   180 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
   181   -- {* Every subset of a finite set is finite. *}
   182 proof -
   183   assume "finite B"
   184   thus "!!A. A \<subseteq> B ==> finite A"
   185   proof induct
   186     case empty
   187     thus ?case by simp
   188   next
   189     case (insert x F A)
   190     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
   191     show "finite A"
   192     proof cases
   193       assume x: "x \<in> A"
   194       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
   195       with r have "finite (A - {x})" .
   196       hence "finite (insert x (A - {x}))" ..
   197       also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
   198       finally show ?thesis .
   199     next
   200       show "A \<subseteq> F ==> ?thesis" by fact
   201       assume "x \<notin> A"
   202       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   203     qed
   204   qed
   205 qed
   206 
   207 lemma rev_finite_subset: "finite B ==> A \<subseteq> B ==> finite A"
   208 by (rule finite_subset)
   209 
   210 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   211 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   212 
   213 lemma finite_Collect_disjI[simp]:
   214   "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
   215 by(simp add:Collect_disj_eq)
   216 
   217 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   218   -- {* The converse obviously fails. *}
   219 by (blast intro: finite_subset)
   220 
   221 lemma finite_Collect_conjI [simp, intro]:
   222   "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
   223   -- {* The converse obviously fails. *}
   224 by(simp add:Collect_conj_eq)
   225 
   226 lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}"
   227 by(simp add: le_eq_less_or_eq)
   228 
   229 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   230   apply (subst insert_is_Un)
   231   apply (simp only: finite_Un, blast)
   232   done
   233 
   234 lemma finite_Union[simp, intro]:
   235  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
   236 by (induct rule:finite_induct) simp_all
   237 
   238 lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)"
   239 by (blast intro: Inter_lower finite_subset)
   240 
   241 lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)"
   242 by (blast intro: INT_lower finite_subset)
   243 
   244 lemma finite_empty_induct:
   245   assumes "finite A"
   246     and "P A"
   247     and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   248   shows "P {}"
   249 proof -
   250   have "P (A - A)"
   251   proof -
   252     {
   253       fix c b :: "'a set"
   254       assume c: "finite c" and b: "finite b"
   255         and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   256       have "c \<subseteq> b ==> P (b - c)"
   257         using c
   258       proof induct
   259         case empty
   260         from P1 show ?case by simp
   261       next
   262         case (insert x F)
   263         have "P (b - F - {x})"
   264         proof (rule P2)
   265           from _ b show "finite (b - F)" by (rule finite_subset) blast
   266           from insert show "x \<in> b - F" by simp
   267           from insert show "P (b - F)" by simp
   268         qed
   269         also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   270         finally show ?case .
   271       qed
   272     }
   273     then show ?thesis by this (simp_all add: assms)
   274   qed
   275   then show ?thesis by simp
   276 qed
   277 
   278 lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
   279 by (rule Diff_subset [THEN finite_subset])
   280 
   281 lemma finite_Diff2 [simp]:
   282   assumes "finite B" shows "finite (A - B) = finite A"
   283 proof -
   284   have "finite A \<longleftrightarrow> finite((A-B) Un (A Int B))" by(simp add: Un_Diff_Int)
   285   also have "\<dots> \<longleftrightarrow> finite(A-B)" using `finite B` by(simp)
   286   finally show ?thesis ..
   287 qed
   288 
   289 lemma finite_compl[simp]:
   290   "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
   291 by(simp add:Compl_eq_Diff_UNIV)
   292 
   293 lemma finite_Collect_not[simp]:
   294   "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
   295 by(simp add:Collect_neg_eq)
   296 
   297 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   298   apply (subst Diff_insert)
   299   apply (case_tac "a : A - B")
   300    apply (rule finite_insert [symmetric, THEN trans])
   301    apply (subst insert_Diff, simp_all)
   302   done
   303 
   304 
   305 text {* Image and Inverse Image over Finite Sets *}
   306 
   307 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   308   -- {* The image of a finite set is finite. *}
   309   by (induct set: finite) simp_all
   310 
   311 lemma finite_image_set [simp]:
   312   "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
   313   by (simp add: image_Collect [symmetric])
   314 
   315 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   316   apply (frule finite_imageI)
   317   apply (erule finite_subset, assumption)
   318   done
   319 
   320 lemma finite_range_imageI:
   321     "finite (range g) ==> finite (range (%x. f (g x)))"
   322   apply (drule finite_imageI, simp add: range_composition)
   323   done
   324 
   325 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   326 proof -
   327   have aux: "!!A. finite (A - {}) = finite A" by simp
   328   fix B :: "'a set"
   329   assume "finite B"
   330   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   331     apply induct
   332      apply simp
   333     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   334      apply clarify
   335      apply (simp (no_asm_use) add: inj_on_def)
   336      apply (blast dest!: aux [THEN iffD1], atomize)
   337     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   338     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   339     apply (rule_tac x = xa in bexI)
   340      apply (simp_all add: inj_on_image_set_diff)
   341     done
   342 qed (rule refl)
   343 
   344 
   345 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   346   -- {* The inverse image of a singleton under an injective function
   347          is included in a singleton. *}
   348   apply (auto simp add: inj_on_def)
   349   apply (blast intro: the_equality [symmetric])
   350   done
   351 
   352 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   353   -- {* The inverse image of a finite set under an injective function
   354          is finite. *}
   355   apply (induct set: finite)
   356    apply simp_all
   357   apply (subst vimage_insert)
   358   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   359   done
   360 
   361 lemma finite_vimageD:
   362   assumes fin: "finite (h -` F)" and surj: "surj h"
   363   shows "finite F"
   364 proof -
   365   have "finite (h ` (h -` F))" using fin by (rule finite_imageI)
   366   also have "h ` (h -` F) = F" using surj by (rule surj_image_vimage_eq)
   367   finally show "finite F" .
   368 qed
   369 
   370 lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
   371   unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
   372 
   373 
   374 text {* The finite UNION of finite sets *}
   375 
   376 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   377   by (induct set: finite) simp_all
   378 
   379 text {*
   380   Strengthen RHS to
   381   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   382 
   383   We'd need to prove
   384   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   385   by induction. *}
   386 
   387 lemma finite_UN [simp]:
   388   "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   389 by (blast intro: finite_UN_I finite_subset)
   390 
   391 lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
   392   finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
   393 apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})")
   394  apply auto
   395 done
   396 
   397 lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow>
   398   finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})"
   399 apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})")
   400  apply auto
   401 done
   402 
   403 
   404 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
   405 by (simp add: Plus_def)
   406 
   407 lemma finite_PlusD: 
   408   fixes A :: "'a set" and B :: "'b set"
   409   assumes fin: "finite (A <+> B)"
   410   shows "finite A" "finite B"
   411 proof -
   412   have "Inl ` A \<subseteq> A <+> B" by auto
   413   hence "finite (Inl ` A :: ('a + 'b) set)" using fin by(rule finite_subset)
   414   thus "finite A" by(rule finite_imageD)(auto intro: inj_onI)
   415 next
   416   have "Inr ` B \<subseteq> A <+> B" by auto
   417   hence "finite (Inr ` B :: ('a + 'b) set)" using fin by(rule finite_subset)
   418   thus "finite B" by(rule finite_imageD)(auto intro: inj_onI)
   419 qed
   420 
   421 lemma finite_Plus_iff[simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
   422 by(auto intro: finite_PlusD finite_Plus)
   423 
   424 lemma finite_Plus_UNIV_iff[simp]:
   425   "finite (UNIV :: ('a + 'b) set) =
   426   (finite (UNIV :: 'a set) & finite (UNIV :: 'b set))"
   427 by(subst UNIV_Plus_UNIV[symmetric])(rule finite_Plus_iff)
   428 
   429 
   430 text {* Sigma of finite sets *}
   431 
   432 lemma finite_SigmaI [simp]:
   433     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   434   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   435 
   436 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   437     finite (A <*> B)"
   438   by (rule finite_SigmaI)
   439 
   440 lemma finite_Prod_UNIV:
   441     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   442   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   443    apply (erule ssubst)
   444    apply (erule finite_SigmaI, auto)
   445   done
   446 
   447 lemma finite_cartesian_productD1:
   448      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
   449 apply (auto simp add: finite_conv_nat_seg_image) 
   450 apply (drule_tac x=n in spec) 
   451 apply (drule_tac x="fst o f" in spec) 
   452 apply (auto simp add: o_def) 
   453  prefer 2 apply (force dest!: equalityD2) 
   454 apply (drule equalityD1) 
   455 apply (rename_tac y x)
   456 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   457  prefer 2 apply force
   458 apply clarify
   459 apply (rule_tac x=k in image_eqI, auto)
   460 done
   461 
   462 lemma finite_cartesian_productD2:
   463      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
   464 apply (auto simp add: finite_conv_nat_seg_image) 
   465 apply (drule_tac x=n in spec) 
   466 apply (drule_tac x="snd o f" in spec) 
   467 apply (auto simp add: o_def) 
   468  prefer 2 apply (force dest!: equalityD2) 
   469 apply (drule equalityD1)
   470 apply (rename_tac x y)
   471 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   472  prefer 2 apply force
   473 apply clarify
   474 apply (rule_tac x=k in image_eqI, auto)
   475 done
   476 
   477 
   478 text {* The powerset of a finite set *}
   479 
   480 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   481 proof
   482   assume "finite (Pow A)"
   483   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   484   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   485 next
   486   assume "finite A"
   487   thus "finite (Pow A)"
   488     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   489 qed
   490 
   491 lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
   492 by(simp add: Pow_def[symmetric])
   493 
   494 
   495 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   496 by(blast intro: finite_subset[OF subset_Pow_Union])
   497 
   498 
   499 lemma finite_subset_image:
   500   assumes "finite B"
   501   shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
   502 using assms proof(induct)
   503   case empty thus ?case by simp
   504 next
   505   case insert thus ?case
   506     by (clarsimp simp del: image_insert simp add: image_insert[symmetric])
   507        blast
   508 qed
   509 
   510 
   511 subsection {* Class @{text finite}  *}
   512 
   513 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
   514 class finite =
   515   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
   516 setup {* Sign.parent_path *}
   517 hide const finite
   518 
   519 context finite
   520 begin
   521 
   522 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   523   by (rule subset_UNIV finite_UNIV finite_subset)+
   524 
   525 end
   526 
   527 lemma UNIV_unit [noatp]:
   528   "UNIV = {()}" by auto
   529 
   530 instance unit :: finite
   531   by default (simp add: UNIV_unit)
   532 
   533 lemma UNIV_bool [noatp]:
   534   "UNIV = {False, True}" by auto
   535 
   536 instance bool :: finite
   537   by default (simp add: UNIV_bool)
   538 
   539 instance * :: (finite, finite) finite
   540   by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
   541 
   542 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   543   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   544 
   545 instance "fun" :: (finite, finite) finite
   546 proof
   547   show "finite (UNIV :: ('a => 'b) set)"
   548   proof (rule finite_imageD)
   549     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
   550     have "range ?graph \<subseteq> Pow UNIV" by simp
   551     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
   552       by (simp only: finite_Pow_iff finite)
   553     ultimately show "finite (range ?graph)"
   554       by (rule finite_subset)
   555     show "inj ?graph" by (rule inj_graph)
   556   qed
   557 qed
   558 
   559 instance "+" :: (finite, finite) finite
   560   by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
   561 
   562 
   563 subsection {* A fold functional for finite sets *}
   564 
   565 text {* The intended behaviour is
   566 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
   567 if @{text f} is ``left-commutative'':
   568 *}
   569 
   570 locale fun_left_comm =
   571   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   572   assumes fun_left_comm: "f x (f y z) = f y (f x z)"
   573 begin
   574 
   575 text{* On a functional level it looks much nicer: *}
   576 
   577 lemma fun_comp_comm:  "f x \<circ> f y = f y \<circ> f x"
   578 by (simp add: fun_left_comm expand_fun_eq)
   579 
   580 end
   581 
   582 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
   583 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where
   584   emptyI [intro]: "fold_graph f z {} z" |
   585   insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y
   586       \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
   587 
   588 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
   589 
   590 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
   591 [code del]: "fold f z A = (THE y. fold_graph f z A y)"
   592 
   593 text{*A tempting alternative for the definiens is
   594 @{term "if finite A then THE y. fold_graph f z A y else e"}.
   595 It allows the removal of finiteness assumptions from the theorems
   596 @{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
   597 The proofs become ugly. It is not worth the effort. (???) *}
   598 
   599 
   600 lemma Diff1_fold_graph:
   601   "fold_graph f z (A - {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)"
   602 by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto)
   603 
   604 lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A"
   605 by (induct set: fold_graph) auto
   606 
   607 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
   608 by (induct set: finite) auto
   609 
   610 
   611 subsubsection{*From @{const fold_graph} to @{term fold}*}
   612 
   613 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
   614   by (auto simp add: less_Suc_eq) 
   615 
   616 lemma insert_image_inj_on_eq:
   617      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
   618         inj_on h {i. i < Suc m}|] 
   619       ==> A = h ` {i. i < m}"
   620 apply (auto simp add: image_less_Suc inj_on_def)
   621 apply (blast intro: less_trans) 
   622 done
   623 
   624 lemma insert_inj_onE:
   625   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 
   626       and inj_on: "inj_on h {i::nat. i<n}"
   627   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
   628 proof (cases n)
   629   case 0 thus ?thesis using aA by auto
   630 next
   631   case (Suc m)
   632   have nSuc: "n = Suc m" by fact
   633   have mlessn: "m<n" by (simp add: nSuc)
   634   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   635   let ?hm = "Fun.swap k m h"
   636   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
   637     by (simp add: inj_on_swap_iff inj_on)
   638   show ?thesis
   639   proof (intro exI conjI)
   640     show "inj_on ?hm {i. i < m}" using inj_hm
   641       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
   642     show "m<n" by (rule mlessn)
   643     show "A = ?hm ` {i. i < m}" 
   644     proof (rule insert_image_inj_on_eq)
   645       show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
   646       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
   647       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
   648         using aA hkeq nSuc klessn
   649         by (auto simp add: swap_def image_less_Suc fun_upd_image 
   650                            less_Suc_eq inj_on_image_set_diff [OF inj_on])
   651     qed
   652   qed
   653 qed
   654 
   655 context fun_left_comm
   656 begin
   657 
   658 lemma fold_graph_determ_aux:
   659   "A = h`{i::nat. i<n} \<Longrightarrow> inj_on h {i. i<n}
   660    \<Longrightarrow> fold_graph f z A x \<Longrightarrow> fold_graph f z A x'
   661    \<Longrightarrow> x' = x"
   662 proof (induct n arbitrary: A x x' h rule: less_induct)
   663   case (less n)
   664   have IH: "\<And>m h A x x'. m < n \<Longrightarrow> A = h ` {i. i<m}
   665       \<Longrightarrow> inj_on h {i. i<m} \<Longrightarrow> fold_graph f z A x
   666       \<Longrightarrow> fold_graph f z A x' \<Longrightarrow> x' = x" by fact
   667   have Afoldx: "fold_graph f z A x" and Afoldx': "fold_graph f z A x'"
   668     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
   669   show ?case
   670   proof (rule fold_graph.cases [OF Afoldx])
   671     assume "A = {}" and "x = z"
   672     with Afoldx' show "x' = x" by auto
   673   next
   674     fix B b u
   675     assume AbB: "A = insert b B" and x: "x = f b u"
   676       and notinB: "b \<notin> B" and Bu: "fold_graph f z B u"
   677     show "x'=x" 
   678     proof (rule fold_graph.cases [OF Afoldx'])
   679       assume "A = {}" and "x' = z"
   680       with AbB show "x' = x" by blast
   681     next
   682       fix C c v
   683       assume AcC: "A = insert c C" and x': "x' = f c v"
   684         and notinC: "c \<notin> C" and Cv: "fold_graph f z C v"
   685       from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   686       from insert_inj_onE [OF Beq notinB injh]
   687       obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   688         and Beq: "B = hB ` {i. i < mB}" and lessB: "mB < n" by auto 
   689       from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
   690       from insert_inj_onE [OF Ceq notinC injh]
   691       obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
   692         and Ceq: "C = hC ` {i. i < mC}" and lessC: "mC < n" by auto 
   693       show "x'=x"
   694       proof cases
   695         assume "b=c"
   696         then moreover have "B = C" using AbB AcC notinB notinC by auto
   697         ultimately show ?thesis  using Bu Cv x x' IH [OF lessC Ceq inj_onC]
   698           by auto
   699       next
   700         assume diff: "b \<noteq> c"
   701         let ?D = "B - {c}"
   702         have B: "B = insert c ?D" and C: "C = insert b ?D"
   703           using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   704         have "finite A" by(rule fold_graph_imp_finite [OF Afoldx])
   705         with AbB have "finite ?D" by simp
   706         then obtain d where Dfoldd: "fold_graph f z ?D d"
   707           using finite_imp_fold_graph by iprover
   708         moreover have cinB: "c \<in> B" using B by auto
   709         ultimately have "fold_graph f z B (f c d)" by(rule Diff1_fold_graph)
   710         hence "f c d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   711         moreover have "f b d = v"
   712         proof (rule IH[OF lessC Ceq inj_onC Cv])
   713           show "fold_graph f z C (f b d)" using C notinB Dfoldd by fastsimp
   714         qed
   715         ultimately show ?thesis
   716           using fun_left_comm [of c b] x x' by (auto simp add: o_def)
   717       qed
   718     qed
   719   qed
   720 qed
   721 
   722 lemma fold_graph_determ:
   723   "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
   724 apply (frule fold_graph_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   725 apply (blast intro: fold_graph_determ_aux [rule_format])
   726 done
   727 
   728 lemma fold_equality:
   729   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
   730 by (unfold fold_def) (blast intro: fold_graph_determ)
   731 
   732 text{* The base case for @{text fold}: *}
   733 
   734 lemma (in -) fold_empty [simp]: "fold f z {} = z"
   735 by (unfold fold_def) blast
   736 
   737 text{* The various recursion equations for @{const fold}: *}
   738 
   739 lemma fold_insert_aux: "x \<notin> A
   740   \<Longrightarrow> fold_graph f z (insert x A) v \<longleftrightarrow>
   741       (\<exists>y. fold_graph f z A y \<and> v = f x y)"
   742 apply auto
   743 apply (rule_tac A1 = A and f1 = f in finite_imp_fold_graph [THEN exE])
   744  apply (fastsimp dest: fold_graph_imp_finite)
   745 apply (blast intro: fold_graph_determ)
   746 done
   747 
   748 lemma fold_insert [simp]:
   749   "finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
   750 apply (simp add: fold_def fold_insert_aux)
   751 apply (rule the_equality)
   752  apply (auto intro: finite_imp_fold_graph
   753         cong add: conj_cong simp add: fold_def[symmetric] fold_equality)
   754 done
   755 
   756 lemma fold_fun_comm:
   757   "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
   758 proof (induct rule: finite_induct)
   759   case empty then show ?case by simp
   760 next
   761   case (insert y A) then show ?case
   762     by (simp add: fun_left_comm[of x])
   763 qed
   764 
   765 lemma fold_insert2:
   766   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
   767 by (simp add: fold_insert fold_fun_comm)
   768 
   769 lemma fold_rec:
   770 assumes "finite A" and "x \<in> A"
   771 shows "fold f z A = f x (fold f z (A - {x}))"
   772 proof -
   773   have A: "A = insert x (A - {x})" using `x \<in> A` by blast
   774   then have "fold f z A = fold f z (insert x (A - {x}))" by simp
   775   also have "\<dots> = f x (fold f z (A - {x}))"
   776     by (rule fold_insert) (simp add: `finite A`)+
   777   finally show ?thesis .
   778 qed
   779 
   780 lemma fold_insert_remove:
   781   assumes "finite A"
   782   shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
   783 proof -
   784   from `finite A` have "finite (insert x A)" by auto
   785   moreover have "x \<in> insert x A" by auto
   786   ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
   787     by (rule fold_rec)
   788   then show ?thesis by simp
   789 qed
   790 
   791 end
   792 
   793 text{* A simplified version for idempotent functions: *}
   794 
   795 locale fun_left_comm_idem = fun_left_comm +
   796   assumes fun_left_idem: "f x (f x z) = f x z"
   797 begin
   798 
   799 text{* The nice version: *}
   800 lemma fun_comp_idem : "f x o f x = f x"
   801 by (simp add: fun_left_idem expand_fun_eq)
   802 
   803 lemma fold_insert_idem:
   804   assumes fin: "finite A"
   805   shows "fold f z (insert x A) = f x (fold f z A)"
   806 proof cases
   807   assume "x \<in> A"
   808   then obtain B where "A = insert x B" and "x \<notin> B" by (rule set_insert)
   809   then show ?thesis using assms by (simp add:fun_left_idem)
   810 next
   811   assume "x \<notin> A" then show ?thesis using assms by simp
   812 qed
   813 
   814 declare fold_insert[simp del] fold_insert_idem[simp]
   815 
   816 lemma fold_insert_idem2:
   817   "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
   818 by(simp add:fold_fun_comm)
   819 
   820 end
   821 
   822 context ab_semigroup_idem_mult
   823 begin
   824 
   825 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
   826 apply unfold_locales
   827  apply (simp add: mult_ac)
   828 apply (simp add: mult_idem mult_assoc[symmetric])
   829 done
   830 
   831 end
   832 
   833 context semilattice_inf
   834 begin
   835 
   836 lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
   837 proof qed (rule inf_assoc inf_commute inf_idem)+
   838 
   839 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
   840 by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
   841 
   842 lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
   843 by (induct pred: finite) (auto intro: le_infI1)
   844 
   845 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
   846 proof(induct arbitrary: a pred:finite)
   847   case empty thus ?case by simp
   848 next
   849   case (insert x A)
   850   show ?case
   851   proof cases
   852     assume "A = {}" thus ?thesis using insert by simp
   853   next
   854     assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
   855   qed
   856 qed
   857 
   858 end
   859 
   860 context semilattice_sup
   861 begin
   862 
   863 lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
   864 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
   865 
   866 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
   867 by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
   868 
   869 lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
   870 by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
   871 
   872 lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
   873 by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
   874 
   875 end
   876 
   877 
   878 subsubsection{* The derived combinator @{text fold_image} *}
   879 
   880 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
   881 where "fold_image f g = fold (%x y. f (g x) y)"
   882 
   883 lemma fold_image_empty[simp]: "fold_image f g z {} = z"
   884 by(simp add:fold_image_def)
   885 
   886 context ab_semigroup_mult
   887 begin
   888 
   889 lemma fold_image_insert[simp]:
   890 assumes "finite A" and "a \<notin> A"
   891 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
   892 proof -
   893   interpret I: fun_left_comm "%x y. (g x) * y"
   894     by unfold_locales (simp add: mult_ac)
   895   show ?thesis using assms by(simp add:fold_image_def)
   896 qed
   897 
   898 (*
   899 lemma fold_commute:
   900   "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
   901   apply (induct set: finite)
   902    apply simp
   903   apply (simp add: mult_left_commute [of x])
   904   done
   905 
   906 lemma fold_nest_Un_Int:
   907   "finite A ==> finite B
   908     ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
   909   apply (induct set: finite)
   910    apply simp
   911   apply (simp add: fold_commute Int_insert_left insert_absorb)
   912   done
   913 
   914 lemma fold_nest_Un_disjoint:
   915   "finite A ==> finite B ==> A Int B = {}
   916     ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
   917   by (simp add: fold_nest_Un_Int)
   918 *)
   919 
   920 lemma fold_image_reindex:
   921 assumes fin: "finite A"
   922 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
   923 using fin by induct auto
   924 
   925 (*
   926 text{*
   927   Fusion theorem, as described in Graham Hutton's paper,
   928   A Tutorial on the Universality and Expressiveness of Fold,
   929   JFP 9:4 (355-372), 1999.
   930 *}
   931 
   932 lemma fold_fusion:
   933   assumes "ab_semigroup_mult g"
   934   assumes fin: "finite A"
   935     and hyp: "\<And>x y. h (g x y) = times x (h y)"
   936   shows "h (fold g j w A) = fold times j (h w) A"
   937 proof -
   938   class_interpret ab_semigroup_mult [g] by fact
   939   show ?thesis using fin hyp by (induct set: finite) simp_all
   940 qed
   941 *)
   942 
   943 lemma fold_image_cong:
   944   "finite A \<Longrightarrow>
   945   (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A"
   946 apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C")
   947  apply simp
   948 apply (erule finite_induct, simp)
   949 apply (simp add: subset_insert_iff, clarify)
   950 apply (subgoal_tac "finite C")
   951  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   952 apply (subgoal_tac "C = insert x (C - {x})")
   953  prefer 2 apply blast
   954 apply (erule ssubst)
   955 apply (drule spec)
   956 apply (erule (1) notE impE)
   957 apply (simp add: Ball_def del: insert_Diff_single)
   958 done
   959 
   960 end
   961 
   962 context comm_monoid_mult
   963 begin
   964 
   965 lemma fold_image_Un_Int:
   966   "finite A ==> finite B ==>
   967     fold_image times g 1 A * fold_image times g 1 B =
   968     fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)"
   969 by (induct set: finite) 
   970    (auto simp add: mult_ac insert_absorb Int_insert_left)
   971 
   972 corollary fold_Un_disjoint:
   973   "finite A ==> finite B ==> A Int B = {} ==>
   974    fold_image times g 1 (A Un B) =
   975    fold_image times g 1 A * fold_image times g 1 B"
   976 by (simp add: fold_image_Un_Int)
   977 
   978 lemma fold_image_UN_disjoint:
   979   "\<lbrakk> finite I; ALL i:I. finite (A i);
   980      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   981    \<Longrightarrow> fold_image times g 1 (UNION I A) =
   982        fold_image times (%i. fold_image times g 1 (A i)) 1 I"
   983 apply (induct set: finite, simp, atomize)
   984 apply (subgoal_tac "ALL i:F. x \<noteq> i")
   985  prefer 2 apply blast
   986 apply (subgoal_tac "A x Int UNION F A = {}")
   987  prefer 2 apply blast
   988 apply (simp add: fold_Un_disjoint)
   989 done
   990 
   991 lemma fold_image_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   992   fold_image times (%x. fold_image times (g x) 1 (B x)) 1 A =
   993   fold_image times (split g) 1 (SIGMA x:A. B x)"
   994 apply (subst Sigma_def)
   995 apply (subst fold_image_UN_disjoint, assumption, simp)
   996  apply blast
   997 apply (erule fold_image_cong)
   998 apply (subst fold_image_UN_disjoint, simp, simp)
   999  apply blast
  1000 apply simp
  1001 done
  1002 
  1003 lemma fold_image_distrib: "finite A \<Longrightarrow>
  1004    fold_image times (%x. g x * h x) 1 A =
  1005    fold_image times g 1 A *  fold_image times h 1 A"
  1006 by (erule finite_induct) (simp_all add: mult_ac)
  1007 
  1008 lemma fold_image_related: 
  1009   assumes Re: "R e e" 
  1010   and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
  1011   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
  1012   shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)"
  1013   using fS by (rule finite_subset_induct) (insert assms, auto)
  1014 
  1015 lemma  fold_image_eq_general:
  1016   assumes fS: "finite S"
  1017   and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y" 
  1018   and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x"
  1019   shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'"
  1020 proof-
  1021   from h f12 have hS: "h ` S = S'" by auto
  1022   {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
  1023     from f12 h H  have "x = y" by auto }
  1024   hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
  1025   from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
  1026   from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp
  1027   also have "\<dots> = fold_image (op *) (f2 o h) e S" 
  1028     using fold_image_reindex[OF fS hinj, of f2 e] .
  1029   also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e]
  1030     by blast
  1031   finally show ?thesis ..
  1032 qed
  1033 
  1034 lemma fold_image_eq_general_inverses:
  1035   assumes fS: "finite S" 
  1036   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
  1037   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x  \<and> g (h x) = f x"
  1038   shows "fold_image (op *) f e S = fold_image (op *) g e T"
  1039   (* metis solves it, but not yet available here *)
  1040   apply (rule fold_image_eq_general[OF fS, of T h g f e])
  1041   apply (rule ballI)
  1042   apply (frule kh)
  1043   apply (rule ex1I[])
  1044   apply blast
  1045   apply clarsimp
  1046   apply (drule hk) apply simp
  1047   apply (rule sym)
  1048   apply (erule conjunct1[OF conjunct2[OF hk]])
  1049   apply (rule ballI)
  1050   apply (drule  hk)
  1051   apply blast
  1052   done
  1053 
  1054 end
  1055 
  1056 subsection {* Generalized summation over a set *}
  1057 
  1058 interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
  1059   proof qed (auto intro: add_assoc add_commute)
  1060 
  1061 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
  1062 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
  1063 
  1064 abbreviation
  1065   Setsum  ("\<Sum>_" [1000] 999) where
  1066   "\<Sum>A == setsum (%x. x) A"
  1067 
  1068 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
  1069 written @{text"\<Sum>x\<in>A. e"}. *}
  1070 
  1071 syntax
  1072   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
  1073 syntax (xsymbols)
  1074   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
  1075 syntax (HTML output)
  1076   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
  1077 
  1078 translations -- {* Beware of argument permutation! *}
  1079   "SUM i:A. b" == "CONST setsum (%i. b) A"
  1080   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
  1081 
  1082 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
  1083  @{text"\<Sum>x|P. e"}. *}
  1084 
  1085 syntax
  1086   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
  1087 syntax (xsymbols)
  1088   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
  1089 syntax (HTML output)
  1090   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
  1091 
  1092 translations
  1093   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
  1094   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
  1095 
  1096 print_translation {*
  1097 let
  1098   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
  1099         if x <> y then raise Match
  1100         else
  1101           let
  1102             val x' = Syntax.mark_bound x;
  1103             val t' = subst_bound (x', t);
  1104             val P' = subst_bound (x', P);
  1105           in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
  1106     | setsum_tr' _ = raise Match;
  1107 in [(@{const_syntax setsum}, setsum_tr')] end
  1108 *}
  1109 
  1110 
  1111 lemma setsum_empty [simp]: "setsum f {} = 0"
  1112 by (simp add: setsum_def)
  1113 
  1114 lemma setsum_insert [simp]:
  1115   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
  1116 by (simp add: setsum_def)
  1117 
  1118 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
  1119 by (simp add: setsum_def)
  1120 
  1121 lemma setsum_reindex:
  1122      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
  1123 by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
  1124 
  1125 lemma setsum_reindex_id:
  1126      "inj_on f B ==> setsum f B = setsum id (f ` B)"
  1127 by (auto simp add: setsum_reindex)
  1128 
  1129 lemma setsum_reindex_nonzero: 
  1130   assumes fS: "finite S"
  1131   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"
  1132   shows "setsum h (f ` S) = setsum (h o f) S"
  1133 using nz
  1134 proof(induct rule: finite_induct[OF fS])
  1135   case 1 thus ?case by simp
  1136 next
  1137   case (2 x F) 
  1138   {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
  1139     then obtain y where y: "y \<in> F" "f x = f y" by auto 
  1140     from "2.hyps" y have xy: "x \<noteq> y" by auto
  1141     
  1142     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
  1143     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
  1144     also have "\<dots> = setsum (h o f) (insert x F)" 
  1145       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
  1146       using h0 
  1147       apply simp
  1148       apply (rule "2.hyps"(3))
  1149       apply (rule_tac y="y" in  "2.prems")
  1150       apply simp_all
  1151       done
  1152     finally have ?case .}
  1153   moreover
  1154   {assume fxF: "f x \<notin> f ` F"
  1155     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
  1156       using fxF "2.hyps" by simp 
  1157     also have "\<dots> = setsum (h o f) (insert x F)"
  1158       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
  1159       apply simp
  1160       apply (rule cong[OF refl[of "op + (h (f x))"]])
  1161       apply (rule "2.hyps"(3))
  1162       apply (rule_tac y="y" in  "2.prems")
  1163       apply simp_all
  1164       done
  1165     finally have ?case .}
  1166   ultimately show ?case by blast
  1167 qed
  1168 
  1169 lemma setsum_cong:
  1170   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
  1171 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
  1172 
  1173 lemma strong_setsum_cong[cong]:
  1174   "A = B ==> (!!x. x:B =simp=> f x = g x)
  1175    ==> setsum (%x. f x) A = setsum (%x. g x) B"
  1176 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
  1177 
  1178 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
  1179 by (rule setsum_cong[OF refl], auto)
  1180 
  1181 lemma setsum_reindex_cong:
  1182    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
  1183     ==> setsum h B = setsum g A"
  1184 by (simp add: setsum_reindex cong: setsum_cong)
  1185 
  1186 
  1187 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
  1188 apply (clarsimp simp: setsum_def)
  1189 apply (erule finite_induct, auto)
  1190 done
  1191 
  1192 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
  1193 by(simp add:setsum_cong)
  1194 
  1195 lemma setsum_Un_Int: "finite A ==> finite B ==>
  1196   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
  1197   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
  1198 by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
  1199 
  1200 lemma setsum_Un_disjoint: "finite A ==> finite B
  1201   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
  1202 by (subst setsum_Un_Int [symmetric], auto)
  1203 
  1204 lemma setsum_mono_zero_left: 
  1205   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1206   and z: "\<forall>i \<in> T - S. f i = 0"
  1207   shows "setsum f S = setsum f T"
  1208 proof-
  1209   have eq: "T = S \<union> (T - S)" using ST by blast
  1210   have d: "S \<inter> (T - S) = {}" using ST by blast
  1211   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
  1212   show ?thesis 
  1213   by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
  1214 qed
  1215 
  1216 lemma setsum_mono_zero_right: 
  1217   "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
  1218 by(blast intro!: setsum_mono_zero_left[symmetric])
  1219 
  1220 lemma setsum_mono_zero_cong_left: 
  1221   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1222   and z: "\<forall>i \<in> T - S. g i = 0"
  1223   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  1224   shows "setsum f S = setsum g T"
  1225 proof-
  1226   have eq: "T = S \<union> (T - S)" using ST by blast
  1227   have d: "S \<inter> (T - S) = {}" using ST by blast
  1228   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
  1229   show ?thesis 
  1230     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
  1231 qed
  1232 
  1233 lemma setsum_mono_zero_cong_right: 
  1234   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1235   and z: "\<forall>i \<in> T - S. f i = 0"
  1236   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  1237   shows "setsum f T = setsum g S"
  1238 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
  1239 
  1240 lemma setsum_delta: 
  1241   assumes fS: "finite S"
  1242   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
  1243 proof-
  1244   let ?f = "(\<lambda>k. if k=a then b k else 0)"
  1245   {assume a: "a \<notin> S"
  1246     hence "\<forall> k\<in> S. ?f k = 0" by simp
  1247     hence ?thesis  using a by simp}
  1248   moreover 
  1249   {assume a: "a \<in> S"
  1250     let ?A = "S - {a}"
  1251     let ?B = "{a}"
  1252     have eq: "S = ?A \<union> ?B" using a by blast 
  1253     have dj: "?A \<inter> ?B = {}" by simp
  1254     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1255     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
  1256       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1257       by simp
  1258     then have ?thesis  using a by simp}
  1259   ultimately show ?thesis by blast
  1260 qed
  1261 lemma setsum_delta': 
  1262   assumes fS: "finite S" shows 
  1263   "setsum (\<lambda>k. if a = k then b k else 0) S = 
  1264      (if a\<in> S then b a else 0)"
  1265   using setsum_delta[OF fS, of a b, symmetric] 
  1266   by (auto intro: setsum_cong)
  1267 
  1268 lemma setsum_restrict_set:
  1269   assumes fA: "finite A"
  1270   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
  1271 proof-
  1272   from fA have fab: "finite (A \<inter> B)" by auto
  1273   have aba: "A \<inter> B \<subseteq> A" by blast
  1274   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
  1275   from setsum_mono_zero_left[OF fA aba, of ?g]
  1276   show ?thesis by simp
  1277 qed
  1278 
  1279 lemma setsum_cases:
  1280   assumes fA: "finite A"
  1281   shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
  1282          setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
  1283 proof-
  1284   have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}" 
  1285     by blast+
  1286   from fA 
  1287   have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
  1288   let ?g = "\<lambda>x. if x \<in> B then f x else g x"
  1289   from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
  1290   show ?thesis by simp
  1291 qed
  1292 
  1293 
  1294 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
  1295   the lhs need not be, since UNION I A could still be finite.*)
  1296 lemma setsum_UN_disjoint:
  1297     "finite I ==> (ALL i:I. finite (A i)) ==>
  1298         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1299       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
  1300 by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
  1301 
  1302 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
  1303 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
  1304 lemma setsum_Union_disjoint:
  1305   "[| (ALL A:C. finite A);
  1306       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
  1307    ==> setsum f (Union C) = setsum (setsum f) C"
  1308 apply (cases "finite C") 
  1309  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
  1310   apply (frule setsum_UN_disjoint [of C id f])
  1311  apply (unfold Union_def id_def, assumption+)
  1312 done
  1313 
  1314 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
  1315   the rhs need not be, since SIGMA A B could still be finite.*)
  1316 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1317     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1318 by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
  1319 
  1320 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1321 lemma setsum_cartesian_product: 
  1322    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
  1323 apply (cases "finite A") 
  1324  apply (cases "finite B") 
  1325   apply (simp add: setsum_Sigma)
  1326  apply (cases "A={}", simp)
  1327  apply (simp) 
  1328 apply (auto simp add: setsum_def
  1329             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1330 done
  1331 
  1332 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
  1333 by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
  1334 
  1335 
  1336 subsubsection {* Properties in more restricted classes of structures *}
  1337 
  1338 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
  1339 apply (case_tac "finite A")
  1340  prefer 2 apply (simp add: setsum_def)
  1341 apply (erule rev_mp)
  1342 apply (erule finite_induct, auto)
  1343 done
  1344 
  1345 lemma setsum_eq_0_iff [simp]:
  1346     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
  1347 by (induct set: finite) auto
  1348 
  1349 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
  1350   (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
  1351 apply(erule finite_induct)
  1352 apply (auto simp add:add_is_1)
  1353 done
  1354 
  1355 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
  1356 
  1357 lemma setsum_Un_nat: "finite A ==> finite B ==>
  1358   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
  1359   -- {* For the natural numbers, we have subtraction. *}
  1360 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
  1361 
  1362 lemma setsum_Un: "finite A ==> finite B ==>
  1363   (setsum f (A Un B) :: 'a :: ab_group_add) =
  1364    setsum f A + setsum f B - setsum f (A Int B)"
  1365 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
  1366 
  1367 lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
  1368   apply (induct set: finite)
  1369   apply simp by (auto simp add: fold_image_insert)
  1370 
  1371 lemma (in comm_monoid_mult) fold_image_Un_one:
  1372   assumes fS: "finite S" and fT: "finite T"
  1373   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
  1374   shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
  1375 proof-
  1376   have "fold_image op * f 1 (S \<inter> T) = 1" 
  1377     apply (rule fold_image_1)
  1378     using fS fT I0 by auto 
  1379   with fold_image_Un_Int[OF fS fT] show ?thesis by simp
  1380 qed
  1381 
  1382 lemma setsum_eq_general_reverses:
  1383   assumes fS: "finite S" and fT: "finite T"
  1384   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
  1385   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
  1386   shows "setsum f S = setsum g T"
  1387   apply (simp add: setsum_def fS fT)
  1388   apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
  1389   apply (erule kh)
  1390   apply (erule hk)
  1391   done
  1392 
  1393 
  1394 
  1395 lemma setsum_Un_zero:  
  1396   assumes fS: "finite S" and fT: "finite T"
  1397   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
  1398   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
  1399   using fS fT
  1400   apply (simp add: setsum_def)
  1401   apply (rule comm_monoid_add.fold_image_Un_one)
  1402   using I0 by auto
  1403 
  1404 
  1405 lemma setsum_UNION_zero: 
  1406   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
  1407   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"
  1408   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
  1409   using fSS f0
  1410 proof(induct rule: finite_induct[OF fS])
  1411   case 1 thus ?case by simp
  1412 next
  1413   case (2 T F)
  1414   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
  1415     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
  1416   from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
  1417   from "2.prems" TF fTF
  1418   show ?case 
  1419     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
  1420 qed
  1421 
  1422 
  1423 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
  1424   (if a:A then setsum f A - f a else setsum f A)"
  1425 apply (case_tac "finite A")
  1426  prefer 2 apply (simp add: setsum_def)
  1427 apply (erule finite_induct)
  1428  apply (auto simp add: insert_Diff_if)
  1429 apply (drule_tac a = a in mk_disjoint_insert, auto)
  1430 done
  1431 
  1432 lemma setsum_diff1: "finite A \<Longrightarrow>
  1433   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1434   (if a:A then setsum f A - f a else setsum f A)"
  1435 by (erule finite_induct) (auto simp add: insert_Diff_if)
  1436 
  1437 lemma setsum_diff1'[rule_format]:
  1438   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
  1439 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))"])
  1440 apply (auto simp add: insert_Diff_if add_ac)
  1441 done
  1442 
  1443 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
  1444   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
  1445 unfolding setsum_diff1'[OF assms] by auto
  1446 
  1447 (* By Jeremy Siek: *)
  1448 
  1449 lemma setsum_diff_nat: 
  1450 assumes "finite B" and "B \<subseteq> A"
  1451 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1452 using assms
  1453 proof induct
  1454   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1455 next
  1456   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1457     and xFinA: "insert x F \<subseteq> A"
  1458     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1459   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1460   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1461     by (simp add: setsum_diff1_nat)
  1462   from xFinA have "F \<subseteq> A" by simp
  1463   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1464   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1465     by simp
  1466   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1467   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1468     by simp
  1469   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1470   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1471     by simp
  1472   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1473 qed
  1474 
  1475 lemma setsum_diff:
  1476   assumes le: "finite A" "B \<subseteq> A"
  1477   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1478 proof -
  1479   from le have finiteB: "finite B" using finite_subset by auto
  1480   show ?thesis using finiteB le
  1481   proof induct
  1482     case empty
  1483     thus ?case by auto
  1484   next
  1485     case (insert x F)
  1486     thus ?case using le finiteB 
  1487       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1488   qed
  1489 qed
  1490 
  1491 lemma setsum_mono:
  1492   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
  1493   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1494 proof (cases "finite K")
  1495   case True
  1496   thus ?thesis using le
  1497   proof induct
  1498     case empty
  1499     thus ?case by simp
  1500   next
  1501     case insert
  1502     thus ?case using add_mono by fastsimp
  1503   qed
  1504 next
  1505   case False
  1506   thus ?thesis
  1507     by (simp add: setsum_def)
  1508 qed
  1509 
  1510 lemma setsum_strict_mono:
  1511   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
  1512   assumes "finite A"  "A \<noteq> {}"
  1513     and "!!x. x:A \<Longrightarrow> f x < g x"
  1514   shows "setsum f A < setsum g A"
  1515   using prems
  1516 proof (induct rule: finite_ne_induct)
  1517   case singleton thus ?case by simp
  1518 next
  1519   case insert thus ?case by (auto simp: add_strict_mono)
  1520 qed
  1521 
  1522 lemma setsum_negf:
  1523   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
  1524 proof (cases "finite A")
  1525   case True thus ?thesis by (induct set: finite) auto
  1526 next
  1527   case False thus ?thesis by (simp add: setsum_def)
  1528 qed
  1529 
  1530 lemma setsum_subtractf:
  1531   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1532     setsum f A - setsum g A"
  1533 proof (cases "finite A")
  1534   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
  1535 next
  1536   case False thus ?thesis by (simp add: setsum_def)
  1537 qed
  1538 
  1539 lemma setsum_nonneg:
  1540   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
  1541   shows "0 \<le> setsum f A"
  1542 proof (cases "finite A")
  1543   case True thus ?thesis using nn
  1544   proof induct
  1545     case empty then show ?case by simp
  1546   next
  1547     case (insert x F)
  1548     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
  1549     with insert show ?case by simp
  1550   qed
  1551 next
  1552   case False thus ?thesis by (simp add: setsum_def)
  1553 qed
  1554 
  1555 lemma setsum_nonpos:
  1556   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
  1557   shows "setsum f A \<le> 0"
  1558 proof (cases "finite A")
  1559   case True thus ?thesis using np
  1560   proof induct
  1561     case empty then show ?case by simp
  1562   next
  1563     case (insert x F)
  1564     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
  1565     with insert show ?case by simp
  1566   qed
  1567 next
  1568   case False thus ?thesis by (simp add: setsum_def)
  1569 qed
  1570 
  1571 lemma setsum_mono2:
  1572 fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}"
  1573 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
  1574 shows "setsum f A \<le> setsum f B"
  1575 proof -
  1576   have "setsum f A \<le> setsum f A + setsum f (B-A)"
  1577     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
  1578   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1579     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1580   also have "A \<union> (B-A) = B" using sub by blast
  1581   finally show ?thesis .
  1582 qed
  1583 
  1584 lemma setsum_mono3: "finite B ==> A <= B ==> 
  1585     ALL x: B - A. 
  1586       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
  1587         setsum f A <= setsum f B"
  1588   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
  1589   apply (erule ssubst)
  1590   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
  1591   apply simp
  1592   apply (rule add_left_mono)
  1593   apply (erule setsum_nonneg)
  1594   apply (subst setsum_Un_disjoint [THEN sym])
  1595   apply (erule finite_subset, assumption)
  1596   apply (rule finite_subset)
  1597   prefer 2
  1598   apply assumption
  1599   apply (auto simp add: sup_absorb2)
  1600 done
  1601 
  1602 lemma setsum_right_distrib: 
  1603   fixes f :: "'a => ('b::semiring_0)"
  1604   shows "r * setsum f A = setsum (%n. r * f n) A"
  1605 proof (cases "finite A")
  1606   case True
  1607   thus ?thesis
  1608   proof induct
  1609     case empty thus ?case by simp
  1610   next
  1611     case (insert x A) thus ?case by (simp add: right_distrib)
  1612   qed
  1613 next
  1614   case False thus ?thesis by (simp add: setsum_def)
  1615 qed
  1616 
  1617 lemma setsum_left_distrib:
  1618   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
  1619 proof (cases "finite A")
  1620   case True
  1621   then show ?thesis
  1622   proof induct
  1623     case empty thus ?case by simp
  1624   next
  1625     case (insert x A) thus ?case by (simp add: left_distrib)
  1626   qed
  1627 next
  1628   case False thus ?thesis by (simp add: setsum_def)
  1629 qed
  1630 
  1631 lemma setsum_divide_distrib:
  1632   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
  1633 proof (cases "finite A")
  1634   case True
  1635   then show ?thesis
  1636   proof induct
  1637     case empty thus ?case by simp
  1638   next
  1639     case (insert x A) thus ?case by (simp add: add_divide_distrib)
  1640   qed
  1641 next
  1642   case False thus ?thesis by (simp add: setsum_def)
  1643 qed
  1644 
  1645 lemma setsum_abs[iff]: 
  1646   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
  1647   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1648 proof (cases "finite A")
  1649   case True
  1650   thus ?thesis
  1651   proof induct
  1652     case empty thus ?case by simp
  1653   next
  1654     case (insert x A)
  1655     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1656   qed
  1657 next
  1658   case False thus ?thesis by (simp add: setsum_def)
  1659 qed
  1660 
  1661 lemma setsum_abs_ge_zero[iff]: 
  1662   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
  1663   shows "0 \<le> setsum (%i. abs(f i)) A"
  1664 proof (cases "finite A")
  1665   case True
  1666   thus ?thesis
  1667   proof induct
  1668     case empty thus ?case by simp
  1669   next
  1670     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
  1671   qed
  1672 next
  1673   case False thus ?thesis by (simp add: setsum_def)
  1674 qed
  1675 
  1676 lemma abs_setsum_abs[simp]: 
  1677   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
  1678   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1679 proof (cases "finite A")
  1680   case True
  1681   thus ?thesis
  1682   proof induct
  1683     case empty thus ?case by simp
  1684   next
  1685     case (insert a A)
  1686     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
  1687     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1688     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
  1689       by (simp del: abs_of_nonneg)
  1690     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1691     finally show ?case .
  1692   qed
  1693 next
  1694   case False thus ?thesis by (simp add: setsum_def)
  1695 qed
  1696 
  1697 
  1698 lemma setsum_Plus:
  1699   fixes A :: "'a set" and B :: "'b set"
  1700   assumes fin: "finite A" "finite B"
  1701   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
  1702 proof -
  1703   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
  1704   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
  1705     by(auto intro: finite_imageI)
  1706   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
  1707   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
  1708   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
  1709 qed
  1710 
  1711 
  1712 text {* Commuting outer and inner summation *}
  1713 
  1714 lemma swap_inj_on:
  1715   "inj_on (%(i, j). (j, i)) (A \<times> B)"
  1716   by (unfold inj_on_def) fast
  1717 
  1718 lemma swap_product:
  1719   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
  1720   by (simp add: split_def image_def) blast
  1721 
  1722 lemma setsum_commute:
  1723   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
  1724 proof (simp add: setsum_cartesian_product)
  1725   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
  1726     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
  1727     (is "?s = _")
  1728     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
  1729     apply (simp add: split_def)
  1730     done
  1731   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
  1732     (is "_ = ?t")
  1733     apply (simp add: swap_product)
  1734     done
  1735   finally show "?s = ?t" .
  1736 qed
  1737 
  1738 lemma setsum_product:
  1739   fixes f :: "'a => ('b::semiring_0)"
  1740   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
  1741   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
  1742 
  1743 lemma setsum_mult_setsum_if_inj:
  1744 fixes f :: "'a => ('b::semiring_0)"
  1745 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
  1746   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
  1747 by(auto simp: setsum_product setsum_cartesian_product
  1748         intro!:  setsum_reindex_cong[symmetric])
  1749 
  1750 
  1751 subsection {* Generalized product over a set *}
  1752 
  1753 definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1754 where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
  1755 
  1756 abbreviation
  1757   Setprod  ("\<Prod>_" [1000] 999) where
  1758   "\<Prod>A == setprod (%x. x) A"
  1759 
  1760 syntax
  1761   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1762 syntax (xsymbols)
  1763   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1764 syntax (HTML output)
  1765   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1766 
  1767 translations -- {* Beware of argument permutation! *}
  1768   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1769   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1770 
  1771 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1772  @{text"\<Prod>x|P. e"}. *}
  1773 
  1774 syntax
  1775   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1776 syntax (xsymbols)
  1777   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1778 syntax (HTML output)
  1779   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1780 
  1781 translations
  1782   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1783   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1784 
  1785 
  1786 lemma setprod_empty [simp]: "setprod f {} = 1"
  1787 by (auto simp add: setprod_def)
  1788 
  1789 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1790     setprod f (insert a A) = f a * setprod f A"
  1791 by (simp add: setprod_def)
  1792 
  1793 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1794 by (simp add: setprod_def)
  1795 
  1796 lemma setprod_reindex:
  1797    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1798 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
  1799 
  1800 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1801 by (auto simp add: setprod_reindex)
  1802 
  1803 lemma setprod_cong:
  1804   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1805 by(fastsimp simp: setprod_def intro: fold_image_cong)
  1806 
  1807 lemma strong_setprod_cong[cong]:
  1808   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1809 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
  1810 
  1811 lemma setprod_reindex_cong: "inj_on f A ==>
  1812     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1813 by (frule setprod_reindex, simp)
  1814 
  1815 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
  1816   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
  1817   shows "setprod h B = setprod g A"
  1818 proof-
  1819     have "setprod h B = setprod (h o f) A"
  1820       by (simp add: B setprod_reindex[OF i, of h])
  1821     then show ?thesis apply simp
  1822       apply (rule setprod_cong)
  1823       apply simp
  1824       by (simp add: eq)
  1825 qed
  1826 
  1827 lemma setprod_Un_one:  
  1828   assumes fS: "finite S" and fT: "finite T"
  1829   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
  1830   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
  1831   using fS fT
  1832   apply (simp add: setprod_def)
  1833   apply (rule fold_image_Un_one)
  1834   using I0 by auto
  1835 
  1836 
  1837 lemma setprod_1: "setprod (%i. 1) A = 1"
  1838 apply (case_tac "finite A")
  1839 apply (erule finite_induct, auto simp add: mult_ac)
  1840 done
  1841 
  1842 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1843 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1844 apply (erule ssubst, rule setprod_1)
  1845 apply (rule setprod_cong, auto)
  1846 done
  1847 
  1848 lemma setprod_Un_Int: "finite A ==> finite B
  1849     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1850 by(simp add: setprod_def fold_image_Un_Int[symmetric])
  1851 
  1852 lemma setprod_Un_disjoint: "finite A ==> finite B
  1853   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1854 by (subst setprod_Un_Int [symmetric], auto)
  1855 
  1856 lemma setprod_mono_one_left: 
  1857   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1858   and z: "\<forall>i \<in> T - S. f i = 1"
  1859   shows "setprod f S = setprod f T"
  1860 proof-
  1861   have eq: "T = S \<union> (T - S)" using ST by blast
  1862   have d: "S \<inter> (T - S) = {}" using ST by blast
  1863   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
  1864   show ?thesis
  1865   by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
  1866 qed
  1867 
  1868 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
  1869 
  1870 lemma setprod_delta: 
  1871   assumes fS: "finite S"
  1872   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  1873 proof-
  1874   let ?f = "(\<lambda>k. if k=a then b k else 1)"
  1875   {assume a: "a \<notin> S"
  1876     hence "\<forall> k\<in> S. ?f k = 1" by simp
  1877     hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
  1878   moreover 
  1879   {assume a: "a \<in> S"
  1880     let ?A = "S - {a}"
  1881     let ?B = "{a}"
  1882     have eq: "S = ?A \<union> ?B" using a by blast 
  1883     have dj: "?A \<inter> ?B = {}" by simp
  1884     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1885     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
  1886     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1887       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1888       by simp
  1889     then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
  1890   ultimately show ?thesis by blast
  1891 qed
  1892 
  1893 lemma setprod_delta': 
  1894   assumes fS: "finite S" shows 
  1895   "setprod (\<lambda>k. if a = k then b k else 1) S = 
  1896      (if a\<in> S then b a else 1)"
  1897   using setprod_delta[OF fS, of a b, symmetric] 
  1898   by (auto intro: setprod_cong)
  1899 
  1900 
  1901 lemma setprod_UN_disjoint:
  1902     "finite I ==> (ALL i:I. finite (A i)) ==>
  1903         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1904       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1905 by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
  1906 
  1907 lemma setprod_Union_disjoint:
  1908   "[| (ALL A:C. finite A);
  1909       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1910    ==> setprod f (Union C) = setprod (setprod f) C"
  1911 apply (cases "finite C") 
  1912  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1913   apply (frule setprod_UN_disjoint [of C id f])
  1914  apply (unfold Union_def id_def, assumption+)
  1915 done
  1916 
  1917 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1918     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1919     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1920 by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
  1921 
  1922 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1923 lemma setprod_cartesian_product: 
  1924      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1925 apply (cases "finite A") 
  1926  apply (cases "finite B") 
  1927   apply (simp add: setprod_Sigma)
  1928  apply (cases "A={}", simp)
  1929  apply (simp add: setprod_1) 
  1930 apply (auto simp add: setprod_def
  1931             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1932 done
  1933 
  1934 lemma setprod_timesf:
  1935      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1936 by(simp add:setprod_def fold_image_distrib)
  1937 
  1938 
  1939 subsubsection {* Properties in more restricted classes of structures *}
  1940 
  1941 lemma setprod_eq_1_iff [simp]:
  1942   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1943 by (induct set: finite) auto
  1944 
  1945 lemma setprod_zero:
  1946      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1947 apply (induct set: finite, force, clarsimp)
  1948 apply (erule disjE, auto)
  1949 done
  1950 
  1951 lemma setprod_nonneg [rule_format]:
  1952    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1953 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  1954 
  1955 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  1956   --> 0 < setprod f A"
  1957 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  1958 
  1959 lemma setprod_zero_iff[simp]: "finite A ==> 
  1960   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1961   (EX x: A. f x = 0)"
  1962 by (erule finite_induct, auto simp:no_zero_divisors)
  1963 
  1964 lemma setprod_pos_nat:
  1965   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1966 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1967 
  1968 lemma setprod_pos_nat_iff[simp]:
  1969   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1970 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1971 
  1972 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1973   (setprod f (A Un B) :: 'a ::{field})
  1974    = setprod f A * setprod f B / setprod f (A Int B)"
  1975 by (subst setprod_Un_Int [symmetric], auto)
  1976 
  1977 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1978   (setprod f (A - {a}) :: 'a :: {field}) =
  1979   (if a:A then setprod f A / f a else setprod f A)"
  1980 by (erule finite_induct) (auto simp add: insert_Diff_if)
  1981 
  1982 lemma setprod_inversef: 
  1983   fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
  1984   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1985 by (erule finite_induct) auto
  1986 
  1987 lemma setprod_dividef:
  1988   fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
  1989   shows "finite A
  1990     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1991 apply (subgoal_tac
  1992          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1993 apply (erule ssubst)
  1994 apply (subst divide_inverse)
  1995 apply (subst setprod_timesf)
  1996 apply (subst setprod_inversef, assumption+, rule refl)
  1997 apply (rule setprod_cong, rule refl)
  1998 apply (subst divide_inverse, auto)
  1999 done
  2000 
  2001 lemma setprod_dvd_setprod [rule_format]: 
  2002     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  2003   apply (cases "finite A")
  2004   apply (induct set: finite)
  2005   apply (auto simp add: dvd_def)
  2006   apply (rule_tac x = "k * ka" in exI)
  2007   apply (simp add: algebra_simps)
  2008 done
  2009 
  2010 lemma setprod_dvd_setprod_subset:
  2011   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  2012   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  2013   apply (unfold dvd_def, blast)
  2014   apply (subst setprod_Un_disjoint [symmetric])
  2015   apply (auto elim: finite_subset intro: setprod_cong)
  2016 done
  2017 
  2018 lemma setprod_dvd_setprod_subset2:
  2019   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  2020       setprod f A dvd setprod g B"
  2021   apply (rule dvd_trans)
  2022   apply (rule setprod_dvd_setprod, erule (1) bspec)
  2023   apply (erule (1) setprod_dvd_setprod_subset)
  2024 done
  2025 
  2026 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  2027     (f i ::'a::comm_semiring_1) dvd setprod f A"
  2028 by (induct set: finite) (auto intro: dvd_mult)
  2029 
  2030 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  2031     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  2032   apply (cases "finite A")
  2033   apply (induct set: finite)
  2034   apply auto
  2035 done
  2036 
  2037 
  2038 subsection {* Finite cardinality *}
  2039 
  2040 text {* This definition, although traditional, is ugly to work with:
  2041 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  2042 But now that we have @{text setsum} things are easy:
  2043 *}
  2044 
  2045 definition card :: "'a set \<Rightarrow> nat" where
  2046   "card A = setsum (\<lambda>x. 1) A"
  2047 
  2048 lemmas card_eq_setsum = card_def
  2049 
  2050 lemma card_empty [simp]: "card {} = 0"
  2051   by (simp add: card_def)
  2052 
  2053 lemma card_insert_disjoint [simp]:
  2054   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  2055   by (simp add: card_def)
  2056 
  2057 lemma card_insert_if:
  2058   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  2059   by (simp add: insert_absorb)
  2060 
  2061 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  2062   by (simp add: card_def)
  2063 
  2064 lemma card_ge_0_finite:
  2065   "card A > 0 \<Longrightarrow> finite A"
  2066   by (rule ccontr) simp
  2067 
  2068 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
  2069   apply auto
  2070   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  2071   done
  2072 
  2073 lemma finite_UNIV_card_ge_0:
  2074   "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
  2075   by (rule ccontr) simp
  2076 
  2077 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  2078   by auto
  2079 
  2080 lemma card_gt_0_iff: "(0 < card A) = (A \<noteq> {} & finite A)"
  2081   by (simp add: neq0_conv [symmetric] card_eq_0_iff) 
  2082 
  2083 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  2084 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  2085 apply(simp del:insert_Diff_single)
  2086 done
  2087 
  2088 lemma card_Diff_singleton:
  2089   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  2090 by (simp add: card_Suc_Diff1 [symmetric])
  2091 
  2092 lemma card_Diff_singleton_if:
  2093   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  2094 by (simp add: card_Diff_singleton)
  2095 
  2096 lemma card_Diff_insert[simp]:
  2097 assumes "finite A" and "a:A" and "a ~: B"
  2098 shows "card(A - insert a B) = card(A - B) - 1"
  2099 proof -
  2100   have "A - insert a B = (A - B) - {a}" using assms by blast
  2101   then show ?thesis using assms by(simp add:card_Diff_singleton)
  2102 qed
  2103 
  2104 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  2105 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
  2106 
  2107 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  2108 by (simp add: card_insert_if)
  2109 
  2110 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  2111 by (simp add: card_def setsum_mono2)
  2112 
  2113 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  2114 apply (induct set: finite, simp, clarify)
  2115 apply (subgoal_tac "finite A & A - {x} <= F")
  2116  prefer 2 apply (blast intro: finite_subset, atomize)
  2117 apply (drule_tac x = "A - {x}" in spec)
  2118 apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  2119 apply (case_tac "card A", auto)
  2120 done
  2121 
  2122 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  2123 apply (simp add: psubset_eq linorder_not_le [symmetric])
  2124 apply (blast dest: card_seteq)
  2125 done
  2126 
  2127 lemma card_Un_Int: "finite A ==> finite B
  2128     ==> card A + card B = card (A Un B) + card (A Int B)"
  2129 by(simp add:card_def setsum_Un_Int)
  2130 
  2131 lemma card_Un_disjoint: "finite A ==> finite B
  2132     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  2133 by (simp add: card_Un_Int)
  2134 
  2135 lemma card_Diff_subset:
  2136   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  2137 by(simp add:card_def setsum_diff_nat)
  2138 
  2139 lemma card_Diff_subset_Int:
  2140   assumes AB: "finite (A \<inter> B)" shows "card (A - B) = card A - card (A \<inter> B)"
  2141 proof -
  2142   have "A - B = A - A \<inter> B" by auto
  2143   thus ?thesis
  2144     by (simp add: card_Diff_subset AB) 
  2145 qed
  2146 
  2147 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  2148 apply (rule Suc_less_SucD)
  2149 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
  2150 done
  2151 
  2152 lemma card_Diff2_less:
  2153   "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  2154 apply (case_tac "x = y")
  2155  apply (simp add: card_Diff1_less del:card_Diff_insert)
  2156 apply (rule less_trans)
  2157  prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
  2158 done
  2159 
  2160 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  2161 apply (case_tac "x : A")
  2162  apply (simp_all add: card_Diff1_less less_imp_le)
  2163 done
  2164 
  2165 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  2166 by (erule psubsetI, blast)
  2167 
  2168 lemma insert_partition:
  2169   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  2170   \<Longrightarrow> x \<inter> \<Union> F = {}"
  2171 by auto
  2172 
  2173 lemma finite_psubset_induct[consumes 1, case_names psubset]:
  2174   assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A"
  2175 using assms(1)
  2176 proof (induct A rule: measure_induct_rule[where f=card])
  2177   case (less A)
  2178   show ?case
  2179   proof(rule assms(2)[OF less(2)])
  2180     fix B assume "finite B" "B \<subset> A"
  2181     show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
  2182   qed
  2183 qed
  2184 
  2185 text{* main cardinality theorem *}
  2186 lemma card_partition [rule_format]:
  2187   "finite C ==>
  2188      finite (\<Union> C) -->
  2189      (\<forall>c\<in>C. card c = k) -->
  2190      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
  2191      k * card(C) = card (\<Union> C)"
  2192 apply (erule finite_induct, simp)
  2193 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  2194        finite_subset [of _ "\<Union> (insert x F)"])
  2195 done
  2196 
  2197 lemma card_eq_UNIV_imp_eq_UNIV:
  2198   assumes fin: "finite (UNIV :: 'a set)"
  2199   and card: "card A = card (UNIV :: 'a set)"
  2200   shows "A = (UNIV :: 'a set)"
  2201 proof
  2202   show "A \<subseteq> UNIV" by simp
  2203   show "UNIV \<subseteq> A"
  2204   proof
  2205     fix x
  2206     show "x \<in> A"
  2207     proof (rule ccontr)
  2208       assume "x \<notin> A"
  2209       then have "A \<subset> UNIV" by auto
  2210       with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
  2211       with card show False by simp
  2212     qed
  2213   qed
  2214 qed
  2215 
  2216 text{*The form of a finite set of given cardinality*}
  2217 
  2218 lemma card_eq_SucD:
  2219 assumes "card A = Suc k"
  2220 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
  2221 proof -
  2222   have fin: "finite A" using assms by (auto intro: ccontr)
  2223   moreover have "card A \<noteq> 0" using assms by auto
  2224   ultimately obtain b where b: "b \<in> A" by auto
  2225   show ?thesis
  2226   proof (intro exI conjI)
  2227     show "A = insert b (A-{b})" using b by blast
  2228     show "b \<notin> A - {b}" by blast
  2229     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
  2230       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
  2231   qed
  2232 qed
  2233 
  2234 lemma card_Suc_eq:
  2235   "(card A = Suc k) =
  2236    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
  2237 apply(rule iffI)
  2238  apply(erule card_eq_SucD)
  2239 apply(auto)
  2240 apply(subst card_insert)
  2241  apply(auto intro:ccontr)
  2242 done
  2243 
  2244 lemma finite_fun_UNIVD2:
  2245   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
  2246   shows "finite (UNIV :: 'b set)"
  2247 proof -
  2248   from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
  2249     by(rule finite_imageI)
  2250   moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
  2251     by(rule UNIV_eq_I) auto
  2252   ultimately show "finite (UNIV :: 'b set)" by simp
  2253 qed
  2254 
  2255 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  2256 apply (cases "finite A")
  2257 apply (erule finite_induct)
  2258 apply (auto simp add: algebra_simps)
  2259 done
  2260 
  2261 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  2262 apply (erule finite_induct)
  2263 apply (auto simp add: power_Suc)
  2264 done
  2265 
  2266 lemma setprod_gen_delta:
  2267   assumes fS: "finite S"
  2268   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)"
  2269 proof-
  2270   let ?f = "(\<lambda>k. if k=a then b k else c)"
  2271   {assume a: "a \<notin> S"
  2272     hence "\<forall> k\<in> S. ?f k = c" by simp
  2273     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
  2274   moreover 
  2275   {assume a: "a \<in> S"
  2276     let ?A = "S - {a}"
  2277     let ?B = "{a}"
  2278     have eq: "S = ?A \<union> ?B" using a by blast 
  2279     have dj: "?A \<inter> ?B = {}" by simp
  2280     from fS have fAB: "finite ?A" "finite ?B" by auto  
  2281     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  2282       apply (rule setprod_cong) by auto
  2283     have cA: "card ?A = card S - 1" using fS a by auto
  2284     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  2285     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  2286       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  2287       by simp
  2288     then have ?thesis using a cA
  2289       by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
  2290   ultimately show ?thesis by blast
  2291 qed
  2292 
  2293 
  2294 lemma setsum_bounded:
  2295   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
  2296   shows "setsum f A \<le> of_nat(card A) * K"
  2297 proof (cases "finite A")
  2298   case True
  2299   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  2300 next
  2301   case False thus ?thesis by (simp add: setsum_def)
  2302 qed
  2303 
  2304 
  2305 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
  2306   unfolding UNIV_unit by simp
  2307 
  2308 
  2309 subsubsection {* Cardinality of unions *}
  2310 
  2311 lemma card_UN_disjoint:
  2312   "finite I ==> (ALL i:I. finite (A i)) ==>
  2313    (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
  2314    ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  2315 apply (simp add: card_def del: setsum_constant)
  2316 apply (subgoal_tac
  2317          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  2318 apply (simp add: setsum_UN_disjoint del: setsum_constant)
  2319 apply (simp cong: setsum_cong)
  2320 done
  2321 
  2322 lemma card_Union_disjoint:
  2323   "finite C ==> (ALL A:C. finite A) ==>
  2324    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  2325    ==> card (Union C) = setsum card C"
  2326 apply (frule card_UN_disjoint [of C id])
  2327 apply (unfold Union_def id_def, assumption+)
  2328 done
  2329 
  2330 
  2331 subsubsection {* Cardinality of image *}
  2332 
  2333 text{*The image of a finite set can be expressed using @{term fold_image}.*}
  2334 lemma image_eq_fold_image:
  2335   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
  2336 proof (induct rule: finite_induct)
  2337   case empty then show ?case by simp
  2338 next
  2339   interpret ab_semigroup_mult "op Un"
  2340     proof qed auto
  2341   case insert 
  2342   then show ?case by simp
  2343 qed
  2344 
  2345 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  2346 apply (induct set: finite)
  2347  apply simp
  2348 apply (simp add: le_SucI finite_imageI card_insert_if)
  2349 done
  2350 
  2351 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  2352 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  2353 
  2354 lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
  2355 by(auto simp: card_image bij_betw_def)
  2356 
  2357 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  2358 by (simp add: card_seteq card_image)
  2359 
  2360 lemma eq_card_imp_inj_on:
  2361   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  2362 apply (induct rule:finite_induct)
  2363 apply simp
  2364 apply(frule card_image_le[where f = f])
  2365 apply(simp add:card_insert_if split:if_splits)
  2366 done
  2367 
  2368 lemma inj_on_iff_eq_card:
  2369   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  2370 by(blast intro: card_image eq_card_imp_inj_on)
  2371 
  2372 
  2373 lemma card_inj_on_le:
  2374   "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  2375 apply (subgoal_tac "finite A") 
  2376  apply (force intro: card_mono simp add: card_image [symmetric])
  2377 apply (blast intro: finite_imageD dest: finite_subset) 
  2378 done
  2379 
  2380 lemma card_bij_eq:
  2381   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  2382      finite A; finite B |] ==> card A = card B"
  2383 by (auto intro: le_antisym card_inj_on_le)
  2384 
  2385 
  2386 subsubsection {* Cardinality of products *}
  2387 
  2388 (*
  2389 lemma SigmaI_insert: "y \<notin> A ==>
  2390   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  2391   by auto
  2392 *)
  2393 
  2394 lemma card_SigmaI [simp]:
  2395   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  2396   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  2397 by(simp add:card_def setsum_Sigma del:setsum_constant)
  2398 
  2399 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  2400 apply (cases "finite A") 
  2401 apply (cases "finite B") 
  2402 apply (auto simp add: card_eq_0_iff
  2403             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  2404 done
  2405 
  2406 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  2407 by (simp add: card_cartesian_product)
  2408 
  2409 
  2410 subsubsection {* Cardinality of sums *}
  2411 
  2412 lemma card_Plus:
  2413   assumes "finite A" and "finite B"
  2414   shows "card (A <+> B) = card A + card B"
  2415 proof -
  2416   have "Inl`A \<inter> Inr`B = {}" by fast
  2417   with assms show ?thesis
  2418     unfolding Plus_def
  2419     by (simp add: card_Un_disjoint card_image)
  2420 qed
  2421 
  2422 lemma card_Plus_conv_if:
  2423   "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)"
  2424 by(auto simp: card_def setsum_Plus simp del: setsum_constant)
  2425 
  2426 
  2427 subsubsection {* Cardinality of the Powerset *}
  2428 
  2429 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  2430 apply (induct set: finite)
  2431  apply (simp_all add: Pow_insert)
  2432 apply (subst card_Un_disjoint, blast)
  2433   apply (blast intro: finite_imageI, blast)
  2434 apply (subgoal_tac "inj_on (insert x) (Pow F)")
  2435  apply (simp add: card_image Pow_insert)
  2436 apply (unfold inj_on_def)
  2437 apply (blast elim!: equalityE)
  2438 done
  2439 
  2440 text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
  2441 
  2442 lemma dvd_partition:
  2443   "finite (Union C) ==>
  2444     ALL c : C. k dvd card c ==>
  2445     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  2446   k dvd card (Union C)"
  2447 apply(frule finite_UnionD)
  2448 apply(rotate_tac -1)
  2449 apply (induct set: finite, simp_all, clarify)
  2450 apply (subst card_Un_disjoint)
  2451    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  2452 done
  2453 
  2454 
  2455 subsubsection {* Relating injectivity and surjectivity *}
  2456 
  2457 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
  2458 apply(rule eq_card_imp_inj_on, assumption)
  2459 apply(frule finite_imageI)
  2460 apply(drule (1) card_seteq)
  2461  apply(erule card_image_le)
  2462 apply simp
  2463 done
  2464 
  2465 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
  2466 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
  2467 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
  2468 
  2469 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
  2470 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
  2471 by(fastsimp simp:surj_def dest!: endo_inj_surj)
  2472 
  2473 corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
  2474 proof
  2475   assume "finite(UNIV::nat set)"
  2476   with finite_UNIV_inj_surj[of Suc]
  2477   show False by simp (blast dest: Suc_neq_Zero surjD)
  2478 qed
  2479 
  2480 (* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
  2481 lemma infinite_UNIV_char_0[noatp]:
  2482   "\<not> finite (UNIV::'a::semiring_char_0 set)"
  2483 proof
  2484   assume "finite (UNIV::'a set)"
  2485   with subset_UNIV have "finite (range of_nat::'a set)"
  2486     by (rule finite_subset)
  2487   moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
  2488     by (simp add: inj_on_def)
  2489   ultimately have "finite (UNIV::nat set)"
  2490     by (rule finite_imageD)
  2491   then show "False"
  2492     by (simp add: infinite_UNIV_nat)
  2493 qed
  2494 
  2495 subsection{* A fold functional for non-empty sets *}
  2496 
  2497 text{* Does not require start value. *}
  2498 
  2499 inductive
  2500   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
  2501   for f :: "'a => 'a => 'a"
  2502 where
  2503   fold1Set_insertI [intro]:
  2504    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
  2505 
  2506 constdefs
  2507   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  2508   "fold1 f A == THE x. fold1Set f A x"
  2509 
  2510 lemma fold1Set_nonempty:
  2511   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
  2512 by(erule fold1Set.cases, simp_all)
  2513 
  2514 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
  2515 
  2516 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
  2517 
  2518 
  2519 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
  2520 by (blast intro: fold_graph.intros elim: fold_graph.cases)
  2521 
  2522 lemma fold1_singleton [simp]: "fold1 f {a} = a"
  2523 by (unfold fold1_def) blast
  2524 
  2525 lemma finite_nonempty_imp_fold1Set:
  2526   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
  2527 apply (induct A rule: finite_induct)
  2528 apply (auto dest: finite_imp_fold_graph [of _ f])
  2529 done
  2530 
  2531 text{*First, some lemmas about @{const fold_graph}.*}
  2532 
  2533 context ab_semigroup_mult
  2534 begin
  2535 
  2536 lemma fun_left_comm: "fun_left_comm(op *)"
  2537 by unfold_locales (simp add: mult_ac)
  2538 
  2539 lemma fold_graph_insert_swap:
  2540 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
  2541 shows "fold_graph times z (insert b A) (z * y)"
  2542 proof -
  2543   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2544 from assms show ?thesis
  2545 proof (induct rule: fold_graph.induct)
  2546   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
  2547 next
  2548   case (insertI x A y)
  2549     have "fold_graph times z (insert x (insert b A)) (x * (z * y))"
  2550       using insertI by force  --{*how does @{term id} get unfolded?*}
  2551     thus ?case by (simp add: insert_commute mult_ac)
  2552 qed
  2553 qed
  2554 
  2555 lemma fold_graph_permute_diff:
  2556 assumes fold: "fold_graph times b A x"
  2557 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> fold_graph times a (insert b (A-{a})) x"
  2558 using fold
  2559 proof (induct rule: fold_graph.induct)
  2560   case emptyI thus ?case by simp
  2561 next
  2562   case (insertI x A y)
  2563   have "a = x \<or> a \<in> A" using insertI by simp
  2564   thus ?case
  2565   proof
  2566     assume "a = x"
  2567     with insertI show ?thesis
  2568       by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap)
  2569   next
  2570     assume ainA: "a \<in> A"
  2571     hence "fold_graph times a (insert x (insert b (A - {a}))) (x * y)"
  2572       using insertI by force
  2573     moreover
  2574     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  2575       using ainA insertI by blast
  2576     ultimately show ?thesis by simp
  2577   qed
  2578 qed
  2579 
  2580 lemma fold1_eq_fold:
  2581 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
  2582 proof -
  2583   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2584   from assms show ?thesis
  2585 apply (simp add: fold1_def fold_def)
  2586 apply (rule the_equality)
  2587 apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
  2588 apply (rule sym, clarify)
  2589 apply (case_tac "Aa=A")
  2590  apply (best intro: the_equality fold_graph_determ)
  2591 apply (subgoal_tac "fold_graph times a A x")
  2592  apply (best intro: the_equality fold_graph_determ)
  2593 apply (subgoal_tac "insert aa (Aa - {a}) = A")
  2594  prefer 2 apply (blast elim: equalityE)
  2595 apply (auto dest: fold_graph_permute_diff [where a=a])
  2596 done
  2597 qed
  2598 
  2599 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  2600 apply safe
  2601  apply simp
  2602  apply (drule_tac x=x in spec)
  2603  apply (drule_tac x="A-{x}" in spec, auto)
  2604 done
  2605 
  2606 lemma fold1_insert:
  2607   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  2608   shows "fold1 times (insert x A) = x * fold1 times A"
  2609 proof -
  2610   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2611   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
  2612     by (auto simp add: nonempty_iff)
  2613   with A show ?thesis
  2614     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)
  2615 qed
  2616 
  2617 end
  2618 
  2619 context ab_semigroup_idem_mult
  2620 begin
  2621 
  2622 lemma fold1_insert_idem [simp]:
  2623   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  2624   shows "fold1 times (insert x A) = x * fold1 times A"
  2625 proof -
  2626   interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2627     by (rule fun_left_comm_idem)
  2628   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
  2629     by (auto simp add: nonempty_iff)
  2630   show ?thesis
  2631   proof cases
  2632     assume "a = x"
  2633     thus ?thesis
  2634     proof cases
  2635       assume "A' = {}"
  2636       with prems show ?thesis by (simp add: mult_idem)
  2637     next
  2638       assume "A' \<noteq> {}"
  2639       with prems show ?thesis
  2640         by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
  2641     qed
  2642   next
  2643     assume "a \<noteq> x"
  2644     with prems show ?thesis
  2645       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  2646   qed
  2647 qed
  2648 
  2649 lemma hom_fold1_commute:
  2650 assumes hom: "!!x y. h (x * y) = h x * h y"
  2651 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
  2652 using N proof (induct rule: finite_ne_induct)
  2653   case singleton thus ?case by simp
  2654 next
  2655   case (insert n N)
  2656   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
  2657   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
  2658   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
  2659   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
  2660     using insert by(simp)
  2661   also have "insert (h n) (h ` N) = h ` insert n N" by simp
  2662   finally show ?case .
  2663 qed
  2664 
  2665 lemma fold1_eq_fold_idem:
  2666   assumes "finite A"
  2667   shows "fold1 times (insert a A) = fold times a A"
  2668 proof (cases "a \<in> A")
  2669   case False
  2670   with assms show ?thesis by (simp add: fold1_eq_fold)
  2671 next
  2672   interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
  2673   case True then obtain b B
  2674     where A: "A = insert a B" and "a \<notin> B" by (rule set_insert)
  2675   with assms have "finite B" by auto
  2676   then have "fold times a (insert a B) = fold times (a * a) B"
  2677     using `a \<notin> B` by (rule fold_insert2)
  2678   then show ?thesis
  2679     using `a \<notin> B` `finite B` by (simp add: fold1_eq_fold A)
  2680 qed
  2681 
  2682 end
  2683 
  2684 
  2685 text{* Now the recursion rules for definitions: *}
  2686 
  2687 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
  2688 by(simp add:fold1_singleton)
  2689 
  2690 lemma (in ab_semigroup_mult) fold1_insert_def:
  2691   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2692 by (simp add:fold1_insert)
  2693 
  2694 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
  2695   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2696 by simp
  2697 
  2698 subsubsection{* Determinacy for @{term fold1Set} *}
  2699 
  2700 (*Not actually used!!*)
  2701 (*
  2702 context ab_semigroup_mult
  2703 begin
  2704 
  2705 lemma fold_graph_permute:
  2706   "[|fold_graph times id b (insert a A) x; a \<notin> A; b \<notin> A|]
  2707    ==> fold_graph times id a (insert b A) x"
  2708 apply (cases "a=b") 
  2709 apply (auto dest: fold_graph_permute_diff) 
  2710 done
  2711 
  2712 lemma fold1Set_determ:
  2713   "fold1Set times A x ==> fold1Set times A y ==> y = x"
  2714 proof (clarify elim!: fold1Set.cases)
  2715   fix A x B y a b
  2716   assume Ax: "fold_graph times id a A x"
  2717   assume By: "fold_graph times id b B y"
  2718   assume anotA:  "a \<notin> A"
  2719   assume bnotB:  "b \<notin> B"
  2720   assume eq: "insert a A = insert b B"
  2721   show "y=x"
  2722   proof cases
  2723     assume same: "a=b"
  2724     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  2725     thus ?thesis using Ax By same by (blast intro: fold_graph_determ)
  2726   next
  2727     assume diff: "a\<noteq>b"
  2728     let ?D = "B - {a}"
  2729     have B: "B = insert a ?D" and A: "A = insert b ?D"
  2730      and aB: "a \<in> B" and bA: "b \<in> A"
  2731       using eq anotA bnotB diff by (blast elim!:equalityE)+
  2732     with aB bnotB By
  2733     have "fold_graph times id a (insert b ?D) y" 
  2734       by (auto intro: fold_graph_permute simp add: insert_absorb)
  2735     moreover
  2736     have "fold_graph times id a (insert b ?D) x"
  2737       by (simp add: A [symmetric] Ax) 
  2738     ultimately show ?thesis by (blast intro: fold_graph_determ) 
  2739   qed
  2740 qed
  2741 
  2742 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
  2743   by (unfold fold1_def) (blast intro: fold1Set_determ)
  2744 
  2745 end
  2746 *)
  2747 
  2748 declare
  2749   empty_fold_graphE [rule del]  fold_graph.intros [rule del]
  2750   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  2751   -- {* No more proofs involve these relations. *}
  2752 
  2753 subsubsection {* Lemmas about @{text fold1} *}
  2754 
  2755 context ab_semigroup_mult
  2756 begin
  2757 
  2758 lemma fold1_Un:
  2759 assumes A: "finite A" "A \<noteq> {}"
  2760 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2761        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2762 using A by (induct rule: finite_ne_induct)
  2763   (simp_all add: fold1_insert mult_assoc)
  2764 
  2765 lemma fold1_in:
  2766   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
  2767   shows "fold1 times A \<in> A"
  2768 using A
  2769 proof (induct rule:finite_ne_induct)
  2770   case singleton thus ?case by simp
  2771 next
  2772   case insert thus ?case using elem by (force simp add:fold1_insert)
  2773 qed
  2774 
  2775 end
  2776 
  2777 lemma (in ab_semigroup_idem_mult) fold1_Un2:
  2778 assumes A: "finite A" "A \<noteq> {}"
  2779 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2780        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2781 using A
  2782 proof(induct rule:finite_ne_induct)
  2783   case singleton thus ?case by simp
  2784 next
  2785   case insert thus ?case by (simp add: mult_assoc)
  2786 qed
  2787 
  2788 
  2789 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
  2790 
  2791 text{*
  2792   As an application of @{text fold1} we define infimum
  2793   and supremum in (not necessarily complete!) lattices
  2794   over (non-empty) sets by means of @{text fold1}.
  2795 *}
  2796 
  2797 context semilattice_inf
  2798 begin
  2799 
  2800 lemma below_fold1_iff:
  2801   assumes "finite A" "A \<noteq> {}"
  2802   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2803 proof -
  2804   interpret ab_semigroup_idem_mult inf
  2805     by (rule ab_semigroup_idem_mult_inf)
  2806   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  2807 qed
  2808 
  2809 lemma fold1_belowI:
  2810   assumes "finite A"
  2811     and "a \<in> A"
  2812   shows "fold1 inf A \<le> a"
  2813 proof -
  2814   from assms have "A \<noteq> {}" by auto
  2815   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  2816   proof (induct rule: finite_ne_induct)
  2817     case singleton thus ?case by simp
  2818   next
  2819     interpret ab_semigroup_idem_mult inf
  2820       by (rule ab_semigroup_idem_mult_inf)
  2821     case (insert x F)
  2822     from insert(5) have "a = x \<or> a \<in> F" by simp
  2823     thus ?case
  2824     proof
  2825       assume "a = x" thus ?thesis using insert
  2826         by (simp add: mult_ac)
  2827     next
  2828       assume "a \<in> F"
  2829       hence bel: "fold1 inf F \<le> a" by (rule insert)
  2830       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  2831         using insert by (simp add: mult_ac)
  2832       also have "inf (fold1 inf F) a = fold1 inf F"
  2833         using bel by (auto intro: antisym)
  2834       also have "inf x \<dots> = fold1 inf (insert x F)"
  2835         using insert by (simp add: mult_ac)
  2836       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  2837       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  2838       ultimately show ?thesis by simp
  2839     qed
  2840   qed
  2841 qed
  2842 
  2843 end
  2844 
  2845 context lattice
  2846 begin
  2847 
  2848 definition
  2849   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
  2850 where
  2851   "Inf_fin = fold1 inf"
  2852 
  2853 definition
  2854   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
  2855 where
  2856   "Sup_fin = fold1 sup"
  2857 
  2858 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
  2859 apply(unfold Sup_fin_def Inf_fin_def)
  2860 apply(subgoal_tac "EX a. a:A")
  2861 prefer 2 apply blast
  2862 apply(erule exE)
  2863 apply(rule order_trans)
  2864 apply(erule (1) fold1_belowI)
  2865 apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice])
  2866 done
  2867 
  2868 lemma sup_Inf_absorb [simp]:
  2869   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
  2870 apply(subst sup_commute)
  2871 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  2872 done
  2873 
  2874 lemma inf_Sup_absorb [simp]:
  2875   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
  2876 by (simp add: Sup_fin_def inf_absorb1
  2877   semilattice_inf.fold1_belowI [OF dual_semilattice])
  2878 
  2879 end
  2880 
  2881 context distrib_lattice
  2882 begin
  2883 
  2884 lemma sup_Inf1_distrib:
  2885   assumes "finite A"
  2886     and "A \<noteq> {}"
  2887   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  2888 proof -
  2889   interpret ab_semigroup_idem_mult inf
  2890     by (rule ab_semigroup_idem_mult_inf)
  2891   from assms show ?thesis
  2892     by (simp add: Inf_fin_def image_def
  2893       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  2894         (rule arg_cong [where f="fold1 inf"], blast)
  2895 qed
  2896 
  2897 lemma sup_Inf2_distrib:
  2898   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2899   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}"
  2900 using A proof (induct rule: finite_ne_induct)
  2901   case singleton thus ?case
  2902     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
  2903 next
  2904   interpret ab_semigroup_idem_mult inf
  2905     by (rule ab_semigroup_idem_mult_inf)
  2906   case (insert x A)
  2907   have finB: "finite {sup x b |b. b \<in> B}"
  2908     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  2909   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  2910   proof -
  2911     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  2912       by blast
  2913     thus ?thesis by(simp add: insert(1) B(1))
  2914   qed
  2915   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2916   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)"
  2917     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
  2918   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)
  2919   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})"
  2920     using insert by(simp add:sup_Inf1_distrib[OF B])
  2921   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})"
  2922     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  2923     using B insert
  2924     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  2925   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2926     by blast
  2927   finally show ?case .
  2928 qed
  2929 
  2930 lemma inf_Sup1_distrib:
  2931   assumes "finite A" and "A \<noteq> {}"
  2932   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  2933 proof -
  2934   interpret ab_semigroup_idem_mult sup
  2935     by (rule ab_semigroup_idem_mult_sup)
  2936   from assms show ?thesis
  2937     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  2938       (rule arg_cong [where f="fold1 sup"], blast)
  2939 qed
  2940 
  2941 lemma inf_Sup2_distrib:
  2942   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2943   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}"
  2944 using A proof (induct rule: finite_ne_induct)
  2945   case singleton thus ?case
  2946     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
  2947 next
  2948   case (insert x A)
  2949   have finB: "finite {inf x b |b. b \<in> B}"
  2950     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  2951   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  2952   proof -
  2953     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  2954       by blast
  2955     thus ?thesis by(simp add: insert(1) B(1))
  2956   qed
  2957   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2958   interpret ab_semigroup_idem_mult sup
  2959     by (rule ab_semigroup_idem_mult_sup)
  2960   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)"
  2961     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
  2962   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)
  2963   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})"
  2964     using insert by(simp add:inf_Sup1_distrib[OF B])
  2965   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})"
  2966     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  2967     using B insert
  2968     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  2969   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2970     by blast
  2971   finally show ?case .
  2972 qed
  2973 
  2974 end
  2975 
  2976 
  2977 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
  2978 
  2979 text{*
  2980   As an application of @{text fold1} we define minimum
  2981   and maximum in (not necessarily complete!) linear orders
  2982   over (non-empty) sets by means of @{text fold1}.
  2983 *}
  2984 
  2985 context linorder
  2986 begin
  2987 
  2988 lemma ab_semigroup_idem_mult_min:
  2989   "ab_semigroup_idem_mult min"
  2990   proof qed (auto simp add: min_def)
  2991 
  2992 lemma ab_semigroup_idem_mult_max:
  2993   "ab_semigroup_idem_mult max"
  2994   proof qed (auto simp add: max_def)
  2995 
  2996 lemma max_lattice:
  2997   "semilattice_inf (op \<ge>) (op >) max"
  2998   by (fact min_max.dual_semilattice)
  2999 
  3000 lemma dual_max:
  3001   "ord.max (op \<ge>) = min"
  3002   by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
  3003 
  3004 lemma dual_min:
  3005   "ord.min (op \<ge>) = max"
  3006   by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
  3007 
  3008 lemma strict_below_fold1_iff:
  3009   assumes "finite A" and "A \<noteq> {}"
  3010   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  3011 proof -
  3012   interpret ab_semigroup_idem_mult min
  3013     by (rule ab_semigroup_idem_mult_min)
  3014   from assms show ?thesis
  3015   by (induct rule: finite_ne_induct)
  3016     (simp_all add: fold1_insert)
  3017 qed
  3018 
  3019 lemma fold1_below_iff:
  3020   assumes "finite A" and "A \<noteq> {}"
  3021   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  3022 proof -
  3023   interpret ab_semigroup_idem_mult min
  3024     by (rule ab_semigroup_idem_mult_min)
  3025   from assms show ?thesis
  3026   by (induct rule: finite_ne_induct)
  3027     (simp_all add: fold1_insert min_le_iff_disj)
  3028 qed
  3029 
  3030 lemma fold1_strict_below_iff:
  3031   assumes "finite A" and "A \<noteq> {}"
  3032   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  3033 proof -
  3034   interpret ab_semigroup_idem_mult min
  3035     by (rule ab_semigroup_idem_mult_min)
  3036   from assms show ?thesis
  3037   by (induct rule: finite_ne_induct)
  3038     (simp_all add: fold1_insert min_less_iff_disj)
  3039 qed
  3040 
  3041 lemma fold1_antimono:
  3042   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  3043   shows "fold1 min B \<le> fold1 min A"
  3044 proof cases
  3045   assume "A = B" thus ?thesis by simp
  3046 next
  3047   interpret ab_semigroup_idem_mult min
  3048     by (rule ab_semigroup_idem_mult_min)
  3049   assume "A \<noteq> B"
  3050   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  3051   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  3052   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  3053   proof -
  3054     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  3055     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  3056     moreover have "(B-A) \<noteq> {}" using prems by blast
  3057     moreover have "A Int (B-A) = {}" using prems by blast
  3058     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  3059   qed
  3060   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  3061   finally show ?thesis .
  3062 qed
  3063 
  3064 definition
  3065   Min :: "'a set \<Rightarrow> 'a"
  3066 where
  3067   "Min = fold1 min"
  3068 
  3069 definition
  3070   Max :: "'a set \<Rightarrow> 'a"
  3071 where
  3072   "Max = fold1 max"
  3073 
  3074 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
  3075 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
  3076 
  3077 lemma Min_insert [simp]:
  3078   assumes "finite A" and "A \<noteq> {}"
  3079   shows "Min (insert x A) = min x (Min A)"
  3080 proof -
  3081   interpret ab_semigroup_idem_mult min
  3082     by (rule ab_semigroup_idem_mult_min)
  3083   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
  3084 qed
  3085 
  3086 lemma Max_insert [simp]:
  3087   assumes "finite A" and "A \<noteq> {}"
  3088   shows "Max (insert x A) = max x (Max A)"
  3089 proof -
  3090   interpret ab_semigroup_idem_mult max
  3091     by (rule ab_semigroup_idem_mult_max)
  3092   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
  3093 qed
  3094 
  3095 lemma Min_in [simp]:
  3096   assumes "finite A" and "A \<noteq> {}"
  3097   shows "Min A \<in> A"
  3098 proof -
  3099   interpret ab_semigroup_idem_mult min
  3100     by (rule ab_semigroup_idem_mult_min)
  3101   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
  3102 qed
  3103 
  3104 lemma Max_in [simp]:
  3105   assumes "finite A" and "A \<noteq> {}"
  3106   shows "Max A \<in> A"
  3107 proof -
  3108   interpret ab_semigroup_idem_mult max
  3109     by (rule ab_semigroup_idem_mult_max)
  3110   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
  3111 qed
  3112 
  3113 lemma Min_Un:
  3114   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  3115   shows "Min (A \<union> B) = min (Min A) (Min B)"
  3116 proof -
  3117   interpret ab_semigroup_idem_mult min
  3118     by (rule ab_semigroup_idem_mult_min)
  3119   from assms show ?thesis
  3120     by (simp add: Min_def fold1_Un2)
  3121 qed
  3122 
  3123 lemma Max_Un:
  3124   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  3125   shows "Max (A \<union> B) = max (Max A) (Max B)"
  3126 proof -
  3127   interpret ab_semigroup_idem_mult max
  3128     by (rule ab_semigroup_idem_mult_max)
  3129   from assms show ?thesis
  3130     by (simp add: Max_def fold1_Un2)
  3131 qed
  3132 
  3133 lemma hom_Min_commute:
  3134   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  3135     and "finite N" and "N \<noteq> {}"
  3136   shows "h (Min N) = Min (h ` N)"
  3137 proof -
  3138   interpret ab_semigroup_idem_mult min
  3139     by (rule ab_semigroup_idem_mult_min)
  3140   from assms show ?thesis
  3141     by (simp add: Min_def hom_fold1_commute)
  3142 qed
  3143 
  3144 lemma hom_Max_commute:
  3145   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  3146     and "finite N" and "N \<noteq> {}"
  3147   shows "h (Max N) = Max (h ` N)"
  3148 proof -
  3149   interpret ab_semigroup_idem_mult max
  3150     by (rule ab_semigroup_idem_mult_max)
  3151   from assms show ?thesis
  3152     by (simp add: Max_def hom_fold1_commute [of h])
  3153 qed
  3154 
  3155 lemma Min_le [simp]:
  3156   assumes "finite A" and "x \<in> A"
  3157   shows "Min A \<le> x"
  3158   using assms by (simp add: Min_def min_max.fold1_belowI)
  3159 
  3160 lemma Max_ge [simp]:
  3161   assumes "finite A" and "x \<in> A"
  3162   shows "x \<le> Max A"
  3163 proof -
  3164   interpret semilattice_inf "op \<ge>" "op >" max
  3165     by (rule max_lattice)
  3166   from assms show ?thesis by (simp add: Max_def fold1_belowI)
  3167 qed
  3168 
  3169 lemma Min_ge_iff [simp, noatp]:
  3170   assumes "finite A" and "A \<noteq> {}"
  3171   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  3172   using assms by (simp add: Min_def min_max.below_fold1_iff)
  3173 
  3174 lemma Max_le_iff [simp, noatp]:
  3175   assumes "finite A" and "A \<noteq> {}"
  3176   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  3177 proof -
  3178   interpret semilattice_inf "op \<ge>" "op >" max
  3179     by (rule max_lattice)
  3180   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
  3181 qed
  3182 
  3183 lemma Min_gr_iff [simp, noatp]:
  3184   assumes "finite A" and "A \<noteq> {}"
  3185   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  3186   using assms by (simp add: Min_def strict_below_fold1_iff)
  3187 
  3188 lemma Max_less_iff [simp, noatp]:
  3189   assumes "finite A" and "A \<noteq> {}"
  3190   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  3191 proof -
  3192   interpret dual: linorder "op \<ge>" "op >"
  3193     by (rule dual_linorder)
  3194   from assms show ?thesis
  3195     by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
  3196 qed
  3197 
  3198 lemma Min_le_iff [noatp]:
  3199   assumes "finite A" and "A \<noteq> {}"
  3200   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  3201   using assms by (simp add: Min_def fold1_below_iff)
  3202 
  3203 lemma Max_ge_iff [noatp]:
  3204   assumes "finite A" and "A \<noteq> {}"
  3205   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  3206 proof -
  3207   interpret dual: linorder "op \<ge>" "op >"
  3208     by (rule dual_linorder)
  3209   from assms show ?thesis
  3210     by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
  3211 qed
  3212 
  3213 lemma Min_less_iff [noatp]:
  3214   assumes "finite A" and "A \<noteq> {}"
  3215   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  3216   using assms by (simp add: Min_def fold1_strict_below_iff)
  3217 
  3218 lemma Max_gr_iff [noatp]:
  3219   assumes "finite A" and "A \<noteq> {}"
  3220   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  3221 proof -
  3222   interpret dual: linorder "op \<ge>" "op >"
  3223     by (rule dual_linorder)
  3224   from assms show ?thesis
  3225     by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
  3226 qed
  3227 
  3228 lemma Min_eqI:
  3229   assumes "finite A"
  3230   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  3231     and "x \<in> A"
  3232   shows "Min A = x"
  3233 proof (rule antisym)
  3234   from `x \<in> A` have "A \<noteq> {}" by auto
  3235   with assms show "Min A \<ge> x" by simp
  3236 next
  3237   from assms show "x \<ge> Min A" by simp
  3238 qed
  3239 
  3240 lemma Max_eqI:
  3241   assumes "finite A"
  3242   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  3243     and "x \<in> A"
  3244   shows "Max A = x"
  3245 proof (rule antisym)
  3246   from `x \<in> A` have "A \<noteq> {}" by auto
  3247   with assms show "Max A \<le> x" by simp
  3248 next
  3249   from assms show "x \<le> Max A" by simp
  3250 qed
  3251 
  3252 lemma Min_antimono:
  3253   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  3254   shows "Min N \<le> Min M"
  3255   using assms by (simp add: Min_def fold1_antimono)
  3256 
  3257 lemma Max_mono:
  3258   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  3259   shows "Max M \<le> Max N"
  3260 proof -
  3261   interpret dual: linorder "op \<ge>" "op >"
  3262     by (rule dual_linorder)
  3263   from assms show ?thesis
  3264     by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
  3265 qed
  3266 
  3267 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
  3268  "finite A \<Longrightarrow> P {} \<Longrightarrow>
  3269   (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
  3270   \<Longrightarrow> P A"
  3271 proof (induct rule: finite_psubset_induct)
  3272   fix A :: "'a set"
  3273   assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
  3274                  (!!b A. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
  3275                   \<Longrightarrow> P B"
  3276   and "finite A" and "P {}"
  3277   and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
  3278   show "P A"
  3279   proof (cases "A = {}")
  3280     assume "A = {}" thus "P A" using `P {}` by simp
  3281   next
  3282     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
  3283     assume "A \<noteq> {}"
  3284     with `finite A` have "Max A : A" by auto
  3285     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
  3286     moreover have "finite ?B" using `finite A` by simp
  3287     ultimately have "P ?B" using `P {}` step IH[of ?B] by blast
  3288     moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
  3289     ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
  3290   qed
  3291 qed
  3292 
  3293 lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
  3294  "\<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"
  3295 by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
  3296 
  3297 end
  3298 
  3299 context linordered_ab_semigroup_add
  3300 begin
  3301 
  3302 lemma add_Min_commute:
  3303   fixes k
  3304   assumes "finite N" and "N \<noteq> {}"
  3305   shows "k + Min N = Min {k + m | m. m \<in> N}"
  3306 proof -
  3307   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  3308     by (simp add: min_def not_le)
  3309       (blast intro: antisym less_imp_le add_left_mono)
  3310   with assms show ?thesis
  3311     using hom_Min_commute [of "plus k" N]
  3312     by simp (blast intro: arg_cong [where f = Min])
  3313 qed
  3314 
  3315 lemma add_Max_commute:
  3316   fixes k
  3317   assumes "finite N" and "N \<noteq> {}"
  3318   shows "k + Max N = Max {k + m | m. m \<in> N}"
  3319 proof -
  3320   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  3321     by (simp add: max_def not_le)
  3322       (blast intro: antisym less_imp_le add_left_mono)
  3323   with assms show ?thesis
  3324     using hom_Max_commute [of "plus k" N]
  3325     by simp (blast intro: arg_cong [where f = Max])
  3326 qed
  3327 
  3328 end
  3329 
  3330 context linordered_ab_group_add
  3331 begin
  3332 
  3333 lemma minus_Max_eq_Min [simp]:
  3334   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
  3335   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  3336 
  3337 lemma minus_Min_eq_Max [simp]:
  3338   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
  3339   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  3340 
  3341 end
  3342 
  3343 
  3344 subsection {* Expressing set operations via @{const fold} *}
  3345 
  3346 lemma (in fun_left_comm) fun_left_comm_apply:
  3347   "fun_left_comm (\<lambda>x. f (g x))"
  3348 proof
  3349 qed (simp_all add: fun_left_comm)
  3350 
  3351 lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
  3352   "fun_left_comm_idem (\<lambda>x. f (g x))"
  3353   by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
  3354     (simp_all add: fun_left_idem)
  3355 
  3356 lemma fun_left_comm_idem_insert:
  3357   "fun_left_comm_idem insert"
  3358 proof
  3359 qed auto
  3360 
  3361 lemma fun_left_comm_idem_remove:
  3362   "fun_left_comm_idem (\<lambda>x A. A - {x})"
  3363 proof
  3364 qed auto
  3365 
  3366 lemma (in semilattice_inf) fun_left_comm_idem_inf:
  3367   "fun_left_comm_idem inf"
  3368 proof
  3369 qed (auto simp add: inf_left_commute)
  3370 
  3371 lemma (in semilattice_sup) fun_left_comm_idem_sup:
  3372   "fun_left_comm_idem sup"
  3373 proof
  3374 qed (auto simp add: sup_left_commute)
  3375 
  3376 lemma union_fold_insert:
  3377   assumes "finite A"
  3378   shows "A \<union> B = fold insert B A"
  3379 proof -
  3380   interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
  3381   from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
  3382 qed
  3383 
  3384 lemma minus_fold_remove:
  3385   assumes "finite A"
  3386   shows "B - A = fold (\<lambda>x A. A - {x}) B A"
  3387 proof -
  3388   interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
  3389   from `finite A` show ?thesis by (induct A arbitrary: B) auto
  3390 qed
  3391 
  3392 context complete_lattice
  3393 begin
  3394 
  3395 lemma inf_Inf_fold_inf:
  3396   assumes "finite A"
  3397   shows "inf B (Inf A) = fold inf B A"
  3398 proof -
  3399   interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
  3400   from `finite A` show ?thesis by (induct A arbitrary: B)
  3401     (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
  3402 qed
  3403 
  3404 lemma sup_Sup_fold_sup:
  3405   assumes "finite A"
  3406   shows "sup B (Sup A) = fold sup B A"
  3407 proof -
  3408   interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
  3409   from `finite A` show ?thesis by (induct A arbitrary: B)
  3410     (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
  3411 qed
  3412 
  3413 lemma Inf_fold_inf:
  3414   assumes "finite A"
  3415   shows "Inf A = fold inf top A"
  3416   using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
  3417 
  3418 lemma Sup_fold_sup:
  3419   assumes "finite A"
  3420   shows "Sup A = fold sup bot A"
  3421   using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
  3422 
  3423 lemma Inf_fin_Inf:
  3424   assumes "finite A" and "A \<noteq> {}"
  3425   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  3426 proof -
  3427   interpret ab_semigroup_idem_mult inf
  3428     by (rule ab_semigroup_idem_mult_inf)
  3429   from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
  3430   moreover with `finite A` have "finite B" by simp
  3431   ultimately show ?thesis  
  3432   by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
  3433     (simp add: Inf_fold_inf)
  3434 qed
  3435 
  3436 lemma Sup_fin_Sup:
  3437   assumes "finite A" and "A \<noteq> {}"
  3438   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  3439 proof -
  3440   interpret ab_semigroup_idem_mult sup
  3441     by (rule ab_semigroup_idem_mult_sup)
  3442   from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
  3443   moreover with `finite A` have "finite B" by simp
  3444   ultimately show ?thesis  
  3445   by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
  3446     (simp add: Sup_fold_sup)
  3447 qed
  3448 
  3449 lemma inf_INFI_fold_inf:
  3450   assumes "finite A"
  3451   shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
  3452 proof (rule sym)
  3453   interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
  3454   interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
  3455   from `finite A` show "?fold = ?inf"
  3456   by (induct A arbitrary: B)
  3457     (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
  3458 qed
  3459 
  3460 lemma sup_SUPR_fold_sup:
  3461   assumes "finite A"
  3462   shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
  3463 proof (rule sym)
  3464   interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
  3465   interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
  3466   from `finite A` show "?fold = ?sup"
  3467   by (induct A arbitrary: B)
  3468     (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
  3469 qed
  3470 
  3471 lemma INFI_fold_inf:
  3472   assumes "finite A"
  3473   shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
  3474   using assms inf_INFI_fold_inf [of A top] by simp
  3475 
  3476 lemma SUPR_fold_sup:
  3477   assumes "finite A"
  3478   shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
  3479   using assms sup_SUPR_fold_sup [of A bot] by simp
  3480 
  3481 end
  3482 
  3483 end