src/HOL/Finite_Set.thy
author nipkow
Fri Dec 19 04:28:45 2003 +0100 (2003-12-19)
changeset 14302 6c24235e8d5d
parent 14208 144f45277d5a
child 14331 8dbbb7cf3637
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/Finite_Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Finite sets *}
     8 
     9 theory Finite_Set = Divides + Power + Inductive + SetInterval:
    10 
    11 subsection {* Collection of finite sets *}
    12 
    13 consts Finites :: "'a set set"
    14 syntax
    15   finite :: "'a set => bool"
    16 translations
    17   "finite A" == "A : Finites"
    18 
    19 inductive Finites
    20   intros
    21     emptyI [simp, intro!]: "{} : Finites"
    22     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    23 
    24 axclass finite \<subseteq> type
    25   finite: "finite UNIV"
    26 
    27 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    28  "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
    29 by(subgoal_tac "A ~= UNIV", blast, blast)
    30 
    31 
    32 lemma finite_induct [case_names empty insert, induct set: Finites]:
    33   "finite F ==>
    34     P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    35   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    36 proof -
    37   assume "P {}" and
    38     insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    39   assume "finite F"
    40   thus "P F"
    41   proof induct
    42     show "P {}" .
    43     fix F x assume F: "finite F" and P: "P F"
    44     show "P (insert x F)"
    45     proof cases
    46       assume "x \<in> F"
    47       hence "insert x F = F" by (rule insert_absorb)
    48       with P show ?thesis by (simp only:)
    49     next
    50       assume "x \<notin> F"
    51       from F this P show ?thesis by (rule insert)
    52     qed
    53   qed
    54 qed
    55 
    56 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    57   "finite F ==> F \<subseteq> A ==>
    58     P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    59     P F"
    60 proof -
    61   assume "P {}" and insert:
    62     "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    63   assume "finite F"
    64   thus "F \<subseteq> A ==> P F"
    65   proof induct
    66     show "P {}" .
    67     fix F x assume "finite F" and "x \<notin> F"
    68       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    69     show "P (insert x F)"
    70     proof (rule insert)
    71       from i show "x \<in> A" by blast
    72       from i have "F \<subseteq> A" by blast
    73       with P show "P F" .
    74     qed
    75   qed
    76 qed
    77 
    78 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
    79   -- {* The union of two finite sets is finite. *}
    80   by (induct set: Finites) simp_all
    81 
    82 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
    83   -- {* Every subset of a finite set is finite. *}
    84 proof -
    85   assume "finite B"
    86   thus "!!A. A \<subseteq> B ==> finite A"
    87   proof induct
    88     case empty
    89     thus ?case by simp
    90   next
    91     case (insert F x A)
    92     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
    93     show "finite A"
    94     proof cases
    95       assume x: "x \<in> A"
    96       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
    97       with r have "finite (A - {x})" .
    98       hence "finite (insert x (A - {x}))" ..
    99       also have "insert x (A - {x}) = A" by (rule insert_Diff)
   100       finally show ?thesis .
   101     next
   102       show "A \<subseteq> F ==> ?thesis" .
   103       assume "x \<notin> A"
   104       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   105     qed
   106   qed
   107 qed
   108 
   109 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   110   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   111 
   112 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   113   -- {* The converse obviously fails. *}
   114   by (blast intro: finite_subset)
   115 
   116 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   117   apply (subst insert_is_Un)
   118   apply (simp only: finite_Un, blast)
   119   done
   120 
   121 lemma finite_empty_induct:
   122   "finite A ==>
   123   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
   124 proof -
   125   assume "finite A"
   126     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   127   have "P (A - A)"
   128   proof -
   129     fix c b :: "'a set"
   130     presume c: "finite c" and b: "finite b"
   131       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   132     from c show "c \<subseteq> b ==> P (b - c)"
   133     proof induct
   134       case empty
   135       from P1 show ?case by simp
   136     next
   137       case (insert F x)
   138       have "P (b - F - {x})"
   139       proof (rule P2)
   140         from _ b show "finite (b - F)" by (rule finite_subset) blast
   141         from insert show "x \<in> b - F" by simp
   142         from insert show "P (b - F)" by simp
   143       qed
   144       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   145       finally show ?case .
   146     qed
   147   next
   148     show "A \<subseteq> A" ..
   149   qed
   150   thus "P {}" by simp
   151 qed
   152 
   153 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   154   by (rule Diff_subset [THEN finite_subset])
   155 
   156 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   157   apply (subst Diff_insert)
   158   apply (case_tac "a : A - B")
   159    apply (rule finite_insert [symmetric, THEN trans])
   160    apply (subst insert_Diff, simp_all)
   161   done
   162 
   163 
   164 subsubsection {* Image and Inverse Image over Finite Sets *}
   165 
   166 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   167   -- {* The image of a finite set is finite. *}
   168   by (induct set: Finites) simp_all
   169 
   170 lemma finite_range_imageI:
   171     "finite (range g) ==> finite (range (%x. f (g x)))"
   172   apply (drule finite_imageI, simp)
   173   done
   174 
   175 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   176 proof -
   177   have aux: "!!A. finite (A - {}) = finite A" by simp
   178   fix B :: "'a set"
   179   assume "finite B"
   180   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   181     apply induct
   182      apply simp
   183     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   184      apply clarify
   185      apply (simp (no_asm_use) add: inj_on_def)
   186      apply (blast dest!: aux [THEN iffD1], atomize)
   187     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   188     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   189     apply (rule_tac x = xa in bexI)
   190      apply (simp_all add: inj_on_image_set_diff)
   191     done
   192 qed (rule refl)
   193 
   194 
   195 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   196   -- {* The inverse image of a singleton under an injective function
   197          is included in a singleton. *}
   198   apply (auto simp add: inj_on_def) 
   199   apply (blast intro: the_equality [symmetric]) 
   200   done
   201 
   202 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   203   -- {* The inverse image of a finite set under an injective function
   204          is finite. *}
   205   apply (induct set: Finites, simp_all) 
   206   apply (subst vimage_insert) 
   207   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
   208   done
   209 
   210 
   211 subsubsection {* The finite UNION of finite sets *}
   212 
   213 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   214   by (induct set: Finites) simp_all
   215 
   216 text {*
   217   Strengthen RHS to
   218   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})"}?
   219 
   220   We'd need to prove
   221   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}"}
   222   by induction. *}
   223 
   224 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   225   by (blast intro: finite_UN_I finite_subset)
   226 
   227 
   228 subsubsection {* Sigma of finite sets *}
   229 
   230 lemma finite_SigmaI [simp]:
   231     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   232   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   233 
   234 lemma finite_Prod_UNIV:
   235     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   236   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   237    apply (erule ssubst)
   238    apply (erule finite_SigmaI, auto)
   239   done
   240 
   241 instance unit :: finite
   242 proof
   243   have "finite {()}" by simp
   244   also have "{()} = UNIV" by auto
   245   finally show "finite (UNIV :: unit set)" .
   246 qed
   247 
   248 instance * :: (finite, finite) finite
   249 proof
   250   show "finite (UNIV :: ('a \<times> 'b) set)"
   251   proof (rule finite_Prod_UNIV)
   252     show "finite (UNIV :: 'a set)" by (rule finite)
   253     show "finite (UNIV :: 'b set)" by (rule finite)
   254   qed
   255 qed
   256 
   257 
   258 subsubsection {* The powerset of a finite set *}
   259 
   260 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   261 proof
   262   assume "finite (Pow A)"
   263   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   264   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   265 next
   266   assume "finite A"
   267   thus "finite (Pow A)"
   268     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   269 qed
   270 
   271 lemma finite_converse [iff]: "finite (r^-1) = finite r"
   272   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   273    apply simp
   274    apply (rule iffI)
   275     apply (erule finite_imageD [unfolded inj_on_def])
   276     apply (simp split add: split_split)
   277    apply (erule finite_imageI)
   278   apply (simp add: converse_def image_def, auto)
   279   apply (rule bexI)
   280    prefer 2 apply assumption
   281   apply simp
   282   done
   283 
   284 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
   285   by (induct k) (simp_all add: lessThan_Suc)
   286 
   287 lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
   288   by (induct k) (simp_all add: atMost_Suc)
   289 
   290 lemma finite_greaterThanLessThan [iff]:
   291   fixes l :: nat shows "finite {)l..u(}"
   292 by (simp add: greaterThanLessThan_def)
   293 
   294 lemma finite_atLeastLessThan [iff]:
   295   fixes l :: nat shows "finite {l..u(}"
   296 by (simp add: atLeastLessThan_def)
   297 
   298 lemma finite_greaterThanAtMost [iff]:
   299   fixes l :: nat shows "finite {)l..u}"
   300 by (simp add: greaterThanAtMost_def)
   301 
   302 lemma finite_atLeastAtMost [iff]:
   303   fixes l :: nat shows "finite {l..u}"
   304 by (simp add: atLeastAtMost_def)
   305 
   306 lemma bounded_nat_set_is_finite:
   307     "(ALL i:N. i < (n::nat)) ==> finite N"
   308   -- {* A bounded set of natural numbers is finite. *}
   309   apply (rule finite_subset)
   310    apply (rule_tac [2] finite_lessThan, auto)
   311   done
   312 
   313 
   314 subsubsection {* Finiteness of transitive closure *}
   315 
   316 text {* (Thanks to Sidi Ehmety) *}
   317 
   318 lemma finite_Field: "finite r ==> finite (Field r)"
   319   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   320   apply (induct set: Finites)
   321    apply (auto simp add: Field_def Domain_insert Range_insert)
   322   done
   323 
   324 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   325   apply clarify
   326   apply (erule trancl_induct)
   327    apply (auto simp add: Field_def)
   328   done
   329 
   330 lemma finite_trancl: "finite (r^+) = finite r"
   331   apply auto
   332    prefer 2
   333    apply (rule trancl_subset_Field2 [THEN finite_subset])
   334    apply (rule finite_SigmaI)
   335     prefer 3
   336     apply (blast intro: r_into_trancl' finite_subset)
   337    apply (auto simp add: finite_Field)
   338   done
   339 
   340 
   341 subsection {* Finite cardinality *}
   342 
   343 text {*
   344   This definition, although traditional, is ugly to work with: @{text
   345   "card A == LEAST n. EX f. A = {f i | i. i < n}"}.  Therefore we have
   346   switched to an inductive one:
   347 *}
   348 
   349 consts cardR :: "('a set \<times> nat) set"
   350 
   351 inductive cardR
   352   intros
   353     EmptyI: "({}, 0) : cardR"
   354     InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR"
   355 
   356 constdefs
   357   card :: "'a set => nat"
   358   "card A == THE n. (A, n) : cardR"
   359 
   360 inductive_cases cardR_emptyE: "({}, n) : cardR"
   361 inductive_cases cardR_insertE: "(insert a A,n) : cardR"
   362 
   363 lemma cardR_SucD: "(A, n) : cardR ==> a : A --> (EX m. n = Suc m)"
   364   by (induct set: cardR) simp_all
   365 
   366 lemma cardR_determ_aux1:
   367     "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)"
   368   apply (induct set: cardR, auto)
   369   apply (simp add: insert_Diff_if, auto)
   370   apply (drule cardR_SucD)
   371   apply (blast intro!: cardR.intros)
   372   done
   373 
   374 lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR"
   375   by (drule cardR_determ_aux1) auto
   376 
   377 lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)"
   378   apply (induct set: cardR)
   379    apply (safe elim!: cardR_emptyE cardR_insertE)
   380   apply (rename_tac B b m)
   381   apply (case_tac "a = b")
   382    apply (subgoal_tac "A = B")
   383     prefer 2 apply (blast elim: equalityE, blast)
   384   apply (subgoal_tac "EX C. A = insert b C & B = insert a C")
   385    prefer 2
   386    apply (rule_tac x = "A Int B" in exI)
   387    apply (blast elim: equalityE)
   388   apply (frule_tac A = B in cardR_SucD)
   389   apply (blast intro!: cardR.intros dest!: cardR_determ_aux2)
   390   done
   391 
   392 lemma cardR_imp_finite: "(A, n) : cardR ==> finite A"
   393   by (induct set: cardR) simp_all
   394 
   395 lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR"
   396   by (induct set: Finites) (auto intro!: cardR.intros)
   397 
   398 lemma card_equality: "(A,n) : cardR ==> card A = n"
   399   by (unfold card_def) (blast intro: cardR_determ)
   400 
   401 lemma card_empty [simp]: "card {} = 0"
   402   by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE)
   403 
   404 lemma card_insert_disjoint [simp]:
   405   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
   406 proof -
   407   assume x: "x \<notin> A"
   408   hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)"
   409     apply (auto intro!: cardR.intros)
   410     apply (rule_tac A1 = A in finite_imp_cardR [THEN exE])
   411      apply (force dest: cardR_imp_finite)
   412     apply (blast intro!: cardR.intros intro: cardR_determ)
   413     done
   414   assume "finite A"
   415   thus ?thesis
   416     apply (simp add: card_def aux)
   417     apply (rule the_equality)
   418      apply (auto intro: finite_imp_cardR
   419        cong: conj_cong simp: card_def [symmetric] card_equality)
   420     done
   421 qed
   422 
   423 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
   424   apply auto
   425   apply (drule_tac a = x in mk_disjoint_insert, clarify)
   426   apply (rotate_tac -1, auto)
   427   done
   428 
   429 lemma card_insert_if:
   430     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
   431   by (simp add: insert_absorb)
   432 
   433 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
   434 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
   435 apply(simp del:insert_Diff_single)
   436 done
   437 
   438 lemma card_Diff_singleton:
   439     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
   440   by (simp add: card_Suc_Diff1 [symmetric])
   441 
   442 lemma card_Diff_singleton_if:
   443     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
   444   by (simp add: card_Diff_singleton)
   445 
   446 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
   447   by (simp add: card_insert_if card_Suc_Diff1)
   448 
   449 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
   450   by (simp add: card_insert_if)
   451 
   452 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
   453   apply (induct set: Finites, simp, clarify)
   454   apply (subgoal_tac "finite A & A - {x} <= F")
   455    prefer 2 apply (blast intro: finite_subset, atomize)
   456   apply (drule_tac x = "A - {x}" in spec)
   457   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
   458   apply (case_tac "card A", auto)
   459   done
   460 
   461 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
   462   apply (simp add: psubset_def linorder_not_le [symmetric])
   463   apply (blast dest: card_seteq)
   464   done
   465 
   466 lemma card_mono: "finite B ==> A <= B ==> card A <= card B"
   467   apply (case_tac "A = B", simp)
   468   apply (simp add: linorder_not_less [symmetric])
   469   apply (blast dest: card_seteq intro: order_less_imp_le)
   470   done
   471 
   472 lemma card_Un_Int: "finite A ==> finite B
   473     ==> card A + card B = card (A Un B) + card (A Int B)"
   474   apply (induct set: Finites, simp)
   475   apply (simp add: insert_absorb Int_insert_left)
   476   done
   477 
   478 lemma card_Un_disjoint: "finite A ==> finite B
   479     ==> A Int B = {} ==> card (A Un B) = card A + card B"
   480   by (simp add: card_Un_Int)
   481 
   482 lemma card_Diff_subset:
   483     "finite A ==> B <= A ==> card A - card B = card (A - B)"
   484   apply (subgoal_tac "(A - B) Un B = A")
   485    prefer 2 apply blast
   486   apply (rule add_right_cancel [THEN iffD1])
   487   apply (rule card_Un_disjoint [THEN subst])
   488      apply (erule_tac [4] ssubst)
   489      prefer 3 apply blast
   490     apply (simp_all add: add_commute not_less_iff_le
   491       add_diff_inverse card_mono finite_subset)
   492   done
   493 
   494 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
   495   apply (rule Suc_less_SucD)
   496   apply (simp add: card_Suc_Diff1)
   497   done
   498 
   499 lemma card_Diff2_less:
   500     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
   501   apply (case_tac "x = y")
   502    apply (simp add: card_Diff1_less)
   503   apply (rule less_trans)
   504    prefer 2 apply (auto intro!: card_Diff1_less)
   505   done
   506 
   507 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
   508   apply (case_tac "x : A")
   509    apply (simp_all add: card_Diff1_less less_imp_le)
   510   done
   511 
   512 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
   513 by (erule psubsetI, blast)
   514 
   515 
   516 subsubsection {* Cardinality of image *}
   517 
   518 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
   519   apply (induct set: Finites, simp)
   520   apply (simp add: le_SucI finite_imageI card_insert_if)
   521   done
   522 
   523 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
   524   apply (induct set: Finites, simp_all, atomize)
   525   apply safe
   526    apply (unfold inj_on_def, blast)
   527   apply (subst card_insert_disjoint)
   528     apply (erule finite_imageI, blast, blast)
   529   done
   530 
   531 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   532   by (simp add: card_seteq card_image)
   533 
   534 
   535 subsubsection {* Cardinality of the Powerset *}
   536 
   537 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
   538   apply (induct set: Finites)
   539    apply (simp_all add: Pow_insert)
   540   apply (subst card_Un_disjoint, blast)
   541     apply (blast intro: finite_imageI, blast)
   542   apply (subgoal_tac "inj_on (insert x) (Pow F)")
   543    apply (simp add: card_image Pow_insert)
   544   apply (unfold inj_on_def)
   545   apply (blast elim!: equalityE)
   546   done
   547 
   548 text {*
   549   \medskip Relates to equivalence classes.  Based on a theorem of
   550   F. Kammüller's.  The @{prop "finite C"} premise is redundant.
   551 *}
   552 
   553 lemma dvd_partition:
   554   "finite C ==> finite (Union C) ==>
   555     ALL c : C. k dvd card c ==>
   556     (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==>
   557   k dvd card (Union C)"
   558   apply (induct set: Finites, simp_all, clarify)
   559   apply (subst card_Un_disjoint)
   560   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
   561   done
   562 
   563 
   564 subsection {* A fold functional for finite sets *}
   565 
   566 text {*
   567   For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
   568   f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
   569 *}
   570 
   571 consts
   572   foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
   573 
   574 inductive "foldSet f e"
   575   intros
   576     emptyI [intro]: "({}, e) : foldSet f e"
   577     insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
   578 
   579 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
   580 
   581 constdefs
   582   fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
   583   "fold f e A == THE x. (A, x) : foldSet f e"
   584 
   585 lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
   586 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   587 
   588 lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
   589   by (induct set: foldSet) auto
   590 
   591 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
   592   by (induct set: Finites) auto
   593 
   594 
   595 subsubsection {* Left-commutative operations *}
   596 
   597 locale LC =
   598   fixes f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
   599   assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   600 
   601 lemma (in LC) foldSet_determ_aux:
   602   "ALL A x. card A < n --> (A, x) : foldSet f e -->
   603     (ALL y. (A, y) : foldSet f e --> y = x)"
   604   apply (induct n)
   605    apply (auto simp add: less_Suc_eq)
   606   apply (erule foldSet.cases, blast)
   607   apply (erule foldSet.cases, blast, clarify)
   608   txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   609   apply (erule rev_mp)
   610   apply (simp add: less_Suc_eq_le)
   611   apply (rule impI)
   612   apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   613    apply (subgoal_tac "Aa = Ab")
   614     prefer 2 apply (blast elim!: equalityE, blast)
   615   txt {* case @{prop "xa \<notin> xb"}. *}
   616   apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   617    prefer 2 apply (blast elim!: equalityE, clarify)
   618   apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   619    prefer 2 apply blast
   620   apply (subgoal_tac "card Aa <= card Ab")
   621    prefer 2
   622    apply (rule Suc_le_mono [THEN subst])
   623    apply (simp add: card_Suc_Diff1)
   624   apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
   625   apply (blast intro: foldSet_imp_finite finite_Diff)
   626   apply (frule (1) Diff1_foldSet)
   627   apply (subgoal_tac "ya = f xb x")
   628    prefer 2 apply (blast del: equalityCE)
   629   apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
   630    prefer 2 apply simp
   631   apply (subgoal_tac "yb = f xa x")
   632    prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
   633   apply (simp (no_asm_simp) add: left_commute)
   634   done
   635 
   636 lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
   637   by (blast intro: foldSet_determ_aux [rule_format])
   638 
   639 lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
   640   by (unfold fold_def) (blast intro: foldSet_determ)
   641 
   642 lemma fold_empty [simp]: "fold f e {} = e"
   643   by (unfold fold_def) blast
   644 
   645 lemma (in LC) fold_insert_aux: "x \<notin> A ==>
   646     ((insert x A, v) : foldSet f e) =
   647     (EX y. (A, y) : foldSet f e & v = f x y)"
   648   apply auto
   649   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   650    apply (fastsimp dest: foldSet_imp_finite)
   651   apply (blast intro: foldSet_determ)
   652   done
   653 
   654 lemma (in LC) fold_insert:
   655     "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
   656   apply (unfold fold_def)
   657   apply (simp add: fold_insert_aux)
   658   apply (rule the_equality)
   659   apply (auto intro: finite_imp_foldSet
   660     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   661   done
   662 
   663 lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
   664   apply (induct set: Finites, simp)
   665   apply (simp add: left_commute fold_insert)
   666   done
   667 
   668 lemma (in LC) fold_nest_Un_Int:
   669   "finite A ==> finite B
   670     ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
   671   apply (induct set: Finites, simp)
   672   apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb)
   673   done
   674 
   675 lemma (in LC) fold_nest_Un_disjoint:
   676   "finite A ==> finite B ==> A Int B = {}
   677     ==> fold f e (A Un B) = fold f (fold f e B) A"
   678   by (simp add: fold_nest_Un_Int)
   679 
   680 declare foldSet_imp_finite [simp del]
   681     empty_foldSetE [rule del]  foldSet.intros [rule del]
   682   -- {* Delete rules to do with @{text foldSet} relation. *}
   683 
   684 
   685 
   686 subsubsection {* Commutative monoids *}
   687 
   688 text {*
   689   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   690   instead of @{text "'b => 'a => 'a"}.
   691 *}
   692 
   693 locale ACe =
   694   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   695     and e :: 'a
   696   assumes ident [simp]: "x \<cdot> e = x"
   697     and commute: "x \<cdot> y = y \<cdot> x"
   698     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   699 
   700 lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   701 proof -
   702   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   703   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   704   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   705   finally show ?thesis .
   706 qed
   707 
   708 lemmas (in ACe) AC = assoc commute left_commute
   709 
   710 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
   711 proof -
   712   have "x \<cdot> e = x" by (rule ident)
   713   thus ?thesis by (subst commute)
   714 qed
   715 
   716 lemma (in ACe) fold_Un_Int:
   717   "finite A ==> finite B ==>
   718     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   719   apply (induct set: Finites, simp)
   720   apply (simp add: AC insert_absorb Int_insert_left
   721     LC.fold_insert [OF LC.intro])
   722   done
   723 
   724 lemma (in ACe) fold_Un_disjoint:
   725   "finite A ==> finite B ==> A Int B = {} ==>
   726     fold f e (A Un B) = fold f e A \<cdot> fold f e B"
   727   by (simp add: fold_Un_Int)
   728 
   729 lemma (in ACe) fold_Un_disjoint2:
   730   "finite A ==> finite B ==> A Int B = {} ==>
   731     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
   732 proof -
   733   assume b: "finite B"
   734   assume "finite A"
   735   thus "A Int B = {} ==>
   736     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
   737   proof induct
   738     case empty
   739     thus ?case by simp
   740   next
   741     case (insert F x)
   742     have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
   743       by simp
   744     also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
   745       by (rule LC.fold_insert [OF LC.intro])
   746         (insert b insert, auto simp add: left_commute)
   747     also from insert have "fold (f o g) e (F \<union> B) =
   748       fold (f o g) e F \<cdot> fold (f o g) e B" by blast
   749     also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B"
   750       by (simp add: AC)
   751     also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
   752       by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
   753 	auto simp add: left_commute)
   754     finally show ?case .
   755   qed
   756 qed
   757 
   758 
   759 subsection {* Generalized summation over a set *}
   760 
   761 constdefs
   762   setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
   763   "setsum f A == if finite A then fold (op + o f) 0 A else 0"
   764 
   765 syntax
   766   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
   767 syntax (xsymbols)
   768   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
   769 translations
   770   "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
   771 
   772 
   773 lemma setsum_empty [simp]: "setsum f {} = 0"
   774   by (simp add: setsum_def)
   775 
   776 lemma setsum_insert [simp]:
   777     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   778   by (simp add: setsum_def
   779     LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
   780 
   781 lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
   782   apply (case_tac "finite A")
   783    prefer 2 apply (simp add: setsum_def)
   784   apply (erule finite_induct, auto)
   785   done
   786 
   787 lemma setsum_eq_0_iff [simp]:
   788     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   789   by (induct set: Finites) auto
   790 
   791 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   792   apply (case_tac "finite A")
   793    prefer 2 apply (simp add: setsum_def)
   794   apply (erule rev_mp)
   795   apply (erule finite_induct, auto)
   796   done
   797 
   798 lemma card_eq_setsum: "finite A ==> card A = setsum (\<lambda>x. 1) A"
   799   -- {* Could allow many @{text "card"} proofs to be simplified. *}
   800   by (induct set: Finites) auto
   801 
   802 lemma setsum_Un_Int: "finite A ==> finite B
   803     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   804   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   805   apply (induct set: Finites, simp)
   806   apply (simp add: plus_ac0 Int_insert_left insert_absorb)
   807   done
   808 
   809 lemma setsum_Un_disjoint: "finite A ==> finite B
   810   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   811   apply (subst setsum_Un_Int [symmetric], auto)
   812   done
   813 
   814 lemma setsum_UN_disjoint:
   815   fixes f :: "'a => 'b::plus_ac0"
   816   shows
   817     "finite I ==> (ALL i:I. finite (A i)) ==>
   818         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   819       setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
   820   apply (induct set: Finites, simp, atomize)
   821   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   822    prefer 2 apply blast
   823   apply (subgoal_tac "A x Int UNION F A = {}")
   824    prefer 2 apply blast
   825   apply (simp add: setsum_Un_disjoint)
   826   done
   827 
   828 lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
   829   apply (case_tac "finite A")
   830    prefer 2 apply (simp add: setsum_def)
   831   apply (erule finite_induct, auto)
   832   apply (simp add: plus_ac0)
   833   done
   834 
   835 lemma setsum_Un: "finite A ==> finite B ==>
   836     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   837   -- {* For the natural numbers, we have subtraction. *}
   838   apply (subst setsum_Un_Int [symmetric], auto)
   839   done
   840 
   841 lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
   842     (if a:A then setsum f A - f a else setsum f A)"
   843   apply (case_tac "finite A")
   844    prefer 2 apply (simp add: setsum_def)
   845   apply (erule finite_induct)
   846    apply (auto simp add: insert_Diff_if)
   847   apply (drule_tac a = a in mk_disjoint_insert, auto)
   848   done
   849 
   850 lemma setsum_cong:
   851   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   852   apply (case_tac "finite B")
   853    prefer 2 apply (simp add: setsum_def, simp)
   854   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C")
   855    apply simp
   856   apply (erule finite_induct, simp)
   857   apply (simp add: subset_insert_iff, clarify)
   858   apply (subgoal_tac "finite C")
   859    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   860   apply (subgoal_tac "C = insert x (C - {x})")
   861    prefer 2 apply blast
   862   apply (erule ssubst)
   863   apply (drule spec)
   864   apply (erule (1) notE impE)
   865   apply (simp add: Ball_def del:insert_Diff_single)
   866   done
   867 
   868 subsubsection{* Min and Max of finite linearly ordered sets *}
   869 
   870 text{* Seemed easier to define directly than via fold. *}
   871 
   872 lemma ex_Max: fixes S :: "('a::linorder)set"
   873   assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
   874 using fin
   875 proof (induct)
   876   case empty thus ?case by simp
   877 next
   878   case (insert S x)
   879   show ?case
   880   proof (cases)
   881     assume "S = {}" thus ?thesis by simp
   882   next
   883     assume nonempty: "S \<noteq> {}"
   884     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
   885     show ?thesis
   886     proof (cases)
   887       assume "x \<le> m" thus ?thesis using m by blast
   888     next
   889       assume "\<not> x \<le> m" thus ?thesis using m
   890 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
   891     qed
   892   qed
   893 qed
   894 
   895 lemma ex_Min: fixes S :: "('a::linorder)set"
   896   assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
   897 using fin
   898 proof (induct)
   899   case empty thus ?case by simp
   900 next
   901   case (insert S x)
   902   show ?case
   903   proof (cases)
   904     assume "S = {}" thus ?thesis by simp
   905   next
   906     assume nonempty: "S \<noteq> {}"
   907     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
   908     show ?thesis
   909     proof (cases)
   910       assume "m \<le> x" thus ?thesis using m by blast
   911     next
   912       assume "\<not> m \<le> x" thus ?thesis using m
   913 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
   914     qed
   915   qed
   916 qed
   917 
   918 constdefs
   919  Min :: "('a::linorder)set \<Rightarrow> 'a"
   920 "Min S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
   921 
   922  Max :: "('a::linorder)set \<Rightarrow> 'a"
   923 "Max S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
   924 
   925 lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
   926                  shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
   927 proof (unfold Min_def, rule theI')
   928   show "\<exists>!m. ?P m"
   929   proof (rule ex_ex1I)
   930     show "\<exists>m. ?P m" using ex_Min[OF a] by blast
   931   next
   932     fix m1 m2 assume "?P m1" "?P m2"
   933     thus "m1 = m2" by (blast dest:order_antisym)
   934   qed
   935 qed
   936 
   937 lemma Max[simp]: assumes a: "finite S" "S \<noteq> {}"
   938                  shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
   939 proof (unfold Max_def, rule theI')
   940   show "\<exists>!m. ?P m"
   941   proof (rule ex_ex1I)
   942     show "\<exists>m. ?P m" using ex_Max[OF a] by blast
   943   next
   944     fix m1 m2 assume "?P m1" "?P m2"
   945     thus "m1 = m2" by (blast dest:order_antisym)
   946   qed
   947 qed
   948 
   949 
   950 text {*
   951   \medskip Basic theorem about @{text "choose"}.  By Florian
   952   Kammüller, tidied by LCP.
   953 *}
   954 
   955 lemma card_s_0_eq_empty:
   956     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
   957   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
   958   apply (simp cong add: rev_conj_cong)
   959   done
   960 
   961 lemma choose_deconstruct: "finite M ==> x \<notin> M
   962   ==> {s. s <= insert x M & card(s) = Suc k}
   963        = {s. s <= M & card(s) = Suc k} Un
   964          {s. EX t. t <= M & card(t) = k & s = insert x t}"
   965   apply safe
   966    apply (auto intro: finite_subset [THEN card_insert_disjoint])
   967   apply (drule_tac x = "xa - {x}" in spec)
   968   apply (subgoal_tac "x ~: xa", auto)
   969   apply (erule rev_mp, subst card_Diff_singleton)
   970   apply (auto intro: finite_subset)
   971   done
   972 
   973 lemma card_inj_on_le:
   974     "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
   975   by (auto intro: card_mono simp add: card_image [symmetric])
   976 
   977 lemma card_bij_eq: 
   978     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; 
   979        finite A; finite B |] ==> card A = card B"
   980   by (auto intro: le_anti_sym card_inj_on_le)
   981 
   982 text{*There are as many subsets of @{term A} having cardinality @{term k}
   983  as there are sets obtained from the former by inserting a fixed element
   984  @{term x} into each.*}
   985 lemma constr_bij:
   986    "[|finite A; x \<notin> A|] ==>
   987     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
   988     card {B. B <= A & card(B) = k}"
   989   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
   990        apply (auto elim!: equalityE simp add: inj_on_def)
   991     apply (subst Diff_insert0, auto)
   992    txt {* finiteness of the two sets *}
   993    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
   994    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
   995    apply fast+
   996   done
   997 
   998 text {*
   999   Main theorem: combinatorial statement about number of subsets of a set.
  1000 *}
  1001 
  1002 lemma n_sub_lemma:
  1003   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1004   apply (induct k)
  1005    apply (simp add: card_s_0_eq_empty, atomize)
  1006   apply (rotate_tac -1, erule finite_induct)
  1007    apply (simp_all (no_asm_simp) cong add: conj_cong
  1008      add: card_s_0_eq_empty choose_deconstruct)
  1009   apply (subst card_Un_disjoint)
  1010      prefer 4 apply (force simp add: constr_bij)
  1011     prefer 3 apply force
  1012    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1013      finite_subset [of _ "Pow (insert x F)", standard])
  1014   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1015   done
  1016 
  1017 theorem n_subsets:
  1018     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1019   by (simp add: n_sub_lemma)
  1020 
  1021 end