src/HOL/Finite_Set.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 14504 7a3d80e276d4
child 14661 9ead82084de8
permissions -rw-r--r--
use more symbols in HTML output
     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     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6 *)
     7 
     8 header {* Finite sets *}
     9 
    10 theory Finite_Set = Divides + Power + Inductive:
    11 
    12 subsection {* Collection of finite sets *}
    13 
    14 consts Finites :: "'a set set"
    15 syntax
    16   finite :: "'a set => bool"
    17 translations
    18   "finite A" == "A : Finites"
    19 
    20 inductive Finites
    21   intros
    22     emptyI [simp, intro!]: "{} : Finites"
    23     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    24 
    25 axclass finite \<subseteq> type
    26   finite: "finite UNIV"
    27 
    28 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    29  "[| ~finite(UNIV::'a set); finite A  |] ==> \<exists>a::'a. a \<notin> A"
    30 by(subgoal_tac "A \<noteq> UNIV", blast, blast)
    31 
    32 
    33 lemma finite_induct [case_names empty insert, induct set: Finites]:
    34   "finite F ==>
    35     P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    36   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    37 proof -
    38   assume "P {}" and
    39     insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    40   assume "finite F"
    41   thus "P F"
    42   proof induct
    43     show "P {}" .
    44     fix F x assume F: "finite F" and P: "P F"
    45     show "P (insert x F)"
    46     proof cases
    47       assume "x \<in> F"
    48       hence "insert x F = F" by (rule insert_absorb)
    49       with P show ?thesis by (simp only:)
    50     next
    51       assume "x \<notin> F"
    52       from F this P show ?thesis by (rule insert)
    53     qed
    54   qed
    55 qed
    56 
    57 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    58   "finite F ==> F \<subseteq> A ==>
    59     P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    60     P F"
    61 proof -
    62   assume "P {}" and insert:
    63     "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    64   assume "finite F"
    65   thus "F \<subseteq> A ==> P F"
    66   proof induct
    67     show "P {}" .
    68     fix F x assume "finite F" and "x \<notin> F"
    69       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    70     show "P (insert x F)"
    71     proof (rule insert)
    72       from i show "x \<in> A" by blast
    73       from i have "F \<subseteq> A" by blast
    74       with P show "P F" .
    75     qed
    76   qed
    77 qed
    78 
    79 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
    80   -- {* The union of two finite sets is finite. *}
    81   by (induct set: Finites) simp_all
    82 
    83 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
    84   -- {* Every subset of a finite set is finite. *}
    85 proof -
    86   assume "finite B"
    87   thus "!!A. A \<subseteq> B ==> finite A"
    88   proof induct
    89     case empty
    90     thus ?case by simp
    91   next
    92     case (insert F x A)
    93     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
    94     show "finite A"
    95     proof cases
    96       assume x: "x \<in> A"
    97       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
    98       with r have "finite (A - {x})" .
    99       hence "finite (insert x (A - {x}))" ..
   100       also have "insert x (A - {x}) = A" by (rule insert_Diff)
   101       finally show ?thesis .
   102     next
   103       show "A \<subseteq> F ==> ?thesis" .
   104       assume "x \<notin> A"
   105       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   106     qed
   107   qed
   108 qed
   109 
   110 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   111   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   112 
   113 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   114   -- {* The converse obviously fails. *}
   115   by (blast intro: finite_subset)
   116 
   117 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   118   apply (subst insert_is_Un)
   119   apply (simp only: finite_Un, blast)
   120   done
   121 
   122 lemma finite_empty_induct:
   123   "finite A ==>
   124   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
   125 proof -
   126   assume "finite A"
   127     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   128   have "P (A - A)"
   129   proof -
   130     fix c b :: "'a set"
   131     presume c: "finite c" and b: "finite b"
   132       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   133     from c show "c \<subseteq> b ==> P (b - c)"
   134     proof induct
   135       case empty
   136       from P1 show ?case by simp
   137     next
   138       case (insert F x)
   139       have "P (b - F - {x})"
   140       proof (rule P2)
   141         from _ b show "finite (b - F)" by (rule finite_subset) blast
   142         from insert show "x \<in> b - F" by simp
   143         from insert show "P (b - F)" by simp
   144       qed
   145       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   146       finally show ?case .
   147     qed
   148   next
   149     show "A \<subseteq> A" ..
   150   qed
   151   thus "P {}" by simp
   152 qed
   153 
   154 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   155   by (rule Diff_subset [THEN finite_subset])
   156 
   157 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   158   apply (subst Diff_insert)
   159   apply (case_tac "a : A - B")
   160    apply (rule finite_insert [symmetric, THEN trans])
   161    apply (subst insert_Diff, simp_all)
   162   done
   163 
   164 
   165 subsubsection {* Image and Inverse Image over Finite Sets *}
   166 
   167 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   168   -- {* The image of a finite set is finite. *}
   169   by (induct set: Finites) simp_all
   170 
   171 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   172   apply (frule finite_imageI)
   173   apply (erule finite_subset, assumption)
   174   done
   175 
   176 lemma finite_range_imageI:
   177     "finite (range g) ==> finite (range (%x. f (g x)))"
   178   apply (drule finite_imageI, simp)
   179   done
   180 
   181 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   182 proof -
   183   have aux: "!!A. finite (A - {}) = finite A" by simp
   184   fix B :: "'a set"
   185   assume "finite B"
   186   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   187     apply induct
   188      apply simp
   189     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   190      apply clarify
   191      apply (simp (no_asm_use) add: inj_on_def)
   192      apply (blast dest!: aux [THEN iffD1], atomize)
   193     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   194     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   195     apply (rule_tac x = xa in bexI)
   196      apply (simp_all add: inj_on_image_set_diff)
   197     done
   198 qed (rule refl)
   199 
   200 
   201 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   202   -- {* The inverse image of a singleton under an injective function
   203          is included in a singleton. *}
   204   apply (auto simp add: inj_on_def)
   205   apply (blast intro: the_equality [symmetric])
   206   done
   207 
   208 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   209   -- {* The inverse image of a finite set under an injective function
   210          is finite. *}
   211   apply (induct set: Finites, simp_all)
   212   apply (subst vimage_insert)
   213   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   214   done
   215 
   216 
   217 subsubsection {* The finite UNION of finite sets *}
   218 
   219 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   220   by (induct set: Finites) simp_all
   221 
   222 text {*
   223   Strengthen RHS to
   224   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   225 
   226   We'd need to prove
   227   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   228   by induction. *}
   229 
   230 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   231   by (blast intro: finite_UN_I finite_subset)
   232 
   233 
   234 subsubsection {* Sigma of finite sets *}
   235 
   236 lemma finite_SigmaI [simp]:
   237     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   238   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   239 
   240 lemma finite_Prod_UNIV:
   241     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   242   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   243    apply (erule ssubst)
   244    apply (erule finite_SigmaI, auto)
   245   done
   246 
   247 instance unit :: finite
   248 proof
   249   have "finite {()}" by simp
   250   also have "{()} = UNIV" by auto
   251   finally show "finite (UNIV :: unit set)" .
   252 qed
   253 
   254 instance * :: (finite, finite) finite
   255 proof
   256   show "finite (UNIV :: ('a \<times> 'b) set)"
   257   proof (rule finite_Prod_UNIV)
   258     show "finite (UNIV :: 'a set)" by (rule finite)
   259     show "finite (UNIV :: 'b set)" by (rule finite)
   260   qed
   261 qed
   262 
   263 
   264 subsubsection {* The powerset of a finite set *}
   265 
   266 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   267 proof
   268   assume "finite (Pow A)"
   269   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   270   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   271 next
   272   assume "finite A"
   273   thus "finite (Pow A)"
   274     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   275 qed
   276 
   277 lemma finite_converse [iff]: "finite (r^-1) = finite r"
   278   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   279    apply simp
   280    apply (rule iffI)
   281     apply (erule finite_imageD [unfolded inj_on_def])
   282     apply (simp split add: split_split)
   283    apply (erule finite_imageI)
   284   apply (simp add: converse_def image_def, auto)
   285   apply (rule bexI)
   286    prefer 2 apply assumption
   287   apply simp
   288   done
   289 
   290 
   291 subsubsection {* Finiteness of transitive closure *}
   292 
   293 text {* (Thanks to Sidi Ehmety) *}
   294 
   295 lemma finite_Field: "finite r ==> finite (Field r)"
   296   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   297   apply (induct set: Finites)
   298    apply (auto simp add: Field_def Domain_insert Range_insert)
   299   done
   300 
   301 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   302   apply clarify
   303   apply (erule trancl_induct)
   304    apply (auto simp add: Field_def)
   305   done
   306 
   307 lemma finite_trancl: "finite (r^+) = finite r"
   308   apply auto
   309    prefer 2
   310    apply (rule trancl_subset_Field2 [THEN finite_subset])
   311    apply (rule finite_SigmaI)
   312     prefer 3
   313     apply (blast intro: r_into_trancl' finite_subset)
   314    apply (auto simp add: finite_Field)
   315   done
   316 
   317 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   318     finite (A <*> B)"
   319   by (rule finite_SigmaI)
   320 
   321 
   322 subsection {* Finite cardinality *}
   323 
   324 text {*
   325   This definition, although traditional, is ugly to work with: @{text
   326   "card A == LEAST n. EX f. A = {f i | i. i < n}"}.  Therefore we have
   327   switched to an inductive one:
   328 *}
   329 
   330 consts cardR :: "('a set \<times> nat) set"
   331 
   332 inductive cardR
   333   intros
   334     EmptyI: "({}, 0) : cardR"
   335     InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR"
   336 
   337 constdefs
   338   card :: "'a set => nat"
   339   "card A == THE n. (A, n) : cardR"
   340 
   341 inductive_cases cardR_emptyE: "({}, n) : cardR"
   342 inductive_cases cardR_insertE: "(insert a A,n) : cardR"
   343 
   344 lemma cardR_SucD: "(A, n) : cardR ==> a : A --> (EX m. n = Suc m)"
   345   by (induct set: cardR) simp_all
   346 
   347 lemma cardR_determ_aux1:
   348     "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)"
   349   apply (induct set: cardR, auto)
   350   apply (simp add: insert_Diff_if, auto)
   351   apply (drule cardR_SucD)
   352   apply (blast intro!: cardR.intros)
   353   done
   354 
   355 lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR"
   356   by (drule cardR_determ_aux1) auto
   357 
   358 lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)"
   359   apply (induct set: cardR)
   360    apply (safe elim!: cardR_emptyE cardR_insertE)
   361   apply (rename_tac B b m)
   362   apply (case_tac "a = b")
   363    apply (subgoal_tac "A = B")
   364     prefer 2 apply (blast elim: equalityE, blast)
   365   apply (subgoal_tac "EX C. A = insert b C & B = insert a C")
   366    prefer 2
   367    apply (rule_tac x = "A Int B" in exI)
   368    apply (blast elim: equalityE)
   369   apply (frule_tac A = B in cardR_SucD)
   370   apply (blast intro!: cardR.intros dest!: cardR_determ_aux2)
   371   done
   372 
   373 lemma cardR_imp_finite: "(A, n) : cardR ==> finite A"
   374   by (induct set: cardR) simp_all
   375 
   376 lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR"
   377   by (induct set: Finites) (auto intro!: cardR.intros)
   378 
   379 lemma card_equality: "(A,n) : cardR ==> card A = n"
   380   by (unfold card_def) (blast intro: cardR_determ)
   381 
   382 lemma card_empty [simp]: "card {} = 0"
   383   by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE)
   384 
   385 lemma card_insert_disjoint [simp]:
   386   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
   387 proof -
   388   assume x: "x \<notin> A"
   389   hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)"
   390     apply (auto intro!: cardR.intros)
   391     apply (rule_tac A1 = A in finite_imp_cardR [THEN exE])
   392      apply (force dest: cardR_imp_finite)
   393     apply (blast intro!: cardR.intros intro: cardR_determ)
   394     done
   395   assume "finite A"
   396   thus ?thesis
   397     apply (simp add: card_def aux)
   398     apply (rule the_equality)
   399      apply (auto intro: finite_imp_cardR
   400        cong: conj_cong simp: card_def [symmetric] card_equality)
   401     done
   402 qed
   403 
   404 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
   405   apply auto
   406   apply (drule_tac a = x in mk_disjoint_insert, clarify)
   407   apply (rotate_tac -1, auto)
   408   done
   409 
   410 lemma card_insert_if:
   411     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
   412   by (simp add: insert_absorb)
   413 
   414 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
   415 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
   416 apply(simp del:insert_Diff_single)
   417 done
   418 
   419 lemma card_Diff_singleton:
   420     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
   421   by (simp add: card_Suc_Diff1 [symmetric])
   422 
   423 lemma card_Diff_singleton_if:
   424     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
   425   by (simp add: card_Diff_singleton)
   426 
   427 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
   428   by (simp add: card_insert_if card_Suc_Diff1)
   429 
   430 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
   431   by (simp add: card_insert_if)
   432 
   433 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
   434   apply (induct set: Finites, simp, clarify)
   435   apply (subgoal_tac "finite A & A - {x} <= F")
   436    prefer 2 apply (blast intro: finite_subset, atomize)
   437   apply (drule_tac x = "A - {x}" in spec)
   438   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
   439   apply (case_tac "card A", auto)
   440   done
   441 
   442 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
   443   apply (simp add: psubset_def linorder_not_le [symmetric])
   444   apply (blast dest: card_seteq)
   445   done
   446 
   447 lemma card_mono: "finite B ==> A <= B ==> card A <= card B"
   448   apply (case_tac "A = B", simp)
   449   apply (simp add: linorder_not_less [symmetric])
   450   apply (blast dest: card_seteq intro: order_less_imp_le)
   451   done
   452 
   453 lemma card_Un_Int: "finite A ==> finite B
   454     ==> card A + card B = card (A Un B) + card (A Int B)"
   455   apply (induct set: Finites, simp)
   456   apply (simp add: insert_absorb Int_insert_left)
   457   done
   458 
   459 lemma card_Un_disjoint: "finite A ==> finite B
   460     ==> A Int B = {} ==> card (A Un B) = card A + card B"
   461   by (simp add: card_Un_Int)
   462 
   463 lemma card_Diff_subset:
   464     "finite A ==> B <= A ==> card A - card B = card (A - B)"
   465   apply (subgoal_tac "(A - B) Un B = A")
   466    prefer 2 apply blast
   467   apply (rule nat_add_right_cancel [THEN iffD1])
   468   apply (rule card_Un_disjoint [THEN subst])
   469      apply (erule_tac [4] ssubst)
   470      prefer 3 apply blast
   471     apply (simp_all add: add_commute not_less_iff_le
   472       add_diff_inverse card_mono finite_subset)
   473   done
   474 
   475 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
   476   apply (rule Suc_less_SucD)
   477   apply (simp add: card_Suc_Diff1)
   478   done
   479 
   480 lemma card_Diff2_less:
   481     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
   482   apply (case_tac "x = y")
   483    apply (simp add: card_Diff1_less)
   484   apply (rule less_trans)
   485    prefer 2 apply (auto intro!: card_Diff1_less)
   486   done
   487 
   488 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
   489   apply (case_tac "x : A")
   490    apply (simp_all add: card_Diff1_less less_imp_le)
   491   done
   492 
   493 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
   494 by (erule psubsetI, blast)
   495 
   496 
   497 subsubsection {* Cardinality of image *}
   498 
   499 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
   500   apply (induct set: Finites, simp)
   501   apply (simp add: le_SucI finite_imageI card_insert_if)
   502   done
   503 
   504 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
   505   apply (induct set: Finites, simp_all, atomize, safe)
   506    apply (unfold inj_on_def, blast)
   507   apply (subst card_insert_disjoint)
   508     apply (erule finite_imageI, blast, blast)
   509   done
   510 
   511 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   512   by (simp add: card_seteq card_image)
   513 
   514 
   515 subsubsection {* Cardinality of the Powerset *}
   516 
   517 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
   518   apply (induct set: Finites)
   519    apply (simp_all add: Pow_insert)
   520   apply (subst card_Un_disjoint, blast)
   521     apply (blast intro: finite_imageI, blast)
   522   apply (subgoal_tac "inj_on (insert x) (Pow F)")
   523    apply (simp add: card_image Pow_insert)
   524   apply (unfold inj_on_def)
   525   apply (blast elim!: equalityE)
   526   done
   527 
   528 text {*
   529   \medskip Relates to equivalence classes.  Based on a theorem of
   530   F. Kammüller's.  The @{prop "finite C"} premise is redundant.
   531 *}
   532 
   533 lemma dvd_partition:
   534   "finite C ==> finite (Union C) ==>
   535     ALL c : C. k dvd card c ==>
   536     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
   537   k dvd card (Union C)"
   538   apply (induct set: Finites, simp_all, clarify)
   539   apply (subst card_Un_disjoint)
   540   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
   541   done
   542 
   543 
   544 subsection {* A fold functional for finite sets *}
   545 
   546 text {*
   547   For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
   548   f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
   549 *}
   550 
   551 consts
   552   foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
   553 
   554 inductive "foldSet f e"
   555   intros
   556     emptyI [intro]: "({}, e) : foldSet f e"
   557     insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
   558 
   559 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
   560 
   561 constdefs
   562   fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
   563   "fold f e A == THE x. (A, x) : foldSet f e"
   564 
   565 lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
   566 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   567 
   568 lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
   569   by (induct set: foldSet) auto
   570 
   571 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
   572   by (induct set: Finites) auto
   573 
   574 
   575 subsubsection {* Left-commutative operations *}
   576 
   577 locale LC =
   578   fixes f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
   579   assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   580 
   581 lemma (in LC) foldSet_determ_aux:
   582   "ALL A x. card A < n --> (A, x) : foldSet f e -->
   583     (ALL y. (A, y) : foldSet f e --> y = x)"
   584   apply (induct n)
   585    apply (auto simp add: less_Suc_eq)
   586   apply (erule foldSet.cases, blast)
   587   apply (erule foldSet.cases, blast, clarify)
   588   txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   589   apply (erule rev_mp)
   590   apply (simp add: less_Suc_eq_le)
   591   apply (rule impI)
   592   apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   593    apply (subgoal_tac "Aa = Ab")
   594     prefer 2 apply (blast elim!: equalityE, blast)
   595   txt {* case @{prop "xa \<notin> xb"}. *}
   596   apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   597    prefer 2 apply (blast elim!: equalityE, clarify)
   598   apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   599    prefer 2 apply blast
   600   apply (subgoal_tac "card Aa <= card Ab")
   601    prefer 2
   602    apply (rule Suc_le_mono [THEN subst])
   603    apply (simp add: card_Suc_Diff1)
   604   apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
   605   apply (blast intro: foldSet_imp_finite finite_Diff)
   606   apply (frule (1) Diff1_foldSet)
   607   apply (subgoal_tac "ya = f xb x")
   608    prefer 2 apply (blast del: equalityCE)
   609   apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
   610    prefer 2 apply simp
   611   apply (subgoal_tac "yb = f xa x")
   612    prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
   613   apply (simp (no_asm_simp) add: left_commute)
   614   done
   615 
   616 lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
   617   by (blast intro: foldSet_determ_aux [rule_format])
   618 
   619 lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
   620   by (unfold fold_def) (blast intro: foldSet_determ)
   621 
   622 lemma fold_empty [simp]: "fold f e {} = e"
   623   by (unfold fold_def) blast
   624 
   625 lemma (in LC) fold_insert_aux: "x \<notin> A ==>
   626     ((insert x A, v) : foldSet f e) =
   627     (EX y. (A, y) : foldSet f e & v = f x y)"
   628   apply auto
   629   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   630    apply (fastsimp dest: foldSet_imp_finite)
   631   apply (blast intro: foldSet_determ)
   632   done
   633 
   634 lemma (in LC) fold_insert:
   635     "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
   636   apply (unfold fold_def)
   637   apply (simp add: fold_insert_aux)
   638   apply (rule the_equality)
   639   apply (auto intro: finite_imp_foldSet
   640     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   641   done
   642 
   643 lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
   644   apply (induct set: Finites, simp)
   645   apply (simp add: left_commute fold_insert)
   646   done
   647 
   648 lemma (in LC) fold_nest_Un_Int:
   649   "finite A ==> finite B
   650     ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
   651   apply (induct set: Finites, simp)
   652   apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb)
   653   done
   654 
   655 lemma (in LC) fold_nest_Un_disjoint:
   656   "finite A ==> finite B ==> A Int B = {}
   657     ==> fold f e (A Un B) = fold f (fold f e B) A"
   658   by (simp add: fold_nest_Un_Int)
   659 
   660 declare foldSet_imp_finite [simp del]
   661     empty_foldSetE [rule del]  foldSet.intros [rule del]
   662   -- {* Delete rules to do with @{text foldSet} relation. *}
   663 
   664 
   665 
   666 subsubsection {* Commutative monoids *}
   667 
   668 text {*
   669   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   670   instead of @{text "'b => 'a => 'a"}.
   671 *}
   672 
   673 locale ACe =
   674   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   675     and e :: 'a
   676   assumes ident [simp]: "x \<cdot> e = x"
   677     and commute: "x \<cdot> y = y \<cdot> x"
   678     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   679 
   680 lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   681 proof -
   682   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   683   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   684   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   685   finally show ?thesis .
   686 qed
   687 
   688 lemmas (in ACe) AC = assoc commute left_commute
   689 
   690 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
   691 proof -
   692   have "x \<cdot> e = x" by (rule ident)
   693   thus ?thesis by (subst commute)
   694 qed
   695 
   696 lemma (in ACe) fold_Un_Int:
   697   "finite A ==> finite B ==>
   698     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   699   apply (induct set: Finites, simp)
   700   apply (simp add: AC insert_absorb Int_insert_left
   701     LC.fold_insert [OF LC.intro])
   702   done
   703 
   704 lemma (in ACe) fold_Un_disjoint:
   705   "finite A ==> finite B ==> A Int B = {} ==>
   706     fold f e (A Un B) = fold f e A \<cdot> fold f e B"
   707   by (simp add: fold_Un_Int)
   708 
   709 lemma (in ACe) fold_Un_disjoint2:
   710   "finite A ==> finite B ==> A Int B = {} ==>
   711     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
   712 proof -
   713   assume b: "finite B"
   714   assume "finite A"
   715   thus "A Int B = {} ==>
   716     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
   717   proof induct
   718     case empty
   719     thus ?case by simp
   720   next
   721     case (insert F x)
   722     have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
   723       by simp
   724     also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
   725       by (rule LC.fold_insert [OF LC.intro])
   726         (insert b insert, auto simp add: left_commute)
   727     also from insert have "fold (f o g) e (F \<union> B) =
   728       fold (f o g) e F \<cdot> fold (f o g) e B" by blast
   729     also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B"
   730       by (simp add: AC)
   731     also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
   732       by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
   733 	auto simp add: left_commute)
   734     finally show ?case .
   735   qed
   736 qed
   737 
   738 
   739 subsection {* Generalized summation over a set *}
   740 
   741 constdefs
   742   setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
   743   "setsum f A == if finite A then fold (op + o f) 0 A else 0"
   744 
   745 syntax
   746   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
   747 syntax (xsymbols)
   748   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
   749 syntax (HTML output)
   750   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
   751 translations
   752   "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
   753 
   754 
   755 lemma setsum_empty [simp]: "setsum f {} = 0"
   756   by (simp add: setsum_def)
   757 
   758 lemma setsum_insert [simp]:
   759     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   760   by (simp add: setsum_def
   761     LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
   762 
   763 lemma setsum_reindex [rule_format]: "finite B ==>
   764                   inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   765 apply (rule finite_induct, assumption, force)
   766 apply (rule impI, auto)
   767 apply (simp add: inj_on_def)
   768 apply (subgoal_tac "f x \<notin> f ` F")
   769 apply (subgoal_tac "finite (f ` F)")
   770 apply (auto simp add: setsum_insert)
   771 apply (simp add: inj_on_def)
   772   done
   773 
   774 lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
   775     setsum f B = setsum id (f ` B)"
   776 by (auto simp add: setsum_reindex id_o)
   777 
   778 lemma setsum_reindex_cong: "finite A ==> inj_on f A ==> 
   779     B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
   780   by (frule setsum_reindex, assumption, simp)
   781 
   782 lemma setsum_cong:
   783   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   784   apply (case_tac "finite B")
   785    prefer 2 apply (simp add: setsum_def, simp)
   786   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C")
   787    apply simp
   788   apply (erule finite_induct, simp)
   789   apply (simp add: subset_insert_iff, clarify)
   790   apply (subgoal_tac "finite C")
   791    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   792   apply (subgoal_tac "C = insert x (C - {x})")
   793    prefer 2 apply blast
   794   apply (erule ssubst)
   795   apply (drule spec)
   796   apply (erule (1) notE impE)
   797   apply (simp add: Ball_def del:insert_Diff_single)
   798   done
   799 
   800 lemma setsum_0: "setsum (%i. 0) A = 0"
   801   apply (case_tac "finite A")
   802    prefer 2 apply (simp add: setsum_def)
   803   apply (erule finite_induct, auto)
   804   done
   805 
   806 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
   807   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
   808   apply (erule ssubst, rule setsum_0)
   809   apply (rule setsum_cong, auto)
   810   done
   811 
   812 lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A"
   813   -- {* Could allow many @{text "card"} proofs to be simplified. *}
   814   by (induct set: Finites) auto
   815 
   816 lemma setsum_Un_Int: "finite A ==> finite B
   817     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   818   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   819   apply (induct set: Finites, simp)
   820   apply (simp add: plus_ac0 Int_insert_left insert_absorb)
   821   done
   822 
   823 lemma setsum_Un_disjoint: "finite A ==> finite B
   824   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   825   apply (subst setsum_Un_Int [symmetric], auto)
   826   done
   827 
   828 lemma setsum_UN_disjoint:
   829     "finite I ==> (ALL i:I. finite (A i)) ==>
   830         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   831       setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
   832   apply (induct set: Finites, simp, atomize)
   833   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   834    prefer 2 apply blast
   835   apply (subgoal_tac "A x Int UNION F A = {}")
   836    prefer 2 apply blast
   837   apply (simp add: setsum_Un_disjoint)
   838   done
   839 
   840 lemma setsum_Union_disjoint:
   841   "finite C ==> (ALL A:C. finite A) ==>
   842         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   843       setsum f (Union C) = setsum (setsum f) C"
   844   apply (frule setsum_UN_disjoint [of C id f])
   845   apply (unfold Union_def id_def, assumption+)
   846   done
   847 
   848 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
   849     (\<Sum> x:A. (\<Sum> y:B x. f x y)) = 
   850     (\<Sum> z:(SIGMA x:A. B x). f (fst z) (snd z))"
   851   apply (subst Sigma_def)
   852   apply (subst setsum_UN_disjoint)
   853   apply assumption
   854   apply (rule ballI)
   855   apply (drule_tac x = i in bspec, assumption)
   856   apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
   857   apply (rule finite_surj)
   858   apply auto
   859   apply (rule setsum_cong, rule refl)
   860   apply (subst setsum_UN_disjoint)
   861   apply (erule bspec, assumption)
   862   apply auto
   863   done
   864 
   865 lemma setsum_cartesian_product: "finite A ==> finite B ==>
   866     (\<Sum> x:A. (\<Sum> y:B. f x y)) = 
   867     (\<Sum> z:A <*> B. f (fst z) (snd z))"
   868   by (erule setsum_Sigma, auto);
   869 
   870 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   871   apply (case_tac "finite A")
   872    prefer 2 apply (simp add: setsum_def)
   873   apply (erule finite_induct, auto)
   874   apply (simp add: plus_ac0)
   875   done
   876 
   877 subsubsection {* Properties in more restricted classes of structures *}
   878 
   879 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   880   apply (case_tac "finite A")
   881    prefer 2 apply (simp add: setsum_def)
   882   apply (erule rev_mp)
   883   apply (erule finite_induct, auto)
   884   done
   885 
   886 lemma setsum_eq_0_iff [simp]:
   887     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   888   by (induct set: Finites) auto
   889 
   890 lemma setsum_constant_nat [simp]:
   891     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
   892   -- {* Later generalized to any semiring. *}
   893   by (erule finite_induct, auto)
   894 
   895 lemma setsum_Un: "finite A ==> finite B ==>
   896     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   897   -- {* For the natural numbers, we have subtraction. *}
   898   by (subst setsum_Un_Int [symmetric], auto)
   899 
   900 lemma setsum_Un_ring: "finite A ==> finite B ==>
   901     (setsum f (A Un B) :: 'a :: ring) =
   902       setsum f A + setsum f B - setsum f (A Int B)"
   903   by (subst setsum_Un_Int [symmetric], auto)
   904 
   905 lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
   906     (if a:A then setsum f A - f a else setsum f A)"
   907   apply (case_tac "finite A")
   908    prefer 2 apply (simp add: setsum_def)
   909   apply (erule finite_induct)
   910    apply (auto simp add: insert_Diff_if)
   911   apply (drule_tac a = a in mk_disjoint_insert, auto)
   912   done
   913 
   914 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
   915   - setsum f A"
   916   by (induct set: Finites, auto)
   917 
   918 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
   919   setsum f A - setsum g A"
   920   by (simp add: diff_minus setsum_addf setsum_negf)
   921 
   922 lemma setsum_nonneg: "[| finite A;
   923     \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
   924     0 \<le>  setsum f A";
   925   apply (induct set: Finites, auto)
   926   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
   927   apply (blast intro: add_mono)
   928   done
   929 
   930 subsubsection {* Cardinality of unions and Sigma sets *}
   931 
   932 lemma card_UN_disjoint:
   933     "finite I ==> (ALL i:I. finite (A i)) ==>
   934         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   935       card (UNION I A) = setsum (%i. card (A i)) I"
   936   apply (subst card_eq_setsum)
   937   apply (subst finite_UN, assumption+)
   938   apply (subgoal_tac "setsum (%i. card (A i)) I =
   939       setsum (%i. (setsum (%x. 1) (A i))) I")
   940   apply (erule ssubst)
   941   apply (erule setsum_UN_disjoint, assumption+)
   942   apply (rule setsum_cong)
   943   apply simp+
   944   done
   945 
   946 lemma card_Union_disjoint:
   947   "finite C ==> (ALL A:C. finite A) ==>
   948         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   949       card (Union C) = setsum card C"
   950   apply (frule card_UN_disjoint [of C id])
   951   apply (unfold Union_def id_def, assumption+)
   952   done
   953 
   954 lemma SigmaI_insert: "y \<notin> A ==>
   955   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
   956   by auto
   957 
   958 lemma card_cartesian_product_singleton: "finite A ==>
   959     card({x} <*> A) = card(A)"
   960   apply (subgoal_tac "inj_on (%y .(x,y)) A")
   961   apply (frule card_image, assumption)
   962   apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
   963   apply (auto simp add: inj_on_def)
   964   done
   965 
   966 lemma card_SigmaI [rule_format,simp]: "finite A ==>
   967   (ALL a:A. finite (B a)) -->
   968   card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
   969   apply (erule finite_induct, auto)
   970   apply (subst SigmaI_insert, assumption)
   971   apply (subst card_Un_disjoint)
   972   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
   973   done
   974 
   975 lemma card_cartesian_product: "[| finite A; finite B |] ==>
   976   card (A <*> B) = card(A) * card(B)"
   977   by simp
   978 
   979 
   980 subsection {* Generalized product over a set *}
   981 
   982 constdefs
   983   setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
   984   "setprod f A == if finite A then fold (op * o f) 1 A else 1"
   985 
   986 syntax
   987   "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
   988                 ("\<Prod>_:_. _" [0, 51, 10] 10)
   989 
   990 syntax (xsymbols)
   991   "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
   992                 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
   993 syntax (HTML output)
   994   "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
   995                 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
   996 translations
   997   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
   998 
   999 
  1000 lemma setprod_empty [simp]: "setprod f {} = 1"
  1001   by (auto simp add: setprod_def)
  1002 
  1003 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1004     setprod f (insert a A) = f a * setprod f A"
  1005   by (auto simp add: setprod_def LC_def LC.fold_insert
  1006       times_ac1_left_commute)
  1007 
  1008 lemma setprod_reindex [rule_format]: "finite B ==>
  1009                   inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
  1010 apply (rule finite_induct, assumption, force)
  1011 apply (rule impI, auto)
  1012 apply (simp add: inj_on_def)
  1013 apply (subgoal_tac "f x \<notin> f ` F")
  1014 apply (subgoal_tac "finite (f ` F)")
  1015 apply (auto simp add: setprod_insert)
  1016 apply (simp add: inj_on_def)
  1017   done
  1018 
  1019 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
  1020     setprod f B = setprod id (f ` B)"
  1021 by (auto simp add: setprod_reindex id_o)
  1022 
  1023 lemma setprod_reindex_cong: "finite A ==> inj_on f A ==> 
  1024     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1025   by (frule setprod_reindex, assumption, simp)
  1026 
  1027 lemma setprod_cong:
  1028   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1029   apply (case_tac "finite B")
  1030    prefer 2 apply (simp add: setprod_def, simp)
  1031   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
  1032    apply simp
  1033   apply (erule finite_induct, simp)
  1034   apply (simp add: subset_insert_iff, clarify)
  1035   apply (subgoal_tac "finite C")
  1036    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
  1037   apply (subgoal_tac "C = insert x (C - {x})")
  1038    prefer 2 apply blast
  1039   apply (erule ssubst)
  1040   apply (drule spec)
  1041   apply (erule (1) notE impE)
  1042   apply (simp add: Ball_def del:insert_Diff_single)
  1043   done
  1044 
  1045 lemma setprod_1: "setprod (%i. 1) A = 1"
  1046   apply (case_tac "finite A")
  1047   apply (erule finite_induct, auto simp add: times_ac1)
  1048   apply (simp add: setprod_def)
  1049   done
  1050 
  1051 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1052   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1053   apply (erule ssubst, rule setprod_1)
  1054   apply (rule setprod_cong, auto)
  1055   done
  1056 
  1057 lemma setprod_Un_Int: "finite A ==> finite B
  1058     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1059   apply (induct set: Finites, simp)
  1060   apply (simp add: times_ac1 insert_absorb)
  1061   apply (simp add: times_ac1 Int_insert_left insert_absorb)
  1062   done
  1063 
  1064 lemma setprod_Un_disjoint: "finite A ==> finite B
  1065   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1066   apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
  1067   done
  1068 
  1069 lemma setprod_UN_disjoint:
  1070     "finite I ==> (ALL i:I. finite (A i)) ==>
  1071         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1072       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1073   apply (induct set: Finites, simp, atomize)
  1074   apply (subgoal_tac "ALL i:F. x \<noteq> i")
  1075    prefer 2 apply blast
  1076   apply (subgoal_tac "A x Int UNION F A = {}")
  1077    prefer 2 apply blast
  1078   apply (simp add: setprod_Un_disjoint)
  1079   done
  1080 
  1081 lemma setprod_Union_disjoint:
  1082   "finite C ==> (ALL A:C. finite A) ==>
  1083         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1084       setprod f (Union C) = setprod (setprod f) C"
  1085   apply (frule setprod_UN_disjoint [of C id f])
  1086   apply (unfold Union_def id_def, assumption+)
  1087   done
  1088 
  1089 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
  1090     (\<Prod> x:A. (\<Prod> y: B x. f x y)) = 
  1091     (\<Prod> z:(SIGMA x:A. B x). f (fst z) (snd z))"
  1092   apply (subst Sigma_def)
  1093   apply (subst setprod_UN_disjoint)
  1094   apply assumption
  1095   apply (rule ballI)
  1096   apply (drule_tac x = i in bspec, assumption)
  1097   apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
  1098   apply (rule finite_surj)
  1099   apply auto
  1100   apply (rule setprod_cong, rule refl)
  1101   apply (subst setprod_UN_disjoint)
  1102   apply (erule bspec, assumption)
  1103   apply auto
  1104   done
  1105 
  1106 lemma setprod_cartesian_product: "finite A ==> finite B ==> 
  1107     (\<Prod> x:A. (\<Prod> y: B. f x y)) = 
  1108     (\<Prod> z:(A <*> B). f (fst z) (snd z))"
  1109   by (erule setprod_Sigma, auto)
  1110 
  1111 lemma setprod_timesf: "setprod (%x. f x * g x) A =
  1112     (setprod f A * setprod g A)"
  1113   apply (case_tac "finite A")
  1114    prefer 2 apply (simp add: setprod_def times_ac1)
  1115   apply (erule finite_induct, auto)
  1116   apply (simp add: times_ac1)
  1117   done
  1118 
  1119 subsubsection {* Properties in more restricted classes of structures *}
  1120 
  1121 lemma setprod_eq_1_iff [simp]:
  1122     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1123   by (induct set: Finites) auto
  1124 
  1125 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
  1126     y^(card A)"
  1127   apply (erule finite_induct)
  1128   apply (auto simp add: power_Suc)
  1129   done
  1130 
  1131 lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
  1132     setprod f A = 0"
  1133   apply (induct set: Finites, force, clarsimp)
  1134   apply (erule disjE, auto)
  1135   done
  1136 
  1137 lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
  1138      --> 0 \<le> setprod f A"
  1139   apply (case_tac "finite A")
  1140   apply (induct set: Finites, force, clarsimp)
  1141   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1142   apply (rule mult_mono, assumption+)
  1143   apply (auto simp add: setprod_def)
  1144   done
  1145 
  1146 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
  1147      --> 0 < setprod f A"
  1148   apply (case_tac "finite A")
  1149   apply (induct set: Finites, force, clarsimp)
  1150   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1151   apply (rule mult_strict_mono, assumption+)
  1152   apply (auto simp add: setprod_def)
  1153   done
  1154 
  1155 lemma setprod_nonzero [rule_format]:
  1156     "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
  1157       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1158   apply (erule finite_induct, auto)
  1159   done
  1160 
  1161 lemma setprod_zero_eq:
  1162     "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
  1163      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1164   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1165   done
  1166 
  1167 lemma setprod_nonzero_field:
  1168     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1169   apply (rule setprod_nonzero, auto)
  1170   done
  1171 
  1172 lemma setprod_zero_eq_field:
  1173     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1174   apply (rule setprod_zero_eq, auto)
  1175   done
  1176 
  1177 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1178     (setprod f (A Un B) :: 'a ::{field})
  1179       = setprod f A * setprod f B / setprod f (A Int B)"
  1180   apply (subst setprod_Un_Int [symmetric], auto)
  1181   apply (subgoal_tac "finite (A Int B)")
  1182   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1183   apply (subst times_divide_eq_right [THEN sym], auto)
  1184   done
  1185 
  1186 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1187     (setprod f (A - {a}) :: 'a :: {field}) =
  1188       (if a:A then setprod f A / f a else setprod f A)"
  1189   apply (erule finite_induct)
  1190    apply (auto simp add: insert_Diff_if)
  1191   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1192   apply (erule ssubst)
  1193   apply (subst times_divide_eq_right [THEN sym])
  1194   apply (auto simp add: mult_ac)
  1195   done
  1196 
  1197 lemma setprod_inversef: "finite A ==>
  1198     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1199       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1200   apply (erule finite_induct)
  1201   apply (simp, simp)
  1202   done
  1203 
  1204 lemma setprod_dividef:
  1205      "[|finite A;
  1206         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1207       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1208   apply (subgoal_tac
  1209          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1210   apply (erule ssubst)
  1211   apply (subst divide_inverse)
  1212   apply (subst setprod_timesf)
  1213   apply (subst setprod_inversef, assumption+, rule refl)
  1214   apply (rule setprod_cong, rule refl)
  1215   apply (subst divide_inverse, auto)
  1216   done
  1217 
  1218 
  1219 subsection{* Min and Max of finite linearly ordered sets *}
  1220 
  1221 text{* Seemed easier to define directly than via fold. *}
  1222 
  1223 lemma ex_Max: fixes S :: "('a::linorder)set"
  1224   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
  1225 using fin
  1226 proof (induct)
  1227   case empty thus ?case by simp
  1228 next
  1229   case (insert S x)
  1230   show ?case
  1231   proof (cases)
  1232     assume "S = {}" thus ?thesis by simp
  1233   next
  1234     assume nonempty: "S \<noteq> {}"
  1235     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
  1236     show ?thesis
  1237     proof (cases)
  1238       assume "x \<le> m" thus ?thesis using m by blast
  1239     next
  1240       assume "~ x \<le> m" thus ?thesis using m
  1241 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
  1242     qed
  1243   qed
  1244 qed
  1245 
  1246 lemma ex_Min: fixes S :: "('a::linorder)set"
  1247   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
  1248 using fin
  1249 proof (induct)
  1250   case empty thus ?case by simp
  1251 next
  1252   case (insert S x)
  1253   show ?case
  1254   proof (cases)
  1255     assume "S = {}" thus ?thesis by simp
  1256   next
  1257     assume nonempty: "S \<noteq> {}"
  1258     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
  1259     show ?thesis
  1260     proof (cases)
  1261       assume "m \<le> x" thus ?thesis using m by blast
  1262     next
  1263       assume "~ m \<le> x" thus ?thesis using m
  1264 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
  1265     qed
  1266   qed
  1267 qed
  1268 
  1269 constdefs
  1270  Min :: "('a::linorder)set => 'a"
  1271 "Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
  1272 
  1273  Max :: "('a::linorder)set => 'a"
  1274 "Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
  1275 
  1276 lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
  1277                  shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
  1278 proof (unfold Min_def, rule theI')
  1279   show "\<exists>!m. ?P m"
  1280   proof (rule ex_ex1I)
  1281     show "\<exists>m. ?P m" using ex_Min[OF a] by blast
  1282   next
  1283     fix m1 m2 assume "?P m1" "?P m2"
  1284     thus "m1 = m2" by (blast dest:order_antisym)
  1285   qed
  1286 qed
  1287 
  1288 lemma Max[simp]: assumes a: "finite S" "S \<noteq> {}"
  1289                  shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
  1290 proof (unfold Max_def, rule theI')
  1291   show "\<exists>!m. ?P m"
  1292   proof (rule ex_ex1I)
  1293     show "\<exists>m. ?P m" using ex_Max[OF a] by blast
  1294   next
  1295     fix m1 m2 assume "?P m1" "?P m2"
  1296     thus "m1 = m2" by (blast dest:order_antisym)
  1297   qed
  1298 qed
  1299 
  1300 subsection {* Theorems about @{text "choose"} *}
  1301 
  1302 text {*
  1303   \medskip Basic theorem about @{text "choose"}.  By Florian
  1304   Kammüller, tidied by LCP.
  1305 *}
  1306 
  1307 lemma card_s_0_eq_empty:
  1308     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  1309   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  1310   apply (simp cong add: rev_conj_cong)
  1311   done
  1312 
  1313 lemma choose_deconstruct: "finite M ==> x \<notin> M
  1314   ==> {s. s <= insert x M & card(s) = Suc k}
  1315        = {s. s <= M & card(s) = Suc k} Un
  1316          {s. EX t. t <= M & card(t) = k & s = insert x t}"
  1317   apply safe
  1318    apply (auto intro: finite_subset [THEN card_insert_disjoint])
  1319   apply (drule_tac x = "xa - {x}" in spec)
  1320   apply (subgoal_tac "x \<notin> xa", auto)
  1321   apply (erule rev_mp, subst card_Diff_singleton)
  1322   apply (auto intro: finite_subset)
  1323   done
  1324 
  1325 lemma card_inj_on_le:
  1326     "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
  1327   by (auto intro: card_mono simp add: card_image [symmetric])
  1328 
  1329 lemma card_bij_eq:
  1330     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1331        finite A; finite B |] ==> card A = card B"
  1332   by (auto intro: le_anti_sym card_inj_on_le)
  1333 
  1334 text{*There are as many subsets of @{term A} having cardinality @{term k}
  1335  as there are sets obtained from the former by inserting a fixed element
  1336  @{term x} into each.*}
  1337 lemma constr_bij:
  1338    "[|finite A; x \<notin> A|] ==>
  1339     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  1340     card {B. B <= A & card(B) = k}"
  1341   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  1342        apply (auto elim!: equalityE simp add: inj_on_def)
  1343     apply (subst Diff_insert0, auto)
  1344    txt {* finiteness of the two sets *}
  1345    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  1346    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  1347    apply fast+
  1348   done
  1349 
  1350 text {*
  1351   Main theorem: combinatorial statement about number of subsets of a set.
  1352 *}
  1353 
  1354 lemma n_sub_lemma:
  1355   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1356   apply (induct k)
  1357    apply (simp add: card_s_0_eq_empty, atomize)
  1358   apply (rotate_tac -1, erule finite_induct)
  1359    apply (simp_all (no_asm_simp) cong add: conj_cong
  1360      add: card_s_0_eq_empty choose_deconstruct)
  1361   apply (subst card_Un_disjoint)
  1362      prefer 4 apply (force simp add: constr_bij)
  1363     prefer 3 apply force
  1364    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1365      finite_subset [of _ "Pow (insert x F)", standard])
  1366   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1367   done
  1368 
  1369 theorem n_subsets:
  1370     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1371   by (simp add: n_sub_lemma)
  1372 
  1373 
  1374 end