src/HOL/Finite_Set.thy
author nipkow
Wed Feb 02 09:15:40 2005 +0100 (2005-02-02)
changeset 15484 2636ec211ec8
parent 15483 704b3ce6d0f7
child 15487 55497029b255
permissions -rw-r--r--
fold and fol1 changes
     1 (*  Title:      HOL/Finite_Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     4                 Additions by Jeremy Avigad in Feb 2004
     5 *)
     6 
     7 header {* Finite sets *}
     8 
     9 theory Finite_Set
    10 imports Divides Power Inductive
    11 begin
    12 
    13 subsection {* Definition and basic properties *}
    14 
    15 consts Finites :: "'a set set"
    16 syntax
    17   finite :: "'a set => bool"
    18 translations
    19   "finite A" == "A : Finites"
    20 
    21 inductive Finites
    22   intros
    23     emptyI [simp, intro!]: "{} : Finites"
    24     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    25 
    26 axclass finite \<subseteq> type
    27   finite: "finite UNIV"
    28 
    29 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    30   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    31   shows "\<exists>a::'a. a \<notin> A"
    32 proof -
    33   from prems have "A \<noteq> UNIV" by blast
    34   thus ?thesis by blast
    35 qed
    36 
    37 lemma finite_induct [case_names empty insert, induct set: Finites]:
    38   "finite F ==>
    39     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    40   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    41 proof -
    42   assume "P {}" and
    43     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    44   assume "finite F"
    45   thus "P F"
    46   proof induct
    47     show "P {}" .
    48     fix x F assume F: "finite F" and P: "P F"
    49     show "P (insert x F)"
    50     proof cases
    51       assume "x \<in> F"
    52       hence "insert x F = F" by (rule insert_absorb)
    53       with P show ?thesis by (simp only:)
    54     next
    55       assume "x \<notin> F"
    56       from F this P show ?thesis by (rule insert)
    57     qed
    58   qed
    59 qed
    60 
    61 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
    62 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
    63  \<lbrakk> \<And>x. P{x};
    64    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
    65  \<Longrightarrow> P F"
    66 using fin
    67 proof induct
    68   case empty thus ?case by simp
    69 next
    70   case (insert x F)
    71   show ?case
    72   proof cases
    73     assume "F = {}" thus ?thesis using insert(4) by simp
    74   next
    75     assume "F \<noteq> {}" thus ?thesis using insert by blast
    76   qed
    77 qed
    78 
    79 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    80   "finite F ==> F \<subseteq> A ==>
    81     P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    82     P F"
    83 proof -
    84   assume "P {}" and insert:
    85     "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    86   assume "finite F"
    87   thus "F \<subseteq> A ==> P F"
    88   proof induct
    89     show "P {}" .
    90     fix x F assume "finite F" and "x \<notin> F"
    91       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    92     show "P (insert x F)"
    93     proof (rule insert)
    94       from i show "x \<in> A" by blast
    95       from i have "F \<subseteq> A" by blast
    96       with P show "P F" .
    97     qed
    98   qed
    99 qed
   100 
   101 text{* Finite sets are the images of initial segments of natural numbers: *}
   102 
   103 lemma finite_imp_nat_seg_image:
   104 assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}"
   105 using fin
   106 proof induct
   107   case empty
   108   show ?case
   109   proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed
   110 next
   111   case (insert a A)
   112   from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast
   113   hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}"
   114     by (auto simp add:image_def Ball_def)
   115   thus ?case by blast
   116 qed
   117 
   118 lemma nat_seg_image_imp_finite:
   119   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
   120 proof (induct n)
   121   case 0 thus ?case by simp
   122 next
   123   case (Suc n)
   124   let ?B = "f ` {i. i < n}"
   125   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
   126   show ?case
   127   proof cases
   128     assume "\<exists>k<n. f n = f k"
   129     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
   130     thus ?thesis using finB by simp
   131   next
   132     assume "\<not>(\<exists> k<n. f n = f k)"
   133     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
   134     thus ?thesis using finB by simp
   135   qed
   136 qed
   137 
   138 lemma finite_conv_nat_seg_image:
   139   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
   140 by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite)
   141 
   142 subsubsection{* Finiteness and set theoretic constructions *}
   143 
   144 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
   145   -- {* The union of two finite sets is finite. *}
   146   by (induct set: Finites) simp_all
   147 
   148 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
   149   -- {* Every subset of a finite set is finite. *}
   150 proof -
   151   assume "finite B"
   152   thus "!!A. A \<subseteq> B ==> finite A"
   153   proof induct
   154     case empty
   155     thus ?case by simp
   156   next
   157     case (insert x F A)
   158     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
   159     show "finite A"
   160     proof cases
   161       assume x: "x \<in> A"
   162       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
   163       with r have "finite (A - {x})" .
   164       hence "finite (insert x (A - {x}))" ..
   165       also have "insert x (A - {x}) = A" by (rule insert_Diff)
   166       finally show ?thesis .
   167     next
   168       show "A \<subseteq> F ==> ?thesis" .
   169       assume "x \<notin> A"
   170       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   171     qed
   172   qed
   173 qed
   174 
   175 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   176   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   177 
   178 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   179   -- {* The converse obviously fails. *}
   180   by (blast intro: finite_subset)
   181 
   182 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   183   apply (subst insert_is_Un)
   184   apply (simp only: finite_Un, blast)
   185   done
   186 
   187 lemma finite_Union[simp, intro]:
   188  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
   189 by (induct rule:finite_induct) simp_all
   190 
   191 lemma finite_empty_induct:
   192   "finite A ==>
   193   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
   194 proof -
   195   assume "finite A"
   196     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   197   have "P (A - A)"
   198   proof -
   199     fix c b :: "'a set"
   200     presume c: "finite c" and b: "finite b"
   201       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   202     from c show "c \<subseteq> b ==> P (b - c)"
   203     proof induct
   204       case empty
   205       from P1 show ?case by simp
   206     next
   207       case (insert x F)
   208       have "P (b - F - {x})"
   209       proof (rule P2)
   210         from _ b show "finite (b - F)" by (rule finite_subset) blast
   211         from insert show "x \<in> b - F" by simp
   212         from insert show "P (b - F)" by simp
   213       qed
   214       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   215       finally show ?case .
   216     qed
   217   next
   218     show "A \<subseteq> A" ..
   219   qed
   220   thus "P {}" by simp
   221 qed
   222 
   223 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   224   by (rule Diff_subset [THEN finite_subset])
   225 
   226 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   227   apply (subst Diff_insert)
   228   apply (case_tac "a : A - B")
   229    apply (rule finite_insert [symmetric, THEN trans])
   230    apply (subst insert_Diff, simp_all)
   231   done
   232 
   233 
   234 text {* Image and Inverse Image over Finite Sets *}
   235 
   236 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   237   -- {* The image of a finite set is finite. *}
   238   by (induct set: Finites) simp_all
   239 
   240 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   241   apply (frule finite_imageI)
   242   apply (erule finite_subset, assumption)
   243   done
   244 
   245 lemma finite_range_imageI:
   246     "finite (range g) ==> finite (range (%x. f (g x)))"
   247   apply (drule finite_imageI, simp)
   248   done
   249 
   250 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   251 proof -
   252   have aux: "!!A. finite (A - {}) = finite A" by simp
   253   fix B :: "'a set"
   254   assume "finite B"
   255   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   256     apply induct
   257      apply simp
   258     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   259      apply clarify
   260      apply (simp (no_asm_use) add: inj_on_def)
   261      apply (blast dest!: aux [THEN iffD1], atomize)
   262     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   263     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   264     apply (rule_tac x = xa in bexI)
   265      apply (simp_all add: inj_on_image_set_diff)
   266     done
   267 qed (rule refl)
   268 
   269 
   270 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   271   -- {* The inverse image of a singleton under an injective function
   272          is included in a singleton. *}
   273   apply (auto simp add: inj_on_def)
   274   apply (blast intro: the_equality [symmetric])
   275   done
   276 
   277 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   278   -- {* The inverse image of a finite set under an injective function
   279          is finite. *}
   280   apply (induct set: Finites, simp_all)
   281   apply (subst vimage_insert)
   282   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   283   done
   284 
   285 
   286 text {* The finite UNION of finite sets *}
   287 
   288 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   289   by (induct set: Finites) simp_all
   290 
   291 text {*
   292   Strengthen RHS to
   293   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   294 
   295   We'd need to prove
   296   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   297   by induction. *}
   298 
   299 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   300   by (blast intro: finite_UN_I finite_subset)
   301 
   302 
   303 text {* Sigma of finite sets *}
   304 
   305 lemma finite_SigmaI [simp]:
   306     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   307   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   308 
   309 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   310     finite (A <*> B)"
   311   by (rule finite_SigmaI)
   312 
   313 lemma finite_Prod_UNIV:
   314     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   315   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   316    apply (erule ssubst)
   317    apply (erule finite_SigmaI, auto)
   318   done
   319 
   320 lemma finite_cartesian_productD1:
   321      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
   322 apply (auto simp add: finite_conv_nat_seg_image) 
   323 apply (drule_tac x=n in spec) 
   324 apply (drule_tac x="fst o f" in spec) 
   325 apply (auto simp add: o_def) 
   326  prefer 2 apply (force dest!: equalityD2) 
   327 apply (drule equalityD1) 
   328 apply (rename_tac y x)
   329 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   330  prefer 2 apply force
   331 apply clarify
   332 apply (rule_tac x=k in image_eqI, auto)
   333 done
   334 
   335 lemma finite_cartesian_productD2:
   336      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
   337 apply (auto simp add: finite_conv_nat_seg_image) 
   338 apply (drule_tac x=n in spec) 
   339 apply (drule_tac x="snd 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 x y)
   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 
   351 instance unit :: finite
   352 proof
   353   have "finite {()}" by simp
   354   also have "{()} = UNIV" by auto
   355   finally show "finite (UNIV :: unit set)" .
   356 qed
   357 
   358 instance * :: (finite, finite) finite
   359 proof
   360   show "finite (UNIV :: ('a \<times> 'b) set)"
   361   proof (rule finite_Prod_UNIV)
   362     show "finite (UNIV :: 'a set)" by (rule finite)
   363     show "finite (UNIV :: 'b set)" by (rule finite)
   364   qed
   365 qed
   366 
   367 
   368 text {* The powerset of a finite set *}
   369 
   370 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   371 proof
   372   assume "finite (Pow A)"
   373   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   374   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   375 next
   376   assume "finite A"
   377   thus "finite (Pow A)"
   378     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   379 qed
   380 
   381 
   382 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   383 by(blast intro: finite_subset[OF subset_Pow_Union])
   384 
   385 
   386 lemma finite_converse [iff]: "finite (r^-1) = finite r"
   387   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   388    apply simp
   389    apply (rule iffI)
   390     apply (erule finite_imageD [unfolded inj_on_def])
   391     apply (simp split add: split_split)
   392    apply (erule finite_imageI)
   393   apply (simp add: converse_def image_def, auto)
   394   apply (rule bexI)
   395    prefer 2 apply assumption
   396   apply simp
   397   done
   398 
   399 
   400 text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
   401 Ehmety) *}
   402 
   403 lemma finite_Field: "finite r ==> finite (Field r)"
   404   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   405   apply (induct set: Finites)
   406    apply (auto simp add: Field_def Domain_insert Range_insert)
   407   done
   408 
   409 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   410   apply clarify
   411   apply (erule trancl_induct)
   412    apply (auto simp add: Field_def)
   413   done
   414 
   415 lemma finite_trancl: "finite (r^+) = finite r"
   416   apply auto
   417    prefer 2
   418    apply (rule trancl_subset_Field2 [THEN finite_subset])
   419    apply (rule finite_SigmaI)
   420     prefer 3
   421     apply (blast intro: r_into_trancl' finite_subset)
   422    apply (auto simp add: finite_Field)
   423   done
   424 
   425 
   426 subsection {* A fold functional for finite sets *}
   427 
   428 text {* The intended behaviour is
   429 @{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"}
   430 if @{text f} is associative-commutative. For an application of @{text fold}
   431 se the definitions of sums and products over finite sets.
   432 *}
   433 
   434 consts
   435   foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
   436 
   437 inductive "foldSet f g z"
   438 intros
   439 emptyI [intro]: "({}, z) : foldSet f g z"
   440 insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk>
   441  \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z"
   442 
   443 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
   444 
   445 constdefs
   446   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
   447   "fold f g z A == THE x. (A, x) : foldSet f g z"
   448 
   449 lemma Diff1_foldSet:
   450   "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z"
   451 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   452 
   453 lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A"
   454   by (induct set: foldSet) auto
   455 
   456 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z"
   457   by (induct set: Finites) auto
   458 
   459 
   460 subsubsection {* Commutative monoids *}
   461 
   462 locale ACf =
   463   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   464   assumes commute: "x \<cdot> y = y \<cdot> x"
   465     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   466 
   467 locale ACe = ACf +
   468   fixes e :: 'a
   469   assumes ident [simp]: "x \<cdot> e = x"
   470 
   471 locale ACIf = ACf +
   472   assumes idem: "x \<cdot> x = x"
   473 
   474 lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   475 proof -
   476   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   477   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   478   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   479   finally show ?thesis .
   480 qed
   481 
   482 lemmas (in ACf) AC = assoc commute left_commute
   483 
   484 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
   485 proof -
   486   have "x \<cdot> e = x" by (rule ident)
   487   thus ?thesis by (subst commute)
   488 qed
   489 
   490 text{* Instantiation of locales: *}
   491 
   492 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
   493 by(fastsimp intro: ACf.intro add_assoc add_commute)
   494 
   495 lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
   496 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
   497 
   498 
   499 lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
   500 by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
   501 
   502 lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
   503 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
   504 
   505 
   506 subsubsection{*From @{term foldSet} to @{term fold}*}
   507 
   508 (* only used in the next lemma, but in there twice *)
   509 lemma card_lemma: assumes A1: "A = insert b B" and notinB: "b \<notin> B" and
   510   card: "A = h`{i. i<Suc n}" and new: "\<not>(EX k<n. h n = h k)"
   511 shows "EX h. B = h`{i. i<n}" (is "EX h. ?P h")
   512 proof
   513   let ?h = "%i. if h i = b then h n else h i"
   514   show "B = ?h`{i. i<n}" (is "_ = ?r")
   515   proof
   516     show "B \<subseteq> ?r"
   517     proof
   518       fix u assume "u \<in> B"
   519       hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
   520       then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
   521 	using card by(auto simp:image_def)
   522       show "u \<in> ?r"
   523       proof cases
   524 	assume "i\<^isub>u < n"
   525 	thus ?thesis using unotb by(fastsimp)
   526       next
   527 	assume "\<not> i\<^isub>u < n"
   528 	with below have [simp]: "i\<^isub>u = n" by arith
   529 	obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
   530 	  using A1 card by blast
   531 	have "i\<^isub>k < n"
   532 	proof (rule ccontr)
   533 	  assume "\<not> i\<^isub>k < n"
   534 	  hence "i\<^isub>k = n" using i\<^isub>k by arith
   535 	  thus False using unotb by simp
   536 	qed
   537 	thus ?thesis by(auto simp add:image_def)
   538       qed
   539     qed
   540   next
   541     show "?r \<subseteq> B"
   542     proof
   543       fix u assume "u \<in> ?r"
   544       then obtain i\<^isub>u where below: "i\<^isub>u < n" and
   545         or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
   546 	by(auto simp:image_def)
   547       from or show "u \<in> B"
   548       proof
   549 	assume [simp]: "b = h i\<^isub>u \<and> u = h n"
   550 	have "u \<in> A" using card by auto
   551         moreover have "u \<noteq> b" using new below by auto
   552 	ultimately show "u \<in> B" using A1 by blast
   553       next
   554 	assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
   555 	moreover hence "u \<in> A" using card below by auto
   556 	ultimately show "u \<in> B" using A1 by blast
   557       qed
   558     qed
   559   qed
   560 qed
   561 
   562 lemma (in ACf) foldSet_determ_aux:
   563   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
   564    \<Longrightarrow> x' = x"
   565 proof (induct n)
   566   case 0 thus ?case by auto
   567 next
   568   case (Suc n)
   569   have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g z; (A,x') \<in> foldSet f g z\<rbrakk>
   570            \<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}"
   571   and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" .
   572   show ?case
   573   proof cases
   574     assume "EX k<n. h n = h k"
   575     hence card': "A = h ` {i. i < n}"
   576       using card by (auto simp:image_def less_Suc_eq)
   577     show ?thesis by(rule IH[OF card' Afoldx Afoldy])
   578   next
   579     assume new: "\<not>(EX k<n. h n = h k)"
   580     show ?thesis
   581     proof (rule foldSet.cases[OF Afoldx])
   582       assume "(A, x) = ({}, z)"
   583       thus "x' = x" using Afoldy by (auto)
   584     next
   585       fix B b y
   586       assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   587 	and y: "(B,y) \<in> foldSet f g z" and notinB: "b \<notin> B"
   588       hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   589       show ?thesis
   590       proof (rule foldSet.cases[OF Afoldy])
   591 	assume "(A,x') = ({}, z)"
   592 	thus ?thesis using A1 by auto
   593       next
   594 	fix C c r
   595 	assume eq2: "(A,x') = (insert c C, g c \<cdot> r)"
   596 	  and r: "(C,r) \<in> foldSet f g z" and notinC: "c \<notin> C"
   597 	hence A2: "A = insert c C" and x': "x' = g c \<cdot> r" by auto
   598 	obtain hB where lessB: "B = hB ` {i. i<n}"
   599 	  using card_lemma[OF A1 notinB card new] by auto
   600 	obtain hC where lessC: "C = hC ` {i. i<n}"
   601 	  using card_lemma[OF A2 notinC card new] by auto
   602 	show ?thesis
   603 	proof cases
   604 	  assume "b = c"
   605 	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   606 	  ultimately show ?thesis using IH[OF lessB] y r x x' by auto
   607 	next
   608 	  assume diff: "b \<noteq> c"
   609 	  let ?D = "B - {c}"
   610 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   611 	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   612 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   613 	  with A1 have "finite ?D" by simp
   614 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
   615 	    using finite_imp_foldSet by rules
   616 	  moreover have cinB: "c \<in> B" using B by(auto)
   617 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   618 	    by(rule Diff1_foldSet)
   619 	  hence "g c \<cdot> d = y" by(rule IH[OF lessB y])
   620           moreover have "g b \<cdot> d = r"
   621 	  proof (rule IH[OF lessC r])
   622 	    show "(C,g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   623 	      by fastsimp
   624 	  qed
   625 	  ultimately show ?thesis using x x' by(auto simp:AC)
   626 	qed
   627       qed
   628     qed
   629   qed
   630 qed
   631 
   632 (* The same proof, but using card 
   633 lemma (in ACf) foldSet_determ_aux:
   634   "!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
   635    \<Longrightarrow> x' = x"
   636 proof (induct n)
   637   case 0 thus ?case by simp
   638 next
   639   case (Suc n)
   640   have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
   641            \<Longrightarrow> x' = x" and card: "card A < Suc n"
   642   and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
   643   from card have "card A < n \<or> card A = n" by arith
   644   thus ?case
   645   proof
   646     assume less: "card A < n"
   647     show ?thesis by(rule IH[OF less Afoldx Afoldy])
   648   next
   649     assume cardA: "card A = n"
   650     show ?thesis
   651     proof (rule foldSet.cases[OF Afoldx])
   652       assume "(A, x) = ({}, e)"
   653       thus "x' = x" using Afoldy by (auto)
   654     next
   655       fix B b y
   656       assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   657 	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
   658       hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   659       show ?thesis
   660       proof (rule foldSet.cases[OF Afoldy])
   661 	assume "(A,x') = ({}, e)"
   662 	thus ?thesis using A1 by auto
   663       next
   664 	fix C c z
   665 	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
   666 	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
   667 	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
   668 	have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   669 	with cardA A1 notinB have less: "card B < n" by simp
   670 	show ?thesis
   671 	proof cases
   672 	  assume "b = c"
   673 	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   674 	  ultimately show ?thesis using IH[OF less] y z x x' by auto
   675 	next
   676 	  assume diff: "b \<noteq> c"
   677 	  let ?D = "B - {c}"
   678 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   679 	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   680 	  have "finite ?D" using finA A1 by simp
   681 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
   682 	    using finite_imp_foldSet by rules
   683 	  moreover have cinB: "c \<in> B" using B by(auto)
   684 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
   685 	    by(rule Diff1_foldSet)
   686 	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
   687           moreover have "g b \<cdot> d = z"
   688 	  proof (rule IH[OF _ z])
   689 	    show "card C < n" using C cardA A1 notinB finA cinB
   690 	      by(auto simp:card_Diff1_less)
   691 	  next
   692 	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
   693 	      by fastsimp
   694 	  qed
   695 	  ultimately show ?thesis using x x' by(auto simp:AC)
   696 	qed
   697       qed
   698     qed
   699   qed
   700 qed
   701 *)
   702 
   703 lemma (in ACf) foldSet_determ:
   704   "(A, x) : foldSet f g z ==> (A, y) : foldSet f g z ==> y = x"
   705 apply(frule foldSet_imp_finite)
   706 apply(simp add:finite_conv_nat_seg_image)
   707 apply(blast intro: foldSet_determ_aux [rule_format])
   708 done
   709 
   710 lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
   711   by (unfold fold_def) (blast intro: foldSet_determ)
   712 
   713 text{* The base case for @{text fold}: *}
   714 
   715 lemma fold_empty [simp]: "fold f g z {} = z"
   716   by (unfold fold_def) blast
   717 
   718 lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   719     ((insert x A, v) : foldSet f g z) =
   720     (EX y. (A, y) : foldSet f g z & v = f (g x) y)"
   721   apply auto
   722   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   723    apply (fastsimp dest: foldSet_imp_finite)
   724   apply (blast intro: foldSet_determ)
   725   done
   726 
   727 text{* The recursion equation for @{text fold}: *}
   728 
   729 lemma (in ACf) fold_insert[simp]:
   730     "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
   731   apply (unfold fold_def)
   732   apply (simp add: fold_insert_aux)
   733   apply (rule the_equality)
   734   apply (auto intro: finite_imp_foldSet
   735     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   736   done
   737 
   738 declare
   739   empty_foldSetE [rule del]  foldSet.intros [rule del]
   740   -- {* Delete rules to do with @{text foldSet} relation. *}
   741 
   742 text{* A simplified version for idempotent functions: *}
   743 
   744 lemma (in ACIf) fold_insert2:
   745 assumes finA: "finite A"
   746 shows "fold (op \<cdot>) g z (insert a A) = g a \<cdot> fold f g z A"
   747 proof cases
   748   assume "a \<in> A"
   749   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
   750     by(blast dest: mk_disjoint_insert)
   751   show ?thesis
   752   proof -
   753     from finA A have finB: "finite B" by(blast intro: finite_subset)
   754     have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
   755     also have "\<dots> = (g a) \<cdot> (fold f g z B)"
   756       using finB disj by(simp)
   757     also have "\<dots> = g a \<cdot> fold f g z A"
   758       using A finB disj by(simp add:idem assoc[symmetric])
   759     finally show ?thesis .
   760   qed
   761 next
   762   assume "a \<notin> A"
   763   with finA show ?thesis by simp
   764 qed
   765 
   766 lemma (in ACIf) foldI_conv_id:
   767   "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
   768 by(erule finite_induct)(simp_all add: fold_insert2 del: fold_insert)
   769 
   770 subsubsection{*Lemmas about @{text fold}*}
   771 
   772 lemma (in ACf) fold_commute:
   773   "finite A ==> (!!z. f (g x) (fold f g z A) = fold f g (f (g x) z) A)"
   774   apply (induct set: Finites, simp)
   775   apply (simp add: left_commute)
   776   done
   777 
   778 lemma (in ACf) fold_nest_Un_Int:
   779   "finite A ==> finite B
   780     ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
   781   apply (induct set: Finites, simp)
   782   apply (simp add: fold_commute Int_insert_left insert_absorb)
   783   done
   784 
   785 lemma (in ACf) fold_nest_Un_disjoint:
   786   "finite A ==> finite B ==> A Int B = {}
   787     ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
   788   by (simp add: fold_nest_Un_Int)
   789 
   790 lemma (in ACf) fold_reindex:
   791 assumes fin: "finite B"
   792 shows "inj_on h B \<Longrightarrow> fold f g z (h ` B) = fold f (g \<circ> h) z B"
   793 using fin apply (induct)
   794  apply simp
   795 apply simp
   796 done
   797 
   798 lemma (in ACe) fold_Un_Int:
   799   "finite A ==> finite B ==>
   800     fold f g e A \<cdot> fold f g e B =
   801     fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   802   apply (induct set: Finites, simp)
   803   apply (simp add: AC insert_absorb Int_insert_left)
   804   done
   805 
   806 corollary (in ACe) fold_Un_disjoint:
   807   "finite A ==> finite B ==> A Int B = {} ==>
   808     fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
   809   by (simp add: fold_Un_Int)
   810 
   811 lemma (in ACe) fold_UN_disjoint:
   812   "\<lbrakk> finite I; ALL i:I. finite (A i);
   813      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   814    \<Longrightarrow> fold f g e (UNION I A) =
   815        fold f (%i. fold f g e (A i)) e I"
   816   apply (induct set: Finites, simp, atomize)
   817   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   818    prefer 2 apply blast
   819   apply (subgoal_tac "A x Int UNION F A = {}")
   820    prefer 2 apply blast
   821   apply (simp add: fold_Un_disjoint)
   822   done
   823 
   824 lemma (in ACf) fold_cong:
   825   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
   826   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
   827    apply simp
   828   apply (erule finite_induct, simp)
   829   apply (simp add: subset_insert_iff, clarify)
   830   apply (subgoal_tac "finite C")
   831    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   832   apply (subgoal_tac "C = insert x (C - {x})")
   833    prefer 2 apply blast
   834   apply (erule ssubst)
   835   apply (drule spec)
   836   apply (erule (1) notE impE)
   837   apply (simp add: Ball_def del: insert_Diff_single)
   838   done
   839 
   840 lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   841   fold f (%x. fold f (g x) e (B x)) e A =
   842   fold f (split g) e (SIGMA x:A. B x)"
   843 apply (subst Sigma_def)
   844 apply (subst fold_UN_disjoint)
   845    apply assumption
   846   apply simp
   847  apply blast
   848 apply (erule fold_cong)
   849 apply (subst fold_UN_disjoint)
   850    apply simp
   851   apply simp
   852  apply blast
   853 apply (simp)
   854 done
   855 
   856 lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
   857    fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
   858 apply (erule finite_induct)
   859  apply simp
   860 apply (simp add:AC)
   861 done
   862 
   863 
   864 subsection {* Generalized summation over a set *}
   865 
   866 constdefs
   867   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   868   "setsum f A == if finite A then fold (op +) f 0 A else 0"
   869 
   870 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   871 written @{text"\<Sum>x\<in>A. e"}. *}
   872 
   873 syntax
   874   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   875 syntax (xsymbols)
   876   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   877 syntax (HTML output)
   878   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   879 
   880 translations -- {* Beware of argument permutation! *}
   881   "SUM i:A. b" == "setsum (%i. b) A"
   882   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
   883 
   884 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   885  @{text"\<Sum>x|P. e"}. *}
   886 
   887 syntax
   888   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   889 syntax (xsymbols)
   890   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   891 syntax (HTML output)
   892   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   893 
   894 translations
   895   "SUM x|P. t" => "setsum (%x. t) {x. P}"
   896   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   897 
   898 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
   899 
   900 syntax
   901   "_Setsum" :: "'a set => 'a::comm_monoid_mult"  ("\<Sum>_" [1000] 999)
   902 
   903 parse_translation {*
   904   let
   905     fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
   906   in [("_Setsum", Setsum_tr)] end;
   907 *}
   908 
   909 print_translation {*
   910 let
   911   fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
   912     | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   913        if x<>y then raise Match
   914        else let val x' = Syntax.mark_bound x
   915                 val t' = subst_bound(x',t)
   916                 val P' = subst_bound(x',P)
   917             in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
   918 in
   919 [("setsum", setsum_tr')]
   920 end
   921 *}
   922 
   923 lemma setsum_empty [simp]: "setsum f {} = 0"
   924   by (simp add: setsum_def)
   925 
   926 lemma setsum_insert [simp]:
   927     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   928   by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
   929 
   930 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   931   by (simp add: setsum_def)
   932 
   933 lemma setsum_reindex:
   934      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   935 by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
   936 
   937 lemma setsum_reindex_id:
   938      "inj_on f B ==> setsum f B = setsum id (f ` B)"
   939 by (auto simp add: setsum_reindex)
   940 
   941 lemma setsum_cong:
   942   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   943 by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
   944 
   945 lemma setsum_reindex_cong:
   946      "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
   947       ==> setsum h B = setsum g A"
   948   by (simp add: setsum_reindex cong: setsum_cong)
   949 
   950 lemma setsum_0: "setsum (%i. 0) A = 0"
   951 apply (clarsimp simp: setsum_def)
   952 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
   953 done
   954 
   955 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
   956   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
   957   apply (erule ssubst, rule setsum_0)
   958   apply (rule setsum_cong, auto)
   959   done
   960 
   961 lemma setsum_Un_Int: "finite A ==> finite B ==>
   962   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   963   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   964 by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
   965 
   966 lemma setsum_Un_disjoint: "finite A ==> finite B
   967   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   968 by (subst setsum_Un_Int [symmetric], auto)
   969 
   970 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   971   the lhs need not be, since UNION I A could still be finite.*)
   972 lemma setsum_UN_disjoint:
   973     "finite I ==> (ALL i:I. finite (A i)) ==>
   974         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   975       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   976 by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
   977 
   978 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   979 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   980 lemma setsum_Union_disjoint:
   981   "[| (ALL A:C. finite A);
   982       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   983    ==> setsum f (Union C) = setsum (setsum f) C"
   984 apply (cases "finite C") 
   985  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   986   apply (frule setsum_UN_disjoint [of C id f])
   987  apply (unfold Union_def id_def, assumption+)
   988 done
   989 
   990 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   991   the rhs need not be, since SIGMA A B could still be finite.*)
   992 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   993     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
   994     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   995 by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
   996 
   997 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   998 lemma setsum_cartesian_product: 
   999    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
  1000 apply (cases "finite A") 
  1001  apply (cases "finite B") 
  1002   apply (simp add: setsum_Sigma)
  1003  apply (cases "A={}", simp)
  1004  apply (simp add: setsum_0) 
  1005 apply (auto simp add: setsum_def
  1006             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1007 done
  1008 
  1009 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
  1010 by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
  1011 
  1012 
  1013 subsubsection {* Properties in more restricted classes of structures *}
  1014 
  1015 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
  1016   apply (case_tac "finite A")
  1017    prefer 2 apply (simp add: setsum_def)
  1018   apply (erule rev_mp)
  1019   apply (erule finite_induct, auto)
  1020   done
  1021 
  1022 lemma setsum_eq_0_iff [simp]:
  1023     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
  1024   by (induct set: Finites) auto
  1025 
  1026 lemma setsum_Un_nat: "finite A ==> finite B ==>
  1027     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
  1028   -- {* For the natural numbers, we have subtraction. *}
  1029   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
  1030 
  1031 lemma setsum_Un: "finite A ==> finite B ==>
  1032     (setsum f (A Un B) :: 'a :: ab_group_add) =
  1033       setsum f A + setsum f B - setsum f (A Int B)"
  1034   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
  1035 
  1036 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
  1037     (if a:A then setsum f A - f a else setsum f A)"
  1038   apply (case_tac "finite A")
  1039    prefer 2 apply (simp add: setsum_def)
  1040   apply (erule finite_induct)
  1041    apply (auto simp add: insert_Diff_if)
  1042   apply (drule_tac a = a in mk_disjoint_insert, auto)
  1043   done
  1044 
  1045 lemma setsum_diff1: "finite A \<Longrightarrow>
  1046   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1047   (if a:A then setsum f A - f a else setsum f A)"
  1048   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1049 
  1050 (* By Jeremy Siek: *)
  1051 
  1052 lemma setsum_diff_nat: 
  1053   assumes finB: "finite B"
  1054   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1055 using finB
  1056 proof (induct)
  1057   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1058 next
  1059   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1060     and xFinA: "insert x F \<subseteq> A"
  1061     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1062   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1063   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1064     by (simp add: setsum_diff1_nat)
  1065   from xFinA have "F \<subseteq> A" by simp
  1066   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1067   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1068     by simp
  1069   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1070   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1071     by simp
  1072   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1073   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1074     by simp
  1075   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1076 qed
  1077 
  1078 lemma setsum_diff:
  1079   assumes le: "finite A" "B \<subseteq> A"
  1080   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1081 proof -
  1082   from le have finiteB: "finite B" using finite_subset by auto
  1083   show ?thesis using finiteB le
  1084     proof (induct)
  1085       case empty
  1086       thus ?case by auto
  1087     next
  1088       case (insert x F)
  1089       thus ?case using le finiteB 
  1090 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1091     qed
  1092   qed
  1093 
  1094 lemma setsum_mono:
  1095   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1096   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1097 proof (cases "finite K")
  1098   case True
  1099   thus ?thesis using le
  1100   proof (induct)
  1101     case empty
  1102     thus ?case by simp
  1103   next
  1104     case insert
  1105     thus ?case using add_mono 
  1106       by force
  1107   qed
  1108 next
  1109   case False
  1110   thus ?thesis
  1111     by (simp add: setsum_def)
  1112 qed
  1113 
  1114 lemma setsum_mono2_nat:
  1115   assumes fin: "finite B" and sub: "A \<subseteq> B"
  1116 shows "setsum f A \<le> (setsum f B :: nat)"
  1117 proof -
  1118   have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
  1119   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1120     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1121   also have "A \<union> (B-A) = B" using sub by blast
  1122   finally show ?thesis .
  1123 qed
  1124 
  1125 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
  1126   - setsum f A"
  1127   by (induct set: Finites, auto)
  1128 
  1129 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1130   setsum f A - setsum g A"
  1131   by (simp add: diff_minus setsum_addf setsum_negf)
  1132 
  1133 lemma setsum_nonneg: "[| finite A;
  1134     \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
  1135     0 \<le> setsum f A";
  1136   apply (induct set: Finites, auto)
  1137   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1138   apply (blast intro: add_mono)
  1139   done
  1140 
  1141 lemma setsum_nonpos: "[| finite A;
  1142     \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
  1143     setsum f A \<le> 0";
  1144   apply (induct set: Finites, auto)
  1145   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1146   apply (blast intro: add_mono)
  1147   done
  1148 
  1149 lemma setsum_mult: 
  1150   fixes f :: "'a => ('b::semiring_0_cancel)"
  1151   shows "r * setsum f A = setsum (%n. r * f n) A"
  1152 proof (cases "finite A")
  1153   case True
  1154   thus ?thesis
  1155   proof (induct)
  1156     case empty thus ?case by simp
  1157   next
  1158     case (insert x A) thus ?case by (simp add: right_distrib)
  1159   qed
  1160 next
  1161   case False thus ?thesis by (simp add: setsum_def)
  1162 qed
  1163 
  1164 lemma setsum_abs: 
  1165   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1166   assumes fin: "finite A" 
  1167   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1168 using fin 
  1169 proof (induct) 
  1170   case empty thus ?case by simp
  1171 next
  1172   case (insert x A)
  1173   thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1174 qed
  1175 
  1176 lemma setsum_abs_ge_zero: 
  1177   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1178   assumes fin: "finite A" 
  1179   shows "0 \<le> setsum (%i. abs(f i)) A"
  1180 using fin 
  1181 proof (induct) 
  1182   case empty thus ?case by simp
  1183 next
  1184   case (insert x A) thus ?case by (auto intro: order_trans)
  1185 qed
  1186 
  1187 
  1188 subsection {* Generalized product over a set *}
  1189 
  1190 constdefs
  1191   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1192   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1193 
  1194 syntax
  1195   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
  1196 
  1197 syntax (xsymbols)
  1198   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1199 syntax (HTML output)
  1200   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1201 translations
  1202   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
  1203 
  1204 syntax
  1205   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1206 
  1207 parse_translation {*
  1208   let
  1209     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1210   in [("_Setprod", Setprod_tr)] end;
  1211 *}
  1212 print_translation {*
  1213 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1214     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1215 in
  1216 [("setprod", setprod_tr')]
  1217 end
  1218 *}
  1219 
  1220 
  1221 lemma setprod_empty [simp]: "setprod f {} = 1"
  1222   by (auto simp add: setprod_def)
  1223 
  1224 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1225     setprod f (insert a A) = f a * setprod f A"
  1226 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
  1227 
  1228 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1229   by (simp add: setprod_def)
  1230 
  1231 lemma setprod_reindex:
  1232      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1233 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
  1234 
  1235 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1236 by (auto simp add: setprod_reindex)
  1237 
  1238 lemma setprod_cong:
  1239   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1240 by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
  1241 
  1242 lemma setprod_reindex_cong: "inj_on f A ==>
  1243     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1244   by (frule setprod_reindex, simp)
  1245 
  1246 
  1247 lemma setprod_1: "setprod (%i. 1) A = 1"
  1248   apply (case_tac "finite A")
  1249   apply (erule finite_induct, auto simp add: mult_ac)
  1250   done
  1251 
  1252 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1253   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1254   apply (erule ssubst, rule setprod_1)
  1255   apply (rule setprod_cong, auto)
  1256   done
  1257 
  1258 lemma setprod_Un_Int: "finite A ==> finite B
  1259     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1260 by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
  1261 
  1262 lemma setprod_Un_disjoint: "finite A ==> finite B
  1263   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1264 by (subst setprod_Un_Int [symmetric], auto)
  1265 
  1266 lemma setprod_UN_disjoint:
  1267     "finite I ==> (ALL i:I. finite (A i)) ==>
  1268         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1269       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1270 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
  1271 
  1272 lemma setprod_Union_disjoint:
  1273   "[| (ALL A:C. finite A);
  1274       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1275    ==> setprod f (Union C) = setprod (setprod f) C"
  1276 apply (cases "finite C") 
  1277  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1278   apply (frule setprod_UN_disjoint [of C id f])
  1279  apply (unfold Union_def id_def, assumption+)
  1280 done
  1281 
  1282 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1283     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
  1284     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
  1285 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
  1286 
  1287 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1288 lemma setprod_cartesian_product: 
  1289      "(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))"
  1290 apply (cases "finite A") 
  1291  apply (cases "finite B") 
  1292   apply (simp add: setprod_Sigma)
  1293  apply (cases "A={}", simp)
  1294  apply (simp add: setprod_1) 
  1295 apply (auto simp add: setprod_def
  1296             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1297 done
  1298 
  1299 lemma setprod_timesf:
  1300      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1301 by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
  1302 
  1303 
  1304 subsubsection {* Properties in more restricted classes of structures *}
  1305 
  1306 lemma setprod_eq_1_iff [simp]:
  1307     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1308   by (induct set: Finites) auto
  1309 
  1310 lemma setprod_zero:
  1311      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1312   apply (induct set: Finites, force, clarsimp)
  1313   apply (erule disjE, auto)
  1314   done
  1315 
  1316 lemma setprod_nonneg [rule_format]:
  1317      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1318   apply (case_tac "finite A")
  1319   apply (induct set: Finites, force, clarsimp)
  1320   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1321   apply (rule mult_mono, assumption+)
  1322   apply (auto simp add: setprod_def)
  1323   done
  1324 
  1325 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1326      --> 0 < setprod f A"
  1327   apply (case_tac "finite A")
  1328   apply (induct set: Finites, force, clarsimp)
  1329   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1330   apply (rule mult_strict_mono, assumption+)
  1331   apply (auto simp add: setprod_def)
  1332   done
  1333 
  1334 lemma setprod_nonzero [rule_format]:
  1335     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1336       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1337   apply (erule finite_induct, auto)
  1338   done
  1339 
  1340 lemma setprod_zero_eq:
  1341     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1342      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1343   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1344   done
  1345 
  1346 lemma setprod_nonzero_field:
  1347     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1348   apply (rule setprod_nonzero, auto)
  1349   done
  1350 
  1351 lemma setprod_zero_eq_field:
  1352     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1353   apply (rule setprod_zero_eq, auto)
  1354   done
  1355 
  1356 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1357     (setprod f (A Un B) :: 'a ::{field})
  1358       = setprod f A * setprod f B / setprod f (A Int B)"
  1359   apply (subst setprod_Un_Int [symmetric], auto)
  1360   apply (subgoal_tac "finite (A Int B)")
  1361   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1362   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1363   done
  1364 
  1365 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1366     (setprod f (A - {a}) :: 'a :: {field}) =
  1367       (if a:A then setprod f A / f a else setprod f A)"
  1368   apply (erule finite_induct)
  1369    apply (auto simp add: insert_Diff_if)
  1370   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1371   apply (erule ssubst)
  1372   apply (subst times_divide_eq_right [THEN sym])
  1373   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1374   done
  1375 
  1376 lemma setprod_inversef: "finite A ==>
  1377     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1378       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1379   apply (erule finite_induct)
  1380   apply (simp, simp)
  1381   done
  1382 
  1383 lemma setprod_dividef:
  1384      "[|finite A;
  1385         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1386       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1387   apply (subgoal_tac
  1388          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1389   apply (erule ssubst)
  1390   apply (subst divide_inverse)
  1391   apply (subst setprod_timesf)
  1392   apply (subst setprod_inversef, assumption+, rule refl)
  1393   apply (rule setprod_cong, rule refl)
  1394   apply (subst divide_inverse, auto)
  1395   done
  1396 
  1397 subsection {* Finite cardinality *}
  1398 
  1399 text {* This definition, although traditional, is ugly to work with:
  1400 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1401 But now that we have @{text setsum} things are easy:
  1402 *}
  1403 
  1404 constdefs
  1405   card :: "'a set => nat"
  1406   "card A == setsum (%x. 1::nat) A"
  1407 
  1408 lemma card_empty [simp]: "card {} = 0"
  1409   by (simp add: card_def)
  1410 
  1411 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1412   by (simp add: card_def)
  1413 
  1414 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1415 by (simp add: card_def)
  1416 
  1417 lemma card_insert_disjoint [simp]:
  1418   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1419 by(simp add: card_def ACf.fold_insert[OF ACf_add])
  1420 
  1421 lemma card_insert_if:
  1422     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1423   by (simp add: insert_absorb)
  1424 
  1425 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1426   apply auto
  1427   apply (drule_tac a = x in mk_disjoint_insert, clarify)
  1428   apply (auto)
  1429   done
  1430 
  1431 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1432 by auto
  1433 
  1434 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1435 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1436 apply(simp del:insert_Diff_single)
  1437 done
  1438 
  1439 lemma card_Diff_singleton:
  1440     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1441   by (simp add: card_Suc_Diff1 [symmetric])
  1442 
  1443 lemma card_Diff_singleton_if:
  1444     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1445   by (simp add: card_Diff_singleton)
  1446 
  1447 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1448   by (simp add: card_insert_if card_Suc_Diff1)
  1449 
  1450 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1451   by (simp add: card_insert_if)
  1452 
  1453 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1454 by (simp add: card_def setsum_mono2_nat)
  1455 
  1456 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1457   apply (induct set: Finites, simp, clarify)
  1458   apply (subgoal_tac "finite A & A - {x} <= F")
  1459    prefer 2 apply (blast intro: finite_subset, atomize)
  1460   apply (drule_tac x = "A - {x}" in spec)
  1461   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1462   apply (case_tac "card A", auto)
  1463   done
  1464 
  1465 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1466   apply (simp add: psubset_def linorder_not_le [symmetric])
  1467   apply (blast dest: card_seteq)
  1468   done
  1469 
  1470 lemma card_Un_Int: "finite A ==> finite B
  1471     ==> card A + card B = card (A Un B) + card (A Int B)"
  1472 by(simp add:card_def setsum_Un_Int)
  1473 
  1474 lemma card_Un_disjoint: "finite A ==> finite B
  1475     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1476   by (simp add: card_Un_Int)
  1477 
  1478 lemma card_Diff_subset:
  1479   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1480 by(simp add:card_def setsum_diff_nat)
  1481 
  1482 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1483   apply (rule Suc_less_SucD)
  1484   apply (simp add: card_Suc_Diff1)
  1485   done
  1486 
  1487 lemma card_Diff2_less:
  1488     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1489   apply (case_tac "x = y")
  1490    apply (simp add: card_Diff1_less)
  1491   apply (rule less_trans)
  1492    prefer 2 apply (auto intro!: card_Diff1_less)
  1493   done
  1494 
  1495 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1496   apply (case_tac "x : A")
  1497    apply (simp_all add: card_Diff1_less less_imp_le)
  1498   done
  1499 
  1500 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1501 by (erule psubsetI, blast)
  1502 
  1503 lemma insert_partition:
  1504   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1505   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1506 by auto
  1507 
  1508 (* main cardinality theorem *)
  1509 lemma card_partition [rule_format]:
  1510      "finite C ==>  
  1511         finite (\<Union> C) -->  
  1512         (\<forall>c\<in>C. card c = k) -->   
  1513         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1514         k * card(C) = card (\<Union> C)"
  1515 apply (erule finite_induct, simp)
  1516 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1517        finite_subset [of _ "\<Union> (insert x F)"])
  1518 done
  1519 
  1520 
  1521 lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
  1522   -- {* Generalized to any @{text comm_semiring_1_cancel} in
  1523         @{text IntDef} as @{text setsum_constant}. *}
  1524 apply (cases "finite A") 
  1525 apply (erule finite_induct, auto)
  1526 done
  1527 
  1528 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
  1529   apply (erule finite_induct)
  1530   apply (auto simp add: power_Suc)
  1531   done
  1532 
  1533 
  1534 subsubsection {* Cardinality of unions *}
  1535 
  1536 lemma card_UN_disjoint:
  1537     "finite I ==> (ALL i:I. finite (A i)) ==>
  1538         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1539       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1540   apply (simp add: card_def)
  1541   apply (subgoal_tac
  1542            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1543   apply (simp add: setsum_UN_disjoint)
  1544   apply (simp add: setsum_constant_nat cong: setsum_cong)
  1545   done
  1546 
  1547 lemma card_Union_disjoint:
  1548   "finite C ==> (ALL A:C. finite A) ==>
  1549         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1550       card (Union C) = setsum card C"
  1551   apply (frule card_UN_disjoint [of C id])
  1552   apply (unfold Union_def id_def, assumption+)
  1553   done
  1554 
  1555 subsubsection {* Cardinality of image *}
  1556 
  1557 text{*The image of a finite set can be expressed using @{term fold}.*}
  1558 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1559   apply (erule finite_induct, simp)
  1560   apply (subst ACf.fold_insert) 
  1561   apply (auto simp add: ACf_def) 
  1562   done
  1563 
  1564 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1565   apply (induct set: Finites, simp)
  1566   apply (simp add: le_SucI finite_imageI card_insert_if)
  1567   done
  1568 
  1569 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1570 by(simp add:card_def setsum_reindex o_def)
  1571 
  1572 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1573   by (simp add: card_seteq card_image)
  1574 
  1575 lemma eq_card_imp_inj_on:
  1576   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1577 apply(induct rule:finite_induct)
  1578  apply simp
  1579 apply(frule card_image_le[where f = f])
  1580 apply(simp add:card_insert_if split:if_splits)
  1581 done
  1582 
  1583 lemma inj_on_iff_eq_card:
  1584   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1585 by(blast intro: card_image eq_card_imp_inj_on)
  1586 
  1587 
  1588 lemma card_inj_on_le:
  1589     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1590 apply (subgoal_tac "finite A") 
  1591  apply (force intro: card_mono simp add: card_image [symmetric])
  1592 apply (blast intro: finite_imageD dest: finite_subset) 
  1593 done
  1594 
  1595 lemma card_bij_eq:
  1596     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1597        finite A; finite B |] ==> card A = card B"
  1598   by (auto intro: le_anti_sym card_inj_on_le)
  1599 
  1600 
  1601 subsubsection {* Cardinality of products *}
  1602 
  1603 (*
  1604 lemma SigmaI_insert: "y \<notin> A ==>
  1605   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1606   by auto
  1607 *)
  1608 
  1609 lemma card_SigmaI [simp]:
  1610   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1611   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1612 by(simp add:card_def setsum_Sigma)
  1613 
  1614 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1615 apply (cases "finite A") 
  1616 apply (cases "finite B") 
  1617   apply (simp add: setsum_constant_nat) 
  1618 apply (auto simp add: card_eq_0_iff
  1619             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1620 done
  1621 
  1622 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1623 by (simp add: card_cartesian_product) 
  1624 
  1625 
  1626 
  1627 subsubsection {* Cardinality of the Powerset *}
  1628 
  1629 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1630   apply (induct set: Finites)
  1631    apply (simp_all add: Pow_insert)
  1632   apply (subst card_Un_disjoint, blast)
  1633     apply (blast intro: finite_imageI, blast)
  1634   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1635    apply (simp add: card_image Pow_insert)
  1636   apply (unfold inj_on_def)
  1637   apply (blast elim!: equalityE)
  1638   done
  1639 
  1640 text {* Relates to equivalence classes.  Based on a theorem of
  1641 F. Kammüller's.  *}
  1642 
  1643 lemma dvd_partition:
  1644   "finite (Union C) ==>
  1645     ALL c : C. k dvd card c ==>
  1646     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1647   k dvd card (Union C)"
  1648 apply(frule finite_UnionD)
  1649 apply(rotate_tac -1)
  1650   apply (induct set: Finites, simp_all, clarify)
  1651   apply (subst card_Un_disjoint)
  1652   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1653   done
  1654 
  1655 
  1656 subsubsection {* Theorems about @{text "choose"} *}
  1657 
  1658 text {*
  1659   \medskip Basic theorem about @{text "choose"}.  By Florian
  1660   Kamm\"uller, tidied by LCP.
  1661 *}
  1662 
  1663 lemma card_s_0_eq_empty:
  1664     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  1665   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  1666   apply (simp cong add: rev_conj_cong)
  1667   done
  1668 
  1669 lemma choose_deconstruct: "finite M ==> x \<notin> M
  1670   ==> {s. s <= insert x M & card(s) = Suc k}
  1671        = {s. s <= M & card(s) = Suc k} Un
  1672          {s. EX t. t <= M & card(t) = k & s = insert x t}"
  1673   apply safe
  1674    apply (auto intro: finite_subset [THEN card_insert_disjoint])
  1675   apply (drule_tac x = "xa - {x}" in spec)
  1676   apply (subgoal_tac "x \<notin> xa", auto)
  1677   apply (erule rev_mp, subst card_Diff_singleton)
  1678   apply (auto intro: finite_subset)
  1679   done
  1680 
  1681 text{*There are as many subsets of @{term A} having cardinality @{term k}
  1682  as there are sets obtained from the former by inserting a fixed element
  1683  @{term x} into each.*}
  1684 lemma constr_bij:
  1685    "[|finite A; x \<notin> A|] ==>
  1686     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  1687     card {B. B <= A & card(B) = k}"
  1688   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  1689        apply (auto elim!: equalityE simp add: inj_on_def)
  1690     apply (subst Diff_insert0, auto)
  1691    txt {* finiteness of the two sets *}
  1692    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  1693    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  1694    apply fast+
  1695   done
  1696 
  1697 text {*
  1698   Main theorem: combinatorial statement about number of subsets of a set.
  1699 *}
  1700 
  1701 lemma n_sub_lemma:
  1702   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1703   apply (induct k)
  1704    apply (simp add: card_s_0_eq_empty, atomize)
  1705   apply (rotate_tac -1, erule finite_induct)
  1706    apply (simp_all (no_asm_simp) cong add: conj_cong
  1707      add: card_s_0_eq_empty choose_deconstruct)
  1708   apply (subst card_Un_disjoint)
  1709      prefer 4 apply (force simp add: constr_bij)
  1710     prefer 3 apply force
  1711    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1712      finite_subset [of _ "Pow (insert x F)", standard])
  1713   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1714   done
  1715 
  1716 theorem n_subsets:
  1717     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1718   by (simp add: n_sub_lemma)
  1719 
  1720 
  1721 subsection{* A fold functional for non-empty sets *}
  1722 
  1723 text{* Does not require start value. *}
  1724 
  1725 consts
  1726   foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1727 
  1728 inductive "foldSet1 f"
  1729 intros
  1730 foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f"
  1731 foldSet1_insertI [intro]:
  1732  "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
  1733   \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
  1734 
  1735 constdefs
  1736   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1737   "fold1 f A == THE x. (A, x) : foldSet1 f"
  1738 
  1739 lemma foldSet1_nonempty:
  1740  "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
  1741 by(erule foldSet1.cases, simp_all) 
  1742 
  1743 
  1744 inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
  1745 
  1746 lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
  1747 apply(rule iffI)
  1748  prefer 2 apply fast
  1749 apply (erule foldSet1.cases)
  1750  apply blast
  1751 apply (erule foldSet1.cases)
  1752  apply blast
  1753 apply blast
  1754 done
  1755 
  1756 lemma Diff1_foldSet1:
  1757   "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
  1758 by (erule insert_Diff [THEN subst], rule foldSet1.intros,
  1759     auto dest!:foldSet1_nonempty)
  1760 
  1761 lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A"
  1762   by (induct set: foldSet1) auto
  1763 
  1764 lemma finite_nonempty_imp_foldSet1:
  1765   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
  1766   by (induct set: Finites) auto
  1767 
  1768 lemma (in ACf) foldSet1_determ_aux:
  1769   "!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x"
  1770 proof (induct n)
  1771   case 0 thus ?case by simp
  1772 next
  1773   case (Suc n)
  1774   have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk>
  1775            \<Longrightarrow> y = x" and card: "card A < Suc n"
  1776   and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" .
  1777   from card have "card A < n \<or> card A = n" by arith
  1778   thus ?case
  1779   proof
  1780     assume less: "card A < n"
  1781     show ?thesis by(rule IH[OF less Afoldx Afoldy])
  1782   next
  1783     assume cardA: "card A = n"
  1784     show ?thesis
  1785     proof (rule foldSet1.cases[OF Afoldx])
  1786       fix a assume "(A, x) = ({a}, a)"
  1787       thus "y = x" using Afoldy by (simp add:foldSet1_sing)
  1788     next
  1789       fix Ax ax x'
  1790       assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')"
  1791 	and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax"
  1792 	and Axnon: "Ax \<noteq> {}"
  1793       hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto
  1794       show ?thesis
  1795       proof (rule foldSet1.cases[OF Afoldy])
  1796 	fix ay assume "(A, y) = ({ay}, ay)"
  1797 	thus ?thesis using eq1 x' Axnon notinx
  1798 	  by (fastsimp simp:foldSet1_sing)
  1799       next
  1800 	fix Ay ay y'
  1801 	assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')"
  1802 	  and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay"
  1803 	  and Aynon: "Ay \<noteq> {}"
  1804 	hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto
  1805 	have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx])
  1806 	with cardA A1 notinx have less: "card Ax < n" by simp
  1807 	show ?thesis
  1808 	proof cases
  1809 	  assume "ax = ay"
  1810 	  then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto
  1811 	  ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto
  1812 	next
  1813 	  assume diff: "ax \<noteq> ay"
  1814 	  let ?B = "Ax - {ay}"
  1815 	  have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B"
  1816 	    using A1 A2 notinx notiny diff by(blast elim!:equalityE)+
  1817 	  show ?thesis
  1818 	  proof cases
  1819 	    assume "?B = {}"
  1820 	    with Ax Ay show ?thesis using x' y' x y by(simp add:commute)
  1821 	  next
  1822 	    assume Bnon: "?B \<noteq> {}"
  1823 	    moreover have "finite ?B" using finA A1 by simp
  1824 	    ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f"
  1825 	      using finite_nonempty_imp_foldSet1 by(blast)
  1826 	    moreover have ayinAx: "ay \<in> Ax" using Ax by(auto)
  1827 	    ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1)
  1828 	    hence "ay\<cdot>b = x'" by(rule IH[OF less x'])
  1829             moreover have "ax\<cdot>b = y'"
  1830 	    proof (rule IH[OF _ y'])
  1831 	      show "card Ay < n" using Ay cardA A1 notinx finA ayinAx
  1832 		by(auto simp:card_Diff1_less)
  1833 	    next
  1834 	      show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon
  1835 		by fastsimp
  1836 	    qed
  1837 	    ultimately show ?thesis using x y by(auto simp:AC)
  1838 	  qed
  1839 	qed
  1840       qed
  1841     qed
  1842   qed
  1843 qed
  1844 
  1845 
  1846 lemma (in ACf) foldSet1_determ:
  1847   "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
  1848 by (blast intro: foldSet1_determ_aux [rule_format])
  1849 
  1850 lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
  1851   by (unfold fold1_def) (blast intro: foldSet1_determ)
  1852 
  1853 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1854   by (unfold fold1_def) blast
  1855 
  1856 lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> 
  1857     ((insert x A, v) : foldSet1 f) =
  1858     (EX y. (A, y) : foldSet1 f & v = f x y)"
  1859 apply auto
  1860 apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
  1861   apply (fastsimp dest: foldSet1_imp_finite)
  1862  apply blast
  1863 apply (blast intro: foldSet1_determ)
  1864 done
  1865 
  1866 lemma (in ACf) fold1_insert:
  1867   "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
  1868 apply (unfold fold1_def)
  1869 apply (simp add: foldSet1_insert_aux)
  1870 apply (rule the_equality)
  1871 apply (auto intro: finite_nonempty_imp_foldSet1
  1872     cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality)
  1873 done
  1874 
  1875 lemma (in ACIf) fold1_insert2[simp]:
  1876 assumes finA: "finite A" and nonA: "A \<noteq> {}"
  1877 shows "fold1 f (insert a A) = f a (fold1 f A)"
  1878 proof cases
  1879   assume "a \<in> A"
  1880   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
  1881     by(blast dest: mk_disjoint_insert)
  1882   show ?thesis
  1883   proof cases
  1884     assume "B = {}"
  1885     thus ?thesis using A by(simp add:idem fold1_singleton)
  1886   next
  1887     assume nonB: "B \<noteq> {}"
  1888     from finA A have finB: "finite B" by(blast intro: finite_subset)
  1889     have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
  1890     also have "\<dots> = f a (fold1 f B)"
  1891       using finB nonB disj by(simp add: fold1_insert)
  1892     also have "\<dots> = f a (fold1 f A)"
  1893       using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric])
  1894     finally show ?thesis .
  1895   qed
  1896 next
  1897   assume "a \<notin> A"
  1898   with finA nonA show ?thesis by(simp add:fold1_insert)
  1899 qed
  1900 
  1901 text{* Now the recursion rules for definitions: *}
  1902 
  1903 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1904 by(simp add:fold1_singleton)
  1905 
  1906 lemma (in ACf) fold1_insert_def:
  1907   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1908 by(simp add:fold1_insert)
  1909 
  1910 lemma (in ACIf) fold1_insert2_def:
  1911   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1912 by(simp add:fold1_insert2)
  1913 
  1914 
  1915 subsubsection{* Lemmas about {@text fold1} *}
  1916 
  1917 lemma (in ACf) fold1_Un:
  1918 assumes A: "finite A" "A \<noteq> {}"
  1919 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  1920        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1921 using A
  1922 proof(induct rule:finite_ne_induct)
  1923   case singleton thus ?case by(simp add:fold1_insert)
  1924 next
  1925   case insert thus ?case by (simp add:fold1_insert assoc)
  1926 qed
  1927 
  1928 lemma (in ACIf) fold1_Un2:
  1929 assumes A: "finite A" "A \<noteq> {}"
  1930 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  1931        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1932 using A
  1933 proof(induct rule:finite_ne_induct)
  1934   case singleton thus ?case by(simp add:fold1_insert2)
  1935 next
  1936   case insert thus ?case by (simp add:fold1_insert2 assoc)
  1937 qed
  1938 
  1939 lemma (in ACf) fold1_in:
  1940   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  1941   shows "fold1 f A \<in> A"
  1942 using A
  1943 proof (induct rule:finite_ne_induct)
  1944   case singleton thus ?case by(simp)
  1945 next
  1946   case insert thus ?case using elem by (force simp add:fold1_insert)
  1947 qed
  1948 
  1949 lemma fold1_le:
  1950   assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1951   and A: "finite (A)" "A \<noteq> {}" and le: "\<And>x y. f x y \<le> x"
  1952   shows "a \<in> A \<Longrightarrow> fold1 f A \<le> a"
  1953 using A
  1954 proof (induct rule:finite_ne_induct)
  1955   case singleton thus ?case by(simp)
  1956 next
  1957   from le have le2: "\<And>x y. f x y \<le> y" by (fastsimp simp:ACf.commute[OF ACf])
  1958   case (insert x F) thus ?case using le le2
  1959     by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: le order_trans)
  1960 qed
  1961 
  1962 lemma fold1_ge:
  1963   assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1964   and A: "finite (A)" "A \<noteq> {}" and ge: "\<And>x y. x \<le> f x y"
  1965   shows "a \<in> A \<Longrightarrow> a \<le> fold1 f A"
  1966 using A
  1967 proof (induct rule:finite_ne_induct)
  1968   case singleton thus ?case by(simp)
  1969 next
  1970   from ge have ge2: "\<And>x y. y \<le> f x y" by (fastsimp simp:ACf.commute[OF ACf])
  1971   case (insert x F) thus ?case using ge ge2
  1972     by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: ge order_trans)
  1973 qed
  1974 
  1975 
  1976 subsection{*Min and Max*}
  1977 
  1978 text{* As an application of @{text fold1} we define the minimal and
  1979 maximal element of a (non-empty) set over a linear order. First we
  1980 show that @{text min} and @{text max} are ACI: *}
  1981 
  1982 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1983 apply(rule ACf.intro)
  1984 apply(auto simp:min_def)
  1985 done
  1986 
  1987 lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1988 apply(rule ACIf.intro[OF ACf_min])
  1989 apply(rule ACIf_axioms.intro)
  1990 apply(auto simp:min_def)
  1991 done
  1992 
  1993 lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1994 apply(rule ACf.intro)
  1995 apply(auto simp:max_def)
  1996 done
  1997 
  1998 lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1999 apply(rule ACIf.intro[OF ACf_max])
  2000 apply(rule ACIf_axioms.intro)
  2001 apply(auto simp:max_def)
  2002 done
  2003 
  2004 text{* Now we make the definitions: *}
  2005 
  2006 constdefs
  2007   Min :: "('a::linorder)set => 'a"
  2008   "Min  ==  fold1 min"
  2009 
  2010   Max :: "('a::linorder)set => 'a"
  2011   "Max  ==  fold1 max"
  2012 
  2013 text{* Now we instantiate the recursion equations and declare them
  2014 simplification rules: *}
  2015 
  2016 declare
  2017   fold1_singleton_def[OF Min_def, simp]
  2018   ACIf.fold1_insert2_def[OF ACIf_min Min_def, simp]
  2019   fold1_singleton_def[OF Max_def, simp]
  2020   ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp]
  2021 
  2022 text{* Now we instantiate some @{text fold1} properties: *}
  2023 
  2024 lemma Min_in [simp]:
  2025   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2026 using ACf.fold1_in[OF ACf_min]
  2027 by(fastsimp simp: Min_def min_def)
  2028 
  2029 lemma Max_in [simp]:
  2030   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2031 using ACf.fold1_in[OF ACf_max]
  2032 by(fastsimp simp: Max_def max_def)
  2033 
  2034 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2035 by(simp add: Min_def fold1_le[OF ACf_min] min_le_iff_disj)
  2036 
  2037 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2038 by(simp add: Max_def fold1_ge[OF ACf_max] le_max_iff_disj)
  2039 
  2040 end