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