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