src/HOL/Finite_Set.thy
author paulson
Wed Feb 02 18:06:00 2005 +0100 (2005-02-02)
changeset 15487 55497029b255
parent 15484 2636ec211ec8
child 15497 53bca254719a
permissions -rw-r--r--
generalization and tidying
     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       --{*@{term h} is not injective, so the cardinality has not increased*}
   576     hence card': "A = h ` {i. i < n}"
   577       using card by (auto simp:image_def less_Suc_eq)
   578     show ?thesis by(rule IH[OF card' Afoldx Afoldy])
   579   next
   580     assume new: "\<not>(EX k<n. h n = h k)"
   581     show ?thesis
   582     proof (rule foldSet.cases[OF Afoldx])
   583       assume "(A, x) = ({}, z)"  --{*fold of a singleton set*}
   584       thus "x' = x" using Afoldy by (auto)
   585     next
   586       fix B b y
   587       assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   588 	and y: "(B,y) \<in> foldSet f g z" and notinB: "b \<notin> B"
   589       hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   590       show ?thesis
   591       proof (rule foldSet.cases[OF Afoldy])
   592 	assume "(A,x') = ({}, z)"
   593 	thus ?thesis using A1 by auto
   594       next
   595 	fix C c r
   596 	assume eq2: "(A,x') = (insert c C, g c \<cdot> r)"
   597 	  and r: "(C,r) \<in> foldSet f g z" and notinC: "c \<notin> C"
   598 	hence A2: "A = insert c C" and x': "x' = g c \<cdot> r" by auto
   599 	obtain hB where lessB: "B = hB ` {i. i<n}"
   600 	  using card_lemma[OF A1 notinB card new] by auto
   601 	obtain hC where lessC: "C = hC ` {i. i<n}"
   602 	  using card_lemma[OF A2 notinC card new] by auto
   603 	show ?thesis
   604 	proof cases
   605 	  assume "b = c"
   606 	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   607 	  ultimately show ?thesis using IH[OF lessB] y r x x' by auto
   608 	next
   609 	  assume diff: "b \<noteq> c"
   610 	  let ?D = "B - {c}"
   611 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   612 	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   613 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   614 	  with A1 have "finite ?D" by simp
   615 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
   616 	    using finite_imp_foldSet by rules
   617 	  moreover have cinB: "c \<in> B" using B by(auto)
   618 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   619 	    by(rule Diff1_foldSet)
   620 	  hence "g c \<cdot> d = y" by(rule IH[OF lessB y])
   621           moreover have "g b \<cdot> d = r"
   622 	  proof (rule IH[OF lessC r])
   623 	    show "(C,g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   624 	      by fastsimp
   625 	  qed
   626 	  ultimately show ?thesis using x x' by(auto simp:AC)
   627 	qed
   628       qed
   629     qed
   630   qed
   631 qed
   632 
   633 (* The same proof, but using card 
   634 lemma (in ACf) foldSet_determ_aux:
   635   "!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
   636    \<Longrightarrow> x' = x"
   637 proof (induct n)
   638   case 0 thus ?case by simp
   639 next
   640   case (Suc n)
   641   have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
   642            \<Longrightarrow> x' = x" and card: "card A < Suc n"
   643   and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
   644   from card have "card A < n \<or> card A = n" by arith
   645   thus ?case
   646   proof
   647     assume less: "card A < n"
   648     show ?thesis by(rule IH[OF less Afoldx Afoldy])
   649   next
   650     assume cardA: "card A = n"
   651     show ?thesis
   652     proof (rule foldSet.cases[OF Afoldx])
   653       assume "(A, x) = ({}, e)"
   654       thus "x' = x" using Afoldy by (auto)
   655     next
   656       fix B b y
   657       assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   658 	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
   659       hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   660       show ?thesis
   661       proof (rule foldSet.cases[OF Afoldy])
   662 	assume "(A,x') = ({}, e)"
   663 	thus ?thesis using A1 by auto
   664       next
   665 	fix C c z
   666 	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
   667 	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
   668 	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
   669 	have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   670 	with cardA A1 notinB have less: "card B < n" by simp
   671 	show ?thesis
   672 	proof cases
   673 	  assume "b = c"
   674 	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   675 	  ultimately show ?thesis using IH[OF less] y z x x' by auto
   676 	next
   677 	  assume diff: "b \<noteq> c"
   678 	  let ?D = "B - {c}"
   679 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   680 	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   681 	  have "finite ?D" using finA A1 by simp
   682 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
   683 	    using finite_imp_foldSet by rules
   684 	  moreover have cinB: "c \<in> B" using B by(auto)
   685 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
   686 	    by(rule Diff1_foldSet)
   687 	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
   688           moreover have "g b \<cdot> d = z"
   689 	  proof (rule IH[OF _ z])
   690 	    show "card C < n" using C cardA A1 notinB finA cinB
   691 	      by(auto simp:card_Diff1_less)
   692 	  next
   693 	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
   694 	      by fastsimp
   695 	  qed
   696 	  ultimately show ?thesis using x x' by(auto simp:AC)
   697 	qed
   698       qed
   699     qed
   700   qed
   701 qed
   702 *)
   703 
   704 lemma (in ACf) foldSet_determ:
   705   "(A, x) : foldSet f g z ==> (A, y) : foldSet f g z ==> y = x"
   706 apply(frule foldSet_imp_finite)
   707 apply(simp add:finite_conv_nat_seg_image)
   708 apply(blast intro: foldSet_determ_aux [rule_format])
   709 done
   710 
   711 lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
   712   by (unfold fold_def) (blast intro: foldSet_determ)
   713 
   714 text{* The base case for @{text fold}: *}
   715 
   716 lemma fold_empty [simp]: "fold f g z {} = z"
   717   by (unfold fold_def) blast
   718 
   719 lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   720     ((insert x A, v) : foldSet f g z) =
   721     (EX y. (A, y) : foldSet f g z & v = f (g x) y)"
   722   apply auto
   723   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   724    apply (fastsimp dest: foldSet_imp_finite)
   725   apply (blast intro: foldSet_determ)
   726   done
   727 
   728 text{* The recursion equation for @{text fold}: *}
   729 
   730 lemma (in ACf) fold_insert[simp]:
   731     "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
   732   apply (unfold fold_def)
   733   apply (simp add: fold_insert_aux)
   734   apply (rule the_equality)
   735   apply (auto intro: finite_imp_foldSet
   736     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   737   done
   738 
   739 declare
   740   empty_foldSetE [rule del]  foldSet.intros [rule del]
   741   -- {* Delete rules to do with @{text foldSet} relation. *}
   742 
   743 text{* A simplified version for idempotent functions: *}
   744 
   745 lemma (in ACIf) fold_insert2:
   746 assumes finA: "finite A"
   747 shows "fold (op \<cdot>) g z (insert a A) = g a \<cdot> fold f g z A"
   748 proof cases
   749   assume "a \<in> A"
   750   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
   751     by(blast dest: mk_disjoint_insert)
   752   show ?thesis
   753   proof -
   754     from finA A have finB: "finite B" by(blast intro: finite_subset)
   755     have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
   756     also have "\<dots> = (g a) \<cdot> (fold f g z B)"
   757       using finB disj by(simp)
   758     also have "\<dots> = g a \<cdot> fold f g z A"
   759       using A finB disj by(simp add:idem assoc[symmetric])
   760     finally show ?thesis .
   761   qed
   762 next
   763   assume "a \<notin> A"
   764   with finA show ?thesis by simp
   765 qed
   766 
   767 lemma (in ACIf) foldI_conv_id:
   768   "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
   769 by(erule finite_induct)(simp_all add: fold_insert2 del: fold_insert)
   770 
   771 subsubsection{*Lemmas about @{text fold}*}
   772 
   773 lemma (in ACf) fold_commute:
   774   "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
   775   apply (induct set: Finites, simp)
   776   apply (simp add: left_commute [of x])
   777   done
   778 
   779 lemma (in ACf) fold_nest_Un_Int:
   780   "finite A ==> finite B
   781     ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
   782   apply (induct set: Finites, simp)
   783   apply (simp add: fold_commute Int_insert_left insert_absorb)
   784   done
   785 
   786 lemma (in ACf) fold_nest_Un_disjoint:
   787   "finite A ==> finite B ==> A Int B = {}
   788     ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
   789   by (simp add: fold_nest_Un_Int)
   790 
   791 lemma (in ACf) fold_reindex:
   792 assumes fin: "finite A"
   793 shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
   794 using fin apply (induct)
   795  apply simp
   796 apply simp
   797 done
   798 
   799 lemma (in ACe) fold_Un_Int:
   800   "finite A ==> finite B ==>
   801     fold f g e A \<cdot> fold f g e B =
   802     fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   803   apply (induct set: Finites, simp)
   804   apply (simp add: AC insert_absorb Int_insert_left)
   805   done
   806 
   807 corollary (in ACe) fold_Un_disjoint:
   808   "finite A ==> finite B ==> A Int B = {} ==>
   809     fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
   810   by (simp add: fold_Un_Int)
   811 
   812 lemma (in ACe) fold_UN_disjoint:
   813   "\<lbrakk> finite I; ALL i:I. finite (A i);
   814      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   815    \<Longrightarrow> fold f g e (UNION I A) =
   816        fold f (%i. fold f g e (A i)) e I"
   817   apply (induct set: Finites, simp, atomize)
   818   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   819    prefer 2 apply blast
   820   apply (subgoal_tac "A x Int UNION F A = {}")
   821    prefer 2 apply blast
   822   apply (simp add: fold_Un_disjoint)
   823   done
   824 
   825 lemma (in ACf) fold_cong:
   826   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
   827   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
   828    apply simp
   829   apply (erule finite_induct, simp)
   830   apply (simp add: subset_insert_iff, clarify)
   831   apply (subgoal_tac "finite C")
   832    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   833   apply (subgoal_tac "C = insert x (C - {x})")
   834    prefer 2 apply blast
   835   apply (erule ssubst)
   836   apply (drule spec)
   837   apply (erule (1) notE impE)
   838   apply (simp add: Ball_def del: insert_Diff_single)
   839   done
   840 
   841 lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   842   fold f (%x. fold f (g x) e (B x)) e A =
   843   fold f (split g) e (SIGMA x:A. B x)"
   844 apply (subst Sigma_def)
   845 apply (subst fold_UN_disjoint)
   846    apply assumption
   847   apply simp
   848  apply blast
   849 apply (erule fold_cong)
   850 apply (subst fold_UN_disjoint)
   851    apply simp
   852   apply simp
   853  apply blast
   854 apply (simp)
   855 done
   856 
   857 lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
   858    fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
   859 apply (erule finite_induct)
   860  apply simp
   861 apply (simp add:AC)
   862 done
   863 
   864 
   865 subsection {* Generalized summation over a set *}
   866 
   867 constdefs
   868   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   869   "setsum f A == if finite A then fold (op +) f 0 A else 0"
   870 
   871 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   872 written @{text"\<Sum>x\<in>A. e"}. *}
   873 
   874 syntax
   875   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   876 syntax (xsymbols)
   877   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   878 syntax (HTML output)
   879   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   880 
   881 translations -- {* Beware of argument permutation! *}
   882   "SUM i:A. b" == "setsum (%i. b) A"
   883   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
   884 
   885 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   886  @{text"\<Sum>x|P. e"}. *}
   887 
   888 syntax
   889   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   890 syntax (xsymbols)
   891   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   892 syntax (HTML output)
   893   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   894 
   895 translations
   896   "SUM x|P. t" => "setsum (%x. t) {x. P}"
   897   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   898 
   899 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
   900 
   901 syntax
   902   "_Setsum" :: "'a set => 'a::comm_monoid_mult"  ("\<Sum>_" [1000] 999)
   903 
   904 parse_translation {*
   905   let
   906     fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
   907   in [("_Setsum", Setsum_tr)] end;
   908 *}
   909 
   910 print_translation {*
   911 let
   912   fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
   913     | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   914        if x<>y then raise Match
   915        else let val x' = Syntax.mark_bound x
   916                 val t' = subst_bound(x',t)
   917                 val P' = subst_bound(x',P)
   918             in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
   919 in
   920 [("setsum", setsum_tr')]
   921 end
   922 *}
   923 
   924 lemma setsum_empty [simp]: "setsum f {} = 0"
   925   by (simp add: setsum_def)
   926 
   927 lemma setsum_insert [simp]:
   928     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   929   by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
   930 
   931 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   932   by (simp add: setsum_def)
   933 
   934 lemma setsum_reindex:
   935      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   936 by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
   937 
   938 lemma setsum_reindex_id:
   939      "inj_on f B ==> setsum f B = setsum id (f ` B)"
   940 by (auto simp add: setsum_reindex)
   941 
   942 lemma setsum_cong:
   943   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   944 by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
   945 
   946 lemma setsum_reindex_cong:
   947      "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
   948       ==> setsum h B = setsum g A"
   949   by (simp add: setsum_reindex cong: setsum_cong)
   950 
   951 lemma setsum_0: "setsum (%i. 0) A = 0"
   952 apply (clarsimp simp: setsum_def)
   953 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
   954 done
   955 
   956 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
   957   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
   958   apply (erule ssubst, rule setsum_0)
   959   apply (rule setsum_cong, auto)
   960   done
   961 
   962 lemma setsum_Un_Int: "finite A ==> finite B ==>
   963   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   964   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   965 by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
   966 
   967 lemma setsum_Un_disjoint: "finite A ==> finite B
   968   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   969 by (subst setsum_Un_Int [symmetric], auto)
   970 
   971 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   972   the lhs need not be, since UNION I A could still be finite.*)
   973 lemma setsum_UN_disjoint:
   974     "finite I ==> (ALL i:I. finite (A i)) ==>
   975         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   976       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   977 by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
   978 
   979 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   980 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   981 lemma setsum_Union_disjoint:
   982   "[| (ALL A:C. finite A);
   983       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   984    ==> setsum f (Union C) = setsum (setsum f) C"
   985 apply (cases "finite C") 
   986  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   987   apply (frule setsum_UN_disjoint [of C id f])
   988  apply (unfold Union_def id_def, assumption+)
   989 done
   990 
   991 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   992   the rhs need not be, since SIGMA A B could still be finite.*)
   993 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   994     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
   995     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   996 by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
   997 
   998 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   999 lemma setsum_cartesian_product: 
  1000    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
  1001 apply (cases "finite A") 
  1002  apply (cases "finite B") 
  1003   apply (simp add: setsum_Sigma)
  1004  apply (cases "A={}", simp)
  1005  apply (simp add: setsum_0) 
  1006 apply (auto simp add: setsum_def
  1007             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1008 done
  1009 
  1010 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
  1011 by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
  1012 
  1013 
  1014 subsubsection {* Properties in more restricted classes of structures *}
  1015 
  1016 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
  1017   apply (case_tac "finite A")
  1018    prefer 2 apply (simp add: setsum_def)
  1019   apply (erule rev_mp)
  1020   apply (erule finite_induct, auto)
  1021   done
  1022 
  1023 lemma setsum_eq_0_iff [simp]:
  1024     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
  1025   by (induct set: Finites) auto
  1026 
  1027 lemma setsum_Un_nat: "finite A ==> finite B ==>
  1028     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
  1029   -- {* For the natural numbers, we have subtraction. *}
  1030   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
  1031 
  1032 lemma setsum_Un: "finite A ==> finite B ==>
  1033     (setsum f (A Un B) :: 'a :: ab_group_add) =
  1034       setsum f A + setsum f B - setsum f (A Int B)"
  1035   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
  1036 
  1037 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
  1038     (if a:A then setsum f A - f a else setsum f A)"
  1039   apply (case_tac "finite A")
  1040    prefer 2 apply (simp add: setsum_def)
  1041   apply (erule finite_induct)
  1042    apply (auto simp add: insert_Diff_if)
  1043   apply (drule_tac a = a in mk_disjoint_insert, auto)
  1044   done
  1045 
  1046 lemma setsum_diff1: "finite A \<Longrightarrow>
  1047   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1048   (if a:A then setsum f A - f a else setsum f A)"
  1049   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1050 
  1051 (* By Jeremy Siek: *)
  1052 
  1053 lemma setsum_diff_nat: 
  1054   assumes finB: "finite B"
  1055   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1056 using finB
  1057 proof (induct)
  1058   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1059 next
  1060   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1061     and xFinA: "insert x F \<subseteq> A"
  1062     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1063   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1064   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1065     by (simp add: setsum_diff1_nat)
  1066   from xFinA have "F \<subseteq> A" by simp
  1067   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1068   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1069     by simp
  1070   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1071   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1072     by simp
  1073   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1074   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1075     by simp
  1076   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1077 qed
  1078 
  1079 lemma setsum_diff:
  1080   assumes le: "finite A" "B \<subseteq> A"
  1081   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1082 proof -
  1083   from le have finiteB: "finite B" using finite_subset by auto
  1084   show ?thesis using finiteB le
  1085     proof (induct)
  1086       case empty
  1087       thus ?case by auto
  1088     next
  1089       case (insert x F)
  1090       thus ?case using le finiteB 
  1091 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1092     qed
  1093   qed
  1094 
  1095 lemma setsum_mono:
  1096   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1097   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1098 proof (cases "finite K")
  1099   case True
  1100   thus ?thesis using le
  1101   proof (induct)
  1102     case empty
  1103     thus ?case by simp
  1104   next
  1105     case insert
  1106     thus ?case using add_mono 
  1107       by force
  1108   qed
  1109 next
  1110   case False
  1111   thus ?thesis
  1112     by (simp add: setsum_def)
  1113 qed
  1114 
  1115 lemma setsum_mono2_nat:
  1116   assumes fin: "finite B" and sub: "A \<subseteq> B"
  1117 shows "setsum f A \<le> (setsum f B :: nat)"
  1118 proof -
  1119   have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
  1120   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1121     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1122   also have "A \<union> (B-A) = B" using sub by blast
  1123   finally show ?thesis .
  1124 qed
  1125 
  1126 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
  1127   - setsum f A"
  1128   by (induct set: Finites, auto)
  1129 
  1130 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1131   setsum f A - setsum g A"
  1132   by (simp add: diff_minus setsum_addf setsum_negf)
  1133 
  1134 lemma setsum_nonneg: "[| finite A;
  1135     \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
  1136     0 \<le> setsum f A";
  1137   apply (induct set: Finites, auto)
  1138   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1139   apply (blast intro: add_mono)
  1140   done
  1141 
  1142 lemma setsum_nonpos: "[| finite A;
  1143     \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
  1144     setsum f A \<le> 0";
  1145   apply (induct set: Finites, auto)
  1146   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1147   apply (blast intro: add_mono)
  1148   done
  1149 
  1150 lemma setsum_mult: 
  1151   fixes f :: "'a => ('b::semiring_0_cancel)"
  1152   shows "r * setsum f A = setsum (%n. r * f n) A"
  1153 proof (cases "finite A")
  1154   case True
  1155   thus ?thesis
  1156   proof (induct)
  1157     case empty thus ?case by simp
  1158   next
  1159     case (insert x A) thus ?case by (simp add: right_distrib)
  1160   qed
  1161 next
  1162   case False thus ?thesis by (simp add: setsum_def)
  1163 qed
  1164 
  1165 lemma setsum_abs: 
  1166   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1167   assumes fin: "finite A" 
  1168   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1169 using fin 
  1170 proof (induct) 
  1171   case empty thus ?case by simp
  1172 next
  1173   case (insert x A)
  1174   thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1175 qed
  1176 
  1177 lemma setsum_abs_ge_zero: 
  1178   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1179   assumes fin: "finite A" 
  1180   shows "0 \<le> setsum (%i. abs(f i)) A"
  1181 using fin 
  1182 proof (induct) 
  1183   case empty thus ?case by simp
  1184 next
  1185   case (insert x A) thus ?case by (auto intro: order_trans)
  1186 qed
  1187 
  1188 
  1189 subsection {* Generalized product over a set *}
  1190 
  1191 constdefs
  1192   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1193   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1194 
  1195 syntax
  1196   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
  1197 
  1198 syntax (xsymbols)
  1199   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1200 syntax (HTML output)
  1201   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1202 translations
  1203   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
  1204 
  1205 syntax
  1206   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1207 
  1208 parse_translation {*
  1209   let
  1210     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1211   in [("_Setprod", Setprod_tr)] end;
  1212 *}
  1213 print_translation {*
  1214 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1215     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1216 in
  1217 [("setprod", setprod_tr')]
  1218 end
  1219 *}
  1220 
  1221 
  1222 lemma setprod_empty [simp]: "setprod f {} = 1"
  1223   by (auto simp add: setprod_def)
  1224 
  1225 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1226     setprod f (insert a A) = f a * setprod f A"
  1227 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
  1228 
  1229 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1230   by (simp add: setprod_def)
  1231 
  1232 lemma setprod_reindex:
  1233      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1234 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
  1235 
  1236 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1237 by (auto simp add: setprod_reindex)
  1238 
  1239 lemma setprod_cong:
  1240   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1241 by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
  1242 
  1243 lemma setprod_reindex_cong: "inj_on f A ==>
  1244     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1245   by (frule setprod_reindex, simp)
  1246 
  1247 
  1248 lemma setprod_1: "setprod (%i. 1) A = 1"
  1249   apply (case_tac "finite A")
  1250   apply (erule finite_induct, auto simp add: mult_ac)
  1251   done
  1252 
  1253 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1254   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1255   apply (erule ssubst, rule setprod_1)
  1256   apply (rule setprod_cong, auto)
  1257   done
  1258 
  1259 lemma setprod_Un_Int: "finite A ==> finite B
  1260     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1261 by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
  1262 
  1263 lemma setprod_Un_disjoint: "finite A ==> finite B
  1264   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1265 by (subst setprod_Un_Int [symmetric], auto)
  1266 
  1267 lemma setprod_UN_disjoint:
  1268     "finite I ==> (ALL i:I. finite (A i)) ==>
  1269         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1270       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1271 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
  1272 
  1273 lemma setprod_Union_disjoint:
  1274   "[| (ALL A:C. finite A);
  1275       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1276    ==> setprod f (Union C) = setprod (setprod f) C"
  1277 apply (cases "finite C") 
  1278  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1279   apply (frule setprod_UN_disjoint [of C id f])
  1280  apply (unfold Union_def id_def, assumption+)
  1281 done
  1282 
  1283 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1284     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
  1285     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
  1286 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
  1287 
  1288 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1289 lemma setprod_cartesian_product: 
  1290      "(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))"
  1291 apply (cases "finite A") 
  1292  apply (cases "finite B") 
  1293   apply (simp add: setprod_Sigma)
  1294  apply (cases "A={}", simp)
  1295  apply (simp add: setprod_1) 
  1296 apply (auto simp add: setprod_def
  1297             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1298 done
  1299 
  1300 lemma setprod_timesf:
  1301      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1302 by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
  1303 
  1304 
  1305 subsubsection {* Properties in more restricted classes of structures *}
  1306 
  1307 lemma setprod_eq_1_iff [simp]:
  1308     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1309   by (induct set: Finites) auto
  1310 
  1311 lemma setprod_zero:
  1312      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1313   apply (induct set: Finites, force, clarsimp)
  1314   apply (erule disjE, auto)
  1315   done
  1316 
  1317 lemma setprod_nonneg [rule_format]:
  1318      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1319   apply (case_tac "finite A")
  1320   apply (induct set: Finites, force, clarsimp)
  1321   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1322   apply (rule mult_mono, assumption+)
  1323   apply (auto simp add: setprod_def)
  1324   done
  1325 
  1326 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1327      --> 0 < setprod f A"
  1328   apply (case_tac "finite A")
  1329   apply (induct set: Finites, force, clarsimp)
  1330   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1331   apply (rule mult_strict_mono, assumption+)
  1332   apply (auto simp add: setprod_def)
  1333   done
  1334 
  1335 lemma setprod_nonzero [rule_format]:
  1336     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1337       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1338   apply (erule finite_induct, auto)
  1339   done
  1340 
  1341 lemma setprod_zero_eq:
  1342     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1343      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1344   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1345   done
  1346 
  1347 lemma setprod_nonzero_field:
  1348     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1349   apply (rule setprod_nonzero, auto)
  1350   done
  1351 
  1352 lemma setprod_zero_eq_field:
  1353     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1354   apply (rule setprod_zero_eq, auto)
  1355   done
  1356 
  1357 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1358     (setprod f (A Un B) :: 'a ::{field})
  1359       = setprod f A * setprod f B / setprod f (A Int B)"
  1360   apply (subst setprod_Un_Int [symmetric], auto)
  1361   apply (subgoal_tac "finite (A Int B)")
  1362   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1363   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1364   done
  1365 
  1366 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1367     (setprod f (A - {a}) :: 'a :: {field}) =
  1368       (if a:A then setprod f A / f a else setprod f A)"
  1369   apply (erule finite_induct)
  1370    apply (auto simp add: insert_Diff_if)
  1371   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1372   apply (erule ssubst)
  1373   apply (subst times_divide_eq_right [THEN sym])
  1374   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1375   done
  1376 
  1377 lemma setprod_inversef: "finite A ==>
  1378     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1379       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1380   apply (erule finite_induct)
  1381   apply (simp, simp)
  1382   done
  1383 
  1384 lemma setprod_dividef:
  1385      "[|finite A;
  1386         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1387       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1388   apply (subgoal_tac
  1389          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1390   apply (erule ssubst)
  1391   apply (subst divide_inverse)
  1392   apply (subst setprod_timesf)
  1393   apply (subst setprod_inversef, assumption+, rule refl)
  1394   apply (rule setprod_cong, rule refl)
  1395   apply (subst divide_inverse, auto)
  1396   done
  1397 
  1398 subsection {* Finite cardinality *}
  1399 
  1400 text {* This definition, although traditional, is ugly to work with:
  1401 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1402 But now that we have @{text setsum} things are easy:
  1403 *}
  1404 
  1405 constdefs
  1406   card :: "'a set => nat"
  1407   "card A == setsum (%x. 1::nat) A"
  1408 
  1409 lemma card_empty [simp]: "card {} = 0"
  1410   by (simp add: card_def)
  1411 
  1412 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1413   by (simp add: card_def)
  1414 
  1415 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1416 by (simp add: card_def)
  1417 
  1418 lemma card_insert_disjoint [simp]:
  1419   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1420 by(simp add: card_def ACf.fold_insert[OF ACf_add])
  1421 
  1422 lemma card_insert_if:
  1423     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1424   by (simp add: insert_absorb)
  1425 
  1426 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1427   apply auto
  1428   apply (drule_tac a = x in mk_disjoint_insert, clarify)
  1429   apply (auto)
  1430   done
  1431 
  1432 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1433 by auto
  1434 
  1435 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1436 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1437 apply(simp del:insert_Diff_single)
  1438 done
  1439 
  1440 lemma card_Diff_singleton:
  1441     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1442   by (simp add: card_Suc_Diff1 [symmetric])
  1443 
  1444 lemma card_Diff_singleton_if:
  1445     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1446   by (simp add: card_Diff_singleton)
  1447 
  1448 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1449   by (simp add: card_insert_if card_Suc_Diff1)
  1450 
  1451 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1452   by (simp add: card_insert_if)
  1453 
  1454 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1455 by (simp add: card_def setsum_mono2_nat)
  1456 
  1457 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1458   apply (induct set: Finites, simp, clarify)
  1459   apply (subgoal_tac "finite A & A - {x} <= F")
  1460    prefer 2 apply (blast intro: finite_subset, atomize)
  1461   apply (drule_tac x = "A - {x}" in spec)
  1462   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1463   apply (case_tac "card A", auto)
  1464   done
  1465 
  1466 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1467   apply (simp add: psubset_def linorder_not_le [symmetric])
  1468   apply (blast dest: card_seteq)
  1469   done
  1470 
  1471 lemma card_Un_Int: "finite A ==> finite B
  1472     ==> card A + card B = card (A Un B) + card (A Int B)"
  1473 by(simp add:card_def setsum_Un_Int)
  1474 
  1475 lemma card_Un_disjoint: "finite A ==> finite B
  1476     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1477   by (simp add: card_Un_Int)
  1478 
  1479 lemma card_Diff_subset:
  1480   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1481 by(simp add:card_def setsum_diff_nat)
  1482 
  1483 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1484   apply (rule Suc_less_SucD)
  1485   apply (simp add: card_Suc_Diff1)
  1486   done
  1487 
  1488 lemma card_Diff2_less:
  1489     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1490   apply (case_tac "x = y")
  1491    apply (simp add: card_Diff1_less)
  1492   apply (rule less_trans)
  1493    prefer 2 apply (auto intro!: card_Diff1_less)
  1494   done
  1495 
  1496 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1497   apply (case_tac "x : A")
  1498    apply (simp_all add: card_Diff1_less less_imp_le)
  1499   done
  1500 
  1501 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1502 by (erule psubsetI, blast)
  1503 
  1504 lemma insert_partition:
  1505   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1506   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1507 by auto
  1508 
  1509 (* main cardinality theorem *)
  1510 lemma card_partition [rule_format]:
  1511      "finite C ==>  
  1512         finite (\<Union> C) -->  
  1513         (\<forall>c\<in>C. card c = k) -->   
  1514         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1515         k * card(C) = card (\<Union> C)"
  1516 apply (erule finite_induct, simp)
  1517 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1518        finite_subset [of _ "\<Union> (insert x F)"])
  1519 done
  1520 
  1521 
  1522 lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
  1523   -- {* Generalized to any @{text comm_semiring_1_cancel} in
  1524         @{text IntDef} as @{text setsum_constant}. *}
  1525 apply (cases "finite A") 
  1526 apply (erule finite_induct, auto)
  1527 done
  1528 
  1529 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
  1530   apply (erule finite_induct)
  1531   apply (auto simp add: power_Suc)
  1532   done
  1533 
  1534 
  1535 subsubsection {* Cardinality of unions *}
  1536 
  1537 lemma card_UN_disjoint:
  1538     "finite I ==> (ALL i:I. finite (A i)) ==>
  1539         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1540       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1541   apply (simp add: card_def)
  1542   apply (subgoal_tac
  1543            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1544   apply (simp add: setsum_UN_disjoint)
  1545   apply (simp add: setsum_constant_nat cong: setsum_cong)
  1546   done
  1547 
  1548 lemma card_Union_disjoint:
  1549   "finite C ==> (ALL A:C. finite A) ==>
  1550         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1551       card (Union C) = setsum card C"
  1552   apply (frule card_UN_disjoint [of C id])
  1553   apply (unfold Union_def id_def, assumption+)
  1554   done
  1555 
  1556 subsubsection {* Cardinality of image *}
  1557 
  1558 text{*The image of a finite set can be expressed using @{term fold}.*}
  1559 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1560   apply (erule finite_induct, simp)
  1561   apply (subst ACf.fold_insert) 
  1562   apply (auto simp add: ACf_def) 
  1563   done
  1564 
  1565 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1566   apply (induct set: Finites, simp)
  1567   apply (simp add: le_SucI finite_imageI card_insert_if)
  1568   done
  1569 
  1570 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1571 by(simp add:card_def setsum_reindex o_def)
  1572 
  1573 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1574   by (simp add: card_seteq card_image)
  1575 
  1576 lemma eq_card_imp_inj_on:
  1577   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1578 apply(induct rule:finite_induct)
  1579  apply simp
  1580 apply(frule card_image_le[where f = f])
  1581 apply(simp add:card_insert_if split:if_splits)
  1582 done
  1583 
  1584 lemma inj_on_iff_eq_card:
  1585   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1586 by(blast intro: card_image eq_card_imp_inj_on)
  1587 
  1588 
  1589 lemma card_inj_on_le:
  1590     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1591 apply (subgoal_tac "finite A") 
  1592  apply (force intro: card_mono simp add: card_image [symmetric])
  1593 apply (blast intro: finite_imageD dest: finite_subset) 
  1594 done
  1595 
  1596 lemma card_bij_eq:
  1597     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1598        finite A; finite B |] ==> card A = card B"
  1599   by (auto intro: le_anti_sym card_inj_on_le)
  1600 
  1601 
  1602 subsubsection {* Cardinality of products *}
  1603 
  1604 (*
  1605 lemma SigmaI_insert: "y \<notin> A ==>
  1606   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1607   by auto
  1608 *)
  1609 
  1610 lemma card_SigmaI [simp]:
  1611   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1612   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1613 by(simp add:card_def setsum_Sigma)
  1614 
  1615 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1616 apply (cases "finite A") 
  1617 apply (cases "finite B") 
  1618   apply (simp add: setsum_constant_nat) 
  1619 apply (auto simp add: card_eq_0_iff
  1620             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1621 done
  1622 
  1623 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1624 by (simp add: card_cartesian_product) 
  1625 
  1626 
  1627 
  1628 subsubsection {* Cardinality of the Powerset *}
  1629 
  1630 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1631   apply (induct set: Finites)
  1632    apply (simp_all add: Pow_insert)
  1633   apply (subst card_Un_disjoint, blast)
  1634     apply (blast intro: finite_imageI, blast)
  1635   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1636    apply (simp add: card_image Pow_insert)
  1637   apply (unfold inj_on_def)
  1638   apply (blast elim!: equalityE)
  1639   done
  1640 
  1641 text {* Relates to equivalence classes.  Based on a theorem of
  1642 F. Kammüller's.  *}
  1643 
  1644 lemma dvd_partition:
  1645   "finite (Union C) ==>
  1646     ALL c : C. k dvd card c ==>
  1647     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1648   k dvd card (Union C)"
  1649 apply(frule finite_UnionD)
  1650 apply(rotate_tac -1)
  1651   apply (induct set: Finites, simp_all, clarify)
  1652   apply (subst card_Un_disjoint)
  1653   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1654   done
  1655 
  1656 
  1657 subsubsection {* Theorems about @{text "choose"} *}
  1658 
  1659 text {*
  1660   \medskip Basic theorem about @{text "choose"}.  By Florian
  1661   Kamm\"uller, tidied by LCP.
  1662 *}
  1663 
  1664 lemma card_s_0_eq_empty:
  1665     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  1666   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  1667   apply (simp cong add: rev_conj_cong)
  1668   done
  1669 
  1670 lemma choose_deconstruct: "finite M ==> x \<notin> M
  1671   ==> {s. s <= insert x M & card(s) = Suc k}
  1672        = {s. s <= M & card(s) = Suc k} Un
  1673          {s. EX t. t <= M & card(t) = k & s = insert x t}"
  1674   apply safe
  1675    apply (auto intro: finite_subset [THEN card_insert_disjoint])
  1676   apply (drule_tac x = "xa - {x}" in spec)
  1677   apply (subgoal_tac "x \<notin> xa", auto)
  1678   apply (erule rev_mp, subst card_Diff_singleton)
  1679   apply (auto intro: finite_subset)
  1680   done
  1681 
  1682 text{*There are as many subsets of @{term A} having cardinality @{term k}
  1683  as there are sets obtained from the former by inserting a fixed element
  1684  @{term x} into each.*}
  1685 lemma constr_bij:
  1686    "[|finite A; x \<notin> A|] ==>
  1687     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  1688     card {B. B <= A & card(B) = k}"
  1689   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  1690        apply (auto elim!: equalityE simp add: inj_on_def)
  1691     apply (subst Diff_insert0, auto)
  1692    txt {* finiteness of the two sets *}
  1693    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  1694    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  1695    apply fast+
  1696   done
  1697 
  1698 text {*
  1699   Main theorem: combinatorial statement about number of subsets of a set.
  1700 *}
  1701 
  1702 lemma n_sub_lemma:
  1703   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1704   apply (induct k)
  1705    apply (simp add: card_s_0_eq_empty, atomize)
  1706   apply (rotate_tac -1, erule finite_induct)
  1707    apply (simp_all (no_asm_simp) cong add: conj_cong
  1708      add: card_s_0_eq_empty choose_deconstruct)
  1709   apply (subst card_Un_disjoint)
  1710      prefer 4 apply (force simp add: constr_bij)
  1711     prefer 3 apply force
  1712    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1713      finite_subset [of _ "Pow (insert x F)", standard])
  1714   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1715   done
  1716 
  1717 theorem n_subsets:
  1718     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1719   by (simp add: n_sub_lemma)
  1720 
  1721 
  1722 subsection{* A fold functional for non-empty sets *}
  1723 
  1724 text{* Does not require start value. *}
  1725 
  1726 consts
  1727   foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1728 
  1729 inductive "foldSet1 f"
  1730 intros
  1731 foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f"
  1732 foldSet1_insertI [intro]:
  1733  "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
  1734   \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
  1735 
  1736 constdefs
  1737   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1738   "fold1 f A == THE x. (A, x) : foldSet1 f"
  1739 
  1740 lemma foldSet1_nonempty:
  1741  "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
  1742 by(erule foldSet1.cases, simp_all) 
  1743 
  1744 
  1745 inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
  1746 
  1747 lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
  1748 apply(rule iffI)
  1749  prefer 2 apply fast
  1750 apply (erule foldSet1.cases)
  1751  apply blast
  1752 apply (erule foldSet1.cases)
  1753  apply blast
  1754 apply blast
  1755 done
  1756 
  1757 lemma Diff1_foldSet1:
  1758   "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
  1759 by (erule insert_Diff [THEN subst], rule foldSet1.intros,
  1760     auto dest!:foldSet1_nonempty)
  1761 
  1762 lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A"
  1763   by (induct set: foldSet1) auto
  1764 
  1765 lemma finite_nonempty_imp_foldSet1:
  1766   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
  1767   by (induct set: Finites) auto
  1768 
  1769 lemma (in ACf) foldSet1_determ_aux:
  1770   "!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x"
  1771 proof (induct n)
  1772   case 0 thus ?case by simp
  1773 next
  1774   case (Suc n)
  1775   have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk>
  1776            \<Longrightarrow> y = x" and card: "card A < Suc n"
  1777   and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" .
  1778   from card have "card A < n \<or> card A = n" by arith
  1779   thus ?case
  1780   proof
  1781     assume less: "card A < n"
  1782     show ?thesis by(rule IH[OF less Afoldx Afoldy])
  1783   next
  1784     assume cardA: "card A = n"
  1785     show ?thesis
  1786     proof (rule foldSet1.cases[OF Afoldx])
  1787       fix a assume "(A, x) = ({a}, a)"
  1788       thus "y = x" using Afoldy by (simp add:foldSet1_sing)
  1789     next
  1790       fix Ax ax x'
  1791       assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')"
  1792 	and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax"
  1793 	and Axnon: "Ax \<noteq> {}"
  1794       hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto
  1795       show ?thesis
  1796       proof (rule foldSet1.cases[OF Afoldy])
  1797 	fix ay assume "(A, y) = ({ay}, ay)"
  1798 	thus ?thesis using eq1 x' Axnon notinx
  1799 	  by (fastsimp simp:foldSet1_sing)
  1800       next
  1801 	fix Ay ay y'
  1802 	assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')"
  1803 	  and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay"
  1804 	  and Aynon: "Ay \<noteq> {}"
  1805 	hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto
  1806 	have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx])
  1807 	with cardA A1 notinx have less: "card Ax < n" by simp
  1808 	show ?thesis
  1809 	proof cases
  1810 	  assume "ax = ay"
  1811 	  then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto
  1812 	  ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto
  1813 	next
  1814 	  assume diff: "ax \<noteq> ay"
  1815 	  let ?B = "Ax - {ay}"
  1816 	  have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B"
  1817 	    using A1 A2 notinx notiny diff by(blast elim!:equalityE)+
  1818 	  show ?thesis
  1819 	  proof cases
  1820 	    assume "?B = {}"
  1821 	    with Ax Ay show ?thesis using x' y' x y by(simp add:commute)
  1822 	  next
  1823 	    assume Bnon: "?B \<noteq> {}"
  1824 	    moreover have "finite ?B" using finA A1 by simp
  1825 	    ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f"
  1826 	      using finite_nonempty_imp_foldSet1 by(blast)
  1827 	    moreover have ayinAx: "ay \<in> Ax" using Ax by(auto)
  1828 	    ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1)
  1829 	    hence "ay\<cdot>b = x'" by(rule IH[OF less x'])
  1830             moreover have "ax\<cdot>b = y'"
  1831 	    proof (rule IH[OF _ y'])
  1832 	      show "card Ay < n" using Ay cardA A1 notinx finA ayinAx
  1833 		by(auto simp:card_Diff1_less)
  1834 	    next
  1835 	      show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon
  1836 		by fastsimp
  1837 	    qed
  1838 	    ultimately show ?thesis using x y by(auto simp:AC)
  1839 	  qed
  1840 	qed
  1841       qed
  1842     qed
  1843   qed
  1844 qed
  1845 
  1846 
  1847 lemma (in ACf) foldSet1_determ:
  1848   "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
  1849 by (blast intro: foldSet1_determ_aux [rule_format])
  1850 
  1851 lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
  1852   by (unfold fold1_def) (blast intro: foldSet1_determ)
  1853 
  1854 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1855   by (unfold fold1_def) blast
  1856 
  1857 lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> 
  1858     ((insert x A, v) : foldSet1 f) =
  1859     (EX y. (A, y) : foldSet1 f & v = f x y)"
  1860 apply auto
  1861 apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
  1862   apply (fastsimp dest: foldSet1_imp_finite)
  1863  apply blast
  1864 apply (blast intro: foldSet1_determ)
  1865 done
  1866 
  1867 lemma (in ACf) fold1_insert:
  1868   "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
  1869 apply (unfold fold1_def)
  1870 apply (simp add: foldSet1_insert_aux)
  1871 apply (rule the_equality)
  1872 apply (auto intro: finite_nonempty_imp_foldSet1
  1873     cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality)
  1874 done
  1875 
  1876 lemma (in ACIf) fold1_insert2[simp]:
  1877 assumes finA: "finite A" and nonA: "A \<noteq> {}"
  1878 shows "fold1 f (insert a A) = f a (fold1 f A)"
  1879 proof cases
  1880   assume "a \<in> A"
  1881   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
  1882     by(blast dest: mk_disjoint_insert)
  1883   show ?thesis
  1884   proof cases
  1885     assume "B = {}"
  1886     thus ?thesis using A by(simp add:idem fold1_singleton)
  1887   next
  1888     assume nonB: "B \<noteq> {}"
  1889     from finA A have finB: "finite B" by(blast intro: finite_subset)
  1890     have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
  1891     also have "\<dots> = f a (fold1 f B)"
  1892       using finB nonB disj by(simp add: fold1_insert)
  1893     also have "\<dots> = f a (fold1 f A)"
  1894       using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric])
  1895     finally show ?thesis .
  1896   qed
  1897 next
  1898   assume "a \<notin> A"
  1899   with finA nonA show ?thesis by(simp add:fold1_insert)
  1900 qed
  1901 
  1902 text{* Now the recursion rules for definitions: *}
  1903 
  1904 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1905 by(simp add:fold1_singleton)
  1906 
  1907 lemma (in ACf) fold1_insert_def:
  1908   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1909 by(simp add:fold1_insert)
  1910 
  1911 lemma (in ACIf) fold1_insert2_def:
  1912   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1913 by(simp add:fold1_insert2)
  1914 
  1915 
  1916 subsubsection{* Lemmas about {@text fold1} *}
  1917 
  1918 lemma (in ACf) fold1_Un:
  1919 assumes A: "finite A" "A \<noteq> {}"
  1920 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  1921        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1922 using A
  1923 proof(induct rule:finite_ne_induct)
  1924   case singleton thus ?case by(simp add:fold1_insert)
  1925 next
  1926   case insert thus ?case by (simp add:fold1_insert assoc)
  1927 qed
  1928 
  1929 lemma (in ACIf) fold1_Un2:
  1930 assumes A: "finite A" "A \<noteq> {}"
  1931 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  1932        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1933 using A
  1934 proof(induct rule:finite_ne_induct)
  1935   case singleton thus ?case by(simp add:fold1_insert2)
  1936 next
  1937   case insert thus ?case by (simp add:fold1_insert2 assoc)
  1938 qed
  1939 
  1940 lemma (in ACf) fold1_in:
  1941   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  1942   shows "fold1 f A \<in> A"
  1943 using A
  1944 proof (induct rule:finite_ne_induct)
  1945   case singleton thus ?case by(simp)
  1946 next
  1947   case insert thus ?case using elem by (force simp add:fold1_insert)
  1948 qed
  1949 
  1950 lemma fold1_le:
  1951   assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1952   and A: "finite (A)" "A \<noteq> {}" and le: "\<And>x y. f x y \<le> x"
  1953   shows "a \<in> A \<Longrightarrow> fold1 f A \<le> a"
  1954 using A
  1955 proof (induct rule:finite_ne_induct)
  1956   case singleton thus ?case by(simp)
  1957 next
  1958   from le have le2: "\<And>x y. f x y \<le> y" by (fastsimp simp:ACf.commute[OF ACf])
  1959   case (insert x F) thus ?case using le le2
  1960     by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: le order_trans)
  1961 qed
  1962 
  1963 lemma fold1_ge:
  1964   assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1965   and A: "finite (A)" "A \<noteq> {}" and ge: "\<And>x y. x \<le> f x y"
  1966   shows "a \<in> A \<Longrightarrow> a \<le> fold1 f A"
  1967 using A
  1968 proof (induct rule:finite_ne_induct)
  1969   case singleton thus ?case by(simp)
  1970 next
  1971   from ge have ge2: "\<And>x y. y \<le> f x y" by (fastsimp simp:ACf.commute[OF ACf])
  1972   case (insert x F) thus ?case using ge ge2
  1973     by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: ge order_trans)
  1974 qed
  1975 
  1976 
  1977 subsection{*Min and Max*}
  1978 
  1979 text{* As an application of @{text fold1} we define the minimal and
  1980 maximal element of a (non-empty) set over a linear order. First we
  1981 show that @{text min} and @{text max} are ACI: *}
  1982 
  1983 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1984 apply(rule ACf.intro)
  1985 apply(auto simp:min_def)
  1986 done
  1987 
  1988 lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1989 apply(rule ACIf.intro[OF ACf_min])
  1990 apply(rule ACIf_axioms.intro)
  1991 apply(auto simp:min_def)
  1992 done
  1993 
  1994 lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  1995 apply(rule ACf.intro)
  1996 apply(auto simp:max_def)
  1997 done
  1998 
  1999 lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2000 apply(rule ACIf.intro[OF ACf_max])
  2001 apply(rule ACIf_axioms.intro)
  2002 apply(auto simp:max_def)
  2003 done
  2004 
  2005 text{* Now we make the definitions: *}
  2006 
  2007 constdefs
  2008   Min :: "('a::linorder)set => 'a"
  2009   "Min  ==  fold1 min"
  2010 
  2011   Max :: "('a::linorder)set => 'a"
  2012   "Max  ==  fold1 max"
  2013 
  2014 text{* Now we instantiate the recursion equations and declare them
  2015 simplification rules: *}
  2016 
  2017 declare
  2018   fold1_singleton_def[OF Min_def, simp]
  2019   ACIf.fold1_insert2_def[OF ACIf_min Min_def, simp]
  2020   fold1_singleton_def[OF Max_def, simp]
  2021   ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp]
  2022 
  2023 text{* Now we instantiate some @{text fold1} properties: *}
  2024 
  2025 lemma Min_in [simp]:
  2026   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2027 using ACf.fold1_in[OF ACf_min]
  2028 by(fastsimp simp: Min_def min_def)
  2029 
  2030 lemma Max_in [simp]:
  2031   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2032 using ACf.fold1_in[OF ACf_max]
  2033 by(fastsimp simp: Max_def max_def)
  2034 
  2035 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2036 by(simp add: Min_def fold1_le[OF ACf_min] min_le_iff_disj)
  2037 
  2038 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2039 by(simp add: Max_def fold1_ge[OF ACf_max] le_max_iff_disj)
  2040 
  2041 end