src/HOL/Finite_Set.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27981 feb0c01cf0fb
child 28823 dcbef866c9e2
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (*  Title:      HOL/Finite_Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     4                 with contributions by Jeremy Avigad
     5 *)
     6 
     7 header {* Finite sets *}
     8 
     9 theory Finite_Set
    10 imports Datatype Divides Transitive_Closure
    11 begin
    12 
    13 subsection {* Definition and basic properties *}
    14 
    15 inductive finite :: "'a set => bool"
    16   where
    17     emptyI [simp, intro!]: "finite {}"
    18   | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
    19 
    20 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    21   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    22   shows "\<exists>a::'a. a \<notin> A"
    23 proof -
    24   from prems have "A \<noteq> UNIV" by blast
    25   thus ?thesis by blast
    26 qed
    27 
    28 lemma finite_induct [case_names empty insert, induct set: finite]:
    29   "finite F ==>
    30     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    31   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    32 proof -
    33   assume "P {}" and
    34     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    35   assume "finite F"
    36   thus "P F"
    37   proof induct
    38     show "P {}" by fact
    39     fix x F assume F: "finite F" and P: "P F"
    40     show "P (insert x F)"
    41     proof cases
    42       assume "x \<in> F"
    43       hence "insert x F = F" by (rule insert_absorb)
    44       with P show ?thesis by (simp only:)
    45     next
    46       assume "x \<notin> F"
    47       from F this P show ?thesis by (rule insert)
    48     qed
    49   qed
    50 qed
    51 
    52 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
    53 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
    54  \<lbrakk> \<And>x. P{x};
    55    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
    56  \<Longrightarrow> P F"
    57 using fin
    58 proof induct
    59   case empty thus ?case by simp
    60 next
    61   case (insert x F)
    62   show ?case
    63   proof cases
    64     assume "F = {}"
    65     thus ?thesis using `P {x}` by simp
    66   next
    67     assume "F \<noteq> {}"
    68     thus ?thesis using insert by blast
    69   qed
    70 qed
    71 
    72 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    73   assumes "finite F" and "F \<subseteq> A"
    74     and empty: "P {}"
    75     and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    76   shows "P F"
    77 proof -
    78   from `finite F` and `F \<subseteq> A`
    79   show ?thesis
    80   proof induct
    81     show "P {}" by fact
    82   next
    83     fix x F
    84     assume "finite F" and "x \<notin> F" and
    85       P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    86     show "P (insert x F)"
    87     proof (rule insert)
    88       from i show "x \<in> A" by blast
    89       from i have "F \<subseteq> A" by blast
    90       with P show "P F" .
    91       show "finite F" by fact
    92       show "x \<notin> F" by fact
    93     qed
    94   qed
    95 qed
    96 
    97 
    98 text{* Finite sets are the images of initial segments of natural numbers: *}
    99 
   100 lemma finite_imp_nat_seg_image_inj_on:
   101   assumes fin: "finite A" 
   102   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
   103 using fin
   104 proof induct
   105   case empty
   106   show ?case  
   107   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 
   108   qed
   109 next
   110   case (insert a A)
   111   have notinA: "a \<notin> A" by fact
   112   from insert.hyps obtain n f
   113     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
   114   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
   115         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
   116     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
   117   thus ?case by blast
   118 qed
   119 
   120 lemma nat_seg_image_imp_finite:
   121   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
   122 proof (induct n)
   123   case 0 thus ?case by simp
   124 next
   125   case (Suc n)
   126   let ?B = "f ` {i. i < n}"
   127   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
   128   show ?case
   129   proof cases
   130     assume "\<exists>k<n. f n = f k"
   131     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
   132     thus ?thesis using finB by simp
   133   next
   134     assume "\<not>(\<exists> k<n. f n = f k)"
   135     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
   136     thus ?thesis using finB by simp
   137   qed
   138 qed
   139 
   140 lemma finite_conv_nat_seg_image:
   141   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
   142 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
   143 
   144 
   145 subsubsection{* Finiteness and set theoretic constructions *}
   146 
   147 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
   148   -- {* The union of two finite sets is finite. *}
   149   by (induct set: finite) simp_all
   150 
   151 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
   152   -- {* Every subset of a finite set is finite. *}
   153 proof -
   154   assume "finite B"
   155   thus "!!A. A \<subseteq> B ==> finite A"
   156   proof induct
   157     case empty
   158     thus ?case by simp
   159   next
   160     case (insert x F A)
   161     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
   162     show "finite A"
   163     proof cases
   164       assume x: "x \<in> A"
   165       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
   166       with r have "finite (A - {x})" .
   167       hence "finite (insert x (A - {x}))" ..
   168       also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
   169       finally show ?thesis .
   170     next
   171       show "A \<subseteq> F ==> ?thesis" by fact
   172       assume "x \<notin> A"
   173       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   174     qed
   175   qed
   176 qed
   177 
   178 lemma finite_Collect_subset[simp]: "finite A \<Longrightarrow> finite{x \<in> A. P x}"
   179 using finite_subset[of "{x \<in> A. P x}" "A"] by blast
   180 
   181 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   182   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   183 
   184 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   185   -- {* The converse obviously fails. *}
   186   by (blast intro: finite_subset)
   187 
   188 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   189   apply (subst insert_is_Un)
   190   apply (simp only: finite_Un, blast)
   191   done
   192 
   193 lemma finite_Union[simp, intro]:
   194  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
   195 by (induct rule:finite_induct) simp_all
   196 
   197 lemma finite_empty_induct:
   198   assumes "finite A"
   199     and "P A"
   200     and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   201   shows "P {}"
   202 proof -
   203   have "P (A - A)"
   204   proof -
   205     {
   206       fix c b :: "'a set"
   207       assume c: "finite c" and b: "finite b"
   208 	and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   209       have "c \<subseteq> b ==> P (b - c)"
   210 	using c
   211       proof induct
   212 	case empty
   213 	from P1 show ?case by simp
   214       next
   215 	case (insert x F)
   216 	have "P (b - F - {x})"
   217 	proof (rule P2)
   218           from _ b show "finite (b - F)" by (rule finite_subset) blast
   219           from insert show "x \<in> b - F" by simp
   220           from insert show "P (b - F)" by simp
   221 	qed
   222 	also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   223 	finally show ?case .
   224       qed
   225     }
   226     then show ?thesis by this (simp_all add: assms)
   227   qed
   228   then show ?thesis by simp
   229 qed
   230 
   231 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   232   by (rule Diff_subset [THEN finite_subset])
   233 
   234 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   235   apply (subst Diff_insert)
   236   apply (case_tac "a : A - B")
   237    apply (rule finite_insert [symmetric, THEN trans])
   238    apply (subst insert_Diff, simp_all)
   239   done
   240 
   241 lemma finite_Diff_singleton [simp]: "finite (A - {a}) = finite A"
   242   by simp
   243 
   244 
   245 text {* Image and Inverse Image over Finite Sets *}
   246 
   247 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   248   -- {* The image of a finite set is finite. *}
   249   by (induct set: finite) simp_all
   250 
   251 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   252   apply (frule finite_imageI)
   253   apply (erule finite_subset, assumption)
   254   done
   255 
   256 lemma finite_range_imageI:
   257     "finite (range g) ==> finite (range (%x. f (g x)))"
   258   apply (drule finite_imageI, simp add: range_composition)
   259   done
   260 
   261 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   262 proof -
   263   have aux: "!!A. finite (A - {}) = finite A" by simp
   264   fix B :: "'a set"
   265   assume "finite B"
   266   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   267     apply induct
   268      apply simp
   269     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   270      apply clarify
   271      apply (simp (no_asm_use) add: inj_on_def)
   272      apply (blast dest!: aux [THEN iffD1], atomize)
   273     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   274     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   275     apply (rule_tac x = xa in bexI)
   276      apply (simp_all add: inj_on_image_set_diff)
   277     done
   278 qed (rule refl)
   279 
   280 
   281 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   282   -- {* The inverse image of a singleton under an injective function
   283          is included in a singleton. *}
   284   apply (auto simp add: inj_on_def)
   285   apply (blast intro: the_equality [symmetric])
   286   done
   287 
   288 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   289   -- {* The inverse image of a finite set under an injective function
   290          is finite. *}
   291   apply (induct set: finite)
   292    apply simp_all
   293   apply (subst vimage_insert)
   294   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   295   done
   296 
   297 
   298 text {* The finite UNION of finite sets *}
   299 
   300 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   301   by (induct set: finite) simp_all
   302 
   303 text {*
   304   Strengthen RHS to
   305   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   306 
   307   We'd need to prove
   308   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   309   by induction. *}
   310 
   311 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   312   by (blast intro: finite_UN_I finite_subset)
   313 
   314 
   315 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
   316 by (simp add: Plus_def)
   317 
   318 text {* Sigma of finite sets *}
   319 
   320 lemma finite_SigmaI [simp]:
   321     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   322   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   323 
   324 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   325     finite (A <*> B)"
   326   by (rule finite_SigmaI)
   327 
   328 lemma finite_Prod_UNIV:
   329     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   330   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   331    apply (erule ssubst)
   332    apply (erule finite_SigmaI, auto)
   333   done
   334 
   335 lemma finite_cartesian_productD1:
   336      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
   337 apply (auto simp add: finite_conv_nat_seg_image) 
   338 apply (drule_tac x=n in spec) 
   339 apply (drule_tac x="fst o f" in spec) 
   340 apply (auto simp add: o_def) 
   341  prefer 2 apply (force dest!: equalityD2) 
   342 apply (drule equalityD1) 
   343 apply (rename_tac y x)
   344 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   345  prefer 2 apply force
   346 apply clarify
   347 apply (rule_tac x=k in image_eqI, auto)
   348 done
   349 
   350 lemma finite_cartesian_productD2:
   351      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
   352 apply (auto simp add: finite_conv_nat_seg_image) 
   353 apply (drule_tac x=n in spec) 
   354 apply (drule_tac x="snd o f" in spec) 
   355 apply (auto simp add: o_def) 
   356  prefer 2 apply (force dest!: equalityD2) 
   357 apply (drule equalityD1)
   358 apply (rename_tac x y)
   359 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   360  prefer 2 apply force
   361 apply clarify
   362 apply (rule_tac x=k in image_eqI, auto)
   363 done
   364 
   365 
   366 text {* The powerset of a finite set *}
   367 
   368 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   369 proof
   370   assume "finite (Pow A)"
   371   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   372   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   373 next
   374   assume "finite A"
   375   thus "finite (Pow A)"
   376     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   377 qed
   378 
   379 
   380 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   381 by(blast intro: finite_subset[OF subset_Pow_Union])
   382 
   383 
   384 lemma finite_converse [iff]: "finite (r^-1) = finite r"
   385   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   386    apply simp
   387    apply (rule iffI)
   388     apply (erule finite_imageD [unfolded inj_on_def])
   389     apply (simp split add: split_split)
   390    apply (erule finite_imageI)
   391   apply (simp add: converse_def image_def, auto)
   392   apply (rule bexI)
   393    prefer 2 apply assumption
   394   apply simp
   395   done
   396 
   397 
   398 text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
   399 Ehmety) *}
   400 
   401 lemma finite_Field: "finite r ==> finite (Field r)"
   402   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   403   apply (induct set: finite)
   404    apply (auto simp add: Field_def Domain_insert Range_insert)
   405   done
   406 
   407 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   408   apply clarify
   409   apply (erule trancl_induct)
   410    apply (auto simp add: Field_def)
   411   done
   412 
   413 lemma finite_trancl: "finite (r^+) = finite r"
   414   apply auto
   415    prefer 2
   416    apply (rule trancl_subset_Field2 [THEN finite_subset])
   417    apply (rule finite_SigmaI)
   418     prefer 3
   419     apply (blast intro: r_into_trancl' finite_subset)
   420    apply (auto simp add: finite_Field)
   421   done
   422 
   423 
   424 subsection {* Class @{text finite}  *}
   425 
   426 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
   427 class finite = itself +
   428   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
   429 setup {* Sign.parent_path *}
   430 hide const finite
   431 
   432 context finite
   433 begin
   434 
   435 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   436   by (rule subset_UNIV finite_UNIV finite_subset)+
   437 
   438 end
   439 
   440 lemma UNIV_unit [noatp]:
   441   "UNIV = {()}" by auto
   442 
   443 instance unit :: finite
   444   by default (simp add: UNIV_unit)
   445 
   446 lemma UNIV_bool [noatp]:
   447   "UNIV = {False, True}" by auto
   448 
   449 instance bool :: finite
   450   by default (simp add: UNIV_bool)
   451 
   452 instance * :: (finite, finite) finite
   453   by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
   454 
   455 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   456   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   457 
   458 instance "fun" :: (finite, finite) finite
   459 proof
   460   show "finite (UNIV :: ('a => 'b) set)"
   461   proof (rule finite_imageD)
   462     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
   463     have "range ?graph \<subseteq> Pow UNIV" by simp
   464     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
   465       by (simp only: finite_Pow_iff finite)
   466     ultimately show "finite (range ?graph)"
   467       by (rule finite_subset)
   468     show "inj ?graph" by (rule inj_graph)
   469   qed
   470 qed
   471 
   472 instance "+" :: (finite, finite) finite
   473   by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
   474 
   475 instance option :: (finite) finite
   476   by default (simp add: insert_None_conv_UNIV [symmetric])
   477 
   478 
   479 subsection {* A fold functional for finite sets *}
   480 
   481 text {* The intended behaviour is
   482 @{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"}
   483 if @{text f} is associative-commutative. For an application of @{text fold}
   484 se the definitions of sums and products over finite sets.
   485 *}
   486 
   487 inductive
   488   foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool"
   489   for f ::  "'a => 'a => 'a"
   490   and g :: "'b => 'a"
   491   and z :: 'a
   492 where
   493   emptyI [intro]: "foldSet f g z {} z"
   494 | insertI [intro]:
   495      "\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk>
   496       \<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)"
   497 
   498 inductive_cases empty_foldSetE [elim!]: "foldSet f g z {} x"
   499 
   500 constdefs
   501   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
   502   "fold f g z A == THE x. foldSet f g z A x"
   503 
   504 text{*A tempting alternative for the definiens is
   505 @{term "if finite A then THE x. foldSet f g e A x else e"}.
   506 It allows the removal of finiteness assumptions from the theorems
   507 @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}.
   508 The proofs become ugly, with @{text rule_format}. It is not worth the effort.*}
   509 
   510 
   511 lemma Diff1_foldSet:
   512   "foldSet f g z (A - {x}) y ==> x: A ==> foldSet f g z A (f (g x) y)"
   513 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   514 
   515 lemma foldSet_imp_finite: "foldSet f g z A x==> finite A"
   516   by (induct set: foldSet) auto
   517 
   518 lemma finite_imp_foldSet: "finite A ==> EX x. foldSet f g z A x"
   519   by (induct set: finite) auto
   520 
   521 
   522 subsubsection{*From @{term foldSet} to @{term fold}*}
   523 
   524 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
   525   by (auto simp add: less_Suc_eq) 
   526 
   527 lemma insert_image_inj_on_eq:
   528      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
   529         inj_on h {i. i < Suc m}|] 
   530       ==> A = h ` {i. i < m}"
   531 apply (auto simp add: image_less_Suc inj_on_def)
   532 apply (blast intro: less_trans) 
   533 done
   534 
   535 lemma insert_inj_onE:
   536   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 
   537       and inj_on: "inj_on h {i::nat. i<n}"
   538   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
   539 proof (cases n)
   540   case 0 thus ?thesis using aA by auto
   541 next
   542   case (Suc m)
   543   have nSuc: "n = Suc m" by fact
   544   have mlessn: "m<n" by (simp add: nSuc)
   545   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   546   let ?hm = "Fun.swap k m h"
   547   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
   548     by (simp add: inj_on_swap_iff inj_on)
   549   show ?thesis
   550   proof (intro exI conjI)
   551     show "inj_on ?hm {i. i < m}" using inj_hm
   552       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
   553     show "m<n" by (rule mlessn)
   554     show "A = ?hm ` {i. i < m}" 
   555     proof (rule insert_image_inj_on_eq)
   556       show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
   557       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
   558       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
   559 	using aA hkeq nSuc klessn
   560 	by (auto simp add: swap_def image_less_Suc fun_upd_image 
   561 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
   562     qed
   563   qed
   564 qed
   565 
   566 context ab_semigroup_mult
   567 begin
   568 
   569 lemma foldSet_determ_aux:
   570   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
   571                 foldSet times g z A x; foldSet times g z A x' \<rbrakk>
   572    \<Longrightarrow> x' = x"
   573 proof (induct n rule: less_induct)
   574   case (less n)
   575     have IH: "!!m h A x x'. 
   576                \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   577                 foldSet times g z A x; foldSet times g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
   578     have Afoldx: "foldSet times g z A x" and Afoldx': "foldSet times g z A x'"
   579      and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
   580     show ?case
   581     proof (rule foldSet.cases [OF Afoldx])
   582       assume "A = {}" and "x = z"
   583       with Afoldx' show "x' = x" by blast
   584     next
   585       fix B b u
   586       assume AbB: "A = insert b B" and x: "x = g b * u"
   587          and notinB: "b \<notin> B" and Bu: "foldSet times g z B u"
   588       show "x'=x" 
   589       proof (rule foldSet.cases [OF Afoldx'])
   590         assume "A = {}" and "x' = z"
   591         with AbB show "x' = x" by blast
   592       next
   593 	fix C c v
   594 	assume AcC: "A = insert c C" and x': "x' = g c * v"
   595            and notinC: "c \<notin> C" and Cv: "foldSet times g z C v"
   596 	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   597         from insert_inj_onE [OF Beq notinB injh]
   598         obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   599                      and Beq: "B = hB ` {i. i < mB}"
   600                      and lessB: "mB < n" by auto 
   601 	from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
   602         from insert_inj_onE [OF Ceq notinC injh]
   603         obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
   604                        and Ceq: "C = hC ` {i. i < mC}"
   605                        and lessC: "mC < n" by auto 
   606 	show "x'=x"
   607 	proof cases
   608           assume "b=c"
   609 	  then moreover have "B = C" using AbB AcC notinB notinC by auto
   610 	  ultimately show ?thesis  using Bu Cv x x' IH[OF lessC Ceq inj_onC]
   611             by auto
   612 	next
   613 	  assume diff: "b \<noteq> c"
   614 	  let ?D = "B - {c}"
   615 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   616 	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   617 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   618 	  with AbB have "finite ?D" by simp
   619 	  then obtain d where Dfoldd: "foldSet times g z ?D d"
   620 	    using finite_imp_foldSet by iprover
   621 	  moreover have cinB: "c \<in> B" using B by auto
   622 	  ultimately have "foldSet times g z B (g c * d)"
   623 	    by(rule Diff1_foldSet)
   624 	  then have "g c * d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   625           then have "u = g c * d" ..
   626           moreover have "v = g b * d"
   627 	  proof (rule sym, rule IH [OF lessC Ceq inj_onC Cv])
   628 	    show "foldSet times g z C (g b * d)" using C notinB Dfoldd
   629 	      by fastsimp
   630 	  qed
   631 	  ultimately show ?thesis using x x'
   632 	    by (simp add: mult_left_commute)
   633 	qed
   634       qed
   635     qed
   636   qed
   637 
   638 lemma foldSet_determ:
   639   "foldSet times g z A x ==> foldSet times g z A y ==> y = x"
   640 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   641 apply (blast intro: foldSet_determ_aux [rule_format])
   642 done
   643 
   644 lemma fold_equality: "foldSet times g z A y ==> fold times g z A = y"
   645   by (unfold fold_def) (blast intro: foldSet_determ)
   646 
   647 text{* The base case for @{text fold}: *}
   648 
   649 lemma (in -) fold_empty [simp]: "fold f g z {} = z"
   650   by (unfold fold_def) blast
   651 
   652 lemma fold_insert_aux: "x \<notin> A ==>
   653     (foldSet times g z (insert x A) v) =
   654     (EX y. foldSet times g z A y & v = g x * y)"
   655   apply auto
   656   apply (rule_tac A1 = A and f1 = times in finite_imp_foldSet [THEN exE])
   657    apply (fastsimp dest: foldSet_imp_finite)
   658   apply (blast intro: foldSet_determ)
   659   done
   660 
   661 text{* The recursion equation for @{text fold}: *}
   662 
   663 lemma fold_insert [simp]:
   664     "finite A ==> x \<notin> A ==> fold times g z (insert x A) = g x * fold times g z A"
   665   apply (unfold fold_def)
   666   apply (simp add: fold_insert_aux)
   667   apply (rule the_equality)
   668   apply (auto intro: finite_imp_foldSet
   669     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   670   done
   671 
   672 lemma fold_rec:
   673 assumes fin: "finite A" and a: "a:A"
   674 shows "fold times g z A = g a * fold times g z (A - {a})"
   675 proof-
   676   have A: "A = insert a (A - {a})" using a by blast
   677   hence "fold times g z A = fold times g z (insert a (A - {a}))" by simp
   678   also have "\<dots> = g a * fold times g z (A - {a})"
   679     by(rule fold_insert) (simp add:fin)+
   680   finally show ?thesis .
   681 qed
   682 
   683 end
   684 
   685 text{* A simplified version for idempotent functions: *}
   686 
   687 context ab_semigroup_idem_mult
   688 begin
   689 
   690 lemma fold_insert_idem:
   691 assumes finA: "finite A"
   692 shows "fold times g z (insert a A) = g a * fold times g z A"
   693 proof cases
   694   assume "a \<in> A"
   695   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
   696     by(blast dest: mk_disjoint_insert)
   697   show ?thesis
   698   proof -
   699     from finA A have finB: "finite B" by(blast intro: finite_subset)
   700     have "fold times g z (insert a A) = fold times g z (insert a B)" using A by simp
   701     also have "\<dots> = g a * fold times g z B"
   702       using finB disj by simp
   703     also have "\<dots> = g a * fold times g z A"
   704       using A finB disj
   705 	by (simp add: mult_idem mult_assoc [symmetric])
   706     finally show ?thesis .
   707   qed
   708 next
   709   assume "a \<notin> A"
   710   with finA show ?thesis by simp
   711 qed
   712 
   713 lemma foldI_conv_id:
   714   "finite A \<Longrightarrow> fold times g z A = fold times id z (g ` A)"
   715 by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert)
   716 
   717 end
   718 
   719 subsubsection{*Lemmas about @{text fold}*}
   720 
   721 context ab_semigroup_mult
   722 begin
   723 
   724 lemma fold_commute:
   725   "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
   726   apply (induct set: finite)
   727    apply simp
   728   apply (simp add: mult_left_commute [of x])
   729   done
   730 
   731 lemma fold_nest_Un_Int:
   732   "finite A ==> finite B
   733     ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
   734   apply (induct set: finite)
   735    apply simp
   736   apply (simp add: fold_commute Int_insert_left insert_absorb)
   737   done
   738 
   739 lemma fold_nest_Un_disjoint:
   740   "finite A ==> finite B ==> A Int B = {}
   741     ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
   742   by (simp add: fold_nest_Un_Int)
   743 
   744 lemma fold_reindex:
   745 assumes fin: "finite A"
   746 shows "inj_on h A \<Longrightarrow> fold times g z (h ` A) = fold times (g \<circ> h) z A"
   747 using fin apply induct
   748  apply simp
   749 apply simp
   750 done
   751 
   752 text{*
   753   Fusion theorem, as described in Graham Hutton's paper,
   754   A Tutorial on the Universality and Expressiveness of Fold,
   755   JFP 9:4 (355-372), 1999.
   756 *}
   757 
   758 lemma fold_fusion:
   759   assumes "ab_semigroup_mult g"
   760   assumes fin: "finite A"
   761     and hyp: "\<And>x y. h (g x y) = times x (h y)"
   762   shows "h (fold g j w A) = fold times j (h w) A"
   763 proof -
   764   interpret ab_semigroup_mult [g] by fact
   765   show ?thesis using fin hyp by (induct set: finite) simp_all
   766 qed
   767 
   768 lemma fold_cong:
   769   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
   770   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold times g z C = fold times h z C")
   771    apply simp
   772   apply (erule finite_induct, simp)
   773   apply (simp add: subset_insert_iff, clarify)
   774   apply (subgoal_tac "finite C")
   775    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   776   apply (subgoal_tac "C = insert x (C - {x})")
   777    prefer 2 apply blast
   778   apply (erule ssubst)
   779   apply (drule spec)
   780   apply (erule (1) notE impE)
   781   apply (simp add: Ball_def del: insert_Diff_single)
   782   done
   783 
   784 end
   785 
   786 context comm_monoid_mult
   787 begin
   788 
   789 lemma fold_Un_Int:
   790   "finite A ==> finite B ==>
   791     fold times g 1 A * fold times g 1 B =
   792     fold times g 1 (A Un B) * fold times g 1 (A Int B)"
   793   by (induct set: finite) 
   794     (auto simp add: mult_ac insert_absorb Int_insert_left)
   795 
   796 corollary fold_Un_disjoint:
   797   "finite A ==> finite B ==> A Int B = {} ==>
   798     fold times g 1 (A Un B) = fold times g 1 A * fold times g 1 B"
   799   by (simp add: fold_Un_Int)
   800 
   801 lemma fold_UN_disjoint:
   802   "\<lbrakk> finite I; ALL i:I. finite (A i);
   803      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   804    \<Longrightarrow> fold times g 1 (UNION I A) =
   805        fold times (%i. fold times g 1 (A i)) 1 I"
   806   apply (induct set: finite, simp, atomize)
   807   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   808    prefer 2 apply blast
   809   apply (subgoal_tac "A x Int UNION F A = {}")
   810    prefer 2 apply blast
   811   apply (simp add: fold_Un_disjoint)
   812   done
   813 
   814 lemma fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   815   fold times (%x. fold times (g x) 1 (B x)) 1 A =
   816   fold times (split g) 1 (SIGMA x:A. B x)"
   817 apply (subst Sigma_def)
   818 apply (subst fold_UN_disjoint, assumption, simp)
   819  apply blast
   820 apply (erule fold_cong)
   821 apply (subst fold_UN_disjoint, simp, simp)
   822  apply blast
   823 apply simp
   824 done
   825 
   826 lemma fold_distrib: "finite A \<Longrightarrow>
   827    fold times (%x. g x * h x) 1 A = fold times g 1 A *  fold times h 1 A"
   828   by (erule finite_induct) (simp_all add: mult_ac)
   829 
   830 end
   831 
   832 
   833 subsection {* Generalized summation over a set *}
   834 
   835 interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
   836   by unfold_locales (auto intro: add_assoc add_commute)
   837 
   838 constdefs
   839   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   840   "setsum f A == if finite A then fold (op +) f 0 A else 0"
   841 
   842 abbreviation
   843   Setsum  ("\<Sum>_" [1000] 999) where
   844   "\<Sum>A == setsum (%x. x) A"
   845 
   846 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   847 written @{text"\<Sum>x\<in>A. e"}. *}
   848 
   849 syntax
   850   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   851 syntax (xsymbols)
   852   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   853 syntax (HTML output)
   854   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   855 
   856 translations -- {* Beware of argument permutation! *}
   857   "SUM i:A. b" == "setsum (%i. b) A"
   858   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
   859 
   860 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   861  @{text"\<Sum>x|P. e"}. *}
   862 
   863 syntax
   864   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   865 syntax (xsymbols)
   866   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   867 syntax (HTML output)
   868   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   869 
   870 translations
   871   "SUM x|P. t" => "setsum (%x. t) {x. P}"
   872   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   873 
   874 print_translation {*
   875 let
   876   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   877     if x<>y then raise Match
   878     else let val x' = Syntax.mark_bound x
   879              val t' = subst_bound(x',t)
   880              val P' = subst_bound(x',P)
   881          in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
   882 in [("setsum", setsum_tr')] end
   883 *}
   884 
   885 
   886 lemma setsum_empty [simp]: "setsum f {} = 0"
   887   by (simp add: setsum_def)
   888 
   889 lemma setsum_insert [simp]:
   890     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   891   by (simp add: setsum_def)
   892 
   893 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   894   by (simp add: setsum_def)
   895 
   896 lemma setsum_reindex:
   897      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   898 by(auto simp add: setsum_def comm_monoid_add.fold_reindex dest!:finite_imageD)
   899 
   900 lemma setsum_reindex_id:
   901      "inj_on f B ==> setsum f B = setsum id (f ` B)"
   902 by (auto simp add: setsum_reindex)
   903 
   904 lemma setsum_cong:
   905   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   906 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_cong)
   907 
   908 lemma strong_setsum_cong[cong]:
   909   "A = B ==> (!!x. x:B =simp=> f x = g x)
   910    ==> setsum (%x. f x) A = setsum (%x. g x) B"
   911 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_cong)
   912 
   913 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
   914   by (rule setsum_cong[OF refl], auto);
   915 
   916 lemma setsum_reindex_cong:
   917      "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   918       ==> setsum h B = setsum g A"
   919   by (simp add: setsum_reindex cong: setsum_cong)
   920 
   921 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
   922 apply (clarsimp simp: setsum_def)
   923 apply (erule finite_induct, auto)
   924 done
   925 
   926 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
   927 by(simp add:setsum_cong)
   928 
   929 lemma setsum_Un_Int: "finite A ==> finite B ==>
   930   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   931   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   932 by(simp add: setsum_def comm_monoid_add.fold_Un_Int [symmetric])
   933 
   934 lemma setsum_Un_disjoint: "finite A ==> finite B
   935   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   936 by (subst setsum_Un_Int [symmetric], auto)
   937 
   938 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   939   the lhs need not be, since UNION I A could still be finite.*)
   940 lemma setsum_UN_disjoint:
   941     "finite I ==> (ALL i:I. finite (A i)) ==>
   942         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   943       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   944 by(simp add: setsum_def comm_monoid_add.fold_UN_disjoint cong: setsum_cong)
   945 
   946 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   947 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   948 lemma setsum_Union_disjoint:
   949   "[| (ALL A:C. finite A);
   950       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   951    ==> setsum f (Union C) = setsum (setsum f) C"
   952 apply (cases "finite C") 
   953  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   954   apply (frule setsum_UN_disjoint [of C id f])
   955  apply (unfold Union_def id_def, assumption+)
   956 done
   957 
   958 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   959   the rhs need not be, since SIGMA A B could still be finite.*)
   960 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   961     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   962 by(simp add:setsum_def comm_monoid_add.fold_Sigma split_def cong:setsum_cong)
   963 
   964 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   965 lemma setsum_cartesian_product: 
   966    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   967 apply (cases "finite A") 
   968  apply (cases "finite B") 
   969   apply (simp add: setsum_Sigma)
   970  apply (cases "A={}", simp)
   971  apply (simp) 
   972 apply (auto simp add: setsum_def
   973             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   974 done
   975 
   976 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   977 by(simp add:setsum_def comm_monoid_add.fold_distrib)
   978 
   979 
   980 subsubsection {* Properties in more restricted classes of structures *}
   981 
   982 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   983   apply (case_tac "finite A")
   984    prefer 2 apply (simp add: setsum_def)
   985   apply (erule rev_mp)
   986   apply (erule finite_induct, auto)
   987   done
   988 
   989 lemma setsum_eq_0_iff [simp]:
   990     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   991   by (induct set: finite) auto
   992 
   993 lemma setsum_Un_nat: "finite A ==> finite B ==>
   994     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   995   -- {* For the natural numbers, we have subtraction. *}
   996   by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
   997 
   998 lemma setsum_Un: "finite A ==> finite B ==>
   999     (setsum f (A Un B) :: 'a :: ab_group_add) =
  1000       setsum f A + setsum f B - setsum f (A Int B)"
  1001   by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
  1002 
  1003 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
  1004     (if a:A then setsum f A - f a else setsum f A)"
  1005   apply (case_tac "finite A")
  1006    prefer 2 apply (simp add: setsum_def)
  1007   apply (erule finite_induct)
  1008    apply (auto simp add: insert_Diff_if)
  1009   apply (drule_tac a = a in mk_disjoint_insert, auto)
  1010   done
  1011 
  1012 lemma setsum_diff1: "finite A \<Longrightarrow>
  1013   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1014   (if a:A then setsum f A - f a else setsum f A)"
  1015   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1016 
  1017 lemma setsum_diff1'[rule_format]: "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
  1018   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))"])
  1019   apply (auto simp add: insert_Diff_if add_ac)
  1020   done
  1021 
  1022 (* By Jeremy Siek: *)
  1023 
  1024 lemma setsum_diff_nat: 
  1025   assumes "finite B"
  1026     and "B \<subseteq> A"
  1027   shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1028   using prems
  1029 proof induct
  1030   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1031 next
  1032   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1033     and xFinA: "insert x F \<subseteq> A"
  1034     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1035   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1036   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1037     by (simp add: setsum_diff1_nat)
  1038   from xFinA have "F \<subseteq> A" by simp
  1039   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1040   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1041     by simp
  1042   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1043   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1044     by simp
  1045   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1046   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1047     by simp
  1048   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1049 qed
  1050 
  1051 lemma setsum_diff:
  1052   assumes le: "finite A" "B \<subseteq> A"
  1053   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1054 proof -
  1055   from le have finiteB: "finite B" using finite_subset by auto
  1056   show ?thesis using finiteB le
  1057   proof induct
  1058     case empty
  1059     thus ?case by auto
  1060   next
  1061     case (insert x F)
  1062     thus ?case using le finiteB 
  1063       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1064   qed
  1065 qed
  1066 
  1067 lemma setsum_mono:
  1068   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1069   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1070 proof (cases "finite K")
  1071   case True
  1072   thus ?thesis using le
  1073   proof induct
  1074     case empty
  1075     thus ?case by simp
  1076   next
  1077     case insert
  1078     thus ?case using add_mono by fastsimp
  1079   qed
  1080 next
  1081   case False
  1082   thus ?thesis
  1083     by (simp add: setsum_def)
  1084 qed
  1085 
  1086 lemma setsum_strict_mono:
  1087   fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
  1088   assumes "finite A"  "A \<noteq> {}"
  1089     and "!!x. x:A \<Longrightarrow> f x < g x"
  1090   shows "setsum f A < setsum g A"
  1091   using prems
  1092 proof (induct rule: finite_ne_induct)
  1093   case singleton thus ?case by simp
  1094 next
  1095   case insert thus ?case by (auto simp: add_strict_mono)
  1096 qed
  1097 
  1098 lemma setsum_negf:
  1099   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
  1100 proof (cases "finite A")
  1101   case True thus ?thesis by (induct set: finite) auto
  1102 next
  1103   case False thus ?thesis by (simp add: setsum_def)
  1104 qed
  1105 
  1106 lemma setsum_subtractf:
  1107   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1108     setsum f A - setsum g A"
  1109 proof (cases "finite A")
  1110   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
  1111 next
  1112   case False thus ?thesis by (simp add: setsum_def)
  1113 qed
  1114 
  1115 lemma setsum_nonneg:
  1116   assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
  1117   shows "0 \<le> setsum f A"
  1118 proof (cases "finite A")
  1119   case True thus ?thesis using nn
  1120   proof induct
  1121     case empty then show ?case by simp
  1122   next
  1123     case (insert x F)
  1124     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
  1125     with insert show ?case by simp
  1126   qed
  1127 next
  1128   case False thus ?thesis by (simp add: setsum_def)
  1129 qed
  1130 
  1131 lemma setsum_nonpos:
  1132   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
  1133   shows "setsum f A \<le> 0"
  1134 proof (cases "finite A")
  1135   case True thus ?thesis using np
  1136   proof induct
  1137     case empty then show ?case by simp
  1138   next
  1139     case (insert x F)
  1140     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
  1141     with insert show ?case by simp
  1142   qed
  1143 next
  1144   case False thus ?thesis by (simp add: setsum_def)
  1145 qed
  1146 
  1147 lemma setsum_mono2:
  1148 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
  1149 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
  1150 shows "setsum f A \<le> setsum f B"
  1151 proof -
  1152   have "setsum f A \<le> setsum f A + setsum f (B-A)"
  1153     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
  1154   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1155     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1156   also have "A \<union> (B-A) = B" using sub by blast
  1157   finally show ?thesis .
  1158 qed
  1159 
  1160 lemma setsum_mono3: "finite B ==> A <= B ==> 
  1161     ALL x: B - A. 
  1162       0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
  1163         setsum f A <= setsum f B"
  1164   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
  1165   apply (erule ssubst)
  1166   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
  1167   apply simp
  1168   apply (rule add_left_mono)
  1169   apply (erule setsum_nonneg)
  1170   apply (subst setsum_Un_disjoint [THEN sym])
  1171   apply (erule finite_subset, assumption)
  1172   apply (rule finite_subset)
  1173   prefer 2
  1174   apply assumption
  1175   apply auto
  1176   apply (rule setsum_cong)
  1177   apply auto
  1178 done
  1179 
  1180 lemma setsum_right_distrib: 
  1181   fixes f :: "'a => ('b::semiring_0)"
  1182   shows "r * setsum f A = setsum (%n. r * f n) A"
  1183 proof (cases "finite A")
  1184   case True
  1185   thus ?thesis
  1186   proof induct
  1187     case empty thus ?case by simp
  1188   next
  1189     case (insert x A) thus ?case by (simp add: right_distrib)
  1190   qed
  1191 next
  1192   case False thus ?thesis by (simp add: setsum_def)
  1193 qed
  1194 
  1195 lemma setsum_left_distrib:
  1196   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
  1197 proof (cases "finite A")
  1198   case True
  1199   then show ?thesis
  1200   proof induct
  1201     case empty thus ?case by simp
  1202   next
  1203     case (insert x A) thus ?case by (simp add: left_distrib)
  1204   qed
  1205 next
  1206   case False thus ?thesis by (simp add: setsum_def)
  1207 qed
  1208 
  1209 lemma setsum_divide_distrib:
  1210   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
  1211 proof (cases "finite A")
  1212   case True
  1213   then show ?thesis
  1214   proof induct
  1215     case empty thus ?case by simp
  1216   next
  1217     case (insert x A) thus ?case by (simp add: add_divide_distrib)
  1218   qed
  1219 next
  1220   case False thus ?thesis by (simp add: setsum_def)
  1221 qed
  1222 
  1223 lemma setsum_abs[iff]: 
  1224   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1225   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1226 proof (cases "finite A")
  1227   case True
  1228   thus ?thesis
  1229   proof induct
  1230     case empty thus ?case by simp
  1231   next
  1232     case (insert x A)
  1233     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1234   qed
  1235 next
  1236   case False thus ?thesis by (simp add: setsum_def)
  1237 qed
  1238 
  1239 lemma setsum_abs_ge_zero[iff]: 
  1240   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1241   shows "0 \<le> setsum (%i. abs(f i)) A"
  1242 proof (cases "finite A")
  1243   case True
  1244   thus ?thesis
  1245   proof induct
  1246     case empty thus ?case by simp
  1247   next
  1248     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
  1249   qed
  1250 next
  1251   case False thus ?thesis by (simp add: setsum_def)
  1252 qed
  1253 
  1254 lemma abs_setsum_abs[simp]: 
  1255   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1256   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1257 proof (cases "finite A")
  1258   case True
  1259   thus ?thesis
  1260   proof induct
  1261     case empty thus ?case by simp
  1262   next
  1263     case (insert a A)
  1264     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
  1265     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1266     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
  1267       by (simp del: abs_of_nonneg)
  1268     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1269     finally show ?case .
  1270   qed
  1271 next
  1272   case False thus ?thesis by (simp add: setsum_def)
  1273 qed
  1274 
  1275 
  1276 text {* Commuting outer and inner summation *}
  1277 
  1278 lemma swap_inj_on:
  1279   "inj_on (%(i, j). (j, i)) (A \<times> B)"
  1280   by (unfold inj_on_def) fast
  1281 
  1282 lemma swap_product:
  1283   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
  1284   by (simp add: split_def image_def) blast
  1285 
  1286 lemma setsum_commute:
  1287   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
  1288 proof (simp add: setsum_cartesian_product)
  1289   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
  1290     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
  1291     (is "?s = _")
  1292     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
  1293     apply (simp add: split_def)
  1294     done
  1295   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
  1296     (is "_ = ?t")
  1297     apply (simp add: swap_product)
  1298     done
  1299   finally show "?s = ?t" .
  1300 qed
  1301 
  1302 lemma setsum_product:
  1303   fixes f :: "'a => ('b::semiring_0)"
  1304   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
  1305   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
  1306 
  1307 
  1308 subsection {* Generalized product over a set *}
  1309 
  1310 constdefs
  1311   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1312   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1313 
  1314 abbreviation
  1315   Setprod  ("\<Prod>_" [1000] 999) where
  1316   "\<Prod>A == setprod (%x. x) A"
  1317 
  1318 syntax
  1319   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1320 syntax (xsymbols)
  1321   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1322 syntax (HTML output)
  1323   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1324 
  1325 translations -- {* Beware of argument permutation! *}
  1326   "PROD i:A. b" == "setprod (%i. b) A" 
  1327   "\<Prod>i\<in>A. b" == "setprod (%i. b) A" 
  1328 
  1329 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1330  @{text"\<Prod>x|P. e"}. *}
  1331 
  1332 syntax
  1333   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1334 syntax (xsymbols)
  1335   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1336 syntax (HTML output)
  1337   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1338 
  1339 translations
  1340   "PROD x|P. t" => "setprod (%x. t) {x. P}"
  1341   "\<Prod>x|P. t" => "setprod (%x. t) {x. P}"
  1342 
  1343 
  1344 lemma setprod_empty [simp]: "setprod f {} = 1"
  1345   by (auto simp add: setprod_def)
  1346 
  1347 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1348     setprod f (insert a A) = f a * setprod f A"
  1349   by (simp add: setprod_def)
  1350 
  1351 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1352   by (simp add: setprod_def)
  1353 
  1354 lemma setprod_reindex:
  1355      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1356 by(auto simp: setprod_def fold_reindex dest!:finite_imageD)
  1357 
  1358 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1359 by (auto simp add: setprod_reindex)
  1360 
  1361 lemma setprod_cong:
  1362   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1363 by(fastsimp simp: setprod_def intro: fold_cong)
  1364 
  1365 lemma strong_setprod_cong:
  1366   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1367 by(fastsimp simp: simp_implies_def setprod_def intro: fold_cong)
  1368 
  1369 lemma setprod_reindex_cong: "inj_on f A ==>
  1370     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1371   by (frule setprod_reindex, simp)
  1372 
  1373 
  1374 lemma setprod_1: "setprod (%i. 1) A = 1"
  1375   apply (case_tac "finite A")
  1376   apply (erule finite_induct, auto simp add: mult_ac)
  1377   done
  1378 
  1379 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1380   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1381   apply (erule ssubst, rule setprod_1)
  1382   apply (rule setprod_cong, auto)
  1383   done
  1384 
  1385 lemma setprod_Un_Int: "finite A ==> finite B
  1386     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1387 by(simp add: setprod_def fold_Un_Int[symmetric])
  1388 
  1389 lemma setprod_Un_disjoint: "finite A ==> finite B
  1390   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1391 by (subst setprod_Un_Int [symmetric], auto)
  1392 
  1393 lemma setprod_UN_disjoint:
  1394     "finite I ==> (ALL i:I. finite (A i)) ==>
  1395         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1396       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1397 by(simp add: setprod_def fold_UN_disjoint cong: setprod_cong)
  1398 
  1399 lemma setprod_Union_disjoint:
  1400   "[| (ALL A:C. finite A);
  1401       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1402    ==> setprod f (Union C) = setprod (setprod f) C"
  1403 apply (cases "finite C") 
  1404  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1405   apply (frule setprod_UN_disjoint [of C id f])
  1406  apply (unfold Union_def id_def, assumption+)
  1407 done
  1408 
  1409 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1410     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1411     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1412 by(simp add:setprod_def fold_Sigma split_def cong:setprod_cong)
  1413 
  1414 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1415 lemma setprod_cartesian_product: 
  1416      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1417 apply (cases "finite A") 
  1418  apply (cases "finite B") 
  1419   apply (simp add: setprod_Sigma)
  1420  apply (cases "A={}", simp)
  1421  apply (simp add: setprod_1) 
  1422 apply (auto simp add: setprod_def
  1423             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1424 done
  1425 
  1426 lemma setprod_timesf:
  1427      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1428 by(simp add:setprod_def fold_distrib)
  1429 
  1430 
  1431 subsubsection {* Properties in more restricted classes of structures *}
  1432 
  1433 lemma setprod_eq_1_iff [simp]:
  1434     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1435   by (induct set: finite) auto
  1436 
  1437 lemma setprod_zero:
  1438      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1439   apply (induct set: finite, force, clarsimp)
  1440   apply (erule disjE, auto)
  1441   done
  1442 
  1443 lemma setprod_nonneg [rule_format]:
  1444      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1445   apply (case_tac "finite A")
  1446   apply (induct set: finite, force, clarsimp)
  1447   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1448   apply (rule mult_mono, assumption+)
  1449   apply (auto simp add: setprod_def)
  1450   done
  1451 
  1452 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1453      --> 0 < setprod f A"
  1454   apply (case_tac "finite A")
  1455   apply (induct set: finite, force, clarsimp)
  1456   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1457   apply (rule mult_strict_mono, assumption+)
  1458   apply (auto simp add: setprod_def)
  1459   done
  1460 
  1461 lemma setprod_nonzero [rule_format]:
  1462     "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
  1463       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1464   apply (erule finite_induct, auto)
  1465   done
  1466 
  1467 lemma setprod_zero_eq:
  1468     "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
  1469      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1470   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1471   done
  1472 
  1473 lemma setprod_nonzero_field:
  1474     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
  1475   apply (rule setprod_nonzero, auto)
  1476   done
  1477 
  1478 lemma setprod_zero_eq_field:
  1479     "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
  1480   apply (rule setprod_zero_eq, auto)
  1481   done
  1482 
  1483 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1484     (setprod f (A Un B) :: 'a ::{field})
  1485       = setprod f A * setprod f B / setprod f (A Int B)"
  1486   apply (subst setprod_Un_Int [symmetric], auto)
  1487   apply (subgoal_tac "finite (A Int B)")
  1488   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1489   apply (subst times_divide_eq_right [THEN sym], auto)
  1490   done
  1491 
  1492 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1493     (setprod f (A - {a}) :: 'a :: {field}) =
  1494       (if a:A then setprod f A / f a else setprod f A)"
  1495 by (erule finite_induct) (auto simp add: insert_Diff_if)
  1496 
  1497 lemma setprod_inversef: "finite A ==>
  1498     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1499       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1500   apply (erule finite_induct)
  1501   apply (simp, simp)
  1502   done
  1503 
  1504 lemma setprod_dividef:
  1505      "[|finite A;
  1506         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1507       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1508   apply (subgoal_tac
  1509          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1510   apply (erule ssubst)
  1511   apply (subst divide_inverse)
  1512   apply (subst setprod_timesf)
  1513   apply (subst setprod_inversef, assumption+, rule refl)
  1514   apply (rule setprod_cong, rule refl)
  1515   apply (subst divide_inverse, auto)
  1516   done
  1517 
  1518 subsection {* Finite cardinality *}
  1519 
  1520 text {* This definition, although traditional, is ugly to work with:
  1521 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1522 But now that we have @{text setsum} things are easy:
  1523 *}
  1524 
  1525 definition
  1526   card :: "'a set \<Rightarrow> nat"
  1527 where
  1528   "card A = setsum (\<lambda>x. 1) A"
  1529 
  1530 lemma card_empty [simp]: "card {} = 0"
  1531 by (simp add: card_def)
  1532 
  1533 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1534 by (simp add: card_def)
  1535 
  1536 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1537 by (simp add: card_def)
  1538 
  1539 lemma card_insert_disjoint [simp]:
  1540   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1541 by(simp add: card_def)
  1542 
  1543 lemma card_insert_if:
  1544     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1545   by (simp add: insert_absorb)
  1546 
  1547 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
  1548   apply auto
  1549   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1550   done
  1551 
  1552 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1553 by auto
  1554 
  1555 
  1556 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1557 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1558 apply(simp del:insert_Diff_single)
  1559 done
  1560 
  1561 lemma card_Diff_singleton:
  1562   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1563 by (simp add: card_Suc_Diff1 [symmetric])
  1564 
  1565 lemma card_Diff_singleton_if:
  1566   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1567 by (simp add: card_Diff_singleton)
  1568 
  1569 lemma card_Diff_insert[simp]:
  1570 assumes "finite A" and "a:A" and "a ~: B"
  1571 shows "card(A - insert a B) = card(A - B) - 1"
  1572 proof -
  1573   have "A - insert a B = (A - B) - {a}" using assms by blast
  1574   then show ?thesis using assms by(simp add:card_Diff_singleton)
  1575 qed
  1576 
  1577 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1578 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
  1579 
  1580 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1581 by (simp add: card_insert_if)
  1582 
  1583 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1584 by (simp add: card_def setsum_mono2)
  1585 
  1586 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1587   apply (induct set: finite, simp, clarify)
  1588   apply (subgoal_tac "finite A & A - {x} <= F")
  1589    prefer 2 apply (blast intro: finite_subset, atomize)
  1590   apply (drule_tac x = "A - {x}" in spec)
  1591   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1592   apply (case_tac "card A", auto)
  1593   done
  1594 
  1595 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1596 apply (simp add: psubset_eq linorder_not_le [symmetric])
  1597 apply (blast dest: card_seteq)
  1598 done
  1599 
  1600 lemma card_Un_Int: "finite A ==> finite B
  1601     ==> card A + card B = card (A Un B) + card (A Int B)"
  1602 by(simp add:card_def setsum_Un_Int)
  1603 
  1604 lemma card_Un_disjoint: "finite A ==> finite B
  1605     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1606 by (simp add: card_Un_Int)
  1607 
  1608 lemma card_Diff_subset:
  1609   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1610 by(simp add:card_def setsum_diff_nat)
  1611 
  1612 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1613   apply (rule Suc_less_SucD)
  1614   apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
  1615   done
  1616 
  1617 lemma card_Diff2_less:
  1618     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1619   apply (case_tac "x = y")
  1620    apply (simp add: card_Diff1_less del:card_Diff_insert)
  1621   apply (rule less_trans)
  1622    prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
  1623   done
  1624 
  1625 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1626   apply (case_tac "x : A")
  1627    apply (simp_all add: card_Diff1_less less_imp_le)
  1628   done
  1629 
  1630 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1631 by (erule psubsetI, blast)
  1632 
  1633 lemma insert_partition:
  1634   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1635   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1636 by auto
  1637 
  1638 text{* main cardinality theorem *}
  1639 lemma card_partition [rule_format]:
  1640      "finite C ==>  
  1641         finite (\<Union> C) -->  
  1642         (\<forall>c\<in>C. card c = k) -->   
  1643         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1644         k * card(C) = card (\<Union> C)"
  1645 apply (erule finite_induct, simp)
  1646 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1647        finite_subset [of _ "\<Union> (insert x F)"])
  1648 done
  1649 
  1650 
  1651 text{*The form of a finite set of given cardinality*}
  1652 
  1653 lemma card_eq_SucD:
  1654 assumes "card A = Suc k"
  1655 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
  1656 proof -
  1657   have fin: "finite A" using assms by (auto intro: ccontr)
  1658   moreover have "card A \<noteq> 0" using assms by auto
  1659   ultimately obtain b where b: "b \<in> A" by auto
  1660   show ?thesis
  1661   proof (intro exI conjI)
  1662     show "A = insert b (A-{b})" using b by blast
  1663     show "b \<notin> A - {b}" by blast
  1664     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
  1665       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
  1666   qed
  1667 qed
  1668 
  1669 lemma card_Suc_eq:
  1670   "(card A = Suc k) =
  1671    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
  1672 apply(rule iffI)
  1673  apply(erule card_eq_SucD)
  1674 apply(auto)
  1675 apply(subst card_insert)
  1676  apply(auto intro:ccontr)
  1677 done
  1678 
  1679 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  1680 apply (cases "finite A")
  1681 apply (erule finite_induct)
  1682 apply (auto simp add: ring_simps)
  1683 done
  1684 
  1685 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
  1686   apply (erule finite_induct)
  1687   apply (auto simp add: power_Suc)
  1688   done
  1689 
  1690 lemma setsum_bounded:
  1691   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
  1692   shows "setsum f A \<le> of_nat(card A) * K"
  1693 proof (cases "finite A")
  1694   case True
  1695   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  1696 next
  1697   case False thus ?thesis by (simp add: setsum_def)
  1698 qed
  1699 
  1700 
  1701 subsubsection {* Cardinality of unions *}
  1702 
  1703 lemma card_UN_disjoint:
  1704     "finite I ==> (ALL i:I. finite (A i)) ==>
  1705         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1706       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1707   apply (simp add: card_def del: setsum_constant)
  1708   apply (subgoal_tac
  1709            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1710   apply (simp add: setsum_UN_disjoint del: setsum_constant)
  1711   apply (simp cong: setsum_cong)
  1712   done
  1713 
  1714 lemma card_Union_disjoint:
  1715   "finite C ==> (ALL A:C. finite A) ==>
  1716         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1717       card (Union C) = setsum card C"
  1718   apply (frule card_UN_disjoint [of C id])
  1719   apply (unfold Union_def id_def, assumption+)
  1720   done
  1721 
  1722 subsubsection {* Cardinality of image *}
  1723 
  1724 text{*The image of a finite set can be expressed using @{term fold}.*}
  1725 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1726 proof (induct rule: finite_induct)
  1727   case empty then show ?case by simp
  1728 next
  1729   interpret ab_semigroup_mult ["op Un"]
  1730     by unfold_locales auto
  1731   case insert 
  1732   then show ?case by simp
  1733 qed
  1734 
  1735 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1736   apply (induct set: finite)
  1737    apply simp
  1738   apply (simp add: le_SucI finite_imageI card_insert_if)
  1739   done
  1740 
  1741 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1742 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  1743 
  1744 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1745 by (simp add: card_seteq card_image)
  1746 
  1747 lemma eq_card_imp_inj_on:
  1748   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1749 apply (induct rule:finite_induct)
  1750 apply simp
  1751 apply(frule card_image_le[where f = f])
  1752 apply(simp add:card_insert_if split:if_splits)
  1753 done
  1754 
  1755 lemma inj_on_iff_eq_card:
  1756   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1757 by(blast intro: card_image eq_card_imp_inj_on)
  1758 
  1759 
  1760 lemma card_inj_on_le:
  1761     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1762 apply (subgoal_tac "finite A") 
  1763  apply (force intro: card_mono simp add: card_image [symmetric])
  1764 apply (blast intro: finite_imageD dest: finite_subset) 
  1765 done
  1766 
  1767 lemma card_bij_eq:
  1768     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1769        finite A; finite B |] ==> card A = card B"
  1770   by (auto intro: le_anti_sym card_inj_on_le)
  1771 
  1772 
  1773 subsubsection {* Cardinality of products *}
  1774 
  1775 (*
  1776 lemma SigmaI_insert: "y \<notin> A ==>
  1777   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1778   by auto
  1779 *)
  1780 
  1781 lemma card_SigmaI [simp]:
  1782   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1783   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1784 by(simp add:card_def setsum_Sigma del:setsum_constant)
  1785 
  1786 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1787 apply (cases "finite A") 
  1788 apply (cases "finite B") 
  1789 apply (auto simp add: card_eq_0_iff
  1790             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1791 done
  1792 
  1793 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1794 by (simp add: card_cartesian_product)
  1795 
  1796 
  1797 
  1798 subsubsection {* Cardinality of the Powerset *}
  1799 
  1800 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1801   apply (induct set: finite)
  1802    apply (simp_all add: Pow_insert)
  1803   apply (subst card_Un_disjoint, blast)
  1804     apply (blast intro: finite_imageI, blast)
  1805   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1806    apply (simp add: card_image Pow_insert)
  1807   apply (unfold inj_on_def)
  1808   apply (blast elim!: equalityE)
  1809   done
  1810 
  1811 text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
  1812 
  1813 lemma dvd_partition:
  1814   "finite (Union C) ==>
  1815     ALL c : C. k dvd card c ==>
  1816     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1817   k dvd card (Union C)"
  1818 apply(frule finite_UnionD)
  1819 apply(rotate_tac -1)
  1820   apply (induct set: finite, simp_all, clarify)
  1821   apply (subst card_Un_disjoint)
  1822   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1823   done
  1824 
  1825 
  1826 subsubsection {* Relating injectivity and surjectivity *}
  1827 
  1828 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
  1829 apply(rule eq_card_imp_inj_on, assumption)
  1830 apply(frule finite_imageI)
  1831 apply(drule (1) card_seteq)
  1832 apply(erule card_image_le)
  1833 apply simp
  1834 done
  1835 
  1836 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
  1837 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
  1838 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
  1839 
  1840 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
  1841 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
  1842 by(fastsimp simp:surj_def dest!: endo_inj_surj)
  1843 
  1844 corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
  1845 proof
  1846   assume "finite(UNIV::nat set)"
  1847   with finite_UNIV_inj_surj[of Suc]
  1848   show False by simp (blast dest: Suc_neq_Zero surjD)
  1849 qed
  1850 
  1851 
  1852 subsection{* A fold functional for non-empty sets *}
  1853 
  1854 text{* Does not require start value. *}
  1855 
  1856 inductive
  1857   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
  1858   for f :: "'a => 'a => 'a"
  1859 where
  1860   fold1Set_insertI [intro]:
  1861    "\<lbrakk> foldSet f id a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
  1862 
  1863 constdefs
  1864   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1865   "fold1 f A == THE x. fold1Set f A x"
  1866 
  1867 lemma fold1Set_nonempty:
  1868   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
  1869   by(erule fold1Set.cases, simp_all) 
  1870 
  1871 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
  1872 
  1873 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
  1874 
  1875 
  1876 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
  1877   by (blast intro: foldSet.intros elim: foldSet.cases)
  1878 
  1879 lemma fold1_singleton [simp]: "fold1 f {a} = a"
  1880   by (unfold fold1_def) blast
  1881 
  1882 lemma finite_nonempty_imp_fold1Set:
  1883   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
  1884 apply (induct A rule: finite_induct)
  1885 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1886 done
  1887 
  1888 text{*First, some lemmas about @{term foldSet}.*}
  1889 
  1890 context ab_semigroup_mult
  1891 begin
  1892 
  1893 lemma foldSet_insert_swap:
  1894 assumes fold: "foldSet times id b A y"
  1895 shows "b \<notin> A \<Longrightarrow> foldSet times id z (insert b A) (z * y)"
  1896 using fold
  1897 proof (induct rule: foldSet.induct)
  1898   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
  1899 next
  1900   case (insertI x A y)
  1901     have "foldSet times (\<lambda>u. u) z (insert x (insert b A)) (x * (z * y))"
  1902       using insertI by force  --{*how does @{term id} get unfolded?*}
  1903     thus ?case by (simp add: insert_commute mult_ac)
  1904 qed
  1905 
  1906 lemma foldSet_permute_diff:
  1907 assumes fold: "foldSet times id b A x"
  1908 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet times id a (insert b (A-{a})) x"
  1909 using fold
  1910 proof (induct rule: foldSet.induct)
  1911   case emptyI thus ?case by simp
  1912 next
  1913   case (insertI x A y)
  1914   have "a = x \<or> a \<in> A" using insertI by simp
  1915   thus ?case
  1916   proof
  1917     assume "a = x"
  1918     with insertI show ?thesis
  1919       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
  1920   next
  1921     assume ainA: "a \<in> A"
  1922     hence "foldSet times id a (insert x (insert b (A - {a}))) (x * y)"
  1923       using insertI by (force simp: id_def)
  1924     moreover
  1925     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1926       using ainA insertI by blast
  1927     ultimately show ?thesis by (simp add: id_def)
  1928   qed
  1929 qed
  1930 
  1931 lemma fold1_eq_fold:
  1932      "[|finite A; a \<notin> A|] ==> fold1 times (insert a A) = fold times id a A"
  1933 apply (simp add: fold1_def fold_def) 
  1934 apply (rule the_equality)
  1935 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ times id]) 
  1936 apply (rule sym, clarify)
  1937 apply (case_tac "Aa=A")
  1938  apply (best intro: the_equality foldSet_determ)  
  1939 apply (subgoal_tac "foldSet times id a A x")
  1940  apply (best intro: the_equality foldSet_determ)  
  1941 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1942  prefer 2 apply (blast elim: equalityE) 
  1943 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1944 done
  1945 
  1946 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  1947 apply safe
  1948 apply simp 
  1949 apply (drule_tac x=x in spec)
  1950 apply (drule_tac x="A-{x}" in spec, auto) 
  1951 done
  1952 
  1953 lemma fold1_insert:
  1954   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  1955   shows "fold1 times (insert x A) = x * fold1 times A"
  1956 proof -
  1957   from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
  1958     by (auto simp add: nonempty_iff)
  1959   with A show ?thesis
  1960     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
  1961 qed
  1962 
  1963 end
  1964 
  1965 context ab_semigroup_idem_mult
  1966 begin
  1967 
  1968 lemma fold1_insert_idem [simp]:
  1969   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  1970   shows "fold1 times (insert x A) = x * fold1 times A"
  1971 proof -
  1972   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
  1973     by (auto simp add: nonempty_iff)
  1974   show ?thesis
  1975   proof cases
  1976     assume "a = x"
  1977     thus ?thesis 
  1978     proof cases
  1979       assume "A' = {}"
  1980       with prems show ?thesis by (simp add: mult_idem) 
  1981     next
  1982       assume "A' \<noteq> {}"
  1983       with prems show ?thesis
  1984 	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem) 
  1985     qed
  1986   next
  1987     assume "a \<noteq> x"
  1988     with prems show ?thesis
  1989       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  1990   qed
  1991 qed
  1992 
  1993 lemma hom_fold1_commute:
  1994 assumes hom: "!!x y. h (x * y) = h x * h y"
  1995 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
  1996 using N proof (induct rule: finite_ne_induct)
  1997   case singleton thus ?case by simp
  1998 next
  1999   case (insert n N)
  2000   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
  2001   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
  2002   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
  2003   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
  2004     using insert by(simp)
  2005   also have "insert (h n) (h ` N) = h ` insert n N" by simp
  2006   finally show ?case .
  2007 qed
  2008 
  2009 end
  2010 
  2011 
  2012 text{* Now the recursion rules for definitions: *}
  2013 
  2014 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
  2015 by(simp add:fold1_singleton)
  2016 
  2017 lemma (in ab_semigroup_mult) fold1_insert_def:
  2018   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2019 by (simp add:fold1_insert)
  2020 
  2021 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
  2022   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2023 by simp
  2024 
  2025 subsubsection{* Determinacy for @{term fold1Set} *}
  2026 
  2027 text{*Not actually used!!*}
  2028 
  2029 context ab_semigroup_mult
  2030 begin
  2031 
  2032 lemma foldSet_permute:
  2033   "[|foldSet times id b (insert a A) x; a \<notin> A; b \<notin> A|]
  2034    ==> foldSet times id a (insert b A) x"
  2035 apply (cases "a=b") 
  2036 apply (auto dest: foldSet_permute_diff) 
  2037 done
  2038 
  2039 lemma fold1Set_determ:
  2040   "fold1Set times A x ==> fold1Set times A y ==> y = x"
  2041 proof (clarify elim!: fold1Set.cases)
  2042   fix A x B y a b
  2043   assume Ax: "foldSet times id a A x"
  2044   assume By: "foldSet times id b B y"
  2045   assume anotA:  "a \<notin> A"
  2046   assume bnotB:  "b \<notin> B"
  2047   assume eq: "insert a A = insert b B"
  2048   show "y=x"
  2049   proof cases
  2050     assume same: "a=b"
  2051     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  2052     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  2053   next
  2054     assume diff: "a\<noteq>b"
  2055     let ?D = "B - {a}"
  2056     have B: "B = insert a ?D" and A: "A = insert b ?D"
  2057      and aB: "a \<in> B" and bA: "b \<in> A"
  2058       using eq anotA bnotB diff by (blast elim!:equalityE)+
  2059     with aB bnotB By
  2060     have "foldSet times id a (insert b ?D) y" 
  2061       by (auto intro: foldSet_permute simp add: insert_absorb)
  2062     moreover
  2063     have "foldSet times id a (insert b ?D) x"
  2064       by (simp add: A [symmetric] Ax) 
  2065     ultimately show ?thesis by (blast intro: foldSet_determ) 
  2066   qed
  2067 qed
  2068 
  2069 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
  2070   by (unfold fold1_def) (blast intro: fold1Set_determ)
  2071 
  2072 end
  2073 
  2074 declare
  2075   empty_foldSetE [rule del]   foldSet.intros [rule del]
  2076   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  2077   -- {* No more proofs involve these relations. *}
  2078 
  2079 subsubsection {* Lemmas about @{text fold1} *}
  2080 
  2081 context ab_semigroup_mult
  2082 begin
  2083 
  2084 lemma fold1_Un:
  2085 assumes A: "finite A" "A \<noteq> {}"
  2086 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2087        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2088 using A by (induct rule: finite_ne_induct)
  2089   (simp_all add: fold1_insert mult_assoc)
  2090 
  2091 lemma fold1_in:
  2092   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
  2093   shows "fold1 times A \<in> A"
  2094 using A
  2095 proof (induct rule:finite_ne_induct)
  2096   case singleton thus ?case by simp
  2097 next
  2098   case insert thus ?case using elem by (force simp add:fold1_insert)
  2099 qed
  2100 
  2101 end
  2102 
  2103 lemma (in ab_semigroup_idem_mult) fold1_Un2:
  2104 assumes A: "finite A" "A \<noteq> {}"
  2105 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2106        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2107 using A
  2108 proof(induct rule:finite_ne_induct)
  2109   case singleton thus ?case by simp
  2110 next
  2111   case insert thus ?case by (simp add: mult_assoc)
  2112 qed
  2113 
  2114 
  2115 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
  2116 
  2117 text{*
  2118   As an application of @{text fold1} we define infimum
  2119   and supremum in (not necessarily complete!) lattices
  2120   over (non-empty) sets by means of @{text fold1}.
  2121 *}
  2122 
  2123 context lower_semilattice
  2124 begin
  2125 
  2126 lemma ab_semigroup_idem_mult_inf:
  2127   "ab_semigroup_idem_mult inf"
  2128   apply unfold_locales
  2129   apply (rule inf_assoc)
  2130   apply (rule inf_commute)
  2131   apply (rule inf_idem)
  2132   done
  2133 
  2134 lemma below_fold1_iff:
  2135   assumes "finite A" "A \<noteq> {}"
  2136   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2137 proof -
  2138   interpret ab_semigroup_idem_mult [inf]
  2139     by (rule ab_semigroup_idem_mult_inf)
  2140   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  2141 qed
  2142 
  2143 lemma fold1_belowI:
  2144   assumes "finite A"
  2145     and "a \<in> A"
  2146   shows "fold1 inf A \<le> a"
  2147 proof -
  2148   from assms have "A \<noteq> {}" by auto
  2149   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  2150   proof (induct rule: finite_ne_induct)
  2151     case singleton thus ?case by simp
  2152   next
  2153     interpret ab_semigroup_idem_mult [inf]
  2154       by (rule ab_semigroup_idem_mult_inf)
  2155     case (insert x F)
  2156     from insert(5) have "a = x \<or> a \<in> F" by simp
  2157     thus ?case
  2158     proof
  2159       assume "a = x" thus ?thesis using insert
  2160         by (simp add: mult_ac_idem)
  2161     next
  2162       assume "a \<in> F"
  2163       hence bel: "fold1 inf F \<le> a" by (rule insert)
  2164       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  2165         using insert by (simp add: mult_ac_idem)
  2166       also have "inf (fold1 inf F) a = fold1 inf F"
  2167         using bel by (auto intro: antisym)
  2168       also have "inf x \<dots> = fold1 inf (insert x F)"
  2169         using insert by (simp add: mult_ac_idem)
  2170       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  2171       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  2172       ultimately show ?thesis by simp
  2173     qed
  2174   qed
  2175 qed
  2176 
  2177 end
  2178 
  2179 lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
  2180   "ab_semigroup_idem_mult sup"
  2181   by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
  2182     (rule dual_lattice)
  2183 
  2184 context lattice
  2185 begin
  2186 
  2187 definition
  2188   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
  2189 where
  2190   "Inf_fin = fold1 inf"
  2191 
  2192 definition
  2193   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
  2194 where
  2195   "Sup_fin = fold1 sup"
  2196 
  2197 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
  2198 apply(unfold Sup_fin_def Inf_fin_def)
  2199 apply(subgoal_tac "EX a. a:A")
  2200 prefer 2 apply blast
  2201 apply(erule exE)
  2202 apply(rule order_trans)
  2203 apply(erule (1) fold1_belowI)
  2204 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
  2205 done
  2206 
  2207 lemma sup_Inf_absorb [simp]:
  2208   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
  2209 apply(subst sup_commute)
  2210 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  2211 done
  2212 
  2213 lemma inf_Sup_absorb [simp]:
  2214   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
  2215 by (simp add: Sup_fin_def inf_absorb1
  2216   lower_semilattice.fold1_belowI [OF dual_lattice])
  2217 
  2218 end
  2219 
  2220 context distrib_lattice
  2221 begin
  2222 
  2223 lemma sup_Inf1_distrib:
  2224   assumes "finite A"
  2225     and "A \<noteq> {}"
  2226   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  2227 proof -
  2228   interpret ab_semigroup_idem_mult [inf]
  2229     by (rule ab_semigroup_idem_mult_inf)
  2230   from assms show ?thesis
  2231     by (simp add: Inf_fin_def image_def
  2232       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  2233         (rule arg_cong [where f="fold1 inf"], blast)
  2234 qed
  2235 
  2236 lemma sup_Inf2_distrib:
  2237   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2238   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}"
  2239 using A proof (induct rule: finite_ne_induct)
  2240   case singleton thus ?case
  2241     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
  2242 next
  2243   interpret ab_semigroup_idem_mult [inf]
  2244     by (rule ab_semigroup_idem_mult_inf)
  2245   case (insert x A)
  2246   have finB: "finite {sup x b |b. b \<in> B}"
  2247     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  2248   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  2249   proof -
  2250     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  2251       by blast
  2252     thus ?thesis by(simp add: insert(1) B(1))
  2253   qed
  2254   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2255   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)"
  2256     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
  2257   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)
  2258   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})"
  2259     using insert by(simp add:sup_Inf1_distrib[OF B])
  2260   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})"
  2261     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  2262     using B insert
  2263     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  2264   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2265     by blast
  2266   finally show ?case .
  2267 qed
  2268 
  2269 lemma inf_Sup1_distrib:
  2270   assumes "finite A" and "A \<noteq> {}"
  2271   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  2272 proof -
  2273   interpret ab_semigroup_idem_mult [sup]
  2274     by (rule ab_semigroup_idem_mult_sup)
  2275   from assms show ?thesis
  2276     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  2277       (rule arg_cong [where f="fold1 sup"], blast)
  2278 qed
  2279 
  2280 lemma inf_Sup2_distrib:
  2281   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2282   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}"
  2283 using A proof (induct rule: finite_ne_induct)
  2284   case singleton thus ?case
  2285     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
  2286 next
  2287   case (insert x A)
  2288   have finB: "finite {inf x b |b. b \<in> B}"
  2289     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  2290   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  2291   proof -
  2292     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  2293       by blast
  2294     thus ?thesis by(simp add: insert(1) B(1))
  2295   qed
  2296   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2297   interpret ab_semigroup_idem_mult [sup]
  2298     by (rule ab_semigroup_idem_mult_sup)
  2299   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)"
  2300     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
  2301   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)
  2302   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})"
  2303     using insert by(simp add:inf_Sup1_distrib[OF B])
  2304   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})"
  2305     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  2306     using B insert
  2307     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  2308   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2309     by blast
  2310   finally show ?case .
  2311 qed
  2312 
  2313 end
  2314 
  2315 context complete_lattice
  2316 begin
  2317 
  2318 text {*
  2319   Coincidence on finite sets in complete lattices:
  2320 *}
  2321 
  2322 lemma Inf_fin_Inf:
  2323   assumes "finite A" and "A \<noteq> {}"
  2324   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  2325 proof -
  2326   interpret ab_semigroup_idem_mult [inf]
  2327     by (rule ab_semigroup_idem_mult_inf)
  2328   from assms show ?thesis
  2329   unfolding Inf_fin_def by (induct A set: finite)
  2330     (simp_all add: Inf_insert_simp)
  2331 qed
  2332 
  2333 lemma Sup_fin_Sup:
  2334   assumes "finite A" and "A \<noteq> {}"
  2335   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  2336 proof -
  2337   interpret ab_semigroup_idem_mult [sup]
  2338     by (rule ab_semigroup_idem_mult_sup)
  2339   from assms show ?thesis
  2340   unfolding Sup_fin_def by (induct A set: finite)
  2341     (simp_all add: Sup_insert_simp)
  2342 qed
  2343 
  2344 end
  2345 
  2346 
  2347 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
  2348 
  2349 text{*
  2350   As an application of @{text fold1} we define minimum
  2351   and maximum in (not necessarily complete!) linear orders
  2352   over (non-empty) sets by means of @{text fold1}.
  2353 *}
  2354 
  2355 context linorder
  2356 begin
  2357 
  2358 lemma ab_semigroup_idem_mult_min:
  2359   "ab_semigroup_idem_mult min"
  2360   by unfold_locales (auto simp add: min_def)
  2361 
  2362 lemma ab_semigroup_idem_mult_max:
  2363   "ab_semigroup_idem_mult max"
  2364   by unfold_locales (auto simp add: max_def)
  2365 
  2366 lemma min_lattice:
  2367   "lower_semilattice (op \<le>) (op <) min"
  2368   by unfold_locales (auto simp add: min_def)
  2369 
  2370 lemma max_lattice:
  2371   "lower_semilattice (op \<ge>) (op >) max"
  2372   by unfold_locales (auto simp add: max_def)
  2373 
  2374 lemma dual_max:
  2375   "ord.max (op \<ge>) = min"
  2376   by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
  2377 
  2378 lemma dual_min:
  2379   "ord.min (op \<ge>) = max"
  2380   by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
  2381 
  2382 lemma strict_below_fold1_iff:
  2383   assumes "finite A" and "A \<noteq> {}"
  2384   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2385 proof -
  2386   interpret ab_semigroup_idem_mult [min]
  2387     by (rule ab_semigroup_idem_mult_min)
  2388   from assms show ?thesis
  2389   by (induct rule: finite_ne_induct)
  2390     (simp_all add: fold1_insert)
  2391 qed
  2392 
  2393 lemma fold1_below_iff:
  2394   assumes "finite A" and "A \<noteq> {}"
  2395   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2396 proof -
  2397   interpret ab_semigroup_idem_mult [min]
  2398     by (rule ab_semigroup_idem_mult_min)
  2399   from assms show ?thesis
  2400   by (induct rule: finite_ne_induct)
  2401     (simp_all add: fold1_insert min_le_iff_disj)
  2402 qed
  2403 
  2404 lemma fold1_strict_below_iff:
  2405   assumes "finite A" and "A \<noteq> {}"
  2406   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2407 proof -
  2408   interpret ab_semigroup_idem_mult [min]
  2409     by (rule ab_semigroup_idem_mult_min)
  2410   from assms show ?thesis
  2411   by (induct rule: finite_ne_induct)
  2412     (simp_all add: fold1_insert min_less_iff_disj)
  2413 qed
  2414 
  2415 lemma fold1_antimono:
  2416   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  2417   shows "fold1 min B \<le> fold1 min A"
  2418 proof cases
  2419   assume "A = B" thus ?thesis by simp
  2420 next
  2421   interpret ab_semigroup_idem_mult [min]
  2422     by (rule ab_semigroup_idem_mult_min)
  2423   assume "A \<noteq> B"
  2424   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  2425   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  2426   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  2427   proof -
  2428     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  2429     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  2430     moreover have "(B-A) \<noteq> {}" using prems by blast
  2431     moreover have "A Int (B-A) = {}" using prems by blast
  2432     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  2433   qed
  2434   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  2435   finally show ?thesis .
  2436 qed
  2437 
  2438 definition
  2439   Min :: "'a set \<Rightarrow> 'a"
  2440 where
  2441   "Min = fold1 min"
  2442 
  2443 definition
  2444   Max :: "'a set \<Rightarrow> 'a"
  2445 where
  2446   "Max = fold1 max"
  2447 
  2448 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
  2449 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
  2450 
  2451 lemma Min_insert [simp]:
  2452   assumes "finite A" and "A \<noteq> {}"
  2453   shows "Min (insert x A) = min x (Min A)"
  2454 proof -
  2455   interpret ab_semigroup_idem_mult [min]
  2456     by (rule ab_semigroup_idem_mult_min)
  2457   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
  2458 qed
  2459 
  2460 lemma Max_insert [simp]:
  2461   assumes "finite A" and "A \<noteq> {}"
  2462   shows "Max (insert x A) = max x (Max A)"
  2463 proof -
  2464   interpret ab_semigroup_idem_mult [max]
  2465     by (rule ab_semigroup_idem_mult_max)
  2466   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
  2467 qed
  2468 
  2469 lemma Min_in [simp]:
  2470   assumes "finite A" and "A \<noteq> {}"
  2471   shows "Min A \<in> A"
  2472 proof -
  2473   interpret ab_semigroup_idem_mult [min]
  2474     by (rule ab_semigroup_idem_mult_min)
  2475   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
  2476 qed
  2477 
  2478 lemma Max_in [simp]:
  2479   assumes "finite A" and "A \<noteq> {}"
  2480   shows "Max A \<in> A"
  2481 proof -
  2482   interpret ab_semigroup_idem_mult [max]
  2483     by (rule ab_semigroup_idem_mult_max)
  2484   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
  2485 qed
  2486 
  2487 lemma Min_Un:
  2488   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2489   shows "Min (A \<union> B) = min (Min A) (Min B)"
  2490 proof -
  2491   interpret ab_semigroup_idem_mult [min]
  2492     by (rule ab_semigroup_idem_mult_min)
  2493   from assms show ?thesis
  2494     by (simp add: Min_def fold1_Un2)
  2495 qed
  2496 
  2497 lemma Max_Un:
  2498   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2499   shows "Max (A \<union> B) = max (Max A) (Max B)"
  2500 proof -
  2501   interpret ab_semigroup_idem_mult [max]
  2502     by (rule ab_semigroup_idem_mult_max)
  2503   from assms show ?thesis
  2504     by (simp add: Max_def fold1_Un2)
  2505 qed
  2506 
  2507 lemma hom_Min_commute:
  2508   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  2509     and "finite N" and "N \<noteq> {}"
  2510   shows "h (Min N) = Min (h ` N)"
  2511 proof -
  2512   interpret ab_semigroup_idem_mult [min]
  2513     by (rule ab_semigroup_idem_mult_min)
  2514   from assms show ?thesis
  2515     by (simp add: Min_def hom_fold1_commute)
  2516 qed
  2517 
  2518 lemma hom_Max_commute:
  2519   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  2520     and "finite N" and "N \<noteq> {}"
  2521   shows "h (Max N) = Max (h ` N)"
  2522 proof -
  2523   interpret ab_semigroup_idem_mult [max]
  2524     by (rule ab_semigroup_idem_mult_max)
  2525   from assms show ?thesis
  2526     by (simp add: Max_def hom_fold1_commute [of h])
  2527 qed
  2528 
  2529 lemma Min_le [simp]:
  2530   assumes "finite A" and "x \<in> A"
  2531   shows "Min A \<le> x"
  2532 proof -
  2533   interpret lower_semilattice ["op \<le>" "op <" min]
  2534     by (rule min_lattice)
  2535   from assms show ?thesis by (simp add: Min_def fold1_belowI)
  2536 qed
  2537 
  2538 lemma Max_ge [simp]:
  2539   assumes "finite A" and "x \<in> A"
  2540   shows "x \<le> Max A"
  2541 proof -
  2542   invoke lower_semilattice ["op \<ge>" "op >" max]
  2543     by (rule max_lattice)
  2544   from assms show ?thesis by (simp add: Max_def fold1_belowI)
  2545 qed
  2546 
  2547 lemma Min_ge_iff [simp, noatp]:
  2548   assumes "finite A" and "A \<noteq> {}"
  2549   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2550 proof -
  2551   interpret lower_semilattice ["op \<le>" "op <" min]
  2552     by (rule min_lattice)
  2553   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
  2554 qed
  2555 
  2556 lemma Max_le_iff [simp, noatp]:
  2557   assumes "finite A" and "A \<noteq> {}"
  2558   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2559 proof -
  2560   invoke lower_semilattice ["op \<ge>" "op >" max]
  2561     by (rule max_lattice)
  2562   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
  2563 qed
  2564 
  2565 lemma Min_gr_iff [simp, noatp]:
  2566   assumes "finite A" and "A \<noteq> {}"
  2567   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2568 proof -
  2569   interpret lower_semilattice ["op \<le>" "op <" min]
  2570     by (rule min_lattice)
  2571   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
  2572 qed
  2573 
  2574 lemma Max_less_iff [simp, noatp]:
  2575   assumes "finite A" and "A \<noteq> {}"
  2576   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  2577 proof -
  2578   note Max = Max_def
  2579   interpret linorder ["op \<ge>" "op >"]
  2580     by (rule dual_linorder)
  2581   from assms show ?thesis
  2582     by (simp add: Max strict_below_fold1_iff [folded dual_max])
  2583 qed
  2584 
  2585 lemma Min_le_iff [noatp]:
  2586   assumes "finite A" and "A \<noteq> {}"
  2587   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2588 proof -
  2589   interpret lower_semilattice ["op \<le>" "op <" min]
  2590     by (rule min_lattice)
  2591   from assms show ?thesis
  2592     by (simp add: Min_def fold1_below_iff)
  2593 qed
  2594 
  2595 lemma Max_ge_iff [noatp]:
  2596   assumes "finite A" and "A \<noteq> {}"
  2597   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  2598 proof -
  2599   note Max = Max_def
  2600   interpret linorder ["op \<ge>" "op >"]
  2601     by (rule dual_linorder)
  2602   from assms show ?thesis
  2603     by (simp add: Max fold1_below_iff [folded dual_max])
  2604 qed
  2605 
  2606 lemma Min_less_iff [noatp]:
  2607   assumes "finite A" and "A \<noteq> {}"
  2608   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2609 proof -
  2610   interpret lower_semilattice ["op \<le>" "op <" min]
  2611     by (rule min_lattice)
  2612   from assms show ?thesis
  2613     by (simp add: Min_def fold1_strict_below_iff)
  2614 qed
  2615 
  2616 lemma Max_gr_iff [noatp]:
  2617   assumes "finite A" and "A \<noteq> {}"
  2618   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  2619 proof -
  2620   note Max = Max_def
  2621   interpret linorder ["op \<ge>" "op >"]
  2622     by (rule dual_linorder)
  2623   from assms show ?thesis
  2624     by (simp add: Max fold1_strict_below_iff [folded dual_max])
  2625 qed
  2626 
  2627 lemma Min_antimono:
  2628   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2629   shows "Min N \<le> Min M"
  2630 proof -
  2631   interpret distrib_lattice ["op \<le>" "op <" min max]
  2632     by (rule distrib_lattice_min_max)
  2633   from assms show ?thesis by (simp add: Min_def fold1_antimono)
  2634 qed
  2635 
  2636 lemma Max_mono:
  2637   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2638   shows "Max M \<le> Max N"
  2639 proof -
  2640   note Max = Max_def
  2641   interpret linorder ["op \<ge>" "op >"]
  2642     by (rule dual_linorder)
  2643   from assms show ?thesis
  2644     by (simp add: Max fold1_antimono [folded dual_max])
  2645 qed
  2646 
  2647 lemma finite_linorder_induct[consumes 1, case_names empty insert]:
  2648  "finite A \<Longrightarrow> P {} \<Longrightarrow>
  2649   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
  2650   \<Longrightarrow> P A"
  2651 proof (induct A rule: measure_induct_rule[where f=card])
  2652   fix A :: "'a set"
  2653   assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
  2654                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
  2655                   \<Longrightarrow> P B"
  2656   and "finite A" and "P {}"
  2657   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
  2658   show "P A"
  2659   proof (cases "A = {}")
  2660     assume "A = {}" thus "P A" using `P {}` by simp
  2661   next
  2662     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
  2663     assume "A \<noteq> {}"
  2664     with `finite A` have "Max A : A" by auto
  2665     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
  2666     note card_Diff1_less[OF `finite A` `Max A : A`]
  2667     moreover have "finite ?B" using `finite A` by simp
  2668     ultimately have "P ?B" using `P {}` step IH by blast
  2669     moreover have "\<forall>a\<in>?B. a < Max A"
  2670       using Max_ge [OF `finite A`] by fastsimp
  2671     ultimately show "P A"
  2672       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
  2673   qed
  2674 qed
  2675 
  2676 end
  2677 
  2678 context ordered_ab_semigroup_add
  2679 begin
  2680 
  2681 lemma add_Min_commute:
  2682   fixes k
  2683   assumes "finite N" and "N \<noteq> {}"
  2684   shows "k + Min N = Min {k + m | m. m \<in> N}"
  2685 proof -
  2686   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  2687     by (simp add: min_def not_le)
  2688       (blast intro: antisym less_imp_le add_left_mono)
  2689   with assms show ?thesis
  2690     using hom_Min_commute [of "plus k" N]
  2691     by simp (blast intro: arg_cong [where f = Min])
  2692 qed
  2693 
  2694 lemma add_Max_commute:
  2695   fixes k
  2696   assumes "finite N" and "N \<noteq> {}"
  2697   shows "k + Max N = Max {k + m | m. m \<in> N}"
  2698 proof -
  2699   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  2700     by (simp add: max_def not_le)
  2701       (blast intro: antisym less_imp_le add_left_mono)
  2702   with assms show ?thesis
  2703     using hom_Max_commute [of "plus k" N]
  2704     by simp (blast intro: arg_cong [where f = Max])
  2705 qed
  2706 
  2707 end
  2708 
  2709 end