src/HOL/Finite_Set.thy
changeset 16733 236dfafbeb63
parent 16632 ad2895beef79
child 16760 5c5f051aaaaa
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Jul 07 12:36:56 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Jul 07 12:39:17 2005 +0200
     1.3 @@ -891,8 +891,9 @@
     1.4    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
     1.5  by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
     1.6  
     1.7 -lemma strong_setsum_cong:
     1.8 -  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setsum f A = setsum g B"
     1.9 +lemma strong_setsum_cong[cong]:
    1.10 +  "A = B ==> (!!x. x:B =simp=> f x = g x)
    1.11 +   ==> setsum (%x. f x) A = setsum (%x. g x) B"
    1.12  by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
    1.13  
    1.14  lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
    1.15 @@ -1704,71 +1705,6 @@
    1.16    done
    1.17  
    1.18  
    1.19 -subsubsection {* Theorems about @{text "choose"} *}
    1.20 -
    1.21 -text {*
    1.22 -  \medskip Basic theorem about @{text "choose"}.  By Florian
    1.23 -  Kamm\"uller, tidied by LCP.
    1.24 -*}
    1.25 -
    1.26 -lemma card_s_0_eq_empty:
    1.27 -    "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
    1.28 -  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
    1.29 -  apply (simp cong add: rev_conj_cong)
    1.30 -  done
    1.31 -
    1.32 -lemma choose_deconstruct: "finite M ==> x \<notin> M
    1.33 -  ==> {s. s <= insert x M & card(s) = Suc k}
    1.34 -       = {s. s <= M & card(s) = Suc k} Un
    1.35 -         {s. EX t. t <= M & card(t) = k & s = insert x t}"
    1.36 -  apply safe
    1.37 -   apply (auto intro: finite_subset [THEN card_insert_disjoint])
    1.38 -  apply (drule_tac x = "xa - {x}" in spec)
    1.39 -  apply (subgoal_tac "x \<notin> xa", auto)
    1.40 -  apply (erule rev_mp, subst card_Diff_singleton)
    1.41 -  apply (auto intro: finite_subset)
    1.42 -  done
    1.43 -
    1.44 -text{*There are as many subsets of @{term A} having cardinality @{term k}
    1.45 - as there are sets obtained from the former by inserting a fixed element
    1.46 - @{term x} into each.*}
    1.47 -lemma constr_bij:
    1.48 -   "[|finite A; x \<notin> A|] ==>
    1.49 -    card {B. EX C. C <= A & card(C) = k & B = insert x C} =
    1.50 -    card {B. B <= A & card(B) = k}"
    1.51 -  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
    1.52 -       apply (auto elim!: equalityE simp add: inj_on_def)
    1.53 -    apply (subst Diff_insert0, auto)
    1.54 -   txt {* finiteness of the two sets *}
    1.55 -   apply (rule_tac [2] B = "Pow (A)" in finite_subset)
    1.56 -   apply (rule_tac B = "Pow (insert x A)" in finite_subset)
    1.57 -   apply fast+
    1.58 -  done
    1.59 -
    1.60 -text {*
    1.61 -  Main theorem: combinatorial statement about number of subsets of a set.
    1.62 -*}
    1.63 -
    1.64 -lemma n_sub_lemma:
    1.65 -  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
    1.66 -  apply (induct k)
    1.67 -   apply (simp add: card_s_0_eq_empty, atomize)
    1.68 -  apply (rotate_tac -1, erule finite_induct)
    1.69 -   apply (simp_all (no_asm_simp) cong add: conj_cong
    1.70 -     add: card_s_0_eq_empty choose_deconstruct)
    1.71 -  apply (subst card_Un_disjoint)
    1.72 -     prefer 4 apply (force simp add: constr_bij)
    1.73 -    prefer 3 apply force
    1.74 -   prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
    1.75 -     finite_subset [of _ "Pow (insert x F)", standard])
    1.76 -  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
    1.77 -  done
    1.78 -
    1.79 -theorem n_subsets:
    1.80 -    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
    1.81 -  by (simp add: n_sub_lemma)
    1.82 -
    1.83 -
    1.84  subsection{* A fold functional for non-empty sets *}
    1.85  
    1.86  text{* Does not require start value. *}