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